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

Commits: 5483f630 by Jean-Alexandre Barszcz at 2020-06-09T13:26:36-04:00 WIP WIP WIP

- - - - -

2 changed files:

- src/elab.ml - src/unification.ml

Changes:

===================================== src/elab.ml ===================================== @@ -61,6 +61,8 @@ module Unif = Unification module OL = Opslexp module EL = Elexp

+type match_res = Impossible | Possible | Match + (* dummies *) let dloc = dummy_location

@@ -621,16 +623,94 @@ and get_implicit_arg ctx loc oname t = | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (loc, oname) t

+and is_typeclass t lctx = true (* TODO *) + (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp_whnf t (ectx_to_lctx ctx) with + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when is_typeclass t1 ctx + -> let lctx = ectx_to_lctx ctx in + let sl = ectx_to_scope_level ctx in + (* FIXME Should it be a special instance metavar? Or do we + know from its type? If we know from the type then + instantiation is the same for both cases (is_typeclass or + not) *) + let arg = newMetavar lctx sl (lexp_location e, v) t1 in + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) in instantiate t []

+and myers_filter_map_index (f : int -> 'a -> 'b option) (m : 'a M.myers) + : ('b M.myers) + = snd (M.fold_right + (fun x (i, l') -> + match (f i x) with + | Some y -> (i - 1, M.cons y l') + | None -> (i - 1, l')) + m (M.length m - 1, M.nil)) + +and check_typeclass_match t1 t2 lctx sl = + match Unif.unify ~checking:sl t1 t2 lctx with + | [] -> Match + | constraints when List.exists (function | (Unif.CKimpossible,_,_,_) -> true + | _ -> false) + constraints -> Impossible + | _ -> Possible + +and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp * sform_type = + Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`"); + let lctx = (ectx_to_lctx ctx) in + let sl = (ectx_to_scope_level ctx) in (* FIXME should we create a new scope ? *) + let env_elem_match (i : int) (elem : DB.env_elem) : (int * DB.env_elem * lexp * ltype) option = + let (vname, _, t') = elem in + let var = mkVar (vname, i) in (* Change the location maybe *) + let t' = mkSusp t' (S.shift (i + 1)) in + let (e, t') = instantiate_implicit var t' ctx in + (* All candidates should have a type that is a typeclass *) + if not (is_typeclass t' ctx) then None else + match check_typeclass_match t t' lctx sl with + | Impossible -> None + (* | Possible -> None *) + | (Possible | Match) -> Some (i, elem, e, t') in + let candidates = + myers_filter_map_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'),e,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') ^ "`"); + (e, Inferred t) + +and resolve_instances ctx e = + (* TODO + + For all instance metavars, we have to do the instance search in + their context. Maybe the elab_context is not necessary, only the + right lctx and scope level. + + Can we get a metavar's lctx from the current ctx and the + metavar's substitution? If yes then we can use OL.fv, otherwise + structural recursion on lexps MEH *) + failwith "TODO" + +and resolve_instances_and_generalize ctx e = + generalize ctx (resolve_instances ctx e) + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated @@ -1822,14 +1902,6 @@ 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 @@ -1837,43 +1909,10 @@ let myers_filter_index (f : int -> 'a -> bool) (m : 'a M.myers) 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 + (* TODO replace with instance metavars *) match sargs, ot with - | ([se; _], _) -> search (infer_type se ctx (loc, None)) - | ([_], Some t) -> search t (* Dummy param to trigger the special form *) + | ([se; _], _) -> search_instance ctx loc (infer_type se ctx (loc, None)) + | ([_], Some t) -> search_instance ctx loc t (* Dummy param to trigger the special form *) | _ -> (sexp_error loc "##instance expects a type argument if not checked"; sform_dummy_ret ctx loc)

===================================== src/unification.ml ===================================== @@ -175,7 +175,7 @@ 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 ?(checking=false) +let rec unify ?checking (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) : return_type = @@ -183,7 +183,7 @@ let rec unify ?(checking=false)

and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) - (c : bool) (* checking mode ? *) + (c : scope_level option) (* checking mode scope level *) : return_type = if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in @@ -233,7 +233,7 @@ and unify' (e1: lexp) (e2: lexp) else None - (_, _) -> None *) -and unify_arrow (checking : bool) (arrow: lexp) (lxp: lexp) ctx vs +and unify_arrow (checking : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), @@ -251,7 +251,7 @@ and unify_arrow (checking : bool) (arrow: lexp) (lxp: lexp) ctx vs then UNIFY ltype & lxp else ERROR - Lambda , _ -> Impossible *) -and unify_lambda (checking : bool) (lambda: lexp) (lxp: lexp) ctx vs : return_type = +and unify_lambda (checking : scope_level option) (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) @@ -268,37 +268,40 @@ and unify_lambda (checking : bool) (lambda: lexp) (lxp: lexp) ctx vs : return_ty - metavar , metavar -> inverse subst (both sides) - metavar , lexp -> inverse subst *) -and unify_metavar (checking : bool) ctx idx s1 (lxp1: lexp) (lxp2: lexp) +and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = - let t = match metavar_lookup idx with + let t, sl = match metavar_lookup idx with | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s in + | MVar (_, t, sl) -> push_susp t s, sl in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> log_info ?loc:None ("Unification of metavar failed:\n " - ^ "?[" ^ subst_string s ^ "]" - ^ "\nAgainst:\n " - ^ lexp_string lxp ^ "\n"); + -> log_info ~loc:(lexp_location lxp) + ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' - -> 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. *) - | _ - -> log_info ?loc:None - ("Unification of metavar type failed:\n " - ^ lexp_string t ^ " != " - ^ lexp_string (OL.get_type ctx lxp) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - [(CKresidual, ctx, lxp1, lxp2)]) in + -> match checking with + | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)] + | _ -> ( + 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. *) + | _ + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)]) in match lxp2 with | Metavar (idx2, s2, name) - -> if idx = idx2 && not checking then + -> if idx = idx2 && checking == None then match common_subset ctx s1 s2 with | S.Identity 0 -> [] (* Optimization! *) (* ¡ s1 != s2 ! @@ -374,7 +377,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx vs - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and unify_call (checking : bool) (call: lexp) (lxp: lexp) ctx vs +and unify_call (checking : scope_level option) (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) @@ -444,7 +447,7 @@ and unify_call (checking : bool) (call: lexp) (lxp: lexp) ctx vs - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and unify_sortlvl (checking : bool) (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sortlvl (checking : scope_level option) (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] @@ -460,7 +463,7 @@ and unify_sortlvl (checking : bool) (sortlvl: lexp) (lxp: lexp) ctx vs : return_ - Sort, Sort -> if Sort ~= Sort then OK else ERROR - Sort, lexp -> ERROR *) -and unify_sort (checking : bool) (sort_: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sort (checking : scope_level option) (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 checking @@ -517,7 +520,7 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

-and unify_inductive (checking : bool) ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive (checking : scope_level option) 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)])

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5483f630fbe10b950d7be014d875e14f3d...