diff options
author | 2016-11-07 13:27:16 +0100 | |
---|---|---|
committer | 2017-02-14 17:26:40 +0100 | |
commit | 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 (patch) | |
tree | a9567a1cc4be9d0625efcb94b021b4729429c0bd /pretyping | |
parent | b77579ac873975a15978c5a4ecf312d577746d26 (diff) |
Typeclasses API using EConstr.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/tacred.ml | 2 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 44 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 10 | ||||
-rw-r--r-- | pretyping/typeclasses_errors.ml | 1 | ||||
-rw-r--r-- | pretyping/typeclasses_errors.mli | 1 |
5 files changed, 30 insertions, 28 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9997976c4..b729f3b9b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1314,7 +1314,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = error_cannot_recognize ref | _ -> try - if eq_gr (global_of_constr (EConstr.to_constr sigma c)) ref + if eq_gr (fst (global_of_constr sigma c)) ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 11f71ee02..a970c434f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -136,23 +136,24 @@ let typeclass_univ_instance (cl,u') = let class_info c = try Refmap.find c !classes - with Not_found -> not_a_class (Global.env()) (printable_constr_of_global c) + with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c)) -let global_class_of_constr env c = - try let gr, u = Universes.global_of_constr c in +let global_class_of_constr env sigma c = + try let gr, u = Termops.global_of_constr sigma c in class_info gr, u with Not_found -> not_a_class env c -let dest_class_app env c = - let cl, args = decompose_app c in - global_class_of_constr env cl, args +let dest_class_app env sigma c = + let cl, args = EConstr.decompose_app sigma c in + global_class_of_constr env sigma cl, (List.map EConstr.Unsafe.to_constr args) -let dest_class_arity env c = - let rels, c = decompose_prod_assum c in - rels, dest_class_app env c +let dest_class_arity env sigma c = + let open EConstr in + let rels, c = decompose_prod_assum sigma c in + rels, dest_class_app env sigma c -let class_of_constr c = - try Some (dest_class_arity (Global.env ()) c) +let class_of_constr sigma c = + try Some (dest_class_arity (Global.env ()) sigma c) with e when CErrors.noncritical e -> None let is_class_constr c = @@ -161,15 +162,14 @@ let is_class_constr c = with Not_found -> false let rec is_class_type evd c = - let c, args = decompose_app c in - match kind_of_term c with + let c, _ = Termops.decompose_app_vect evd c in + match EConstr.kind evd (EConstr.of_constr c) with | Prod (_, _, t) -> is_class_type evd t - | Evar (e, _) when Evd.is_defined evd e -> - is_class_type evd (EConstr.Unsafe.to_constr (Evarutil.whd_head_evar evd (EConstr.of_constr c))) + | Cast (t, _, _) -> is_class_type evd t | _ -> is_class_constr c let is_class_evar evd evi = - is_class_type evd evi.Evd.evar_concl + is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) (* * classes persistent object @@ -222,7 +222,7 @@ let discharge_class (_,cl) = let discharge_context ctx' subst (grs, ctx) = let grs' = let newgrs = List.map (fun decl -> - match decl |> RelDecl.get_type |> class_of_constr with + match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) ctx' @@ -270,7 +270,7 @@ let add_class cl = let check_instance env sigma c = try let (evd, c) = resolve_one_typeclass env sigma - (Retyping.get_type_of env sigma c) in + (EConstr.of_constr (Retyping.get_type_of env sigma c)) in not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false @@ -282,10 +282,10 @@ let build_subclasses ~check env sigma glob pri = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in + let ty = EConstr.of_constr ty in let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in let rec aux pri c ty path = - let ty = Evarutil.nf_evar sigma ty in - match class_of_constr ty with + match class_of_constr sigma ty with | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = @@ -313,7 +313,7 @@ let build_subclasses ~check env sigma glob pri = let declare_proj hints (cref, pri, body) = let path' = cref :: path in let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in - let rest = aux pri body ty path' in + let rest = aux pri body (EConstr.of_constr ty) path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs in @@ -406,7 +406,7 @@ let remove_instance i = let declare_instance pri local glob = let ty = Global.type_of_global_unsafe glob in - match class_of_constr ty with + match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob) (* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2530f5dfa..ec36c57e0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -61,13 +61,13 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c (** These raise a UserError if not a class. Caution: the typeclass structures is not instantiated w.r.t. the universe instance. This is done separately by typeclass_univ_instance. *) -val dest_class_app : env -> constr -> typeclass puniverses * constr list +val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * constr list (** Get the instantiated typeclass structure for a given universe instance. *) val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option +val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference @@ -99,11 +99,11 @@ val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map val mark_resolvable : evar_info -> evar_info val is_class_evar : evar_map -> evar_info -> bool -val is_class_type : evar_map -> types -> bool +val is_class_type : evar_map -> EConstr.types -> bool val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map -val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr +val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> open_constr val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -120,7 +120,7 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> val remove_instance_hint : global_reference -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t -val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t +val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> open_constr) Hook.t val declare_instance : int option -> bool -> global_reference -> unit diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index b1dfb19a0..2db0e9e88 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,6 +9,7 @@ (*i*) open Names open Term +open EConstr open Environ open Constrexpr open Globnames diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index ee76f6383..9bd430e4d 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -9,6 +9,7 @@ open Loc open Names open Term +open EConstr open Environ open Constrexpr open Globnames |