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/a1461ffe5326270999f6782632608d103c...