Diverses petites simplications de la machine de preuves.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 66 insertions, 56 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 09e9adbc5..ec90fc925 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -18,6 +18,7 @@ open Instantiate
 open Environ
 open Evd
 open Proof_type
+open Proof_trees
 open Logic
 open Reductionops
 open Tacmach
@@ -79,9 +80,18 @@ let applyHead n c wc =
   apprec n c (w_type_of wc c) wc
 
 let mimick_evar hdc nargs sp wc =
-  (w_Focusing_THEN sp
+  let evd = Evd.map wc.sigma sp in
+  let wc' = extract_decl sp wc in
+  let (wc'', c) = applyHead nargs hdc wc' in
+    if wc'==wc''
+    then w_Define sp c wc
+    else 
+      let wc''' = restore_decl sp evd wc'' in
+	w_Define sp c {it = wc.it ; sigma = wc'''.sigma}
+
+(*  (w_Focusing_THEN sp
      (applyHead nargs hdc)
-     (fun c wc -> w_Define sp c wc)) wc
+     (fun c wc -> w_Define sp c wc)) wc *)
 
 
 (* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes:
@@ -266,7 +276,10 @@ and w_resrec metas evars wc =
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
-let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc))
+(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
+let unifyTerms m n gls = 
+  tclIDTAC {it = gls.it; 
+	    sigma = (get_gc (fst (w_Unify CONV m n [] (Refiner.project_with_focus gls))))}
 
 let unify m gls =
   let n = pf_concl gls in unifyTerms m n gls
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 12f928e99..c88d949af 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -27,10 +27,8 @@ open Refiner
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
 let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
 
-type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a
 type w_tactic = named_context sigma -> named_context sigma
 
-
 let local_Constraints gs = refiner Change_evars gs
 
 let startWalk gls =
@@ -45,13 +43,6 @@ let startWalk gls =
              {it=gls'.it; sigma = get_gc (ids_it wc')})*)
       else error "Walking"))
 
-let walking_THEN wt rt gls =
-  let (wc,kONT) = startWalk gls in
-  let (wc',rslt) = wt wc in 
-  tclTHEN (kONT wc') (rt rslt) gls
-
-let walking wt = walking_THEN (fun wc -> (wt wc,())) (fun () -> tclIDTAC)
-
 let extract_decl sp evc =
   let evdmap = evc.sigma in
   let evd = Evd.map evdmap sp in 
@@ -71,7 +62,7 @@ let restore_decl sp evd evc =
  *
  * It is an error to cause SP to change state while we are focused on it. *)
 
-let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
+(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
                        (wc : named_context sigma) =
   let hyps  = wc.it
   and evd   = Evd.map wc.sigma sp in
@@ -82,29 +73,20 @@ let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
     wt' rslt wc
   else 
     let wc''' = restore_decl sp evd wc'' in 
-    wt' rslt {it = hyps; sigma = wc'''.sigma}
+    wt' rslt {it = hyps; sigma = wc'''.sigma} *)
       
 let w_add_sign (id,t) (wc : named_context sigma) =
   { it = Sign.add_named_decl (id,None,t) wc.it;
     sigma = wc.sigma }
 
-let ctxt_type_of evc c = 
-  type_of (Global.env_of_context evc.it) evc.sigma c
-
-let w_IDTAC wc = wc
-
-let w_Focusing sp wt = 
-  w_Focusing_THEN sp (fun wc -> (wt wc,())) (fun _ -> w_IDTAC)
-
 let w_Focus sp wc = extract_decl sp wc
 
 let w_Underlying wc = wc.sigma
 let w_whd wc c      = Evarutil.whd_castappevar (w_Underlying wc) c
-let w_type_of wc c  = ctxt_type_of wc c
+let w_type_of wc c  =
+  type_of (Global.env_of_context wc.it) wc.sigma c
 let w_env     wc    = get_env wc
 let w_hyps    wc    = named_context (get_env wc)
-let w_ORELSE wt1 wt2 wc = 
-  try wt1 wc with e when catchable_exception e -> wt2 wc
 let w_defined_const wc sp = defined_constant (w_env wc) sp
 let w_defined_evar wc k      = Evd.is_defined (w_Underlying wc) k
 let w_const_value wc         = constant_value (w_env wc)
@@ -123,7 +105,7 @@ let w_Define sp c wc =
   let spdecl = Evd.map (w_Underlying wc) sp in
   let cty = 
     try 
-      ctxt_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
+      w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
     with Not_found -> 
       error "Instantiation contains unlegal variables"
   in 
@@ -141,23 +123,42 @@ let w_Define sp c wc =
 (* Instantiation of existential variables *)
 (******************************************)
 
-let instantiate_pf n c pfts = 
-  let gls = top_goal_of_pftreestate pfts in
-  let (wc,_) = startWalk gls in
-  let sigma  = (w_Underlying wc) in 
-  let (sp,_) = 
-    try 
-      List.nth (Evd.non_instantiated sigma) (n-1)
-    with Failure _ -> 
-      error "not so many uninstantiated existential variables"
+(* The instantiate tactic *)
+
+let evars_of evc c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+    | _ -> fold_constr evrec acc c
   in 
