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/classops.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 30d100af9f..fd21f5bd12 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -192,13 +192,14 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) let find_class_type sigma t = - let t', args = Reductionops.whd_betaiotazeta_stack sigma t in - match kind_of_term t' with - | Var id -> CL_SECVAR id, Univ.Instance.empty, args - | Const (sp,u) -> CL_CONST sp, u, args + let inj = EConstr.Unsafe.to_constr in + let t', args = Reductionops.whd_betaiotazeta_stack sigma (EConstr.of_constr t) in + match EConstr.kind sigma t' with + | Var id -> CL_SECVAR id, Univ.Instance.empty, List.map inj args + | Const (sp,u) -> CL_CONST sp, u, List.map inj args | Proj (p, c) when not (Projection.unfolded p) -> - CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args - | Ind (ind_sp,u) -> CL_IND ind_sp, u, args + CL_PROJ (Projection.constant p), Univ.Instance.empty, List.map inj (c :: args) + | Ind (ind_sp,u) -> CL_IND ind_sp, u, List.map inj args | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] | Sort _ -> CL_SORT, Univ.Instance.empty, [] | _ -> raise Not_found @@ -232,7 +233,7 @@ let class_of env sigma t = let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) with Not_found -> - let t = Tacred.hnf_constr env sigma t in + let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) @@ -276,7 +277,7 @@ let apply_on_class_of env sigma t cont = t, cont i with Not_found -> (* Is it worth to be more incremental on the delta steps? *) - let t = Tacred.hnf_constr env sigma t in + let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; @@ -297,9 +298,9 @@ let lookup_path_to_sort_from env sigma s = let get_coercion_constructor env coe = let c, _ = - Reductionops.whd_all_stack env Evd.empty coe.coe_value + Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value) in - match kind_of_term c with + match EConstr.kind Evd.empty (** FIXME *) c with | Construct (cstr,u) -> (cstr, Inductiveops.constructor_nrealargs cstr -1) | _ -> @@ -403,7 +404,7 @@ type coercion = { let reference_arity_length ref = let t = Universes.unsafe_type_of_global ref in - List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t)) + List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) let projection_arity_length p = let len = reference_arity_length (ConstRef p) in -- 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/classops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index fd21f5bd12..577f41a7d7 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -441,7 +441,7 @@ let cache_coercion (_, c) = let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty value in + let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in let xf = { coe_value = value; coe_type = typ; -- cgit v1.2.3 From ce2b509734f3b70494a0a35b0b4eda593c1c8eb6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 19:07:16 +0100 Subject: Classops API using EConstr. --- pretyping/classops.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 577f41a7d7..753127357a 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -193,7 +193,7 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab let find_class_type sigma t = let inj = EConstr.Unsafe.to_constr in - let t', args = Reductionops.whd_betaiotazeta_stack sigma (EConstr.of_constr t) in + let t', args = Reductionops.whd_betaiotazeta_stack sigma t in match EConstr.kind sigma t' with | Var id -> CL_SECVAR id, Univ.Instance.empty, List.map inj args | Const (sp,u) -> CL_CONST sp, u, List.map inj args @@ -215,7 +215,7 @@ let subst_cl_typ subst ct = match ct with | CL_CONST c -> let c',t = subst_con_kn subst c in if c' == c then ct else - pi1 (find_class_type Evd.empty t) + pi1 (find_class_type Evd.empty (EConstr.of_constr t)) | CL_IND i -> let i' = subst_ind subst i in if i' == i then ct else CL_IND i' @@ -231,10 +231,10 @@ let class_of env sigma t = try let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, u, args) + (EConstr.Unsafe.to_constr t, n1, i, u, args) with Not_found -> - let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in - let (cl, u, args) = find_class_type sigma t in + let t = Tacred.hnf_constr env sigma t in + let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) in @@ -274,11 +274,11 @@ let apply_on_class_of env sigma t cont = let (cl,u,args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i + EConstr.Unsafe.to_constr t, cont i with Not_found -> (* Is it worth to be more incremental on the delta steps? *) - let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in - let (cl, u, args) = find_class_type sigma t in + let t = Tacred.hnf_constr env sigma t in + let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; t, cont i -- cgit v1.2.3 From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 20:33:06 +0100 Subject: Coercion API using EConstr. --- pretyping/classops.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 753127357a..ad43bf3229 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -192,14 +192,13 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) let find_class_type sigma t = - let inj = EConstr.Unsafe.to_constr in let t', args = Reductionops.whd_betaiotazeta_stack sigma t in match EConstr.kind sigma t' with - | Var id -> CL_SECVAR id, Univ.Instance.empty, List.map inj args - | Const (sp,u) -> CL_CONST sp, u, List.map inj args + | Var id -> CL_SECVAR id, Univ.Instance.empty, args + | Const (sp,u) -> CL_CONST sp, u, args | Proj (p, c) when not (Projection.unfolded p) -> - CL_PROJ (Projection.constant p), Univ.Instance.empty, List.map inj (c :: args) - | Ind (ind_sp,u) -> CL_IND ind_sp, u, List.map inj args + CL_PROJ (Projection.constant p), Univ.Instance.empty, (c :: args) + | Ind (ind_sp,u) -> CL_IND ind_sp, u, args | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] | Sort _ -> CL_SORT, Univ.Instance.empty, [] | _ -> raise Not_found @@ -231,10 +230,11 @@ let class_of env sigma t = try let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in - (EConstr.Unsafe.to_constr t, n1, i, u, args) + (t, n1, i, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in + let t = EConstr.of_constr t in + let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) in @@ -274,11 +274,12 @@ let apply_on_class_of env sigma t cont = let (cl,u,args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; - EConstr.Unsafe.to_constr t, cont i + t, cont i with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in - let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in + let t = EConstr.of_constr t in + let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; t, cont i -- cgit v1.2.3 From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- pretyping/classops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ad43bf3229..9011186a3d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -319,7 +319,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; let subst, ctx = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in - (make_judge c' t', b, b'), ctx + (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- pretyping/classops.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 9011186a3d..23d20dad3e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -51,6 +51,7 @@ type coe_info_typ = { coe_param : int } let coe_info_typ_equal c1 c2 = + let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in eq_constr c1.coe_value c2.coe_value && eq_constr c1.coe_type c2.coe_type && c1.coe_local == c2.coe_local && -- 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/classops.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 23d20dad3e..e4331aade2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -234,7 +234,6 @@ let class_of env sigma t = (t, n1, i, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let t = EConstr.of_constr t in let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) @@ -279,7 +278,6 @@ let apply_on_class_of env sigma t cont = with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in - let t = EConstr.of_constr t in let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; -- 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/classops.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index e4331aade2..13310c44d5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -442,6 +442,7 @@ let cache_coercion (_, c) = let it, _ = class_info c.coercion_target in let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; coe_type = typ; -- 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/classops.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 13310c44d5..632ba0d9cd 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -193,15 +193,16 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) let find_class_type sigma t = + let open EConstr in let t', args = Reductionops.whd_betaiotazeta_stack sigma t in match EConstr.kind sigma t' with - | Var id -> CL_SECVAR id, Univ.Instance.empty, args + | Var id -> CL_SECVAR id, EInstance.empty, args | Const (sp,u) -> CL_CONST sp, u, args | Proj (p, c) when not (Projection.unfolded p) -> - CL_PROJ (Projection.constant p), Univ.Instance.empty, (c :: args) + CL_PROJ (Projection.constant p), EInstance.empty, (c :: args) | Ind (ind_sp,u) -> CL_IND ind_sp, u, args - | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] - | Sort _ -> CL_SORT, Univ.Instance.empty, [] + | Prod (_,_,_) -> CL_FUN, EInstance.empty, [] + | Sort _ -> CL_SORT, EInstance.empty, [] | _ -> raise Not_found -- cgit v1.2.3