dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE

value.ml (649B)


      1 module B = Builtin
      2 module I = Internal
      3 
      4 type value =
      5 | RefClo of environment ref * I.term
      6 | NeutralMatch of {
      7 	scrutinee: value;
      8 	cases_clo: I.case array closure;
      9 	switch: I.switch;
     10 }
     11 | NeutralApp of value * value array
     12 | FnClosure of I.abstraction closure
     13 | FnTypeClosure of I.abstraction closure
     14 | Data of {
     15 	tag: Name.Tag.t;
     16 	tagi: int;
     17 	args: value array;
     18 	datatype_clo: I.datatype closure;
     19 }
     20 | DataTypeClosure of I.datatype closure
     21 | Nat of Z.t
     22 | Arb of Uniq.uniq
     23 (*| Meta of ...*)
     24 | Builtin of B.builtin
     25 | Future of Uniq.uniq * int
     26 
     27 and environment = value Env.environment
     28 
     29 and 'a closure = environment * 'a
     30 
     31 type context = value Ctx.context
     32