commit b6e9ede1270d59ca6bde8e6e1cd1885550586527
parent 5377553a6de6ea89292b8f5ea8199d249ee25e9d
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Tue, 9 Jan 2024 00:19:18 -0800
Improve error handling; make 0-ary functions desugar to Unit domain
Diffstat:
8 files changed, 123 insertions(+), 36 deletions(-)
diff --git a/ctx.ml b/ctx.ml
@@ -21,7 +21,7 @@ let empty = {
let assign ctx names typ value =
let asn = {typ; value; active = true} in
- let shadow ctx name =
+ let shadow ctx {data = name; _} =
let add_to_tsil = function
| None -> Some (Snoc (Lin, asn))
| Some t -> Some (Snoc (t, asn)) in
diff --git a/desugar.ml b/desugar.ml
@@ -5,6 +5,14 @@ module A = Abstract
exception Error of Loc.t * string
let error loc msg = raise (Error (loc, msg))
+let patt_wild = Loc.None @$ A.PWild
+let patt_true = Loc.None @$ A.PData (Tag.Of "true", [||])
+let term_unit = Loc.None @$ A.Data (Tag.Of "", [||])
+let term_unit_typ =
+ Loc.None @$ A.DataType (Tag.Map.singleton (Tag.Of "") (Loc.None @$ A.Ctor [||]))
+let patt_wild_unit =
+ Loc.None @$ A.PAnnot (patt_wild, term_unit_typ)
+
let rec term = function
(* Handle parens specially, so that we use the inner loc. *)
| {data = C.Paren t; _} -> term t
@@ -16,20 +24,20 @@ and term' loc = function
| C.Seq (t, u) ->
let definer = Loc.None @$ {
A.recursive = false;
- A.lhs = Loc.None @$ A.PWild;
+ A.lhs = patt_wild;
A.rhs = term t;
} in
A.Let ([|definer|], term u)
| C.Match (scrutinee, cases) -> A.Match (term scrutinee, Array.map case cases)
| C.If (c, t, f) ->
A.Match (term c, [|
- Loc.None @$ A.Case (Loc.None @$ A.PData (Tag.Of "true", [||]), term t);
- Loc.None @$ A.Case (Loc.None @$ A.PWild, term f);
+ Loc.None @$ A.Case (patt_true, term t);
+ Loc.None @$ A.Case (patt_wild, term f);
|])
| C.Iff (c, t) ->
A.Match (term c, [|
- Loc.None @$ A.Case (Loc.None @$ A.PData (Tag.Of "true", [||]), term t);
- Loc.None @$ A.Case (Loc.None @$ A.PWild, Loc.None @$ A.Data (Tag.Of "", [||]));
+ Loc.None @$ A.Case (patt_true, term t);
+ Loc.None @$ A.Case (patt_wild, term_unit);
|])
| C.Annot (t, u) -> A.Annot (term t, term u)
(* TODO: Idea: Modify variables in abstract syntax to have a level instead of
@@ -39,7 +47,17 @@ and term' loc = function
| C.Add (t, u) -> A.App (Loc.None @$ A.Var (Name.Of "`+", 0), [|term t; term u|])
| C.Mul (t, u) -> A.App (Loc.None @$ A.Var (Name.Of "`*", 0), [|term t; term u|])
| C.App (fn, args) -> A.App (term fn, Array.map term args)
-| C.Fn (params, body) -> A.Fn (Array.map param params, term body)
+| C.Fn (params, body) ->
+ let params =
+ if Array.length params = 0 then
+ [|Loc.None @$ {
+ A.plicity = Plicity.Ex;
+ A.patt = patt_wild_unit;
+ A.typ = None;
+ }|]
+ else
+ Array.map param params in
+ A.Fn (params, term body)
| C.FnType (doms, cod) -> A.FnType (Array.map domain doms, term cod)
| C.Variant (tag, fields) -> A.Data (tag, Array.map term fields)
| C.VariantType ctors ->
diff --git a/elab.ml b/elab.ml
@@ -24,6 +24,7 @@ and error' =
| ErrFnArityMismatch
| ErrFnPlicityMismatch
| ErrUnexpectedCtor of Tag.t
+| ErrDuplicateName of Name.t
let rec string_of_error {loc; data = e} =
Loc.to_string loc ^ " " ^ string_of_error' e
@@ -44,6 +45,7 @@ and string_of_error' = function
| ErrFnArityMismatch -> "ErrFnArityMismatch"
| ErrFnPlicityMismatch -> "ErrFnPlicityMismatch"
| ErrUnexpectedCtor _ -> "ErrUnexpectedCtor"
+| ErrDuplicateName _ -> "ErrDuplicateName"
exception Exn of error
@@ -56,6 +58,12 @@ exception BlockedOnFuture of Uniq.t * int * Name.t
* end with a prime, which returns in the result monad.
* TODO: Make sure every function has both versions, even if unused? *)
+let declare_name' name_set {loc; data = name} =
+ if Name.Set.mem name name_set then
+ abort (loc @$ ErrDuplicateName name)
+ else
+ Name.Set.add name name_set
+
let rec infer ctx t =
try Ok (infer' ctx t) with
| Exn e -> Error e
@@ -65,7 +73,8 @@ and infer' (ctx: 'a Ctx.context) {loc; data = t} = match t with
let (body, vtyp) = infer' ctx body in
(I.Let (definers, body), vtyp)
-| A.Match _ -> no_impl "infer match"
+| A.Match (scrutinee, cases) -> no_impl ""
+ (*let (scrutinee, vtyp) = infer' ctx scrutinee in *)
| A.Annot (t, a) ->
let a = check' ctx a V.Type in
@@ -288,10 +297,12 @@ and infer_definers' ctx definers =
* assignments. We later set the active flag to false on assignments
* for non-recusive definers, so that the rhs of non-recursive definers
* can not access their own assignment. *)
+ let name_set = ref Name.Set.empty in
let ctx_with_asns = ref ctx in
let asns = Array.make ndefiners garbage in
for i = 0 to ndefiners - 1 do
let (names, vtyp) = infer_lhs' ctx definers.(i) in
+ name_set := Array.fold_left declare_name' !name_set names;
let (ctx', asn) = Ctx.assign !ctx_with_asns names vtyp (V.Arb vars.(i)) in
ctx_with_asns := ctx';
asns.(i) <- asn
@@ -388,11 +399,14 @@ and infer_binders' ctx loc binders =
let vars = Uniq.fresh arity in
let ctx = Ctx.bind ctx vars in
+
(* Add future assignments to ctx. *)
+ let name_set = ref Name.Set.empty in
let ctx = ref ctx in
let asns = Array.make arity garbage in
for i = 0 to arity - 1 do
let names = irrefutable_patt_names binders.(i).data.patt in
+ name_set := Array.fold_left declare_name' !name_set names;
let typ = V.Future (id, i) in
let value = V.Arb vars.(i) in
let (ctx', asn) = Ctx.assign !ctx names typ value in
@@ -499,6 +513,12 @@ and infer_ctor' ctx {loc; data = A.Ctor binders} =
let (_, binders) = infer_binders' ctx loc binders in
binders
+(* XXX: We're assuming in at least one place (the single non-recursive definer
+ * case in infer_definers') that these functions that operate on patterns
+ * never return an array with duplicated names. (Actually, duplicate names in
+ * multibinders is no problem, but we want to forbid them to avoid programmer
+ * errors.) *)
+
and infer_irrefutable_patt ctx patt =
try Ok (infer_irrefutable_patt' ctx patt) with
| Exn e -> Error e
@@ -517,7 +537,7 @@ and check_irrefutable_patt ctx patt vtyp =
| Exn e -> Error e
and check_irrefutable_patt' ctx {loc; data = patt} vtyp = match patt with
| A.PWild -> [||]
-| A.PBind name -> [|name|]
+| A.PBind name -> [|loc @$ name|]
| A.PAnnot (patt, typ') ->
let typ' = check' ctx typ' V.Type in
let vtyp' = eval ctx.env typ' in
@@ -529,6 +549,6 @@ and check_irrefutable_patt' ctx {loc; data = patt} vtyp = match patt with
and irrefutable_patt_names {loc; data = patt} = match patt with
| A.PWild -> [||]
-| A.PBind name -> [|name|]
+| A.PBind name -> [|loc @$ name|]
| A.PAnnot (patt, _) -> irrefutable_patt_names patt
| A.PData _ -> abort (loc @$ ErrDataPattRefutable)
diff --git a/internal.ml b/internal.ml
@@ -84,8 +84,10 @@ let rec write_term buf = function
| Data (tag, args) ->
P.parens buf 6 @@ fun () ->
P.at 7 P.string buf (Tag.to_string tag);
- P.string buf " ";
- P.at 7 P.fold_left buf " " write_term args
+ begin if Array.length args > 0 then
+ P.string buf " ";
+ P.at 7 P.fold_left buf " " write_term args
+ end
| DataType ctors ->
P.parens buf 7 @@ fun () ->
P.string buf "#{";
diff --git a/lexer.mll b/lexer.mll
@@ -2,11 +2,24 @@
open Global
open Parser
-exception Error of Loc.t * string
-
-let error lexbuf msg =
+type error = error' node
+and error' =
+| ErrIndexTooBig
+| ErrInvalidNumberTerminator
+| ErrNoRule
+
+let rec string_of_error {loc; data = e} =
+ Loc.to_string loc ^ " " ^ string_of_error' e
+and string_of_error' = function
+| ErrIndexTooBig -> "name index too big"
+| ErrInvalidNumberTerminator -> "invalid terminator after integer literal"
+| ErrNoRule -> "lexical error"
+
+exception Exn of error
+
+let abort lexbuf e =
let loc = Loc.of_position (Lexing.lexeme_start_p lexbuf) in
- raise (Error (loc, msg))
+ raise (Exn {loc; data = e})
}
let dnumeral = ['0'-'9']
@@ -94,15 +107,15 @@ rule token = parse
if Z.fits_int z then
INDEXED_NAME (x, Z.to_int z)
else
- error lexbuf "name index too big"
+ abort lexbuf ErrIndexTooBig
}
| name as x { NAME x }
| number as n { NAT (Z.of_string n) }
| number invalid_number_terminator
- { error lexbuf "invalid terminator after integer literal" }
+ { abort lexbuf ErrInvalidNumberTerminator }
-| _ { error lexbuf "invalid byte" }
+| _ { abort lexbuf ErrNoRule }
{
}
diff --git a/main.ml b/main.ml
@@ -1,3 +1,4 @@
+open Global
module I = Internal
module V = Value
@@ -17,15 +18,24 @@ let buf = Lexing.from_string "T := #{@a Nat; @b #()}; @a 3 : T"
*)
let buf = Lexing.from_string "\
+ (fn => Nat) ()\
+"
+
+(*
+let buf = Lexing.from_string "\
fact: Nat -> Nat := rec fn n =>\n\
if eq n 0 then 1 else n * fact (n + 1);\n\
fact 3\n\
"
+*)
let concrete =
try Parser.start Lexer.token buf with
- | Lexer.Error (loc, msg) ->
- let () = print_endline ("[" ^ Loc.to_string loc ^ "] " ^ msg) in
+ | Lexer.Exn e ->
+ print_endline (Lexer.string_of_error e);
+ exit 1
+ | Parser.Exn e ->
+ print_endline (Parser.string_of_error e);
exit 1
let abstract = Desugar.term concrete
@@ -40,10 +50,14 @@ let ctx =
codomain = I.Builtin I.NatType;
}) in
let ctx = Ctx.empty in
- let (ctx, _) = Ctx.assign ctx [|Name.Of "Type"|] V.Type V.Type in
- let (ctx, _) = Ctx.assign ctx [|Name.Of "Nat"|] V.Type (V.Builtin I.NatType) in
- let (ctx, _) = Ctx.assign ctx [|Name.Of "`+"|] nat_op_typ (V.Builtin I.NatOpAdd) in
- let (ctx, _) = Ctx.assign ctx [|Name.Of "`*"|] nat_op_typ (V.Builtin I.NatOpMul) in
+ let (ctx, _) = Ctx.assign ctx
+ [|Loc.None @$ Name.Of "Type"|] V.Type V.Type in
+ let (ctx, _) = Ctx.assign ctx
+ [|Loc.None @$ Name.Of "Nat"|] V.Type (V.Builtin I.NatType) in
+ let (ctx, _) = Ctx.assign ctx
+ [|Loc.None @$ Name.Of "`+"|] nat_op_typ (V.Builtin I.NatOpAdd) in
+ let (ctx, _) = Ctx.assign ctx
+ [|Loc.None @$ Name.Of "`*"|] nat_op_typ (V.Builtin I.NatOpMul) in
ctx
let (internal, ty) =
diff --git a/name.ml b/name.ml
@@ -1,7 +1,11 @@
type name = Of of string
type t = name
-module Map = Map.Make(struct
+module Ord = struct
type t = name
let compare (Of x) (Of y) = String.compare x y
-end)
+end
+
+module Map = Map.Make(Ord)
+
+module Set = Set.Make(Ord)
diff --git a/parser.mly b/parser.mly
@@ -2,6 +2,25 @@
open Global
module C = Concrete
+type error = error' node
+and error' =
+| ErrInvalidTerm
+| ErrInvalidPatt
+| ErrIndexInPatt
+| ErrEmptyDomain
+
+let rec string_of_error {loc; data = e} =
+ Loc.to_string loc ^ " " ^ string_of_error' e
+and string_of_error' = function
+| ErrInvalidTerm -> "invalid term"
+| ErrInvalidPatt -> "invalid pattern"
+| ErrIndexInPatt -> "only unindexed variables can appear in patterns"
+| ErrEmptyDomain -> "empty domain"
+
+exception Exn of error
+
+let abort loc e = raise (Exn (loc @$ e))
+
(* To avoid reduce-reduce conflicts, we need to distinguish between raw
* expressions (which are generally of unknown syntactic category) and concrete
* terms/patterns/etc. In a hand-written parser, we'd have more control over
@@ -47,9 +66,6 @@ let to_array len lst =
List.iteri (Array.set arr) lst;
arr
-exception Error of Loc.t * string
-let error loc msg = raise (Error (loc, msg))
-
let rec term {loc; data = e} = loc @$ match e with
| Let (len, definers, body) -> C.Let (to_array len definers, term body)
| Seq (a, b) -> C.Seq (term a, term b)
@@ -59,8 +75,8 @@ let rec term {loc; data = e} = loc @$ match e with
| Annot (a, b) -> C.Annot (term a, term b)
| Add (a, b) -> C.Add (term a, term b)
| Mul (a, b) -> C.Mul (term a, term b)
-| Or _ -> error loc "'|' can not appear in terms (yet)"
-| And _ -> error loc "'&' can not appear in terms (yet)"
+| Or _ -> abort loc ErrInvalidTerm
+| And _ -> abort loc ErrInvalidTerm
| App (f, len, args) -> C.App (term f, Array.map term (to_array len args))
| Fn (len, params, body) -> C.Fn (to_array len params, term body)
| FnType (len, doms, cod) -> C.FnType (to_array len doms, term cod)
@@ -70,7 +86,7 @@ let rec term {loc; data = e} = loc @$ match e with
| TupleType (len, doms) -> C.TupleType (to_array len doms)
| Unit -> C.Unit
| Nat n -> C.Nat n
-| Underscore -> error loc "'_' can not appear in terms (yet)"
+| Underscore -> abort loc ErrInvalidTerm
| IndexedVar (x, i) -> C.Var (x, Some i)
| Var x -> C.Var (x, None)
| Paren e -> C.Paren (term e)
@@ -91,9 +107,9 @@ and patt {loc; data = e} = loc @$ match e with
| Paren p -> C.PParen (patt p)
| Let _ | Seq _ | Match _ | If _ | Iff _ | Add _ | Mul _
| App _ | Fn _ | FnType _ | VariantType _ | TupleType _ ->
- error loc "invalid pattern"
+ abort loc ErrInvalidPatt
| IndexedVar _ ->
- error loc "only unindexed variables can appear in patterns"
+ abort loc ErrIndexInPatt
let loc_of i = Loc.of_position (Parsing.rhs_start_pos i)
let (@$) i x = loc_of i @$ x
@@ -167,7 +183,7 @@ expr3: (* Function arrow (right-associative) *)
| LBRACK domain_list RBRACK SINGLE_ARROW expr3 {
let (len, lst) = $2 in
if len = 0 then
- error (loc_of 2) "empty domain"
+ abort (loc_of 2) ErrEmptyDomain
else
4 @$ FnType (len, lst, $5)
}
