diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 47 |
1 files changed, 26 insertions, 21 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 08051fd3..efb3c339 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -25,6 +25,13 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen + let typeclasses_unique_solutions = ref false let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions @@ -64,16 +71,16 @@ type typeclass = { cl_univs : Univ.AUContext.t; (* The class implementation *) - cl_impl : global_reference; + cl_impl : GlobRef.t; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : global_reference option list * Context.Rel.t; + cl_context : GlobRef.t option list * Constr.rel_context; (* Context of definitions and properties on defs, will not be shared *) - cl_props : Context.Rel.t; + cl_props : Constr.rel_context; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; cl_strict : bool; @@ -84,19 +91,19 @@ type typeclass = { type typeclasses = typeclass Refmap.t type instance = { - is_class: global_reference; - is_info: Vernacexpr.hint_info_expr; + is_class: GlobRef.t; + is_info: hint_info; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_impl: global_reference; + is_impl: GlobRef.t; } type instances = (instance Refmap.t) Refmap.t let instance_impl is = is.is_impl -let hint_priority is = is.is_info.Vernacexpr.hint_priority +let hint_priority is = is.is_info.hint_priority let new_instance cl info glob impl = let global = @@ -158,7 +165,7 @@ let rec is_class_type evd c = | _ -> is_class_constr evd c let is_class_evar evd evi = - is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) + is_class_type evd evi.Evd.evar_concl (* * classes persistent object @@ -173,12 +180,12 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.Smart.map do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> - (x, y, Option.smartmap do_subst_con z)) projs in + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> + (x, y, Option.Smart.map do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; @@ -216,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.Smart.map Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -227,12 +234,12 @@ let discharge_class (_,cl) = let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in - let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in + let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in { cl_univs = cl_univs'; cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } @@ -266,8 +273,6 @@ let check_instance env sigma c = not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false -open Vernacexpr - let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in let _next_id = @@ -276,7 +281,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in - let inst, ctx = Universes.fresh_instance_from ctx None in + let inst, ctx = UnivGen.fresh_instance_from ctx None in let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in @@ -316,7 +321,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob, inst) in + let term = UnivGen.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] @@ -475,7 +480,7 @@ let instances r = let cl = class_info r in instances_of cl let is_class gr = - Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes + Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes let is_instance = function | ConstRef c -> |