Typer Octobre 2022

typer@iro.umontreal.ca

1 participants
6 discussions

[Git][monnier/typer] Pushed new branch ja-perf
by Jean-Alexandre Barszcz (＠jabarszcz) 12 Oct '22

12 Oct '22

Jean-Alexandre Barszcz pushed new branch ja-perf at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/ja-perf You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][location-sinfo] lctx_lookup/print_lexp_ctx
by Ismaila FALL (＠Fallismaila) 10 Oct '22

10 Oct '22

Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: 28d2df4e by Fallismaila at 2022-10-10T22:07:49+00:00 lctx_lookup/print_lexp_ctx - - - - - 9 changed files: - + - + _) - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/heuristic.ml - src/opslexp.ml - src/subst.ml - + winehq.key Changes: ===================================== ===================================== @@ -0,0 +1,140 @@ +src/builtin.ml: = ref (SMap.add "Macro" impossible SMap.empty) +src/builtin.ml: = predef_map := SMap.add name lexp (!predef_map) +src/builtin.ml:let dloc = DB.dloc +src/builtin.ml: = let map = !lmap in +src/debruijn.ml:let dloc = dummy_location +src/debruijn.ml:let level1 = mkSortLevel (mkSLsucc level0) +src/debruijn.ml:let level2 = mkSortLevel (mkSLsucc level1) +src/debruijn.ml:let type0 = mkSort (dsinfo, Stype level0) +src/debruijn.ml:let type1 = mkSort (dsinfo, Stype level1) +src/debruijn.ml:let type2 = mkSort (dsinfo, Stype level2) +src/debruijn.ml: = scope_level (* Integer identifying a level. *) +src/debruijn.ml: = (ltype * lctx_length) list (* the list of type classes *) +src/debruijn.ml: = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx +src/debruijn.ml: = let (_, (n, _), lctx, _, _) = ctx in +src/debruijn.ml: = sl +src/debruijn.ml: = get_size ectx - slen +src/debruijn.ml: = (Grammar.default_grammar, empty_senv, empty_lctx, +src/debruijn.ml:let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = +src/debug.ml: * = 32 *) +src/elab.ml: = newMetavar ctx sl (loc, Some "τ") +src/elab.ml: = try +src/elab.ml: = List.fold_right (fun (l,e,t) (o', defs) +src/elab.ml: = List.fold_right (fun (ak, v, t) (o', args) +src/elab.ml: = SMap.map +src/elab.ml: = List.fold_right +src/elab.ml: = SMap.map +src/elab.ml: = let arg = match aty with +src/elab.ml: = List.fold_right +src/elab.ml: = List.fold_right +src/elab.ml: let usr_lctx = ectx_to_lctx usr_elctx in +src/elab.ml: let ld_lctx = ectx_to_lctx ld_elctx in +src/elab.ml: let usr_len = M.length usr_lctx in +src/elab.ml: let dflt_len = M.length dflt_lctx in +src/elab.ml: = try let _ = register_special_forms () in +src/eval.ml:let make_symbol loc _depth args_val = match args_val with +src/eval.ml:let make_string loc _depth args_val = match args_val with +src/eval.ml:let make_float loc _depth args_val = match args_val with +src/eval.ml:let make_block loc _depth args_val = match args_val with +src/eval.ml: let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) +src/eval.ml: = Hashtbl.Make +src/eval.ml: = List.fold_left (fun (rctx, evs, alldefs) (loname, e, _) +src/fmt.ml:let red = "\x1b[31m" +src/fmt.ml:let green = "\x1b[32m" +src/fmt.ml:let yellow = "\x1b[33m" +src/fmt.ml:let cyan = "\x1b[36m" +src/fmt.ml:let reset = "\x1b[0m" +src/heuristic.ml: = List.map (fun (_kind, ((l,oname) as name)) +src/instargs.ml: = U.IMap.find_opt id (!metavar_resolution_contexts) +src/instargs.ml: = (* First, check that there is only one possible resolution context +src/instargs.ml: = Impossible (* Unification (matching) failed with impossible constraints *) +src/inverse_subst.ml: * X[σ] = e ==> X[σ][σ⁻¹] = e[σ⁻¹] +src/inverse_subst.ml: -> let size = imp_cnt + sizeOf cons_lst in +src/inverse_subst.ml: "Subst-inversion-bug: %s ∘ %s == %s !!\n" +src/inverse_subst.ml: = match s with +src/inverse_subst.ml: * (λe)[s] ==> λ(e[lift s]) +src/inverse_subst.ml: * (λe)[s⁻¹] ==> λ(e[s'⁻¹]) +src/inverse_subst.ml: = if n = 0 then s else +src/inverse_subst.ml: = L.fold_left (fun (s,ndefs) (v, def, ty) +src/inverse_subst.ml: = L.fold_left (fun (s, nargs) (ak, v, t) +src/inverse_subst.ml: = L.fold_left (fun (s, nargs) (ak, v, t) +src/lexp.ml: = try U.IMap.find id (!metavar_table) +src/lexp.ml:let mkImm s = hc (Imm s) +src/lexp.ml:let mkSortLevel l = hc (SortLevel l) +src/lexp.ml:let mkSort (l, s) = hc (Sort (l, s)) +src/lexp.ml:let mkBuiltin (v, t) = hc (Builtin (v, t)) +src/lexp.ml:let mkVar v = hc (Var v) +src/lexp.ml:let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) +src/lexp.ml:let mkLet (l, ds, e) = hc (Let (l, ds, e)) +src/lexp.ml:let mkArrow (l, k, v, t1, t2) = hc (Arrow (l, k, v, t1, t2)) +src/lexp.ml:let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +src/lexp.ml:let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) +src/lexp.ml:let mkCons (t, n) = hc (Cons (t, n)) +src/lexp.ml:let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) +src/lexp.ml:let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) +src/lexp.ml: * = τ[(e₃[(e₂[e₁/x])/y,e₁/x])/z,(e₂[e₁/x])/y,e₁/x] +src/lexp.ml: = if Hashtbl.mem hcs_table (e, s) +src/lexp.ml: = L.fold_left (fun (s, nargs) (ak, v, t) +src/lexp.ml: = L.fold_left (fun (s, nargs) (ak, v, t) +src/lexp.ml: = List.map (fun (_kind, ((l,oname) as name)) +src/lexp.ml:and lexp_cprint ctx e = print_string (lexp_cstring ctx e) +src/lexp.ml: let inter_ctx = add_indent ctx 1 in +src/lexp.ml: let lexp_str' = lexp_str ctx in +src/lexp.ml: let color = pp_color ctx in +src/lexp.ml: let isize = pp_size ctx in +src/lexp.ml: let red = if color then red else "" in +src/lexp.ml: let green = if color then green else "" in +src/lexp.ml: let yellow = if color then yellow else "" in +src/lexp.ml: let cyan = if color then cyan else "" in +src/lexp.ml: let reset = if color then reset else "" in +src/lexp.ml: let keyword str = magenta ^ str ^ reset in +src/lexp.ml: let error str = red ^ str ^ reset in +src/lexp.ml: let tval str = yellow ^ str ^ reset in +src/lexp.ml: = List.fold_left +src/lexp.ml: = List.fold_left (fun str v +src/opslexp.ml: = SortResult of ltype +src/opslexp.ml: = Hashtbl.Make +src/opslexp.ml: = ref (SMap.empty : (DB.lexp_context +src/opslexp.ml:let lookup_type = DB.lctx_lookup_type +src/opslexp.ml: = List.fold_left +src/opslexp.ml: = try let _ = List.find (fun (e1', e2') +src/opslexp.ml: = (* assert (not (set_member_p s e1 e2)); *) +src/opslexp.ml: = List.map (let s = S.shift n in +src/opslexp.ml: = if e1 == e2 then true +src/opslexp.ml: = SMap.fold +src/opslexp.ml: = (IMap.merge (fun _m oss1 oss2 +src/opslexp.ml: = (ss1, ss2) in +src/opslexp.ml: = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) +src/opslexp.ml: = List.fold_left (fun (fvs, o) (_, e, t) +src/opslexp.ml: = List.fold_left (fun s (_, _, t) +src/opslexp.ml: = SMap.fold +src/opslexp.ml: = SMap.fold +src/sexp.ml: = if empty_args_are_not_args then +src/source.ml: = +src/subst.ml: * #i[s] ==> lookup i s +src/subst.ml: * (e₁ e₂)[s] ==> (e₁[s]) (e₂[s]) +src/subst.ml: * (λ e)[s] ==> λ(e[#0 · (s ↑1)]) +src/subst.ml: * e[s₁][s₂] ==> e[s₁ ∘ s₂] +src/subst.ml: * (λ e₁) e₂ ==> e₁[e₂·id] +src/subst.ml: * (s ↑n₂) ↑n₁ ==> s ↑(n₁+n₂) {part of m1} +src/subst.ml: * s₁ ∘ id ==> s₁ {m2} +src/subst.ml: * s₁ ∘ s₂ ↑n ==> (s₁ ∘ s₂) ↑n {part of m1} +src/subst.ml: * id ∘ s ==> s {m3} +src/subst.ml: * s₁ ↑n ∘ e·s₂ ==> s₁ ↑(n-1) ∘ s₂ {m4 & m5} +src/subst.ml: * e·s₁ ∘ s₂ ==> (e[s₂])·(s₁ ∘ s₂) {m6} +src/unification.ml: = let idx = !global_last_metavar + 1 in +src/unification.ml: = create_metavar_1 sl t (Myers.length ctx) +src/unification.ml:type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list +src/unification.ml: * ?a[0 => x, 1 => y, 2 => z, ...] =?= ?a[0 => x, 1 => b, 2 => z, ...] +src/unification.ml: = match matching with +src/unification.ml: * ^ "\n =\n " +src/unification.ml: * ^ "\n =\n " +src/unification.ml: * ^ "\n =\n " +src/unification.ml: = if not (List.length args1 == List.length args2) then +src/unification.ml: = unif_formals ctx vs args1 args2 in +src/util.ml: = Char.code c < 128 || Char.code c >= 192 +tests/elab_test.ml:no = datacons Decidable no; +tests/elab_test.ml: | true => no (p := false≠true) +tests/utest_lib.ml:let expect_equal_bool = _expect_equal_t Bool.equal string_of_bool +tests/utest_lib.ml:let expect_equal_int = _expect_equal_t Int.equal string_of_int +tests/utest_lib.ml:let expect_equal_str = _expect_equal_t String.equal (fun g -> g) ===================================== _) ===================================== ===================================== src/REPL.ml ===================================== @@ -131,6 +131,7 @@ let eval_interactive grammar used in subsequent declarations. *) let sexps = sexp_parse_all_to_list (ectx_get_grammar ectx) tokens (Some ";") in + (* printf "\n"; printf "********************************************************************** \n"; printf "**************** REPL --> eval_interactive --> sexps ***************** \n"; @@ -139,6 +140,7 @@ let eval_interactive List.iter (fun sexp -> print_string "\n"; print_string " "; sexp_print sexp) sexps; printf "\n"; printf "\n"; + *) let decls, exprs = classify_sexps sexps in @@ -152,6 +154,7 @@ let eval_interactive Elab.resolve_instances_and_generalize ctx lxp Elab.wrapLambda lxp in let lexprs = List.map (generalize_lexp ectx') lexprs in + (* printf "\n"; printf "********************************************************************** \n"; printf "**************** REPL --> eval_interactive --> lexprs **************** \n"; @@ -161,7 +164,7 @@ let eval_interactive let ty = (OL.check (ectx_to_lctx ectx') lexpr) in print_string "\n"; lexp_print ty; print_string "\n"; print_string "\n"; ) lexprs; - + *) List.iter interactive#process_decls ldecls; Log.print_log (); ===================================== src/debruijn.ml ===================================== @@ -40,6 +40,8 @@ open Sexp open Lexp +open Pexp + module M = Myers open Fmt @@ -365,6 +367,142 @@ let ectx_set_inst_def (ectx : elab_context) (inst_def : bool) : elab_context = let (tcs, _, insts) = ectx_to_tcctx ectx in ectx_set_tcctx (tcs, inst_def, insts) ectx +let rec heuristic_unparse lxp = + match lexp_lexp' lxp with + | Susp _ + -> heuristic_unparse (nosusp lxp) + | Imm (sexp) + -> sexp + | Builtin ((l,name), _) + -> Symbol (l, "##" ^ name) + | Var ((loc, name), _db_index) + -> Symbol (sexp_location loc, maybename name) + | Proj (l,lxp,(loc,str)) + -> Node (Symbol (sexp_location l, "__.__"), + [(heuristic_unparse lxp);(Symbol (loc,str))]) + | Cons (t, (l, name)) + -> Node (sdatacons, + [heuristic_unparse t; Symbol (l, name)]) + | Lambda (kind, vdef, ltp, body) + -> let l = lexp_location lxp in + let st = heuristic_unparse ltp in + (match kind with + | Aerasable -> heuristic_unparse body + | Anormal -> Node (Symbol (l, "lambda_->_"), + [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); + heuristic_unparse body]) + | Aimplicit -> heuristic_unparse body + ) + + | Arrow (loc, arg_kind, (l, oname), ltp1, ltp2) + -> let ut1 = heuristic_unparse ltp1 in + (match arg_kind with + | Aerasable -> heuristic_unparse (mkSusp ltp2 (S.substitute (mkMetavar (-1, S.identity, (l, oname))))); + | Anormal -> Node (Symbol (sexp_location loc, "_->_"), + [(match oname with + | None -> ut1 + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); + heuristic_unparse ltp2]) + | Aimplicit -> heuristic_unparse (mkSusp ltp2 (S.substitute (mkMetavar (-1, S.identity, (l, oname))))); + ) + + | Let (loc, ldecls, body) + -> (* (vdef * lexp * ltype) list *) + let sdecls = List.fold_left + (fun acc (vdef, lxp, ltp) + -> Node (Symbol (lexp_location lxp, "_=_"), + [Symbol (sname vdef); heuristic_unparse ltp]) + :: Node (Symbol (lexp_location lxp, "_=_"), + [Symbol (sname vdef); heuristic_unparse lxp]) + :: acc) + [] ldecls in + Node (Symbol (sexp_location loc, "let_in_"), + [Node (Symbol (sexp_location loc, "_;_"), sdecls); + heuristic_unparse body]) + + | Call (_loc, lxp, largs) + -> (* (arg_kind * lexp) list *) + let fargs = List.filter ( fun (kind, _) -> kind = Anormal ) largs in + let sargs = List.map ( fun (_, elem) -> heuristic_unparse elem ) fargs in + Node (heuristic_unparse lxp, sargs) + + | Inductive (loc, label, lfargs, ctors) + -> (* (arg_kind * vdef * ltype) list *) + (* (arg_kind * pvar * pexp option) list *) + let pfargs = List.map (fun (kind, vdef, ltp) -> + (kind, sname vdef, Some (heuristic_unparse ltp))) lfargs in + + Node (stypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map + (fun (name, types) + -> Node (Symbol (sexp_location loc, name), + List.map + (fun arg -> + match arg with + | (Anormal, (_,None), t) -> heuristic_unparse t + | (ak, s, t) + -> let (l,_) as id = sname s in + Node (Symbol (l, match ak with + | Anormal -> "_:_" + | Aimplicit -> "_::_" + | Aerasable -> "_:::_"), + [Symbol id; heuristic_unparse t])) + types)) + (SMap.bindings ctors)) + + | Case (loc, target, bltp, branches, default) + -> let bt = heuristic_unparse bltp in + let pbranch = List.map (fun (str, (loc, args, bch)) -> + match args with + | [] -> Ppatsym (loc, Some str), heuristic_unparse bch + | _ -> + let pat_args + = List.map (fun (_kind, ((l,oname) as name)) + -> match oname with + | Some vdef -> (Some (sexp_location l,vdef), name) + | None -> (None, name)) + args + (* FIXME: Rather than a Pcons we'd like to refer to an existing + * binding with that value! *) + in (Ppatcons (Node (sdatacons, + [bt; Symbol (sexp_location loc, str)]), + pat_args), + heuristic_unparse bch) + ) (SMap.bindings branches) in + + let pbranch = match default with + | Some (v,dft) -> (Ppatsym v, + heuristic_unparse dft)::pbranch + | None -> pbranch + in let e = heuristic_unparse target in + Node (Symbol (sexp_location loc, "case_"), + e :: List.map + (fun (pat, branch) -> + Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), + [pexp_u_pat pat; branch])) + pbranch) + + (* FIXME: The cases below are all broken! *) + | Metavar (_idx, _subst, (loc, name)) + -> Symbol (sexp_location loc, "?" ^ (maybename name)) + | SortLevel (SLz) + -> Symbol (U.dummy_location, "##TypeLevel.z") + | SortLevel (SLsucc l) + -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), + [heuristic_unparse l]) + | SortLevel (SLlub (l1, l2)) + -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + [heuristic_unparse l1; heuristic_unparse l2]) + | Sort (l, StypeOmega) + -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) + -> Symbol (sexp_location l, "##TypeLevel.Sort") + | Sort (_l, Stype sl) + -> Node (Symbol (lexp_location sl, "##Type_"), + [heuristic_unparse sl]) + let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = print_string (make_title " LEXP CONTEXT "); ===================================== src/elab.ml ===================================== @@ -197,7 +197,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = "Exception while conversion-checking types: %s and %s" (lexp_string ltype) (lexp_string ltype'); - raise e) + raise e) then elab_check_proper_type ctx ltype var else ===================================== src/heuristic.ml ===================================== @@ -1,12 +1,18 @@ open Lexp open Sexp -open Pexp open Debruijn module OL = Opslexp +module S = Subst +module BI = Builtin + +(* + * open Pexp +*) (* ugly printing (sexp_print (pexp_unparse (heuristic_unparse e))) *) +(* let rec heuristic_unparse lxp = match lexp_lexp' lxp with | Susp _ @@ -15,11 +21,8 @@ let rec heuristic_unparse lxp = -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) - | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) - (* - -> let s = maybename name in - if s = "ℓ" then Symbol (sexp_location loc, "") else Symbol (sexp_location loc, maybename name) - *) + | Var ((loc, name), _db_index) + -> Symbol (sexp_location loc, maybename name) | Proj (l,lxp,(loc,str)) -> Node (Symbol (sexp_location l, "__.__"), [(heuristic_unparse lxp);(Symbol (loc,str))]) @@ -29,34 +32,25 @@ let rec heuristic_unparse lxp = | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = heuristic_unparse ltp in - Node (Symbol (l, match kind with - | Anormal -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); - heuristic_unparse body]) + (match kind with + | Aerasable -> heuristic_unparse body + | Anormal -> Node (Symbol (l, "lambda_->_"), + [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); + heuristic_unparse body]) + | Aimplicit -> heuristic_unparse body + ) | Arrow (loc, arg_kind, (l, oname), ltp1, ltp2) -> let ut1 = heuristic_unparse ltp1 in (match arg_kind with - | Aerasable -> Node (Symbol (sexp_location loc, "_≡>_"), - [(match oname with - | None -> ut1 - | Some v -> Node (Symbol (sexp_location l, "_:_"), - [Symbol (sexp_location l,v); Symbol (sexp_location l, "?")])); - heuristic_unparse ltp2]) + | Aerasable -> heuristic_unparse (mkSusp ltp2 (S.substitute (mkMetavar (-1, S.identity, (l, oname))))); | Anormal -> Node (Symbol (sexp_location loc, "_->_"), [(match oname with | None -> ut1 | Some v -> Node (Symbol (sexp_location l, "_:_"), [Symbol (sexp_location l,v); ut1])); heuristic_unparse ltp2]) - | Aimplicit -> Node (Symbol (sexp_location loc, "_=>_"), - [(match oname with - | None -> ut1 (* Inverse_subst.dsinfo *) - | Some v -> Node (Symbol (sexp_location l, "_:_"), - [Symbol (sexp_location l,v); ut1])); - heuristic_unparse ltp2]) + | Aimplicit -> heuristic_unparse (mkSusp ltp2 (S.substitute (mkMetavar (-1, S.identity, (l, oname))))); ) | Let (loc, ldecls, body) @@ -73,12 +67,13 @@ let rec heuristic_unparse lxp = [Node (Symbol (sexp_location loc, "_;_"), sdecls); heuristic_unparse body]) - | Call(_, lxp, largs) + | Call (_loc, lxp, largs) -> (* (arg_kind * lexp) list *) - let sargs = List.map (fun (_kind, elem) -> heuristic_unparse elem) largs in - Node (heuristic_unparse lxp, sargs) + let fargs = List.filter ( fun (kind, _) -> kind = Anormal ) largs in + let sargs = List.map ( fun (_, elem) -> heuristic_unparse elem ) fargs in + Node (heuristic_unparse lxp, sargs) - | Inductive(loc, label, lfargs, ctors) + | Inductive (loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) (* (arg_kind * pvar * pexp option) list *) let pfargs = List.map (fun (kind, vdef, ltp) -> @@ -136,9 +131,8 @@ let rec heuristic_unparse lxp = pbranch) (* FIXME: The cases below are all broken! *) - | Metavar (idx, subst, (loc, name)) - -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]") + | Metavar (_idx, _subst, (loc, name)) + -> Symbol (sexp_location loc, "?" ^ (maybename name)) | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) @@ -154,24 +148,25 @@ let rec heuristic_unparse lxp = | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [heuristic_unparse sl]) - +*) let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = print_string (Fmt.make_title " LEXP CONTEXT "); Fmt.make_rheader - [(Some ('l', 10), "NAME"); - (Some ('l', 10), "LEXP_UNPARSE"); - (Some ('l', 20), "LEXP"); - (Some ('l', 42), " TYPE")]; + [ + (Some ('l', 10), "NAME"); + (Some ('l', 10), "LEXP_UNPARSE"); + (Some ('l', 42), " TYPE") + ]; print_string (Fmt.make_sep '-'); - let _ = " | | " in + let _prefix = " | " in let print i = try - let _, name, _lexp, ty = + let _r, name, _lexp, ty = match env_lookup_by_index i (ectx_to_lctx ctx) with | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty | ((_, name), _, ty) -> 0, name, None, ty @@ -183,23 +178,45 @@ let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = String.sub name' 0 9 ^ "…" else name' in - Printf.printf " %-10s || " short_name; - let res = heuristic_unparse ty in - sexp_print res; + Printf.printf " | %-10s | " short_name; + print_newline (); + let se = heuristic_unparse ty in + sexp_print se; + print_newline (); - Printf.printf " |-->|: "; + let le = Elab.infer_and_generalize_type ctx se (se, name) in + lexp_print le; + print_newline (); - let s = fst (Elab.elaborate ctx res None) in - lexp_print s; - (* - Printf.printf " |--> "; + if (try OL.conv_p (ectx_to_lctx ctx) ty le + with + | e + -> Elab.info + ~print_action:(Elab.lexp_print_details ty) + ~loc:(sexp_location se) + "Exception while conversion-checking types: %s and %s" + (lexp_string ty) + (lexp_string le); + raise e) + then + print_string "PPPAAARRRFFFAAAIIITTT PPPAAARRRFFFAAAIIITTT PPPAAARRRFFFAAAIIITTT !!!" + else + fatal + ~print_action:(fun _ -> + List.iter Elab.print_indent_line [ + (match (se, name) with (_, Some n) -> n | _ -> "<anon>") + ^ " = " ^ lexp_string ty ^ " !: " ^ lexp_string ty; + " because"; + lexp_string le ^ " != " ^ lexp_string ty + ]) + ~loc:(sexp_location se) + "Type check error: ¡¡ctx_define error!!" - lexp_print ty; print_newline (); - *) - print_newline () + print_newline (); + with | Not_found -> print_endline " | %-7d | Not_found |" ===================================== src/opslexp.ml ===================================== @@ -1102,7 +1102,6 @@ and get_type ctx e = | Var (((_, _name), _idx) as v) -> lookup_type ctx v | Proj (l, e, (loc, label)) -> ( - let call_split e = match lexp_lexp' e with | Call (_l, f, args) -> (f, args) ===================================== src/subst.ml ===================================== @@ -201,10 +201,6 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) in compose_cons o1 s2 0 in compose' s1 s2 -(* Adjust a substitution for use under one more binder. - * I.e. take a substitution from Δs to Δₜ and return a substitution - * from Δs,x to Δₜ,x. - * Also known as `lift`. *) let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = cons (mkVar l 0) (mkShift s 1) ===================================== winehq.key ===================================== @@ -0,0 +1,53 @@ +-----BEGIN PGP PUBLIC KEY BLOCK----- + +mQGNBFwOmrgBDAC9FZW3dFpew1hwDaqRfdQQ1ABcmOYu1NKZHwYjd+bGvcR2LRGe +R5dfRqG1Uc/5r6CPCMvnWxFprymkqKEADn8eFn+aCnPx03HrhA+lNEbciPfTHylt +NTTuRua7YpJIgEOjhXUbxXxnvF8fhUf5NJpJg6H6fPQARUW+5M//BlVgwn2jhzlW +U+uwgeJthhiuTXkls9Yo3EoJzmkUih+ABZgvaiBpr7GZRw9GO1aucITct0YDNTVX +KA6el78/udi5GZSCKT94yY9ArN4W6NiOFCLV7MU5d6qMjwGFhfg46NBv9nqpGinK +3NDjqCevKouhtKl2J+nr3Ju3Spzuv6Iex7tsOqt+XdZCoY+8+dy3G5zbJwBYsMiS +rTNF55PHtBH1S0QK5OoN2UR1ie/aURAyAFEMhTzvFB2B2v7C0IKIOmYMEG+DPMs9 +FQs/vZ1UnAQgWk02ZiPryoHfjFO80+XYMrdWN+RSo5q9ODClloaKXjqI/aWLGirm +KXw2R8tz31go3NMAEQEAAbQnV2luZUhRIHBhY2thZ2VzIDx3aW5lLWRldmVsQHdp +bmVocS5vcmc+iQHOBBMBCgA4AhsDBQsJCAcCBhUKCQgLAgQWAgMBAh4BAheAFiEE +1D9kAUU2nFHXht3qdvGiD/mHZy8FAlwOmyUACgkQdvGiD/mHZy/zkwv7B+nKFlDY +Bzz/7j0gqIODbs5FRZRtuf/IuPP3vZdWlNfAW/VyaLtVLJCM/mmaf/O6/gJ+D+E9 +BBoSmHdHzBBOQHIj5IbRedynNcHT5qXsdBeU2ZPR50sdE+jmukvw3Wa5JijoDgUu +LGLGtU48Z3JsBXQ54OlnTZXQ2SMFhRUa10JANXSJQ+QY2Wo2Pi2+MEAHcrd71A2S +0mT2DQSSBQ92c6WPfUpOSBawd8P0ipT7rVFNLJh8HVQGyEWxPl8ecDEHoVfG2rdV +D0ADbNLx9031UUwpUicO6vW/2Ec7c3VNG1cpOtyNTw/lEgvsXOh3GQs/DvFvMy/h +QzaeF3Qq6cAPlKuxieJe4lLYFBTmCAT4iB1J8oeFs4G7ScfZH4+4NBe3VGoeCD/M +Wl+qxntAroblxiFuqtPJg+NKZYWBzkptJNhnrBxcBnRinGZLw2k/GR/qPMgsR2L4 +cP+OUuka+R2gp9oDVTZTyMowz+ROIxnEijF50pkj2VBFRB02rfiMp7q6iQIzBBAB +CgAdFiEE2iNXmnTUrZr50/lFzvrI6q8XUZ0FAlwOm3AACgkQzvrI6q8XUZ3KKg/+ +MD8CgvLiHEX90fXQ23RZQRm2J21w3gxdIen/N8yJVIbK7NIgYhgWfGWsGQedtM7D +hMwUlDSRb4rWy9vrXBaiZoF3+nK9AcLvPChkZz28U59Jft6/l0gVrykey/ERU7EV +w1Ie1eRu0tRSXsKvMZyQH8897iHZ7uqoJgyk8U8CvSW+V80yqLB2M8Tk8ECZq34f +HqUIGs4Wo0UZh0vV4+dEQHBh1BYpmmWl+UPf7nzNwFWXu/EpjVhkExRqTnkEJ+Ai +OxbtrRn6ETKzpV4DjyifqQF639bMIem7DRRf+mkcrAXetvWkUkE76e3E9KLvETCZ +l4SBfgqSZs2vNngmpX6Qnoh883aFo5ZgVN3v6uTS+LgTwMt/XlnDQ7+Zw+ehCZ2R +CO21Y9Kbw6ZEWls/8srZdCQ2LxnyeyQeIzsLnqT/waGjQj35i4exzYeWpojVDb3r +tvvOALYGVlSYqZXIALTx2/tHXKLHyrn1C0VgHRnl+hwv7U49f7RvfQXpx47YQN/C +PWrpbG69wlKuJptr+olbyoKAWfl+UzoO8vLMo5njWQNAoAwh1H8aFUVNyhtbkRuq +l0kpy1Cmcq8uo6taK9lvYp8jak7eV8lHSSiGUKTAovNTwfZG2JboGV4/qLDUKvpa +lPp2xVpF9MzA8VlXTOzLpSyIVxZnPTpL+xR5P9WQjMS5AY0EXA6auAEMAMReKL89 +0z0SL+/i/geB/agfG/k6AXiG2a9kVWeIjAqFwHKl9W/DTNvOqCDgAt51oiHGRRjt +1Xm3XZD4p+GM1uZWn9qIFL49Gt5x94TqdrsKTVCJr0Kazn2mKQc7aja0zac+WtZG +OFn7KbniuAcwtC780cyikfmmExLI1/Vjg+NiMlMtZfpK6FIW+ulPiDQPdzIhVppx +w9/KlR2Fvh4TbzDsUqkFQSSAFdQ65BWgvzLpZHdKO/ILpDkThLbipjtvbBv/pHKM +O/NFTNoYkJ3cNW/kfcynwV+4AcKwdRz2A3Mez+g5TKFYPZROIbayOo01yTMLfz2p +jcqki/t4PACtwFOhkAs+MYPPyZDUkTFcEJQCPDstkAgmJWI3K2qELtDOLQyps3WY +Mfp+mntOdc8bKjFTMcCEk1zcm14K4Oms+w6dw2UnYsX1FAYYhPm8HUYwE4kP8M+D +9HGLMjLqqF/kanlCFZs5Avx3mDSAx6zS8vtNdGh+64oDNk4x4A2j8GTUuQARAQAB +iQG8BBgBCgAmFiEE1D9kAUU2nFHXht3qdvGiD/mHZy8FAlwOmrgCGwwFCQPCZwAA +CgkQdvGiD/mHZy9FnAwAgfUkxsO53Pm2iaHhtF4+BUc8MNJj64Jvm1tghr6PBRtM +hpbvvN8SSOFwYIsS+2BMsJ2ldox4zMYhuvBcgNUlix0G0Z7h1MjftDdsLFi1DNv2 +J9dJ9LdpWdiZbyg4Sy7WakIZ/VvH1Znd89Imo7kCScRdXTjIw2yCkotE5lK7A6Ns +NbVuoYEN+dbGioF4csYehnjTdojwF/19mHFxrXkdDZ/V6ZYFIFxEsxL8FEuyI4+o +LC3DFSA4+QAFdkjGFXqFPlaEJxWt5d7wk0y+tt68v+ulkJ900BvR+OOMqQURwrAi +iP3I28aRrMjZYwyqHl8i/qyIv+WRakoDKV+wWteR5DmRAPHmX2vnlPlCmY8ysR6J +2jUAfuDFVu4/qzJe6vw5tmPJMdfvy0W5oogX6sEdin5M5w2b3WrN8nXZcjbWymqP +6jCdl6eoCCkKNOIbr/MMSkd2KqAqDVM5cnnlQ7q+AXzwNpj3RGJVoBxbS0nn9JWY +QNQrWh9rAcMIGT+b1le0 +=4lsa +-----END PGP PUBLIC KEY BLOCK----- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/28d2df4e8fec99a8e219843f8206fe9d1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/28d2df4e8fec99a8e219843f8206fe9d1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch wop-server
by Stefan (＠monnier) 07 Oct '22

07 Oct '22

Stefan deleted branch wop-server at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] * src/lexp.ml (push_susp): Don't call `mkSLlub'` with suspensions
by Stefan (＠monnier) 07 Oct '22

07 Oct '22

Stefan pushed to branch main at Stefan / Typer Commits: bf851a68 by Stefan Monnier at 2022-10-07T19:23:48-04:00 * src/lexp.ml (push_susp): Don't call `mkSLlub'` with suspensions (mkSLlub'): Improve error message ever so slightly - - - - - 1 changed file: - src/lexp.ml Changes: ===================================== src/lexp.ml ===================================== @@ -356,8 +356,8 @@ 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) - -> Log.log_fatal ~section:"internal" "lub of SLz" + | (SortLevel SLz, e) | (e, SortLevel SLz) + -> Log.log_fatal ~section:"internal" "lub of SLz with %S" (lexp_head (hc e)) | (SortLevel (SLsucc _), SortLevel (SLsucc _)) -> Log.log_fatal ~section:"internal" "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), @@ -554,7 +554,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | SortLevel (SLz) -> e | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s)) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) + -> mkSortLevel (mkSLlub' (push_susp e1 s, push_susp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (_, _) -> e | Builtin _ -> e View it on GitLab: https://gitlab.com/monnier/typer/-/commit/bf851a685972478e08e8011862cfa7135… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/bf851a685972478e08e8011862cfa7135… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch tp/ift6172-2021
by Stefan (＠monnier) 03 Oct '22

03 Oct '22

Stefan deleted branch tp/ift6172-2021 at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch tp/ift6172
by Stefan (＠monnier) 03 Oct '22

03 Oct '22

Stefan pushed new branch tp/ift6172 at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/tp/ift6172 You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Octobre 2022