module Proof_trees

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

7 files changed, 120 insertions, 79 deletions

diff --git a/.depend b/.depend
index d05d68444b..659a3c9a18 100644
--- a/.depend
+++ b/.depend
@@ -41,15 +41,20 @@ library/libobject.cmi: kernel/names.cmi
 library/nametab.cmi: kernel/names.cmi 
 library/summary.cmi: kernel/names.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
+parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
+    kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
 parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi 
 parsing/pcoq.cmi: parsing/coqast.cmi 
+parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi 
+parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
 proofs/logic.cmi: kernel/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: lib/pp.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
-    kernel/term.cmi 
+    kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
@@ -232,9 +237,11 @@ proofs/logic.cmx: parsing/coqast.cmx kernel/evd.cmx kernel/names.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/term.cmx \
     kernel/typing.cmx proofs/logic.cmi 
 proofs/proof_trees.cmo: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
-    kernel/sign.cmi lib/stamps.cmi kernel/term.cmi proofs/proof_trees.cmi 
+    kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi \
+    proofs/proof_trees.cmi 
 proofs/proof_trees.cmx: parsing/coqast.cmx kernel/evd.cmx kernel/names.cmx \
-    kernel/sign.cmx lib/stamps.cmx kernel/term.cmx proofs/proof_trees.cmi 
+    kernel/sign.cmx lib/stamps.cmx kernel/term.cmx lib/util.cmx \
+    proofs/proof_trees.cmi 
 toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
diff --git a/dev/TODO b/dev/TODO
index 188d677b0d..0ec070bc2b 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -12,7 +12,7 @@
 
  o Lib
      - écrire une fonction d'export qui supprimme les FrozenState,
-       vérifie qu'il n'y a pas de section ouvert, et présente les
+       vérifie qu'il n'y a pas de section ouverte, et présente les
        déclarations dans l'ordre chronologique (y compris dans les
        sections fermées ?). A utiliser dans Library pour sauver un module.
 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 5836f7775c..9295d35872 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -19,53 +19,45 @@ type evar_body =
   | Evar_defined of constr
 
 type evar_info = {
-  evar_concl : typed_type;           (* the type of the evar ...          *)
-  evar_hyps  : typed_type signature; (* ... under a certain signature     *)
-  evar_body  : evar_body }           (* any other necessary information   *)
+  evar_concl : constr;
+  evar_hyps : typed_type signature;
+  evar_body : evar_body }
 
 type evar_map = evar_info Intmap.t
 
 let mt_evd = Intmap.empty
 
-let to_list evc = Intmap.fold (fun sp x acc -> (sp,x)::acc) evc []
-let dom evc = Intmap.fold (fun sp _ acc -> sp::acc) evc []
+let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc []
 let map evc k = Intmap.find k evc
 let rmv evc k = Intmap.remove k evc
 let remap evc k i = Intmap.add k i evc
 let in_dom evc k = Intmap.mem k evc
 
-let add_with_info evd sp newinfo = 
-  Intmap.add sp newinfo evd
+let add evd ev newinfo =  Intmap.add ev newinfo evd
 
-let add_noinfo evd sp sign typ = 
-  let newinfo = 
-    { evar_concl = typ;
-      evar_hyps  = sign;
-      evar_body  = Evar_empty }
-  in 
-  Intmap.add sp newinfo evd
-
-let define evd sp body = 
-  let oldinfo = map evd sp in
+let define evd ev body = 
+  let oldinfo = map evd ev in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
-      evar_hyps  = oldinfo.evar_hyps;
-      evar_body  = Evar_defined body } 
+      evar_hyps = oldinfo.evar_hyps;
+      evar_body = Evar_defined body } 
   in
   match oldinfo.evar_body with
-    | Evar_empty -> Intmap.add sp newinfo evd
+    | Evar_empty -> Intmap.add ev newinfo evd
     | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
 
 let non_instantiated sigma = 
-  let listsp = to_list sigma in
+  let listev = to_list sigma in
   List.fold_left 
-    (fun l ((sp,evd) as d) -> 
+    (fun l ((ev,evd) as d) -> 
        if evd.evar_body = Evar_empty then (d::l) else l)
-    [] listsp
+    [] listev
     
-let is_evar sigma sp = in_dom sigma sp
+let is_evar sigma ev = in_dom sigma ev
 
-let is_defined sigma sp =
-  let info = map sigma sp in not (info.evar_body = Evar_empty)
+let is_defined sigma ev =
+  let info = map sigma ev in 
+  not (info.evar_body = Evar_empty)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index fa60292836..89cefcab11 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -10,7 +10,8 @@ open Sign
 (* The type of mappings for existential variables.
    The keys are integers and the associated information is a record
    containing the type of the evar ([concl]), the signature under which 
-   it was introduced ([hyps]) and its definition ([body]). *)
+   it was introduced ([hyps]) and its definition ([body]). 
+   [evar_info] is used to add any other kind of information. *)
 
 type evar = int
 
