std.ml (1710B)
1 module B = Builtin 2 module I = Internal 3 module V = Value 4 5 let t_Nat: I.term = I.Builtin B.NatType 6 let v_Nat: V.value = V.Builtin B.NatType 7 8 let t_Type: I.term = I.Builtin B.Type 9 let v_Type: V.value = V.Builtin B.Type 10 11 let dt_Bool: I.datatype = 12 { 13 ctors = [| 14 {binders = [||]; order = [||]}; 15 {binders = [||]; order = [||]}; 16 |]; 17 names = Name.Tag.Map.add (Name.Tag.Of "false") 0 18 @@ Name.Tag.Map.add (Name.Tag.Of "true") 1 Name.Tag.Map.empty; 19 } 20 let t_Bool: I.term = I.DataType dt_Bool 21 let v_Bool: V.value = V.DataTypeClosure (Env.empty, dt_Bool) 22 23 let v_false: V.value = 24 V.Data { 25 tag = Name.Tag.Of "false"; 26 tagi = 0; 27 args = [||]; 28 datatype_clo = (Env.empty, dt_Bool); 29 } 30 31 let v_true: V.value = 32 V.Data { 33 tag = Name.Tag.Of "true"; 34 tagi = 1; 35 args = [||]; 36 datatype_clo = (Env.empty, dt_Bool); 37 } 38 39 let v_Nat_Nat_arrow 40 : I.term -> V.value 41 = fun cod -> 42 let nat_binder = { 43 I.plicity = Plicity.Ex; 44 I.patt = { 45 I.names = [||]; 46 I.disc = I.DWild t_Nat; 47 }; 48 } in 49 V.FnTypeClosure (Env.empty, { 50 multibinder = {binders = [|nat_binder; nat_binder|]; order = [|0; 1|]}; 51 term = cod; 52 }) 53 let v_Nat_Nat_arrow_Nat: V.value = v_Nat_Nat_arrow t_Nat 54 let v_Nat_Nat_arrow_Bool: V.value = v_Nat_Nat_arrow t_Bool 55 56 let infer 57 : B.builtin -> V.value 58 = function 59 | B.Type -> v_Type 60 | B.NatType -> v_Type 61 | B.NatOpAdd -> v_Nat_Nat_arrow_Nat 62 | B.NatOpSub -> v_Nat_Nat_arrow_Nat 63 | B.NatOpMul -> v_Nat_Nat_arrow_Nat 64 | B.NatOpDiv -> v_Nat_Nat_arrow_Nat 65 | B.NatOpMod -> v_Nat_Nat_arrow_Nat 66 | B.NatOpLt -> v_Nat_Nat_arrow_Bool 67 | B.NatOpLe -> v_Nat_Nat_arrow_Bool 68 | B.NatOpEq -> v_Nat_Nat_arrow_Bool 69 | B.NatOpGe -> v_Nat_Nat_arrow_Bool 70 | B.NatOpGt -> v_Nat_Nat_arrow_Bool 71 | B.NatOpNe -> v_Nat_Nat_arrow_Bool