aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/decl_expr.mli108
-rw-r--r--proofs/decl_mode.ml121
-rw-r--r--proofs/decl_mode.mli73
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/pfedit.ml22
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--proofs/proof_trees.ml25
-rw-r--r--proofs/proof_trees.mli4
-rw-r--r--proofs/proof_type.ml9
-rw-r--r--proofs/proof_type.mli11
-rw-r--r--proofs/refiner.ml122
-rw-r--r--proofs/refiner.mli10
14 files changed, 473 insertions, 50 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
new file mode 100644
index 0000000000..24af3842cb
--- /dev/null
+++ b/proofs/decl_expr.mli
@@ -0,0 +1,108 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Util
+open Tacexpr
+
+type ('constr,'tac) justification =
+ By_tactic of 'tac
+| Automated of 'constr list
+
+type 'it statement =
+ {st_label:name;
+ st_it:'it}
+
+type thesis_kind =
+ Plain
+ | Sub of int
+ | For of identifier
+
+type 'this or_thesis =
+ This of 'this
+ | Thesis of thesis_kind
+
+type side = Lhs | Rhs
+
+type elim_type =
+ ET_Case_analysis
+ | ET_Induction
+
+type block_type =
+ B_proof
+ | B_claim
+ | B_focus
+ | B_elim of elim_type
+
+type ('it,'constr,'tac) cut =
+ {cut_stat: 'it statement;
+ cut_by: ('constr,'tac) justification}
+
+type ('var,'constr) hyp =
+ Hvar of 'var
+ | Hprop of 'constr statement
+
+type ('constr,'tac) casee =
+ Real of 'constr
+ | Virtual of ('constr,'constr,'tac) cut
+
+type ('hyp,'constr,'pat,'tac) bare_proof_instr =
+ | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
+ | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
+ | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
+ | Pcut of ('constr or_thesis,'constr,'tac) cut
+ | Prew of side * ('constr,'constr,'tac) cut
+ | Passume of ('hyp,'constr) hyp list
+ | Plet of ('hyp,'constr) hyp list
+ | Pgiven of ('hyp,'constr) hyp list
+ | Pconsider of 'constr*('hyp,'constr) hyp list
+ | Pclaim of 'constr statement
+ | Pfocus of 'constr statement
+ | Pdefine of identifier * 'hyp list * 'constr
+ | Pcast of identifier or_thesis * 'constr
+ | Psuppose of ('hyp,'constr) hyp list
+ | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+ | Ptake of 'constr list
+ | Pper of elim_type * ('constr,'tac) casee
+ | Pend of block_type
+ | Pescape
+
+type emphasis = int
+
+type ('hyp,'constr,'pat,'tac) gen_proof_instr=
+ {emph: emphasis;
+ instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
+
+
+type raw_proof_instr =
+ ((identifier*(Topconstr.constr_expr option)) located,
+ Topconstr.constr_expr,
+ Topconstr.cases_pattern_expr,
+ raw_tactic_expr) gen_proof_instr
+
+type glob_proof_instr =
+ ((identifier*(Genarg.rawconstr_and_expr option)) located,
+ Genarg.rawconstr_and_expr,
+ Topconstr.cases_pattern_expr,
+ Tacexpr.glob_tactic_expr) gen_proof_instr
+
+type proof_pattern =
+ {pat_vars: Term.types statement list;
+ pat_aliases: (Term.constr*Term.types) statement list;
+ pat_constr: Term.constr;
+ pat_typ: Term.types;
+ pat_pat: Rawterm.cases_pattern;
+ pat_expr: Topconstr.cases_pattern_expr}
+
+type proof_instr =
+ (Term.constr statement,
+ Term.constr,
+ proof_pattern,
+ Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
new file mode 100644
index 0000000000..094c562532
--- /dev/null
+++ b/proofs/decl_mode.ml
@@ -0,0 +1,121 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Evd
+open Util
+
+let daimon_flag = ref false
+
+let set_daimon_flag () = daimon_flag:=true
+let clear_daimon_flag () = daimon_flag:=false
+let get_daimon_flag () = !daimon_flag
+
+type command_mode =
+ Mode_tactic
+ | Mode_proof
+ | Mode_none
+
+let mode_of_pftreestate pts =
+ let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
+ if goal.evar_extra = None then
+ Mode_tactic
+ else
+ Mode_proof
+
+let get_current_mode () =
+ try
+ mode_of_pftreestate (Pfedit.get_pftreestate ())
+ with _ -> Mode_none
+
+let check_not_proof_mode str =
+ if get_current_mode () = Mode_proof then
+ error str
+
+type split_tree=
+ Push of (Idset.t * split_tree)
+ | Split of (Idset.t * inductive * (Idset.t * split_tree) option array)
+ | Pop of split_tree
+ | End_of_branch of (identifier * int)
+
+type elim_kind =
+ EK_dep of split_tree
+ | EK_nodep
+ | EK_unknown
+
+type per_info =
+ {per_casee:constr;
+ per_ctype:types;
+ per_ind:inductive;
+ per_pred:constr;
+ per_args:constr list;
+ per_params:constr list;
+ per_nparams:int}
+
+type stack_info =
+ Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
+ | Suppose_case
+ | Claim
+ | Focus_claim
+
+type pm_info =
+ { pm_last: Names.name (* anonymous if none *);
+ pm_hyps: Idset.t;
+ pm_partial_goal : constr ; (* partial goal construction *)
+ pm_subgoals : (metavariable*constr) list;
+ pm_stack : stack_info list }
+
+let pm_in,pm_out = Dyn.create "pm_info"
+
+let get_info gl=
+ match gl.evar_extra with
+ None -> invalid_arg "get_info"
+ | Some extra ->
+ try pm_out extra with _ -> invalid_arg "get_info"
+
+let get_stack pts =
+ let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
+ info.pm_stack
+
+let get_top_stack pts =
+ let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
+ info.pm_stack
+
+let get_end_command pts =
+ match mode_of_pftreestate pts with
+ Mode_proof ->
+ Some
+ begin
+ match get_top_stack pts with
+ [] -> "\"end proof\""
+ | Claim::_ -> "\"end claim\""
+ | Focus_claim::_-> "\"end focus\""
+ | (Suppose_case :: Per (et,_,_,_) :: _
+ | Per (et,_,_,_) :: _ ) ->
+ begin
+ match et with
+ Decl_expr.ET_Case_analysis ->
+ "\"end cases\" or start a new case"
+ | Decl_expr.ET_Induction ->
+ "\"end induction\" or start a new case"
+ end
+ | _ -> anomaly "lonely suppose"
+ end
+ | Mode_tactic ->
+ begin
+ try
+ ignore
+ (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
+ Some "\"return\""
+ with Not_found -> None
+ end
+ | Mode_none ->
+ error "no proof in progress"
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
new file mode 100644
index 0000000000..0dd1cb33c3
--- /dev/null
+++ b/proofs/decl_mode.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Evd
+open Tacmach
+
+val set_daimon_flag : unit -> unit
+val clear_daimon_flag : unit -> unit
+val get_daimon_flag : unit -> bool
+
+type command_mode =
+ Mode_tactic
+ | Mode_proof
+ | Mode_none
+
+val mode_of_pftreestate : pftreestate -> command_mode
+
+val get_current_mode : unit -> command_mode
+
+val check_not_proof_mode : string -> unit
+
+type split_tree=
+ Push of (Idset.t * split_tree)
+ | Split of (Idset.t * inductive * (Idset.t*split_tree) option array)
+ | Pop of split_tree
+ | End_of_branch of (identifier * int)
+
+type elim_kind =
+ EK_dep of split_tree
+ | EK_nodep
+ | EK_unknown
+
+
+type per_info =
+ {per_casee:constr;
+ per_ctype:types;
+ per_ind:inductive;
+ per_pred:constr;
+ per_args:constr list;
+ per_params:constr list;
+ per_nparams:int}
+
+type stack_info =
+ Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
+ | Suppose_case
+ | Claim
+ | Focus_claim
+
+type pm_info =
+ { pm_last: Names.name (* anonymous if none *);
+ pm_hyps: Idset.t;
+ pm_partial_goal : constr ; (* partial goal construction *)
+ pm_subgoals : (metavariable*constr) list;
+ pm_stack : stack_info list }
+
+val pm_in : pm_info -> Dyn.t
+
+val get_info : Proof_type.goal -> pm_info
+
+val get_end_command : pftreestate -> string option
+
+val get_stack : pftreestate -> stack_info list
+
+val get_top_stack : pftreestate -> stack_info list
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d5ea25bd30..b0f933a504 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -22,7 +22,7 @@ open Refiner
(* w_tactic pour instantiate *)
-let w_refine env ev rawc evd =
+let w_refine ev rawc evd =
if Evd.is_defined (evars_of evd) ev then
error "Instantiate called on already-defined evar";
let e_info = Evd.find (evars_of evd) ev in
@@ -45,5 +45,5 @@ let instantiate_pf_com n com pfts =
let env = Evd.evar_env evi in
let rawc = Constrintern.intern_constr sigma env com in
let evd = create_evar_defs sigma in
- let evd' = w_refine env sp rawc evd in
+ let evd' = w_refine sp rawc evd in
change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 090671e046..7b9da802c1 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -18,7 +18,7 @@ open Refiner
(* Refinement of existential variables. *)
-val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
+val w_refine : evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
val instantiate_pf_com :
int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 209c3bb65f..b5c8011051 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -88,7 +88,7 @@ let clear_hyps ids gl =
if List.mem id' cleared_ids then
error (string_of_id id'^" is used in conclusion"))
(global_vars_set env ncl);
- mk_goal nhyps ncl
+ mk_goal nhyps ncl gl.evar_extra
(* The ClearBody tactic *)
@@ -264,6 +264,7 @@ let goal_type_of env sigma c =
let rec mk_refgoals sigma goal goalacc conclty trm =
let env = evar_env goal in
let hyps = goal.evar_hyps in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
(*
if not (occur_meta trm) then
let t'ty = (unsafe_machine env sigma trm).uj_type in
@@ -315,6 +316,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
and mk_hdgoals sigma goal goalacc trm =
let env = evar_env goal in
let hyps = goal.evar_hyps in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
@@ -392,6 +394,7 @@ let prim_refiner r sigma goal =
let env = evar_env goal in
let sign = goal.evar_hyps in
let cl = goal.evar_concl in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
match r with
(* Logical rules *)
| Intro id ->
@@ -474,7 +477,8 @@ let prim_refiner r sigma goal =
let _ = find_coinductive env sigma b in ()
with Not_found ->
error ("All methods must construct elements " ^
- "in coinductive types")
+ "in coinductiv-> goal
+e types")
in
let all = (f,cl)::others in
List.iter (fun (_,c) -> check_is_coind env c) all;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f724589f69..c6cb86dc92 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -150,6 +150,14 @@ let subtree_solved () =
is_complete_proof (proof_of_pftreestate pts) &
not (is_top_pftreestate pts)
+let tree_solved () =
+ let pts = get_pftreestate () in
+ is_complete_proof (proof_of_pftreestate pts)
+
+let top_tree_solved () =
+ let pts = get_pftreestate () in
+ is_complete_proof (proof_of_pftreestate (top_of_tree pts))
+
(*********************************************************************)
(* Undo functions *)
(*********************************************************************)
@@ -243,7 +251,7 @@ let set_end_tac tac =
(*********************************************************************)
let start_proof na str sign concl hook =
- let top_goal = mk_goal sign concl in
+ let top_goal = mk_goal sign concl None in
let ts = {
top_end_tac = None;
top_goal = top_goal;
@@ -253,7 +261,6 @@ let start_proof na str sign concl hook =
start(na,ts);
set_current_proof na
-
let solve_nth k tac =
let pft = get_pftreestate () in
if not (List.mem (-1) (cursor_of_pftreestate pft)) then
@@ -309,7 +316,6 @@ let traverse_prev_unproven () = mutate prev_unproven
let traverse_next_unproven () = mutate next_unproven
-
(* The goal focused on *)
let focus_n = ref 0
let make_focus n = focus_n := n
@@ -317,5 +323,11 @@ let focus () = !focus_n
let focused_goal () = let n = !focus_n in if n=0 then 1 else n
let reset_top_of_tree () =
- let pts = get_pftreestate () in
- if not (is_top_pftreestate pts) then mutate top_of_tree
+ mutate top_of_tree
+
+let reset_top_of_script () =
+ mutate (fun pts ->
+ try
+ up_until_matching_rule is_proof_instr pts
+ with Not_found -> top_of_tree pts)
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8871e7e00c..c3d531c692 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -172,8 +172,12 @@ val make_focus : int -> unit
val focus : unit -> int
val focused_goal : unit -> int
val subtree_solved : unit -> bool
+val tree_solved : unit -> bool
+val top_tree_solved : unit -> bool
val reset_top_of_tree : unit -> unit
+val reset_top_of_script : unit -> unit
+
val traverse : int -> unit
val traverse_nth_goal : int -> unit
val traverse_next_unproven : unit -> unit
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 73cc5d2736..c7a32682aa 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -18,6 +18,7 @@ open Sign
open Evd
open Environ
open Evarutil
+open Decl_expr
open Proof_type
open Tacred
open Typing
@@ -32,9 +33,9 @@ let is_bind = function
(* Functions on goals *)
-let mk_goal hyps cl =
+let mk_goal hyps cl extra =
{ evar_hyps = hyps; evar_concl = cl;
- evar_body = Evar_empty}
+ evar_body = Evar_empty; evar_extra = extra }
(* Functions on proof trees *)
@@ -52,7 +53,7 @@ let children_of_proof pf =
let goal_of_proof pf = pf.goal
let subproof_of_proof pf = match pf.ref with
- | Some (Tactic (_,pf), _) -> pf
+ | Some (Nested (_,pf), _) -> pf
| _ -> failwith "subproof_of_proof"
let status_of_proof pf = pf.open_subgoals
@@ -62,7 +63,7 @@ let is_complete_proof pf = pf.open_subgoals = 0
let is_leaf_proof pf = (pf.ref = None)
let is_tactic_proof pf = match pf.ref with
- | Some (Tactic _, _) -> true
+ | Some (Nested (Tactic _,_),_) -> true
| _ -> false
@@ -72,6 +73,22 @@ let pf_lookup_name_as_renamed env ccl s =
let pf_lookup_index_as_renamed env ccl n =
Detyping.lookup_index_as_renamed env ccl n
+(* Functions on rules (Proof mode) *)
+
+let is_dem_rule = function
+ Decl_proof _ -> true
+ | _ -> false
+
+let is_proof_instr = function
+ Nested(Proof_instr (_,_),_) -> true
+ | _ -> false
+
+let is_focussing_command = function
+ Decl_proof b -> b
+ | Nested (Proof_instr (b,_),_) -> b
+ | _ -> false
+
+
(*********************************************************************)
(* Pretty printing functions *)
(*********************************************************************)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 1b691e2584..dcbddbd9e8 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -21,7 +21,7 @@ open Proof_type
(* This module declares readable constraints, and a few utilities on
constraints and proof trees *)
-val mk_goal : named_context_val -> constr -> goal
+val mk_goal : named_context_val -> constr -> Dyn.t option -> goal
val rule_of_proof : proof_tree -> rule
val ref_of_proof : proof_tree -> (rule * proof_tree list)
@@ -36,6 +36,8 @@ val is_tactic_proof : proof_tree -> bool
val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option
val pf_lookup_index_as_renamed : env -> constr -> int -> int option
+val is_proof_instr : rule -> bool
+val is_focussing_command : rule -> bool
(*s Pretty printing functions. *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index db3c0e7e25..4037237026 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -16,6 +16,7 @@ open Libnames
open Term
open Util
open Tacexpr
+open Decl_expr
open Rawterm
open Genarg
open Nametab
@@ -52,9 +53,15 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Tactic of tactic_expr * proof_tree
+ | Nested of compound_rule * proof_tree
+ | Decl_proof of bool
+ | Daimon
| Change_evars
+and compound_rule=
+ | Tactic of tactic_expr
+ | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
+
and goal = evar_info
and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index e222730582..74c36c9811 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -16,6 +16,7 @@ open Libnames
open Term
open Util
open Tacexpr
+open Decl_expr
open Rawterm
open Genarg
open Nametab
@@ -46,7 +47,7 @@ type prim_rule =
evar_body = Evar_Empty;
evar_info = { pgm : [The Realizer pgm if any]
lc : [Set of evar num occurring in subgoal] }}
- sigma = { stamp = [an int characterizing the ed field, for quick compare]
+ sigma = { stamp = [an int chardacterizing the ed field, for quick compare]
ed : [A set of existential variables depending in the subgoal]
number of first evar,
it = { evar_concl = [the type of first evar]
@@ -80,9 +81,15 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Tactic of tactic_expr * proof_tree
+ | Nested of compound_rule * proof_tree
+ | Decl_proof of bool
+ | Daimon
| Change_evars
+and compound_rule=
+ | Tactic of tactic_expr
+ | Proof_instr of bool * proof_instr
+
and goal = evar_info
and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ee4b672a18..48c9238e05 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -50,10 +50,10 @@ let norm_goal sigma gl =
let red_fun = Evarutil.nf_evar sigma in
let ncl = red_fun gl.evar_concl in
let ngl =
- { evar_concl = ncl;
- evar_hyps = map_named_val red_fun gl.evar_hyps;
- evar_body = gl.evar_body} in
- if Evd.eq_evar_info ngl gl then None else Some ngl
+ { gl with
+ evar_concl = ncl;
+ evar_hyps = map_named_val red_fun gl.evar_hyps } in
+ if Evd.eq_evar_info ngl gl then None else Some ngl
(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -91,9 +91,9 @@ let rec frontier p =
(List.flatten gll,
(fun retpfl ->
let pfl' = mapshape (List.map List.length gll) vl retpfl in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}))
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}))
let rec frontier_map_rec f n p =
@@ -111,9 +111,9 @@ let rec frontier_map_rec f n p =
(fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
(n,[]) pfl in
let pfl' = List.rev rpfl' in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}
let frontier_map f n p =
let nmax = p.open_subgoals in
@@ -137,9 +137,9 @@ let rec frontier_mapi_rec f i p =
(fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
(i,[]) pfl in
let pfl' = List.rev rpfl' in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}
let frontier_mapi f p = frontier_mapi_rec f 1 p
@@ -152,10 +152,10 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
(* leaf g is the canonical incomplete proof of a goal g *)
-let leaf g = {
- open_subgoals = 1;
- goal = g;
- ref = None }
+let leaf g =
+ { open_subgoals = 1;
+ goal = g;
+ ref = None }
(* Tactics table. *)
@@ -187,15 +187,19 @@ let lookup_tactic s =
let check_subproof_connection gl spfl =
list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
-let abstract_tactic_expr te tacfun gls =
- let (sgl_sigma,v) = tacfun gls in
- let hidden_proof = v (List.map leaf sgl_sigma.it) in
+
+let abstract_operation syntax semantics gls =
+ let (sgl_sigma,validation) = semantics gls in
+ let hidden_proof = validation (List.map leaf sgl_sigma.it) in
(sgl_sigma,
fun spfl ->
assert (check_subproof_connection sgl_sigma.it spfl);
{ open_subgoals = and_status (List.map pf_status spfl);
goal = gls.it;
- ref = Some(Tactic(te,hidden_proof),spfl) })
+ ref = Some(Nested(syntax,hidden_proof),spfl)})
+
+let abstract_tactic_expr te tacfun gls =
+ abstract_operation (Tactic te) tacfun gls
let refiner = function
| Prim pr as r ->
@@ -209,8 +213,21 @@ let refiner = function
goal = goal_sigma.it;
ref = Some(r,spfl) })))
- | Tactic _ -> failwith "Refiner: should not occur"
+
+ | Nested (_,_) | Decl_proof _ ->
+ failwith "Refiner: should not occur"
+ (* Daimon is a canonical unfinished proof *)
+
+ | Daimon ->
+ fun gls ->
+ ({it=[];sigma=gls.sigma},
+ fun spfl ->
+ assert (spfl=[]);
+ { open_subgoals = 0;
+ goal = gls.it;
+ ref = Some(Daimon,[])})
+
(* [Local_constraints lc] makes the local constraints be [lc] and
normalizes evars *)
@@ -271,14 +288,16 @@ let extract_open_proof sigma pf =
let rec proof_extractor vl = function
| {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
- | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
+ | {ref=Some(Nested(_,hidden_proof),spfl)} ->
let sgl,v = frontier hidden_proof in
let flat_proof = v spfl in
proof_extractor vl flat_proof
-
+
| {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
+
+ | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
- | {ref=None;goal=goal} ->
+ | {ref=(None|Some(Daimon,[]));goal=goal} ->
let visible_rels =
map_succeed
(fun id ->
@@ -680,9 +699,9 @@ let descend n p =
let pf' = List.hd pfl' in
let spfl = left@(pf'::right) in
let newstatus = and_status (List.map pf_status spfl) in
- { open_subgoals = newstatus;
- goal = p.goal;
- ref = Some(r,spfl) }
+ { p with
+ open_subgoals = newstatus;
+ ref = Some(r,spfl) }
else
error "descend: validation"))
| _ -> assert false)
@@ -699,7 +718,7 @@ let traverse n pts = match n with
tpfsigma = pts.tpfsigma })
| -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
(match pts.tpf.ref with
- | Some (Tactic (_,spf),_) ->
+ | Some (Nested (_,spf),_) ->
let v = (fun pfl -> pts.tpf) in
{ tpf = spf;
tstack = (-1,v)::pts.tstack;
@@ -718,10 +737,11 @@ let app_tac sigr tac p =
sigr := gll.sigma;
v (List.map leaf gll.it)
-(* solve the nth subgoal with tactic tac *)
-let solve_nth_pftreestate n tac pts =
+(* modify proof state at current position *)
+
+let map_pftreestate f pts =
let sigr = ref pts.tpfsigma in
- let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+ let tpf' = f sigr pts.tpf in
let tpf'' =
if !sigr == pts.tpfsigma then tpf'
else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
@@ -729,6 +749,12 @@ let solve_nth_pftreestate n tac pts =
tpfsigma = !sigr;
tstack = pts.tstack }
+(* solve the nth subgoal with tactic tac *)
+
+let solve_nth_pftreestate n tac =
+ map_pftreestate
+ (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
+
let solve_pftreestate = solve_nth_pftreestate 1
(* This function implements a poor man's undo at the current goal.
@@ -880,6 +906,38 @@ let prev_unproven pts =
let rec top_of_tree pts =
if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
+let change_rule f pts =
+ let mark_top _ pt =
+ match pt.ref with
+ Some (oldrule,l) ->
+ {pt with ref=Some (f oldrule,l)}
+ | _ -> invalid_arg "change_rule" in
+ map_pftreestate mark_top pts
+
+let match_rule p pts =
+ match (proof_of_pftreestate pts).ref with
+ Some (r,_) -> p r
+ | None -> false
+
+let rec up_until_matching_rule p pts =
+ if is_top_pftreestate pts then
+ raise Not_found
+ else
+ let one_up = traverse 0 pts in
+ if match_rule p one_up then
+ pts
+ else
+ up_until_matching_rule p one_up
+
+let rec up_to_matching_rule p pts =
+ if match_rule p pts then
+ pts
+ else
+ if is_top_pftreestate pts then
+ raise Not_found
+ else
+ let one_up = traverse 0 pts in
+ up_to_matching_rule p one_up
(* Change evars *)
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 41b312e5db..097ff99a93 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -40,6 +40,7 @@ val lookup_tactic : string -> (closed_generic_argument list) -> tactic
(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
a single proof node *)
+val abstract_operation : compound_rule -> tactic -> tactic
val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
val abstract_tactic_expr : tactic_expr -> tactic -> tactic
val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
@@ -170,11 +171,14 @@ type pftreestate
val proof_of_pftreestate : pftreestate -> proof_tree
val cursor_of_pftreestate : pftreestate -> int list
val is_top_pftreestate : pftreestate -> bool
+val match_rule : (rule -> bool) -> pftreestate -> bool
val evc_of_pftreestate : pftreestate -> evar_map
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
+val map_pftreestate :
+ (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
@@ -193,6 +197,12 @@ val node_next_unproven : int -> pftreestate -> pftreestate
val next_unproven : pftreestate -> pftreestate
val prev_unproven : pftreestate -> pftreestate
val top_of_tree : pftreestate -> pftreestate
+val match_rule : (rule -> bool) -> pftreestate -> bool
+val up_until_matching_rule : (rule -> bool) ->
+ pftreestate -> pftreestate
+val up_to_matching_rule : (rule -> bool) ->
+ pftreestate -> pftreestate
+val change_rule : (rule -> rule) -> pftreestate -> pftreestate
val change_constraints_pftreestate
: evar_map -> pftreestate -> pftreestate
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:11:10 +0000