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

Commits: c6bfd8b5 by Jean-Alexandre Barszcz at 2020-06-16T13:34:41-04:00 WIP WIP getting there

- - - - -

5 changed files:

- samples/decidable.typer - src/elab.ml - + src/instances.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== samples/decidable.typer ===================================== @@ -138,7 +138,18 @@ decideLT =

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 + +if_then_else_ + = macro (lambda args -> + let e1 = List_nth 0 args Sexp_error; + e2 = List_nth 1 args Sexp_error; + e3 = List_nth 2 args Sexp_error; + in IO_return (quote (case (instance () : (Decidable (uquote e1))) + | yes => uquote e2 + | no => uquote e3))); + +test2 : Bool; +test2 = if (even (succ zero)) then false else true; \ No newline at end of file

===================================== src/elab.ml ===================================== @@ -57,12 +57,11 @@ open Grammar module BI = Builtin

module Unif = Unification +module Inst = Instances

module OL = Opslexp module EL = Elexp

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

@@ -259,6 +258,13 @@ let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name)

+let newInstanceMetavar (ctx : elab_context) name t = + let lctx = ectx_to_lctx ctx in + let sl = ectx_to_scope_level ctx in + let meta = Unif.create_metavar lctx sl t in + Inst.add_instance_metavar meta ctx (fst name); + mkMetavar (meta, S.identity, name) + let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level

@@ -623,20 +629,12 @@ 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 + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass t1 ctx + -> let arg = newInstanceMetavar ctx (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 @@ -653,29 +651,22 @@ and myers_filter_map_index (f : int -> 'a -> 'b option) (m : 'a M.myers) | 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 = +and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp option = Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`"); + let ctx = ectx_new_scope ctx in let lctx = (ectx_to_lctx ctx) in - let sl = (ectx_to_scope_level ctx) in (* FIXME should we create a new scope ? *) + let sl = (ectx_to_scope_level ctx) in 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 ((_, namopt), _, t') = elem in + let var = mkVar ((loc,namopt), i) in 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 + if not (Inst.is_typeclass t' ctx) then None else + match Inst.check_typeclass_match t t' lctx sl with + | (Impossible | Possible) -> None (* | Possible -> None *) - | (Possible | Match) -> Some (i, elem, e, t') in + | (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 ^ "`:") @@ -685,31 +676,40 @@ and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp * s 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) + | None -> None | 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 + Some e + +and resolve_instances e = + let (_, (fv_map, _)) = OL.fv e in + U.IMap.iter (fun i (sl, t, cl, vn) -> + match Inst.instance_metavar_lookup i with + | Some (ctx, loc) -> + (match search_instance ctx loc t with + | Some e -> Unif.associate i e; resolve_instances e + | None -> + error ~loc ("No instance found for type `" ^ (lexp_string t) ^ "`") + ) + | None -> () + ) fv_map

- 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) + resolve_instances e; + generalize ctx e + +and sdform_typeclass (ctx : elab_context) loc sargs _ot : elab_context = + match sargs with + | [se] -> + let t = infer_type se ctx (loc, None) in + (* TODO add t as a typeclass in the context ? *) + ctx + | _ + -> sexp_error loc "typeclass expects 1 argument"; ctx

and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form @@ -1077,7 +1077,7 @@ and lexp_parse_inductive ctors ctx = (fun (ak, n, t) aa -> Arrow (ak, n, t, dummy_location, aa)) acc impossible in - let g = generalize nctx altacc in + let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t l e -> Arrow (Aerasable, vname, t, l, e)) altacc in @@ -1242,7 +1242,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in - let g = generalize nctx (strip_rettype t) in + let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e -> mkArrow (Aerasable, name, t, l, e)) t @@ -1250,7 +1250,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - let g = generalize nctx e in + let g = resolve_instances_and_generalize nctx e in let e' = g (fun ne vname t l e -> mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)) @@ -1370,6 +1370,10 @@ and lexp_decls_1 -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) pending_decls pending_defs

+ | Node (Symbol (l, "typeclass"), args) :: sdecls + -> lexp_decls_1 sdecls ectx (sdform_typeclass nctx l args None) + pending_decls pending_defs + | Node (Symbol ((l, _) as v), sargs) :: sdecls -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in @@ -1904,17 +1908,19 @@ let sform_load usr_elctx loc sargs ot =

(** 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. + of the requested type in the context. **) let sform_instance ctx loc sargs ot = - (* TODO replace with instance metavars *) match sargs, ot with - | ([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 *) + | ([se; _], _) -> (* Dummy param to trigger the special form *) + let t = infer_type se ctx (loc, None) in + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Inferred t) + | ([_], Some t) -> (* Dummy param to trigger the special form *) + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Checked) | _ -> (sexp_error loc "##instance expects a type argument if not checked"; - sform_dummy_ret ctx loc) + sform_dummy_ret ctx loc)

(* Register special forms. *) let register_special_forms () =

===================================== src/instances.ml ===================================== @@ -0,0 +1,30 @@ +module Unif = Unification +module U = Util +module DB = Debruijn +module L = Lexp +module OL = Opslexp + +(* FIXME Is it possible to have multiple references to the same + instance metavar? It would break the following code *) +let instance_metavar_table = ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) +let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) option + = U.IMap.find_opt id (!instance_metavar_table) +let add_instance_metavar (id : L.meta_id) (ctx : DB.elab_context) (loc : U.location) : unit + = instance_metavar_table := U.IMap.add id (ctx, loc) !instance_metavar_table + +let is_typeclass (t : L.ltype) (ctx : DB.elab_context) = + (* TODO *) + match OL.lexp_whnf t (DB.ectx_to_lctx ctx) with + | L.Call (L.Var ((_,Some s),_), _) when s = "Decidable" -> true + | _ -> false + +type match_res = Impossible | Possible | Match + +let 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 +

===================================== src/opslexp.ml ===================================== @@ -723,6 +723,7 @@ module LMap = Hashtbl.Make (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) let fv_memo = LMap.create 1000 +let fv_flush () = LMap.clear fv_memo

let fv_empty = (DB.set_empty, mv_set_empty) let fv_union (fv1, mv1) (fv2, mv2)

===================================== src/unification.ml ===================================== @@ -55,8 +55,9 @@ type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list type return_type = constraints

(** Alias for VMap.add*) -let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst - = U.IMap.add id (MVal lxp) subst +let associate (id: meta_id) (lxp: lexp) : unit + = metavar_table := U.IMap.add id (MVal lxp) (!metavar_table); + OL.fv_flush ()

let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error @@ -288,7 +289,7 @@ and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: -> match checking with | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)] | _ -> ( - metavar_table := associate idx lxp' (!metavar_table); + associate idx lxp'; match unify t (OL.get_type ctx lxp) ctx with | [] as r -> r (* FIXME: Let's ignore the error for now. *) @@ -352,7 +353,7 @@ and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: * ^ "\n =\n " * ^ subst_string (scompose s s2) * ^ "\n"); *) - metavar_table := associate idx lexp (!metavar_table); + associate idx lexp; assert (OL.conv_p ctx lxp1 lxp2); [] else

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