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. --- plugins/firstorder/instances.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index eebd974ea8..a3513692c5 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t= let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (whd_all env evmap typ) in + let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in match nam with Name id -> id | Anonymous -> dummy_bvid in -- cgit v1.2.3 From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- plugins/firstorder/instances.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a3513692c5..44bdb585a1 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in let evmap, _ = - try Typing.type_of (pf_env gl) evmap gt + try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt) with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) -- cgit v1.2.3 From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 19:52:48 +0100 Subject: Tacmach API using EConstr. --- plugins/firstorder/instances.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 44bdb585a1..6c245063c8 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t= let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_unsafe_type_of gl idc in + let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in -- 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. --- plugins/firstorder/instances.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 6c245063c8..a320b47aa3 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -117,6 +117,7 @@ let mk_open_instance id idc gl m t= let nid=(fresh_id avoid var_id gl) in let evmap = Sigma.Unsafe.of_evar_map evmap in let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + let c = EConstr.Unsafe.to_constr c in let evmap = Sigma.to_evar_map evmap in let decl = LocalAssum (Name nid, c) in aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in @@ -131,13 +132,13 @@ let left_instance_tac (inst,id) continue seq= if lookup (id,None) seq then tclFAIL 0 (Pp.str "already done") else - tclTHENS (Proofview.V82.of_tactic (cut dom)) + tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom))) [tclTHENLIST [Proofview.V82.of_tactic introf; pf_constr_of_global id (fun idc -> (fun gls-> Proofview.V82.of_tactic (generalize - [mkApp(idc, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls)); + [EConstr.of_constr (mkApp(idc, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|]))]) gls)); Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; @@ -154,14 +155,15 @@ let left_instance_tac (inst,id) continue seq= let gt= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in + let gt = EConstr.of_constr gt in let evmap, _ = - try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt) + try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) else pf_constr_of_global id (fun idc -> - Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])])) + Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(idc,[|t|]))])) in tclTHENLIST [special_generalize; @@ -172,16 +174,16 @@ let left_instance_tac (inst,id) continue seq= let right_instance_tac inst continue seq= match inst with Phantom dom -> - tclTHENS (Proofview.V82.of_tactic (cut dom)) + tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom))) [tclTHENLIST [Proofview.V82.of_tactic introf; (fun gls-> Proofview.V82.of_tactic (split (ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); + [EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY (Proofview.V82.of_tactic assumption)] | Real ((0,t),_) -> - (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t]))) + (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t]))) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") -- 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. --- plugins/firstorder/instances.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a320b47aa3..24d4346d9a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t= let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in + let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in match nam with Name id -> id | Anonymous -> dummy_bvid in -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- plugins/firstorder/instances.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 24d4346d9a..2881b53339 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t= let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in + let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in match nam with Name id -> id | Anonymous -> dummy_bvid in -- cgit v1.2.3 From 01849481fbabc3a3fa6c483e703996b01e37fca5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:25:11 +0100 Subject: Removing compatibility layers from Tacticals --- plugins/firstorder/instances.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 2881b53339..ef8172de41 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t= let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in + let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in @@ -127,6 +127,7 @@ let mk_open_instance id idc gl m t= (* tactics *) let left_instance_tac (inst,id) continue seq= + let open EConstr in match inst with Phantom dom-> if lookup (id,None) seq then @@ -137,8 +138,8 @@ let left_instance_tac (inst,id) continue seq= [Proofview.V82.of_tactic introf; pf_constr_of_global id (fun idc -> (fun gls-> Proofview.V82.of_tactic (generalize - [EConstr.of_constr (mkApp(idc, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|]))]) gls)); + [mkApp(idc, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls)); Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; @@ -152,18 +153,19 @@ let left_instance_tac (inst,id) continue seq= pf_constr_of_global id (fun idc -> fun gl-> let evmap,rc,ot = mk_open_instance id idc gl m t in + let ot = EConstr.of_constr ot in let gt= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in - let gt = EConstr.of_constr gt in let evmap, _ = try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) else + let t = EConstr.of_constr t in pf_constr_of_global id (fun idc -> - Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(idc,[|t|]))])) + Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])])) in tclTHENLIST [special_generalize; -- 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. --- plugins/firstorder/instances.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/firstorder/instances.ml') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index ef8172de41..9dc2a51a61 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -117,10 +117,9 @@ let mk_open_instance id idc gl m t= let nid=(fresh_id avoid var_id gl) in let evmap = Sigma.Unsafe.of_evar_map evmap in let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let c = EConstr.Unsafe.to_constr c in let evmap = Sigma.to_evar_map evmap in let decl = LocalAssum (Name nid, c) in - aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in + aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in evmap, decls, revt -- cgit v1.2.3