commit a56d4e7da22851289923593d8fb4751ec4092128
parent cc623dfe6e5bf45199824c718b939516a7b2285e
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 29 Jan 2024 04:40:57 -0800
Catch syntax errors
Diffstat:
4 files changed, 28 insertions(+), 9 deletions(-)
diff --git a/elab.ml b/elab.ml
@@ -209,7 +209,9 @@ and elaborate'
(I.Fn {multibinder = {binders = params'; order}; term = body}, vfntype)
-(*| A.Fn _, Check vtyp -> E.abort loc @@ ErrExpectedFnType vtyp*)
+| A.Fn _, Check vtyp ->
+ let typ = quote ctx.env vtyp in
+ E.abort loc @@ E.ElabExpectedFnType typ
| A.FnType {data = {multibinder = domains; term = codomain}; _}, Infer ->
let (ctx, multibinder) = infer_multibinder' ctx loc domains in
@@ -229,7 +231,9 @@ and elaborate'
| None -> E.abort loc @@ E.ElabUnexpectedTag tag
end
-(*| A.Data _, Check vtyp -> E.abort loc @@ ErrExpectedDataType vtyp*)
+| A.Data _, Check vtyp ->
+ let typ = quote ctx.env vtyp in
+ E.abort loc @@ E.ElabExpectedDataType typ
| A.DataType ctors, Infer ->
let next = ref 0 in
@@ -254,8 +258,8 @@ and elaborate'
| A.Builtin b, Infer -> (I.Builtin b, Std.infer b)
-| (A.Annot _ | A.App _ | A.Fn _ | A.FnType _ | A.Data _ | A.DataType _
- | A.Nat _ | A.Var _ | A.Builtin _) as t, Check vexpected ->
+| (A.Annot _ | A.App _ | A.FnType _ | A.DataType _ | A.Nat _
+ | A.Var _ | A.Builtin _) as t, Check vexpected ->
let (t, vinferred) = infer' ctx {loc; data = t} in
begin try unify ctx.env vexpected vinferred with
| UnifyFail ->
diff --git a/error.ml b/error.ml
@@ -12,6 +12,7 @@ and error' =
| ParserInvalidTerm
| ParserInvalidPatt
| ParserEmptyDomain
+| ParserNoRule
| DesugarDuplicateTag of Name.Tag.t
| DesugarDataAndData
@@ -20,7 +21,6 @@ and error' =
| ElabNonInferablePatt
| ElabUnifyFail of I.term * I.term
| ElabUnexpectedTag of Name.Tag.t
-| ElabExpectedDataType of I.term
| ElabNoLetAnnot of error
| ElabBinderCycle of Name.Var.t list
| ElabUnannotImplicitIsType of error
@@ -35,7 +35,8 @@ and error' =
| ElabNonExhaustiveMatch
| ElabRedundantCase
| ElabCantInferMatch
-(*| ElabExpectedFnType of I.term*)
+| ElabExpectedFnType of I.term
+| ElabExpectedDataType of I.term
let rec pp_print ppf {loc; data = e} =
F.fprintf ppf "@[<v>[%a] %a@]"
@@ -56,6 +57,8 @@ and pp_print' ppf = function
F.pp_print_string ppf "invalid pattern"
| ParserEmptyDomain ->
F.pp_print_string ppf "empty domain"
+| ParserNoRule ->
+ F.pp_print_string ppf "syntax error"
| DesugarDuplicateTag tag ->
F.fprintf ppf "%s: %a"
@@ -90,7 +93,6 @@ and pp_print' ppf = function
| ElabBinderCycle _ -> F.pp_print_string ppf "ErrBinderCycle"
| ElabArityMismatch -> F.pp_print_string ppf "ErrArityMismatch"
| ElabUnboundVar _ -> F.pp_print_string ppf "ErrUnboundVar"
-| ElabExpectedDataType _ -> F.pp_print_string ppf "ErrExpectedDataType"
| ElabFnArityMismatch -> F.pp_print_string ppf "ErrFnArityMismatch"
| ElabFnPlicityMismatch -> F.pp_print_string ppf "ErrFnPlicityMismatch"
| ElabUnexpectedTag _ -> F.pp_print_string ppf "ErrUnexpectedTag"
@@ -98,8 +100,11 @@ and pp_print' ppf = function
| ElabNonExhaustiveMatch -> F.pp_print_string ppf "ElabNonExhaustiveMatch"
| ElabRedundantCase -> F.pp_print_string ppf "ElabRedundantCase"
| ElabCantInferMatch -> F.pp_print_string ppf "ElabCantInferMatch"
-(*| ElabExpectedFnType _ -> "ErrExpectedFnType"*)
+| ElabExpectedFnType _ -> F.pp_print_string ppf "ErrExpectedFnType"
+| ElabExpectedDataType _ -> F.pp_print_string ppf "ErrExpectedDataType"
exception Exn of error
-let abort loc e = raise (Exn (loc @$ e))
+let abort
+: 'a. Loc.t -> error' -> 'a
+= fun loc e -> raise (Exn (loc @$ e))
diff --git a/main.ml b/main.ml
@@ -3,6 +3,7 @@ module B = Builtin
module I = Internal
module V = Value
+(*
let buf = Lexing.from_string "\
\\comment :)\n\
N := [A: Type, A, A -> A] -> A;\n\
@@ -12,6 +13,7 @@ let buf = Lexing.from_string "\
`f i v e` := add two three;\n\
`f i v e` Nat 0 (fn n => n + 1)\n\
"
+*)
(*
let buf = Lexing.from_string "\
@@ -68,6 +70,13 @@ let buf = Lexing.from_string "\
"
*)
+let buf = Lexing.from_string "\
+ Opt := fn A: Type => #{@some A; @none};\n\
+ div: [Nat, Nat] -> Opt Nat := fn m, n =>\n\
+ if n = 0 then @none else @some (m / n);\n\
+ (div 3 0, div 12 3): #(Opt Nat, Opt Nat)\n\
+"
+
let ctx =
let ctx = ref Ctx.empty in
let assign s t v =
diff --git a/parser.mly b/parser.mly
@@ -138,6 +138,7 @@ let loc () =
* x < y && y < z. *)
start: expr0 EOF { term $1 }
+ | error { E.abort (loc_of 1) @@ E.ParserNoRule }
expr0: (* Definitions and sequencing *)
| definer_list SEMICOLON expr0 {
