abstract.ml (1274B)
1 (* Abstract syntax is "desugared" concrete syntax. See desugar.ml. *) 2 3 open Node 4 module B = Builtin 5 6 type var_name = var_name' node 7 and var_name' = Name.Var.t 8 9 type tag_name = tag_name' node 10 and tag_name' = Name.Tag.t 11 12 type term = term' node 13 and term' = 14 | Let of definer array * term 15 | Match of term * case array 16 | Annot of term * term 17 | App of term * term array 18 | Fn of abstraction 19 | FnType of abstraction 20 | Data of tag_name * term array 21 | TupleData of term array (* Can be inferred, unlike regular Data. *) 22 | DataType of multibinder Name.Tag.Map.t 23 | Nat of Z.t 24 | Var of var_name * int 25 | Builtin of B.builtin (* Only arises during desugaring. *) 26 27 and definer = definer' node 28 and definer' = { 29 recursive: bool; 30 lhs: patt; 31 rhs: term; 32 } 33 34 and case = case' node 35 and case' = { 36 patt: patt; 37 body: term; 38 } 39 40 and binder = binder' node 41 and binder' = { 42 plicity: Plicity.t; 43 patt: patt; 44 } 45 46 and multibinder = multibinder' node 47 and multibinder' = binder array 48 49 and abstraction = abstraction' node 50 and abstraction' = { 51 multibinder: multibinder; 52 term: term; 53 } 54 55 and patt = patt' node 56 and patt' = { 57 names: var_name array; 58 typs: term array; 59 disc: discriminant; 60 } 61 62 and discriminant = discriminant' node 63 and discriminant' = 64 | DWild 65 | DData of { 66 tag: tag_name; 67 subpatts: patt array; 68 }