From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- proofs/redexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 34443b93da..a442a5e63a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = let ctyp = Retyping.get_type_of env sigma c in - if Termops.occur_meta_or_existential c then + if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp -- cgit v1.2.3 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. --- proofs/redexpr.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index a442a5e63a..40a8077a72 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,10 +24,11 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = + let c = EConstr.Unsafe.to_constr c in let ctyp = Retyping.get_type_of env sigma c in if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then error "vm_compute does not support existential variables."; - Vnorm.cbv_vm env c ctyp + Vnorm.cbv_vm env sigma c ctyp let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -39,13 +40,15 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else + let c = EConstr.Unsafe.to_constr c in let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) - in Reductionops.Stack.zip ~refold:true state + in + EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state) let strong_cbn flags = strong (whd_cbn flags) -- cgit v1.2.3 From 2db085e62f7797cc999518eb58983ac059763e1f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:13:08 +0100 Subject: Vnorm API using EConstr. --- proofs/redexpr.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 40a8077a72..348cd1bcbb 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,11 +24,8 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let c = EConstr.Unsafe.to_constr c in - let ctyp = Retyping.get_type_of env sigma c in - if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then - error "vm_compute does not support existential variables."; - Vnorm.cbv_vm env sigma c ctyp + let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" -- cgit v1.2.3 From 6bd193ff409b01948751525ce0f905916d7a64bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:38:35 +0100 Subject: Nativenorm API using EConstr. --- proofs/redexpr.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 348cd1bcbb..62fe2c17ca 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -37,9 +37,8 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let c = EConstr.Unsafe.to_constr c in - let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c ctyp + let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = let (state,_) = -- 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. --- proofs/redexpr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 62fe2c17ca..19e72e697f 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,7 +24,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = @@ -37,7 +37,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = -- cgit v1.2.3 From b77579ac873975a15978c5a4ecf312d577746d26 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 21:59:18 +0100 Subject: Tacred API using EConstr. --- proofs/redexpr.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 19e72e697f..d4a58da326 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -200,6 +200,9 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) +let out_with_occurrences' (occs,c) = + (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c) + let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl @@ -239,8 +242,8 @@ let reduction_of_red_expr env = (e_red (strong_cbn (make_flag f)), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) - | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) - | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) + | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast) + | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> -- 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. --- proofs/redexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d4a58da326..a830e25d9e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -44,7 +44,7 @@ let whd_cbn flags env sigma t = let (state,_) = (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) in - EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state) + Reductionops.Stack.zip ~refold:true sigma state let strong_cbn flags = strong (whd_cbn flags) -- 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 --- proofs/redexpr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index a830e25d9e..8878051c89 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = let ctyp = Retyping.get_type_of env sigma c in - Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) + Vnorm.cbv_vm env sigma c ctyp let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -38,7 +38,7 @@ let cbv_native env sigma c = cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) + Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = -- cgit v1.2.3 From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- proofs/redexpr.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8878051c89..0fe5c73f15 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -11,6 +11,7 @@ open CErrors open Util open Names open Term +open EConstr open Declarations open Globnames open Genredexpr @@ -200,9 +201,6 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let out_with_occurrences' (occs,c) = - (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c) - let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl @@ -242,8 +240,8 @@ let reduction_of_red_expr env = (e_red (strong_cbn (make_flag f)), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) - | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast) - | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast) + | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) + | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> @@ -256,9 +254,12 @@ let reduction_of_red_expr env = in reduction_of_red_expr +let subst_mps subst c = + EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) + let subst_red_expr subs = Miscops.map_red_expr_gen - (Mod_subst.subst_mps subs) + (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) -- cgit v1.2.3