commit cf53b44cb71672987ab0f078f94b0645eb646398
parent 9eb795db62dcf1c0a587ae41a7c74abd615cf244
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Tue, 19 Dec 2023 21:36:42 -0800
Rework concrete and abstract syntax
WIP
Diffstat:
15 files changed, 336 insertions(+), 231 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -5,4 +5,5 @@ lexer.ml
parser.ml
parser.output
test
+test2
main
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-main: common.ml concrete.ml parser.ml lexer.ml abstract.ml conctoabs.ml core.ml value.ml eval.ml elab.ml main.ml
+main: loc.ml node.ml common.ml field.ml concrete.ml parser.ml lexer.ml abstract.ml cnctoabs.ml main.ml #core.ml value.ml eval.ml elab.ml main.ml
ocamlfind ocamlopt -o $@ -g -linkpkg -package zarith $^
lexer.ml: lexer.mll
diff --git a/abstract.ml b/abstract.ml
@@ -1,30 +1,49 @@
open Common
+(* Abstract syntax is "desugared" concrete syntax. *)
+
(* 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 =
+type term = term' Node.t
+and term' =
| Let of patt * term * term
| Match of term * case list
| Annot of term * term
| App of term * term list
-| Access of term * ident
-| Index of term * term
-| Deref of term
| Fn of patt list * term
-| FnType of (patt * term) list * term
-| Data of ident * (ident * term) list (* TODO: constructor tag should be path eventually *)
-| DataType of (ident * (patt * term) list) list
+| FnType of annot list * term
+| Data of ident * term Field.t list
+| DataType of cons list
| Nat of Z.t
| Ident of ident
-and patt =
+(*
+| Access of term * ident
+| Index of term * term
+| Deref of 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
-| PAssign of term
| PAnnot of patt * term
-| PData of ident * (ident * patt) list
+| PData of ident * patt Field.t list
| PNat of Z.t
| PAnd of patt * patt
| POr of patt * patt
-and case = Case of {patt: patt; guard: term option; body: term}
+(*
+| PAssign of term
+*)
+
+and annot = annot' Node.t
+and annot' =
+| AType of term
+| APatt of patt * term
diff --git a/cnctoabs.ml b/cnctoabs.ml
@@ -0,0 +1,76 @@
+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
+
+let rec term = function
+| Node.Of (_, C.Paren t) -> term t
+| n -> Node.map term' n
+and term' = function
+| C.Let (p, scrutinee, body) -> A.Let (patt p, term scrutinee, term body)
+(* TODO: Maybe Seq should desugar to a unit pattern instead, so that
+ * 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, [
+ 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, [
+ Loc.None @$ A.Case (Loc.None @$ A.PData ("true", []), term t);
+ Loc.None @$ A.Case (Loc.None @$ A.PWild, Loc.None @$ A.Data ("", []));
+ ])
+| C.Annot (t, u) -> A.Annot (term t, term u)
+| C.Add (t, u) -> A.App (Loc.None @$ A.Ident "`+", [term t; term u])
+| C.Mul (t, u) -> A.App (Loc.None @$ A.Ident "`*", [term t; term u])
+| C.Or (t, u) -> A.App (Loc.None @$ A.Ident "`|", [term t; term u])
+| C.And (t, u) -> A.App (Loc.None @$ A.Ident "`&", [term t; term u])
+| 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.Unit -> A.Data ("", [])
+| C.Nat n -> A.Nat n
+| C.Underscore -> failwith "no impl: holes"
+| C.Ident x -> A.Ident x
+| C.Paren _ -> failwith "impossible"
+
+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
+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.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.PParen _ -> failwith "impossible"
+
+and annot = function
+| Node.Of (_, C.AParen a) -> annot a
+| n -> Node.map annot' n
+and annot' = function
+| C.AType t -> A.AType (term t)
+| C.APatt (p, t) -> A.APatt (patt p, term t)
+| C.AParen _ -> failwith "impossible"
diff --git a/common.ml b/common.ml
@@ -2,8 +2,15 @@ type ident = string
type index = int
type level = int
+(*
+exception Error of loc * msg
+let error loc msg = raise (TypeError)
+*)
+
(* 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
| [], [] -> true
| _, _ -> invalid_arg "all2: lists have different length"
+
+let (@$) loc x = Node.Of (loc, x)
diff --git a/concrete.ml b/concrete.ml
@@ -1,31 +1,96 @@
open Common
-type expr =
-| Let of expr * expr * expr
-| Seq of expr * expr
-| Match of expr * case list
-| If of expr * expr * expr
-| Iff of expr * 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
-| Deref of expr
-| Fn of expr list * expr
-| FnType of expr list * expr
-| Variant of ident * expr list
-| VariantType of (ident * expr list) list
-| Tuple of expr list
-| TupleType of expr list
-| Record of (ident * expr) list
-| RecordType of (ident * expr) list
+exception InvalidPattern
+
+type term = term' Node.t
+and term' =
+| Let of patt * term * term
+| Seq of term * term
+| Match of term * case list
+| If of term * term * term
+| Iff of term * term
+| Annot of term * term
+| Add of term * term
+| Mul of term * term
+| Or of term * term
+| And of term * term
+| App of term * term list
+| Fn of patt list * term
+| FnType of annot list * term
+| Variant of ident * term list
+| VariantType of cons list
+| Tuple of term list
+| TupleType of annot list
+| Record of term Field.t list
+| RecordType of annot list
| Unit
| Nat of Z.t
| Underscore
| Ident of ident
-| Paren of expr
-and case = Case of {patt: expr; guard: expr option; body: expr}
+| Paren of term
+(*
+| Access of term * ident
+| Index of term * term
+| Deref of 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
+| PVariant of ident * patt list
+| PTuple of patt list
+| PRecord of patt Field.t list
+| PUnit
+| PNat of Z.t
+| PAnd of patt * patt
+| POr of patt * patt
+| PParen of patt
+(*
+| PAssign of term
+*)
+
+and annot = annot' Node.t
+and annot' =
+| AType of term
+| APatt of patt * term
+| AParen of annot
+
+let rec patt p = Node.map patt' p
+and patt' = function
+| Let _ -> raise InvalidPattern
+| Seq _ -> raise InvalidPattern
+| Match _ -> raise InvalidPattern
+| If _ -> raise InvalidPattern
+| Iff _ -> raise InvalidPattern
+| Annot (p, t) -> PAnnot (patt p, t)
+| Add _ -> raise InvalidPattern (* TODO: n + k patterns? *)
+| Mul _ -> raise InvalidPattern
+| Or (p, q) -> POr (patt p, patt q)
+| And (p, q) -> PAnd (patt p, patt q)
+| App _ -> raise InvalidPattern
+| Fn _ -> raise InvalidPattern
+| FnType _ -> raise InvalidPattern
+| Variant (x, ts) -> PVariant (x, List.map patt ts)
+| VariantType _ -> raise InvalidPattern
+| Tuple ts -> PTuple (List.map patt ts)
+| TupleType _ -> raise InvalidPattern
+| Record tfs -> PRecord (List.map (Field.map patt) tfs)
+| RecordType _ -> raise InvalidPattern
+| Unit -> PUnit
+| Nat n -> PNat n
+| Underscore -> PWild
+| Ident x -> PBind x
+| Paren p -> PParen (patt p)
+
+let rec annot = function
+| Node.Of (loc, Annot (p, t)) -> loc @$ APatt (patt p, t)
+| Node.Of (loc, Paren a) -> loc @$ AParen (annot a)
+| Node.Of (loc, _) as n -> loc @$ AType n
diff --git a/conctoabs.ml b/conctoabs.ml
@@ -1,89 +0,0 @@
-open Common
-module C = Concrete
-module A = Abstract
-
-exception InvalidPattern
-
-let rec map_ordered f =
- let rec go i = function
- | [] -> []
- | e :: es -> (string_of_int i, f e) :: go (i + 1) es in
- go 0
-
-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.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};
- A.Case {patt = A.PWild; guard = None; body = term c};
- ])
-| C.Iff (a, b) -> A.Match (term a, [
- A.Case {patt = A.PData ("true", []); guard = None; body = term b};
- A.Case {patt = A.PWild; guard = None; body = A.Data ("", [])};
- ])
-| 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)
-| C.Deref a -> A.Deref (term a)
-| 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 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 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"
-| C.Ident x -> A.Ident x
-| C.Paren a -> term a
-
-and patt = function
-| C.Let _ -> raise InvalidPattern
-| C.Seq _ -> raise InvalidPattern
-| C.Match _ -> raise InvalidPattern
-| C.If _ -> raise InvalidPattern
-| C.Iff _ -> raise InvalidPattern
-| 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
-| C.Deref a -> A.PAssign (term a)
-| C.Fn _ -> raise InvalidPattern
-| C.FnType _ -> raise InvalidPattern
-| C.Variant (x, es) -> A.PData (x, map_ordered patt es)
-| C.VariantType _ -> raise InvalidPattern
-| C.Tuple es -> A.PData ("", map_ordered patt es)
-| C.TupleType _ -> raise InvalidPattern
-| C.Record xes -> A.PData ("", map_named patt xes)
-| C.RecordType _ -> raise InvalidPattern
-| C.Unit -> A.PData ("", [])
-| 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}
-
-and annot = function
-| C.Annot (a, b) -> (patt a, term b)
-| b -> (A.PWild, term b)
diff --git a/elab.ml b/elab.ml
@@ -1,7 +1,7 @@
open Common
open Eval
module A = Abstract
-module C = Core
+module I = Internal
module V = Value
(* TODO: use a hashtable or map for ident -> level lookups *)
@@ -21,55 +21,50 @@ let default_ctx = {
Some "Type";
];
values = [
- V.Intrin C.NatOpMul;
- V.Intrin C.NatOpAdd;
- V.Intrin C.NatType;
- V.Intrin C.Type;
+ V.Intrin I.NatOpMul;
+ V.Intrin I.NatOpAdd;
+ V.Intrin I.NatType;
+ V.Intrin I.Type;
];
types =
let nat_op_type = V.FnType (
[],
2,
- [C.Intrin C.NatType; C.Intrin C.NatType],
- C.Intrin C.NatType
+ [I.Intrin I.NatType; I.Intrin I.NatType],
+ I.Intrin I.NatType
) in
- [nat_op_type; nat_op_type; V.Intrin C.Type; V.Intrin C.Type];
+ [nat_op_type; nat_op_type; V.Intrin I.Type; V.Intrin I.Type];
}
-(* Add `x := v : t` to ctx. *)
-let bind_def ctx x v t = {
+(* Add `x := v : a` to ctx. *)
+let bind_def ctx x v a = {
len = 1 + ctx.len;
names = x :: ctx.names;
values = v :: ctx.values;
- types = t :: ctx.types;
+ types = a :: ctx.types;
}
-(* Add `x : t` to ctx. *)
-let bind_arb ctx x t = bind_def ctx x (V.Arb ctx.len) t
-
-let rec bind_arb_telescope ctx xs ts = match xs, ts with
-| x :: xs, t :: ts -> bind_arb_telescope (bind_arb ctx x t) xs ts
-| [], [] -> ctx
-| _, _ -> failwith "impossible"
+(* Add `x : a` to ctx. *)
+let bind_arb ctx x a = bind_def ctx x (V.Arb ctx.len) a
let rec infer ctx = function
| A.Let (A.PAnnot (p, a), scrutinee, body) ->
- let a = check ctx a (V.Intrin C.Type) 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
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)
+ (I.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)
+ (I.Let (scrutinee, body), vb)
| A.Match _ -> failwith "no impl: match"
| A.Annot (tm, a) ->
- let a = check ctx a (V.Intrin C.Type) in
+ let a = check ctx a (V.Intrin I.Type) in
let va = eval ctx.values a in
let tm = check ctx tm va in
(tm, va)
@@ -90,7 +85,7 @@ let rec infer ctx = function
| [], [] -> ([], eval env cod)
| _, _ -> failwith "impossible" in
let (args, vcod) = go env args doms in
- (C.App (f, args), vcod)
+ (I.App (f, args), vcod)
| _ -> failwith "type error: expected function type in application"
end
| A.Access _ -> failwith "no impl: access"
@@ -99,7 +94,7 @@ let rec infer ctx = function
| A.Fn (ps, body) ->
let rec go ctx = function
| A.PAnnot (p, dom) :: ps ->
- let dom = check ctx dom (V.Intrin C.Type) in
+ let dom = check ctx dom (V.Intrin I.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
@@ -112,25 +107,25 @@ let rec infer ctx = function
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))
+ (I.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
| (p, dom) :: anns ->
- let cdom = check ctx dom (V.Intrin C.Type) in
+ let cdom = check ctx dom (V.Intrin I.Type) in
let vdom = eval ctx.values cdom in
let x = check_patt ctx p vdom in
let (cdoms, ccod) = go (bind_arb ctx x vdom) anns in
(cdom :: cdoms, ccod)
- | [] -> ([], check ctx cod (V.Intrin C.Type)) in
+ | [] -> ([], check ctx cod (V.Intrin I.Type)) in
let (cdoms, ccod) = go ctx anns in
- (C.FnType (arity, cdoms, ccod), V.Intrin C.Type)
+ (I.FnType (arity, cdoms, ccod), V.Intrin I.Type)
| A.Data _ -> failwith "no impl: data"
| A.DataType _ -> failwith "no impl: data type"
-| A.Nat n -> (C.Nat n, V.Intrin C.NatType)
+| A.Nat n -> (I.Nat n, V.Intrin I.NatType)
| A.Ident x ->
let rec go i ys ts = match ys, ts with
- | Some y :: ys, t :: ts -> if x = y then (C.Var i, t) else go (i + 1) ys ts
+ | Some y :: ys, t :: ts -> if x = y then (I.Var i, t) else go (i + 1) ys ts
| None :: ys, _ :: ts -> go (i + 1) ys ts
| [], [] -> failwith ("unbound identifier: " ^ x)
| _, _ -> failwith "impossible" in
@@ -139,19 +134,19 @@ let rec infer ctx = function
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 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
- C.Let (scrutinee, body)
+ I.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)
+ I.Let (scrutinee, body)
| A.Fn (ps, body), V.FnType (env, arity, doms, cod) ->
if List.length ps <> arity then
failwith "type error: arity mismatch"
@@ -168,7 +163,7 @@ and check ctx tm vty = match tm, vty with
check ctx body vcod
| _, _ -> failwith "impossible" in
let cbody = go ctx ps env doms in
- C.Fn (arity, cbody)
+ I.Fn (arity, cbody)
| tm, vexpected ->
let (tm, vinferred) = infer ctx tm in
if conv ctx.len vexpected vinferred then
@@ -176,15 +171,15 @@ and check ctx tm vty = match tm, vty with
else
failwith "type error: expected/inferred mismatch"
-and check_patt ctx p t = match p with
+and check_patt ctx {loc; x = p} va = match p with
| A.PWild -> None
| A.PBind x -> Some x
| A.PAssign _ -> failwith "no impl: assign pattern"
-| 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
- check_patt ctx p t
+| A.PAnnot (p, b) ->
+ let b = check ctx b (V.Intrin I.Type) in
+ let vb = eval ctx.values cb in
+ if conv ctx.len va vb then
+ check_patt ctx p va
else
failwith "pattern does not unify with inferred type"
| A.PData _ -> failwith "no impl: data pattern"
diff --git a/field.ml b/field.ml
@@ -0,0 +1,7 @@
+open Common
+
+type 'a t = 'a t' Node.t
+and 'a t' = Of of ident * 'a
+
+let map' f (Of (id, x)) = Of (id, f x)
+let map f = Node.map (map' f)
diff --git a/core.ml b/internal.ml
diff --git a/lexer.mll b/lexer.mll
@@ -1,6 +1,12 @@
{
+open Common
open Parser
-exception LexerError of Lexing.position * string
+
+exception LexerError of Loc.t * string
+
+let error lexbuf msg =
+ let loc = Loc.of_position (Lexing.lexeme_start_p lexbuf) in
+ raise (LexerError (loc, msg))
}
let dnumeral = ['0'-'9']
@@ -81,7 +87,10 @@ rule token = parse
| ident_start ident_cont* { IDENT (Lexing.lexeme lexbuf) }
| number { NAT (Z.of_string (Lexing.lexeme lexbuf)) }
-| number invalid_number_terminator { raise (LexerError (Lexing.lexeme_start_p lexbuf, "invalid terminator after integer literal")) }
+| number invalid_number_terminator
+ { error lexbuf "invalid terminator after integer literal" }
+
+| _ { error lexbuf "invalid byte" }
(*
| "<" { LT }
diff --git a/loc.ml b/loc.ml
@@ -0,0 +1,10 @@
+type t =
+| None
+| Loc of int * int
+
+let of_position (pos: Lexing.position) =
+ Loc (pos.pos_lnum, pos.pos_cnum - pos.pos_bol)
+
+let to_string = function
+| None -> "?:?"
+| Loc (row, col) -> string_of_int row ^ ":" ^ string_of_int col
diff --git a/main.ml b/main.ml
@@ -7,11 +7,14 @@ let buf = Lexing.from_string "\
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 abstract = Cnctoabs.term concrete
+(*
let ctx = Elab.default_ctx
let (core, core_type) = Elab.infer ctx abstract
let norm = Eval.quote ctx.len (Eval.eval ctx.values core)
let () = print_endline (Core.to_string 0 core)
let () = print_endline (Core.to_string 0 norm)
+*)
diff --git a/node.ml b/node.ml
@@ -0,0 +1,3 @@
+type 'a t = Of of Loc.t * 'a
+
+let map f (Of (loc, x)) = Of (loc, f x)
diff --git a/parser.mly b/parser.mly
@@ -1,5 +1,9 @@
%{
+open Common
open Concrete
+
+let locate i x = Loc.of_position (Parsing.rhs_start_pos i) @$ x
+let (@$) = locate
%}
%token EOF
@@ -19,7 +23,7 @@ open Concrete
%token <Z.t> NAT
%start start
-%type <Concrete.expr> start
+%type <Concrete.term> start
%nonassoc PREC_TUPLE
%nonassoc SINGLE_ARROW
@@ -39,73 +43,73 @@ open Concrete
start: expr0 EOF { $1 }
expr0: (* Sequencing *)
- | expr1 COLON_EQ expr1 SEMICOLON expr0 { Let ($1, $3, $5) }
- | expr1 SEMICOLON expr0 { Seq ($1, $3) }
+ | expr2 COLON_EQ expr1 SEMICOLON expr0 { 2 @$ Let (patt $1, $3, $5) }
+ | expr1 SEMICOLON expr0 { 2 @$ Seq ($1, $3) }
| expr1 { $1 }
expr1: (* Control flow *)
- | expr2 MATCH LBRACE cases RBRACE { Match($1, $4) }
- | IF expr1 THEN expr1 ELSE expr1 { If ($2, $4, $6) }
- | IFF expr1 DO expr1 { Iff ($2, $4) }
- | FN annot_list DOUBLE_ARROW expr1 { Fn ($2, $4) }
+ | expr2 MATCH LBRACE case_list RBRACE { 2 @$ Match($1, $4) }
+ (* if let: "if p := x then t else f"; and similarly for iff *)
+ | IF expr1 THEN expr1 ELSE expr1 { 1 @$ If ($2, $4, $6) }
+ | IFF expr1 DO expr1 { 1 @$ Iff ($2, $4) }
+ | FN expr2_list DOUBLE_ARROW expr1 { 1 @$ Fn (List.map patt $2, $4) }
| expr2 { $1 }
-expr2: (* Type annotations (right-associative); lowest prec for patterns *)
- | expr3 COLON expr2 { Annot($1, $3) }
+expr2: (* Type annotations (right-associative) *)
+ | expr3 COLON expr2 { 2 @$ Annot ($1, $3) }
| expr3 { $1 }
expr3: (* Function arrow (right-associative) *)
- | expr6 SINGLE_ARROW expr3 { FnType ([$1], $3) }
- | tuple SINGLE_ARROW expr3 { FnType ($1, $3) }
+ | expr6 SINGLE_ARROW expr3 { 2 @$ FnType ([annot $1], $3) }
+ | paren_expr_list SINGLE_ARROW expr3 { 2 @$ FnType (List.map annot $1, $3) }
| expr4 { $1 }
expr4: (* Additive binary operators (left-associative) *)
- | expr4add PLUS expr5 { Add ($1, $3) }
- | expr4or PIPE expr5 { Or ($1, $3) }
+ | expr4add PLUS expr5 { 2 @$ Add ($1, $3) }
+ | expr4or PIPE expr5 { 2 @$ Or ($1, $3) }
| expr5 { $1 }
expr4add:
- | expr4add PLUS expr5 { Add ($1, $3) }
+ | expr4add PLUS expr5 { 2 @$ Add ($1, $3) }
| expr5 { $1 }
expr4or:
- | expr4or PIPE expr5 { Or ($1, $3) }
+ | expr4or PIPE expr5 { 2 @$ Or ($1, $3) }
| expr5 { $1 }
expr5: (* Multiplicative binary operators (left-associative) *)
- | expr5mul ASTERISK expr6 { Mul ($1, $3) }
- | expr5and AMPERSAND expr6 { And ($1, $3) }
+ | expr5mul ASTERISK expr6 { 2 @$ Mul ($1, $3) }
+ | expr5and AMPERSAND expr6 { 2 @$ And ($1, $3) }
| expr6 { $1 }
expr5mul:
- | expr5mul ASTERISK expr6 { Mul ($1, $3) }
+ | expr5mul ASTERISK expr6 { 2 @$ Mul ($1, $3) }
| expr6 { $1 }
expr5and:
- | expr5and AMPERSAND expr6 { And ($1, $3) }
+ | expr5and AMPERSAND expr6 { 2 @$ And ($1, $3) }
| expr6 { $1 }
expr6:
- | expr7 expr7 expr7_apposition { App ($1, $2 :: $3) }
- | AT IDENT expr7_apposition { Variant ($2, $3) }
+ | expr7 expr7 expr7_apposition { 1 @$ App ($1, $2 :: $3) }
+ | AT IDENT expr7_apposition { 1 @$ Variant ($2, $3) }
| expr7 { $1 }
expr7:
- | expr7 DOT IDENT { Access ($1, $3) }
- | expr7 DOT LPAREN expr0 RPAREN { Index ($1, $4) }
- | expr7 EXCLAM { Deref $1 }
+ (*
+ | expr7 DOT IDENT { 2 @$ Access ($1, $3) }
+ | expr7 DOT LPAREN expr0 RPAREN { 2 @$ Index ($1, $4) }
+ | expr7 EXCLAM { 2 @$ Deref $1 }
+ *)
| expr8 { $1 }
expr8:
- | UNDERSCORE { Underscore }
- | IDENT { Ident $1 }
- | NAT { Nat $1 }
- | HASH_LBRACK variant_def_list RBRACK { VariantType $2 }
- | HASH_LPAREN annot_list RPAREN { TupleType $2 }
- | HASH_LBRACE field_def_list RBRACE { RecordType $2 }
- | tuple %prec PREC_TUPLE { Tuple $1 }
- | LBRACE field_list RBRACE { Record $2 }
- | LPAREN RPAREN { Unit }
- | LPAREN expr0 RPAREN { Paren $2 }
-
-cases: (* Has optional trailing semicolon *)
- | case SEMICOLON cases { $1 :: $3 }
- | case { [$1] }
+ | UNDERSCORE { 1 @$ Underscore }
+ | IDENT { 1 @$ Ident $1 }
+ | NAT { 1 @$ Nat $1 }
+ | HASH_LBRACK cons_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) }
+ | paren_expr_list %prec PREC_TUPLE { 1 @$ Tuple $1 }
+ | LBRACE field_list RBRACE { 1 @$ Record $2 }
+ | LPAREN RPAREN { 1 @$ Unit }
+ | LPAREN expr0 RPAREN { 1 @$ Paren $2 }
+
+expr1_list:
+ | expr1 COMMA expr1_list { $1 :: $3 }
+ | expr1 { [$1] }
| { [] }
-case:
- | expr2 IF expr1 DOUBLE_ARROW expr1 { Case {patt = $1; guard = Some ($3); body = $5} }
- | expr2 DOUBLE_ARROW expr1 { Case {patt = $1; guard = None; body = $3} }
-annot_list: (* Has optional trailing comma *)
- | expr2 COMMA annot_list { $1 :: $3 }
+expr2_list:
+ | expr2 COMMA expr2_list { $1 :: $3 }
| expr2 { [$1] }
| { [] }
@@ -113,32 +117,27 @@ expr7_apposition:
| expr7 expr7_apposition { $1 :: $2 }
| { [] }
-variant_def_list: (* Has optional trailing semicolon *)
- | variant_def SEMICOLON variant_def_list { $1 :: $3 }
- | variant_def { [$1] }
- | { [] }
-variant_def:
- | AT IDENT annot_list { ($2, $3) }
+paren_expr_list: LPAREN expr1 COMMA expr1_list RPAREN { $2 :: $4 }
-field_def_list: (* Has optional trailing comma *)
- | field_def COMMA field_def_list { $1 :: $3 }
- | field_def { [$1] }
+case:
+ | expr2 DOUBLE_ARROW expr1 { 2 @$ Case (patt $1, $3) }
+case_list:
+ | case COMMA case_list { $1 :: $3 }
+ | case { [$1] }
| { [] }
-field_def:
- | IDENT COLON expr2 { ($1, $3) }
-tuple: (* Nonempty; trailing comma mandatory for 1-tuples *)
- | LPAREN expr1 COMMA expr1_list RPAREN { $2 :: $4 }
-expr1_list: (* Has optional trailing comma *)
- | expr1 COMMA expr1_list { $1 :: $3 }
- | expr1 { [$1] }
+cons:
+ | AT IDENT expr2_list { 1 @$ Cons ($2, List.map annot $3) }
+cons_list:
+ | cons SEMICOLON cons_list { $1 :: $3 }
+ | cons { [$1] }
| { [] }
-field_list: (* Has optional trailing comma *)
+field:
+ | IDENT COLON_EQ expr1 { 2 @$ Field.Of ($1, $3) }
+field_list:
| field COMMA field_list { $1 :: $3 }
| field { [$1] }
| { [] }
-field:
- | IDENT COLON_EQ expr1 { ($1, $3) }
%%
