commit 2c7eb0844adceb5e16dd5b83583293438c1c3914
parent 1b84163cd6506ed3c7efae7a18a656ea382cae49
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Tue, 30 Jan 2024 00:37:23 -0800
Add CLI
Diffstat:
4 files changed, 60 insertions(+), 63 deletions(-)
diff --git a/eval.ml b/eval.ml
@@ -78,7 +78,7 @@ let rec eval
let var = Env.index env ij in
begin match Env.eval env var with
| Some v -> v
- | None -> Arb var
+ | None -> V.Arb var
end
| I.Builtin b -> V.Builtin b
diff --git a/examples/church b/examples/church
@@ -0,0 +1,7 @@
+\ This is a comment.
+N := [A: Type, A, A -> A] -> A;
+add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;
+two: N := fn A, z, s => s (s z);
+three: N := fn A, z, s => s (s (s z));
+`f i v e` := add two three;
+`f i v e` Nat 0 (fn n => n + 1)
diff --git a/examples/list b/examples/list
@@ -0,0 +1,10 @@
+UnaryNat: Type := rec #{
+ @Z;
+ @S UnaryNat;
+};
+@S (@S @Z): UnaryNat
+\List: Type -> Type := rec fn A => #{
+\ @nil;
+\ @cons A, List A;
+\};
+\@cons 1 @nil : List Nat
diff --git a/main.ml b/main.ml
@@ -1,3 +1,4 @@
+open Util
open Node
module B = Builtin
module I = Internal
@@ -5,13 +6,6 @@ module V = Value
(*
let buf = Lexing.from_string "\
- \\comment :)\n\
- N := [A: Type, A, A -> A] -> A;\n\
- add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;\n\
- two: N := fn A, z, s => s (s z);\n\
- three: N := fn A, z, s => s (s (s z));\n\
- `f i v e` := add two three;\n\
- `f i v e` Nat 0 (fn n => n + 1)\n\
"
*)
@@ -28,56 +22,22 @@ let buf = Lexing.from_string "\
(*
let buf = Lexing.from_string "\
- f := fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat =>\
- fn a: Nat, b: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat => 3; 3\
-"
-*)
-
-(*
-let buf = Lexing.from_string "\
- T & S := #{@a Nat; @b #(), Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat; @c #(); @d #(); @e #(); @f #(); @g #(); @h #(); @i #(); @j #(); @k #(); @l #(); @m #()};\n\
- @a 3 : S\n\
-"
-*)
-
-(*
-let buf = Lexing.from_string "\
- f: Nat := g,\n\
- g: Nat := f;\n\
- 3\n\
-"
-*)
-
-(*
-let buf = Lexing.from_string "\
- T & S := #{@a Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat; @b #()};\n\
- @a 0 1 2 3 4 5 6 7 8 9 10 11 : S\n\
-"
-*)
-
-(*
-let buf = Lexing.from_string "\
- `` := () : #();\
- (fn => Nat) ``\
-"
-*)
-
-(*
-let buf = Lexing.from_string "\
fact: Nat -> Nat := rec fn n =>\n\
if n = 0 then 1 else n * fact (n - 1);\n\
fact 6\n\
"
*)
+(*
let buf = Lexing.from_string "\
Opt := fn A: Type => #{@some A; @none};\n\
div: [Nat, Nat] -> Opt Nat := fn m, n =>\n\
if n = 0 then @none else @some (m / n);\n\
(div 3 0, div 12 3)\n\
"
+*)
-let ctx =
+let default_ctx =
let ctx = ref Ctx.empty in
let assign s t v =
let (ctx', _) = Ctx.assign !ctx [|Name.Var.Of s|] t v in
@@ -97,24 +57,44 @@ let ctx =
assign "<>" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpNe;
!ctx
-let print fmt a =
- Format.set_margin 80;
- Format.set_max_indent 0;
- Format.printf "%a@." fmt a
+let print_usage () =
+ Format.eprintf "usage: %s (elab|type|eval) PATH@." Sys.argv.(0)
+
+let main () =
+ let argc = Array.length Sys.argv in
+ if argc <> 3 then begin print_usage (); exit 1 end;
+
+ let mode = Sys.argv.(1) in
+ begin match mode with
+ | "elab" | "type" | "eval" -> ()
+ | _ -> print_usage (); exit 1
+ end;
+
+ let input =
+ let path = Sys.argv.(2) in
+ let file =
+ try open_in path with
+ | Sys_error msg -> Format.eprintf "%s@." msg; exit 1 in
+ Lexing.from_channel file in
-let (internal, ty) = try
- let concrete = Parser.start Lexer.token buf in
- let abstract = Desugar.term concrete in
- Elab.infer' ctx abstract
-with Error.Exn e ->
- print Error.pp_print e;
- exit 1
+ let (term, vtyp) =
+ try
+ let concrete = Parser.start Lexer.token input in
+ let abstract = Desugar.term concrete in
+ Elab.infer' default_ctx abstract
+ with Error.Exn e ->
+ Format.eprintf "%a@." Error.pp_print e;
+ exit 1 in
-let internal' = Quote.quote ctx.env (Eval.eval ctx.env internal)
+ match mode with
+ | "elab" ->
+ Format.printf "%a@." (Pretty.pp_print_term 0) term
+ | "type" ->
+ let typ = Quote.quote Env.empty vtyp in
+ Format.printf "%a@." (Pretty.pp_print_term 0) typ
+ | "eval" ->
+ let term' = Quote.quote Env.empty (Eval.eval Env.empty term) in
+ Format.printf "%a@." (Pretty.pp_print_term 0) term'
+ | _ -> impossible "invalid mode"
-let () =
- print (Pretty.pp_print_term 0) internal;
- print Format.pp_print_string "\
- ----------------------------------------\
- ----------------------------------------";
- print (Pretty.pp_print_term 0) internal'
+let () = main ()
