Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Septembre 2016
- 5 participants
- 30 discussions
Est-ce que le bug pourrait venir de la fonction `env_lookup_type` ?
let env_lookup_type ctx (v : vref): lexp =
let (_, idx) = v in
let (r, _, _, ltp) = _env_lookup ctx v in
(L.push_susp ltp (S.shift (idx - 0 + 0)))
J'ai essayé plusieurs indices et j'ai repéré quelque chose d'étrange
lorsque je fais un shift de idx, j’obtiens Macro[20]
mais lorsque je fais un shift de idx + 1 j’obtiens Macro[22].
Voici une liste de tests qui montre le comportement du shift.
Shift: idx
macro_type=inductive_ (Macro) (Macro_ (List[33] Sexp[47]) -> Sexp[47])
ltp=Macro[20] (= inductive-cons Macro[21] Macro_)
Shift: idx + 1
macro_type=inductive_ (Macro) (Macro_ (List[33] Sexp[47]) -> Sexp[47])
ltp=Macro[22] (= float_)
Shift: idx + 2
macro_type=inductive_ (Macro) (Macro_ (List[33] Sexp[47]) -> Sexp[47])
ltp=Macro[24] (= node_)
Shift: idx - 1
macro_type=inductive_ (Macro) (Macro_ (List[33] Sexp[47]) -> Sexp[47])
ltp=Macro[18] (= sexp_dispatch_)
--
Pierre Delaunay
3
5
[Git][monnier/typer][master] * src/lparse.ml (_lexp_rec_decl): Call lexp_p_infer with complete context
by Stefan 29 Sep '16
by Stefan 29 Sep '16
29 Sep '16
Stefan pushed to branch master at Stefan / Typer
Commits:
8458627d by Stefan Monnier at 2016-09-29T10:51:32-04:00
* src/lparse.ml (_lexp_rec_decl): Call lexp_p_infer with complete context
This fixes an assertion failure in "EVAL - Mutually Recursive Definition".
- - - - -
2 changed files:
- src/debruijn.ml
- src/lparse.ml
Changes:
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -109,9 +109,9 @@ let rec senv_lookup (name: string) (ctx: elab_context): int =
raw_idx
let lexp_ctx_cons (ctx : lexp_context) offset d v t =
- assert (offset >= 0 &&
- (ctx = M.nil ||
- let (previous_offset, _, _, _) = M.car ctx in
+ assert (offset >= 0
+ && (ctx = M.nil
+ || let (previous_offset, _, _, _) = M.car ctx in
previous_offset >= 0 && previous_offset <= 1 + offset));
M.cons (offset, d, v, t) ctx
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -808,9 +808,7 @@ and _lexp_rec_decl decls ctx i =
* i.e let decl parsing *)
(* to compute recursive offset *)
- let n = (List.length decls) in
let lst = ref [] in
- (* print_int n; print_string "\n"; *)
(* add all elements to the environment *)
let tctx = List.fold_left (fun vctx decl ->
@@ -826,23 +824,23 @@ and _lexp_rec_decl decls ctx i =
lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in
(* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *)
- let i = ref 0 in
+ let i = ref (1 + List.length decls) in
let ctx = List.fold_left (fun vctx decl ->
- i := !i + 1;
+ i := !i - 1;
match decl with
(* +1 because we allow each definition to be recursive *)
(* lexp infer *)
| Ldecl ((l, s), Some pxp, None) ->
let lxp, ltp = lexp_p_infer pxp tctx in
lst := ((l, s), lxp, ltp)::!lst;
- (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)
+ (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp)
(* lexp check *)
| Ldecl ((l, s), Some pxp, Some ptp) ->
- let ltp, _ = lexp_p_infer ptp vctx in
+ let ltp, _ = lexp_p_infer ptp tctx in
let lxp = lexp_p_check pxp ltp tctx in
lst := ((l, s), lxp, ltp)::!lst;
- (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)
+ (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp)
(* macros *)
| Lmcall (a, sargs) ->
View it on GitLab: https://gitlab.com/monnier/typer/commit/8458627dcbd32d188256633bfe9220972b2…
1
0
[Git][monnier/typer][master] * src/lparse.ml (_lexp_p_infer) <Parrow>: Also add anon vars to lctx
by Stefan 29 Sep '16
by Stefan 29 Sep '16
29 Sep '16
Stefan pushed to branch master at Stefan / Typer
Commits:
f49911fd by Stefan Monnier at 2016-09-29T00:41:49-04:00
* src/lparse.ml (_lexp_p_infer) <Parrow>: Also add anon vars to lctx
* src/debruijn.ml (ectx_extend_anon): New function.
* src/lparse.ml (_type_shift): Remove function.
(_lexp_p_infer) <Parrow>: Also add anonymous vars to lctx.
- - - - -
2 changed files:
- src/debruijn.ml
- src/lparse.ml
Changes:
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -118,6 +118,9 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t =
let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) =
lexp_ctx_cons ctx 0 (Some def) v t
+let ectx_extend_anon (ectx: elab_context) (t: lexp) : elab_context =
+ let ((n, map), lctx, f) = ectx in
+ ((n + 1, map), lexp_ctx_cons lctx 0 None Variable t, f)
let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
let (loc, name) = def in
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -75,14 +75,6 @@ type mdecl =
| Ldecl of symbol * pexp option * pexp option
| Lmcall of symbol * sexp list
-(* This is used to make Type annotation and inferred type having the same index *)
-(* since inferred type might need to parse a lambda var to infer the type *)
-
-let _type_shift tp i =
- match tp with
- | Var(v, idx) -> Var(v, idx)
- | expr -> expr
-
let ctx_define (ctx: elab_context) var lxp ltype =
let (_, cctx, _) = ctx in
if OL.conv_p ltype (OL.check cctx lxp) then
@@ -184,12 +176,11 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
(* ------------------------------------------------------------------ *)
| Parrow (kind, ovar, tp, loc, expr) ->
let ltp, _ = lexp_infer tp ctx in
- let nctx, sh = match ovar with
- | None -> ctx, 0
- | Some var -> (env_extend ctx var Variable ltp), 1 in
+ let nctx = match ovar with
+ | None -> ectx_extend_anon ctx ltp
+ | Some var -> env_extend ctx var Variable ltp in
let lxp, _ = lexp_infer expr nctx in
- let lxp = _type_shift lxp sh in
let v = Arrow(kind, ovar, ltp, tloc, lxp) in
v, type0
@@ -225,8 +216,6 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
let nctx = env_extend ctx var Variable ltp in
let lbody, lbtp = lexp_infer body nctx in
- (* We added one variable in the ctx
- let lbtp = _type_shift lbtp 1 in *)
let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in
Lambda(kind, var, ltp, lbody), lambda_type
@@ -350,18 +339,16 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =
(* make a list of all branches return type *)
let texp = ref [] in
- let ctx_len = get_size ctx in
(* Read patterns one by one *)
let fold_fun (merged, dflt) (pat, exp) =
(* Create pattern context *)
let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in
- let nctx_len = get_size nctx in
(* parse using pattern context *)
let exp, ltp = lexp_infer exp nctx in
(* we added len(arg) variable int the context *)
- texp := (_type_shift ltp (nctx_len - ctx_len))::!texp;
+ texp := ltp::!texp;
(* Check ltp type. Must be similar to rtype *)
(if type_check ltp then ()
@@ -569,6 +556,8 @@ and lexp_read_pattern pattern exp target ctx:
("`" ^ lexp_to_str (it)
^ "` is not an inductive type!") in
+ (* FIXME: Don't remove them, add them without names! *)
+ (* FIXME: Add support for explicit-implicit fields! *)
(* Remove non explicit argument. *)
let rec remove_nexplicit args acc =
match args with
View it on GitLab: https://gitlab.com/monnier/typer/commit/f49911fd102c1e9b11b43a743e5da2e44ba…
1
0
[Git][monnier/typer][master] * src/opslexp.ml (lookup_type, lookup_value): Move to debruijn.ml
by Stefan 29 Sep '16
by Stefan 29 Sep '16
29 Sep '16
Stefan pushed to branch master at Stefan / Typer
Commits:
9bb74c93 by Stefan Monnier at 2016-09-29T00:10:31-04:00
* src/opslexp.ml (lookup_type, lookup_value): Move to debruijn.ml
* src/debruijn.ml (_get_env): Remove functions.
(env_lookup_by_index, print_lexp_ctx): Change ctx type.
(lctx_lookup): Rename from _env_lookup; change ctx type.
(lctx_lookup_type, lctx_lookup_value): Move from opslexp.ml; use
lctx_lookup.
(env_lookup_type, env_lookup_expr): Use them.
- - - - -
5 changed files:
- src/REPL.ml
- src/debruijn.ml
- src/debug_util.ml
- src/lparse.ml
- src/opslexp.ml
Changes:
=====================================
src/REPL.ml
=====================================
--- a/src/REPL.ml
+++ b/src/REPL.ml
@@ -216,7 +216,7 @@ let rec repl i clxp rctx =
| "%quit" | "%q" -> ()
| "%help" | "%h" -> (print_string _help_msg; repl clxp rctx)
| "%who" | "%w" -> (print_rte_ctx rctx; repl clxp rctx)
- | "%info" | "%i" -> (print_lexp_ctx clxp; repl clxp rctx)
+ | "%info" | "%i" -> (print_lexp_ctx (ectx_to_lctx clxp); repl clxp rctx)
| "%calltrace" | "%ct" -> (print_eval_trace (); repl clxp rctx)
(* command with arguments *)
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -89,7 +89,6 @@ let ectx_to_lctx (ectx : elab_context) : lexp_context =
let _make_scope = StringMap.empty
let _make_senv_type = (0, _make_scope)
let _make_myers = M.nil
-let _get_env(ctx: elab_context): lexp_context = let (_, ev, _) = ctx in ev
(* Public methods: DO USE
* ---------------------------------- *)
@@ -158,12 +157,12 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) =
recursion_offset - 1)
(ctx, List.length defs) defs
-let env_lookup_by_index index (ctx: elab_context): env_elem =
- (Myers.nth index (_get_env ctx))
+let env_lookup_by_index index (ctx: lexp_context): env_elem =
+ Myers.nth index ctx
(* Print context *)
-let print_lexp_ctx (ctx : elab_context) =
- let ((n, map), env, f) = ctx in
+let print_lexp_ctx (ctx : lexp_context) =
+ let n = M.length ctx in
print_string (make_title " LEXP CONTEXT ");
@@ -187,15 +186,12 @@ let print_lexp_ctx (ctx : elab_context) =
| _ -> "" in
extract_names tl (name::acc) in
- let ord = extract_names env [] in
+ let ord = extract_names ctx [] in
let rec _print idx ord =
match ord with
| [] -> ()
| hd::tl ->(
- let idx2 = StringMap.find hd map in
-
- (if idx2 != idx then ());
print_string " | "; lalign_print_string hd 10;
print_string " | "; lalign_print_int (n - idx - 1) 7;
@@ -243,11 +239,10 @@ let _name_error loc estr str ctx =
(* generic lookup *)
-let _env_lookup ctx (v: vref): env_elem =
- let ((dv_size, _), info_env, _) = ctx in
+let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
let ((loc, ename), dbi) = v in
- try(let ret = (Myers.nth dbi info_env) in
+ try(let ret = (Myers.nth dbi ctx) in
let _ = match ret with
| (_, Some (_, name), _, _) ->
(* Check if names match *)
@@ -259,17 +254,23 @@ let _env_lookup ctx (v: vref): env_elem =
Not_found -> debruijn_error loc "DeBruijn index out of bounds!"
+
+let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp =
+ let (_, i) = vref in
+ let (_, _, _, t) = lctx_lookup ctx vref in
+ mkSusp t (S.shift (i + 1))
+
+let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option =
+ let (_, i) = vref in
+ match lctx_lookup ctx vref with
+ | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o)))
+ | _ -> None
+
let env_lookup_type ctx (v : vref): lexp =
- let (_, idx) = v in
- let (_, _, _, ltp) = _env_lookup ctx v in
- mkSusp ltp (S.shift (idx + 0))
+ lctx_lookup_type (ectx_to_lctx ctx) v
let env_lookup_expr ctx (v : vref): lexp option =
- let (_, idx) = v in
- let (r, _, lxp, _) = _env_lookup ctx v in
- match lxp with
- | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r)))
- | _ -> None
+ lctx_lookup_value (ectx_to_lctx ctx) v
(* replace an expression by another *)
(* Most of the time it should be O(1) but it can be O(n) *)
=====================================
src/debug_util.ml
=====================================
--- a/src/debug_util.ml
+++ b/src/debug_util.ml
@@ -345,7 +345,7 @@ let main () =
debug_lexp_decls flexps; print_string "\n"));
(if (get_p_option "lctx") then(
- print_lexp_ctx nctx; print_string "\n"));
+ print_lexp_ctx (ectx_to_lctx nctx); print_string "\n"));
let clean_lxp = List.map OL.clean_decls lexps in
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -433,7 +433,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
"Expected non-explicit arg"
| t ->
lexp_print t; print_string "\n";
- print_lexp_ctx ctx;
+ print_lexp_ctx (ectx_to_lctx ctx);
lexp_fatal (sexp_location sarg)
"Explicit arg to non-function") in
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -45,16 +45,8 @@ let impredicative_erase = true (* Allows erasable args to be impredicative. *)
(* Lexp context *)
-let lookup_type (ctx : DB.lexp_context) vref =
- let (_, i) = vref in
- let (_, _, _, t) = Myers.nth i ctx in
- mkSusp t (S.shift (i + 1))
-
-let lookup_value (ctx : DB.lexp_context) vref =
- let (_, i) = vref in
- match Myers.nth i ctx with
- | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o)))
- | _ -> None
+let lookup_type = DB.lctx_lookup_type
+let lookup_value = DB.lctx_lookup_value
(********* Testing if two types are "convertible" aka "equivalent" *********)
View it on GitLab: https://gitlab.com/monnier/typer/commit/9bb74c93c894824a65e35b03f5cea2ef5d5…
1
0
[Git][monnier/typer][unification] 7 commits: Merge branch 'master' of gitlab.com:monnier/typer
by Stefan 26 Sep '16
by Stefan 26 Sep '16
26 Sep '16
Stefan pushed to branch unification at Stefan / Typer
Commits:
e314669e by Pierre Delaunay at 2016-09-25T13:39:35-04:00
Merge branch 'master' of gitlab.com:monnier/typer
- - - - -
f83ee0b4 by Pierre Delaunay at 2016-09-26T12:05:47-04:00
Merge branch 'master' of github.com:Delaunay/typer
- - - - -
12a677ab by Pierre Delaunay at 2016-09-26T19:27:11-04:00
Try to fix our Macro_ index problem. Nevertheless, it does not work
as a lot of index are not computed correctly anymore
* Moved (print_lexp_ctx) from lparse.ml to debruijn.ml to help debugging
* src/lparse.ml: types and expression are processed in a different context
- - - - -
db617a20 by Pierre Delaunay at 2016-09-26T19:54:32-04:00
Merge with master. Indices seem to be correct.
Nevertheles, Macro are still not recognized as such
(back to the original issue)
- - - - -
e938c998 by Stefan Monnier at 2016-09-26T20:29:14-04:00
Make type levels more canonical
* src/lexp.ml (sort_level): Replace SLn with SLz.
(lexp_location, _lexp_to_str): Adjust accordingly.
* src/opslexp.ml (sort_level_max): New function.
(sort_compose): Use it.
(impredicative_erase): New var.
(check): Adjust for new SLz. Obey impredicative_erase.
Fix level calculation for inductive types.
* src/builtin.ml (type0, type1, type2): Adjust.
- - - - -
5949b172 by Stefan Monnier at 2016-09-26T20:29:53-04:00
Missing changes in last commit
- - - - -
6d7b4793 by Stefan Monnier at 2016-09-26T20:34:16-04:00
Merge branch 'trunk' into unification
- - - - -
10 changed files:
- btl/types.typer
- samples/nat.typer
- src/builtin.ml
- src/debruijn.ml
- src/fmt_lexp.ml
- src/lexp.ml
- src/lparse.ml
- src/opslexp.ml
- src/unification.ml
- tests/eval_test.ml
Changes:
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -66,7 +66,7 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool);
% -----------------------------------------------------
List : Type -> Type;
-List = inductive_ (dList (a : Type)) (nil) (cons a (List a));
+List = inductive_ (List (a : Type)) (nil) (cons a (List a));
nil = inductive-cons List nil;
cons = inductive-cons List cons;
@@ -76,7 +76,7 @@ length = lambda a ≡>
lambda xs ->
case xs
| nil => 0
- | cons hd tl => (1 + (length(a := a) tl));
+ | cons hd tl => (1 + (length (a := a) tl));
head : (a : Type) ≡> List a -> a;
head = lambda a ≡>
@@ -92,6 +92,7 @@ tail = lambda a ≡>
| nil => nil
| cons hd tl => tl;
+
% -----------------------------------------------------
% Macro
% -----------------------------------------------------
@@ -103,8 +104,8 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp);
integer_ = Built-in "integer_" (Int -> Sexp);
float_ = Built-in "float_" (Float -> Sexp);
-% Macro : Type;
-Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp));
+Macro : Type;
+Macro = inductive_ (Macro) (Macro_ (List Sexp -> Sexp));
Macro_ = inductive-cons Macro Macro_ ;
expand_macro_ : Macro -> List Sexp -> Sexp;
@@ -187,3 +188,6 @@ declexpr = Built-in "declexpr" Macro;
+
+
+
=====================================
samples/nat.typer
=====================================
--- a/samples/nat.typer
+++ b/samples/nat.typer
@@ -5,39 +5,31 @@ zero = inductive-cons Nat zero;
succ = inductive-cons Nat succ;
to-num : Nat -> Int;
-to-num = lambda (x : Nat) ->
- case x
- | (succ y) => (1 + (to-num y))
- | zero => 0;
-
-one = (succ zero);
-two = (succ one);
-three = (succ two);
+to-num = lambda (x : Nat) -> case x
+ | (succ y) => (1 + (to-num y))
+ | zero => 0;
plus : Nat -> Nat -> Nat;
-plus = lambda (x : Nat) ->
- lambda (y : Nat) ->
- case x
- | zero => y
- | succ z => succ (plus z y);
+plus = lambda (x : Nat) -> lambda (y : Nat) -> case x
+ | zero => y
+ | succ z => succ (plus z y);
+one = succ zero;
+two = succ one;
+three = succ two;
-odd : Nat -> Int;
even : Nat -> Int;
+odd : Nat -> Int;
odd = lambda (n : Nat) -> case n
- | zero => 0
- | succ y => (even y);
+ | zero => 0
+ | succ y => (even y);
even = lambda (n : Nat) -> case n
- | zero => 1
- | succ y => (odd y);
-
-%n1 = (to-num zero);
-%n2 = (to-num one);
-%n3 = (to-num two);
+ | zero => 1
+ | succ y => (odd y);
-%m1 = (to-num (plus zero two)); % 2
-%m2 = (to-num (plus two zero)); % 2
-%m3 = (to-num (plus two one)); % 3
-o1 = (even two);
\ No newline at end of file
+a = odd one;
+b = even one;
+c = odd two;
+d = even two;
\ No newline at end of file
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -75,7 +75,7 @@ let get_predef_raw (name: string) : lexp =
| None -> builtin_error dloc ("\""^ name ^ "\" was not predefined")
let get_predef_option (name: string) ctx =
- let r = (get_size ctx) - !builtin_size - 1 in
+ let r = (get_size ctx) - !builtin_size - 0 in
match !(SMap.find name (!predef_map)) with
| Some exp -> Some (mkSusp exp (S.shift r))
| None -> None
@@ -98,9 +98,12 @@ let dump_predef () =
(* Builtin types *)
let dloc = dummy_location
-let type0 = Sort (dloc, Stype (SortLevel (SLn 0)))
-let type1 = Sort (dloc, Stype (SortLevel (SLn 1)))
-let type2 = Sort (dloc, Stype (SortLevel (SLn 2)))
+let level0 = SortLevel SLz
+let level1 = SortLevel (SLsucc level0)
+let level2 = SortLevel (SLsucc level1)
+let type0 = Sort (dloc, Stype level0)
+let type1 = Sort (dloc, Stype level1)
+let type2 = Sort (dloc, Stype level2)
let type_omega = Sort (dloc, StypeOmega)
let type_level = Sort (dloc, StypeLevel)
@@ -343,7 +346,7 @@ let declexpr_impl loc largs ctx ftype =
let lxp = match env_lookup_expr ctx ((loc, vn), vi) with
| Some lxp -> lxp
| None -> builtin_error loc "no expr available" in
- let ltp = env_lookup_type ctx ((loc, vn), vi) in
+ let ltp = env_lookup_type ctx ((loc, vn), vi) in (* FIXME: Unused? *)
lxp, ftype
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -46,6 +46,9 @@ let debruijn_warning = msg_warning "DEBRUIJN"
(* Type definitions
* ---------------------------------- *)
+let dloc = dummy_location
+let type0 = Sort (dloc, Stype (SortLevel SLz))
+let dltype = type0
type property_key = (int * string) (* rev_dbi * Var name *)
module PropertyMap
@@ -116,7 +119,8 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t =
let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) =
lexp_ctx_cons ctx 0 (Some def) v t
-let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
+
+let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
let (loc, name) = def in
let ((n, map), env, f) = ctx in
(try let _ = senv_lookup name ctx in
@@ -124,9 +128,11 @@ let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
with Not_found -> ());
let nmap = StringMap.add name n map in
((n + 1, nmap),
- lexp_ctx_cons env 0 (Some def) v t,
+ lexp_ctx_cons env r (Some def) v t,
f)
+let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t
+
let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) =
let (ctx, _) =
List.fold_left
@@ -152,10 +158,88 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) =
recursion_offset - 1)
(ctx, List.length defs) defs
-let _name_error loc estr str =
- if estr = str then () else
+let env_lookup_by_index index (ctx: elab_context): env_elem =
+ (Myers.nth index (_get_env ctx))
+
+(* Print context *)
+let print_lexp_ctx (ctx : elab_context) =
+ let ((n, map), env, f) = ctx in
+
+ print_string (make_title " LEXP CONTEXT ");
+
+ make_rheader [
+ (Some ('l', 10), "NAME");
+ (Some ('l', 7), "INDEX");
+ (Some ('l', 10), "NAME");
+ (Some ('l', 4), "OFF");
+ (Some ('l', 29), "VALUE:TYPE")];
+
+ print_string (make_sep '-');
+
+ (* it is annoying to print according to StringMap order *)
+ (* let's use myers list order *)
+ let rec extract_names (lst: lexp_context) acc =
+ match lst with
+ | M.Mnil -> acc
+ | M.Mcons (hd, tl, _, _) ->
+ let name = match hd with
+ | (_, Some (_, name), _, _) -> name
+ | _ -> "" in
+ extract_names tl (name::acc) in
+
+ let ord = extract_names env [] in
+
+ let rec _print idx ord =
+ match ord with
+ | [] -> ()
+ | hd::tl ->(
+ let idx2 = StringMap.find hd map in
+
+ (if idx2 != idx then ());
+
+ print_string " | "; lalign_print_string hd 10;
+ print_string " | "; lalign_print_int (n - idx - 1) 7;
+ print_string " | ";
+
+ let ptr_str = "" in (*" | | | | " in *)
+
+ try let r, name, exp, tp =
+ match env_lookup_by_index (n - idx - 1) ctx with
+ | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp
+ | _ -> 0, "", None, dltype in
+
+ (* Print env Info *)
+ lalign_print_string name 10; (* name must match *)
+ print_string " | ";
+ lalign_print_int r 4;
+ print_string " | ";
+
+ let _ = (match exp with
+ | None -> print_string "<var>"
+ | Some exp -> lexp_print exp)
+ (* let str = _lexp_to_str (!debug_ppctx) exp in
+ let str = (match str_split str '\n' with
+ | hd::tl -> print_string (hd ^ "\n"); tl
+ | _ -> []) in
+
+ List.iter (fun elem ->
+ print_string (ptr_str ^ elem ^ "\n")) str) *)in
+
+ print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n";
+
+ _print (idx + 1) tl
+
+ with Not_found ->
+ (print_string "Not_found |\n"; _print (idx + 1) tl)) in
+
+ _print 0 ord; print_string (make_sep '=')
+
+
+let _name_error loc estr str ctx =
+ if estr = str then () else (
+ print_lexp_ctx ctx;
debruijn_error loc ("DeBruijn index refers to wrong name. " ^
- "Expected: \"" ^ estr ^ "\" got \"" ^ str ^ "\"")
+ "Expected: \"" ^ estr ^ "\" got \"" ^ str ^ "\""))
(* generic lookup *)
@@ -167,7 +251,7 @@ let _env_lookup ctx (v: vref): env_elem =
let _ = match ret with
| (_, Some (_, name), _, _) ->
(* Check if names match *)
- _name_error loc ename name;
+ _name_error loc ename name ctx;
| _ -> () in
ret)
@@ -187,9 +271,6 @@ let env_lookup_expr ctx (v : vref): lexp option =
| LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r)))
| _ -> None
-let env_lookup_by_index index (ctx: elab_context): env_elem =
- (Myers.nth index (_get_env ctx))
-
(* replace an expression by another *)
(* Most of the time it should be O(1) but it can be O(n) *)
let replace_by ctx name by =
=====================================
src/fmt_lexp.ml
=====================================
--- a/src/fmt_lexp.ml
+++ b/src/fmt_lexp.ml
@@ -63,8 +63,8 @@ and string_of_kind = function
and string_of_sort_level lvl =
match lvl with
- | L.SLn i -> "SLn(" ^ string_of_int i ^ ")"
- | L.SLsucc l -> "SLsucc(" ^ string_of_lxp l^ ")"
+ | L.SLz -> "SLz"
+ | L.SLsucc l -> "SLsucc(" ^ string_of_lxp l ^ ")"
and string_of_sort sort =
match sort with
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -81,13 +81,24 @@ type ltype = lexp
* * unification. *\)
* | MetaFoF
* and subst = lexp VMap.t *)
+ (*
+ * The PTS I'm imagining looks like:
+ *
+ * S = { TypeLevel, TypeOmega, Type ℓ }
+ * A = { Level : TypeLevel, Z : Level, S : Level → Level,
+ * Type : (ℓ : Level) → Type (S ℓ) }
+ * R = { (TypeLevel, Type ℓ, TypeOmega),
+ * (TypeLevel, TypeOmega, TypeOmega),
+ * (Type ℓ, TypeOmega, TypeOmega),
+ * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) }
+ *)
and sort =
| Stype of lexp
| StypeOmega
| StypeLevel
and sort_level =
- | SLn of int
- | SLsucc of lexp
+ | SLz
+ | SLsucc of lexp
type varbind =
@@ -253,7 +264,7 @@ let rec lexp_location e =
match e with
| Sort (l,_) -> l
| SortLevel (SLsucc e) -> lexp_location e
- | SortLevel (SLn _) -> U.dummy_location
+ | SortLevel SLz -> U.dummy_location
| Imm s -> sexp_location s
| Var ((l,_),_) -> l
| Builtin ((l, _), _) -> l
@@ -778,7 +789,7 @@ and _lexp_to_str ctx exp =
| Builtin ((_, name), _) -> name
| Sort (_, Stype lvl) -> (match lvl with
- | SortLevel (SLn v) -> "Type_" ^ (string_of_int v)
+ | SortLevel SLz -> "Type_0"
| _ -> "Type_?")
| _ -> print_string "Printing Not Implemented\n"; "-- --"
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -176,14 +176,15 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
(* Symbol i.e identifier *)
| Pvar (loc, name) ->(
- try let idx = (senv_lookup name ctx) in
+ try
+ let idx = (senv_lookup name ctx) in
let lxp = (make_var name idx loc) in
(* search type *)
let ltp = env_lookup_type ctx ((loc, name), idx) in
lxp, ltp
- with Not_found ->
+ with e ->
(lexp_error loc ("The variable: \"" ^ name ^ "\" was not declared");
(* Error recovery. The -1 index will raise an error later on *)
(make_var name (-1) loc), dltype))
@@ -441,7 +442,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
* Constructor : a constructor is returned
* Anonymous : lambda *)
- (* retrieve function's body *)
+ (* retrieve function's body (sqr 3) sqr is a Pvar() *)
let body, ltp = _lexp_p_infer func ctx (i + 1) in
let ltp = nosusp ltp in
@@ -481,12 +482,11 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
sexp_print sarg; print_string "\n";
lexp_fatal (sexp_location sarg)
"Expected non-explicit arg"
- | e -> Debug_fun.do_debug (fun () ->
- print_endline ("<>explicit arg : " ^ Fmt_lexp.string_of_lxp ltp);
- print_endline ("<>explicit res : " ^ Fmt_lexp.string_of_lxp e);
- ());
- lexp_fatal (sexp_location sarg)
- "Explicit arg to non-function") in
+ | t ->
+ lexp_print t; print_string "\n";
+ print_lexp_ctx ctx;
+ lexp_fatal (sexp_location sarg)
+ "Explicit arg to non-function") in
let handle_funcall () =
(* Here we use lexp_whnf on actual code, but it's OK
@@ -551,32 +551,32 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
_lexp_p_infer pxp ctx (i + 1) in
(* This is the builtin Macro type *)
- let macro_type = match get_predef_option "Macro" ctx with
- | Some lxp -> lxp
- (* When type.typer is being parsed and the predef is not yet
- * available *)
- | None -> dltype in
+ let macro_type, macro_disp = match get_predef_option "Macro" ctx with
+ | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true
+ (* When type.typer is being parsed and the predef is not yet available *)
+ | None -> dltype, false in
+
+ (*print_string "\nmacro_type="; lexp_print macro_type;
+ print_string "\nltp="; lexp_print ltp;
+ print_string " (= "; lexp_print (OL.lexp_whnf ltp (ectx_to_lctx ctx)); print_string ")\n"; *)
(* determine function type *)
match func, ltp with
- (* This is a work around for the bug described below *)
| Pvar(l, name), _ when is_builtin_macro name ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- (get_macro_impl loc name) loc largs ctx ltp
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ (get_macro_impl loc name) loc largs ctx ltp
- (* FIXME: the branch 'builtin macro' is never used because of missing shift somewhere *)
- (* while special forms have a type macro this does not recognize them as such *)
- | macro, _ when OL.conv_p ltp macro_type -> (
+ | macro, _ when (macro_disp && (OL.conv_p ltp macro_type))-> (
match macro with
| Pvar(l, name) when is_builtin_macro name ->
- print_string name;
let pargs = List.map pexp_parse sargs in
let largs = _lexp_parse_all pargs ctx i in
(get_macro_impl loc name) loc largs ctx ltp
(* true macro *)
- | _ -> handle_macro_call ())
+ | _ ->
+ handle_macro_call ())
(* FIXME: Handle special-forms here as well! *)
| _ -> handle_funcall ()
@@ -628,17 +628,21 @@ and lexp_read_pattern pattern exp target ctx:
^ "` is not an inductive type!") in
(* Remove non explicit argument. *)
- let rec remove_nexplicit args acc =
- match args with
- | [] -> List.rev acc
- | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc)
- | hd::tl -> remove_nexplicit tl acc in
-
- let cons_args = remove_nexplicit cons_args [] in
-
- (* read pattern args *)
- let args, nctx = lexp_read_pattern_args args cons_args ctx in
- (cons_name, loc, args), nctx
+ let rec remove_nexplicit args acc =
+ match args with
+ | [] -> List.rev acc
+ | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc)
+ | hd::tl -> remove_nexplicit tl acc in
+
+ let cons_args = remove_nexplicit cons_args [] in
+
+ (* read pattern args *)
+ let args, nctx = lexp_read_pattern_args args cons_args ctx in
+ (cons_name, loc, args), nctx
+ | _ -> lexp_warning (pexp_location ctor)
+ ("Invalid constructor `"
+ ^ (pexp_to_string ctor) ^ "`");
+ ("_", pexp_location ctor, []), ctx
(* Read patterns inside a constructor *)
and lexp_read_pattern_args args (args_type : lexp list) ctx:
@@ -873,8 +877,9 @@ and _lexp_rec_decl decls ctx i =
* i.e let decl parsing *)
(* to compute recursive offset *)
- let n = (List.length decls) + 1 in
+ let n = (List.length decls) in
let lst = ref [] in
+ (* print_int n; print_string "\n"; *)
(* add all elements to the environment *)
let tctx = List.fold_left (fun vctx decl ->
@@ -883,29 +888,30 @@ and _lexp_rec_decl decls ctx i =
env_extend vctx (l, s) ForwardRef dltype
| Ldecl((l, s), _, Some ptp) ->
- let lxp, _ = lexp_p_infer ptp vctx in
- env_extend vctx (l, s) ForwardRef lxp
+ let ltp, _ = lexp_p_infer ptp vctx in
+ env_extend vctx (l, s) ForwardRef ltp
| Lmcall _ ->
lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in
+ (* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *)
let i = ref 0 in
let ctx = List.fold_left (fun vctx decl ->
i := !i + 1;
match decl with
+ (* +1 because we allow each definition to be recursive *)
(* lexp infer *)
| Ldecl ((l, s), Some pxp, None) ->
- let lxp, ltp = lexp_p_infer pxp vctx in
+ let lxp, ltp = lexp_p_infer pxp tctx in
lst := ((l, s), lxp, ltp)::!lst;
- (* replace forward ref by its true value *)
- replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp)
+ (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)
(* lexp check *)
| Ldecl ((l, s), Some pxp, Some ptp) ->
let ltp, _ = lexp_p_infer ptp vctx in
- let lxp = lexp_p_check pxp ltp vctx in
+ let lxp = lexp_p_check pxp ltp tctx in
lst := ((l, s), lxp, ltp)::!lst;
- replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp)
+ (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)
(* macros *)
| Lmcall (a, sargs) ->
@@ -914,7 +920,7 @@ and _lexp_rec_decl decls ctx i =
(* unused arg *)
| Ldecl ((l, s), None, _) ->
lexp_error l ("Variable \"" ^ s ^ "\" is unused!");
- vctx) tctx decls in
+ vctx) ctx decls in
(List.rev !lst), ctx
@@ -931,80 +937,6 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =
(loop p ctx [])
-(* Print context *)
-and print_lexp_ctx (ctx : elab_context) =
- let ((n, map), env, f) = ctx in
-
- print_string (make_title " LEXP CONTEXT ");
-
- make_rheader [
- (Some ('l', 10), "NAME");
- (Some ('l', 7), "INDEX");
- (Some ('l', 10), "NAME");
- (Some ('l', 4), "OFF");
- (Some ('l', 29), "VALUE:TYPE")];
-
- print_string (make_sep '-');
-
- (* it is annoying to print according to StringMap order *)
- (* let's use myers list order *)
- let rec extract_names (lst: lexp_context) acc =
- match lst with
- | Mnil-> acc
- | Mcons (hd, tl, _, _) ->
- let name = match hd with
- | (_, Some (_, name), _, _) -> name
- | _ -> "" in
- extract_names tl (name::acc) in
-
- let ord = extract_names env [] in
-
- let rec _print idx ord =
- match ord with
- | [] -> ()
- | hd::tl ->(
- let idx2 = StringMap.find hd map in
-
- (if idx2 != idx then ());
-
- print_string " | "; lalign_print_string hd 10;
- print_string " | "; lalign_print_int (n - idx - 1) 7;
- print_string " | ";
-
- let ptr_str = "" in (*" | | | | " in *)
-
- try let r, name, exp, tp =
- match env_lookup_by_index (n - idx - 1) ctx with
- | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp
- | _ -> 0, "", None, dltype in
-
- (* Print env Info *)
- lalign_print_string name 10; (* name must match *)
- print_string " | ";
- lalign_print_int r 4;
- print_string " | ";
-
- let _ = (match exp with
- | None -> print_string "<var>"
- | Some exp -> lexp_print exp)
- (* let str = _lexp_to_str (!debug_ppctx) exp in
- let str = (match str_split str '\n' with
- | hd::tl -> print_string (hd ^ "\n"); tl
- | _ -> []) in
-
- List.iter (fun elem ->
- print_string (ptr_str ^ elem ^ "\n")) str) *)in
-
- print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n";
-
- _print (idx + 1) tl
-
- with Not_found ->
- (print_string "Not_found |\n"; _print (idx + 1) tl)) in
-
- _print 0 ord;
-
- print_string (make_sep '=')
and print_lexp_trace () =
print_trace " LEXP TRACE " 50 pexp_to_string pexp_print !_global_lexp_trace
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -37,7 +37,11 @@ module S = Subst
module B = Builtin
module DB = Debruijn
-let conv_erase = true (* If true, conv ignores erased terms. *)
+(* `conv_erase` is supposed to be safe according to the ICC papers. *)
+let conv_erase = true (* Makes conv ignore erased terms. *)
+
+(* The safety of `impredicative_erase` is unknown. But I like the idea. *)
+let impredicative_erase = true (* Allows erasable args to be impredicative. *)
(* Lexp context *)
@@ -195,14 +199,24 @@ let assert_type e t t' =
if conv_p t t' then ()
else U.msg_error "TC" (lexp_location e) "Type mismatch"; ()
+let rec sort_level_max l1 l2 = match l1, l2 with
+ | SortLevel SLz, l2 -> l2
+ | l1, SortLevel SLz -> l1
+ | SortLevel (SLsucc l1), SortLevel (SLsucc l2)
+ -> SortLevel (SLsucc (sort_level_max l1 l2))
+ | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *)
+ -> U.msg_error "TC" (lexp_location l1)
+ ("Can't compute the max of levels `"
+ ^ lexp_to_string l1 ^ "` and `"
+ ^ lexp_to_string l2 ^ "`");
+ SortLevel SLz
+
let sort_compose l s1 s2 =
match s1, s2 with
- | (Stype (SortLevel (SLn n1)), Stype (SortLevel (SLn n2)))
- (* Basic predicativity rule. *)
- -> Stype (SortLevel (SLn (max n1 n2)))
- | ( (StypeLevel, Stype (SortLevel (SLn _)))
+ | (Stype l1, Stype l2) -> Stype (sort_level_max l1 l2)
+ | ( (StypeLevel, Stype _)
| (StypeLevel, StypeOmega)
- (* | (Sort (_, Stype (SortLevel (SLn _))), Sort (_, StypeOmega)) *))
+ | (Stype _, StypeOmega))
-> StypeOmega
| _,_ -> (U.msg_error "TC" l
"Mismatch sorts for arg and result";
@@ -218,8 +232,8 @@ let rec check ctx e =
-> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!";
B.type_int)
| SortLevel (_) -> B.type_level
- | Sort (l, Stype (SortLevel (SLn n)))
- -> Sort (l, Stype (SortLevel (SLn (1 + n))))
+ | Sort (l, Stype (SortLevel l1 as sl1))
+ -> Sort (l, Stype (SortLevel (SLsucc sl1)))
| Sort (_, (StypeOmega|StypeLevel))
-> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!";
B.type_omega)
@@ -248,7 +262,8 @@ let rec check ctx e =
let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in
match k1, k2 with
| (Sort (_, s1), Sort (_, s2))
- -> Sort (l, sort_compose l s1 s2)
+ -> if ak == P.Aerasable && impredicative_erase then k2
+ else Sort (l, sort_compose l s1 s2)
| (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2)
"Not a proper type";
Sort (l, StypeOmega))
@@ -280,20 +295,29 @@ let rec check ctx e =
"Calling a non function!"; ft))
ft args
| Inductive (l, label, args, cases)
- -> let rec arg_loop args s ctx =
+ -> let level = SMap.fold
+ (fun _ case level ->
+ List.fold_left
+ (fun level (ak, _, t) ->
+ if ak == P.Aerasable && impredicative_erase
+ then level
+ else match check ctx t with
+ | Sort (_, Stype level')
+ (* FIXME: scoping of level vars! *)
+ -> sort_level_max level level'
+ | _ -> U.msg_error "TC" (lexp_location t)
+ "Field type is not a Type!";
+ SortLevel SLz)
+ level
+ case)
+ cases (SortLevel SLz) in
+ let rec arg_loop args ctx =
match args with
- | [] -> Sort (l, s)
+ | [] -> Sort (l, Stype level)
| (ak, v, t)::args
- -> let s' = match check ctx t with
- | Sort (_, s') -> s'
- | _ -> (U.msg_error "TC" (lexp_location t)
- "Field type is not a Type!";
- Stype (SortLevel (SLn 0))) in
- Arrow (ak, Some v, t, lexp_location t,
- (* FIXME: `sort_compose` doesn't do what we want! *)
- arg_loop args (sort_compose l s s')
- (DB.lctx_extend ctx v Variable t)) in
- let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in
+ -> Arrow (ak, Some v, t, lexp_location t,
+ arg_loop args (DB.lctx_extend ctx v Variable t)) in
+ let tct = arg_loop args ctx in
(* FIXME: Check cases! *)
tct
| Case (l, e, it, ret, branches, default)
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -301,7 +301,7 @@ and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type
and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type =
match sortlvl, lxp with
| (SortLevel s, SortLevel s2) -> (match s, s2 with
- | SLn i, SLn j when i = j -> Some (subst, [])
+ | SLz, SLz -> Some (subst, [])
| SLsucc l1, SLsucc l2 -> unify l1 l2 subst
| _, _ -> None)
| _, _ -> None
=====================================
tests/eval_test.ml
=====================================
--- a/tests/eval_test.ml
+++ b/tests/eval_test.ml
@@ -70,7 +70,7 @@ let _ = test_eval_eqv_named
"a = 10; b = a; c = b; d = c;"
- "d" (* == *) "10"
+ "d" (* == *) "10"
(* Let
* ------------------------ *)
@@ -92,7 +92,7 @@ let _ = test_eval_eqv_named
"sqr : Int -> Int;
sqr = lambda x -> x * x;"
- "(sqr 4);" (* == *) "16"
+ "sqr 4;" (* == *) "16"
let _ = test_eval_eqv_named
"Nested Lambda"
@@ -103,7 +103,7 @@ let _ = test_eval_eqv_named
cube : Int -> Int;
cube = lambda x -> x * (sqr x);"
- "(cube 4)" (* == *) "64"
+ "cube 4" (* == *) "64"
(* Cases + Inductive types
@@ -130,7 +130,7 @@ let _ = test_eval_eqv_named
| ctr2 l => 2
| _ => 3;"
- "(test_fun a); (test_fun b); (test_fun c)"
+ "test_fun a; test_fun b; test_fun c"
"1; 2; 3"
@@ -156,11 +156,11 @@ let _ = test_eval_eqv_named
"Inductive::Recursive Call"
(nat_decl ^ "
- one = (succ zero);
- two = (succ one);
- three = (succ two);")
+ one = succ zero;
+ two = succ one;
+ three = succ two;")
- "(to-num zero); (to-num one); (to-num two);"
+ "to-num zero; to-num one; to-num two;"
"0; 1; 2"
@@ -168,9 +168,9 @@ let _ = test_eval_eqv_named
"Inductive::Nat Plus"
(nat_decl ^ "
- one = (succ zero);
- two = (succ one);
- three = (succ two);
+ one = succ zero;
+ two = succ one;
+ three = succ two;
plus : Nat -> Nat -> Nat;
plus = lambda (x : Nat) -> lambda (y : Nat) -> case x
@@ -187,11 +187,13 @@ let _ = test_eval_eqv_named
"Mutually Recursive Definition"
(nat_decl ^ "
- one = (succ zero);
- two = (succ one);
- three = (succ two);
+ one = succ zero;
+ two = succ one;
+ three = succ two;
even : Nat -> Int;
+ odd : Nat -> Int;
+
odd = lambda (n : Nat) -> case n
| zero => 0
| succ y => (even y);
@@ -200,7 +202,7 @@ let _ = test_eval_eqv_named
| zero => 1
| succ y => (odd y);")
- "(odd one); (even one); (odd two); (even two);"
+ "odd one; even one; odd two; even two;"
"1; 0; 0; 1"
@@ -212,9 +214,9 @@ let _ = test_eval_eqv_named
add = lambda x y -> (x + y);
inc : Int -> Int;
- inc = (add 1);"
+ inc = add 1;"
- "(inc 1); (inc 2); (inc 3);"
+ "inc 1; inc 2; inc 3;"
"2; 3; 4"
View it on GitLab: https://gitlab.com/monnier/typer/compare/a761156cbf492f33a65ef146d0b38b5260…
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
5949b172 by Stefan Monnier at 2016-09-26T20:29:53-04:00
Missing changes in last commit
- - - - -
1 changed file:
- src/lparse.ml
Changes:
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -570,17 +570,21 @@ and lexp_read_pattern pattern exp target ctx:
^ "` is not an inductive type!") in
(* Remove non explicit argument. *)
- let rec remove_nexplicit args acc =
- match args with
- | [] -> List.rev acc
- | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc)
- | hd::tl -> remove_nexplicit tl acc in
-
- let cons_args = remove_nexplicit cons_args [] in
-
- (* read pattern args *)
- let args, nctx = lexp_read_pattern_args args cons_args ctx in
- (cons_name, loc, args), nctx
+ let rec remove_nexplicit args acc =
+ match args with
+ | [] -> List.rev acc
+ | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc)
+ | hd::tl -> remove_nexplicit tl acc in
+
+ let cons_args = remove_nexplicit cons_args [] in
+
+ (* read pattern args *)
+ let args, nctx = lexp_read_pattern_args args cons_args ctx in
+ (cons_name, loc, args), nctx
+ | _ -> lexp_warning (pexp_location ctor)
+ ("Invalid constructor `"
+ ^ (pexp_to_string ctor) ^ "`");
+ ("_", pexp_location ctor, []), ctx
(* Read patterns inside a constructor *)
and lexp_read_pattern_args args (args_type : lexp list) ctx:
View it on GitLab: https://gitlab.com/monnier/typer/commit/5949b172d8b5f6635b0896a0aea29db44e0…
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
e938c998 by Stefan Monnier at 2016-09-26T20:29:14-04:00
Make type levels more canonical
* src/lexp.ml (sort_level): Replace SLn with SLz.
(lexp_location, _lexp_to_str): Adjust accordingly.
* src/opslexp.ml (sort_level_max): New function.
(sort_compose): Use it.
(impredicative_erase): New var.
(check): Adjust for new SLz. Obey impredicative_erase.
Fix level calculation for inductive types.
* src/builtin.ml (type0, type1, type2): Adjust.
- - - - -
4 changed files:
- src/builtin.ml
- src/debruijn.ml
- src/lexp.ml
- src/opslexp.ml
Changes:
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -98,9 +98,12 @@ let dump_predef () =
(* Builtin types *)
let dloc = dummy_location
-let type0 = Sort (dloc, Stype (SortLevel (SLn 0)))
-let type1 = Sort (dloc, Stype (SortLevel (SLn 1)))
-let type2 = Sort (dloc, Stype (SortLevel (SLn 2)))
+let level0 = SortLevel SLz
+let level1 = SortLevel (SLsucc level0)
+let level2 = SortLevel (SLsucc level1)
+let type0 = Sort (dloc, Stype level0)
+let type1 = Sort (dloc, Stype level1)
+let type2 = Sort (dloc, Stype level2)
let type_omega = Sort (dloc, StypeOmega)
let type_level = Sort (dloc, StypeLevel)
@@ -343,7 +346,7 @@ let declexpr_impl loc largs ctx ftype =
let lxp = match env_lookup_expr ctx ((loc, vn), vi) with
| Some lxp -> lxp
| None -> builtin_error loc "no expr available" in
- let ltp = env_lookup_type ctx ((loc, vn), vi) in
+ let ltp = env_lookup_type ctx ((loc, vn), vi) in (* FIXME: Unused? *)
lxp, ftype
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -47,7 +47,7 @@ let debruijn_warning = msg_warning "DEBRUIJN"
* ---------------------------------- *)
let dloc = dummy_location
-let type0 = Sort (dloc, Stype (SortLevel (SLn 0)))
+let type0 = Sort (dloc, Stype (SortLevel SLz))
let dltype = type0
type property_key = (int * string) (* rev_dbi * Var name *)
@@ -180,8 +180,8 @@ let print_lexp_ctx (ctx : elab_context) =
(* let's use myers list order *)
let rec extract_names (lst: lexp_context) acc =
match lst with
- | Mnil-> acc
- | Mcons (hd, tl, _, _) ->
+ | M.Mnil -> acc
+ | M.Mcons (hd, tl, _, _) ->
let name = match hd with
| (_, Some (_, name), _, _) -> name
| _ -> "" in
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -80,13 +80,24 @@ type ltype = lexp
* * unification. *\)
* | MetaFoF
* and subst = lexp VMap.t *)
+ (*
+ * The PTS I'm imagining looks like:
+ *
+ * S = { TypeLevel, TypeOmega, Type ℓ }
+ * A = { Level : TypeLevel, Z : Level, S : Level → Level,
+ * Type : (ℓ : Level) → Type (S ℓ) }
+ * R = { (TypeLevel, Type ℓ, TypeOmega),
+ * (TypeLevel, TypeOmega, TypeOmega),
+ * (Type ℓ, TypeOmega, TypeOmega),
+ * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) }
+ *)
and sort =
| Stype of lexp
| StypeOmega
| StypeLevel
and sort_level =
- | SLn of int
- | SLsucc of lexp
+ | SLz
+ | SLsucc of lexp
type varbind =
@@ -246,7 +257,7 @@ let rec lexp_location e =
match e with
| Sort (l,_) -> l
| SortLevel (SLsucc e) -> lexp_location e
- | SortLevel (SLn _) -> U.dummy_location
+ | SortLevel SLz -> U.dummy_location
| Imm s -> sexp_location s
| Var ((l,_),_) -> l
| Builtin ((l, _), _) -> l
@@ -769,7 +780,7 @@ and _lexp_to_str ctx exp =
| Builtin ((_, name), _) -> name
| Sort (_, Stype lvl) -> (match lvl with
- | SortLevel (SLn v) -> "Type_" ^ (string_of_int v)
+ | SortLevel SLz -> "Type_0"
| _ -> "Type_?")
| _ -> print_string "Printing Not Implemented"; "-- --"
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -37,7 +37,11 @@ module S = Subst
module B = Builtin
module DB = Debruijn
-let conv_erase = true (* If true, conv ignores erased terms. *)
+(* `conv_erase` is supposed to be safe according to the ICC papers. *)
+let conv_erase = true (* Makes conv ignore erased terms. *)
+
+(* The safety of `impredicative_erase` is unknown. But I like the idea. *)
+let impredicative_erase = true (* Allows erasable args to be impredicative. *)
(* Lexp context *)
@@ -185,14 +189,24 @@ let assert_type e t t' =
if conv_p t t' then ()
else U.msg_error "TC" (lexp_location e) "Type mismatch"; ()
+let rec sort_level_max l1 l2 = match l1, l2 with
+ | SortLevel SLz, l2 -> l2
+ | l1, SortLevel SLz -> l1
+ | SortLevel (SLsucc l1), SortLevel (SLsucc l2)
+ -> SortLevel (SLsucc (sort_level_max l1 l2))
+ | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *)
+ -> U.msg_error "TC" (lexp_location l1)
+ ("Can't compute the max of levels `"
+ ^ lexp_to_string l1 ^ "` and `"
+ ^ lexp_to_string l2 ^ "`");
+ SortLevel SLz
+
let sort_compose l s1 s2 =
match s1, s2 with
- | (Stype (SortLevel (SLn n1)), Stype (SortLevel (SLn n2)))
- (* Basic predicativity rule. *)
- -> Stype (SortLevel (SLn (max n1 n2)))
- | ( (StypeLevel, Stype (SortLevel (SLn _)))
+ | (Stype l1, Stype l2) -> Stype (sort_level_max l1 l2)
+ | ( (StypeLevel, Stype _)
| (StypeLevel, StypeOmega)
- (* | (Sort (_, Stype (SortLevel (SLn _))), Sort (_, StypeOmega)) *))
+ | (Stype _, StypeOmega))
-> StypeOmega
| _,_ -> (U.msg_error "TC" l
"Mismatch sorts for arg and result";
@@ -208,8 +222,8 @@ let rec check ctx e =
-> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!";
B.type_int)
| SortLevel (_) -> B.type_level
- | Sort (l, Stype (SortLevel (SLn n)))
- -> Sort (l, Stype (SortLevel (SLn (1 + n))))
+ | Sort (l, Stype (SortLevel l1 as sl1))
+ -> Sort (l, Stype (SortLevel (SLsucc sl1)))
| Sort (_, (StypeOmega|StypeLevel))
-> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!";
B.type_omega)
@@ -238,7 +252,8 @@ let rec check ctx e =
let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in
match k1, k2 with
| (Sort (_, s1), Sort (_, s2))
- -> Sort (l, sort_compose l s1 s2)
+ -> if ak == P.Aerasable && impredicative_erase then k2
+ else Sort (l, sort_compose l s1 s2)
| (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2)
"Not a proper type";
Sort (l, StypeOmega))
@@ -270,20 +285,29 @@ let rec check ctx e =
"Calling a non function!"; ft))
ft args
| Inductive (l, label, args, cases)
- -> let rec arg_loop args s ctx =
+ -> let level = SMap.fold
+ (fun _ case level ->
+ List.fold_left
+ (fun level (ak, _, t) ->
+ if ak == P.Aerasable && impredicative_erase
+ then level
+ else match check ctx t with
+ | Sort (_, Stype level')
+ (* FIXME: scoping of level vars! *)
+ -> sort_level_max level level'
+ | _ -> U.msg_error "TC" (lexp_location t)
+ "Field type is not a Type!";
+ SortLevel SLz)
+ level
+ case)
+ cases (SortLevel SLz) in
+ let rec arg_loop args ctx =
match args with
- | [] -> Sort (l, s)
+ | [] -> Sort (l, Stype level)
| (ak, v, t)::args
- -> let s' = match check ctx t with
- | Sort (_, s') -> s'
- | _ -> (U.msg_error "TC" (lexp_location t)
- "Field type is not a Type!";
- Stype (SortLevel (SLn 0))) in
- Arrow (ak, Some v, t, lexp_location t,
- (* FIXME: `sort_compose` doesn't do what we want! *)
- arg_loop args (sort_compose l s s')
- (DB.lctx_extend ctx v Variable t)) in
- let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in
+ -> Arrow (ak, Some v, t, lexp_location t,
+ arg_loop args (DB.lctx_extend ctx v Variable t)) in
+ let tct = arg_loop args ctx in
(* FIXME: Check cases! *)
tct
| Case (l, e, it, ret, branches, default)
View it on GitLab: https://gitlab.com/monnier/typer/commit/e938c9982c3e7e753cd33906c99c9273d82…
1
0
[Git][monnier/typer][master] 4 commits: Merge branch 'master' of gitlab.com:monnier/typer
by Setepenre 26 Sep '16
by Setepenre 26 Sep '16
26 Sep '16
Setepenre pushed to branch master at Stefan / Typer
Commits:
e314669e by Pierre Delaunay at 2016-09-25T13:39:35-04:00
Merge branch 'master' of gitlab.com:monnier/typer
- - - - -
f83ee0b4 by Pierre Delaunay at 2016-09-26T12:05:47-04:00
Merge branch 'master' of github.com:Delaunay/typer
- - - - -
12a677ab by Pierre Delaunay at 2016-09-26T19:27:11-04:00
Try to fix our Macro_ index problem. Nevertheless, it does not work
as a lot of index are not computed correctly anymore
* Moved (print_lexp_ctx) from lparse.ml to debruijn.ml to help debugging
* src/lparse.ml: types and expression are processed in a different context
- - - - -
db617a20 by Pierre Delaunay at 2016-09-26T19:54:32-04:00
Merge with master. Indices seem to be correct.
Nevertheles, Macro are still not recognized as such
(back to the original issue)
- - - - -
6 changed files:
- btl/types.typer
- samples/nat.typer
- src/builtin.ml
- src/debruijn.ml
- src/lparse.ml
- tests/eval_test.ml
Changes:
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -66,7 +66,7 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool);
% -----------------------------------------------------
List : Type -> Type;
-List = inductive_ (dList (a : Type)) (nil) (cons a (List a));
+List = inductive_ (List (a : Type)) (nil) (cons a (List a));
nil = inductive-cons List nil;
cons = inductive-cons List cons;
@@ -76,7 +76,7 @@ length = lambda a ≡>
lambda xs ->
case xs
| nil => 0
- | cons hd tl => (1 + (length(a := a) tl));
+ | cons hd tl => (1 + (length (a := a) tl));
head : (a : Type) ≡> List a -> a;
head = lambda a ≡>
@@ -92,6 +92,7 @@ tail = lambda a ≡>
| nil => nil
| cons hd tl => tl;
+
% -----------------------------------------------------
% Macro
% -----------------------------------------------------
@@ -103,8 +104,8 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp);
integer_ = Built-in "integer_" (Int -> Sexp);
float_ = Built-in "float_" (Float -> Sexp);
-% Macro : Type;
-Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp));
+Macro : Type;
+Macro = inductive_ (Macro) (Macro_ (List Sexp -> Sexp));
Macro_ = inductive-cons Macro Macro_ ;
expand_macro_ : Macro -> List Sexp -> Sexp;
@@ -181,3 +182,6 @@ declexpr = Built-in "declexpr" Macro;
+
+
+
=====================================
samples/nat.typer
=====================================
--- a/samples/nat.typer
+++ b/samples/nat.typer
@@ -5,39 +5,31 @@ zero = inductive-cons Nat zero;
succ = inductive-cons Nat succ;
to-num : Nat -> Int;
-to-num = lambda (x : Nat) ->
- case x
- | (succ y) => (1 + (to-num y))
- | zero => 0;
-
-one = (succ zero);
-two = (succ one);
-three = (succ two);
+to-num = lambda (x : Nat) -> case x
+ | (succ y) => (1 + (to-num y))
+ | zero => 0;
plus : Nat -> Nat -> Nat;
-plus = lambda (x : Nat) ->
- lambda (y : Nat) ->
- case x
- | zero => y
- | succ z => succ (plus z y);
+plus = lambda (x : Nat) -> lambda (y : Nat) -> case x
+ | zero => y
+ | succ z => succ (plus z y);
+one = succ zero;
+two = succ one;
+three = succ two;
-odd : Nat -> Int;
even : Nat -> Int;
+odd : Nat -> Int;
odd = lambda (n : Nat) -> case n
- | zero => 0
- | succ y => (even y);
+ | zero => 0
+ | succ y => (even y);
even = lambda (n : Nat) -> case n
- | zero => 1
- | succ y => (odd y);
-
-%n1 = (to-num zero);
-%n2 = (to-num one);
-%n3 = (to-num two);
+ | zero => 1
+ | succ y => (odd y);
-%m1 = (to-num (plus zero two)); % 2
-%m2 = (to-num (plus two zero)); % 2
-%m3 = (to-num (plus two one)); % 3
-o1 = (even two);
\ No newline at end of file
+a = odd one;
+b = even one;
+c = odd two;
+d = even two;
\ No newline at end of file
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -75,7 +75,7 @@ let get_predef_raw (name: string) : lexp =
| None -> builtin_error dloc ("\""^ name ^ "\" was not predefined")
let get_predef_option (name: string) ctx =
- let r = (get_size ctx) - !builtin_size - 1 in
+ let r = (get_size ctx) - !builtin_size - 0 in
match !(SMap.find name (!predef_map)) with
| Some exp -> Some (mkSusp exp (S.shift r))
| None -> None
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -46,6 +46,9 @@ let debruijn_warning = msg_warning "DEBRUIJN"
(* Type definitions
* ---------------------------------- *)
+let dloc = dummy_location
+let type0 = Sort (dloc, Stype (SortLevel (SLn 0)))
+let dltype = type0
type property_key = (int * string) (* rev_dbi * Var name *)
module PropertyMap
@@ -116,7 +119,8 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t =
let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) =
lexp_ctx_cons ctx 0 (Some def) v t
-let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
+
+let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
let (loc, name) = def in
let ((n, map), env, f) = ctx in
(try let _ = senv_lookup name ctx in
@@ -124,9 +128,11 @@ let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) =
with Not_found -> ());
let nmap = StringMap.add name n map in
((n + 1, nmap),
- lexp_ctx_cons env 0 (Some def) v t,
+ lexp_ctx_cons env r (Some def) v t,
f)
+let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t
+
let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) =
let (ctx, _) =
List.fold_left
@@ -152,10 +158,88 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) =
recursion_offset - 1)
(ctx, List.length defs) defs
-let _name_error loc estr str =
- if estr = str then () else
+let env_lookup_by_index index (ctx: elab_context): env_elem =
+ (Myers.nth index (_get_env ctx))
+
+(* Print context *)
+let print_lexp_ctx (ctx : elab_context) =
+ let ((n, map), env, f) = ctx in
+
+ print_string (make_title " LEXP CONTEXT ");
+
+ make_rheader [
+ (Some ('l', 10), "NAME");
+ (Some ('l', 7), "INDEX");
+ (Some ('l', 10), "NAME");
+ (Some ('l', 4), "OFF");
+ (Some ('l', 29), "VALUE:TYPE")];
+
+ print_string (make_sep '-');
+
+ (* it is annoying to print according to StringMap order *)
+ (* let's use myers list order *)
+ let rec extract_names (lst: lexp_context) acc =
+ match lst with
+ | Mnil-> acc
+ | Mcons (hd, tl, _, _) ->
+ let name = match hd with
+ | (_, Some (_, name), _, _) -> name
+ | _ -> "" in
+ extract_names tl (name::acc) in
+
+ let ord = extract_names env [] in
+
+ let rec _print idx ord =
+ match ord with
+ | [] -> ()
+ | hd::tl ->(
+ let idx2 = StringMap.find hd map in
+
+ (if idx2 != idx then ());
+
+ print_string " | "; lalign_print_string hd 10;
+ print_string " | "; lalign_print_int (n - idx - 1) 7;
+ print_string " | ";
+
+ let ptr_str = "" in (*" | | | | " in *)
+
+ try let r, name, exp, tp =
+ match env_lookup_by_index (n - idx - 1) ctx with
+ | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp
+ | _ -> 0, "", None, dltype in
+
+ (* Print env Info *)
+ lalign_print_string name 10; (* name must match *)
+ print_string " | ";
+ lalign_print_int r 4;
+ print_string " | ";
+
+ let _ = (match exp with
+ | None -> print_string "<var>"
+ | Some exp -> lexp_print exp)
+ (* let str = _lexp_to_str (!debug_ppctx) exp in
+ let str = (match str_split str '\n' with
+ | hd::tl -> print_string (hd ^ "\n"); tl
+ | _ -> []) in
+
+ List.iter (fun elem ->
+ print_string (ptr_str ^ elem ^ "\n")) str) *)in
+
+ print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n";
+
+ _print (idx + 1) tl
+
+ with Not_found ->
+ (print_string "Not_found |\n"; _print (idx + 1) tl)) in
+
+ _print 0 ord; print_string (make_sep '=')
+
+
+let _name_error loc estr str ctx =
+ if estr = str then () else (
+ print_lexp_ctx ctx;
debruijn_error loc ("DeBruijn index refers to wrong name. " ^
- "Expected: \"" ^ estr ^ "\" got \"" ^ str ^ "\"")
+ "Expected: \"" ^ estr ^ "\" got \"" ^ str ^ "\""))
(* generic lookup *)
@@ -167,7 +251,7 @@ let _env_lookup ctx (v: vref): env_elem =
let _ = match ret with
| (_, Some (_, name), _, _) ->
(* Check if names match *)
- _name_error loc ename name;
+ _name_error loc ename name ctx;
| _ -> () in
ret)
@@ -187,9 +271,6 @@ let env_lookup_expr ctx (v : vref): lexp option =
| LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r)))
| _ -> None
-let env_lookup_by_index index (ctx: elab_context): env_elem =
- (Myers.nth index (_get_env ctx))
-
(* replace an expression by another *)
(* Most of the time it should be O(1) but it can be O(n) *)
let replace_by ctx name by =
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -162,14 +162,15 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
(* Symbol i.e identifier *)
| Pvar (loc, name) ->(
- try let idx = (senv_lookup name ctx) in
+ try
+ let idx = (senv_lookup name ctx) in
let lxp = (make_var name idx loc) in
(* search type *)
let ltp = env_lookup_type ctx ((loc, name), idx) in
lxp, ltp
- with Not_found ->
+ with e ->
(lexp_error loc ("The variable: \"" ^ name ^ "\" was not declared");
(* Error recovery. The -1 index will raise an error later on *)
(make_var name (-1) loc), dltype))
@@ -224,8 +225,8 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
let nctx = env_extend ctx var Variable ltp in
let lbody, lbtp = lexp_infer body nctx in
- (* We added one variable in the ctx * )
- let lbtp = _type_shift lbtp 1 in *)
+ (* We added one variable in the ctx
+ let lbtp = _type_shift lbtp 1 in *)
let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in
Lambda(kind, var, ltp, lbody), lambda_type
@@ -401,7 +402,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
* Constructor : a constructor is returned
* Anonymous : lambda *)
- (* retrieve function's body *)
+ (* retrieve function's body (sqr 3) sqr is a Pvar() *)
let body, ltp = _lexp_p_infer func ctx (i + 1) in
let ltp = nosusp ltp in
@@ -432,6 +433,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
"Expected non-explicit arg"
| t ->
lexp_print t; print_string "\n";
+ print_lexp_ctx ctx;
lexp_fatal (sexp_location sarg)
"Explicit arg to non-function") in
@@ -493,32 +495,32 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
_lexp_p_infer pxp ctx (i + 1) in
(* This is the builtin Macro type *)
- let macro_type = match get_predef_option "Macro" ctx with
- | Some lxp -> lxp
- (* When type.typer is being parsed and the predef is not yet
- * available *)
- | None -> dltype in
+ let macro_type, macro_disp = match get_predef_option "Macro" ctx with
+ | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx), true
+ (* When type.typer is being parsed and the predef is not yet available *)
+ | None -> dltype, false in
+
+ (*print_string "\nmacro_type="; lexp_print macro_type;
+ print_string "\nltp="; lexp_print ltp;
+ print_string " (= "; lexp_print (OL.lexp_whnf ltp (ectx_to_lctx ctx)); print_string ")\n"; *)
(* determine function type *)
match func, ltp with
- (* This is a work around for the bug described below *)
| Pvar(l, name), _ when is_builtin_macro name ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- (get_macro_impl loc name) loc largs ctx ltp
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ (get_macro_impl loc name) loc largs ctx ltp
- (* FIXME: the branch 'builtin macro' is never used because of missing shift somewhere *)
- (* while special forms have a type macro this does not recognize them as such *)
- | macro, _ when OL.conv_p ltp macro_type -> (
+ | macro, _ when (macro_disp && (OL.conv_p ltp macro_type))-> (
match macro with
| Pvar(l, name) when is_builtin_macro name ->
- print_string name;
let pargs = List.map pexp_parse sargs in
let largs = _lexp_parse_all pargs ctx i in
(get_macro_impl loc name) loc largs ctx ltp
(* true macro *)
- | _ -> handle_macro_call ())
+ | _ ->
+ handle_macro_call ())
(* FIXME: Handle special-forms here as well! *)
| _ -> handle_funcall ()
@@ -813,8 +815,9 @@ and _lexp_rec_decl decls ctx i =
* i.e let decl parsing *)
(* to compute recursive offset *)
- let n = (List.length decls) + 1 in
+ let n = (List.length decls) in
let lst = ref [] in
+ (* print_int n; print_string "\n"; *)
(* add all elements to the environment *)
let tctx = List.fold_left (fun vctx decl ->
@@ -823,29 +826,30 @@ and _lexp_rec_decl decls ctx i =
env_extend vctx (l, s) ForwardRef dltype
| Ldecl((l, s), _, Some ptp) ->
- let lxp, _ = lexp_p_infer ptp vctx in
- env_extend vctx (l, s) ForwardRef lxp
+ let ltp, _ = lexp_p_infer ptp vctx in
+ env_extend vctx (l, s) ForwardRef ltp
| Lmcall _ ->
lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in
+ (* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *)
let i = ref 0 in
let ctx = List.fold_left (fun vctx decl ->
i := !i + 1;
match decl with
+ (* +1 because we allow each definition to be recursive *)
(* lexp infer *)
| Ldecl ((l, s), Some pxp, None) ->
- let lxp, ltp = lexp_p_infer pxp vctx in
+ let lxp, ltp = lexp_p_infer pxp tctx in
lst := ((l, s), lxp, ltp)::!lst;
- (* replace forward ref by its true value *)
- replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp)
+ (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)
(* lexp check *)
| Ldecl ((l, s), Some pxp, Some ptp) ->
let ltp, _ = lexp_p_infer ptp vctx in
- let lxp = lexp_p_check pxp ltp vctx in
+ let lxp = lexp_p_check pxp ltp tctx in
lst := ((l, s), lxp, ltp)::!lst;
- replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp)
+ (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)
(* macros *)
| Lmcall (a, sargs) ->
@@ -854,7 +858,7 @@ and _lexp_rec_decl decls ctx i =
(* unused arg *)
| Ldecl ((l, s), None, _) ->
lexp_error l ("Variable \"" ^ s ^ "\" is unused!");
- vctx) tctx decls in
+ vctx) ctx decls in
(List.rev !lst), ctx
@@ -871,80 +875,6 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =
(loop p ctx [])
-(* Print context *)
-and print_lexp_ctx (ctx : elab_context) =
- let ((n, map), env, f) = ctx in
-
- print_string (make_title " LEXP CONTEXT ");
-
- make_rheader [
- (Some ('l', 10), "NAME");
- (Some ('l', 7), "INDEX");
- (Some ('l', 10), "NAME");
- (Some ('l', 4), "OFF");
- (Some ('l', 29), "VALUE:TYPE")];
-
- print_string (make_sep '-');
-
- (* it is annoying to print according to StringMap order *)
- (* let's use myers list order *)
- let rec extract_names (lst: lexp_context) acc =
- match lst with
- | Mnil-> acc
- | Mcons (hd, tl, _, _) ->
- let name = match hd with
- | (_, Some (_, name), _, _) -> name
- | _ -> "" in
- extract_names tl (name::acc) in
-
- let ord = extract_names env [] in
-
- let rec _print idx ord =
- match ord with
- | [] -> ()
- | hd::tl ->(
- let idx2 = StringMap.find hd map in
-
- (if idx2 != idx then ());
-
- print_string " | "; lalign_print_string hd 10;
- print_string " | "; lalign_print_int (n - idx - 1) 7;
- print_string " | ";
-
- let ptr_str = "" in (*" | | | | " in *)
-
- try let r, name, exp, tp =
- match env_lookup_by_index (n - idx - 1) ctx with
- | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp
- | _ -> 0, "", None, dltype in
-
- (* Print env Info *)
- lalign_print_string name 10; (* name must match *)
- print_string " | ";
- lalign_print_int r 4;
- print_string " | ";
-
- let _ = (match exp with
- | None -> print_string "<var>"
- | Some exp -> lexp_print exp)
- (* let str = _lexp_to_str (!debug_ppctx) exp in
- let str = (match str_split str '\n' with
- | hd::tl -> print_string (hd ^ "\n"); tl
- | _ -> []) in
-
- List.iter (fun elem ->
- print_string (ptr_str ^ elem ^ "\n")) str) *)in
-
- print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n";
-
- _print (idx + 1) tl
-
- with Not_found ->
- (print_string "Not_found |\n"; _print (idx + 1) tl)) in
-
- _print 0 ord;
-
- print_string (make_sep '=')
and print_lexp_trace () =
print_trace " LEXP TRACE " 50 pexp_to_string pexp_print !_global_lexp_trace
=====================================
tests/eval_test.ml
=====================================
--- a/tests/eval_test.ml
+++ b/tests/eval_test.ml
@@ -70,7 +70,7 @@ let _ = test_eval_eqv_named
"a = 10; b = a; c = b; d = c;"
- "d" (* == *) "10"
+ "d" (* == *) "10"
(* Let
* ------------------------ *)
@@ -92,7 +92,7 @@ let _ = test_eval_eqv_named
"sqr : Int -> Int;
sqr = lambda x -> x * x;"
- "(sqr 4);" (* == *) "16"
+ "sqr 4;" (* == *) "16"
let _ = test_eval_eqv_named
"Nested Lambda"
@@ -103,7 +103,7 @@ let _ = test_eval_eqv_named
cube : Int -> Int;
cube = lambda x -> x * (sqr x);"
- "(cube 4)" (* == *) "64"
+ "cube 4" (* == *) "64"
(* Cases + Inductive types
@@ -130,7 +130,7 @@ let _ = test_eval_eqv_named
| ctr2 l => 2
| _ => 3;"
- "(test_fun a); (test_fun b); (test_fun c)"
+ "test_fun a; test_fun b; test_fun c"
"1; 2; 3"
@@ -156,11 +156,11 @@ let _ = test_eval_eqv_named
"Inductive::Recursive Call"
(nat_decl ^ "
- one = (succ zero);
- two = (succ one);
- three = (succ two);")
+ one = succ zero;
+ two = succ one;
+ three = succ two;")
- "(to-num zero); (to-num one); (to-num two);"
+ "to-num zero; to-num one; to-num two;"
"0; 1; 2"
@@ -168,9 +168,9 @@ let _ = test_eval_eqv_named
"Inductive::Nat Plus"
(nat_decl ^ "
- one = (succ zero);
- two = (succ one);
- three = (succ two);
+ one = succ zero;
+ two = succ one;
+ three = succ two;
plus : Nat -> Nat -> Nat;
plus = lambda (x : Nat) -> lambda (y : Nat) -> case x
@@ -187,11 +187,13 @@ let _ = test_eval_eqv_named
"Mutually Recursive Definition"
(nat_decl ^ "
- one = (succ zero);
- two = (succ one);
- three = (succ two);
+ one = succ zero;
+ two = succ one;
+ three = succ two;
even : Nat -> Int;
+ odd : Nat -> Int;
+
odd = lambda (n : Nat) -> case n
| zero => 0
| succ y => (even y);
@@ -200,7 +202,7 @@ let _ = test_eval_eqv_named
| zero => 1
| succ y => (odd y);")
- "(odd one); (even one); (odd two); (even two);"
+ "odd one; even one; odd two; even two;"
"1; 0; 0; 1"
@@ -212,9 +214,9 @@ let _ = test_eval_eqv_named
add = lambda x y -> (x + y);
inc : Int -> Int;
- inc = (add 1);"
+ inc = add 1;"
- "(inc 1); (inc 2); (inc 3);"
+ "inc 1; inc 2; inc 3;"
"2; 3; 4"
View it on GitLab: https://gitlab.com/monnier/typer/compare/fac6cb52949425bd38aa3e92c5b89fb2f5…
1
0
[Git][monnier/typer][unification] 2 commits: Allow expressions as constructor names and inductive type refs
by Stefan 26 Sep '16
by Stefan 26 Sep '16
26 Sep '16
Stefan pushed to branch unification at Stefan / Typer
Commits:
fac6cb52 by Stefan Monnier at 2016-09-26T09:30:40-04:00
Allow expressions as constructor names and inductive type refs
* src/lexp.ml (lexp): Allow an lexp for the inductive type arg of Cons.
(lexp_unparse): Adjust accordingly.
(push_susp): Adjust accordingly. Also merge fix from unification branch.
* src/lparse.ml (_lexp_p_infer): Adjust to new Pcons and Cons
(lexp_get_inductive_type): Remove.
(lexp_read_pattern): Adjust to new Ppatcons.
* src/opslexp.ml (conv_p', check): Adjust to new Cons.
* src/pexp.ml (ppat): Allow any exp as constructor.
(pexp): Allow an exp for the inductive type arg of Cons.
- - - - -
a761156c by Stefan Monnier at 2016-09-26T09:50:04-04:00
Merge branch 'trunk' into unification
- - - - -
6 changed files:
- src/fmt_lexp.ml
- src/lexp.ml
- src/lparse.ml
- src/opslexp.ml
- src/pexp.ml
- src/unification.ml
Changes:
=====================================
src/fmt_lexp.ml
=====================================
--- a/src/fmt_lexp.ml
+++ b/src/fmt_lexp.ml
@@ -40,7 +40,7 @@ and string_of_lxp lxp =
| L.Imm (Sexp.Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")"
| L.Imm (Sexp.String (_, value)) -> "String(" ^ value ^ ")"
| L.Imm (Sexp.Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")"
- | L.Cons (((_,tname),_),(_, cname)) -> "Cons(" ^ tname ^ ", " ^ cname ^")"
+ | L.Cons (it, (_, cname)) -> "Cons(" ^ string_of_lxp it ^ ", " ^ cname ^")"
| L.Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")"
| L.Let (_) -> "Let(..)"
| L.Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")"
@@ -77,7 +77,7 @@ let rec colored_string_of_lxp lxp lcol vcol =
| L.Imm (Sexp.Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")"
| L.Imm (Sexp.String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")"
| L.Imm (Sexp.Float (_, value)) -> (lcol "Float" ) ^ "(" ^ (vcol (string_of_float value)) ^ ")"
- | L.Cons (((_,name),_),_) -> (lcol "Cons" ) ^ "(" ^ (vcol name) ^ ")"
+ | L.Cons (it, _) -> (lcol "Cons" ) ^ "(" ^ (colored_string_of_lxp it lcol vcol) ^ ")"
| L.Builtin ((_, name), _) -> (lcol "Builtin") ^ "(" ^ (vcol name) ^ ")"
| L.Let (_) -> (lcol "Let(..)")
| L.Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")"
@@ -121,7 +121,8 @@ let rec string_of_pexp pxp =
| Pexp.Plambda _ -> "Plambda (...)"
| Pexp.Pcall _ -> "Pcall (...)"
| Pexp.Pinductive _ -> "Pinductive (...)"
- | Pexp.Pcons ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ s2 ^ ")"
+ | Pexp.Pcons (it, (_, s2)) -> "Pcons (" ^ string_of_pexp it
+ ^ ", " ^ s2 ^ ")"
| Pexp.Pcase _ -> "Pcase (...)"
| _ -> "Pexp not handled"
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -60,7 +60,7 @@ type ltype = lexp
| Inductive of U.location * label
* ((arg_kind * vdef * ltype) list) (* formal Args *)
* ((arg_kind * vdef option * ltype) list) SMap.t
- | Cons of vref * symbol (* = Type info * ctor_name *)
+ | Cons of lexp * symbol (* = Type info * ctor_name *)
| Case of U.location * lexp
* ltype (* The base inductive type over which we switch. *)
* ltype (* The type of the return value of all branches *)
@@ -307,7 +307,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
ncase)
cases in
Inductive (l, label, nargs, ncases)
- | Cons _ -> e
+ | Cons (it, name) -> Cons (mkSusp it s, name)
| Case (l, e, it, ret, cases, default)
-> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s,
SMap.map (fun (l, cargs, e)
@@ -503,7 +503,7 @@ let rec lexp_unparse lxp =
| Imm (sexp) -> Pimm (sexp)
| Builtin ((loc, name), _) -> Pvar((loc, name))
| Var ((loc, name), _) -> Pvar((loc, name))
- | Cons (((iloc, iname), idx), ctor) -> Pcons((iloc, iname), ctor)
+ | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor)
| Lambda (kind, vdef, ltp, body) ->
Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body)
| Arrow (arg_kind, vdef, ltp1, loc, ltp2) ->
@@ -538,6 +538,7 @@ let rec lexp_unparse lxp =
in Pinductive(label, pfargs, ctor)
| Case (loc, target, tltp, bltp, branches, default) ->
+ let bt = lexp_unparse bltp in
let pbranch = List.map (fun (str, (loc, args, bch)) ->
match args with
| [] -> Ppatvar (loc, str), lexp_unparse bch
@@ -546,7 +547,9 @@ let rec lexp_unparse lxp =
match vdef with
| Some vdef -> Some (kind, vdef), Ppatvar(vdef)
| None -> None, Ppatany(loc)) args
- in Ppatcons ((loc, str), pat_args), lexp_unparse bch
+ (* FIXME: Rather than a Pcons we'd like to refer to an existing
+ * binding with that value! *)
+ in Ppatcons (Pcons (bt, (loc, str)), pat_args), lexp_unparse bch
) (SMap.bindings branches) in
let pbranch = match default with
@@ -697,8 +700,8 @@ and _lexp_to_str ctx exp =
(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^
(make_indent 1) ^ (lexp_to_stri 1 lbody)
- | Cons(((_, idt_name), idx), (_, ctor_name)) ->
- (keyword "inductive-cons ") ^ idt_name ^ (index idx) ^ " " ^ ctor_name
+ | Cons(t, (_, ctor_name)) ->
+ (keyword "inductive-cons ") ^ (lexp_to_str t) ^ " " ^ ctor_name
| Call(fname, args) -> (
(* get function name *)
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -232,49 +232,36 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
lexp_call fname _args ctx i
(* Pcons *)
- | Pcons(vr, sym) -> (
- let (loc, type_name) = vr in
- let (_, cname) = sym in
-
- (* An inductive type named type_name must be in the environment *)
- try let idx = senv_lookup type_name ctx in
- (* Check if the constructor exists *)
- let idt = match env_lookup_expr ctx (vr, idx) with
- | Some idt -> idt
- | None -> lexp_fatal loc ("expression " ^ type_name ^ " not found") in
-
- (* make Base type *)
- let inductive_type = Var((loc, type_name), idx) in
-
- (* Get constructor args *)
- let formal, args = match nosusp idt with
- | Inductive(_, _, formal, ctor_def) -> (
- try formal, (SMap.find cname ctor_def)
- with Not_found ->
- lexp_error loc
- ("Constructor \"" ^ cname ^ "\" does not exist");
- [], [])
- | _ -> lexp_error loc "Not an Inductive Type";
- Debug_fun.do_debug (fun () ->
- print_string ("idt : " ^ Fmt_lexp.string_of_lxp (nosusp idt) ^ ", p : " ^ (Fmt_lexp.string_of_pexp p));
- print_newline (); ());
- [], []
- in
-
- (* build Arrow type *)
- let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
- Arrow(kind, v, tp, loc, ltp)) inductive_type (List.rev args) in
-
- (* Add Aerasable argument *)
- let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
- Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in
-
- Cons((vr, idx), sym), cons_type
-
- with Not_found ->
- lexp_error loc
- ("The inductive type: " ^ type_name ^ " was not declared");
- Cons((vr, -1), sym), dltype)
+ | Pcons(t, sym) ->
+ let idt, _ = lexp_infer t ctx in
+ let (loc, cname) = sym in
+ let meta_ctx, _ = !global_substitution in
+
+ (* Get constructor args *)
+ let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx)
+ meta_ctx with
+ | Inductive(_, _, formal, ctor_def) -> (
+ try formal, (SMap.find cname ctor_def)
+ with Not_found ->
+ lexp_error loc
+ ("Constructor \"" ^ cname ^ "\" does not exist");
+ [], [])
+
+ | _ -> lexp_error loc "Not an Inductive Type";
+ Debug_fun.do_debug (fun () ->
+ print_string ("idt : " ^ Fmt_lexp.string_of_lxp (nosusp idt) ^ ", p : " ^ (Fmt_lexp.string_of_pexp p));
+ print_newline (); ());
+ [], [] in
+
+ (* build Arrow type *)
+ let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
+ Arrow(kind, v, tp, loc, ltp)) idt (List.rev args) in
+
+ (* Add Aerasable argument *)
+ let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
+ Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in
+
+ Cons(idt, sym), cons_type
(* Pcase: we can infer iff `patterns` is not empty *)
| Pcase (loc, target, patterns) ->
@@ -594,35 +581,19 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
(* FIXME: Handle special-forms here as well! *)
| _ -> handle_funcall ()
-(* return the inductive type declaration from the constructor *)
-and lexp_get_inductive_type loc ctor_name ctx : (string * lexp option) =
- let cons_idx = senv_lookup ctor_name ctx in
- let cons = match env_lookup_expr ctx ((loc, ctor_name), cons_idx) with
- | Some lxp -> lxp
- | None -> lexp_warning loc ("constructor \"" ^ ctor_name ^ "\" not found"); dltype in
-
- (* get inductive type index *)
- match cons with
- | Cons(((_, name), idx), _) ->
- (* get inductive type declaration *)
- name, env_lookup_expr ctx ((loc, name), idx + cons_idx)
-
- | _ -> lexp_warning loc (ctor_name ^ " is not a constructor");
- "", None
-
(* Read a pattern and create the equivalent representation *)
and lexp_read_pattern pattern exp target ctx:
((string * location * (arg_kind * vdef option) list) * elab_context) =
match pattern with
- | Ppatany (loc) -> (* Catch all expression nothing to do *)
+ | Ppatany (loc) -> (* Catch all expression nothing to do. *)
("_", loc, []), ctx
| Ppatvar ((loc, name) as var) ->(
try(
let idx = senv_lookup name ctx in
match env_lookup_expr ctx ((loc, name), idx) with
- (* We are matching a constructor *)
+ (* We are matching a constructor. *)
| Some (Cons _) -> (name, loc, []), ctx
(* name is defined but is not a constructor *)
@@ -631,28 +602,32 @@ and lexp_read_pattern pattern exp target ctx:
| _ -> let nctx = ctx_define ctx var target dltype in
(name, loc, []), nctx)
- (* would it not make a default match too? *)
+ (* Would it not make a default match too? *)
with Not_found ->
- (* Create a variable containing target *)
+ (* Create a variable containing target. *)
let nctx = ctx_define ctx var target dltype in
(name, loc, []), nctx)
- | Ppatcons (ctor_name, args) ->
- let (loc, cons_name) = ctor_name in
-
- (* We need the constructor type info *)
- let inductive_name, inductive_ref = match lexp_get_inductive_type loc cons_name ctx with
- | name, Some lxp -> name, lxp
- | _ -> "", dltype in
-
- (*get cons argument types *)
- let cons_args = match inductive_ref with
- | Inductive(_, _, _, map) -> (try SMap.find cons_name map
- with Not_found -> lexp_warning loc
- (inductive_name ^ " does not hold a " ^ cons_name ^ " constructor"); [])
- | _ -> [] in
-
- (* remove non explicit argument *)
+ | Ppatcons (ctor, args) ->
+ (* Get cons argument types. *)
+ let lctor, _ = lexp_p_infer ctor ctx in
+ let meta_ctx, _ = !global_substitution in
+ match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with
+ | Cons (it, (loc, cons_name))
+ -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx)
+ meta_ctx with
+ | Inductive(_, _, _, map)
+ -> (try SMap.find cons_name map
+ with Not_found
+ -> lexp_warning loc
+ ("`" ^ lexp_to_str (it)
+ ^ "` does not hold a `"
+ ^ cons_name ^ "` constructor"); [])
+ | it -> lexp_fatal loc
+ ("`" ^ lexp_to_str (it)
+ ^ "` is not an inductive type!") in
+
+ (* Remove non explicit argument. *)
let rec remove_nexplicit args acc =
match args with
| [] -> List.rev acc
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -108,7 +108,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool =
| _,_ -> false in
l1 == l2 && conv_args s1 s2 args1 args2
&& SMap.equal (conv_fields s1 s2) cases1 cases2
- | (Cons (v1, l1), Cons (v2, l2)) -> l1 == l2 && conv_p (Var v1) (Var v2)
+ | (Cons (t1, l1), Cons (t2, l2)) -> l1 == l2 && conv_p t1 t2
(* FIXME: Various missing cases, such as Let, Case, and beta-reduction. *)
| (_, _) -> false
@@ -131,7 +131,7 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2
* but only on *types*. If you must use it on code, be sure to use its
* return value as little as possible since WHNF will inherently introduce
* call-by-name behavior. *)
-let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx =
+let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp =
Debug_fun.do_debug (fun () ->
prerr_endline ("[StackTrace] ------------------------------------------");
prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx");
@@ -339,9 +339,9 @@ let rec check ctx e =
| _ -> ())
| _,_ -> U.msg_error "TC" l "Case on a non-inductive type!");
ret
- | Cons (vr, (_, name))
- -> (match lookup_value ctx vr with
- | Some (Inductive (l, _, fargs, constructors) as it)
+ | Cons (t, (_, name))
+ -> (match lexp_whnf t ctx VMap.empty with
+ | Inductive (l, _, fargs, constructors) as it
-> let fieldtypes = SMap.find name constructors in
let rec indtype fargs start_index =
match fargs with
=====================================
src/pexp.ml
=====================================
--- a/src/pexp.ml
+++ b/src/pexp.ml
@@ -36,15 +36,6 @@ type pvar = symbol
(* type sort = Type | Ext *)
(* type tag = string *)
-type ppat =
- (* This data type allows nested patterns, but in reality we don't
- * support them. I.e. we don't want Ppatcons within Ppatcons. *)
- | Ppatany of location
- | Ppatvar of pvar
- (* FIXME: For modules and such, we'll want to generalize this
- * `pvar' to a pexp. *)
- | Ppatcons of pvar * ((arg_kind * symbol) option * ppat) list
-
type pexp =
(* | Psort of location * sort *)
| Pimm of sexp (* Used for strings, ... *)
@@ -59,9 +50,16 @@ type pexp =
* otherwise isomorphic types. *)
| Pinductive of symbol * (arg_kind * pvar * pexp option) list
* (symbol * (arg_kind * pvar option * pexp) list) list
- | Pcons of pvar * symbol
+ | Pcons of pexp * symbol
| Pcase of location * pexp * (ppat * pexp) list
+and ppat =
+ (* This data type allows nested patterns, but in reality we don't
+ * support them. I.e. we don't want Ppatcons within Ppatcons. *)
+ | Ppatany of location
+ | Ppatvar of pvar
+ | Ppatcons of pexp * ((arg_kind * symbol) option * ppat) list
+
and pdecl =
| Ptype of symbol * pexp (* identifier : expr *)
| Pexpr of symbol * pexp (* identifier = expr *)
@@ -80,13 +78,13 @@ let rec pexp_location e =
| Plambda (_,(l,_), _, _) -> l
| Pcall (f, _) -> pexp_location f
| Pinductive ((l,_), _, _) -> l
- | Pcons ((l,_),_) -> l
+ | Pcons (e,_) -> pexp_location e
| Pcase (l, _, _) -> l
let rec pexp_pat_location e = match e with
| Ppatany l -> l
| Ppatvar (l,_) -> l
- | Ppatcons ((l, _), _) -> l
+ | Ppatcons (e, _) -> pexp_location e
(* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp"
* and "pexp_u" is the prefix for "unparse a pexp, returning a sexp". *)
@@ -159,8 +157,8 @@ let rec pexp_parse (s : sexp) : pexp =
| Node (Symbol (start, "inductive_"), _)
-> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_")
(* constructor *)
- | Node (Symbol (start, "inductive-cons"), [Symbol tname; Symbol tag])
- -> Pcons (tname, tag)
+ | Node (Symbol (start, "inductive-cons"), [e; Symbol tag])
+ -> Pcons (pexp_parse e, tag)
| Node (Symbol (start, "cons_"), _)
-> pexp_error start "Unrecognized constructor call"; Pmetavar (start, "_")
(* cases analysis *)
@@ -266,15 +264,15 @@ and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp =
and pexp_p_pat (s : sexp) : ppat = match s with
| Symbol (l, "_") -> Ppatany l
| Symbol s -> Ppatvar s
- | Node (Symbol c, args)
- -> Ppatcons (c, List.map pexp_p_pat_arg args)
+ | Node (c, args)
+ -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args)
| _ -> let l = sexp_location s in
pexp_error l "Unknown pattern"; Ppatany l
and pexp_u_pat (p : ppat) : sexp = match p with
| Ppatany l -> Symbol (l, "_")
| Ppatvar s -> Symbol s
- | Ppatcons (c, args) -> Node (Symbol c, List.map pexp_u_pat_arg args)
+ | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args)
and pexp_p_decls e: pdecl list =
match e with
@@ -337,9 +335,9 @@ and pexp_unparse (e : pexp) : sexp =
-> Node (Symbol s,
List.map pexp_u_ind_arg types))
branches)
- | Pcons (tname, ((l,_) as tag)) ->
+ | Pcons (t, ((l,_) as tag)) ->
Node (Symbol (l, "cons_"),
- [Symbol tname; Symbol tag])
+ [pexp_unparse t; Symbol tag])
| Pcase (start, e, branches) ->
Node (Symbol (start, "case_"),
pexp_unparse e
@@ -417,5 +415,5 @@ let pexp_to_string e =
| Plambda (_,(_,_), _, _) -> "Plambda"
| Pcall (_, _) -> "Pcall"
| Pinductive ((_,_), _, _) -> "Pinductive"
- | Pcons ((_,_),_) -> "Pcons"
+ | Pcons (_,_) -> "Pcons"
| Pcase (_, _, _) -> "Pcase"
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -115,10 +115,8 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type =
*)
and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type =
match (cons, lxp) with
- | (Cons ((_, idx), (_, name)),
- Cons ((_, idx2), (_, name2))) when name = name2 ->
- if idx = idx2 then Some (subst, [])
- else None
+ | (Cons (it1, (_, name)),
+ Cons (it2, (_, name2))) when name = name2 -> unify it1 it2 subst
| (_, _) -> None
(** Unify a builtin (bltin) and a lexp (lxp) if it is possible
View it on GitLab: https://gitlab.com/monnier/typer/compare/df72decc0f773ba25bf13abbf2f87f5760…
1
0
[Git][monnier/typer][master] Allow expressions as constructor names and inductive type refs
by Stefan 26 Sep '16
by Stefan 26 Sep '16
26 Sep '16
Stefan pushed to branch master at Stefan / Typer
Commits:
fac6cb52 by Stefan Monnier at 2016-09-26T09:30:40-04:00
Allow expressions as constructor names and inductive type refs
* src/lexp.ml (lexp): Allow an lexp for the inductive type arg of Cons.
(lexp_unparse): Adjust accordingly.
(push_susp): Adjust accordingly. Also merge fix from unification branch.
* src/lparse.ml (_lexp_p_infer): Adjust to new Pcons and Cons
(lexp_get_inductive_type): Remove.
(lexp_read_pattern): Adjust to new Ppatcons.
* src/opslexp.ml (conv_p', check): Adjust to new Cons.
* src/pexp.ml (ppat): Allow any exp as constructor.
(pexp): Allow an exp for the inductive type arg of Cons.
- - - - -
4 changed files:
- src/lexp.ml
- src/lparse.ml
- src/opslexp.ml
- src/pexp.ml
Changes:
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -60,7 +60,7 @@ type ltype = lexp
| Inductive of U.location * label
* ((arg_kind * vdef * ltype) list) (* formal Args *)
* ((arg_kind * vdef option * ltype) list) SMap.t
- | Cons of vref * symbol (* = Type info * ctor_name *)
+ | Cons of lexp * symbol (* = Type info * ctor_name *)
| Case of U.location * lexp
* ltype (* The base inductive type over which we switch. *)
* ltype (* The type of the return value of all branches *)
@@ -300,7 +300,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
ncase)
cases in
Inductive (l, label, nargs, ncases)
- | Cons _ -> e
+ | Cons (it, name) -> Cons (mkSusp it s, name)
| Case (l, e, it, ret, cases, default)
-> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s,
SMap.map (fun (l, cargs, e)
@@ -317,14 +317,13 @@ let rec push_susp e s = (* Push a suspension one level down. *)
(* Susp should never appear around Var/Susp/Metavar because mkSusp
* pushes the subst into them eagerly. IOW if there's a Susp(Var..)
* or Susp(Metavar..) it's because some chunk of code should use mkSusp
- * rather than Susp. *)
- | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *)
- push_susp e (scompose s' s)
- | (Var _)
- -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *)
- push_susp (mkSusp e s) S.identity
-
-let nosusp e = (* Return `e` without `Susp`. *)
+ * rather than Susp.
+ * But we still have to handle them here, since push_susp is called
+ * in many other cases than just when we bump into a Susp. *)
+ | Susp (e,s') -> push_susp e (scompose s' s)
+ | (Var _) -> nosusp (mkSusp e s)
+
+and nosusp e = (* Return `e` without `Susp`. *)
match e with
| Susp(e, s) -> push_susp e s
| _ -> e
@@ -497,7 +496,7 @@ let rec lexp_unparse lxp =
| Imm (sexp) -> Pimm (sexp)
| Builtin ((loc, name), _) -> Pvar((loc, name))
| Var ((loc, name), _) -> Pvar((loc, name))
- | Cons (((iloc, iname), idx), ctor) -> Pcons((iloc, iname), ctor)
+ | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor)
| Lambda (kind, vdef, ltp, body) ->
Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body)
| Arrow (arg_kind, vdef, ltp1, loc, ltp2) ->
@@ -532,6 +531,7 @@ let rec lexp_unparse lxp =
in Pinductive(label, pfargs, ctor)
| Case (loc, target, tltp, bltp, branches, default) ->
+ let bt = lexp_unparse bltp in
let pbranch = List.map (fun (str, (loc, args, bch)) ->
match args with
| [] -> Ppatvar (loc, str), lexp_unparse bch
@@ -540,7 +540,9 @@ let rec lexp_unparse lxp =
match vdef with
| Some vdef -> Some (kind, vdef), Ppatvar(vdef)
| None -> None, Ppatany(loc)) args
- in Ppatcons ((loc, str), pat_args), lexp_unparse bch
+ (* FIXME: Rather than a Pcons we'd like to refer to an existing
+ * binding with that value! *)
+ in Ppatcons (Pcons (bt, (loc, str)), pat_args), lexp_unparse bch
) (SMap.bindings branches) in
let pbranch = match default with
@@ -689,8 +691,8 @@ and _lexp_to_str ctx exp =
(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^
(make_indent 1) ^ (lexp_to_stri 1 lbody)
- | Cons(((_, idt_name), idx), (_, ctor_name)) ->
- (keyword "inductive-cons ") ^ idt_name ^ (index idx) ^ " " ^ ctor_name
+ | Cons(t, (_, ctor_name)) ->
+ (keyword "inductive-cons ") ^ (lexp_to_str t) ^ " " ^ ctor_name
| Call(fname, args) -> (
(* get function name *)
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -234,45 +234,30 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
lexp_call fname _args ctx i
(* Pcons *)
- | Pcons(vr, sym) -> (
- let (loc, type_name) = vr in
- let (_, cname) = sym in
+ | Pcons(t, sym) ->
+ let idt, _ = lexp_infer t ctx in
+ let (loc, cname) = sym in
- (* An inductive type named type_name must be in the environment *)
- try let idx = senv_lookup type_name ctx in
- (* Check if the constructor exists *)
- let idt = match env_lookup_expr ctx (vr, idx) with
- | Some idt -> idt
- | None -> lexp_fatal loc ("expression " ^ type_name ^ " not found") in
+ (* Get constructor args *)
+ let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) with
+ | Inductive(_, _, formal, ctor_def) -> (
+ try formal, (SMap.find cname ctor_def)
+ with Not_found ->
+ lexp_error loc
+ ("Constructor \"" ^ cname ^ "\" does not exist");
+ [], [])
- (* make Base type *)
- let inductive_type = Var((loc, type_name), idx) in
+ | _ -> lexp_error loc "Not an Inductive Type"; [], [] in
- (* Get constructor args *)
- let formal, args = match nosusp idt with
- | Inductive(_, _, formal, ctor_def) -> (
- try formal, (SMap.find cname ctor_def)
- with Not_found ->
- lexp_error loc
- ("Constructor \"" ^ cname ^ "\" does not exist");
- [], [])
+ (* build Arrow type *)
+ let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
+ Arrow(kind, v, tp, loc, ltp)) idt (List.rev args) in
- | _ -> lexp_error loc "Not an Inductive Type"; [], [] in
+ (* Add Aerasable argument *)
+ let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
+ Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in
- (* build Arrow type *)
- let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
- Arrow(kind, v, tp, loc, ltp)) inductive_type (List.rev args) in
-
- (* Add Aerasable argument *)
- let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
- Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in
-
- Cons((vr, idx), sym), cons_type
-
- with Not_found ->
- lexp_error loc
- ("The inductive type: " ^ type_name ^ " was not declared");
- Cons((vr, -1), sym), dltype)
+ Cons(idt, sym), cons_type
(* Pcase: we can infer iff `patterns` is not empty *)
| Pcase (loc, target, patterns) ->
@@ -538,35 +523,19 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
(* FIXME: Handle special-forms here as well! *)
| _ -> handle_funcall ()
-(* return the inductive type declaration from the constructor *)
-and lexp_get_inductive_type loc ctor_name ctx : (string * lexp option) =
- let cons_idx = senv_lookup ctor_name ctx in
- let cons = match env_lookup_expr ctx ((loc, ctor_name), cons_idx) with
- | Some lxp -> lxp
- | None -> lexp_warning loc ("constructor \"" ^ ctor_name ^ "\" not found"); dltype in
-
- (* get inductive type index *)
- match cons with
- | Cons(((_, name), idx), _) ->
- (* get inductive type declaration *)
- name, env_lookup_expr ctx ((loc, name), idx + cons_idx)
-
- | _ -> lexp_warning loc (ctor_name ^ " is not a constructor");
- "", None
-
(* Read a pattern and create the equivalent representation *)
and lexp_read_pattern pattern exp target ctx:
((string * location * (arg_kind * vdef option) list) * elab_context) =
match pattern with
- | Ppatany (loc) -> (* Catch all expression nothing to do *)
+ | Ppatany (loc) -> (* Catch all expression nothing to do. *)
("_", loc, []), ctx
| Ppatvar ((loc, name) as var) ->(
try(
let idx = senv_lookup name ctx in
match env_lookup_expr ctx ((loc, name), idx) with
- (* We are matching a constructor *)
+ (* We are matching a constructor. *)
| Some (Cons _) -> (name, loc, []), ctx
(* name is defined but is not a constructor *)
@@ -575,28 +544,30 @@ and lexp_read_pattern pattern exp target ctx:
| _ -> let nctx = ctx_define ctx var target dltype in
(name, loc, []), nctx)
- (* would it not make a default match too? *)
+ (* Would it not make a default match too? *)
with Not_found ->
- (* Create a variable containing target *)
+ (* Create a variable containing target. *)
let nctx = ctx_define ctx var target dltype in
(name, loc, []), nctx)
- | Ppatcons (ctor_name, args) ->
- let (loc, cons_name) = ctor_name in
-
- (* We need the constructor type info *)
- let inductive_name, inductive_ref = match lexp_get_inductive_type loc cons_name ctx with
- | name, Some lxp -> name, lxp
- | _ -> "", dltype in
-
- (*get cons argument types *)
- let cons_args = match inductive_ref with
- | Inductive(_, _, _, map) -> (try SMap.find cons_name map
- with Not_found -> lexp_warning loc
- (inductive_name ^ " does not hold a " ^ cons_name ^ " constructor"); [])
- | _ -> [] in
-
- (* remove non explicit argument *)
+ | Ppatcons (ctor, args) ->
+ (* Get cons argument types. *)
+ let lctor, _ = lexp_p_infer ctor ctx in
+ match OL.lexp_whnf lctor (ectx_to_lctx ctx) with
+ | Cons (it, (loc, cons_name))
+ -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx) with
+ | Inductive(_, _, _, map)
+ -> (try SMap.find cons_name map
+ with Not_found
+ -> lexp_warning loc
+ ("`" ^ lexp_to_str (it)
+ ^ "` does not hold a `"
+ ^ cons_name ^ "` constructor"); [])
+ | it -> lexp_fatal loc
+ ("`" ^ lexp_to_str (it)
+ ^ "` is not an inductive type!") in
+
+ (* Remove non explicit argument. *)
let rec remove_nexplicit args acc =
match args with
| [] -> List.rev acc
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -108,7 +108,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool =
| _,_ -> false in
l1 == l2 && conv_args s1 s2 args1 args2
&& SMap.equal (conv_fields s1 s2) cases1 cases2
- | (Cons (v1, l1), Cons (v2, l2)) -> l1 == l2 && conv_p (Var v1) (Var v2)
+ | (Cons (t1, l1), Cons (t2, l2)) -> l1 == l2 && conv_p t1 t2
(* FIXME: Various missing cases, such as Let, Case, and beta-reduction. *)
| (_, _) -> false
@@ -329,9 +329,9 @@ let rec check ctx e =
| _ -> ())
| _,_ -> U.msg_error "TC" l "Case on a non-inductive type!");
ret
- | Cons (vr, (_, name))
- -> (match lookup_value ctx vr with
- | Some (Inductive (l, _, fargs, constructors) as it)
+ | Cons (t, (_, name))
+ -> (match lexp_whnf t ctx with
+ | Inductive (l, _, fargs, constructors) as it
-> let fieldtypes = SMap.find name constructors in
let rec indtype fargs start_index =
match fargs with
=====================================
src/pexp.ml
=====================================
--- a/src/pexp.ml
+++ b/src/pexp.ml
@@ -36,15 +36,6 @@ type pvar = symbol
(* type sort = Type | Ext *)
(* type tag = string *)
-type ppat =
- (* This data type allows nested patterns, but in reality we don't
- * support them. I.e. we don't want Ppatcons within Ppatcons. *)
- | Ppatany of location
- | Ppatvar of pvar
- (* FIXME: For modules and such, we'll want to generalize this
- * `pvar' to a pexp. *)
- | Ppatcons of pvar * ((arg_kind * symbol) option * ppat) list
-
type pexp =
(* | Psort of location * sort *)
| Pimm of sexp (* Used for strings, ... *)
@@ -59,9 +50,16 @@ type pexp =
* otherwise isomorphic types. *)
| Pinductive of symbol * (arg_kind * pvar * pexp option) list
* (symbol * (arg_kind * pvar option * pexp) list) list
- | Pcons of pvar * symbol
+ | Pcons of pexp * symbol
| Pcase of location * pexp * (ppat * pexp) list
+and ppat =
+ (* This data type allows nested patterns, but in reality we don't
+ * support them. I.e. we don't want Ppatcons within Ppatcons. *)
+ | Ppatany of location
+ | Ppatvar of pvar
+ | Ppatcons of pexp * ((arg_kind * symbol) option * ppat) list
+
and pdecl =
| Ptype of symbol * pexp (* identifier : expr *)
| Pexpr of symbol * pexp (* identifier = expr *)
@@ -80,13 +78,13 @@ let rec pexp_location e =
| Plambda (_,(l,_), _, _) -> l
| Pcall (f, _) -> pexp_location f
| Pinductive ((l,_), _, _) -> l
- | Pcons ((l,_),_) -> l
+ | Pcons (e,_) -> pexp_location e
| Pcase (l, _, _) -> l
let rec pexp_pat_location e = match e with
| Ppatany l -> l
| Ppatvar (l,_) -> l
- | Ppatcons ((l, _), _) -> l
+ | Ppatcons (e, _) -> pexp_location e
(* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp"
* and "pexp_u" is the prefix for "unparse a pexp, returning a sexp". *)
@@ -159,8 +157,8 @@ let rec pexp_parse (s : sexp) : pexp =
| Node (Symbol (start, "inductive_"), _)
-> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_")
(* constructor *)
- | Node (Symbol (start, "inductive-cons"), [Symbol tname; Symbol tag])
- -> Pcons (tname, tag)
+ | Node (Symbol (start, "inductive-cons"), [e; Symbol tag])
+ -> Pcons (pexp_parse e, tag)
| Node (Symbol (start, "cons_"), _)
-> pexp_error start "Unrecognized constructor call"; Pmetavar (start, "_")
(* cases analysis *)
@@ -266,15 +264,15 @@ and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp =
and pexp_p_pat (s : sexp) : ppat = match s with
| Symbol (l, "_") -> Ppatany l
| Symbol s -> Ppatvar s
- | Node (Symbol c, args)
- -> Ppatcons (c, List.map pexp_p_pat_arg args)
+ | Node (c, args)
+ -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args)
| _ -> let l = sexp_location s in
pexp_error l "Unknown pattern"; Ppatany l
and pexp_u_pat (p : ppat) : sexp = match p with
| Ppatany l -> Symbol (l, "_")
| Ppatvar s -> Symbol s
- | Ppatcons (c, args) -> Node (Symbol c, List.map pexp_u_pat_arg args)
+ | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args)
and pexp_p_decls e: pdecl list =
match e with
@@ -337,9 +335,9 @@ and pexp_unparse (e : pexp) : sexp =
-> Node (Symbol s,
List.map pexp_u_ind_arg types))
branches)
- | Pcons (tname, ((l,_) as tag)) ->
+ | Pcons (t, ((l,_) as tag)) ->
Node (Symbol (l, "cons_"),
- [Symbol tname; Symbol tag])
+ [pexp_unparse t; Symbol tag])
| Pcase (start, e, branches) ->
Node (Symbol (start, "case_"),
pexp_unparse e
@@ -417,5 +415,5 @@ let pexp_to_string e =
| Plambda (_,(_,_), _, _) -> "Plambda"
| Pcall (_, _) -> "Pcall"
| Pinductive ((_,_), _, _) -> "Pinductive"
- | Pcons ((_,_),_) -> "Pcons"
+ | Pcons (_,_) -> "Pcons"
| Pcase (_, _, _) -> "Pcase"
View it on GitLab: https://gitlab.com/monnier/typer/commit/fac6cb52949425bd38aa3e92c5b89fb2f55…
1
0