commit 9709acfc587cdcb130e970f6728d396c0f85a0bf
parent 7d38e9e1686d610201799505fcf506e6f4f289ea
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Thu, 28 Dec 2023 13:22:22 -0800
Stuff
Don't remember what's different from previous commits (maybe the
addition of ADTs), but this commit at least builds.
Diffstat:
11 files changed, 260 insertions(+), 116 deletions(-)
diff --git a/abstract.ml b/abstract.ml
@@ -14,8 +14,8 @@ and term' =
| App of term * term list
| Fn of patt list * term
| FnType of annot list * term
-| Data of ident * term Field.t list
-| DataType of cons list
+| Data of ident * term list
+| DataType of annot list IdentMap.t
| Nat of Z.t
| Var of ident * int
(*
@@ -27,19 +27,16 @@ and term' =
and case = case' Node.t
and case' = Case of patt * term
-and cons = cons' Node.t
-and cons' = Cons of ident * annot list
-
and patt = patt' Node.t
and patt' =
| PWild
| PBind of ident
| PAnnot of patt * term
-| PData of ident * patt Field.t list
+| PData of ident * patt list
+(*
| PNat of Z.t
| PAnd of patt * patt
| POr of patt * patt
-(*
| PAssign of term
*)
diff --git a/cnctoabs.ml b/cnctoabs.ml
@@ -1,12 +1,12 @@
+(* TODO: rename this module to "desugar" *)
+
open Common
module C = Concrete
module A = Abstract
-let rec ordered_fields f =
- let rec go i = function
- | t :: ts -> (Loc.None @$ Field.Of (string_of_int i, f t)) :: go (i + 1) ts
- | [] -> [] in
- go 0
+exception Error of Loc.t * string
+
+let error loc msg = raise (Error (loc, msg))
let rec term = function
| Node.Of (_, C.Paren t) -> term t
@@ -17,11 +17,13 @@ and term' = function
* non-unit results can't be ignored. *)
| C.Seq (t, u) -> A.Let (Loc.None @$ A.PWild, term t, term u)
| C.Match (scrutinee, cs) -> A.Match (term scrutinee, List.map case cs)
-| C.If (cond, t, f) -> A.Match (term cond, [
+| C.If (cond, t, f) ->
+ A.Match (term cond, [
Loc.None @$ A.Case (Loc.None @$ A.PData ("true", []), term t);
Loc.None @$ A.Case (Loc.None @$ A.PWild, term f);
])
-| C.Iff (cond, t) -> A.Match (term cond, [
+| C.Iff (cond, t) ->
+ A.Match (term cond, [
Loc.None @$ A.Case (Loc.None @$ A.PData ("true", []), term t);
Loc.None @$ A.Case (Loc.None @$ A.PWild, Loc.None @$ A.Data ("", []));
])
@@ -37,12 +39,21 @@ and term' = function
| C.App (f, args) -> A.App (term f, List.map term args)
| C.Fn (ps, body) -> A.Fn (List.map patt ps, term body)
| C.FnType (anns, cod) -> A.FnType (List.map annot anns, term cod)
-| C.Variant (x, ts) -> A.Data (x, ordered_fields term ts)
-| C.VariantType vs -> A.DataType (List.map cons vs)
-| C.Tuple ts -> A.Data ("", ordered_fields term ts)
-| C.TupleType anns -> A.DataType [Loc.None @$ A.Cons ("", List.map annot anns)]
-| C.Record tfs -> A.Data ("", List.map (Field.map term) tfs)
-| C.RecordType anns -> A.DataType [Loc.None @$ A.Cons ("", List.map annot anns)]
+| C.Variant (tag, ts) -> A.Data (tag, List.map term ts)
+| C.VariantType ctors ->
+ let rec go m = function
+ | Node.Of (loc, C.Ctor (tag, anns)) :: ctors ->
+ if IdentMap.mem tag m then
+ error loc "duplicate constructor"
+ else
+ go (IdentMap.add tag (List.map annot anns) m) ctors
+ | [] -> m in
+ A.DataType (go IdentMap.empty ctors)
+| C.Tuple ts -> A.Data ("", List.map term ts)
+| C.TupleType anns ->
+ A.DataType (IdentMap.singleton "" (List.map annot anns))
+| C.Record _ -> failwith "no impl: records"
+| C.RecordType _ -> failwith "no impl: record types"
| C.Unit -> A.Data ("", [])
| C.Nat n -> A.Nat n
| C.Underscore -> failwith "no impl: holes"
@@ -53,9 +64,6 @@ and term' = function
and case c = Node.map case' c
and case' (C.Case (p, t)) = A.Case (patt p, term t)
-and cons c = Node.map cons' c
-and cons' (C.Cons (x, anns)) = A.Cons (x, List.map annot anns)
-
and patt = function
| Node.Of (_, C.PParen p) -> patt p
| n -> Node.map patt' n
@@ -63,13 +71,13 @@ and patt' = function
| C.PWild -> A.PWild
| C.PBind x -> A.PBind x
| C.PAnnot (p, t) -> A.PAnnot (patt p, term t)
-| C.PVariant (x, ps) -> A.PData (x, ordered_fields patt ps)
-| C.PTuple ps -> A.PData ("", ordered_fields patt ps)
-| C.PRecord pfs -> A.PData ("", List.map (Field.map patt) pfs)
+| C.PVariant (tag, ps) -> A.PData (tag, List.map patt ps)
+| C.PTuple ps -> A.PData ("", List.map patt ps)
+| C.PRecord pfs -> failwith "no impl: record patterns"
| C.PUnit -> A.PData ("", [])
-| C.PNat n -> A.PNat n
-| C.PAnd (p, q) -> A.PAnd (patt p, patt q)
-| C.POr (p, q) -> A.POr (patt p, patt q)
+| C.PNat _ -> failwith "no impl: nat patterns"
+| C.PAnd _ -> failwith "no impl: and patterns"
+| C.POr _ -> failwith "no impl: or patterns"
| C.PParen _ -> failwith "impossible"
and annot = function
diff --git a/common.ml b/common.ml
@@ -2,6 +2,8 @@ type ident = string
type index = int
type level = int
+module IdentMap = Map.Make(String)
+
(* Short-circuiting AND fold_left. *)
let rec all2 f xs ys = match xs, ys with
| x :: xs, y :: ys -> f x y && all2 f xs ys
diff --git a/concrete.ml b/concrete.ml
@@ -18,11 +18,11 @@ and term' =
| Fn of patt list * term
| FnType of annot list * term
| Variant of ident * term list
-| VariantType of cons list
+| VariantType of ctor list
| Tuple of term list
| TupleType of annot list
| Record of term Field.t list
-| RecordType of annot list
+| RecordType of annot Field.t list
| Unit
| Nat of Z.t
| Underscore
@@ -38,8 +38,8 @@ and term' =
and case = case' Node.t
and case' = Case of patt * term
-and cons = cons' Node.t
-and cons' = Cons of ident * annot list
+and ctor = ctor' Node.t
+and ctor' = Ctor of ident * annot list
and patt = patt' Node.t
and patt' =
diff --git a/elab.ml b/elab.ml
@@ -16,30 +16,6 @@ type context = {
types: V.value list;
}
-let default_ctx = {
- len = 3;
- names = [
- Some "`*";
- Some "`+";
- Some "Nat";
- Some "Type";
- ];
- values = [
- V.Intrin I.NatOpMul;
- V.Intrin I.NatOpAdd;
- V.Intrin I.NatType;
- V.Intrin I.Type;
- ];
- types =
- let nat_op_type = V.FnType (
- [],
- 2,
- [I.Intrin I.NatType; I.Intrin I.NatType],
- I.Intrin I.NatType
- ) in
- [nat_op_type; nat_op_type; V.Intrin I.Type; V.Intrin I.Type];
-}
-
(* Add `x := v : a` to ctx. *)
let bind_def ctx x v a = {
len = 1 + ctx.len;
@@ -51,19 +27,32 @@ let bind_def ctx x v a = {
(* Add `x : a` to ctx. *)
let bind_arb ctx x a = bind_def ctx x (V.Arb ctx.len) a
+let default_ctx =
+ let nat_op_type = V.FnType (
+ [],
+ 2,
+ [I.Intrin I.NatType; I.Intrin I.NatType],
+ I.Intrin I.NatType
+ ) in
+ let ctx = {len = 0; names = []; values = []; types = []} in
+ let ctx = bind_def ctx (Some "Type") (V.Intrin I.Type) (V.Intrin I.Type) in
+ let ctx = bind_def ctx (Some "Nat") (V.Intrin I.NatType) (V.Intrin I.Type) in
+ let ctx = bind_def ctx (Some "`+") (V.Intrin I.NatOpAdd) nat_op_type in
+ let ctx = bind_def ctx (Some "`*") (V.Intrin I.NatOpAdd) nat_op_type in
+ ctx
+
let rec infer ctx (Node.Of (loc, t)) = match t with
-| A.Let (Node.Of (_, A.PAnnot (p, a)), scrutinee, body) ->
- let a = check ctx a (V.Intrin I.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
- (I.Let (scrutinee, body), vb)
| A.Let (p, scrutinee, body) ->
- let (scrutinee, va) = infer ctx scrutinee in
+ let (x, scrutinee, va) =
+ match infer_patt ctx p with
+ | Some (x, va) ->
+ let scrutinee = check ctx scrutinee va in
+ (x, scrutinee, va)
+ | None ->
+ let (scrutinee, va) = infer ctx scrutinee in
+ let x = check_patt ctx p va in
+ (x, scrutinee, va) 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
(I.Let (scrutinee, body), vb)
| A.Match _ -> failwith "no impl: match"
@@ -124,8 +113,20 @@ let rec infer ctx (Node.Of (loc, t)) = match t with
| [] -> ([], check ctx cod (V.Intrin I.Type)) in
let (doms, cod) = go ctx anns in
(I.FnType (arity, doms, cod), V.Intrin I.Type)
-| A.Data _ -> failwith "no impl: data"
-| A.DataType _ -> failwith "no impl: data type"
+| A.Data _ ->
+ error loc "can not infer type for data constructor"
+| A.DataType ctors ->
+ let rec go ctx = function
+ | Node.Of (_, ann) :: anns ->
+ let (p, a) = match ann with
+ | A.AType a -> (Loc.None @$ A.PWild, a)
+ | A.APatt (p, a) -> (p, a) in
+ let a = check ctx a (V.Intrin I.Type) in
+ let va = eval ctx.values a in
+ let x = check_patt ctx p va in
+ a :: go (bind_arb ctx x va) anns
+ | [] -> [] in
+ (I.DataType (IdentMap.map (go ctx) ctors), V.Intrin I.Type)
| A.Nat n -> (I.Nat n, V.Intrin I.NatType)
| A.Var (x, i) ->
let rec go j i' ys ts = match i', ys, ts with
@@ -136,26 +137,25 @@ let rec infer ctx (Node.Of (loc, t)) = match t with
| i', None :: ys, t :: ts ->
go (j + 1) i' ys ts
| _, [], [] ->
- (* TODO: We should print x ^ "#0" if the programmer wrote x ^ "#0". *)
+ (* TODO: We should print x ^ "#0" iff the programmer wrote x ^ "#0". *)
let x = if i = 0 then x else x ^ "#" ^ string_of_int i in
error loc ("unbound identifier: " ^ x)
| _, _, _ -> failwith "impossible" in
go 0 i ctx.names ctx.types
and check ctx (Node.Of (loc, t') as t) va = match t', va with
-(* TODO: Match, Data *)
-| A.Let (Node.Of (_, A.PAnnot (p, a)), scrutinee, body), vb ->
- let a = check ctx a (V.Intrin I.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
- I.Let (scrutinee, body)
+(* TODO: Match *)
| A.Let (p, scrutinee, body), vb ->
- let (scrutinee, va) = infer ctx scrutinee in
+ let (x, scrutinee, va) =
+ match infer_patt ctx p with
+ | Some (x, va) ->
+ let scrutinee = check ctx scrutinee va in
+ (x, scrutinee, va)
+ | None ->
+ let (scrutinee, va) = infer ctx scrutinee in
+ let x = check_patt ctx p va in
+ (x, scrutinee, va) 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
I.Let (scrutinee, body)
| A.Fn (ps, body), V.FnType (env, arity, doms, cod) ->
@@ -175,6 +175,28 @@ and check ctx (Node.Of (loc, t') as t) va = match t', va with
| _, _ -> failwith "impossible" in
let cbody = go ctx ps env doms in
I.Fn (arity, cbody)
+| A.Fn _, _ -> error loc "expected function type"
+| A.Data (tag, args), V.DataType (env, ctors) ->
+ begin match IdentMap.find_opt tag ctors with
+ | Some bs ->
+ if List.length args <> List.length bs then
+ error loc "arity mismatch"
+ else
+ (* TODO: this is similar to Fn checking code. *)
+ let rec go args env bs = match args, bs with
+ | arg :: args, b :: bs ->
+ let vb = eval env b in
+ let arg = check ctx arg vb in
+ let varg = eval ctx.values arg in
+ arg :: go args (varg :: env) bs
+ | [], [] -> []
+ | _, _ -> failwith "impossible" in
+ I.Data (tag, go args env bs)
+ | None -> error loc ("expected data type with constructor \"" ^ tag ^ "\"")
+ end
+| A.Data _, _ -> error loc "expected data type"
+(* TODO: use (A _ | B _ | C _) idiom for catch-all case so that we get an
+ * exhaustiveness warning when we add new variants *)
| _, vexpected ->
let (t, vinferred) = infer ctx t in
if conv ctx.len vexpected vinferred then
@@ -183,10 +205,25 @@ and check ctx (Node.Of (loc, t') as t) va = match t', va with
(* TODO: pretty-print types *)
error loc "expected/inferred mismatch"
-and check_patt ctx (Node.Of (loc, p)) va = match p with
+(* Currently, we can only infer types from annotation patterns, but in the
+ * future we will be able to infer type T from p & q if we can infer it from
+ * p (resp., q) and check q (resp., p) against T. *)
+(* TODO: consistency issue: infer_patt returns option, whereas infer raises an
+ * exception *)
+and infer_patt ctx (Node.Of (_, p)) = match p with
| A.PWild -> None
-| A.PBind x -> Some x
-| A.PAnnot (p, b) ->
+| A.PBind _ -> None
+| A.PAnnot (p, a) ->
+ let a = check ctx a (V.Intrin I.Type) in
+ let va = eval ctx.values a in
+ let x = check_patt ctx p va in
+ Some (x, va)
+| A.PData _ -> None
+
+and check_patt ctx (Node.Of (loc, p)) va = match p, va with
+| A.PWild, _ -> None (*[]*)
+| A.PBind x, va -> Some x (*[(x, va)]*)
+| A.PAnnot (p, b), va ->
let b = check ctx b (V.Intrin I.Type) in
let vb = eval ctx.values b in
if conv ctx.len va vb then
@@ -194,7 +231,25 @@ and check_patt ctx (Node.Of (loc, p)) va = match p with
else
(* TODO: pretty-print types *)
error loc "pattern does not unify with inferred type"
-| 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"
+| A.PData _, _ -> failwith "no impl"
+(*
+| A.PData (tag, ps), V.DataType (env, ctors) ->
+ (* TODO: this is similar to checking code for Data. *)
+ begin match IdentMap.find_opt tag ctors with
+ | Some bs ->
+ if List.length ps <> List.length bs then
+ error loc "arity mismatch"
+ else
+ let rec go ctx ps env bs = match ps, bs with
+ | p :: ps, b :: bs ->
+ let vb = eval env b in
+ let binding = check_patt ctx p vb in
+ let v = eval ctx.values arg in
+ arg :: go args (varg :: env) bs
+ | [], [] -> []
+ | _, _ -> failwith "impossible" in
+ I.Data (tag, go args env bs)
+ | None -> error loc ("expected data type with constructor \"" ^ tag ^ "\"")
+ end
+| A.PData _, _ -> error loc "expected data type"
+*)
diff --git a/eval.ml b/eval.ml
@@ -10,26 +10,28 @@ let weaken env l n =
let rec eval env = function
| I.Let (scrutinee, body) -> eval (eval env scrutinee :: env) body
-| I.Case _ -> failwith "no impl: case"
-| I.App (f, args) ->
- begin match eval env f, List.map (eval env) args with
- (* β-reduction *)
- | V.Fn (cap, _, body), vargs -> eval (List.rev_append vargs cap) body
- | V.Intrin I.NatOpAdd, [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
- | V.Intrin I.NatOpMul, [V.Nat m; V.Nat n] -> V.Nat (Z.mul m n)
- (* neutral application *)
- | vf, vargs -> V.App (vf, vargs)
- end
+| I.Switch _ -> failwith "no impl: switch"
+| I.App (callee, args) -> apply (eval env callee) (List.map (eval env) args)
| I.Fn (arity, body) -> V.Fn (env, arity, body)
| I.FnType (arity, doms, cod) -> V.FnType (env, arity, doms, cod)
+| I.Data (tag, args) -> V.Data (tag, List.map (eval env) args)
+| I.DataType ctors -> V.DataType (env, ctors)
| I.Nat n -> V.Nat n
| I.Var i -> List.nth env i
| I.Intrin a -> V.Intrin a
+and apply callee args = match callee, args with
+(* β-reduction *)
+| V.Fn (cap, _, body), args -> eval (List.rev_append args cap) body
+| V.Intrin I.NatOpAdd, [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
+| V.Intrin I.NatOpMul, [V.Nat m; V.Nat n] -> V.Nat (Z.mul m n)
+(* neutral application *)
+| callee, args -> App (callee, args)
+
(* TODO: quote of eval normalizes terms; in some cases below, we probabaly
* don't need to eval before quoting *)
let rec quote l = function
-| V.Case _ -> failwith "no impl: case"
+| V.Switch _ -> failwith "no impl: switch"
| V.App (f, args) -> I.App (quote l f, List.map (quote l) args)
| V.Fn (env, arity, body) ->
let vbody = eval (weaken env l arity) body in
@@ -43,6 +45,14 @@ let rec quote l = function
| [] -> ([], quote l (eval env cod)) in
let (cdoms, ccod) = go l env doms in
I.FnType (arity, cdoms, ccod)
+| V.Data (tag, args) -> I.Data (tag, List.map (quote l) args)
+| V.DataType (env, ctors) ->
+ let rec go l env = function
+ | b :: bs ->
+ let b = quote l (eval env b) in
+ b :: go (l + 1) (V.Arb l :: env) bs
+ | [] -> [] in
+ I.DataType (IdentMap.map (go l env) ctors)
| V.Nat n -> I.Nat n
| V.Arb i -> I.Var (l - i - 1)
| V.Intrin a -> I.Intrin a
@@ -53,7 +63,7 @@ let rec quote_telescope l = function
let rec conv l a b = match a, b with
(* TODO: η-equality? *)
-(* TODO: Case *)
+(* TODO: Switch *)
| 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 (&&)
diff --git a/internal.ml b/internal.ml
@@ -1,5 +1,14 @@
open Common
+(*
+type ('a, 'b) telescope = 'a list * 'b
+(* fn's have telescope domain AND codomain? i.e., telescopic mappings a la
+ * de bruijn. *)
+(* subst's are (term, int) telescope (but the terminology breaks down here) *)
+
+let (@:) tm ty = {tm; ty}
+*)
+
type intrin =
| Type
| NatType
@@ -8,25 +17,59 @@ type intrin =
type term =
| Let of term * term
-| Case of term * case list
+| Switch of term * case list
| App of term * term list
| Fn of int * term
| FnType of int * term list * term
+| Data of ident * term list
+| DataType of term list IdentMap.t
| Nat of Z.t
| Var of index
| Intrin of intrin
+(*| Subst of term * subst*)
and case = patt * term
and patt = patt_discriminant list
and patt_discriminant =
| PattDiscTrue
| PattDiscFalse
| PattDiscData of ident * int
+(*
+and subst =
+| Shift of int (* Nonnegative shift. Shift 0 is the identity substitution. *)
+| Cons of subst * term
+
+let rec cons_vars s = function
+| 0 -> s
+| n -> cons_vars (Cons (s, Var (n - 1))) (n - 1)
+
+(* compose f g is the substitution that does f first and g second. *)
+let rec compose f g = match f, g with
+| Shift 0, g -> g
+| Shift i, Shift j -> Shift (i + j)
+| Shift i, Cons (g, _) -> compose (Shift (i - 1)) g
+| Cons (f, t), g -> Cons (compose f g, substitute t g)
+
+and substitute t f = match t, f with
+| Let (t, u), f -> Let (Subst t f, Subst u f)
+| Switch _, _ -> failwith "no impl: switch"
+| App (t, us), f -> App (Subst (t, f), List.map (fun u -> Subst (u, f)) us)
+| Fn (arity, t), f ->
+ let f = cons_vars (compose f (Shift arity)) arity in
+ Fn (arity, Subst (t, f))
+| Fn (arity, )
+| Nat n -> Nat n
+| Var i, Shift j -> Var (i + j)
+| Var 0, Cons (_, u) -> u
+| Var i, Cons (f, _) -> substitute (Var (i - 1)) f
+| Intrin i, _ -> Intrin i
+| Subst (t, g), f -> substitute t (compose g f)
+*)
let rec to_string m e =
let s = to_string in
let (c, s) = match e with
| Let (scrutinee, body) -> (0, s 1 scrutinee ^ "; " ^ s 0 body)
- | Case _ -> failwith "no impl: case"
+ | Switch _ -> failwith "no impl: switch"
| App (f, args) -> (6, String.concat " " (List.map (s 7) (f :: args)))
| Fn (arity, body) -> (1, "fn " ^ string_of_int arity ^ " => " ^ s 1 body)
| FnType (_, doms, cod) ->
@@ -34,6 +77,13 @@ let rec to_string m e =
| dom :: [] -> s 4 dom
| doms -> "(" ^ String.concat ", " (List.map (s 1) doms) ^ ")" in
(3, sdoms ^ " -> " ^ s 3 cod)
+ | Data (tag, ts) ->
+ (6, "@" ^ String.concat " " (tag :: List.map (s 7) ts))
+ | DataType ctors ->
+ let string_of_ctor (tag, ts) =
+ "@" ^ String.concat " " (tag :: List.map (s 7) ts) in
+ let ctors = List.map string_of_ctor (IdentMap.to_list ctors) in
+ (8, "#[" ^ String.concat "; " ctors ^ "]")
| Nat n -> (8, Z.to_string n)
| Var i -> (8, "?" ^ string_of_int i)
| Intrin Type -> (8, "`Type")
diff --git a/lexer.mll b/lexer.mll
@@ -67,6 +67,8 @@ rule token = parse
| "{" { LBRACE }
| "}" { RBRACE }
+| "=" { EQ }
+
| "+" { PLUS }
| "*" { ASTERISK }
diff --git a/main.ml b/main.ml
@@ -8,7 +8,7 @@ let buf = Lexing.from_string "\
five Nat 0 (fn n => n + 1)\n\
"
*)
-let buf = Lexing.from_string "Type := 3; Type := 4; Type#2"
+let buf = Lexing.from_string "T := #[@a Nat; @b #()]; @a 3 : T"
let concrete =
try Parser.start Lexer.token buf with
diff --git a/parser.mly b/parser.mly
@@ -12,6 +12,7 @@ let (@$) = locate
%token HASH_LPAREN LPAREN RPAREN
%token HASH_LBRACK LBRACK RBRACK
%token HASH_LBRACE LBRACE RBRACE
+%token EQ
%token PLUS ASTERISK
%token PIPE AMPERSAND
%token MATCH
@@ -97,11 +98,11 @@ expr8:
| IDENT_INDEX { 1 @$ let (x, i) = $1 in IdentIndex (x, i) }
| IDENT { 1 @$ Ident $1 }
| NAT { 1 @$ Nat $1 }
- | HASH_LBRACK cons_list RBRACK { 1 @$ VariantType $2 }
+ | HASH_LBRACK ctor_list RBRACK { 1 @$ VariantType $2 }
| HASH_LPAREN expr2_list RPAREN { 1 @$ TupleType (List.map annot $2) }
- | HASH_LBRACE expr2_list RBRACE { 1 @$ RecordType (List.map annot $2) }
+ | HASH_LBRACE annot_field_list RBRACE { 1 @$ RecordType $2 }
| paren_expr_list %prec PREC_TUPLE { 1 @$ Tuple $1 }
- | LBRACE field_list RBRACE { 1 @$ Record $2 }
+ | LBRACE term_field_list RBRACE { 1 @$ Record $2 }
| LPAREN RPAREN { 1 @$ Unit }
| LPAREN expr0 RPAREN { 1 @$ Paren $2 }
@@ -128,18 +129,32 @@ case_list:
| case { [$1] }
| { [] }
-cons:
- | AT IDENT expr2_list { 1 @$ Cons ($2, List.map annot $3) }
-cons_list:
- | cons SEMICOLON cons_list { $1 :: $3 }
- | cons { [$1] }
+ctor:
+ | AT IDENT expr2_list { 1 @$ Ctor ($2, List.map annot $3) }
+ctor_list:
+ | ctor SEMICOLON ctor_list { $1 :: $3 }
+ | ctor { [$1] }
| { [] }
-field:
+annot_field:
+ | IDENT COLON expr2 {
+ let ann = 2 @$ APatt (1 @$ PBind $1, $3) in
+ 2 @$ Field.Of ($1, ann)
+ }
+ | IDENT EQ expr3 COLON expr2 {
+ let ann = 4 @$ APatt (2 @$ PAnd (1 @$ PBind $1, patt $3), $5) in
+ 4 @$ Field.Of ($1, ann)
+ }
+annot_field_list:
+ | annot_field COMMA annot_field_list { $1 :: $3 }
+ | annot_field { [$1] }
+ | { [] }
+
+term_field:
| IDENT COLON_EQ expr1 { 2 @$ Field.Of ($1, $3) }
-field_list:
- | field COMMA field_list { $1 :: $3 }
- | field { [$1] }
+term_field_list:
+ | term_field COMMA term_field_list { $1 :: $3 }
+ | term_field { [$1] }
| { [] }
%%
diff --git a/value.ml b/value.ml
@@ -1,11 +1,16 @@
open Common
module I = Internal
+(* TODO: Abstract notion of closure, so we don't need to manage environments
+ * ad-hoc while elaborating (it's error prone!). *)
+
type value =
-| Case of value * environ * I.case list
+| Switch of value * environ * I.case list
| App of value * value list
| Fn of environ * int * I.term
| FnType of environ * int * I.term list * I.term
+| Data of ident * value list
+| DataType of environ * I.term list IdentMap.t
| Nat of Z.t
| Arb of level
| Intrin of I.intrin
