mailman.iro.umontreal.ca
Sign In
Sign Up
Sign In
Sign Up
Manage this list
×
Keyboard Shortcuts
Thread View
j
: Next unread message
k
: Previous unread message
j a
: Jump to all threads
j l
: Jump to MailingList overview
2026
March
February
January
2025
December
November
October
September
August
July
June
May
April
March
February
January
2024
December
November
October
September
August
July
June
May
April
March
February
January
2023
December
November
October
September
August
July
June
May
April
March
February
January
2022
December
November
October
September
August
July
June
May
April
March
February
January
2021
December
November
October
September
August
July
June
May
April
March
February
January
2020
December
November
October
September
August
July
June
May
April
March
February
January
2019
December
November
October
September
August
July
June
May
April
March
February
January
2018
December
November
October
September
August
July
June
May
April
March
February
January
2017
December
November
October
September
August
July
June
May
April
March
February
January
2016
December
November
October
September
August
July
June
May
April
March
February
List overview
Download
Typer
October 2022
----- 2026 -----
March 2026
February 2026
January 2026
----- 2025 -----
December 2025
November 2025
October 2025
September 2025
August 2025
July 2025
June 2025
May 2025
April 2025
March 2025
February 2025
January 2025
----- 2024 -----
December 2024
November 2024
October 2024
September 2024
August 2024
July 2024
June 2024
May 2024
April 2024
March 2024
February 2024
January 2024
----- 2023 -----
December 2023
November 2023
October 2023
September 2023
August 2023
July 2023
June 2023
May 2023
April 2023
March 2023
February 2023
January 2023
----- 2022 -----
December 2022
November 2022
October 2022
September 2022
August 2022
July 2022
June 2022
May 2022
April 2022
March 2022
February 2022
January 2022
----- 2021 -----
December 2021
November 2021
October 2021
September 2021
August 2021
July 2021
June 2021
May 2021
April 2021
March 2021
February 2021
January 2021
----- 2020 -----
December 2020
November 2020
October 2020
September 2020
August 2020
July 2020
June 2020
May 2020
April 2020
March 2020
February 2020
January 2020
----- 2019 -----
December 2019
November 2019
October 2019
September 2019
August 2019
July 2019
June 2019
May 2019
April 2019
March 2019
February 2019
January 2019
----- 2018 -----
December 2018
November 2018
October 2018
September 2018
August 2018
July 2018
June 2018
May 2018
April 2018
March 2018
February 2018
January 2018
----- 2017 -----
December 2017
November 2017
October 2017
September 2017
August 2017
July 2017
June 2017
May 2017
April 2017
March 2017
February 2017
January 2017
----- 2016 -----
December 2016
November 2016
October 2016
September 2016
August 2016
July 2016
June 2016
May 2016
April 2016
March 2016
February 2016
typer@iro.umontreal.ca
1 participants
6 discussions
Start a n
N
ew thread
[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
0
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
0
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
0
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
0
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
0
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
0
0
Results per page:
10
25
50
100
200