Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer

Commits: 440cc0a6 by Jean-Alexandre Barszcz at 2020-05-15T19:14:06-04:00 [WIP] First draft of an instance search algorithm

- - - - -

6 changed files:

- samples/decidable.typer - src/elab.ml - src/log.ml - src/myers.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== samples/decidable.typer ===================================== @@ -135,3 +135,10 @@ decideLT = case p | ltZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ ?)) | ltS => absurd (? : (a' < b')) (? : Not (a' < b'))); + +test1 : Bool; +test1 = + let inst = decideEven (a := (succ zero)) in + case (instance () : Decidable (even (succ zero))) + | yes => true + | no => false; % Why wrong index in eval

===================================== src/elab.ml ===================================== @@ -707,7 +707,8 @@ and check_inferred ctx e inferred_t t = -> lexp_error (lexp_location e) e ("Type mismatch(" ^ (match ck with | Unif.CKimpossible -> "impossible" - | Unif.CKresidual -> "residue") + | Unif.CKresidual -> "residue" + | _ -> failwith "impossible" ) ^ ")! Context expected:\n " ^ lexp_string t ^ "\nbut expression has type:\n " ^ lexp_string inferred_t ^ "\ncan't unify:\n " @@ -1646,7 +1647,8 @@ let rec sform_lambda kind ctx loc sargs ot = -> lexp_error (lexp_location lt1') lt1' ("Type mismatch(" ^ (match ck with | Unif.CKimpossible -> "impossible" - | Unif.CKresidual -> "residue") + | Unif.CKresidual -> "residue" + | _ -> failwith "impossible") ^ ")! Context expected:\n " ^ lexp_string lt1 ^ "\nbut parameter has type:\n " ^ lexp_string lt1' ^ "\ncan't unify:\n " @@ -1820,6 +1822,61 @@ let sform_load usr_elctx loc sargs ot =

(tuple',Lazy)

+let myers_filter_index (f : int -> 'a -> bool) (m : 'a M.myers) + : ((int * 'a) M.myers) + = snd (M.fold_right + (fun x (i, l') -> + if (f i x) then (i - 1, M.cons (i, x) l') + else (i - 1, l')) + m (M.length m - 1, M.nil)) + +(** + Draft of a special form "instance" that gets refers to a variable + of the requested type in the context. Ultimately, this search + should be automatically triggered at the call sites for a new kind + of argument (instance arguments) similarly to implicit arguments. + **) +let sform_instance ctx loc sargs ot = + let search (t : ltype) : lexp * sform_type = + Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`"); + let lctx = (ectx_to_lctx ctx) in + let env_elem_match (i : int) (e : DB.env_elem) : bool = + let (_, _, t') = e in + let t' = mkSusp t' (S.shift (i + 1)) in + (* TODO decompose the arrows to match on the result type and + then recursively search for the parameters' types *) + let constraints = Unif.unify ~checking:true t' t lctx in + List.for_all (function | (Unif.CKimpossible,_,_,_) -> false + | (Unif.CKresidual,_,_,_) -> + false (* Should be true maybe ? *) + | _ -> true) + constraints in + let candidates = + myers_filter_index env_elem_match lctx in + Log.log_debug ("Candidates for instance of type `" ^ lexp_string t ^ "`:") + ~print_action:(fun () -> + M.iter (fun (i, ((_, so),_,t')) -> + lalign_print_int i 4; + lalign_print_string (match so with | Some s -> s | None -> "<none>") 10; + print_endline (lexp_string t')) candidates); + match M.safe_car candidates with + | None -> + (error ~loc + ("No instance found in context for type `" ^ lexp_string t ^ "`"); + sform_dummy_ret ctx loc) + | Some (i, (vname, _, t')) -> + let t' = mkSusp t' (S.shift (i + 1)) in + Log.log_debug ~loc + ("Found candidate at index " ^ (string_of_int i) ^ ": `" ^ + (lexp_string (Var (vname, i))) ^ " : " ^ (lexp_string t') ^ "`"); + (Var (vname, i), Inferred t') (* FIXME : What location should we use here ? *) + in + match sargs, ot with + | ([se; _], _) -> search (infer_type se ctx (loc, None)) + | ([_], Some t) -> search t (* Dummy param to trigger the special form *) + | _ -> (sexp_error loc "##instance expects a type argument if not checked"; + sform_dummy_ret ctx loc) + (* Register special forms. *) let register_special_forms () = List.iter add_special_form @@ -1849,6 +1906,7 @@ let register_special_forms () = (* FIXME: These should be functions! *) ("decltype", sform_decltype); ("declexpr", sform_declexpr); + ("instance", sform_instance); ]

(* Default context with builtin types

===================================== src/log.ml ===================================== @@ -133,11 +133,13 @@ let print_entry entry = let log_entry (entry : log_entry) = if (entry.level <= typer_log_config.level) then ( - log_push entry; - if (typer_log_config.print_at_log) + if (typer_log_config.print_at_log || + entry.level >= Debug) then (print_entry entry; flush stdout) + else + log_push entry )

let count_msgs (lvlp : log_level -> bool) =

===================================== src/myers.ml ===================================== @@ -54,11 +54,21 @@ let car l = | Mnil -> raise Not_found | Mcons (x, _, _, _) -> x

+let safe_car l = + match l with + | Mnil -> None + | Mcons (x, _, _, _) -> Some x + let cdr l = match l with | Mnil -> Mnil | Mcons (_, l, _, _) -> l

+let safe_cdr l = + match l with + | Mnil -> None + | Mcons (_, l, _, _) -> Some l + let case l n c = match l with | Mnil -> n () @@ -136,3 +146,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil

let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let iter (f : 'a -> unit) (l : 'a myers) : unit + = fold_left (fun _ x -> f x; ()) () l

===================================== src/unification.ml ===================================== @@ -46,6 +46,7 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) | CKresidual (* We failed to find a unifier. *) + | CKassoc (* Couldn't associate because of checking mode *) (* FIXME: Each constraint should additionally come with a description of how it relates to its "top-level" or some other info which might let us fix the problem (e.g. by introducing coercions). *) @@ -174,13 +175,15 @@ let rec s_offset s = match s with

The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) *) -let rec unify (e1: lexp) (e2: lexp) +let rec unify ?(checking=false) + (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) : return_type = - unify' e1 e2 ctx OL.set_empty + unify' e1 e2 ctx OL.set_empty checking

and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) + (c : bool) (* checking mode ? *) : return_type = if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in @@ -192,24 +195,24 @@ and unify' (e1: lexp) (e2: lexp) match (e1', e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l - | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> unify_call r l ctx vs' - | ((Call _ as l), r) -> unify_call l r ctx vs' - | (l, (Var _ as r)) -> unify_var r l ctx vs' - | ((Var _ as l), r) -> unify_var l r ctx vs' - | (l, (Arrow _ as r)) -> unify_arrow r l ctx vs' - | ((Arrow _ as l), r) -> unify_arrow l r ctx vs' - | (l, (Lambda _ as r)) -> unify_lambda r l ctx vs' - | ((Lambda _ as l), r) -> unify_lambda l r ctx vs' + | (l, (Metavar (idx, s, _) as r)) -> unify_metavar c ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> unify_metavar c ctx idx s l r + | (l, (Call _ as r)) -> unify_call c r l ctx vs' + | ((Call _ as l), r) -> unify_call c l r ctx vs' + | (l, (Var _ as r)) -> unify_var r l ctx vs' + | ((Var _ as l), r) -> unify_var l r ctx vs' + | (l, (Arrow _ as r)) -> unify_arrow c r l ctx vs' + | ((Arrow _ as l), r) -> unify_arrow c l r ctx vs' + | (l, (Lambda _ as r)) -> unify_lambda c r l ctx vs' + | ((Lambda _ as l), r) -> unify_lambda c l r ctx vs' (* | (l, (Case _ as r)) -> unify_case r l subst *) (* | ((Case _ as l), r) -> unify_case l r subst *) (* | (l, (Inductive _ as r)) -> unify_induct r l subst *) (* | ((Inductive _ as l), r) -> unify_induct l r subst *) - | (l, (Sort _ as r)) -> unify_sort r l ctx vs' - | ((Sort _ as l), r) -> unify_sort l r ctx vs' - | (l, (SortLevel _ as r)) -> unify_sortlvl r l ctx vs' - | ((SortLevel _ as l), r) -> unify_sortlvl l r ctx vs' + | (l, (Sort _ as r)) -> unify_sort c r l ctx vs' + | ((Sort _ as l), r) -> unify_sort c l r ctx vs' + | (l, (SortLevel _ as r)) -> unify_sortlvl c r l ctx vs' + | ((SortLevel _ as l), r) -> unify_sortlvl c l r ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -217,7 +220,7 @@ and unify' (e1: lexp) (e2: lexp) * ^ " and " * ^ snd label2 * ^ "\n"); *) - unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + unify_inductive c ctx vs' args1 args2 consts1 consts2 e1 e2 | _ -> (if OL.conv_p ctx e1' e2' then [] else ((* print_string "Unification failure on default\n"; *) [(CKresidual, ctx, e1, e2)])) @@ -230,16 +233,16 @@ and unify' (e1: lexp) (e2: lexp) else None - (_, _) -> None *) -and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs +and unify_arrow (checking : bool) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) + then (unify' ltype1 ltype2 ctx vs checking) @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) + (OL.set_shift vs) checking) else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]

@@ -248,15 +251,15 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs then UNIFY ltype & lxp else ERROR - Lambda , _ -> Impossible *) -and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = +and unify_lambda (checking : bool) (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) + then (unify' ltype1 ltype2 ctx vs checking) @(unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) + (OL.set_shift vs) checking) else [(CKimpossible, ctx, lambda, lxp)] | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

@@ -265,7 +268,7 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> inverse subst (both sides) - metavar , lexp -> inverse subst *) -and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) +and unify_metavar (checking : bool) ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with @@ -281,7 +284,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) [(CKresidual, ctx, lxp1, lxp2)] | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' - -> metavar_table := associate idx lxp' (!metavar_table); + -> if checking then [(CKassoc, ctx, lxp1, lxp2)] else ( + metavar_table := associate idx lxp' (!metavar_table); match unify t (OL.get_type ctx lxp) ctx with | [] as r -> r (* FIXME: Let's ignore the error for now. *) @@ -291,10 +295,10 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) ^ lexp_string t ^ " != " ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - [(CKresidual, ctx, lxp1, lxp2)] in + [(CKresidual, ctx, lxp1, lxp2)]) in match lxp2 with | Metavar (idx2, s2, name) - -> if idx = idx2 then + -> if idx = idx2 && not checking then match common_subset ctx s1 s2 with | S.Identity 0 -> [] (* Optimization! *) (* ¡ s1 != s2 ! @@ -370,14 +374,14 @@ and unify_var (var: lexp) (lxp: lexp) ctx vs - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and unify_call (call: lexp) (lxp: lexp) ctx vs +and unify_call (checking : bool) (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then - (unify' e1 e2 ctx vs)@op + (unify' e1 e2 ctx vs checking)@op else [(CKimpossible, ctx, call, lxp)]) [] (List.combine lxp_list1 lxp_list2) @@ -440,15 +444,15 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sortlvl (checking : bool) (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] - | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs checking | SLlub (l11, l12), SLlub (l21, l22) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) - (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) + (unify' l11 l21 ctx vs checking)@(unify' l12 l22 ctx vs checking) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) | _, _ -> [(CKresidual, ctx, sortlvl, lxp)]

@@ -456,10 +460,10 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - Sort, Sort -> if Sort ~= Sort then OK else ERROR - Sort, lexp -> ERROR *) -and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sort (checking : bool) (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with - | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs checking | StypeOmega, StypeOmega -> [] | StypeLevel, StypeLevel -> [] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) @@ -513,7 +517,7 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

-and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive (checking : bool) ctx vs args1 args2 consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) @@ -522,7 +526,7 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = -> (DB.lexp_ctx_cons ctx v1 Variable t1, OL.set_shift vs, if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] - else (unify' t1 t2 ctx vs) @ residue)) + else (unify' t1 t2 ctx vs checking) @ residue)) (ctx, vs, []) (List.combine args1 args2) in let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in

===================================== tests/unify_test.ml ===================================== @@ -199,6 +199,7 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res = else (Unification, res, lxp1, lxp2) | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2) + | _ -> failwith "impossible"

let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = let r, _, _, _ = test_input lxp1 lxp2

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/440cc0a6a65fe16f62f600e4867bdcb7ca...