From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- pretyping/typeclasses.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4207eccb9a..50dd66ea0a 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -289,7 +289,7 @@ let build_subclasses ~check env sigma glob pri = | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = - Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels)) + Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels))) in let projargs = Array.of_list (args @ [instapp]) in let projs = List.map_filter -- cgit v1.2.3 From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- pretyping/typeclasses.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 50dd66ea0a..8c03329e24 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -300,7 +300,7 @@ let build_subclasses ~check env sigma glob pri = | Some (Forward, pri') -> let proj = Option.get proj in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in - if check && check_instance env sigma body then None + if check && check_instance env sigma (EConstr.of_constr body) then None else let pri = match pri, pri' with @@ -312,7 +312,7 @@ let build_subclasses ~check env sigma glob pri = in let declare_proj hints (cref, pri, body) = let path' = cref :: path in - let ty = Retyping.get_type_of env sigma body in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in let rest = aux pri body ty path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs -- cgit v1.2.3 From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:23:13 +0100 Subject: Evarconv API using EConstr. --- pretyping/typeclasses.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 8c03329e24..11f71ee023 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -165,7 +165,7 @@ let rec is_class_type evd c = match kind_of_term c with | Prod (_, _, t) -> is_class_type evd t | Evar (e, _) when Evd.is_defined evd e -> - is_class_type evd (Evarutil.whd_head_evar evd c) + is_class_type evd (EConstr.Unsafe.to_constr (Evarutil.whd_head_evar evd (EConstr.of_constr c))) | _ -> is_class_constr c let is_class_evar evd evi = -- cgit v1.2.3 From 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 13:27:16 +0100 Subject: Typeclasses API using EConstr. --- pretyping/typeclasses.ml | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 11f71ee023..a970c434f4 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 *) -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- pretyping/typeclasses.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a970c434f4..f59a6dcd94 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -156,17 +156,17 @@ 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 = - try let gr, u = Universes.global_of_constr c in +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in Refmap.mem gr !classes with Not_found -> false let rec is_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in - match EConstr.kind evd (EConstr.of_constr c) with + match EConstr.kind evd c with | Prod (_, _, t) -> is_class_type evd t | Cast (t, _, _) -> is_class_type evd t - | _ -> is_class_constr c + | _ -> is_class_constr evd c let is_class_evar evd evi = is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- pretyping/typeclasses.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index f59a6dcd94..9ee34341ba 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -291,6 +291,7 @@ let build_subclasses ~check env sigma glob pri = let instapp = Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels))) in + let instapp = EConstr.Unsafe.to_constr instapp in let projargs = Array.of_list (args @ [instapp]) in let projs = List.map_filter (fun (n, b, proj) -> -- cgit v1.2.3 From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- pretyping/typeclasses.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9ee34341ba..9da7005e09 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -270,7 +270,7 @@ let add_class cl = let check_instance env sigma c = try let (evd, c) = resolve_one_typeclass env sigma - (EConstr.of_constr (Retyping.get_type_of env sigma c)) in + (Retyping.get_type_of env sigma c) in not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false @@ -314,7 +314,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 (EConstr.of_constr ty) path' in + let rest = aux pri body ty path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs in -- cgit v1.2.3 From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 15:30:02 +0100 Subject: Introducing contexts parameterized by the inner term type. This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. --- pretyping/typeclasses.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9da7005e09..50ae66eb0e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -289,7 +289,7 @@ let build_subclasses ~check env sigma glob pri = | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = - Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels))) + Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels))) in let instapp = EConstr.Unsafe.to_constr instapp in let projargs = Array.of_list (args @ [instapp]) in -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- pretyping/typeclasses.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 50ae66eb0e..ce570ee127 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -300,6 +300,7 @@ let build_subclasses ~check env sigma glob pri = | Some (Backward, _) -> None | Some (Forward, pri') -> let proj = Option.get proj in + let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in if check && check_instance env sigma (EConstr.of_constr body) then None else -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- pretyping/typeclasses.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 478499d91d..93c71e6ea9 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -303,6 +303,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = | Some (Forward, info) -> let proj = Option.get proj in let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in + let u = EConstr.EInstance.kind sigma u in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in if check && check_instance env sigma (EConstr.of_constr body) then None else -- cgit v1.2.3