dtlc

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

concrete.ml (1449B)


      1 open Node
      2 
      3 type binop =
      4 | LOr | LAnd
      5 | Lt  | Le  | Eq  | Ge  | Gt  | Ne
      6 | Add | Sub | Mul | Div | Mod
      7 
      8 type var_name = var_name' node
      9 and var_name' = Name.Var.t
     10 
     11 type tag_name = tag_name' node
     12 and tag_name' = Name.Tag.t
     13 
     14 type term = term' node
     15 and term' =
     16 | Let of definer array * term
     17 | Seq of term * term
     18 | Match of term * case array
     19 | If of cond * term * term
     20 | Iff of cond * term
     21 | Annot of term * term
     22 | BinOp of term * binop * term
     23 | App of term * term array
     24 | Fn of param array * term
     25 | FnType of domain array * term
     26 | Variant of tag_name * term array
     27 | VariantType of ctor array
     28 | Tuple of term array
     29 | TupleType of domain array
     30 | Unit
     31 | Nat of Z.t
     32 | IndexedVar of var_name * int
     33 | Var of var_name
     34 | Paren of term
     35 
     36 and definer = definer' node
     37 and definer' =
     38 | Definer of patt * term
     39 | RecDefiner of patt * term
     40 
     41 and case = case' node
     42 and case' = Case of patt * term
     43 
     44 and cond = cond' node
     45 and cond' =
     46 | TrueCond of term
     47 | PattCond of patt * term
     48 
     49 and param = param' node
     50 and param' = Param of Plicity.t * patt
     51 
     52 and domain = domain' node
     53 and domain' =
     54 | ExplicitDomain of term
     55 | ImplicitTypeDomain of patt
     56 | AnnotDomain of Plicity.t * patt * term
     57 
     58 and ctor = ctor' node
     59 and ctor' = Ctor of tag_name * domain array
     60 
     61 and patt = patt' node
     62 and patt' =
     63 | PWild
     64 | PBind of var_name
     65 | PAnnot of patt * term
     66 | PVariant of tag_name * patt array
     67 | PTuple of patt array
     68 | PUnit
     69 | PNat of Z.t
     70 | PAnd of patt * patt
     71 | POr of patt * patt
     72 | PParen of patt