Typer Novembre 2022

typer@iro.umontreal.ca

1 participants
4 discussions

[Git][monnier/typer][main] * src/opslexp.ml (conv_p'): Make sure fold_left2 gets args of eq length
by Stefan (＠monnier) 16 Nov '22

16 Nov '22

Stefan pushed to branch main at Stefan / Typer Commits: 272e5346 by Stefan Monnier at 2022-11-16T12:48:06-05:00 * src/opslexp.ml (conv_p'): Make sure fold_left2 gets args of eq length - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -398,7 +398,8 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> eqp && ak1 = ak2 && (conv_erase && ak1 = P.Aerasable || conv_p t1 t2)) true args1 args2 in - conv_p f1 f2 && conv_arglist_p args1 args2 + List.length args1 == List.length.args2 + && conv_p f1 f2 && conv_arglist_p args1 args2 | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) -> let rec conv_fields ctx vs fields1 fields2 = match fields1, fields2 with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/272e5346f0e77a4c2d22c4ae2ac2e55fc… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/272e5346f0e77a4c2d22c4ae2ac2e55fc… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][location-sinfo] heuristic.ml
by Ismaila FALL (＠Fallismaila) 10 Nov '22

10 Nov '22

Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: a1461ffe by Fallismaila at 2022-11-10T19:11:39+00:00 heuristic.ml - - - - - 6 changed files: - src/debruijn.ml - src/elab.ml - src/eval.ml - src/heuristic.ml - src/lexp.ml - src/opslexp.ml Changes: ===================================== src/debruijn.ml ===================================== @@ -367,142 +367,6 @@ 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 ===================================== @@ -735,7 +735,7 @@ and infer_type pexp ectx (var: vname) = t and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dsinfo, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (lexp_sinfo body, decls, lxp)) declss body and unify_with_arrow ctx tloc lxp kind var aty @@ -773,7 +773,8 @@ and unify_or_error lctx lxp ?lxp_name expect actual = (lexp_string actual) (lexp_string t1) (lexp_string t2); - assert (not (OL.conv_p lctx expect actual)) +(* Log.print_log (); + assert (not (OL.conv_p lctx expect actual)) *) | [] -> () (* This is a crucial function: take an expression `e` of type `inferred_t` @@ -1111,7 +1112,7 @@ and lexp_parse_inductive ctors ctx = acc impossible in let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t _l e - -> mkArrow (lexp_sinfo e, Aerasable, vname, t, e)) + -> mkArrow (lexp_sinfo altacc, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1187,7 +1188,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - let value = EV.eval_call (sexp_location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) + let value = EV.eval_call (sexp_location loc) (EL.Var ((loc, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd @@ -1331,7 +1332,7 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (stp, + -> let ltp = infer_and_generalize_type nctx stp (epsilon (loc), Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) @@ -1353,7 +1354,7 @@ and lexp_decls_1 pending_defs then (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (stp, Some vname) ForwardRef ltp) + else recur [] (ectx_extend nctx (epsilon (loc), Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ @@ -1365,13 +1366,13 @@ and lexp_decls_1 | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((l, vname)); sexp] + | [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 = (epsilon (l), Some vname) in + let var = (sexp, 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, @@ -1639,7 +1640,7 @@ let sform_identifier ctx loc sargs ot = (sexp_error l {|Invalid special identifier "%s"|} name; sform_dummy_ret ctx loc) - | [Symbol (_loc, name)] + | [Symbol (_, name)] when String.length name >= 1 && String.get name 0 = '?' -> let name = if name = "?" then "" else string_sub name 1 (String.length name) in @@ -1663,8 +1664,8 @@ let sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" - ^^ " repeated at a different scope level!") + (error ~loc:(sexp_location loc) "Bug in the elaboration of a metavar repeated at a different scope level!"; + sform_dummy_ret ctx loc) | MVal _ -> (* FIXME: We face the same problem as above, but here, the situation is worse, we don't even know the scope ===================================== src/eval.ml ===================================== @@ -558,7 +558,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 (dsinfo, e, [(Anormal, mkVar (vdummy, -1))])) + -> Vtype (L.mkCall (lexp_sinfo e, e, [(Anormal, mkVar (vdummy, -1))])) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) and eval_case ctx i loc target pat dflt = ===================================== src/heuristic.ml ===================================== @@ -1,156 +1,168 @@ open Lexp open Sexp -open Debruijn +open Pexp +module DB = Debruijn +module Unif = Unification module OL = Opslexp module S = Subst module BI = Builtin +module M = Myers +module Ps = Positivity -(* - * open Pexp -*) - - -(* ugly printing (sexp_print (pexp_unparse (heuristic_unparse e))) *) -(* -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)) + +let mkMetavar_1 name = + let meta = Unif.create_metavar_1 (-437) impossible (-1) in + mkMetavar (meta, S.identity, name) + +(* ugly printing (sexp_pri +nt (pexp_unparse (heuristic_unparse e))) *) +let heuristic_unparse cf lxp = + let rec loop lxp = + if cf 2 == 42 then lexp_sinfo lxp + else + match lexp_lexp' lxp with + | Susp _ + -> loop (nosusp lxp) + | Imm (sexp) + -> sexp + | Builtin ((l,name), _) + -> Symbol (l, "##" ^ name) + | Var ((loc, name), _) + -> Symbol (sexp_location loc, maybename name) + | Proj (l,lxp,(loc,str)) + -> Node (Symbol (sexp_location l, "__.__"), + [(loop lxp);(Symbol (loc,str))]) + | Cons (t, (l, name)) + -> Node (sdatacons, + [loop t; Symbol (l, name)]) + + | Lambda (kind, vdef, ltp, body) + -> let l = lexp_location lxp in + let st = loop ltp in + if kind != Anormal && cf 2 == 0 + then loop body + else Node (Symbol (l, match kind with + | Anormal -> "##lambda_->_" + | Aimplicit -> "##lambda_=>_" + | Aerasable -> "##lambda_≡>_"), + [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); + loop body]) + + | Arrow (loc, arg_kind, (l, oname), ltp1, ltp2) + -> let ut1 = loop ltp1 in + if arg_kind != Anormal && cf 2 == 0 + then loop (mkSusp ltp2 (S.substitute (mkMetavar_1 (l, oname)))) + else Node (Symbol (sexp_location loc, match arg_kind with + | Anormal -> "_->_" + | Aimplicit -> "_=>_" + | Aerasable -> "_≡>_"), + [(match oname with None -> ut1 + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); + loop ltp2]) + + | 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); loop ltp]) + :: Node (Symbol (lexp_location lxp, "_=_"), + [Symbol (sname vdef); loop lxp]) + :: acc) + [] ldecls in + Node (Symbol (sexp_location loc, "##let_in_"), + [Node (Symbol (sexp_location loc, "_;_"), sdecls); + loop body]) + + | Call (_, lxp, largs) + -> (* (arg_kind * lexp) list *) + let fargs = List.filter ( fun (kind, _) -> if cf 2 == 0 then kind = Anormal else kind != Anormal ) largs in + let sargs = List.map ( fun (_, elem) -> loop elem) fargs in + Node (loop 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 (loop 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) -> loop t + | (ak, s, t) + -> let (l,_) as id = sname s in + Node (Symbol (l, match ak with + | Anormal -> "_:_" + | Aimplicit -> "_::_" + | Aerasable -> "_:::_"), + [Symbol id; loop 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_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = + | Case (loc, target, bltp, branches, default) + -> let bt = loop bltp in + let pbranch = List.map (fun (str, (loc, args, bch)) -> + match args with + | [] -> Ppatsym (loc, Some str), loop 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), + loop bch) + ) (SMap.bindings branches) in + + let pbranch = match default with + | Some (v,dft) -> (Ppatsym v, + loop dft)::pbranch + | None -> pbranch + in let e = loop 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)) + -> (match metavar_lookup idx with + | MVal e -> loop (push_susp e subst) + | _ -> Symbol (sexp_location loc, "?" ^ (maybename name)) + ) + | SortLevel (SLz) + -> Symbol (U.dummy_location, "##TypeLevel_z") + | SortLevel (SLsucc l) + -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), + [loop l]) + | SortLevel (SLlub (l1, l2)) + -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + [loop l1; loop 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_"), + [loop sl]) + in loop lxp + + +let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) = print_string (Fmt.make_title " LEXP CONTEXT "); Fmt.make_rheader @@ -162,15 +174,16 @@ let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = print_string (Fmt.make_sep '-'); - let _prefix = " | " in + let _ = " | " in let print i = try let _r, name, _lexp, ty = - match env_lookup_by_index i (ectx_to_lctx ctx) with + match DB.env_lookup_by_index i (DB.ectx_to_lctx ctx) with | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty | ((_, name), _, ty) -> 0, name, None, ty in + let ty = mkSusp ty (S.shift (i + 1)) in let name' = maybename name in let short_name = if String.length name' > 10 @@ -182,37 +195,162 @@ let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = Printf.printf " | %-10s | " short_name; print_newline (); - let se = heuristic_unparse ty in - sexp_print se; - print_newline (); + lexp_print ty; + print_newline(); - let le = Elab.infer_and_generalize_type ctx se (se, name) in - lexp_print le; - print_newline (); + let generate_population (le : lexp) n : sexp list = + let pop = ref [] in + for i = 1 to n do + let s = heuristic_unparse (fun _ -> Random.int i) le in + pop := s :: !pop + done; + !pop + in - if (try OL.conv_p (ectx_to_lctx ctx) ty le + let fitness (s : sexp) : bool = + let le = ( + try Elab.infer_and_generalize_type ctx s (s, name) 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!!" + | e -> + raise e + ) in + OL.conv_p (DB.ectx_to_lctx ctx) ty le + in + + let size (s : sexp) : int = + let counter = ref 0 in + let rec loop s = + match s with + | Node (_, args) -> counter := !counter + 1; + List.iter ( + fun e -> loop e + ) args; + | _ -> counter := !counter + 1 + in loop s; + !counter + in + + let best_sexp (ss : sexp list) : sexp = + let res = List.filter (fun e -> fitness e == true) ss in + let s = ref DB.dsinfo in + let min = ref 0 in + List.iter ( + fun e -> + if (size (e) < !min) + then min := size (e); s := e; + ) res; + !s; + in + + let max_sexp (ss : sexp list) : sexp = + let s = ref DB.dsinfo in + let max = ref 0 in + List.iter ( + fun e -> + if (size (e) > !max) + then s := e; max := size (e); + ) ss; + !s; + in + + let _min_sexp res = + let s = ref DB.dsinfo in + let min = ref 0 in + List.iter ( + fun e -> + if (size (e) < !min) + then s := e; min := size (e); + ) res; + !s + in + + let select_sexp (ss : sexp list) : sexp list = + let res = ref [] in + List.iter ( + fun e -> + if (size(e) > 15) + then res := e :: !res + ) ss; + !res + in + + let crossover (s1: sexp) (s2 : sexp) : sexp = + let cross1 s1 s2 = + match s1, s2 with + | Node (s1, ss1), Node (s2, ss2) + -> Node ((if Random.bool () then s1 else s2), + let rec crosslist ss1 ss2 = + match ss1, ss2 with + | (e1 :: ss1), (e2 :: ss2) + -> (if Random.bool () then e2 else e1) :: crosslist ss1 ss2 + | _ -> if Random.bool () then ss1 else ss2 + in crosslist ss1 ss2 + ) + | _ -> if Random.bool () then s1 else s2 + in + let _cross2 s1 s2 = + match s1, s2 with + | Node (s1, ss1), Node (s2, ss2) + -> Node ((if Random.bool () then s1 else s2), + if Random.bool () + then s1 :: ss1 + else s2 :: ss2 + ) + | _ -> if Random.bool () then s1 else s2 + in + + if Random.bool () + then cross1 s1 s2 + else cross1 s1 s2 + in + + let generate_parent (ss : sexp list) : sexp list = + let se = select_sexp ss in + let res = ref [] in + for _i = 1 to (List.length ss) do + let s1 = List.nth se (Random.int (List.length se)) in + sexp_print s1; print_newline (); + let s2 = List.nth ss (Random.int (List.length ss)) in + sexp_print s2; print_newline (); + let s = crossover s1 s2 in res := s :: !res; + sexp_print s; + print_newline (); + print_newline (); + done; + !res + in + + + let algorithm lexp = + let loop ss = + let res = ref [] in + for _i = 1 to 20 do + let se = generate_parent ss in + let s = best_sexp se in + if s <> DB.dsinfo then + res := s :: !res + else + res := (max_sexp ss) :: !res; + done; + !res + in + + let pop = generate_population lexp 10 in + let s = best_sexp pop in + if s <> DB.dsinfo then + sexp_print s + else + let res = loop pop in + let se = best_sexp res in + if se <> DB.dsinfo then + sexp_print se + else + print_string " crossover --> "; sexp_print (max_sexp res); + in + + + algorithm ty; + print_newline (); print_newline (); @@ -241,9 +379,9 @@ let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = print_string (Fmt.make_sep '=') (* Only print user defined variables *) -let print_heur_ctx (lctx : elab_context) : unit = - print_heur_ctx_n lctx [(0, M.length (ectx_to_lctx lctx) - !builtin_size)] +let print_heur_ctx (lctx : DB.elab_context) : unit = + print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx) - !builtin_size)] (* Dump the whole context *) -let dump_heur_ctx (lctx : elab_context) : unit = - print_heur_ctx_n lctx [(0, M.length (ectx_to_lctx lctx))] +let dump_heur_ctx (lctx : DB.elab_context) : unit = + print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx))] ===================================== src/lexp.ml ===================================== @@ -324,7 +324,7 @@ let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) 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 mkMetavar (n, s, v) = assert (n >= 0); hc (Metavar (n, s, v)) let mkCall (l, f, es) = match lexp_lexp' f, es with | Call (l, f', es'), _ -> hc (Call (l, f', es' @ es)) @@ -519,23 +519,22 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) let rec lexp_sinfo s = match lexp_lexp' s with | Sort (l,_) -> l - | SortLevel (SLsucc s) -> lexp_sinfo s - | SortLevel (SLlub (s, _)) -> lexp_sinfo s + | SortLevel (SLsucc l) -> lexp_sinfo l + | SortLevel (SLlub (l, _)) -> lexp_sinfo l | SortLevel SLz -> dummy_sinfo | Imm s -> s - | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> epsilon l - | Let (l,_,_) -> l - | Arrow (l,_,_,_,_) -> l - | Lambda (_,(l,_),_,_) -> l - | Call (_,f,_) -> lexp_sinfo f - | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> epsilon l - | Case (l,_,_,_,_) -> l - | Susp (s, _) -> lexp_sinfo s - (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> l - | Proj (l,_,_) -> l + | Var ((s,_),_) -> s + | Builtin ((loc, _), _) -> epsilon loc + | Let (s,_,_) -> s + | Arrow (s,_,_,_,_) -> s + | Lambda (_,(s,_),_,_) -> s + | Call (s,_,_) -> s + | Inductive (s,_,_,_) -> s + | Cons (l,_) -> lexp_sinfo l + | Case (s,_,_,_,_) -> s + | Susp (l, _) -> lexp_sinfo l + | Metavar (_,_,(s,_)) -> s + | Proj (s,_,_) -> s let lexp_location e = @@ -1021,7 +1020,7 @@ and lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) - | Arrow(_loc, k, (_, Some name), tp, expr) -> + | Arrow(_, k, (_, Some name), tp, expr) -> "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str' expr) @@ -1029,7 +1028,7 @@ and lexp_str ctx (exp : lexp) : string = "(" ^ (lexp_str' tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" - | Lambda(k, (_loc, name), ltype, lbody) -> + | Lambda(k, (_, name), ltype, lbody) -> let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ ===================================== src/opslexp.ml ===================================== @@ -1101,52 +1101,52 @@ and get_type ctx e = | Sort (_, StypeOmega) -> DB.sort_omega | 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) - | _ -> (e,[]) in - let etype = lexp_whnf (get_type ctx e) ctx in - let it, aargs = call_split etype in - match lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors = 1 - -> let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(sexp_location l) - "Wrong arg number to inductive type!"; s) in - let s = mksubst S.identity fargs aargs in - let (_,fieldtypes) = List.hd (SMap.bindings constructors) in - let rec getfieldtype s (fieldtypes - : (arg_kind * vname * ltype) list) = - match fieldtypes with - | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" - label; - etype - | (ak, (_, Some fn), ftype)::_ when fn = label - (* We found our field! *) - -> if not (ak = Aerasable) - then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(sexp_location l) - "Can't Proj an erasable field: %s" label; - Lexp.impossible) - | (_, vdef, _)::fieldtypes - -> let fvdef vdef e loc lbl = - match vdef with - |(_, Some _) -> mkProj (loc, e, lbl) - |_ -> Lexp.impossible in - let fieldref = fvdef vdef e l (loc, label) in - getfieldtype (S.cons fieldref s) fieldtypes in - getfieldtype s fieldtypes - | Inductive _, _ - -> Log.log_error ~loc:(sexp_location l) - "Proj on an inductive type that's not a tuple!"; - etype - | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; - etype) + -> ( + let call_split e = + match lexp_lexp' e with + | Call (_l, f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (get_type ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:(sexp_location l) + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes + : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" + label; + etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if not (ak = Aerasable) + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:(sexp_location l) + "Can't Proj an erasable field: %s" label; + Lexp.impossible) + | (_, vdef, _)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(_, Some _) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:(sexp_location l) + "Proj on an inductive type that's not a tuple!"; + etype + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; + etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a1461ffe5326270999f6782632608d103… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a1461ffe5326270999f6782632608d103… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][ja-refl] 16 commits: Add Zarith dependency to opam file
by Jean-Alexandre Barszcz (＠jabarszcz) 09 Nov '22

09 Nov '22

Jean-Alexandre Barszcz pushed to branch ja-refl at Stefan / Typer Commits: 50069ddc by Shon Feder at 2022-03-11T20:42:03-05:00 Add Zarith dependency to opam file Also adds "synopsis" and "description" fields, with content taken from https://www.iro.umontreal.ca/~monnier/ - - - - - 12c08fbb by Shon Feder at 2022-03-11T20:42:03-05:00 Ignore the opam switch directory - - - - - a2bc3d5c by Stefan Monnier at 2022-05-10T14:50:33-04:00 * src/debruijn.ml (senv_lookup): Fix ordering of tests - - - - - c422f432 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-26T18:51:50+00:00 [OK] Compilateur - - - - - cbd1e53a by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-31T20:45:09+00:00 Ajout du type sinfo - - - - - 471c1ff6 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-31T20:52:07+00:00 Ajout du type sinfo pour Sexp-info - - - - - f0551384 by Stefan Monnier at 2022-08-27T14:07:24-04:00 Merge branch 'add-zarith-dependency' into 'main' See merge request monnier/typer!2 - - - - - 525e358e by Simon Génier at 2022-08-28T22:37:40-04:00 Add a test for type ascription. Also improve how discrepancies in sexp tests are reported. - - - - - 2a824e2d by Simon Génier at 2022-08-28T22:39:23-04:00 Pretty-prints the code emitted by the Gambit backend. It spawns Gambit as a subprocess and delegates the pretty-printing to it. We only have to worry about emitting valid code. I intend to use the inferior Gambit mechanism to also implement a REPL. - - - - - cc46ac0a by Simon Génier at 2022-09-02T14:34:57-04:00 Fix off by one error on line numbers. The source_file object start in a kind of null state, with an empty line, causing to read the first line lazily as the first char is peeked. This means we need to put the cursor before the first line and not on the first line! - - - - - 29c3f091 by Simon Génier at 2022-09-02T14:36:31-04:00 Merge branch 'oops-fix-off-by-one-error-on-line-numbers' - - - - - ef72535e by Jean-Alexandre Barszcz at 2022-09-28T22:20:38-04:00 [WIP] Don't close the types of builtins `lexp_close` introduces redundant definitions with let-expressions. Instead of closing the built-in (with their type), we keep track of their context (length) and shift them appropriately where they are used. - - - - - acf0b570 by Jean-Alexandre Barszcz at 2022-10-12T03:24:48-04:00 [WIP] Add an internal name ("id") to make typecons more nominal Comparing all the constructors and parameters of typeconses for conversion is slow. This commit takes the easy and short approach, by minimally changing the `Inductive` constructor and only adding an internal name. Conversion is checked by comparing this internal name, which is faster. However, type safety relies on the proper use of this name. Design constraints: I would like to 1. be able to escape the nominal paradigm and refer to a typecons by value if needed (if its internal name is known). 2. not influence the property that the pretty printed code can be re-elaborated. A challenge here is that typeconses can be substituted through the code, so they have to be "pure". 3. avoid larger changes to the context (if the formal parameter and constructor info is not present in the typecons, it has to be somewhere in the context). Another option meeting these requirement would be to add an indirection (eg. `typeconsref`) to `lexp` that is not substituted like normal variables, but still points to the typecons in context. The elaboration of inductives would bind the typecons and return a reference to it. This indirection would take care of the redundancy of the current representation and avoid inconsistencies, but require a bit more work to implement. - - - - - 35c30984 by Jean-Alexandre Barszcz at 2022-11-09T01:20:59-05:00 [WIP] Fix predefs; Reflect lists and S-exps - - - - - 53a58925 by Jean-Alexandre Barszcz at 2022-11-09T13:04:39-05:00 [WIP] Remove Vsexp from value_type - - - - - 511daa3a by Jean-Alexandre Barszcz at 2022-11-09T13:05:47-05:00 [WIP] Replace the Sexp builtins by regular constructors - - - - - 29 changed files: - .gitignore - + .idea/workspace.xml - btl/builtins.typer - btl/pervasive.typer - debug_util.ml - opam - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/dune - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - + src/predefs.ml - + src/pretty-printer.scm - src/sexp.ml - src/source.ml - src/unification.ml - src/util.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/dc04f51bd034814b4d743881ed4903b5… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/dc04f51bd034814b4d743881ed4903b5… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compile-pervasives] Print multiline locations.
by Simon Génier (＠ilovemonoids) 04 Nov '22

04 Nov '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: c6e03ab0 by Simon Génier at 2022-11-04T16:43:26-04:00 Print multiline locations. - - - - - 1 changed file: - src/source.ml Changes: ===================================== src/source.ml ===================================== @@ -175,31 +175,60 @@ module Location = struct let display_context (location : t) (f : formatter) : unit = + let print_within line_number = + let line = Container.nth_line location.container line_number in + let before = String.sub line 0 location.start_offset in + let focus = + String.sub + line + location.start_offset + (location.end_offset - location.start_offset) + in + let after = + String.sub + line + location.end_offset + (String.length line - location.end_offset) + in + fprintf f "%d | %s@{<cyan>%s@}%s@." line_number before focus after; + in + + let print_start_line line_number start_offset = + let line = Container.nth_line location.container line_number in + let before = String.sub line 0 start_offset in + let focus = + String.sub line start_offset (String.length line - start_offset) + in + fprintf f "%d | %s@{<cyan>%s@}@." line_number before focus; + in + + let print_middle_line line_number = + let line = Container.nth_line location.container line_number in + fprintf f "%d | @{<cyan>%s@}@." line_number line; + in + + let print_end_line line_number end_offset = + let line = Container.nth_line location.container line_number in + let focus = String.sub line 0 end_offset in + let after = String.sub line end_offset (String.length line - end_offset) in + fprintf f "%d | @{<cyan>%s@}%s@." line_number focus after; + in + if location != dummy then begin fprintf f " → In: @{<green>%s@}@." (Container.name location.container); if location.start_line = location.end_line - then - let line = Container.nth_line location.container location.start_line in - let before = String.sub line 0 location.start_offset in - let focus = - String.sub - line - location.start_offset - (location.end_offset - location.start_offset) - in - let after = - String.sub - line - location.end_offset - (String.length line - location.end_offset) - in - fprintf f "%d | %s@{<cyan>%s@}%s@." location.start_line before focus after; - else - failwith "TODO" + then print_within location.start_line + else begin + print_start_line location.start_line location.start_offset; + for line_number = location.start_line + 1 to location.end_line - 1 do + print_middle_line line_number; + done; + print_end_line location.end_line location.end_offset; end + end end (** A source object is text paired with a cursor. *) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c6e03ab0f974d75cc87a3a15184172fda… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c6e03ab0f974d75cc87a3a15184172fda… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Novembre 2022