diff options
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | src/ast/Ast.ml | 6 | ||||
| -rw-r--r-- | src/elaborator/Elaborator.ml | 31 | ||||
| -rw-r--r-- | src/parser/Grammar.mly | 4 | ||||
| -rw-r--r-- | src/pretty/Pretty.ml | 5 |
5 files changed, 32 insertions, 16 deletions
diff --git a/README.md b/README.md index ce6c1f8..40bfde5 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ not-function applied to `false` (which evaluates to `true`). - [x] build a better repl - [ ] improve error messages - [ ] implement top-level definitions -- [ ] implement less aggrevating syntax for non-dependent function & pair types +- [x] implement less aggrevating syntax for non-dependent function & pair types - [ ] add a type of natural numbers - [ ] replace type-in-type with a proper (cumulative?) hierarchy of universes -> maybe use the mugen library or figure out typical ambiguity? diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml index 1a1d4c5..3a6fac6 100644 --- a/src/ast/Ast.ml +++ b/src/ast/Ast.ml @@ -7,9 +7,11 @@ and raw_expr = | Var of Ident.t | Check of expr * expr | Pi of arg * expr + | Fun of expr * expr | Lam of local_name * expr | App of expr * expr | Sg of arg * expr + | Prod of expr * expr | Pair of expr * expr | Fst of expr | Snd of expr @@ -52,12 +54,16 @@ and dump_raw_expr fmt = function dump_expr scrut | Pi (dom, cod) -> Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod + | Fun (dom, cod) -> + Format.fprintf fmt "@[<5>Fun (@[%a@],@ @[%a@])@]" dump_expr dom dump_expr cod | Lam (var, body) -> Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_local_name var dump_expr body | App (fn, arg) -> Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg | Sg (fst, snd) -> Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd + | Prod (fst, snd) -> + Format.fprintf fmt "@[<6>Prod (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd | Pair (fst, snd) -> Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index df2a358..ba1da02 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -53,19 +53,17 @@ let quote v = NbE.quote ~size:(Eff.read()).size v (** Pretty-printing helpers *) let pp () = let names = (Eff.read()).names in fun fmt tm -> - Pretty.pp ~names fmt tm + Pretty.pp ~names fmt tm (** Main algorithm *) +type connective = [ `Pi | `Sigma ] + let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = Error.tracef ?loc:tm.loc "when checking against the type @[%a@]" (pp()) (quote tp) @@ fun () -> match tm.value with - | A.Pi ((name, base), fam) -> begin match tp with - | D.Type -> - let base = check ~tm:base ~tp in - let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in - S.Pi (name.value, base, fam) - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end + | A.Pi ((name, base), fam) -> check_connective `Pi ~name:name.value ~base ~fam ~tp + | A.Fun (base, fam) -> check_connective `Pi ~name:None ~base ~fam ~tp | A.Lam (name, body) -> begin match tp with | D.Pi (_, base, fam) -> let body = bind ~name:name.value ~tp:base @@ fun arg -> @@ -74,12 +72,8 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = S.Lam (name.value, body) | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (pp()) (quote tp) end - | A.Sg ((name, base), fam) -> begin match tp with - | D.Type -> - let base = check ~tm:base ~tp in - let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in - S.Sg (name.value, base, fam) - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end + | A.Sg ((name, base), fam) -> check_connective `Sigma ~name:name.value ~base ~fam ~tp + | A.Prod (base, fam) -> check_connective `Sigma ~name:None ~base ~fam ~tp | A.Pair (fst, snd) -> begin match tp with | D.Sg (_, base, fam) -> let fst = check ~tm:fst ~tp:base in @@ -111,6 +105,17 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = end; tm +and check_connective connective ~(name : Ident.local) ~(base : A.expr) ~(fam : A.expr) ~(tp : D.t) = + match tp with + | D.Type -> + let base = check ~tm:base ~tp in + let fam = bind ~name:name ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in + begin match connective with + | `Pi -> S.Pi (name, base, fam) + | `Sigma -> S.Sg (name, base, fam) + end + | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) + and infer (tm : A.expr) : D.t * S.t = Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> match tm.value with diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly index bb98029..d8e9ee0 100644 --- a/src/parser/Grammar.mly +++ b/src/parser/Grammar.mly @@ -47,6 +47,8 @@ raw_expr: | a = arg; ARROW; b = expr { Pi (a, b) } + | a = expr; ARROW; b = expr + { Fun (a, b) } | BACKSLASH; a = local_name; ARROW; b = expr { Lam (a, b) } | a = expr; b = expr %prec APP @@ -54,6 +56,8 @@ raw_expr: | a = arg; ASTERISK; b = expr { Sg (a, b) } + | a = expr; ASTERISK; b = expr + { Prod (a, b) } | LPR; a = expr; COMMA; b = expr; RPR { Pair (a, b) } | FST; p = expr diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml index ba78881..8b7ad1a 100644 --- a/src/pretty/Pretty.ml +++ b/src/pretty/Pretty.ml @@ -67,8 +67,9 @@ struct pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case ) fmt - and pp_arg fmt (name, tp) = - Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp + and pp_arg fmt (name, tp) = match name with + | Some name -> (delimited @@ fun fmt (name, tp) -> Fmt.pf fmt "(@[%s@] : @[%a@])" name pp tp) fmt (name, tp) + | None -> pp fmt tp (* TODO: improve indentation *) and pp fmt = function |