Quelques structures de donnée plus les modules principaux (et

parfaitement en cours) de la nouvelle machinerie de preuves.



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

1 files changed, 259 insertions, 0 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
new file mode 100644
index 000000000..c0bfc6f75
--- /dev/null
+++ b/proofs/proof.ml
@@ -0,0 +1,259 @@
+(************************************************************************)
+(*  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: proof.ml aspiwack $ *)
+
+(* This module implements the actual proof datatype. It enforces strong
+   invariants, and it is the only module that should access the module
+   Subproof.
+   Actually from outside the proofs/ subdirectory, this is the only module
+   that should be used directly. *)
+
+(* arnaud: rajouter le blabla sur la  théorie du module ici *)
+
+(* arnaud: penser à garder une liste des positions qui seraient valide ? *)
+
+open Term
+
+type ('a,'b) subproof = ('a,'b) Subproof.subproof 
+     (* rather than opening Subproof *)
+
+open Transactional_stack
+
+
+
+type evar = unit (* arnaud: à compléter en temps utile aussi *)
+
+type 'a proof = { (* The root of the proof *)
+		  mutable root : ('a,[ `Subproof | `Resolved ]) Subproof.pointer;
+		  (* The list of focusings to be able to backtrack.
+		     The current focusing is the head of the list.
+		     The empty list means that the root is focused *)
+                  mutable focus : (constr,[ `Subproof | `Resolved | `Open ]) 
+		                                            Subproof.pointer list;
+		  (* The undo stack *)
+		  undo_stack : 'a undo_action transactional_stack;
+		  (* The dependent goal heap *)
+		  mutable dependent_goals : 
+		          ((constr,[ `Subproof | `Resolved | `Open ]) Subproof.pointer, evar) Biassoc.biassoc
+		}
+and 'a undo_action =  (* arnaud: à compléter et nettoyer en temps utile *)
+(*    | MutateBack of (constr,[ `Subproof | `Resolved | `Open ])  Subproof.pointer 
+ * (constr,[ `Subproof | `Resolved | `Open ]) subproof *)
+    | MutateBack of packed_mutation
+    | Unfocus of 'a proof
+    | Focus of 'a proof * (constr,[`Subproof|`Resolved|`Open]) Subproof.pointer
+(*    | MutateRootBack of ('a,[ `Subproof | `Resolved ]) Subproof.pointer 
+ * ('a,[ `Subproof | `Resolved ]) subproof *)
+
+(* Encoding the type
+     exists 'b 'c.{ sp : ('b,'c) subproof ; pt : ('b,'c) Subproof.pointer }
+   trick from Benjaming Pierce and Daniel Bünzli (cf: http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.en.html ) *)
+
+and ('b,'c) mutation = { sp : ('b,'c) subproof ; pt : ('b,'c) Subproof.pointer }
+and 't mutation_scope = { bind_mutation:'b 'c.('b,'c) mutation -> 't }
+and packed_mutation = { open_mutation : 't. 't mutation_scope -> 't }
+
+
+
+(* makes a packed_mutation out of mutation *)
+let pack_mutation mutn =
+  { open_mutation = fun scope -> scope.bind_mutation mutn }
+
+(* uses a scoped function on a packed mutation *)
+let unpack_mutation pck scp =
+  pck.open_mutation scp
+
+
+
+(* Gives the type of a proof action *)
+type 'a action = 'a proof -> 'a undo_action transaction -> unit
+
+(* arnaud: déplacer les séquences en externe, utiliser 
+  ('a proof -> 'a undo_action transaction) sequence pour les actions.
+   Et fournir l'algèbre correspondante. *)
+type 'b sequence = | Atom of 'b | Compound of 'b sequence*'b sequence
+
+
+(*** The following functions give more abstract methods to access
+     the data of a proof ***)
+
+(* This function gives the position of the focus if the proof is
+   focused, [None] otherwise *)
+let get_focus pr =
+  match pr.focus with
+  | [] -> None
+  | pos::_ -> Some pos
+
+(* The following function gives the content of the root *)
+let get_root pr =
+  pr.root
+
+(*** The following functions are somewhat unsafe, they are meant to 
+     be used by other functions later. They shouldn't be declared in
+     the .mli ***)
+
+
+(* This function performs a focusing on a given position
+   with no safety check nor caring of undos *)
+let unsafe_focus pr pos =
+  pr.focus <- pos::pr.focus
+
+(* This function unfocuses the proof [pr] with no safety
+   check nor caring of undos *)
+let unsafe_unfocus pr =
+  pr.focus <- List.tl pr.focus
+
+
+
+
+
+(*** The following functions define the basic safety mechanism of the
+     proof system, they may be unsafe if not used carefully. There is
+     currently no reason to export them in the .mli ***)
+
+let do_packed_mutation =
+  let scoped_mutate = 
+    { bind_mutation = fun mtn -> Subproof.mutate mtn.pt mtn.sp }
+  in
+  fun pck ->
+    unpack_mutation pck scoped_mutate
+
+
+(* This function interpetes (and execute) a single [undo_action] *)
+let execute_undo_action = function
+(*  | MutateBack(pt, sp) -> Subproof.mutate pt sp *)
+  | MutateBack pck -> do_packed_mutation pck
+  | Unfocus pr -> unsafe_unfocus pr
+  | Focus(pr, pt) -> unsafe_focus pr pt
+(*  | MutateRootBack(pt, sp) -> Subproof.mutate pt sp *)
+				
+
+(* This function interpetes a list of undo action, starting with
+   the one on the head. *)
+let execute_undo_sequence l =
+  List.iter execute_undo_action l
+
+(* This function gives the rollback procedure on unsuccessful commands .
+   tr is the current transaction. *)
+let rollback tr =
+  Transactional_stack.rollback execute_undo_sequence tr
+
+
+
+
+
+(* exception which represent a failure in a command *)
+exception Failure of Pp.std_ppcmds
+
+(* function to raise a failure less verbosely *)
+let fail msg = raise (Failure msg)
+
+
+
+(*** The functions that come below are meant to be used as 
+     atomic transformations, they raise [Failure] when they fail
+     and they push an [undo_action] to revert themselves.
+     They are still internal actions. *)
+
+(* This function performs sound mutation at a given position.
+   That is a mutation which stores an undo_action into the 
+   transaction [tr] *)
+let mutate pt sp tr =
+  push (MutateBack (pack_mutation {sp=sp;pt=pt})) tr;
+  Subproof.mutate pt sp
+
+(* arnaud:
+let mutate_root pt sp tr = 
+  push (MutateRootBack ( pt , Subproof.get pt)) tr;
+  Subproof.mutate pt sp *)
+
+(* This function focuses the proof [pr] at position [pt] and 
+   pushes an [undo_action] into the transaction [tr]. *)
+let focus pt pr tr =
+  push (Unfocus pr) tr;
+  unsafe_focus pr pt
+
+(* This function unfocuses the proof [pr], fails if 
+   [pr] is not focused (i.e. it shows its root). It
+   pushed an [undo_action] into the transaction [tr] *)
+let unfocus pr tr =
+  match pr.focus with
+  | [] -> fail (Pp.str "This proof is not focused")
+  | pt::_ -> push (Focus (pr,pt)) tr; unsafe_unfocus pr
+
+
+(*** The following function are composed transformations ***)
+
+(* This pair of functions tries percolate the resolved subgoal as much
+   as possible. It unfocuses the proof as much as needed so that it
+   is not focused on a resolved proof *)
+(* only [resolve] is meant to be used later on *)
+(* [deep_resolve] takes care of the non-root cases *)
+(* arnaud: rajouter les instanciations de métavariables *)
+let resolve =
+  (* This function unfocuses a proof until it is totally unfocused or
+     is focused on a non-resolved subproof *)
+  let rec unfocus_until_sound pr tr = 
+    match get_focus pr with
+    | None -> ()
+    | Some pt -> if Subproof.is_resolved (Subproof.get pt) then
+	           (unfocus pr tr;
+                    unfocus_until_sound pr tr)
+                 else 
+                   ()  
+  in
+  let resolve_iterator_fun tr pt =
+    try 
+      let res = Subproof.resolve (Subproof.get pt) in
+      mutate pt res tr
+    with Subproof.Unresolved ->
+      ()
+  in
+  let resolve_iterator tr = 
+    { Subproof.iterator = fun pt -> resolve_iterator_fun tr pt }
+  in
+  fun pr tr ->
+    Subproof.percolate (resolve_iterator tr) (get_root pr);
+    unfocus_until_sound pr tr
+
+
+(*** mechanism functions for sequences ***)
+let rec iter f seq =
+  match seq with
+  | Atom a -> f a
+  | Compound (lft,rgt) -> (iter f lft);(iter f rgt)
+
+(*** The following function takes a transformation and make it into 
+     a command ***)
+
+let do_command actions pr = 
+  let tr = start_transaction pr.undo_stack in
+  try 
+   iter (fun action -> action pr tr; resolve pr tr) actions;
+   commit tr
+  with e -> (* traitement particulier de Failure ? *)
+    rollback tr;
+    raise e
+  
+
+(*** The functions below are actually commands that can be used,
+     They cannot be used as a part of a compound transformation ***)
+
+(* This function gives the semantics of the "undo" command.
+   [pr] is the current proof *)
+let undo pr = 
+  Transactional_stack.pop execute_undo_sequence (pr.undo_stack)
+
+
+(*** The following functions define the tactic machinery. They 
+     transform a tactical expression into a sequence of actions. ***)
+(* apply_one *)
+(* apply_all *)
+(* apply_array *)
+(* apply_extend *)