-  let wc' = w_Define sp c wc in 
-  let newgc = w_Underlying wc' in 
-  change_constraints_pftreestate newgc pfts
+  evrec [] c
+
+let instantiate n c gl = 
+  let wc = Refiner.project_with_focus gl in
+  let evl = evars_of wc.sigma gl.it.evar_concl in
+    if List.length evl < n then error "not enough evars";
+    let (n,_) as k = destEvar (List.nth evl (n-1)) in 
+      if Evd.is_defined wc.sigma n then 
+	error "Instantiate called on already-defined evar";
+      let wc' = w_Define n c wc in 
+	tclIDTAC {it = gl.it ; sigma = wc'.sigma}
+
+let pfic gls c =
+  let evc = gls.sigma in 
+  Astterm.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
+
+let instantiate_tac = function
+  | [Integer n; Command com] ->
+      (fun gl -> instantiate n (pfic gl com) gl)
+  | [Integer n; Constr c] ->
+      (fun gl -> instantiate n c gl)
+  | _ -> invalid_arg "Instantiate called with bad arguments"
+
+(* vernac command existential *)
 
 let instantiate_pf_com n com pfts = 
   let gls = top_goal_of_pftreestate pfts in
-  let (wc,_) = startWalk gls in
+  let wc = project_with_focus gls in
   let sigma = (w_Underlying wc) in 
   let (sp,evd) = 
     try
@@ -167,5 +168,7 @@ let instantiate_pf_com n com pfts =
   in 
   let c = Astterm.interp_constr sigma (Evarutil.evar_env evd) com in     
   let wc' = w_Define sp c wc in
-  let newgc = w_Underlying wc' in
+  let newgc = (w_Underlying wc') in
   change_constraints_pftreestate newgc pfts
+
+
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 9f09cfba5..4138a49c3 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -32,7 +32,6 @@ val rc_of_glsigma : goal sigma -> named_context sigma
     hyps  : context of the goal;
     decls : a superset of evars of which the goal may depend })]
 *)
-type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a
 
 (* A [w_tactic] is a tactic which modifies the a set of evars of which
 a goal depend, either by instantiating one, or by declaring a new
@@ -45,10 +44,12 @@ val local_Constraints :
 val startWalk : 
   goal sigma -> named_context sigma * (named_context sigma -> tactic)
 
-val walking_THEN    : 'a result_w_tactic -> ('a -> tactic) -> tactic
-val walking         : w_tactic -> tactic
-val w_Focusing_THEN : 
-  evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
+val extract_decl : evar -> named_context sigma -> named_context sigma
+
+val restore_decl : evar -> evar_info -> named_context sigma -> named_context sigma
+
+(* val w_Focusing_THEN : 
+  evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic *)
 
 val w_Declare    : evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
@@ -61,9 +62,6 @@ val w_type_of    : named_context sigma -> constr -> constr
 val w_add_sign   : (identifier * types) -> named_context sigma 
                      -> named_context sigma
 
-val w_IDTAC      : w_tactic
-val w_ORELSE     : w_tactic -> w_tactic -> w_tactic
-val ctxt_type_of : named_context sigma -> constr -> constr
 val w_whd_betadeltaiota : named_context sigma -> constr -> constr
 val w_hnf_constr        : named_context sigma -> constr -> constr
 val w_conv_x            : named_context sigma -> constr -> constr -> bool
@@ -71,5 +69,6 @@ val w_const_value       : named_context sigma -> constant -> constr
 val w_defined_const     : named_context sigma -> constant -> bool
 val w_defined_evar      : named_context sigma -> existential_key -> bool
 
-val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate : evar -> constr -> tactic
+val instantiate_tac : tactic_arg list -> tactic
 val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f6424df8d..2b8416eae 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -223,7 +223,7 @@ let solve_nth k tac =
 let by tac = mutate (solve_pftreestate tac)
 
 let instantiate_nth_evar_com n c =
-  mutate (instantiate_pf_com n c)
+  mutate (Evar_refiner.instantiate_pf_com n c)
 
 let traverse n = mutate (traverse n)
  
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5e4b6b495..03f3d906c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -163,8 +163,6 @@ let prev_unproven           = prev_unproven
 let top_of_tree             = top_of_tree
 let frontier                = frontier
 let change_constraints_pftreestate = change_constraints_pftreestate
-let instantiate_pf     = Evar_refiner.instantiate_pf
-let instantiate_pf_com = Evar_refiner.instantiate_pf_com
 
 (*************************************************)
 (* Tacticals re-exported from the Refiner module.*)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 0a685a447..7dda94210 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -89,7 +89,7 @@ val frontier : transformation_tactic
 
 (*s Functions for handling the state of the proof editor. *)
 
-type pftreestate
+type pftreestate = Refiner.pftreestate
 
 val proof_of_pftreestate    : pftreestate -> proof_tree
 val cursor_of_pftreestate   : pftreestate -> int list
@@ -114,9 +114,6 @@ val prev_unproven           : pftreestate -> pftreestate
 val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   evar_map -> pftreestate -> pftreestate
-val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
-val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
-
 
 (*s Tacticals re-exported from the Refiner module. *)