commit 9eb795db62dcf1c0a587ae41a7c74abd615cf244
parent 489485290ee773d93718fd0c7e42df66a3fa1ed1
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 18 Dec 2023 20:55:44 -0800
Some refactoring
Diffstat:
9 files changed, 157 insertions(+), 94 deletions(-)
diff --git a/abstract.ml b/abstract.ml
@@ -1,8 +1,11 @@
open Common
-(* TODO: Here (and elsewhere) we should be using arrays instead of lists. *)
+(* TODO: Here (and elsewhere) we should be using arrays instead of lists.
+ * Keeps lists in concrete syntax for convenience when parsing, but change
+ * to arrays in abstract syntax and make the conversion in conctoabs. *)
type term =
+| Let of patt * term * term
| Match of term * case list
| Annot of term * term
| App of term * term list
@@ -10,19 +13,18 @@ type term =
| Index of term * term
| Deref of term
| Fn of patt list * term
-| FnType of annot list * term
+| FnType of (patt * term) list * term
| Data of ident * (ident * term) list (* TODO: constructor tag should be path eventually *)
-| DataType of (ident * annot list) list
+| DataType of (ident * (patt * term) list) list
| Nat of Z.t
| Ident of ident
and patt =
| PWild
| PBind of ident
| PAssign of term
-| PAnnot of annot
+| PAnnot of patt * term
| PData of ident * (ident * patt) list
| PNat of Z.t
| PAnd of patt * patt
| POr of patt * patt
-and annot = Annot of patt * term
and case = Case of {patt: patt; guard: term option; body: term}
diff --git a/concrete.ml b/concrete.ml
@@ -9,6 +9,8 @@ type expr =
| Annot of expr * expr
| Add of expr * expr
| Mul of expr * expr
+| Or of expr * expr
+| And of expr * expr
| App of expr * expr list
| Access of expr * ident
| Index of expr * expr
diff --git a/conctoabs.ml b/conctoabs.ml
@@ -15,12 +15,8 @@ let rec map_named f = function
| (x, e) :: xes -> (x, f e) :: map_named f xes
let rec term = function
-| C.Let (p, a, b) -> A.Match (term a, [
- A.Case {patt = patt p; guard = None; body = term b}
- ])
-| C.Seq (a, b) -> A.Match (term a, [
- A.Case {patt = A.PWild; guard = None; body = term b}
- ])
+| C.Let (p, a, b) -> A.Let (patt p, term a, term b)
+| C.Seq (a, b) -> A.Let (A.PWild, term a, term b)
| C.Match (a, cs) -> A.Match (term a, List.map case cs)
| C.If (a, b, c) -> A.Match (term a, [
A.Case {patt = A.PData ("true", []); guard = None; body = term b};
@@ -33,6 +29,8 @@ let rec term = function
| C.Annot (a, b) -> A.Annot (term a, term b)
| C.Add (a, b) -> A.App (A.Ident "`+", [term a; term b])
| C.Mul (a, b) -> A.App (A.Ident "`*", [term a; term b])
+| C.Or (a, b) -> A.App (A.Ident "`|", [term a; term b])
+| C.And (a, b) -> A.App (A.Ident "`&", [term a; term b])
| C.App (a, bs) -> A.App (term a, List.map term bs)
| C.Access (a, x) -> A.Access (term a, x)
| C.Index (a, b) -> A.Index (term a, term b)
@@ -40,13 +38,14 @@ let rec term = function
| C.Fn (ps, a) -> A.Fn (List.map patt ps, term a)
| C.FnType (anns, cod) -> A.FnType (List.map annot anns, term cod)
| C.Variant (x, es) -> A.Data (x, map_ordered term es)
-| C.VariantType vs -> A.DataType (map_named (List.map annot) vs)
+| C.VariantType variant_defs ->
+ A.DataType (map_named (List.map annot) variant_defs)
| C.Tuple es -> A.Data ("", map_ordered term es)
| C.TupleType anns -> A.DataType [("", List.map annot anns)]
-| C.Record fs -> A.Data ("", map_named term fs)
-| C.RecordType fds ->
- let fd_to_ann (x, e) = A.Annot (A.PBind x, term e) in
- A.DataType [("", List.map fd_to_ann fds)]
+| C.Record fields -> A.Data ("", map_named term fields)
+| C.RecordType field_defs ->
+ let field_def_to_annot (x, e) = (A.PBind x, term e) in
+ A.DataType [("", List.map field_def_to_annot field_defs)]
| C.Unit -> A.Data ("", [])
| C.Nat n -> A.Nat n
| C.Underscore -> failwith "no impl: holes"
@@ -59,9 +58,11 @@ and patt = function
| C.Match _ -> raise InvalidPattern
| C.If _ -> raise InvalidPattern
| C.Iff _ -> raise InvalidPattern
-| C.Annot (p, a) -> A.PAnnot (A.Annot (patt p, term a))
+| C.Annot (p, a) -> A.PAnnot (patt p, term a)
| C.Add _ -> raise InvalidPattern (* n + k patterns? *)
| C.Mul _ -> raise InvalidPattern
+| C.Or (p, q) -> A.POr (patt p, patt q)
+| C.And (p, q) -> A.PAnd (patt p, patt q)
| C.App _ -> raise InvalidPattern
| C.Access _ -> raise InvalidPattern
| C.Index _ -> raise InvalidPattern
@@ -84,5 +85,5 @@ and case (C.Case {patt = p; guard = g; body = b}) =
A.Case {patt = patt p; guard = Option.map term g; body = term b}
and annot = function
-| C.Annot (a, b) -> A.Annot (patt a, term b)
-| b -> A.Annot (A.PWild, term b)
+| C.Annot (a, b) -> (patt a, term b)
+| b -> (A.PWild, term b)
diff --git a/core.ml b/core.ml
@@ -25,7 +25,7 @@ and patt_discriminant =
let rec to_string m e =
let s = to_string in
let (c, s) = match e with
- | Let _ -> failwith "no impl: let"
+ | Let (scrutinee, body) -> (0, s 1 scrutinee ^ "; " ^ s 0 body)
| Case _ -> failwith "no impl: case"
| App (f, args) -> (6, String.concat " " (List.map (s 7) (f :: args)))
| Fn (arity, body) -> (1, "fn " ^ string_of_int arity ^ " => " ^ s 1 body)
diff --git a/elab.ml b/elab.ml
@@ -4,6 +4,7 @@ module A = Abstract
module C = Core
module V = Value
+(* TODO: use a hashtable or map for ident -> level lookups *)
type context = {
len: int;
names: ident option list;
@@ -52,44 +53,70 @@ let rec bind_arb_telescope ctx xs ts = match xs, ts with
| _, _ -> failwith "impossible"
let rec infer ctx = function
+| A.Let (A.PAnnot (p, a), scrutinee, body) ->
+ let a = check ctx a (V.Intrin C.Type) in
+ let va = eval ctx.values a in
+ let x = check_patt ctx p va in
+ let scrutinee = check ctx scrutinee va in
+ let vscrutinee = eval ctx.values scrutinee in
+ let (body, vb) = infer (bind_def ctx x vscrutinee va) body in
+ (C.Let (scrutinee, body), vb)
+| A.Let (p, scrutinee, body) ->
+ let (scrutinee, va) = infer ctx scrutinee in
+ let vscrutinee = eval ctx.values scrutinee in
+ let x = check_patt ctx p va in
+ let (body, vb) = infer (bind_def ctx x vscrutinee va) body in
+ (C.Let (scrutinee, body), vb)
| A.Match _ -> failwith "no impl: match"
-| A.Annot (a, t) ->
- let ct = check ctx t (V.Intrin C.Type) in
- let vt = eval ctx.values ct in
- let ca = check ctx a vt in
- (ca, vt)
+| A.Annot (tm, a) ->
+ let a = check ctx a (V.Intrin C.Type) in
+ let va = eval ctx.values a in
+ let tm = check ctx tm va in
+ (tm, va)
| A.App (f, args) ->
- let (cf, tf) = infer ctx f in
- begin match tf with
+ let (f, fty) = infer ctx f in
+ begin match fty with
| V.FnType (env, arity, doms, cod) ->
- if List.length args <> arity then failwith "arity mismatch" else
- let rec go env args doms = match args, doms with
- | arg :: args, dom :: doms ->
- let vdom = eval env dom in
- let carg = check ctx arg vdom in
- let varg = eval ctx.values carg in
- let (cargs, vcod) = go (varg :: env) args doms in
- (carg :: cargs, vcod)
- | [], [] -> ([], eval env cod)
- | _, _ -> failwith "impossible" in
- let (cargs, vcod) = go env args doms in
- (C.App (cf, cargs), vcod)
- | _ -> failwith "expected function type in application"
+ if List.length args <> arity then
+ failwith "type error: arity mismatch in application"
+ else
+ let rec go env args doms = match args, doms with
+ | arg :: args, dom :: doms ->
+ let vdom = eval env dom in
+ let arg = check ctx arg vdom in
+ let varg = eval ctx.values arg in
+ let (args, vcod) = go (varg :: env) args doms in
+ (arg :: args, vcod)
+ | [], [] -> ([], eval env cod)
+ | _, _ -> failwith "impossible" in
+ let (args, vcod) = go env args doms in
+ (C.App (f, args), vcod)
+ | _ -> failwith "type error: expected function type in application"
end
| A.Access _ -> failwith "no impl: access"
| A.Index _ -> failwith "no impl: index"
| A.Deref _ -> failwith "no impl: deref"
| A.Fn (ps, body) ->
- let (xs, vdoms) = infer_patt_telescope ctx ps in
- let arity = List.length xs in
- let (cbody, vcod) = infer (bind_arb_telescope ctx xs vdoms) body in
- let cdoms = quote_telescope ctx.len vdoms in
- let ccod = quote (ctx.len + arity) vcod in
- (C.Fn (arity, cbody), V.FnType (ctx.values, arity, cdoms, ccod))
+ let rec go ctx = function
+ | A.PAnnot (p, dom) :: ps ->
+ let dom = check ctx dom (V.Intrin C.Type) in
+ let vdom = eval ctx.values dom in
+ let x = check_patt ctx p vdom in
+ let (body, doms, vcod) = go (bind_arb ctx x vdom) ps in
+ (body, dom :: doms, vcod)
+ | _ :: ps ->
+ failwith "type error: can not infer type for unannotated function parameter"
+ | [] ->
+ let (body, vcod) = infer ctx body in
+ (body, [], vcod) in
+ let (body, doms, vcod) = go ctx ps in
+ let arity = List.length doms in
+ let cod = quote (ctx.len + arity) vcod in
+ (C.Fn (arity, body), V.FnType (ctx.values, arity, doms, cod))
| A.FnType (anns, cod) ->
let arity = List.length anns in
let rec go ctx = function
- | A.Annot (p, dom) :: anns ->
+ | (p, dom) :: anns ->
let cdom = check ctx dom (V.Intrin C.Type) in
let vdom = eval ctx.values cdom in
let x = check_patt ctx p vdom in
@@ -109,38 +136,51 @@ let rec infer ctx = function
| _, _ -> failwith "impossible" in
go 0 ctx.names ctx.types
-and check ctx a t = match a, t with
-(* TODO: Match, Fn, Data *)
-| a, t ->
- let (ca, ta) = infer ctx a in
- if conv ctx.len t ta then ca else failwith "type error"
-
-and infer_patt ctx = function
-| A.PWild -> failwith "can not infer type for wild pattern"
-| A.PBind _ -> failwith "can not infer type for bind pattern"
-| A.PAssign _ -> failwith "no impl: assign pattern"
-| A.PAnnot (A.Annot (p, t)) ->
- let ct = check ctx t (V.Intrin C.Type) in
- let vt = eval ctx.values ct in
- let x = check_patt ctx p vt in
- (x, vt)
-| A.PData _ -> failwith "no impl: data pattern"
-| A.PNat _ -> failwith "no impl: nat pattern"
-| A.PAnd _ -> failwith "no impl: and pattern"
-| A.POr _ -> failwith "no impl: or pattern"
-
-and infer_patt_telescope ctx = function
-| p :: ps ->
- let (x, t) = infer_patt ctx p in
- let (xs, ts) = infer_patt_telescope (bind_arb ctx x t) ps in
- (x :: xs, t :: ts)
-| [] -> ([], [])
+and check ctx tm vty = match tm, vty with
+(* TODO: Match, Data *)
+| A.Let (A.PAnnot (p, a), scrutinee, body), vb ->
+ let a = check ctx a (V.Intrin C.Type) in
+ let va = eval ctx.values a in
+ let x = check_patt ctx p va in
+ let scrutinee = check ctx scrutinee va in
+ let vscrutinee = eval ctx.values scrutinee in
+ let body = check (bind_def ctx x vscrutinee va) body vb in
+ C.Let (scrutinee, body)
+| A.Let (p, scrutinee, body), vb ->
+ let (scrutinee, va) = infer ctx scrutinee in
+ let vscrutinee = eval ctx.values scrutinee in
+ let x = check_patt ctx p va in
+ let body = check (bind_def ctx x vscrutinee va) body vb in
+ C.Let (scrutinee, body)
+| A.Fn (ps, body), V.FnType (env, arity, doms, cod) ->
+ if List.length ps <> arity then
+ failwith "type error: arity mismatch"
+ else
+ let rec go ctx ps env doms = match ps, doms with
+ | p :: ps, dom :: doms ->
+ let vdom = eval env dom in
+ let x = check_patt ctx p vdom in
+ let ctx = bind_arb ctx x vdom in
+ let env = List.hd ctx.values :: env in
+ go ctx ps env doms
+ | [], [] ->
+ let vcod = eval env cod in
+ check ctx body vcod
+ | _, _ -> failwith "impossible" in
+ let cbody = go ctx ps env doms in
+ C.Fn (arity, cbody)
+| tm, vexpected ->
+ let (tm, vinferred) = infer ctx tm in
+ if conv ctx.len vexpected vinferred then
+ tm
+ else
+ failwith "type error: expected/inferred mismatch"
and check_patt ctx p t = match p with
| A.PWild -> None
| A.PBind x -> Some x
| A.PAssign _ -> failwith "no impl: assign pattern"
-| A.PAnnot (A.Annot (p, u)) ->
+| A.PAnnot (p, u) ->
let cu = check ctx u (V.Intrin C.Type) in
let vu = eval ctx.values cu in
if conv ctx.len vu t then
@@ -151,13 +191,3 @@ and check_patt ctx p t = match p with
| A.PNat _ -> failwith "no impl: nat pattern"
| A.PAnd _ -> failwith "no impl: and pattern"
| A.POr _ -> failwith "no impl: or pattern"
-
-(*
-and check_patt_telescope ctx ps ts = match ps, ts with
-| p :: ps, t :: ts ->
- let x = check_patt ctx p t in
- let xs = check_patt_telescope (bind_arb ctx x t) ps ts in
- x :: xs
-| [], [] -> []
-| _, _ -> failwith "impossible"
-*)
diff --git a/eval.ml b/eval.ml
@@ -9,7 +9,7 @@ let weaken env l n =
go env l
let rec eval env = function
-| C.Let _ -> failwith "no impl: let"
+| C.Let (scrutinee, body) -> eval (eval env scrutinee :: env) body
| C.Case _ -> failwith "no impl: case"
| C.App (f, args) ->
begin match eval env f, List.map (eval env) args with
diff --git a/lexer.mll b/lexer.mll
@@ -63,6 +63,9 @@ rule token = parse
| "+" { PLUS }
| "*" { ASTERISK }
+| "|" { PIPE }
+| "&" { AMPERSAND }
+
| "match" { MATCH }
| "if" { IF }
@@ -74,6 +77,7 @@ rule token = parse
| "fn" { FN }
+| "_" { UNDERSCORE }
| ident_start ident_cont* { IDENT (Lexing.lexeme lexbuf) }
| number { NAT (Z.of_string (Lexing.lexeme lexbuf)) }
diff --git a/main.ml b/main.ml
@@ -1,5 +1,13 @@
(*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 buf = Lexing.from_string "N := (A: Type, A, A -> A) -> A; ((fn m: N, n: N => 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 buf = Lexing.from_string "\
+ 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));\
+ five := add two three;\
+ five Nat 0 (fn n => 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
@@ -9,17 +9,18 @@ open Concrete
%token HASH_LBRACK LBRACK RBRACK
%token HASH_LBRACE LBRACE RBRACE
%token PLUS ASTERISK
+%token PIPE AMPERSAND
%token MATCH
%token IF THEN ELSE
%token IFF DO
%token FN
+%token UNDERSCORE
%token <Common.ident> IDENT
%token <Z.t> NAT
%start start
%type <Concrete.expr> start
-%nonassoc PREC_EXPR4
%nonassoc PREC_TUPLE
%nonassoc SINGLE_ARROW
@@ -51,14 +52,28 @@ expr2: (* Type annotations (right-associative); lowest prec for patterns *)
| expr3 COLON expr2 { Annot($1, $3) }
| expr3 { $1 }
expr3: (* Function arrow (right-associative) *)
- | expr4 SINGLE_ARROW expr3 { FnType ([$1], $3) }
+ | expr6 SINGLE_ARROW expr3 { FnType ([$1], $3) }
| tuple SINGLE_ARROW expr3 { FnType ($1, $3) }
- | expr4 %prec PREC_EXPR4 { $1 }
-expr4:
- | expr4 PLUS expr5 { Add ($1, $3) }
+ | expr4 { $1 }
+expr4: (* Additive binary operators (left-associative) *)
+ | expr4add PLUS expr5 { Add ($1, $3) }
+ | expr4or PIPE expr5 { Or ($1, $3) }
| expr5 { $1 }
-expr5:
- | expr5 ASTERISK expr6 { Mul ($1, $3) }
+expr4add:
+ | expr4add PLUS expr5 { Add ($1, $3) }
+ | expr5 { $1 }
+expr4or:
+ | expr4or PIPE expr5 { Or ($1, $3) }
+ | expr5 { $1 }
+expr5: (* Multiplicative binary operators (left-associative) *)
+ | expr5mul ASTERISK expr6 { Mul ($1, $3) }
+ | expr5and AMPERSAND expr6 { And ($1, $3) }
+ | expr6 { $1 }
+expr5mul:
+ | expr5mul ASTERISK expr6 { Mul ($1, $3) }
+ | expr6 { $1 }
+expr5and:
+ | expr5and AMPERSAND expr6 { And ($1, $3) }
| expr6 { $1 }
expr6:
| expr7 expr7 expr7_apposition { App ($1, $2 :: $3) }
@@ -70,7 +85,8 @@ expr7:
| expr7 EXCLAM { Deref $1 }
| expr8 { $1 }
expr8:
- | IDENT { if $1 = "_" then Underscore else Ident $1 }
+ | UNDERSCORE { Underscore }
+ | IDENT { Ident $1 }
| NAT { Nat $1 }
| HASH_LBRACK variant_def_list RBRACK { VariantType $2 }
| HASH_LPAREN annot_list RPAREN { TupleType $2 }
