Simon Génier pushed to branch lambda-elab-error-message at Stefan / Typer
Commits: 2bd6aa15 by Stefan Monnier at 2020-08-10T23:52:31-04:00 * btl/builtins.typer (Eq_comm): Update FIXME
- - - - - 28d16874 by irradiee at 2020-08-14T05:59:20-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp
- - - - - f04cab52 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Delay parsing of declarations until elaboration for define-operator
* elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that later declarations can be parsed in a context with newly declared operators
- - - - - 456370bc by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Remove the parsing error for tightly binding postfix operators
- - - - - 8beb9266 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Dump the evaluation context when the variable names don't match
- - - - - 2e00884b by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Assign the builtins Int.+, etc to suitable variables Int_+, etc.
_+_ can be Int.+ by default, but we should also keep that value in Int_+ in case _+_ gets reassigned (with a num typeclass, for instance).
- - - - - ac4cc3a5 by Jean-Alexandre Barszcz at 2020-08-20T15:01:14-04:00 Apply the instantiated metavariable substs when displaying lexps
- - - - - f0b33b28 by Jean-Alexandre Barszcz at 2020-08-20T15:01:36-04:00 Replace instantiated metavars when checking syntactic equality
- - - - - 68f25184 by irradiee at 2020-08-24T13:11:01-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp
- - - - - 588b6327 by Jean-Alexandre Barszcz at 2020-09-04T23:06:53-04:00 Fix `lexp_whnf` for Case
A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another.
This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields.
Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case.
- - - - - cb949360 by Simon Génier at 2020-09-08T10:48:22-04:00 Print incorrect arguments to a lambda expression.
- - - - -
17 changed files:
- GNUmakefile - btl/builtins.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/env.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/elab_test.ml - tests/unify_test.ml
Changes:
===================================== GNUmakefile ===================================== @@ -4,9 +4,13 @@ OCAMLBUILD=ocamlbuild
BUILDDIR := _build
+OCAMLCP := ocamlcp +OCAMLOPT := ocamlopt +OCAMLDEP := ocamldep + SRC_FILES := $(wildcard ./src/*.ml) -CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) +DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG))
OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str @@ -108,3 +112,30 @@ run/typer-file:
run/test-file: @./$(BUILDDIR)/test + +# Compile into bytecode using ocamlc in profiling mode. +# Generate a ocamlprof.dump file. +profiling-cp: + # ============================ + # profiling bytecode + # ============================ + ocamlfind $(OCAMLCP) -o profiling -linkpkg -package zarith \ + -I src str.cma -P f $(DEPSORT_FILES) + +# Compile into native code using ocamlopt in profiling mode. +# Generate a gmon.out file. +profiling-optp: + # ============================ + # profiling native code + # ============================ + ocamlfind $(OCAMLOPTP) -o profiling -linkpkg -package zarith \ + -I src str.cmxa -P f $(DEPSORT_FILES) + +# Clean profiling +# FIXME: We prefer generate files in the "./$(BUILDDIR)/" folder but how ? +# No -build-dir option found for ocamlc and ocamlopt. +clean-profiling: + -rm -rf profiling + -rm -rf src/*.cm[iox] src/*.o + -rm -rf ocamlprof.dump + -rm -rf gmon.out
===================================== btl/builtins.typer ===================================== @@ -47,7 +47,7 @@ Void = typecons Void;
%% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l -Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! +Eq_refl : ((x : ?t) ≡> Eq x x); Eq_refl = Built-in "Eq.refl";
Eq_cast : (x : ?) ≡> (y : ?) @@ -63,8 +63,11 @@ Eq_cast = Built-in "Eq.cast"; %% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: I can't figure out how `(p := p)` - %% gets inferred here, yet it seems to work!?! + %% FIXME: The code is incorrectly accepted even without + %% this `(p := p)` because we just get a metavar which + %% remains uninstantiated and undetected (and then gets + %% throw away by erasure)! + (p := p) Eq_refl;
%% General recursion!! @@ -77,7 +80,7 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) %% %% But this is not sufficient, because you could use `Y` to create %% new recursive *types* which then let you construct new arbitrary -%% recursive values of previously uninhabited types. +%% recursive values of previously non-existent types. %% E.g. you could create `Y <something> = ((... → t) -> t) -> t` %% and then give the term `λx. x x` inhabiting that type, and from that %% get a proof of False. @@ -100,10 +103,15 @@ true = datacons Bool true; false = datacons Bool false;
%% Basic operators -_+_ = Built-in "Int.+" : Int -> Int -> Int; -_-_ = Built-in "Int.-" : Int -> Int -> Int; -_*_ = Built-in "Int.*" : Int -> Int -> Int; -_/_ = Built-in "Int./" : Int -> Int -> Int; +Int_+ = Built-in "Int.+" : Int -> Int -> Int; +Int_- = Built-in "Int.-" : Int -> Int -> Int; +Int_* = Built-in "Int.*" : Int -> Int -> Int; +Int_/ = Built-in "Int./" : Int -> Int -> Int; + +_+_ = Int_+; +_-_ = Int_-; +_*_ = Int_*; +_/_ = Int_/;
%% modulo Int_mod = Built-in "Int.mod" : Int -> Int -> Int;
===================================== src/REPL.ml ===================================== @@ -135,7 +135,9 @@ let ierase_type (lexps: (ldecl list list * lexpr list)) =
let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in - let ldecls, lctx = Elab.lexp_p_decls pdecls lctx in + (* FIXME We take the parsed input here but we should take the + unparsed tokens directly instead *) + let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in let lexprs = Elab.lexp_parse_all pexprs lctx in List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) lexprs; @@ -164,8 +166,7 @@ let ieval f str ectx rctx = let raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - let lxps, ectx = Elab.lexp_p_decls nods ectx in + let lxps, ectx = Elab.lexp_p_decls [] sxps ectx in let elxps = List.map OL.clean_decls lxps in (* At this point, `elxps` is a `(vname * elexp) list list`, where: * - each `(vname * elexp)` is a definition @@ -231,6 +232,7 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table))
(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> (
===================================== src/builtin.ml ===================================== @@ -57,7 +57,7 @@ open Util
open Sexp (* Integer/Float *) open Pexp (* arg_kind *) -module L = Lexp + module OL = Opslexp open Lexp
===================================== src/debruijn.ml ===================================== @@ -35,8 +35,10 @@ module Str = Str
open Util + + open Lexp -module L = Lexp + module M = Myers open Fmt
@@ -300,7 +302,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start =
(* Only print user defined variables *) let print_lexp_ctx (ctx : lexp_context) = - print_lexp_ctx_n ctx !L.builtin_size + print_lexp_ctx_n ctx !builtin_size
(* Dump the whole context *) let dump_lexp_ctx (ctx : lexp_context) =
===================================== src/debug_util.ml ===================================== @@ -138,8 +138,6 @@ let arg_defs = [ Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); ("-tok", Arg.Unit (add_p_option "tok"), " Print tok debug info"); - ("-sexp", - Arg.Unit (add_p_option "sexp"), " Print sexp debug info"); ("-pexp", Arg.Unit (add_p_option "pexp"), " Print pexp debug info"); ("-lexp", @@ -152,7 +150,6 @@ let arg_defs = [ Arg.Unit (fun () -> add_p_option "pretok" (); add_p_option "tok" (); - add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" (); add_p_option "lctx" (); @@ -165,7 +162,6 @@ let parse_args () =
let make_default () = arg_print_options := SMap.empty; - add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" ()
@@ -176,10 +172,8 @@ let format_source () = let filename = List.hd (!arg_files) in let pretoks = prelex_file filename in let toks = lex default_stt pretoks in - let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) - toks (Some ";") in let ctx = Elab.default_ectx in - let lexps, _ = Elab.lexp_p_decls nodes ctx in + let lexps, _ = Elab.lexp_p_decls [] toks ctx in
print_string (make_sep '-'); print_string "\n";
@@ -235,26 +229,12 @@ let main () = print_string (make_title " Base Sexp"); debug_sexp_print_all toks; print_string "\n"));
- (* get node sexp *) - print_string yellow; - let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) - toks (Some ";") in - print_string reset; - - (if (get_p_option "sexp") then( - print_string (make_title " Node Sexp "); - debug_sexp_print_all nodes; print_string "\n")); - - (* Parse All Declaration *) - print_string yellow; - print_string reset; - (* get lexp *) let octx = Elab.default_ectx in
(* debug lexp parsing once merged *) print_string yellow; - let lexps, nctx = try Elab.lexp_p_decls nodes octx + let lexps, nctx = try Elab.lexp_p_decls [] toks octx with e -> print_string reset; raise e in
===================================== src/elab.ml ===================================== @@ -121,7 +121,7 @@ let sform_default_ectx = ref empty_elab_context * to errors in the user's code). *)
let elab_check_sort (ctx : elab_context) lsort var ltp = - match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) + match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) ~loc:(lexp_location lsort) @@ -238,9 +238,9 @@ let ctx_define_rec (ctx: elab_context) decls = * infer the types and perform macro-expansion. * * More specifically, we do it with 2 mutually recursive functions: - * - `check` takes a Pexp along with its expected type and returns an Lexp + * - `check` takes an Sexp along with its expected type and returns an Lexp * of that type (hopefully) - * - `infer` takes a Pexp and infers its type (which it returns along with + * - `infer` takes an Sexp and infers its type (which it returns along with * the Lexp). * This is the idea of "bidirectional type checking", which minimizes * the amount of "guessing" and/or annotations. Since we infer types anyway @@ -323,7 +323,7 @@ let rec meta_to_var ids (e : lexp) = * into something like * * Γ ⊢ λ x₁…xₙ ≡> e[x₁…xₙ/m₁…mₙ] : τ₁…τₙ ≡> τ - * + * * The above substitution is not the usual capture-avoiding substitution * since it replaces metavars with vars rather than vars with terms. * It's more like *instanciation* of those metavars. @@ -402,7 +402,7 @@ let rec meta_to_var ids (e : lexp) = * (case (B) above), so don't let it refer to the new vars. *) S.Identity (n + count) else - Identity n + S.Identity n | S.Cons (e, s', n) -> let o' = o - n in if o' < 0 then @@ -414,7 +414,8 @@ let rec meta_to_var ids (e : lexp) =
(* `o` is the binding depth at which we are relative to the "root" * of the expression (i.e. where the new vars will be inserted). *) - and loop o e = match e with + and loop o e = + match lexp_lexp' e with | Imm _ -> e | SortLevel SLz -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) @@ -576,7 +577,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype =
and elab_special_form ctx f args ot = let loc = lexp_location f in - match OL.lexp_whnf f (ectx_to_lctx ctx) with + match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _, _) -> (* Special form. *) (get_special_form name) ctx loc args ot @@ -624,7 +625,7 @@ and get_implicit_arg ctx loc oname t = (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = - match OL.lexp_whnf t (ectx_to_lctx ctx) with + match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) @@ -636,7 +637,7 @@ and infer_type pexp ectx var = * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) let t, s = infer pexp ectx in - (match OL.lexp_whnf s (ectx_to_lctx ectx) with + (match OL.lexp'_whnf s (ectx_to_lctx ectx) with | Sort (_, _) -> () (* All clear! *) (* FIXME: We could automatically coerce Type levels to Sorts, so we * could write `(a : TypeLevel) -> a -> a` instead of @@ -698,7 +699,8 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = * we use is to instantiate implicit arguments when needed, but we could/should * do lots of other things. *) and check_inferred ctx e inferred_t t = - let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) with + let (e, inferred_t) = + match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in @@ -749,7 +751,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | [] -> () in (cs, args) | None - -> match OL.lexp_whnf it' (ectx_to_lctx ctx) with + -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> let (s, targs) = List.fold_left (fun (s, targs) (ak, name, t) @@ -764,11 +766,13 @@ and check_case rtype (loc, target, ppatterns) ctx = ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); it_cs_as := Some (it', cs, args); (cs, args) - | _ -> let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) - with | Call (f, args) -> (f, args) + | _ -> let call_split e = + match OL.lexp'_whnf e (ectx_to_lctx ctx) with + | Call (f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in - let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with + let constructors = + match OL.lexp'_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -792,15 +796,17 @@ and check_case rtype (loc, target, ppatterns) ctx = let add_branch pctor pargs = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in - let rec inst_args ctx e = match OL.lexp_whnf e (ectx_to_lctx ctx) with + let rec inst_args ctx e = + let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in + match lexp_lexp' lxp with | Lambda (Aerasable, v, t, body) -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) v t in let nctx = ctx_extend ctx v Variable t in let body = inst_args nctx body in mkSusp body (S.substitute arg) - | e -> e in - match nosusp (inst_args ctx lctor) with + | e -> lxp in + match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in let (constructors, targs) = get_cs_as it' lctor in @@ -912,7 +918,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in - match sargs, ltp' with + match sargs, lexp_lexp' ltp' with | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in @@ -967,7 +973,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = largs, ltp
| sarg :: sargs, _ - -> let (arg_type, ret_type) = match ltp' with + -> let (arg_type, ret_type) = match lexp_lexp' ltp' with | Arrow (ak, _, arg_type, _, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) | _ -> unify_with_arrow ctx (sexp_location sarg) @@ -994,17 +1000,18 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> Arrow (ak, n, t, dummy_location, aa)) + -> mkArrow (ak, n, t, dummy_location, aa)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> Arrow (Aerasable, vname, t, l, e)) + -> mkArrow (Aerasable, vname, t, l, e)) altacc in if altacc' == altacc then acc (* No generalization! *) else (* Convert the Lexp back into a list of fields. *) - let rec loop e = match e with + let rec loop e = + match lexp_lexp' e with | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' @@ -1157,8 +1164,10 @@ and infer_and_generalize_type (ctx : elab_context) se name = * * But we don't bother trying to catch all cases currently. *) - let rec strip_rettype t = match t with - | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + let rec strip_rettype t = + match lexp_lexp' t with + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in @@ -1181,136 +1190,152 @@ and infer_and_generalize_def (ctx : elab_context) se = (e', t')
and lexp_decls_1 - (sdecls : sexp list) + (sdecls : sexp list) (* What's already parsed *) + (tokens : token list) (* Rest of input *) (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : location SMap.t) (* Pending type decls. *) (pending_defs : (symbol * sexp) list) (* Pending definitions. *) - : (vname * lexp * ltype) list * sexp list * elab_context = - - let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = - match sdecls with - | [] -> (if not (SMap.is_empty pending_decls) then - let (s, loc) = SMap.choose pending_decls in - error ~loc ("Variable `" ^ s ^ "` declared but not defined!") - else - assert (pending_defs == [])); - [], [], nctx - - | Symbol (_, "") :: sdecls - -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - | Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls - -> lexp_decls_1 (List.append sdecls' sdecls) - ectx nctx pending_decls pending_defs - - | Node (Symbol (loc, "_:_"), args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in - if SMap.mem vname pending_decls then - (* Don't burp: take'em all and unify! *) - let pt_idx = senv_lookup vname nctx in - (* Take the previous type annotation. *) - let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> Log.internal_error "Var not found at its index!" in - (* Unify it with the new one. *) - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (_::_) - -> lexp_error loc ltp - ("New type annotation `" - ^ lexp_string ltp ^ "` incompatible with previous `" - ^ lexp_string pt ^ "`") - | [] -> () in - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - else if List.exists (fun ((_, vname'), _) -> vname = vname') - pending_defs then - (error ~loc ("Variable `" ^ vname ^ "` already defined!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else lexp_decls_1 sdecls ectx - (ectx_extend nctx (loc, Some vname) ForwardRef ltp) - (SMap.add vname loc pending_decls) - pending_defs - | _ -> error ~loc "Invalid type declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | Node (Symbol (l, "_=_") as head, args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol ((l, vname)); sexp] - when SMap.is_empty pending_decls - -> assert (pending_defs == []); - (* Used to be true before we added define-operator. *) - (* assert (ectx == nctx); *) - let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in - (* Lexp decls are always recursive, so we have to shift by 1 to - * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, - ctx_define nctx var lexp ltp - - | [Symbol (l, vname); sexp] - -> if SMap.mem vname pending_decls then - let decl_loc = SMap.find vname pending_decls in - let v = ({file = l.file; - line = l.line; - column = l.column; - docstr = String.concat "\n" [decl_loc.docstr; l.docstr]}, - vname) in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, sexp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, nctx - else - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - else - (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | [Node (Symbol s, args) as d; body] - -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - lexp_decls_1 ((Node (head, - [Symbol s; - Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list args; body])])) - :: sdecls) - ectx nctx pending_decls pending_defs - - | _ -> error ~loc:l "Invalid definition syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | Node (Symbol (l, "define-operator"), args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) - pending_decls pending_defs - - | Node (Symbol ((l, _) as v), sargs) :: sdecls - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - lexp_decls_1 (sdecl' :: sdecls) ectx nctx - pending_decls pending_defs - - | sexp :: sdecls - -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + : (vname * lexp * ltype) list * sexp list * token list * elab_context = + + let rec lexp_decls_1 sdecls tokens nctx pending_decls pending_defs = + let sdecl, sdecls, toks = + match (sdecls, tokens) with + | (s :: sdecls, _) -> Some s, sdecls, tokens + | ([], []) -> None, [], [] + | ([], _) -> + let (s, toks) = sexp_parse_all (ectx_get_grammar nctx) + tokens (Some ";") in + Some s, [], toks in + let recur prepend_sdecls nctx pending_decls pending_defs = + lexp_decls_1 (List.append prepend_sdecls sdecls) + toks nctx pending_decls pending_defs in + match sdecl with + | None -> (if not (SMap.is_empty pending_decls) then + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") + else + assert (pending_defs == [])); + [], [], [], nctx + + | Some (Symbol (_, "")) + -> recur [] nctx pending_decls pending_defs + + | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) + -> recur sdecls' nctx pending_decls pending_defs + + | Some (Node (Symbol (loc, "_:_"), args) as thesexp) + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + if SMap.mem vname pending_decls then + (* Don't burp: take'em all and unify! *) + let pt_idx = senv_lookup vname nctx in + (* Take the previous type annotation. *) + let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | _ -> Log.internal_error "Var not found at its index!" in + (* Unify it with the new one. *) + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with + | (_::_) + -> lexp_error loc ltp + ("New type annotation `" + ^ lexp_string ltp ^ "` incompatible with previous `" + ^ lexp_string pt ^ "`") + | [] -> () in + recur [] nctx pending_decls pending_defs + else if List.exists (fun ((_, vname'), _) -> vname = vname') + pending_defs then + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); + recur [] nctx pending_decls pending_defs) + else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) + pending_defs + | _ -> error ~loc ("Invalid type declaration syntax : `" ^ + (sexp_string thesexp) ^ "`"); + recur [] nctx pending_decls pending_defs) + + | Some (Node (Symbol (l, "_=_") as head, args) as thesexp) + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol ((l, vname)); sexp] + when SMap.is_empty pending_decls + -> assert (pending_defs == []); + (* Used to be true before we added define-operator. *) + (* assert (ectx == nctx); *) + let (lexp, ltp) = infer_and_generalize_def nctx sexp in + let var = (l, Some vname) in + (* Lexp decls are always recursive, so we have to shift by 1 to + * account for the extra var (ourselves). *) + [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, + ctx_define nctx var lexp ltp + + | [Symbol (l, vname); sexp] + -> if SMap.mem vname pending_decls then + let decl_loc = SMap.find vname pending_decls in + let v = ({file = l.file; + line = l.line; + column = l.column; + docstr = String.concat "\n" [decl_loc.docstr; + l.docstr]}, + vname) in + let pending_decls = SMap.remove vname pending_decls in + let pending_defs = ((v, sexp) :: pending_defs) in + if SMap.is_empty pending_decls then + let nctx = ectx_new_scope nctx in + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, sdecls, toks, nctx + else + recur [] nctx pending_decls pending_defs + + else + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); + recur [] nctx pending_decls pending_defs) + + | [Node (Symbol s, args) as d; body] + -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) + recur [Node (head, + [Symbol s; + Node (Symbol (sexp_location d, "lambda_->_"), + [sexp_u_list args; body])])] + nctx pending_decls pending_defs + + | _ -> error ~loc:l ("Invalid definition syntax : `" ^ + (sexp_string thesexp) ^ "`"); + recur [] nctx pending_decls pending_defs) + + | Some (Node (Symbol (l, "define-operator"), args)) + (* FIXME: Move this to a "special form"! *) + -> recur [] (sdform_define_operator nctx l args None) + pending_decls pending_defs + + | Some (Node (Symbol ((l, _) as v), sargs)) + -> (* expand macro and get the generated declarations *) + let sdecl' = lexp_decls_macro v sargs nctx in + recur [sdecl'] nctx pending_decls pending_defs + + | Some sexp + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; + recur [] nctx pending_decls pending_defs
in (EV.set_getenv nctx; - let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + let res = lexp_decls_1 sdecls tokens nctx + pending_decls pending_defs in (Log.stop_on_error (); res))
-and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) +and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = - let impl sdecls ctx = match sdecls with - | [] -> [], ectx_new_scope ctx - | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in - let declss, nnctx = lexp_p_decls sdecls nctx in - decls :: declss, nnctx in - let res = impl sdecls ctx in (Log.stop_on_error (); res) + let rec impl sdecls tokens ctx = + match (sdecls, tokens) with + | ([], []) -> [], ectx_new_scope ctx + | _ -> + let decls, sdecls, tokens, nctx = + lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in + Log.stop_on_error (); + let declss, nnctx = impl sdecls tokens nctx in + decls :: declss, nnctx in + impl sdecls tokens ctx
and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in @@ -1338,10 +1363,12 @@ and sform_new_attribute ctx loc sargs ot = and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with - | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr + | [table; e; attr] when is_var e + -> table, (n - (get_var_db_index (get_var e)), U.get_vname_name (get_var_vname (get_var e))), attr | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in
- let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with + let map, attr_type = + match OL.lexp'_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal ~loc "add-attribute expects a table as first argument" in
@@ -1351,13 +1378,17 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy)
-and get_attribute ctx loc largs = - let ctx_n = get_size ctx in - let table, var = match largs with - | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in
- let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with + and get_attribute ctx loc largs = + let ctx_n = get_size ctx in + let table, var = match largs with + | [table; e] when is_var e + -> table, (ctx_n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in + + + let map = + match OL.lexp'_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map | _ -> fatal ~loc "get-attribute expects a table as first argument" in
@@ -1372,33 +1403,39 @@ and sform_get_attribute ctx loc (sargs : sexp list) ot = and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with - | [table; Var((_, Some name), idx)] -> table, (n - idx, name) + | [table; e] when is_var e + -> table, (n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in
- let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with + + let map, attr_type = + let lp = OL.lexp_whnf table (ectx_to_lctx ctx) in + match lexp_lexp' lp with | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc lxp + | lxp -> lexp_fatal loc table "get-attribute expects a table as first argument" in
(BI.o2l_bool ctx (AttributeMap.mem var map), Lazy)
-and sform_declexpr ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [Var((_, vn), vi)] - -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; - sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; - sform_dummy_ret ctx loc + and sform_declexpr ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with + | Some lxp -> (lxp, Lazy) + | None -> error ~loc "no expr available"; + sform_dummy_ret ctx loc) + | _ -> error ~loc "declexpr expects one argument"; + sform_dummy_ret ctx loc + + + let sform_decltype ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) + | _ -> error ~loc "decltype expects one argument"; + sform_dummy_ret ctx loc
-let sform_decltype ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [Var((_, vn), vi)] - -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error ~loc "decltype expects one argument"; - sform_dummy_ret ctx loc
let builtin_value_types : ltype option SMap.t ref = ref SMap.empty
@@ -1581,7 +1618,8 @@ let sform_identifier ctx loc sargs ot = -> Inverse_subst.apply_inv_subst t subst in let mv = newMetavar octx sl (loc, Some name) t in (if not (name = "") then - let idx = match mv with + let idx = + match lexp_lexp' mv with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); @@ -1605,9 +1643,10 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (arg, ost1) = match sarg with | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) | Symbol arg -> (elab_p_id arg, None) - | _ -> sexp_error (sexp_location sarg) - "Unrecognized lambda argument"; - ((dummy_location, None), None) in + | _ + -> let message = "Unrecognized lambda argument: " ^ sexp_string sarg in + sexp_error (sexp_location sarg) message; + ((dummy_location, None), None) in
let olt1 = match ost1 with | Some st -> Some (infer_type st ctx arg) @@ -1636,7 +1675,8 @@ let rec sform_lambda kind ctx loc sargs ot = None (* Read var type from the provided type *) | Some t - -> match OL.lexp_whnf t (ectx_to_lctx ctx) with + -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in + match lexp_lexp' lp with | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind -> (match olt1 with | None -> () @@ -1664,7 +1704,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> alt)
| lt - -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 + -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind arg olt1 in mklam lt1 (Some lt2))
| _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->" @@ -1695,7 +1735,7 @@ let rec sform_case ctx loc sargs ot = match sargs with
let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] - -> let declss, nctx = lexp_p_decls [sdecls] ctx in + -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in (* FIXME: Use `elaborate`. *) let bdy, ltp = infer sbody (ectx_new_scope nctx) in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in @@ -1772,9 +1812,7 @@ let sform_load usr_elctx loc sargs ot = let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) - sxps (Some ";") in - let _, elctx = lexp_p_decls nods elctx + let _, elctx = lexp_p_decls [] sxps elctx in elctx in
(* read file as elab_context *) @@ -1860,9 +1898,7 @@ let default_ectx let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) - sxps (Some ";") in - let _, lctx = lexp_p_decls nods elctx + let _, lctx = lexp_p_decls [] sxps elctx in lctx in
(* Register predef *) @@ -1922,10 +1958,8 @@ let lexp_expr_str str ctx =
let lexp_decl_str str ctx = try let tenv = default_stt in - let grm = ectx_get_grammar ctx in - let limit = Some ";" in - let sdecls = sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + let tokens = lex_str str tenv in + lexp_p_decls [] tokens ctx with Log.Stop_Compilation s -> ([],ctx)
@@ -1946,4 +1980,3 @@ let eval_decl_str str lctx rctx = let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) -
===================================== src/env.ml ===================================== @@ -167,6 +167,41 @@ let make_runtime_ctx = M.nil
let get_rte_size (ctx: runtime_env): int = M.length ctx
+let print_myers_list l print_fun start = + let n = (M.length l) - 1 in + print_string (make_title " ENVIRONMENT "); + make_rheader [(None, "INDEX"); + (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; + print_string (make_sep '-'); + + for i = start to n do + print_string " | "; + ralign_print_int (n - i) 5; + print_string " | "; + print_fun (M.nth (n - i) l); + done; + print_string (make_sep '=') + +let print_rte_ctx_n (ctx: runtime_env) start = + print_myers_list + ctx + (fun (n, vref) -> + let g = !vref in + let _ = + match n with + | (_, Some m) -> lalign_print_string m 12; print_string " | " + | _ -> print_string (make_line ' ' 12); print_string " | " in + + value_print g; print_string "\n") start + +(* Only print user defined variables *) +let print_rte_ctx ctx = + print_rte_ctx_n ctx (!L.builtin_size) + +(* Dump the whole context *) +let dump_rte_ctx ctx = + print_rte_ctx_n ctx 0 + let get_rte_variable (name: vname) (idx: int) (ctx: runtime_env): value_type = try ( @@ -177,7 +212,7 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - fatal + fatal ~print_action:(fun () -> dump_rte_ctx ctx) ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))
@@ -212,37 +247,3 @@ let nfirst_rte_var n ctx = List.rev acc in loop 0 []
-let print_myers_list l print_fun start = - let n = (M.length l) - 1 in - print_string (make_title " ENVIRONMENT "); - make_rheader [(None, "INDEX"); - (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; - print_string (make_sep '-'); - - for i = start to n do - print_string " | "; - ralign_print_int (n - i) 5; - print_string " | "; - print_fun (M.nth (n - i) l); - done; - print_string (make_sep '=') - -let print_rte_ctx_n (ctx: runtime_env) start = - print_myers_list - ctx - (fun (n, vref) -> - let g = !vref in - let _ = - match n with - | (_, Some m) -> lalign_print_string m 12; print_string " | " - | _ -> print_string (make_line ' ' 12); print_string " | " in - - value_print g; print_string "\n") start - -(* Only print user defined variables *) -let print_rte_ctx ctx = - print_rte_ctx_n ctx (!L.builtin_size) - -(* Dump the whole context *) -let dump_rte_ctx ctx = - print_rte_ctx_n ctx 0
===================================== src/eval.ml ===================================== @@ -484,7 +484,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Anormal, Var (vdummy, -1))])) + -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1))])) | _ -> value_fatal loc f "Trying to call a non-function!"
and eval_case ctx i loc target pat dflt = @@ -738,10 +738,9 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons _ -> true (* It's indeed a constructor! *) - | _ -> false + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons _ -> true (* It's indeed a constructor! *) + | _ -> false with Senv_Lookup_Fail _ -> false
let erasable_p name nth ectx = @@ -753,32 +752,33 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> - is_erasable ctors - | _ -> false ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> is_erasable (get_inductive_ctor (get_inductive i)) + | _ -> false) | _ -> false with Senv_Lookup_Fail _ -> false
let erasable_p2 t name ectx = - let is_erasable ctors = match (smap_find_opt t ctors) with - | Some args -> - (List.exists - (fun (k, oname, _) - -> match oname with - | (_, Some n) -> (n = name && k = Aerasable) - | _ -> false) - args) - | _ -> false in + let is_erasable ctors = + match (smap_find_opt t ctors) with + | Some args + -> (List.exists + (fun (k, oname, _) + -> match oname with + | (_, Some n) -> (n = name && k = Aerasable) + | _ -> false) + args) + | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> - is_erasable ctors - | _ -> false ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> is_erasable (get_inductive_ctor (get_inductive i)) + | _ -> false) | _ -> false with Senv_Lookup_Fail _ -> false
@@ -791,12 +791,12 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> - find_nth ctors - | _ -> "_" ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> find_nth (get_inductive_ctor (get_inductive i)) + | _ -> "_") | _ -> "_" with Senv_Lookup_Fail _ -> "_"
@@ -812,12 +812,12 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> - find_arg ctors - | _ -> (-1) ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> find_arg (get_inductive_ctor (get_inductive i)) + | _ -> (-1)) | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)
===================================== src/inverse_subst.ml ===================================== @@ -56,11 +56,11 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: Lexp.subst) : substIR option = - let rec transfo (s: Lexp.subst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: subst) : substIR option = + let rec transfo (s: subst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) - match v with + match lexp_lexp' v with | Var (_, v) -> v | _ -> assert false in @@ -68,15 +68,16 @@ let transfo (s: Lexp.subst) : substIR option = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in match s with - | S.Cons (Var _ as v, s, o) -> - let off_acc = off_acc + o in + | S.Cons (e, s, o) when is_var e + -> let off_acc = off_acc + o in (match transfo s off_acc (idx + 1) imp_cnt with | Some (tail, off, imp) - -> let newVar = shiftVar v off_acc + -> let newVar = shiftVar e off_acc in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off, imp) + else Some (((shiftVar e off_acc), idx)::tail, off, imp) | None -> None) - | S.Cons (Imm (Sexp.Symbol (_, "")), s, o) + | S.Cons (e, s, o) + when pred_imm e (fun s -> Sexp.pred_symbol s (fun n -> n = "")) -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) | S.Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) @@ -93,7 +94,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Lexp.mkVar ((U.dummy_location, None), idx) + mkVar ((U.dummy_location, None), idx)
(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -104,18 +105,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: Lexp.subst): Lexp.subst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: subst): subst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: Lexp.subst) (nbVar: int): Lexp.subst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: subst) (nbVar: int): subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None
@@ -145,7 +146,8 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = let is_identity s = let rec is_identity s acc = match s with - | S.Cons(Var(_, idx), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | S.Cons(e, s1, 0) when pred_var e (fun e -> get_var_db_index e = acc) + -> is_identity s1 (acc + 1) | S.Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0 @@ -154,7 +156,7 @@ let is_identity s =
<code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: Lexp.subst) : Lexp.subst option = +let inverse (s: subst) : subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -182,7 +184,8 @@ let inverse (s: Lexp.subst) : Lexp.subst option = * with non-variables, in which case the "inverse" is ambiguous. *) let rec invertible (s: subst) : bool = match s with | S.Identity _ -> true - | S.Cons (e, s, _) -> (match e with Var _ -> true | _ -> e = impossible) + | S.Cons (e, s, _) + -> (match lexp_lexp' e with Var _ -> true | _ -> e = impossible) && invertible s
exception Not_invertible @@ -193,13 +196,13 @@ let rec lookup_inv_subst (i : db_index) (s : subst) : db_index = match s with | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible | S.Identity o -> i - o - | S.Cons (Var (_, i'), s, o) when i' = i - o - -> (try let i'' = lookup_inv_subst i' s in + | S.Cons (e, s, o) when pred_var e (fun e -> get_var_db_index e = i - o) + -> (try let i'' = lookup_inv_subst (get_var_db_index (get_var e)) s in assert (i'' != 0); raise Ambiguous with Not_invertible -> 0) | S.Cons (e, s, o) - -> assert (match e with Var _ -> true | _ -> e = impossible); + -> assert (match lexp_lexp' e with Var _ -> true | _ -> e = impossible); 1 + lookup_inv_subst (i - o) s
(* When going under a binder, we have the rule @@ -248,7 +251,8 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with * The function presumes that `invertible s` was true. * This can be used like mkSusp/push_susp, but it's not lazy. * This is because it can signal errors Not_invertible or Ambiguous. *) -and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with +and apply_inv_subst (e : lexp) (s : subst) : lexp = + match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s))
===================================== src/lexp.ml ===================================== @@ -60,7 +60,9 @@ module AttributeMap = Map.Make (struct type t = attribute_key let compare = comp
type ltype = lexp and subst = lexp S.subst - and lexp = +(* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) + and lexp = lexp' * int + and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort @@ -150,14 +152,13 @@ type metavar_info = | MVal of lexp (* Exp to which the var is instantiated. *) | MVar of scope_level (* Outermost scope in which the var appears. *) * ltype (* Expected type. *) - (* We'd like to keep the lexp_content in which the type is to be + (* We'd like to keep the lexp_context in which the type is to be * understood, but lexp_context is not yet defined here, * so we just keep the length of the lexp_context. *) * ctx_length type meta_subst = metavar_info U.IMap.t
let dummy_scope_level = 0 -let impossible = Imm Sexp.dummy_epsilon
let builtin_size = ref 0
@@ -169,22 +170,140 @@ let metavar_lookup (id : meta_id) : metavar_info
(********************** Hash-consing **********************)
-(* let hc_table : (lexp, lexp) Hashtbl.t = Hashtbl.create 1000 - * let hc (e : lexp) : lexp = - * try Hashtbl.find hc_table e - * with Not_found -> Hashtbl.add hc_table e e; e *) +(** Hash-consing test ** +* with: Hashtbl.hash / lexp'_hash +* median bucket length: 7 / 7 +* biggest bucket length: 205 / 36 +* found/new lexp entries: - / 2 *) + +let lexp_lexp' (e, h) = e +let lexp_hash (e, h) = h + +(* Hash `Lexp` using combine_hash (lxor) with hash of "sub-lexp". *) +let lexp'_hash (lp : lexp') = + match lp with + | Imm s -> U.combine_hash 1 (Hashtbl.hash s) + | SortLevel l + -> U.combine_hash 2 + (match l with + | SLz -> Hashtbl.hash l + | SLsucc lp -> lexp_hash lp + | SLlub (lp1, lp2) + -> U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) + | Sort (l, s) + -> U.combine_hash 3 (U.combine_hash (Hashtbl.hash l) + (match s with + | Stype lp -> lexp_hash lp + | StypeOmega -> Hashtbl.hash s + | StypeLevel -> Hashtbl.hash s)) + | Builtin (v, t, m) + -> U.combine_hash 4 (U.combine_hash + (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) + (match m with + | Some m -> Hashtbl.hash m + | None -> 404)) + | Var v -> U.combine_hash 5 (Hashtbl.hash v) + | Let (l, ds, e) + -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (U.combine_hashes + (List.map (fun e -> let (n, lp, lt) = e in + (U.combine_hash (Hashtbl.hash n) + (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) + ds)) + (lexp_hash e))) + | Arrow (k, v, t1, l, t2) + -> U.combine_hash 7 (U.combine_hash + (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t1) + (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + | Lambda (k, v, t, e) + -> U.combine_hash 8 (U.combine_hash + (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t) (lexp_hash e))) + | Inductive (l, n, a, cs) + -> U.combine_hash 9 (U.combine_hash + (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) + (U.combine_hash (U.combine_hashes + (List.map (fun e -> let (ak, n, lt) = e in + (U.combine_hash (Hashtbl.hash ak) + (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) + a)) + (Hashtbl.hash cs))) + | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) + | Case (l, e, rt, bs, d) + -> U.combine_hash 11 (U.combine_hash + (U.combine_hash (Hashtbl.hash l) (lexp_hash e)) + (U.combine_hash (lexp_hash rt) (U.combine_hash + (Hashtbl.hash bs) + (match d with + | Some (n, lp) -> U.combine_hash (Hashtbl.hash n) (lexp_hash lp) + | _ -> 0)))) + | Metavar (id, s, v) + -> U.combine_hash 12 (U.combine_hash id + (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) + | Call (e, args) + -> U.combine_hash 13 (U.combine_hash (lexp_hash e) + (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in + (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) + args))) + | Susp (lp, subst) + -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + +(* Equality function for hash table + * using physical equality for "sub-lexp" and compare for `subst`. *) +let hc_eq e1 e2 = + match (lexp_lexp' e1, lexp_lexp' e2) with + | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 + | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 + | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 + | (Imm s1, Imm s2) -> s1 = s2 + | (SortLevel SLz, SortLevel SLz) -> true + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> e1 == e2 + | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) + -> e11 == e12 && e21 == e22 + | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true + | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true + | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 + | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Var (_, i1), Var (_, i2)) -> i1 = i2 + | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && compare s1 s2 = 0 + | (Let (_, defs1, e1), Let (_, defs2, e2)) + -> e1 == e2 && List.for_all2 + (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 + | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + -> ak1 = ak2 && t11 == t12 && t21 == t22 + | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + -> ak1 = ak2 && t1 == t2 && e1 == e2 + | (Call (e1, as1), Call (e2, as2)) + -> e1 == e2 && List.for_all2 + (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 + | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) + -> l1 = l2 && List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2 + && SMap.equal (List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 + | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) + -> e1 == e2 && r1 == r2 && SMap.equal + (fun (_, fields1, e1) (_, fields2, e2) + -> e1 == e2 && List.for_all2 + (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) ctor1 ctor2 + && (match (def1, def2) with + | (Some (_, e1), Some (_, e2)) -> e1 == e2 + | _ -> def1 = def2) + | (Metavar (i1, s1, _), Metavar (i2, s2, _)) + -> i1 = i2 && compare s1 s2 = 0 + | _ -> false
module WHC = Weak.Make (struct type t = lexp - (* Using (=) instead of `compare` results - * in an *enormous* slowdown. Apparently - * `compare` checks == before recursing - * but (=) doesn't? *) - let equal x y = (compare x y = 0) - let hash = Hashtbl.hash - end) + let equal x y = hc_eq x y + let hash = lexp_hash + end) + let hc_table : WHC.t = WHC.create 1000 -let hc : lexp -> lexp = WHC.merge hc_table
+let hc (l : lexp') : lexp = + WHC.merge hc_table (l, lexp'_hash l)
let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) @@ -198,14 +317,16 @@ let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) - = match f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) - | _, [] -> f - | _ -> hc (Call (f, es)) - -and lexp_head e = - match e with +let mkCall (f, es) = + match lexp_lexp' f, es with + | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | _, [] -> f + | _ -> hc (Call (f, es)) + +let impossible = mkImm Sexp.dummy_epsilon + +let lexp_head e = + match lexp_lexp' e with | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" | Let _ -> "let" @@ -222,7 +343,8 @@ and lexp_head e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"
-let mkSLlub' (e1, e2) = match (e1, e2) with +let mkSLlub' (e1, e2) = + match (lexp_lexp' e1, lexp_lexp' e2) with (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l | (SortLevel SLz, _) | (_, SortLevel SLz) @@ -235,11 +357,54 @@ let mkSLlub' (e1, e2) = match (e1, e2) with | _ -> Log.log_fatal ~section:"internal" ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2)
-let mkSLsucc e = match e with - | SortLevel _ | Var _ | Metavar _ | Susp _ - -> SLsucc e - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " - +let mkSLsucc e = + match lexp_lexp' e with + | SortLevel _ | Var _ | Metavar _ | Susp _ + -> SLsucc e + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " + +(********************** Lexp tests ************************) + +let pred_imm l pred = + match lexp_lexp' l with + | Imm s -> pred s + | _ -> false + +let is_imm l = pred_imm l (fun e -> true) + +let pred_var l pred = + match lexp_lexp' l with + | Var v -> pred v + | _ -> false + +let is_var l = pred_var l (fun e -> true) + +let get_var l = + match lexp_lexp' l with + | Var v -> v + | _ -> Log.log_fatal ~section:"internal" "Lexp is not Var " + +let get_var_db_index v = + let (n, idx) = v in idx + +let get_var_vname v = + let (n, idx) = v in n + +let pred_inductive l pred = + match lexp_lexp' l with + | Inductive (l, n, a, cs) -> pred (l, n, a, cs) + | _ -> false + +let get_inductive l = +match lexp_lexp' l with + | Inductive (l, n, a, cs) -> (l, n, a, cs) + | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive " + +let get_inductive_ctor i = + let (l, n, a, cs) = i in cs + +let is_inductive l = pred_inductive l (fun e -> true) + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -274,9 +439,9 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 let rec mkSusp e s = if S.identity_p s then e else (* We apply the substitution eagerly to some terms. - * There's no deep technical rason for that: + * There's no deep technical reason for that: * it just seemed like a good idea to do it eagerly when it's easy. *) - match e with + match lexp_lexp' e with | Imm _ -> e | Builtin _ -> e | Susp (e, s') -> mkSusp_memo e (scompose s' s) @@ -313,7 +478,7 @@ let rec sunshift n = let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))
(* The quick test below seemed to indicate that about 50% of the "sink"s - * are applied on top of another "sink" and hence cound be combined into + * are applied on top of another "sink" and hence could be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify * the complexity of adding a `Lift` to `subst`. *) @@ -338,7 +503,7 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))
let rec lexp_location e = - match e with + match lexp_lexp' e with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e @@ -365,10 +530,10 @@ let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l,n) = (l, maybename n)
let rec push_susp e s = (* Push a suspension one level down. *) - match e with + match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e') -> mkSortLevel (mkSLsucc (mkSusp e' s)) + | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s)) | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) @@ -424,14 +589,15 @@ let rec push_susp e s = (* Push a suspension one level down. *) | (Var _ | Metavar _) -> nosusp (mkSusp e s)
and nosusp e = (* Return `e` with no outermost `Susp`. *) - match e with + match lexp_lexp' e with | Susp(e, s) -> push_susp e s | _ -> e
(* Get rid of `Susp`ensions and instantiated `Metavar`s. *) let clean e = - let rec clean s e = match e with + let rec clean s e = + match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) @@ -468,7 +634,7 @@ let clean e = L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (clean s it, name) + | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) @@ -495,8 +661,8 @@ let stypecons = Symbol (U.dummy_location, "##typecons")
(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = - match lxp with - | Susp _ as e -> lexp_unparse (nosusp e) + match lexp_lexp' lxp with + | Susp _ -> lexp_unparse (nosusp lxp) | Imm (sexp) -> sexp | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) @@ -626,7 +792,7 @@ and subst_string s = match s with -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"
and lexp_name e = - match e with + match lexp_lexp' e with | Imm _ -> lexp_string e | Var _ -> lexp_string e | _ -> lexp_head e @@ -716,7 +882,7 @@ let get_binary_op_name name =
let rec get_precedence expr ctx = let lkp name = SMap.find name (pp_grammar ctx) in - match expr with + match lexp_lexp' expr with | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" @@ -784,14 +950,15 @@ and lexp_str ctx (exp : lexp) : string = let kindp_str k = match k with | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in
- let get_name fname = match fname with + let get_name fname = + match lexp_lexp' fname with | Builtin ((_, name), _, _) -> name, 0 | Var((_, Some name), idx) -> name, idx | Lambda _ -> "__", 0 | Cons _ -> "__", 0 | _ -> "__", -1 in
- match exp with + match lexp_lexp' exp with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) | Integer(_, s) -> tval (string_of_int s) @@ -805,7 +972,7 @@ and lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx e + | MVal e -> lexp_str ctx (push_susp e subst) | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))
| Let (_, decls, body) -> @@ -902,9 +1069,6 @@ and lexp_str ctx (exp : lexp) : string =
| Builtin ((_, name), _, _) -> "##" ^ name
- | Sort (_, Stype (SortLevel SLz)) -> "##Type" - | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" - | Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")" | Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω"
@@ -913,6 +1077,14 @@ and lexp_str ctx (exp : lexp) : string = | SortLevel (SLlub (e1, e2)) -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"
+ | Sort (_, Stype l) + -> match lexp_lexp' l with + | SortLevel SLz -> "##Type" + | SortLevel (SLsucc lp) + when (match lexp_lexp' lp with SortLevel SLz -> true | _ -> false) + -> "##Type1" + | _ -> "(##Type_ " ^ lexp_string l ^ ")" + and lexp_str_ctor ctx ctors =
let pretty = pp_pretty ctx in @@ -947,11 +1119,8 @@ and lexp_str_decls ctx decls =
let rec eq e1 e2 = e1 == e2 || - match (e1, e2) with - | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 - | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 - | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 - | (Imm s1, Imm s2) -> s1 = s2 + match (lexp_lexp' e1, lexp_lexp' e2) with + | (Imm s1, Imm s2) -> sexp_equal s1 s2 | (SortLevel SLz, SortLevel SLz) -> true | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) @@ -961,39 +1130,45 @@ let rec eq e1 e2 = | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 - | (Susp (e1, s1), e2) -> eq (push_susp e1 s1) e2 - | (e1, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) + | (Susp (e1, s1), _) -> eq (push_susp e1 s1) e2 + | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) | (Let (_, defs1, e1), Let (_, defs2, e2)) - -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) - -> eq t1 t2 && eq e1 e2) - defs1 defs2 + -> eq e1 e2 && List.for_all2 + (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2) defs1 defs2 | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) -> ak1 = ak2 && eq t11 t12 && eq t21 t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && eq t1 t2 && eq e1 e2 | (Call (e1, as1), Call (e2, as2)) - -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) - as1 as2 - | (Inductive (_, l1, as1, cases1), Inductive (_, l2, as2, cases2)) - -> l1 = l2 - && List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) - as1 as2 - && SMap.equal (List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) - -> ak1 = ak2 && eq e1 e2)) - cases1 cases2 + -> eq e1 e2 && List.for_all2 + (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 + | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) + -> l1 = l2 && List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 + && SMap.equal (List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 - | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) - -> eq e1 e2 && eq r1 r2 - && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) - -> eq e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) - -> ak1 = ak2) - fields1 fields2) - cases1 cases2 + | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) + -> eq e1 e2 && eq r1 r2 && SMap.equal + (fun (_, fields1, e1) (_, fields2, e2) -> eq e1 e2 && List.for_all2 + (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) ctor1 ctor2 && (match (def1, def2) with - | (Some (_, e1), Some (_, e2)) -> eq e1 e2 - | _ -> def1 = def2) + | (Some (_, e1), Some (_, e2)) -> eq e1 e2 + | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) - -> i1 = i2 && subst_eq s1 s2 + -> if i1 == i2 then subst_eq s1 s2 else + (match (metavar_lookup i1, metavar_lookup i2) with + | (MVal l, _) -> eq (push_susp l s1) e2 + | (_, MVal l) -> eq e1 (push_susp l s2) + | _ -> false) + | (Metavar (i1, s1, _), _) + -> (match metavar_lookup i1 with + | MVal l -> eq (push_susp l s1) e2 + | _ -> false) + | (_, Metavar (i2, s2, _)) + -> (match metavar_lookup i2 with + | MVal l -> eq e1 (push_susp l s2) + | _ -> false) | _ -> false
and subst_eq s1 s2 = @@ -1012,4 +1187,3 @@ and subst_eq s1 s2 = eq e1 (mkSusp e2 (S.shift o)) && subst_eq s1 (S.mkShift s2 o) | _ -> false -
===================================== src/opslexp.ml ===================================== @@ -132,78 +132,88 @@ let lexp_close lctx e = * 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 lexp_whnf e (ctx : DB.lexp_context) : lexp = - let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = - match e with + +let lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = + match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf e' ctx) - | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - | Call (e, []) -> lexp_whnf e ctx + | Some e' -> lexp_whnf_aux e' ctx) + | Susp (e, s) -> lexp_whnf_aux (push_susp e s) ctx + | Call (e, []) -> lexp_whnf_aux e ctx | Call (f, (((_, arg)::args) as xs)) -> - (match lexp_whnf f ctx with + (match lexp_lexp' (lexp_whnf_aux f ctx) with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx)), args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf e ctx in - let reduce name aargs = + let e' = lexp_whnf_aux e ctx in + let reduce it name aargs = + let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive (_,_,fargs,_) -> fargs + | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left - (fun (s,d) (_, arg) -> - (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s, - d + 1)) - (S.identity, 0) + (fun (s, targs) (_, arg) -> + match targs with + | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) + | _targ::targs -> + (* Ignore the type arguments *) + (s, targs)) + (S.identity, targs) aargs in - lexp_whnf (push_susp branch subst) ctx + lexp_whnf_aux (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf (push_susp default (S.substitute e')) ctx + -> lexp_whnf_aux (push_susp default (S.substitute e')) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in - (match e' with - | Cons (_, (_, name)) -> reduce name [] + (match lexp_lexp' e' with + | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> - (match lexp_whnf f ctx with - | Cons (_, (_, name)) -> reduce name aargs + (match lexp_lexp' (lexp_whnf_aux f ctx) with + | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> lexp_whnf (push_susp e s) ctx + | MVal e -> lexp_whnf_aux (push_susp e s) ctx | _ -> e)
(* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> lexp_whnf (push_susp body (lexp_defs_subst l S.identity defs)) ctx + -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs)) ctx
- | e -> e + | elem -> e
- in lexp_whnf e ctx + in lexp_whnf_aux e ctx
+let lexp'_whnf e (ctx : DB.lexp_context) : lexp' = + lexp_lexp' (lexp_whnf_aux e ctx) + +let lexp_whnf e (ctx : DB.lexp_context) : lexp = + lexp_whnf_aux e ctx
(** A very naive implementation of sets of pairs of lexps. *) type set_plexp = (lexp * lexp) list let set_empty : set_plexp = [] let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool - = assert (e1 == Lexp.hc e1); - assert (e2 == Lexp.hc e2); - try let _ = List.find (fun (e1', e2') + = try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s in true @@ -230,7 +240,8 @@ let level_canon e = let o = try IMap.find v m with Not_found -> -1 in if o < d then (c, IMap.add v d m) else acc in
- let rec canon e d ((c,m) as acc) = match e with + let rec canon e d ((c,m) as acc) = + match lexp_lexp' e with | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) @@ -259,7 +270,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = if changed && set_member_p vs e1' e2' then true else let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in - match (e1', e2') with + match (lexp_lexp' e1', lexp_lexp' e2') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 @@ -332,14 +343,16 @@ let conv_p (ctx : DB.lexp_context) e1 e2 (********* Testing if a lexp is properly typed *********)
let rec mkSLlub ctx e1 e2 = - match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with + let lwhnf1 = lexp_whnf e1 ctx in + let lwhnf2 = lexp_whnf e2 ctx in + match (lexp_lexp' lwhnf1, lexp_lexp' lwhnf2) with | (SortLevel SLz, _) -> e2 | (_, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon e1' in - let ce2 = level_canon e2' in + -> let ce1 = level_canon lwhnf1 in + let ce2 = level_canon lwhnf2 in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) @@ -353,7 +366,9 @@ type sort_compose_result let sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen * if `v` is a TypeLevel. *) - match (lexp_whnf k1 ctx1, lexp_whnf k2 ctx2) with + let lwhnf1 = lexp'_whnf k1 ctx1 in + let lwhnf2 = lexp'_whnf k2 ctx2 in + match (lwhnf1, lwhnf2) with | (Sort (_, s1), Sort (_, s2)) -> (match s1, s2 with | (Stype l1, Stype l2) @@ -408,7 +423,7 @@ let nerased_let defs erased = * will be non-erasable, so in `let x = z; y = x ...` * where `z` is erasable, `x` will be found * to be erasable, but not `y`. *) - match e with Var (_, idx) -> DB.set_mem idx nerased + match lexp_lexp' e with Var (_, idx) -> DB.set_mem idx nerased | _ -> false) defs in if not (List.mem true es) then nerased else @@ -430,14 +445,13 @@ let rec check'' erased ctx e = (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in - (match lexp_whnf s ctx with - | Sort _ -> () - | _ -> error_tc ~loc:(lexp_location t) - ("Not a proper type: " ^ lexp_string t)); - (* FIXME: return the `sort` rather than the surrounding `lexp`! *) - s in - - match e with + (match lexp'_whnf s ctx with + | Sort _ -> () + | _ -> error_tc ~loc:(lexp_location t) + ("Not a proper type: " ^ lexp_string t)); + (* FIXME: return the `sort` rather than the surrounding `lexp`! *) + s in + match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string @@ -528,7 +542,7 @@ let rec check'' erased ctx e = (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in - match lexp_whnf ft ctx with + match lexp'_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (error_tc ~loc:(lexp_location arg) @@ -551,8 +565,8 @@ let rec check'' erased ctx e = let (level, _, _, _) = List.fold_left (fun (level, ictx, erased, n) (ak, v, t) -> - ((match lexp_whnf (check_type erased ictx t) - ictx with + ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -570,7 +584,7 @@ let rec check'' erased ctx e = ("Field type " ^ lexp_string t ^ " is not a Type! (" - ^ lexp_string tt ^")"); + ^ lexp_string lwhnf ^")"); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -590,12 +604,13 @@ let rec check'' erased ctx e = tct | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) - -> let call_split e = match e with + -> let call_split e = + match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in - (match lexp_whnf it ctx, aargs with + (match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -644,8 +659,8 @@ let rec check'' erased ctx e = | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx with - | Inductive (l, _, fargs, constructors) + -> (match lexp'_whnf t ctx with + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -732,7 +747,8 @@ let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)
let rec fv (e : lexp) : (DB.set * mv_set) = - let fv' e = match e with + let fv' e = + match lexp_lexp' e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty | SortLevel (SLsucc e) -> fv e @@ -807,7 +823,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (* This should never signal any warning/error. *)
let rec get_type ctx e = - match e with + match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string @@ -838,7 +854,7 @@ let rec get_type ctx e = -> let ft = get_type ctx f in List.fold_left (fun ft (ak,arg) - -> match lexp_whnf ft ctx with + -> match lexp'_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) @@ -854,7 +870,7 @@ let rec get_type ctx e = let (level, _, _) = List.fold_left (fun (level, ictx, n) (ak, v, t) -> - ((match lexp_whnf (get_type ictx t) ictx with + ((match lexp'_whnf (get_type ictx t) ictx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -878,7 +894,7 @@ let rec get_type ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx with + -> (match lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in @@ -911,9 +927,8 @@ let rec get_type ctx e =
(*********** Type erasure, before evaluation. *****************)
-let rec erase_type (lxp: L.lexp): E.elexp = - - match lxp with +let rec erase_type (lxp: lexp): E.elexp = + match lexp_lexp' lxp with | L.Imm(s) -> E.Imm(s) | L.Builtin(v, _, _) -> E.Builtin(v) | L.Var(v) -> E.Var(v) @@ -943,7 +958,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | Metavar (idx, s, _) + | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) | MVar (_, t, _) @@ -1004,7 +1019,8 @@ let ctx2tup ctx nctx = let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) - Call (Cons (Inductive (loc, type_label, [], + + mkCall (mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, @@ -1024,10 +1040,10 @@ let ctx2tup ctx nctx = -> (P.Aimplicit, mkVar (oname, offset - i - 1))) types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> Let (loc, [(name, mkSusp e (S.shift 1), t)], + -> mkLet (loc, [(name, mkSusp e (S.shift 1), t)], mk_lets_and_tup blocs ((name, t) :: types)) | (DB.CVfix (defs, _) :: blocs) - -> Let (loc, defs, + -> mkLet (loc, defs, mk_lets_and_tup blocs (List.append (List.rev (List.map (fun (oname, _, t)
===================================== src/sexp.ml ===================================== @@ -45,6 +45,15 @@ type token = sexp let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location
+(********************** Sexp tests **********************) + +let pred_symbol s pred = + match s with + | Symbol (_, n) -> pred n + | _ -> false + +let is_symbol e = pred_symbol e (fun e -> true) + (**************** Hash-consing symbols *********************)
module SHash = Hashtbl.Make (struct type t = string @@ -160,13 +169,18 @@ let rec sexp_parse (g : grammar) (rest : sexp list) mk_node ((l,"")::op) largs rargs true), rest) | (Some ll, None) when ll > level - (* A closer without matching opener. - * It might simply be a postfix symbol that binds very tightly. - * We currently signal an error because it's more common for - * it to be a closer with missing opener. *) - -> sexp_error l ("Lonely postfix/closer ""^name^"""); - sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] + (* A closer without matching opener or a postfix symbol + that binds very tightly. Previously, we signaled an + error (assuming the former), but it prevented the use + tightly binding postfix operators. + + For example, it signaled spurious errors when parsing + expressions with a tightly binding postfix # operator + that implemented record construction by taking an + inductive as argument and returning the inductive's only + constructor. *) + -> sexp_parse rest' level op largs + [mk_node [(l,name);(l,"")] [] rargs true] | (Some ll, Some rl) when ll > level (* A new infix which binds more tightly, i.e. does not close * the current `op' but takes its `rargs' instead. *)
===================================== src/unification.ml ===================================== @@ -61,7 +61,8 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error "Checking occurrence of an instantiated metavar!!" | MVar (sl, _, _) - -> let rec oi e = match e with + -> let rec oi e = + match lexp_lexp' e with | Imm _ -> false | SortLevel SLz -> false | SortLevel (SLsucc e) -> oi e @@ -189,21 +190,21 @@ and unify' (e1: lexp) (e2: lexp) let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in - match (e1', e2') with + match (lexp_lexp' e1', lexp_lexp' e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l - | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> unify_call r l ctx vs' + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' + | (_, Call _) -> unify_call e2' e1' ctx vs' (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> unify_lambda l r ctx vs' - | (Call _ as l, r) -> unify_call l r ctx vs' + | (Arrow _ , _) -> unify_arrow e1' e2' ctx vs' + | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' + | (Call _, _) -> unify_call e1' e2' ctx vs' (* | (Case _ as l, r) -> unify_case l r subst *) (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _ as l, r) -> unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' + | (Sort _, _) -> unify_sort e1' e2' ctx vs' + | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -227,7 +228,7 @@ and unify' (e1: lexp) (e2: lexp) *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = - match (arrow, lxp) with + match (lexp_lexp' arrow, lexp_lexp' lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 @@ -250,7 +251,7 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs - Lambda , lexp -> unify lexp lambda subst *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - match (lambda, lxp) with + match (lexp_lexp' lambda, lexp_lexp' lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 @@ -300,7 +301,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in - match lxp2 with + match lexp_lexp' lxp2 with | Metavar (idx2, s2, name) -> if idx = idx2 then match common_subset ctx s1 s2 with @@ -370,7 +371,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) *) and unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = - match (call, lxp) with + match (lexp_lexp' call, lexp_lexp' lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) @@ -439,7 +440,7 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, _ -> ERROR *) and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - match sortlvl, lxp with + match lexp_lexp' sortlvl, lexp_lexp' lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs @@ -456,7 +457,7 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - Sort, lexp -> ERROR *) and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = - match sort_, lxp with + match lexp_lexp' sort_, lexp_lexp' lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs | StypeOmega, StypeOmega -> []
===================================== src/util.ml ===================================== @@ -45,6 +45,15 @@ type vref = vname * db_index
type bottom = | B_o_t_t_o_m_ of bottom
+let get_vname_name_option vname = + let (loc, name) = vname in name + +let get_vname_name vname = + let (loc, name) = vname in + match name with + | Some n -> n + | _ -> "" (* FIXME: Replace with dummy_name ? *) + (* print debug info *) let loc_string loc = "Ln " ^ (Fmt.ralign_int loc.line 3) ^ ", cl " ^ (Fmt.ralign_int loc.column 3) @@ -116,3 +125,22 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = match opt with | None -> None | Some x -> Some (fn x) + +(* It seemed good to use the prime number 31. + * FIXME: Pick another one ? *) +let combine_hash e1 e2 = (e1 * 31) lxor e2 + +let rec combine_hashes li = + match li with + | [] -> 31 + | e :: l -> combine_hash (e * 31) (combine_hashes l) + +let get_stats_hashtbl stats = + let (tl, ne, sumb, smallb, medianb, bigb) = stats in + Printf.printf "\n\ttable length: %i\n + number of entries: %i\n + sum of bucket lengths: %i\n + smallest bucket length: %i\n + median bucket length: %i\n + biggest bucket length: %i\n" + tl ne sumb smallb medianb bigb
===================================== tests/elab_test.ml ===================================== @@ -51,8 +51,24 @@ let generate_tests (name: string) (test input_gen fmt tester)
(* let input = "y = lambda x -> x + 1;" *) -let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; -res = id 3;" +let inputs = + [("identity", {| +id = lambda (α : Type) ≡> lambda (x : α) -> x; +res = id 3; + |}); + ("whnf of case", {| +Box = (typecons (Box (l : TypeLevel) (t : Type_ l)) (box t)); +box = (datacons Box box); +unbox b = ##case_ (b | box inside => inside); +alwaysbool b = ##case_ (b | box _ => Bool); + +example1 : unbox (box (lambda x -> Bool)) 1; +example1 = true; + +example2 : alwaysbool (box Int); +example2 = true; + |}); + ]
let generate_lexp_from_str str = List.hd ((fun (lst, _) -> @@ -63,9 +79,22 @@ let generate_lexp_from_str str =
let _ = generate_tests "TYPECHECK" - (fun () -> [generate_lexp_from_str input]) - (fun x -> List.map lexp_string x) - (fun x -> (x, true)) + (fun () -> inputs) + (fun x -> x) + (fun (name, input) -> + let result = + try + let ectx = Elab.default_ectx in + let pres = Prelexer.prelex_string input in + let sxps = Lexer.lex Grammar.default_stt pres in + let _lxps, _ectx = Elab.lexp_p_decls [] sxps ectx in + Log.stop_on_error(); + true + with + | Log.Stop_Compilation _ -> (Log.print_and_clear_log (); false) + | Log.Internal_error _ -> (Log.print_and_clear_log (); false) in + (name, result) + )
let lctx = Elab.default_ectx (* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () ->
===================================== tests/unify_test.ml ===================================== @@ -125,14 +125,14 @@ let input_type_t = generate_ltype_from_str str_type2
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
- ( Lambda ((Anormal), + ( mkLambda ((Anormal), (Util.dummy_location, Some "L1"), - Var((Util.dummy_location, Some "z"), 3), - Imm (Integer (Util.dummy_location, 3))), - Lambda ((Anormal), + mkVar((Util.dummy_location, Some "z"), 3), + mkImm (Integer (Util.dummy_location, 3))), + mkLambda ((Anormal), (Util.dummy_location, Some "L2"), - Var((Util.dummy_location, Some "z"), 4), - Imm (Integer (Util.dummy_location, 3))), Nothing ) + mkVar((Util.dummy_location, Some "z"), 4), + mkImm (Integer (Util.dummy_location, 3))), Nothing )
::(input_induct , input_induct , Equivalent) (* 2 *) ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) @@ -183,8 +183,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
::(input_type , input_type_t , Equivalent) (* 44 *)
- ::(Metavar (0, S.identity, (Util.dummy_location, Some "M")), - Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *) + ::(mkMetavar (0, S.identity, (Util.dummy_location, Some "M")), + mkVar ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)
::[]
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/1eb77aa201478f48c70d015b9d5b2b427...