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

Commits: 2a7b7e3f by Jean-Alexandre Barszcz at 2020-06-23T12:39:25-04:00 [WIP] Add a set of typeclasses to the elab context

- - - - -

4 changed files:

- samples/decidable.typer - src/debruijn.ml - src/elab.ml - src/instances.ml

Changes:

===================================== samples/decidable.typer ===================================== @@ -11,6 +11,8 @@ exfalso f = ##case_ f; yes = datacons Decidable true; no = datacons Decidable false;

+typeclass Decidable; + Eq_trans : (x : ?t) => (y : ?t) => (a : ?t) -> (ax : Eq a x) => (ay : Eq a y) => Eq x y;

===================================== src/debruijn.ml ===================================== @@ -112,26 +112,29 @@ type meta_scope * lctx_length (* Length of ctx when the scope is added. *) * (meta_id SMap.t ref) (* Metavars already known in this scope. *)

+type typeclass_ctx + = (ltype * lctx_length) list (* FIXME make it a set of lexps ? *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * meta_scope + = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx

let get_size (ctx : elab_context) - = let (_, (n, _), lctx, _) = ctx in + = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n

let ectx_to_grm (ectx : elab_context) : Grammar.grammar = - let (grm,_, _, _) = ectx in grm + let (grm,_, _, _, _) = ectx in grm

(* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_,_, lctx, _) = ectx in lctx + let (_,_, lctx, _, _) = ectx in lctx

-let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level +let ectx_to_scope_level ((_, _, _, (sl, _, _), _) : elab_context) : scope_level = sl

-let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen, _), _) as ectx) : int = get_size ectx - slen

(* Public methods: DO USE @@ -142,7 +145,7 @@ let empty_lctx = M.nil

let empty_elab_context : elab_context = (Grammar.default_grammar, empty_senv, empty_lctx, - (0, 0, ref SMap.empty)) + (0, 0, ref SMap.empty), [])

(* senv_lookup caller were using Not_found exception *) exception Senv_Lookup_Fail of (string list) @@ -150,7 +153,7 @@ let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds)

(* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = - let (_, (n, map), _, _) = ctx in + let (_, (n, map), _, _, _) = ctx in try n - (SMap.find name map) - 1 with Not_found -> let get_related_names (n : db_ridx) name map = @@ -189,11 +192,11 @@ let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) =

let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, oname) = def in - let (grm, (n, map), env, sl) = ctx in + let (grm, (n, map), env, sl, tcctx) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), lexp_ctx_cons env def v t, - sl) + sl, tcctx)

let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t

@@ -207,28 +210,33 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx

let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let (grm, (n, senv), lctx, sl) = ctx in + let (grm, (n, senv), lctx, sl, tcctx) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, oname), _, _) -> (match oname with None -> senv | Some name -> SMap.add name i senv), i + 1) (senv, n) defs in - (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl, tcctx)

let ectx_new_scope (ectx : elab_context) : elab_context = - let (grm, senv, lctx, (scope, _, rmmap)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap))) + let (grm, senv, lctx, (scope, _, rmmap), tcctx) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)), tcctx)

let ectx_get_scope (ectx : elab_context) : meta_scope = - let (_, _, _, sl) = ectx in sl + let (_, _, _, sl, _) = ectx in sl

let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = - let (grm, _, _, _) = ectx in grm + let (grm, _, _, _, _) = ectx in grm

let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx

+let env_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = + let (grm, senv, lctx, sl, tcctx) = ectx in + let ntcctx = ((t, get_size ectx) :: tcctx) in + (grm, senv, lctx, sl, ntcctx) + (* Print context *) let print_lexp_ctx_n (ctx : lexp_context) start = let n = (M.length ctx) - 1 in

===================================== src/elab.ml ===================================== @@ -288,8 +288,8 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | Symbol (_, "") -> None | Integer (_, n) -> Some n | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in - let (grm, a, b, c) = ctx in - (SMap.add name (level l, level r) grm, a, b, c) + let (grm, a, b, c, d) = ctx in + (SMap.add name (level l, level r) grm, a, b, c, d) | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ @@ -633,7 +633,7 @@ and get_implicit_arg ctx loc oname t = 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 Inst.is_typeclass t1 ctx + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass ctx t1 -> 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) @@ -662,7 +662,7 @@ and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp opt 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 (Inst.is_typeclass t' ctx) then None else + if not (Inst.is_typeclass ctx t') then None else match Inst.check_typeclass_match t t' lctx sl with | (Impossible | Possible) -> None (* | Possible -> None *) @@ -706,8 +706,7 @@ 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 + Inst.add_typeclass ctx t | _ -> sexp_error loc "typeclass expects 1 argument"; ctx

@@ -1191,9 +1190,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* FIXME: Generalize when/where possible, so things like `map` can be defined without type annotations! *) (* Preserve the new operators added to nctx. *) - let ectx = let (_, a, b, c) = ectx in - let (grm, _, _, _) = nctx in - (grm, a, b, c) in + let ectx = let (_, a, b, c, _) = ectx in + let (grm, _, _, _, tcctx) = nctx in + (grm, a, b, c, tcctx) in let (declmap, nctx) = List.fold_right (fun ((l, vname), pexp) (map, nctx) -> @@ -1203,10 +1202,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in let e = check pexp adjusted_t nctx in - let (grm, ec, lc, sl) = nctx in + let (grm, ec, lc, sl, tcctx) = nctx in let d = (v', LetDef (i + 1, e), t) in (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + (grm, ec, Myers.set_nth i d lc, sl, tcctx)) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in

===================================== src/instances.ml ===================================== @@ -2,6 +2,7 @@ module Unif = Unification module U = Util module DB = Debruijn module L = Lexp +module S = Subst module OL = Opslexp

(* FIXME Is it possible to have multiple references to the same @@ -12,11 +13,41 @@ let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) op 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 +let env_is_typeclass (ectx : DB.elab_context) (t : L.ltype) : bool = + let (_, _, _, _, tcctx) = ectx in + let cl = DB.get_size ectx in + List.exists (fun (t', cl') -> + let i = cl - cl' in + let t' = L.mkSusp t' (S.shift i) in + OL.conv_p (DB.ectx_to_lctx ectx) t t' + (*(Unif.unify ~checking:(max_int (* FIXME *)) t t' (DB.ectx_to_lctx ectx)) = []*) + ) tcctx + + +let get_ind (lctx : DB.lexp_context) (t : L.ltype) : L.ltype option = + match OL.lexp_whnf t lctx with + | L.Call (typecons, _) -> + (match OL.lexp_whnf typecons lctx with + | L.Inductive _ as ind -> Some ind + | _ -> None + ) + | L.Inductive _ as ind -> Some ind + | _ -> None + + +let is_typeclass (ctx : DB.elab_context) (t : L.ltype) = + let lctx = DB.ectx_to_lctx ctx in + match get_ind lctx t with + | Some ind -> env_is_typeclass ctx ind + | None -> false + +let add_typeclass (ctx : DB.elab_context) (t : L.ltype) : DB.elab_context = + let lctx = DB.ectx_to_lctx ctx in + match get_ind lctx t with + | Some ind -> DB.env_add_typeclass ctx ind + | None -> Log.log_error ("Failed to add type class to context " + ^ " because it is not an inductive : `" + ^ (L.lexp_string t) ^ "`"); ctx

type match_res = Impossible | Possible | Match

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