@@ -21,12 +22,14 @@ type evar_body =
   | Evar_defined of constr
 
 type evar_info = {
-  evar_concl : typed_type;
-  evar_hyps  : typed_type signature;
-  evar_body  : evar_body }
+  evar_concl : constr;
+  evar_hyps : typed_type signature;
+  evar_body : evar_body }
 
 type evar_map
 
+val add : evar_map -> evar -> evar_info -> evar_map
+
 val dom : evar_map -> evar list
 val map : evar_map -> evar -> evar_info
 val rmv : evar_map -> evar -> evar_map
@@ -35,9 +38,6 @@ val in_dom : evar_map -> evar -> bool
 val to_list : evar_map -> (evar * evar_info) list
 
 val mt_evd : evar_map
-val add_with_info : evar_map -> evar -> evar_info -> evar_map
-val add_noinfo : 
-  evar_map -> evar -> typed_type signature -> typed_type -> evar_map
 
 val define : evar_map -> evar -> constr -> evar_map
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ce5dfbc607..5ce323ed95 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -10,7 +10,7 @@ open Proof_trees
 
 val pr_prim_rule : prim_rule -> std_ppcmds
 
-val prim_refiner : prim_rule -> 'a Evd.evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> Evd.evar_map -> goal -> goal list
 
 val prim_extractor : 
   ((typed_type, constr) env -> proof_tree -> constr) -> 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 994b1b353a..a2a10095dc 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Util
 open Names
 open Term
 open Sign
@@ -60,7 +61,7 @@ type prim_rule = {
   params : Coqast.t list;
   terms : constr list }
 
-type local_constraints = Spset.t
+type local_constraints = Intset.t
 
 type proof_tree = {
   status : pf_status;
@@ -68,7 +69,9 @@ type proof_tree = {
   ref : (rule * proof_tree list) option; 
   subproof : proof_tree option }
 
-and goal = ctxtty evar_info
+and goal = {
+  goal_ev : evar_info;
+  goal_ctxtty : ctxtty }
 
 and rule =
   | Prim of prim_rule
@@ -81,49 +84,36 @@ and ctxtty = {
   mimick : proof_tree option;
   lc     : local_constraints } 
 
-and evar_declarations = ctxtty evar_map
+type evar_declarations = goal Intmap.t
+
 
 let is_bind = function
   | Bindings _ -> true
   | _ -> false
 
-let lc_toList lc = Spset.elements lc
+let lc_toList lc = Intset.elements lc
 
 (* Functions on goals *)
 
-let mkGOAL ctxt sign cl = 
-  { evar_hyps = sign; 
-    evar_concl = cl; 
-    evar_body = Evar_empty; 
-    evar_info = Some ctxt }
+let mk_goal ctxt sign cl = 
+  { goal_ev = { evar_hyps = sign; evar_concl = cl; evar_body = Evar_empty };
+    goal_ctxtty = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
 let mt_ctxt lc = { pgm = None; mimick = None; lc = lc }
 
-let get_ctxt ctxt = 
-  match ctxt.evar_info with
-    | Some x -> x
-    | None -> assert false
+let get_ctxt gl = gl.goal_ctxtty
 
-let get_pgm evd = 
-  match evd.evar_info with
-    | Some x -> x.pgm
-    | None -> assert false
+let get_pgm gl = gl.goal_ctxtty.pgm
 
 let set_pgm pgm ctxt = { ctxt with pgm = pgm }
 
-let get_mimick evd   = 
-  match evd.evar_info with
-    | Some x -> x.mimick
-    | None -> assert false
+let get_mimick gl = gl.goal_ctxtty.mimick
 
-let set_mimick mimick ctxt = {mimick = mimick; pgm = ctxt.pgm;lc=ctxt.lc}
+let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc }
 
-let get_lc evd = 
-  match evd.evar_info with
-    | Some x -> x.lc
-    | None -> assert false
+let get_lc gl = gl.goal_ctxtty.lc
 
 (* Functions on proof trees *)
 
@@ -166,7 +156,7 @@ let is_tactic_proof pf =
 
 (* A local constraint is just a set of section_paths *)
 
-(* recall : type local_constraints    = Spset.t *)
+(* recall : type local_constraints = Intset.t *)
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program and mimick
@@ -190,37 +180,38 @@ let mt_evcty lc gc =
   ts_mk { focus = lc; sign = nil_sign; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); sign = gl.evar_hyps ; decls = evds }
+  ts_mk { focus = (get_lc gl); sign = gl.goal_ev.evar_hyps ; decls = evds }
 
 let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
 		       
 let rc_add evc (k,v) = 
   ts_mod
-    (fun evc -> { focus =(Spset.add k evc.focus);
+    (fun evc -> { focus = (Intset.add k evc.focus);
                   sign  = evc.sign;
-                  decls = Evd.add_with_info evc.decls k v })
+                  decls = Intmap.add k v evc.decls })
     evc
 
 let get_hyps  evc = (ts_it evc).sign
 let get_focus evc = (ts_it evc).focus
 let get_decls evc = (ts_it evc).decls
 let get_gc    evc = (ts_mk (ts_it evc).decls)
