commit 489485290ee773d93718fd0c7e42df66a3fa1ed1
parent 795ed7b03d11afeb39e89d07dbface2f7d2ff9f7
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Sun, 17 Dec 2023 20:11:59 -0800
Stuff
Diffstat:
8 files changed, 31 insertions(+), 10 deletions(-)
diff --git a/concrete.ml b/concrete.ml
@@ -25,4 +25,5 @@ type expr =
| Nat of Z.t
| Underscore
| Ident of ident
+| Paren of expr
and case = Case of {patt: expr; guard: expr option; body: expr}
diff --git a/conctoabs.ml b/conctoabs.ml
@@ -51,6 +51,7 @@ let rec term = function
| C.Nat n -> A.Nat n
| C.Underscore -> failwith "no impl: holes"
| C.Ident x -> A.Ident x
+| C.Paren a -> term a
and patt = function
| C.Let _ -> raise InvalidPattern
@@ -77,6 +78,7 @@ and patt = function
| C.Nat n -> A.PNat n
| C.Underscore -> A.PWild
| C.Ident x -> A.PBind x
+| C.Paren a -> patt a
and case (C.Case {patt = p; guard = g; body = b}) =
A.Case {patt = patt p; guard = Option.map term g; body = term b}
diff --git a/core.ml b/core.ml
@@ -4,6 +4,7 @@ type intrin =
| Type
| NatType
| NatOpAdd
+| NatOpMul
type term =
| Let of term * term
@@ -37,5 +38,6 @@ let rec to_string m e =
| Var i -> (8, "?" ^ string_of_int i)
| Intrin Type -> (8, "`Type")
| Intrin NatType -> (8, "`Nat")
- | Intrin NatOpAdd -> (8, "`+") in
+ | Intrin NatOpAdd -> (8, "`+")
+ | Intrin NatOpMul -> (8, "`*") in
if c < m then "(" ^ s ^ ")" else s
diff --git a/elab.ml b/elab.ml
@@ -13,16 +13,26 @@ type context = {
let default_ctx = {
len = 3;
- names = [Some "`+"; Some "Nat"; Some "Type"];
- values = [V.Intrin C.NatOpAdd; V.Intrin C.NatType; V.Intrin C.Type];
+ names = [
+ Some "`*";
+ Some "`+";
+ Some "Nat";
+ Some "Type";
+ ];
+ values = [
+ V.Intrin C.NatOpMul;
+ V.Intrin C.NatOpAdd;
+ V.Intrin C.NatType;
+ V.Intrin C.Type;
+ ];
types =
- let nat_op_add_type = V.FnType (
+ let nat_op_type = V.FnType (
[],
2,
[C.Intrin C.NatType; C.Intrin C.NatType],
C.Intrin C.NatType
) in
- [nat_op_add_type; V.Intrin C.Type; V.Intrin C.Type];
+ [nat_op_type; nat_op_type; V.Intrin C.Type; V.Intrin C.Type];
}
(* Add `x := v : t` to ctx. *)
diff --git a/eval.ml b/eval.ml
@@ -16,6 +16,7 @@ let rec eval env = function
(* β-reduction *)
| V.Fn (cap, _, body), vargs -> eval (List.rev_append vargs cap) body
| V.Intrin C.NatOpAdd, [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
+ | V.Intrin C.NatOpMul, [V.Nat m; V.Nat n] -> V.Nat (Z.mul m n)
(* neutral application *)
| vf, vargs -> V.App (vf, vargs)
end
@@ -54,6 +55,9 @@ let rec conv l a b = match a, b with
(* TODO: η-equality? *)
(* TODO: Case *)
| V.App (af, aargs), V.App (bf, bargs) ->
+ (* Note that aargs and bargs aren't necessarily the same length, but they
+ * are if af and bf are convertible, so the short-circuiting of (&&)
+ * ensures that all2 can't fail. *)
conv l af bf && all2 (conv l) aargs bargs
| V.Fn (aenv, arity, abody), V.Fn (benv, _, bbody) ->
let vabody = eval (weaken aenv l arity) abody in
diff --git a/lexer.mll b/lexer.mll
@@ -76,8 +76,8 @@ rule token = parse
| ident_start ident_cont* { IDENT (Lexing.lexeme lexbuf) }
-| number invalid_number_terminator { raise (LexerError (Lexing.lexeme_start_p lexbuf, "invalid terminator after integer literal")) }
| number { NAT (Z.of_string (Lexing.lexeme lexbuf)) }
+| number invalid_number_terminator { raise (LexerError (Lexing.lexeme_start_p lexbuf, "invalid terminator after integer literal")) }
(*
| "<" { LT }
diff --git a/main.ml b/main.ml
@@ -1,4 +1,5 @@
-let buf = Lexing.from_string "(fn x:Nat, y:Nat => x + y) 1 2"
+(*let buf = Lexing.from_string "(fn A: Nat -> Type, f: (A 0, A 1) -> A 2, x: A 0, y: A 1 => f x y) (fn _: Nat => Nat) (fn x: Nat, y: Nat => x + y) 3 4 : Nat"*)
+let buf = Lexing.from_string "((fn m: (A: Type, A, A -> A) -> A, n: (A: Type, A, A -> A) -> A => fn A: Type, z: A, s: A -> A => m A (n A z s) s) (fn A: Type, z: A, s: A -> A => s (s z)) (fn A: Type, z: A, s: A -> A => s (s (s z)))) Nat 0 (fn n: Nat => n + 1)"
let concrete = Parser.start Lexer.token buf
let abstract = Conctoabs.term concrete
let ctx = Elab.default_ctx
diff --git a/parser.mly b/parser.mly
@@ -29,8 +29,9 @@ open Concrete
* Anonymous functions (no recursion support):
* fn x -> ...
* Named functions ((mutual) recursion support)):
- * f := func x -> ...;
- * g := func y -> ...;
+ * f := func x -> ...,
+ * h := func y -> ...,
+ * g := func z -> ...;
* (Think of ":= func" as being one symbol).
* We can make a similar distinction for types with "ty" vs "type". *)
@@ -77,7 +78,7 @@ expr8:
| tuple %prec PREC_TUPLE { Tuple $1 }
| LBRACE field_list RBRACE { Record $2 }
| LPAREN RPAREN { Unit }
- | LPAREN expr0 RPAREN { $2 }
+ | LPAREN expr0 RPAREN { Paren $2 }
cases: (* Has optional trailing semicolon *)
| case SEMICOLON cases { $1 :: $3 }
