main.ml (2670B)
1 open Util 2 open Node 3 module B = Builtin 4 module I = Internal 5 module V = Value 6 7 (* 8 let buf = Lexing.from_string "\ 9 " 10 *) 11 12 (* 13 let buf = Lexing.from_string "\ 14 Bool := #{@false; @true};\n\ 15 T := #(b: Bool, (if b then Nat else Type));\n\ 16 ((@true, 3): T) match {\n\ 17 (@true, n) => n,\n\ 18 (@false, _) => 2,\n\ 19 }: Nat\n\ 20 " 21 *) 22 23 (* 24 let buf = Lexing.from_string "\ 25 fact: Nat -> Nat := rec fn n =>\n\ 26 if n = 0 then 1 else n * fact (n - 1);\n\ 27 fact 6\n\ 28 " 29 *) 30 31 (* 32 let buf = Lexing.from_string "\ 33 Opt := fn A: Type => #{@some A; @none};\n\ 34 div: [Nat, Nat] -> Opt Nat := fn m, n =>\n\ 35 if n = 0 then @none else @some (m / n);\n\ 36 (div 3 0, div 12 3)\n\ 37 " 38 *) 39 40 let default_ctx = 41 let ctx = ref Ctx.empty in 42 let assign s t v = 43 let (ctx', _) = Ctx.assign !ctx [|Name.Var.Of s|] t v in 44 ctx := ctx' in 45 assign "Type" Std.v_Type @@ V.Builtin B.Type; 46 assign "Nat" Std.v_Type @@ V.Builtin B.NatType; 47 assign "+" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpAdd; 48 assign "-" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpSub; 49 assign "*" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpMul; 50 assign "/" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpDiv; 51 assign "%" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpMod; 52 assign "<" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpLt; 53 assign "<=" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpLe; 54 assign "=" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpEq; 55 assign ">=" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpGe; 56 assign ">" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpGt; 57 assign "<>" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpNe; 58 !ctx 59 60 let print_usage () = 61 Format.eprintf "usage: %s (elab|type|eval) PATH@." Sys.argv.(0) 62 63 let main () = 64 let argc = Array.length Sys.argv in 65 if argc <> 3 then begin print_usage (); exit 1 end; 66 67 let mode = Sys.argv.(1) in 68 begin match mode with 69 | "elab" | "type" | "eval" -> () 70 | _ -> print_usage (); exit 1 71 end; 72 73 let input = 74 let path = Sys.argv.(2) in 75 let file = 76 try open_in path with 77 | Sys_error msg -> Format.eprintf "%s@." msg; exit 1 in 78 Lexing.from_channel file in 79 80 let (term, vtyp) = 81 try 82 let concrete = Parser.start Lexer.token input in 83 let abstract = Desugar.term concrete in 84 Elab.infer' default_ctx abstract 85 with Error.Exn e -> 86 Format.eprintf "%a@." Error.pp_print e; 87 exit 1 in 88 89 match mode with 90 | "elab" -> 91 Format.printf "%a@." (Pretty.pp_print_term 0) term 92 | "type" -> 93 let typ = Quote.quote Env.empty vtyp in 94 Format.printf "%a@." (Pretty.pp_print_term 0) typ 95 | "eval" -> 96 let term' = Quote.quote Env.empty (Eval.eval Env.empty term) in 97 Format.printf "%a@." (Pretty.pp_print_term 0) term' 98 | _ -> impossible "invalid mode" 99 100 let () = main ()