+
 let remap evc (k,v) = 
   ts_mod
     (fun evc -> { focus = evc.focus;
                   sign  = evc.sign;
-                  decls = Evd.remap evc.decls k v })
+                  decls = Intmap.add k v evc.decls })
     evc
 
-let lc_exists f lc = Spset.fold (fun e b -> (f e) or b) lc false
+let lc_exists f lc = Intset.fold (fun e b -> (f e) or b) lc false
 
-(* MENTIONS SIGMA SP LOC is true exactly when LOC is defined, and SP is
- * on LOC's access list, or an evar on LOC's access list mentions SP. *)
+(* [mentions sigma sp loc] is true exactly when [loc] is defined, and [sp] is
+ * on [loc]'s access list, or an evar on [loc]'s access list mentions [sp]. *)
 
 let rec mentions sigma sp loc =
-  let loc_evd = map (ts_it sigma).decls loc in 
-  match loc_evd.evar_body with 
-    | Evar_defined _ -> (Spset.mem sp (get_lc loc_evd) 
+  let loc_evd = Intmap.find loc (ts_it sigma).decls in 
+  match loc_evd.goal_ev.evar_body with 
+    | Evar_defined _ -> (Intset.mem sp (get_lc loc_evd) 
 			 or lc_exists (mentions sigma sp) (get_lc loc_evd))
     | _ -> false
 
@@ -229,7 +220,7 @@ let rec mentions sigma sp loc =
  * MENTIONS SIGMA SP LOC' is true. *)
 
 let rec accessible sigma sp loc =
-  let loc_evd = map (ts_it sigma).decls loc in 
+  let loc_evd = Intmap.find loc (ts_it sigma).decls in 
   lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd)
 
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index d20bd8b1f5..e6c912b931 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -2,8 +2,11 @@
 (* $Id$ *)
 
 (*i*)
+open Util
+open Stamps
 open Names
 open Term
+open Sign
 open Evd
 (*i*)
 
@@ -63,7 +66,7 @@ type prim_rule = {
   params : Coqast.t list;
   terms : constr list }
 
-type local_constraints = Spset.t
+type local_constraints = Intset.t
 
 (* [ref] = [None] if the goal has still to be proved, 
    and [Some (r,l)] if the rule [r] was applied to the goal
@@ -79,7 +82,9 @@ type proof_tree = {
   ref : (rule * proof_tree list) option; 
   subproof : proof_tree option }
 
-and goal = ctxtty evar_info
+and goal = {
+  goal_ev : evar_info;
+  goal_ctxtty : ctxtty }
 
 and rule =
   | Prim of prim_rule
@@ -92,4 +97,50 @@ and ctxtty = {
   mimick : proof_tree option;
   lc     : local_constraints } 
 
-and evar_declarations = ctxtty evar_map
+type evar_declarations = goal Intmap.t
+
+
+val mk_goal : ctxtty -> typed_type signature -> constr -> goal
+
+val mt_ctxt    : local_constraints -> ctxtty
+val get_ctxt   : goal  -> ctxtty
+val get_pgm    : goal -> constr option
+val set_pgm    : constr option -> ctxtty -> ctxtty
+val get_mimick : goal ->  proof_tree option
+val set_mimick : proof_tree option ->  ctxtty -> ctxtty
+val get_lc     : goal -> local_constraints
+
+val rule_of_proof     : proof_tree -> rule
+val ref_of_proof      : proof_tree -> (rule * proof_tree list)
+val children_of_proof : proof_tree -> proof_tree list
+val goal_of_proof     : proof_tree -> goal
+val subproof_of_proof : proof_tree -> proof_tree
+val status_of_proof   : proof_tree -> pf_status
+val is_complete_proof : proof_tree -> bool
+val is_leaf_proof     : proof_tree -> bool
+val is_tactic_proof   : proof_tree -> bool
+
+
+(* A global constraint is a mappings of existential variables
+   with some extra information for the program and mimick tactics. *)
+
+type global_constraints = evar_declarations timestamped
+
+(* A readable constraint is a global constraint plus a focus set
+   of existential variables and a signature. *)
+
+type evar_recordty = {
+  focus : local_constraints;
+  sign  : typed_type signature;
+  decls : evar_declarations }
+
+and readable_constraints = evar_recordty timestamped
+
+val rc_of_gc  : global_constraints -> goal -> readable_constraints
+val rc_add    : readable_constraints -> int * goal -> readable_constraints
+val get_hyps  : readable_constraints -> typed_type signature
+val get_focus : readable_constraints -> local_constraints
+val get_decls : readable_constraints -> evar_declarations
+val get_gc    : readable_constraints -> global_constraints
+val remap     : readable_constraints -> int * goal -> readable_constraints
+val ctxt_access : readable_constraints -> int -> bool