diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 20 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 38 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 3 | ||||
| -rw-r--r-- | interp/topconstr.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
5 files changed, 52 insertions, 13 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 54abacaf6..6c09e4ace 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -696,11 +696,9 @@ let intern_typeclass_binders intern_type lvar env bl = (env, (na,bk,None,ty)::bl)) env bl -let intern_typeclass_binder intern_type lvar (env,bl) na b ty = - let ctx = (na, b, ty) in - let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in - let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in - intern_typeclass_binders intern_type lvar (env,ifvs) bind +let intern_typeclass_binder intern_type lvar (env,bl) cb = + let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in + intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind]) let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function | LocalRawAssum(nal,bk,ty) -> @@ -713,8 +711,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = fu (fun ((ids,ts,sc),bl) (_,na) -> ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl)) (env,bl) nal - | TypeClass b -> - intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty) + | TypeClass (b,b') -> + intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty)) | LocalRawDef((loc,na),def) -> ((name_fold Idset.add na ids,ts,sc), (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) @@ -1029,9 +1027,9 @@ let internalise sigma globalenv env allow_patvar lvar c = in match bk with | Default b -> default env b nal - | TypeClass b -> + | TypeClass (b,b') -> let env, ibind = intern_typeclass_binder intern_type lvar - (env, []) (List.hd nal) b ty in + (env, []) (List.hd nal,(b,b'),ty) in let body = intern_type env body in it_mkRProd ibind body @@ -1045,9 +1043,9 @@ let internalise sigma globalenv env allow_patvar lvar c = | [] -> intern env body in match bk with | Default b -> default env b nal - | TypeClass b -> + | TypeClass (b, b') -> let env, ibind = intern_typeclass_binder intern_type lvar - (env, []) (List.hd nal) b ty in + (env, []) (List.hd nal,(b,b'),ty) in let body = intern env body in it_mkRLambda ibind body diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index bef2573e5..d084a3f7d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -193,6 +193,44 @@ let resolve_class_binders env l = in fv_ctx, ctx +let full_class_binder env (iid, (bk, bk'), cl as c) = + let avoid = Idset.union env (ids_of_list (compute_context_vars env [c])) in + let c, avoid = + match bk' with + | Implicit -> + let (loc, id, l) = + try destClassAppExpl cl + with Not_found -> + user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class") + in + let gr = Nametab.global id in + (try + let c = class_info gr in + let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in + (iid, bk, CAppExpl (loc, (None, id), args)), avoid + with Not_found -> not_a_class (Global.env ()) (constr_of_global gr)) + | Explicit -> ((iid,bk,cl), avoid) + in c + +let compute_constraint_freevars env (oid, _, x) = + let bound = match snd oid with Name n -> Idset.add n env | Anonymous -> env in + let ids = free_vars_of_constr_expr x ~bound [] in + freevars_of_ids env (List.rev ids) + +let resolve_class_binder env c = + let cstr = full_class_binder env c in + let fv_ctx = + let elts = compute_constraint_freevars env cstr in + List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts + in fv_ctx, cstr + +let generalize_class_binder_raw env c = + let env = Idset.union env (Termops.vars_of_env (Global.env())) in + let fv_ctx, cstr = resolve_class_binder env c in + let ids' = List.fold_left (fun acc ((loc, id), t) -> Idset.add id acc) env fv_ctx in + let ctx' = List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx in + ids', ctx', cstr + let generalize_class_binders_raw env l = let env = Idset.union env (Termops.vars_of_env (Global.env())) in let fv_ctx, cstrs = resolve_class_binders env l in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index bd061a1ed..ac1b8c99a 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -43,6 +43,9 @@ val resolve_class_binders : Idset.t -> typeclass_context -> (identifier located * constr_expr) list * typeclass_context val full_class_binders : Idset.t -> typeclass_context -> typeclass_context + +val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr -> + Idset.t * typeclass_context * typeclass_constraint val generalize_class_binders_raw : Idset.t -> typeclass_context -> (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list diff --git a/interp/topconstr.ml b/interp/topconstr.ml index cef1b9391..570eae7e5 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -590,7 +590,7 @@ type notation = string type explicitation = ExplByPos of int * identifier option | ExplByName of identifier -type binder_kind = Default of binding_kind | TypeClass of binding_kind +type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 6790e400f..46133c27b 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -95,7 +95,7 @@ type notation = string type explicitation = ExplByPos of int * identifier option | ExplByName of identifier -type binder_kind = Default of binding_kind | TypeClass of binding_kind +type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) |