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. --- stm/lemmas.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 55f33be399..9896d5a93c 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -108,7 +108,7 @@ let find_mutually_recursive_statements thms = (* Cofixpoint or fixpoint w/o explicit decreasing argument *) | None | Some (None, CStructRec) -> let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> fst (whd_all_stack env Evd.empty c)) + (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c)))) (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> @@ -122,8 +122,8 @@ let find_mutually_recursive_statements thms = []) 0 (List.rev whnf_hyp_hds)) in let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in - match kind_of_term whnf_ccl with + let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in + match kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> -- 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. --- stm/stm.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 23d68c4b86..6012e3d2d9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1703,9 +1703,10 @@ end = struct (* {{{ *) Future.purify (fun () -> let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in + let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in if not ( - Evarutil.is_ground_term sigma0 Evd.(evar_concl g) && - List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) + is_ground Evd.(evar_concl g) && + List.for_all (Context.Named.Declaration.for_all is_ground) Evd.(evar_context g)) then CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^ @@ -1719,7 +1720,7 @@ end = struct (* {{{ *) | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> let t = Evarutil.nf_evar sigma t in - if Evarutil.is_ground_term sigma t then + if Evarutil.is_ground_term sigma (EConstr.of_constr t) then RespBuiltSubProof (t, Evd.evar_universe_context sigma) else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () -- 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. --- stm/lemmas.ml | 4 ++-- stm/stm.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 9896d5a93c..04f888a84d 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -393,7 +393,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with + match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -401,7 +401,7 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with + in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false diff --git a/stm/stm.ml b/stm/stm.ml index 6012e3d2d9..d60412c0cd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1792,7 +1792,7 @@ end = struct (* {{{ *) str"uc=" ++ Evd.pr_evar_universe_context uc))); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> - Tactics.exact_no_check pt) + Tactics.exact_no_check (EConstr.of_constr pt)) with TacTask.NoProgress -> if solve then Tacticals.New.tclSOLVE [] else tclUNIT () }) -- cgit v1.2.3 From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- stm/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 04f888a84d..9942e911ab 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -466,7 +466,7 @@ let start_proof_com ?inference_hook kind thms hook = evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, - (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), + (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) thms 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. --- stm/lemmas.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 9942e911ab..e3f1c1ac28 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -461,6 +461,7 @@ let start_proof_com ?inference_hook kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in + let t' = EConstr.Unsafe.to_constr t' in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); -- cgit v1.2.3 From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- stm/lemmas.ml | 6 +++--- stm/lemmas.mli | 6 +++--- stm/stm.ml | 4 +++- 3 files changed, 9 insertions(+), 7 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index e3f1c1ac28..77fb960e16 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in @@ -461,13 +461,12 @@ let start_proof_com ?inference_hook kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - let t' = EConstr.Unsafe.to_constr t' in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, - (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx), + (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) thms in @@ -519,6 +518,7 @@ let save_proof ?proof = function | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in + let typ = EConstr.Unsafe.to_constr typ in let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) let pproofs, _univs = diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 39c089be9f..681413a297 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -19,17 +19,17 @@ val call_hook : Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a (** A hook start_proof calls on the type of the definition being started *) -val set_start_hook : (types -> unit) -> unit +val set_start_hook : (EConstr.types -> unit) -> unit val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> + ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> + ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit diff --git a/stm/stm.ml b/stm/stm.ml index d60412c0cd..47e806929b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1719,8 +1719,10 @@ end = struct (* {{{ *) match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> + let t = EConstr.of_constr t in let t = Evarutil.nf_evar sigma t in - if Evarutil.is_ground_term sigma (EConstr.of_constr t) then + if Evarutil.is_ground_term sigma t then + let t = EConstr.Unsafe.to_constr t in RespBuiltSubProof (t, Evd.evar_universe_context sigma) else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () -- cgit v1.2.3 From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 23:48:28 +0100 Subject: Moving printing code from Evd to Termops. --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 47e806929b..6f5da37f4a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1791,7 +1791,7 @@ end = struct (* {{{ *) prerr_endline (fun () -> string_of_ppcmds(hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ - str"uc=" ++ Evd.pr_evar_universe_context uc))); + str"uc=" ++ Termops.pr_evar_universe_context uc))); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check (EConstr.of_constr pt)) -- cgit v1.2.3