From 0820caf877c5b74ebcca580d7872f1f69d19274f Mon Sep 17 00:00:00 2001 From: aspiwack Date: Tue, 23 Oct 2007 15:12:59 +0000 Subject: Enlevé les trucs commités au mauvais endroit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/biassoc.ml | 74 ------ lib/biassoc.mli | 61 ----- proofs/goal.ml | 14 -- proofs/goal.mli | 14 -- proofs/permutation.ml | 79 ------- proofs/permutation.mli | 29 --- proofs/proof.ml | 259 --------------------- proofs/proof.mli | 34 --- proofs/subproof.ml | 503 ----------------------------------------- proofs/subproof.mli | 180 --------------- proofs/transactional_stack.ml | 127 ----------- proofs/transactional_stack.mli | 61 ----- 12 files changed, 1435 deletions(-) delete mode 100644 lib/biassoc.ml delete mode 100644 lib/biassoc.mli delete mode 100644 proofs/goal.ml delete mode 100644 proofs/goal.mli delete mode 100644 proofs/permutation.ml delete mode 100644 proofs/permutation.mli delete mode 100644 proofs/proof.ml delete mode 100644 proofs/proof.mli delete mode 100644 proofs/subproof.ml delete mode 100644 proofs/subproof.mli delete mode 100644 proofs/transactional_stack.ml delete mode 100644 proofs/transactional_stack.mli diff --git a/lib/biassoc.ml b/lib/biassoc.ml deleted file mode 100644 index 2c8fc32167..0000000000 --- a/lib/biassoc.ml +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (* if there is no (lt, ?) in the left Map, then there - is no (?,lt) in the Right table. Thus bm is already - free of any reference to lt *) - bm - -let remove_with_right rt bm = (* see remove_with_left *) - try - let lt = find_with_right rt bm in - { left = Gmap.remove lt bm.left ; - right = Gmap.remove rt bm.right } - with Not_found -> - bm - -let add lt rt bm = - if not (mem_with_left lt bm) && not (mem_with_right rt bm) then - { left = Gmap.add lt rt bm.left ; - right = Gmap.add rt lt bm.right } - else - raise (Invalid_argument "Biassoc: non unique values") - diff --git a/lib/biassoc.mli b/lib/biassoc.mli deleted file mode 100644 index 45426d1bc3..0000000000 --- a/lib/biassoc.mli +++ /dev/null @@ -1,61 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool -(** tests the emptyness of a bidirectional association table *) -val add : 'a -> 'b -> ('a,'b) biassoc -> ('a,'b) biassoc -(** [add lt rt bm] return a bidirectional association table identical - to [bm] except that there is an additional association between - [lt] and [rt]. - If [lt] or [rt] are already present in an association in [bm] - then it raises [Invalid_argument "Biassoc: non unique values"] - instead *) -val find_with_left : 'a -> ('a,'b) biassoc -> 'b -(** [find_with_left lt bm] returns the value associated to [lt] it - there is one. It raises [Not_found] otherwise. *) -val find_with_right : 'b -> ('a,'b) biassoc -> 'a -(** [find_with_right] works as [find_with_left] except that - it implements the other direction of the association. *) -val remove_with_left : 'a -> ('a,'b) biassoc -> ('a,'b) biassoc -(** [remove_with_left lt bm] returns a stack identical to [bm] - except that any association with [lt] has been removed. *) -val remove_with_right : 'b -> ('a,'b) biassoc -> ('a,'b) biassoc -(** [remove_with_right] works as [remove_with_left] except that - the key is from the right side of the associations. *) -val mem_with_left : 'a -> ('a,'b) biassoc -> bool -(** [mem_with_left lt bm] returns [true] if there is a value - associated to [lt] in [bm]. It returns [false] otherwise. *) -val mem_with_right : 'b -> ('a,'b) biassoc -> bool -(** [mem_with_right] works as [mem_with_left] except that it - implements the other direction. *) diff --git a/proofs/goal.ml b/proofs/goal.ml deleted file mode 100644 index 2172373170..0000000000 --- a/proofs/goal.ml +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - try - Array.iteri locally_correct arr ; - true - with Not_found -> - false - - -(* Function checking if an array is a permutation of [| 0 1 ... (n-1) |] *) -let check_permutation arr = - let new_arr = Array.copy arr in - Array.fast_sort compare new_arr; - check_correct new_arr - -(* Function to build a permutation from an array. - Raises Invalid_argument "Permutation.of_array: ill formed permutation" - if the array is not a permutation of [| 0 1 ... (n-1) |] *) -let of_array arr = - if check_permutation arr then - Array.copy arr - else - invalid_arg "Permutation.of_array: ill formed permutation" - -(* Produces an occurence of the identity of size n *) -let identity n = - Array.init n (fun i -> i) - -(* For an [n > Array.length perm], it extends the permutation with the - identity *) -let extend perm n = - let ext = identity n in - Array.blit perm 0 ext 0 (Array.length perm); - ext - -(* Function to permute an array. - Raises Invalid_argument "Permutation.permute: array and permutation size do not match" - if the size of the array is smaller than that of the permutation. - If the size of the array is bigger than the permutation, then the permutation is extended *) -let permute = - (* permutes [arr] according to [per] both must be of length [len] *) - let unsafe_permute perm arr len = - Array.init len (fun i-> arr.(perm.(i))) - in - fun perm arr -> - let plen = Array.length perm in - let alen = Array.length arr in - if alen > plen then - unsafe_permute (extend perm alen) arr alen - else if alen = plen then - unsafe_permute perm arr alen - else - invalid_arg "Permutation.permute: array and permutation size do not match" diff --git a/proofs/permutation.mli b/proofs/permutation.mli deleted file mode 100644 index 9063f58159..0000000000 --- a/proofs/permutation.mli +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* permutation - -(* Function to permute an array. - Raises Invalid_argument "Permutation.permute: array and permutation size do not match" - if the size of the array is smaller than that of the permutation. - If the size of the array is bigger than the permutation, then the permutation is extended *) -val permute : permutation -> 'a array -> 'a array diff --git a/proofs/proof.ml b/proofs/proof.ml deleted file mode 100644 index c0bfc6f755..0000000000 --- a/proofs/proof.ml +++ /dev/null @@ -1,259 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* '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 *) diff --git a/proofs/proof.mli b/proofs/proof.mli deleted file mode 100644 index 4e30d8dafa..0000000000 --- a/proofs/proof.mli +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a - -val do_command : 'a transformation -> 'a proof -> unit - - diff --git a/proofs/subproof.ml b/proofs/subproof.ml deleted file mode 100644 index 66c87ae298..0000000000 --- a/proofs/subproof.ml +++ /dev/null @@ -1,503 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a}. There - is two main obstactle to this design choice : - 1/ There is no existential type in OCaml - 2/ There is sometimes need to know that internal subproofs - actually are constr _subproof, since tactics create such new goals. - The 1/ could be avoided by additional boxings and a bit of extra - verbosity, though it will probably impair a bit the legibility of - the code. The 2/ seems more of a problem thus the actual design - choice is probably definite *) -and 'a partially_resolved_subproof = - { node : constr _subproof array; - resolver : constr array -> 'a - } -and 'a _pointer = - | Root of 'a _subproof ref - | Node of 'a _subproof array*int - -type ('a,+'b) pointer = 'a _pointer - -(* This type gives *) -type ('a,+'b) subproof = 'a _subproof - -(* Internal function which gives the subproof contained by the pointer *) -let get = function - | Root r_sp -> !r_sp - | Node(sp_array,ix) -> sp_array.(ix) - -(* Internal function which gives the "real" subproof represented by a subproof. - it goes through the Route-s and Permutation-s to give the useful content - of the proof *) -let rec simplify = function - | (Open _ as sp) - | (Resolved _ as sp) - | (Subproof _ as sp) - | Permutation(_,sp) -> sp - | Route pt -> simplify (get pt) - -(* composition of the above two functions *) -let get_simplify sp = simplify (get sp) - -let mutate pt sp = - match pt with - | Root r_nd -> r_nd := sp - | Node(sp_array,ix) -> sp_array.(ix) <- sp - -(* Type of the iterators (used with the iteration function) *) -(* The need to define a new type is due the universal quantification - since not all the nodes have the same type case *) -type iterator = { iterator : 'a.'a _pointer -> unit } - -(* The percolation function applies a function to all node pointer in the - subproof. It is guaranteed that an ancestor node will have the function - applied after all its descendants. *) -(* This function may be a little ad hoc, it has been design mostly solely - for the interaction with [resolve] and [mutate] and being able to add - undo information around the resolution. *) -(* The extra seemingly unnecessary functions are here for typing issue, - the idea is that traverse_deep (: iterator -> constr _subproof -> unit) - doesn't have the same type as traverse - (: iterator -> 'a -> _subproof -> unit) *) -let percolate = - let rec percolate_body traverse it pt = - match get pt with - | Resolved _ -> () - | Open _ -> it.iterator pt - | Subproof prs - | Permutation(_, Subproof prs) -> traverse it prs ; it.iterator pt - | Permutation(_, _) -> it.iterator pt - | Route pt -> percolate_body traverse it pt - in - let traverse_body traverse_deep it prs = - Array.iteri (fun i _ -> percolate_body traverse_deep it (Node(prs.node,i))) - prs.node - in - let rec traverse_deep it prs = - traverse_body traverse_deep it prs - in - let rec traverse it prs = - traverse_body traverse_deep it prs - in - fun it pt -> percolate_body traverse it pt - - -(* This function is meant to turn a subproof that is actually - resolved into a Resolved Goal. - It can fail by raising the exception Unresolved when the current goal is - open or when not all it's immediate children are Resolved. - It is meant to be use later as the main tile of building a general - recursive resolve function which will take care of the additional - bureaucracy (such as the undo and such) *) -exception Unresolved - -let rec resolve = - let atomic_convert sp = (*converts a Resolved _ into a constr *) - match simplify sp with - | Resolved constr -> constr - | _ -> raise Unresolved - in - let convert arr = - Array.map atomic_convert arr - in - fun sp -> - match simplify sp with - | Open _ -> raise Unresolved - | Resolved _ as sp -> sp - | Subproof psr -> let sub_constr = convert psr.node in - Resolved (psr.resolver sub_constr) - | _ -> Util.anomaly "Subproof.resolve: failure of simplify" - -(* This function returns [true] if it's argument is resolved, and - [false] otherwise] *) -let is_resolved sp = - match simplify sp with - | Resolved _ -> true - | _ -> false - -(* This function returns the array containing pointers to all the open - subgoals of a given subproof pointer *) -(* extra functions due to typing issue *) -let opengoals = - let list_opengoals_node_body loga next cont pt = - match get pt with - (* by construction a pointer containing an Open goal are - always constr _pointer. If we omit the magic, then we - cannot express opengoals in all generality *) - | Open _ -> [(Obj.magic pt:constr _pointer)] - | Resolved _ -> next cont - | Subproof psr -> loga next cont psr.node 0 - (* For the semantics to be correct here we need all the - open goals to be contained in subproofs from the permuted - array all such open goal to be actually linked to the subproof. - This invariant is not enforced by typing (unfortunately), but - should be kept correct as long as one does not do absurd things - with proofs *) - | Permutation (arr,_) ->let sp_arr = Array.map get arr in - loga next cont sp_arr ((Array.length arr) - 1) - | Route _ -> Util.anomaly "Subproof.opengoals: abnormal Route node" - in - let rec list_opengoals_array return cont sp_arr ix = - if ix < 0 then - return cont - else - let next new_cont = list_opengoals_array return new_cont sp_arr ix in - list_opengoals_node_body list_opengoals_array next cont (Node(sp_arr,ix)) - in - let list_opengoals_node pt = - list_opengoals_node_body list_opengoals_array (fun cont -> cont) [] pt - in - fun pt -> - Array.of_list (list_opengoals_node pt) - -(* This function returns the result of a resolved subproof *) -let get_result sp = - match simplify sp with - | Resolved res -> res - | _ -> Util.anomaly "Subproof.get_result: failure of simplify" - -(* This function returns the actual goal represented by an open - goal subproof *) -let get_goal sp = - match simplify sp with - | Open gl -> gl - | _ -> Util.anomaly "Subproof.get_goal: failure of simplify" - -(* Reorders the open goals of the given pointer, according to the - permutation *) -let reorder = - let copy pt = (* creates a new pointer towards the same content *) - Root (ref (get pt)) - in - let route pt_route pt_content = (* mutates [pt_route] into a route to *) - (* [pt_content] *) - mutate pt_route (Route (pt_content)) - in - fun perm pt -> - let og = opengoals pt in - let copied_og = Array.map copy og in - Array.iteri (fun i pt -> route pt copied_og.(i)) og; - let reordered_og = Permutation.permute perm copied_og in - mutate pt (Permutation(reordered_og, get pt)) - - -(* The following function creates a new subproof *) -let open_subproof ?(subgoals=[||]) ~resolver = - Subproof { node = Array.map (fun g -> Open g) subgoals; - resolver = resolver } - -(* The following function creates a new pointer with a new subproof in it *) -let start_subproof ?(subgoals=[||]) ~resolver = - Root (ref (open_subproof ~subgoals:subgoals ~resolver:resolver)) - - - -(*arnaud: - let list_opengoals_body log_deep traverse return cont sp_arr ix = - let next cont = traverse cont sp_arr (ix-1) in - if ix < 0 then - return cont - else - match get sp_arr.(ix) with - | Open _ -> [Node(sp_arr,ix)] - | Resolved _ -> next cont - | Subproof psr -> log_deep next cont psr.node 0 - (* For the semantics to be correct here we need all the - open goals to be contained in subproofs from the permuted - array all such open goal to be actually linked to the subproof. - This invariant is not enforced by typing (unfortunately), but - should be kept correct as long as one does not do absurd things - with proofs *) - | Permutation (arr,_) -> log_deep next cont arr ((Array.length arr) - 1) - | Route (_, _) -> anomaly "Subproof.opengoals: abnormal Route node" - in - let rec deep_list_opengoals return cont sp_arr ix = - list_opengoals_body deep_list_opengoals (deep_list_opengoals return) - in - let rec list_opengoals cont sp_arr ix = - list_opengoals_body deep_list_opengoals - traverse - (fun cont -> cont) - in - function - | Root r_sp -> match !sp with - | Subproof - | Node(sp_arr, ix) -> Array.of_list (list_opengoals [] sp ix) *) - - - -(* arnaud: - -(* The type 'a subproof represents the type of subproofs "returning" - an object of type 'a. *) -(* In essence the type 'a proof_node should be an existential type - of the shape 'a proof_node = exists 'b.{ node : 'b subproof array; - fallback : 'b array -> 'a} - However, this extra layer of abstraction is hardly needed in practice - and since existential types are not primitive in OCaml (though - somewhat encodable through some additional boxing) it wasn't worth - the extra complication. - The type of nodes is specialized (in constr subproof) to allow clearer - and more efficient code *) -(* arnaud: rather old style -type 'a proof_node = - { node : constr subproof array; - callback : constr array -> 'a - } -and 'a subproof = - [ `Open of goal - | `Resolved of 'a - | `Subproof of 'a proof_node ] *) - -(* arnaud: old style - | OpenGoal of goal - | PartiallyResolvedGoal of 'a proof_node - | ResolvedGoal of 'a *) - -(* This type replaces an existential typing *) -type 'a deep_node = - | Root of 'a proof_node - | Node of constr proof_node - -(* The type to identify a specific node or leaf of a subproof *) -type 'a position = { handle:'a deep_node; - index:int} - -(* This function is meant to turn a `Subproof that is actually - resolved into a Resolved Goal. - It can fail by raising the exception Unresolved when the current goal is - open or when not all it's immediate children are Resolved. - It is meant to be use later as the main tile of building a general - recursive resolve function which will take care of the additional - bureaucracy (such as the undo and such) *) -exception Unresolved - -let resolve = - let convert arr =(* converts an array of `Resolved into an array of constr *) - Array.map - (function | `Resolved constr -> constr - | _ -> raise Unresolved) arr - in - - function | `Subproof sp -> - let sub_constr = convert sp.node in - `Resolved (sp.callback sub_constr) - | (`Resolved _) as rg -> rg - | `Open _ -> raise Unresolved - - -(* arnaud: virer ce truc inutile, comprendre une solution à base de dictionaire - ou filtre éventuellement -(* The following function switches two proof_node (identified by their indices) - of a given subproof. *) -(* spiwack: I don't really know if it will prove a useful function. It has - the very big default that it does not scale up very well. Indeed, - it does not allow switching proofs that are in different subtrees, - which is what the user may wants to do, but can't be done at this - level. - It is not currently in the .mli would require a bit of thinking - to get the right version. *) -(* arnaud : cette fonction mute le callback, faire attention à bien faire - l'undo proprement *) -let switch = - let array_switch i j arr = - let buf_i = arr.(i) in - let buf_j = arr.(j) in (* not necessary, could be replaced by a - length check *) - arr.(i) <- buf_j; arr.(j) <- buf_i - in - - fun i j sp -> - array_switch i j sp.node; - sp.callback <- (fun arr -> array_switch i j arr; - (* the array that is switched - back is a newly born array - no risk of corrupting data - by modifying it *) - sp.callback arr) -*) - -(* The following function creates a new subproof *) -let open_proof ?(subgoals=[||]) ~callback = - `Subproof { node = Array.map (fun g -> `Open g) subgoals; - callback = callback } - - -(* This function returns the subproof pointed by the position [pos] *) -let of_position pos = - match pos.handle with - | Root sp -> sp.node.(pos.index) - | Node sp -> sp.node.(pos.index) - -(* The following function returns the position of the nth opened subgoal. - Raises not_found if there is not that many subgoals. - It acts either on a subproof of the form `Subproof _ or on a position *) -let rec nth_subgoal = - (* [nth_subgoal] basically does a depth-first search of the proof - subtree. - The implementation of the function is a bit tricky, due to typing - issue (again the absence of existential types makes things a bit - more tedious (yet less than if we used an encoding)). - The main subfunction is the function [abstract_traverse] which - takes as arguments the recursive calls. The argument [traverse] - is the function that is called when checking the next goal of - a node (and is abstracted inside the function [next]). The - argument [deep_traverse] is called when going one node deeper - in the subproof tree. The [return] argument is used when - backtracking to a parent node. [n] is the number of open goals - to find before we find the goal we look for: it is decreased by - [1] each time we find a open subgoal, except if it is already [1] - in which case we terminate the algorithm on the first open subgoal - we find. [ix] represent the current index in the array of the node. - [pn] is the current subproof node we are currently traversing. - Finally [box] is a function giving a way to coerce the current - [proof_node] (namely [pn]) into the appropriate ['a deep_node] - where ['a] correspond to the return type of the root of the proof - we consider. - This function being defined we can define the two main subroutines - [deep_traverse] is basically [abstract_traverse deep_traverse - deep_traverse]. It performs the search inside any non-root node - since all of them are of type [constr proof_node] it is simply - self-recursive. - The function [traverse] takes care of the search on the root node. - That is, basically, [abstract_traverse traverse deep_traverse]. - Because of the heterogeneous typing of the root and deep nodes - it calls deep_traverse when it goes deeper in the tree *) - let abstract_traverse traverse deep_traverse return n ix pn box = - if ix < Array.length pn.node then - let next n = traverse n (ix+1) pn in - match pn.node.(ix) with - | `Open _ when n = 1 -> {handle=box pn;index=ix} - | `Open _ -> next (n-1) - | `Resolved _ -> next n - | `Subproof rpn -> deep_traverse next n 0 rpn - else - return n - in - let node u = Node u in - let rec deep_traverse return n ix pn = - abstract_traverse (deep_traverse return) deep_traverse return n ix pn node - in - let root u = Root u in - let rec traverse n ix pn = - abstract_traverse traverse - deep_traverse - (fun _ -> raise Not_found) - n - ix - pn root - in - fun n sp -> - if n < 1 then - invalid_arg "Subproof.nth_subgoal: no non-positive open goal" - else - match sp with - | `Subproof pn -> traverse n 0 pn - | `Position pos -> - match of_position pos with - | `Subproof pn -> deep_traverse (fun _ -> raise Not_found) n 0 pn - | `Open _ when n=1 -> pos - | `Open _ -> raise Not_found - | `Resolved _ -> raise Not_found - -(* arnaud: to clean - let abstract_traverse traverse n parents ix sp dsp = - if ix < Array.length sp.node then - match sp.node.(ix) with - | `Open _ when n = 1 -> {handle=dsp;index=ix} - | `Open _ -> traverse (n-1) parents (ix+1) dsp - | `Resolved _ -> traverse n parents (ix+1) dsp - | `Subproof rsp -> traverse n ((dsp, ix)::parents) - 0 (Node rsp) - else - match parents with - | (dsp, jx)::q -> traverse n q (jx+1) dsp - | [] -> raise Not_found - in - let rec traverse n parents ix = function - | (Root sp) as dsp -> abstract_traverse traverse n parents ix sp dsp - | (Node sp) as dsp -> abstract_traverse traverse n parents ix sp dsp - in - fun n (`Subproof sp )-> - if n < 1 then - invalid_arg "Subproof.nth_subgoal: no non-positive open goal" - else - traverse n [] 0 (Root sp) *) - - -(* This function changes the goal at a certain position *) -let mutate pos new_content = - match pos.handle with - | Root sp -> sp.node.(pos.index) <- new_content - | Node sp -> sp.node.(pos.index) <- new_content - - -(* This function iters a function on all the subproofs of a proof node, - except the node of the root *) -let iter f pn = - let bpn = Node pn in - Array.iteri (fun i -> f { handle=bpn ; index=i}) pn.node - -(* This function iters a function on all the subproof of the root proof - node *) -let root_iter f pn = - let bpn = Root pn in - Array.iteri (fun i -> f { handle=bpn ; index=i}) pn.node -*) diff --git a/proofs/subproof.mli b/proofs/subproof.mli deleted file mode 100644 index edb9b23846..0000000000 --- a/proofs/subproof.mli +++ /dev/null @@ -1,180 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ('a,'b) subproof - -(* Changes the subproof held by a pointer *) -val mutate : ('a,'b) pointer -> ('a,'b) subproof -> unit - - -(* Type of functions to be used with [percolate] *) -type iterator = - { iterator : 'a.('a,[ `Subproof | `Open | `Resolved ]) pointer -> unit } - -(* The percolation function applies a function to all node pointer in the - subproof. It is guaranteed that an ancestor node will have the function - applied after all its descendants. *) -(* This function may be a little ad hoc, it has been design mostly solely - for the interaction with [resolve] and [mutate] and being able to add - undo information around the resolution. *) -val percolate : iterator -> ('a,'b) pointer -> unit - -(* This function is meant to turn a subproof that is actually - resolved into a Resolved Goal. - It can fail by raising the exception Unresolved when the current goal is - open or when not all it's immediate children are Resolved. - It is meant to be use later as the main tile of building a general - recursive resolve function which will take care of the additional - bureaucracy (such as the undo and such) *) -exception Unresolved -val resolve : ('a,'b) subproof -> ('a, [> `Resolved]) subproof - -(* This function returns [true] if it's argument is resolved, and - [false] otherwise] *) -val is_resolved : ('a,'b) subproof -> bool - -(* This function returns the array containing pointers to all the open - subgoals of a given subproof pointer *) -val opengoals : ('a,'b) pointer -> (constr, [> `Open]) pointer array - -(* This function returns the result of a resolved subproof *) -val get_result : ('a,[< `Result ]) subproof -> 'a - -(* This function returns the actual goal represented by an open - goal subproof *) -val get_goal : (constr, [< `Open ]) subproof -> Goal.goal - -(* Reorders the open goals of the given pointer, according to the - permutation *) -val reorder : Permutation.permutation -> ('a, 'b) pointer -> unit - -(* The following function creates a new subproof *) -val open_subproof : ?subgoals:Goal.goal array -> - resolver:(constr array -> 'a) -> - ('a, [>`Subproof]) subproof - -(* The following function creates a new pointer with a new subproof in it *) -val start_subproof : ?subgoals:Goal.goal array -> - resolver:(constr array -> 'a) -> - ('a, [>`Subproof]) pointer - - -(* arnaud: -open Term -open Goal - -(* A type which corresponds to the `Subproof case of subproofs *) -type 'a proof_node - -(* The type 'a subproof represents the type of subproof "returning" - an object of type 'a. *) -type 'a subproof = - [ `Open of goal - | `Resolved of 'a - | `Subproof of 'a proof_node ] - - -(* The type to identify a specific node or leaf of a subproof. - Be careful, it indicates a physical position. It can give - unexpected results if it is used after a proof has mutated *) -type 'a position - - -(* This function is meant to turn a PartiallyResolvedGoal that is actually - resolved into a Resolved Goal. - It can fail by raising the exception Unresolved when the current goal is - open or when not all it's immediate children are Resolved. - It is meant to be use later as the main tile of building a general - recursive resolve function which will take care of the additional - bureaucracy (such as the undo and such). - It is a pure function. *) -exception Unresolved - -val resolve : [< 'a subproof ] -> [> `Resolved of 'a ] - - -(* The following function creates a new subproof *) -val open_proof : ?subgoals:goal array -> - callback:(constr array -> 'a) -> - [ `Subproof of 'a proof_node ] - -(* The following function returns the position of the nth opened subgoal. - Raises not_found if there is not that many subgoals. *) -val nth_subgoal : int -> [< `Subproof of 'a proof_node - | `Position of 'a position ] -> 'a position - -(* This function changes the goal at a certain position *) -val mutate : 'a position -> constr subproof -> unit - -(* This function returns the subproof pointed by the position [pos] *) -val of_position : 'a position -> constr subproof - -(* This function iters a function on all the subproofs of a proof node, - except the node of the root *) -val iter : ('a position -> constr subproof ->unit) -> constr proof_node -> unit - - -(* This function iters a function on all the subproof of the root proof - node *) -val root_iter : ('a position -> constr subproof->unit) -> 'a proof_node -> unit -*) diff --git a/proofs/transactional_stack.ml b/proofs/transactional_stack.ml deleted file mode 100644 index 74b95e6c0b..0000000000 --- a/proofs/transactional_stack.ml +++ /dev/null @@ -1,127 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a stack - val push : 'a -> 'a stack -> unit - val pop : 'a stack -> 'a - val snapshot : 'a stack -> 'a list - val lock : 'a stack -> unit - val unlock : 'a stack -> unit - val locked : 'a stack -> bool - end) = - (* arnaud: the type of Stack has not been abstracted yet - out of sheer lazyness *) - (* stacks are basically a list without the possibility of map/fold. - they contain an extra lock that is hear for pure safety reasons. - trying to push or pop to a locked stack raises an anomaly *) - struct - type 'a stack = {mutable stack : 'a list ; mutable locked : bool } - - let create () = { stack = [] ; locked = false} - let push a st = - if st.locked then - Util.anomaly - "Transactional_stack.Stack.push: nsafe use of a stack" - else - st.stack <- a::st.stack - - let pop st = - if st.locked then - Util.anomaly - "Transactional_stack.Stack.pop: unsafe use of a stack" - else - match st.stack with - | [] -> raise Not_found - | a::r -> st.stack <- r ; a - let snapshot st = st.stack - - let lock st = st.locked <- true - let unlock st = st.locked <- false - - let locked st = st.locked - end - - -type 'a transactional_stack = 'a list Stack.stack -type 'a transaction = { transaction: 'a Stack.stack; - t_stack: 'a transactional_stack } - - -(* General note : freezing/unfreezing of transactional stacks and - death of transactions both use the lock mechanism of stacks. - In some case it imposes naturally a restriction, in other cases - we also need to check the lock manually. *) - - -let start_transaction t_st = - if Stack.locked t_st then - Util.anomaly - "Transitional_stack.start_transaction: cannot start a transaction from a frozen stack" - else - Stack.lock t_st; - { transaction = Stack.create () ; - t_stack = t_st } - -let commit tr = - if Stack.locked tr.transaction then - Util.anomaly "Transitional_stack.commit: cannot commit a dead transaction" - else - Stack.unlock tr.t_stack; - Stack.push (Stack.snapshot tr.transaction) tr.t_stack; - Stack.lock tr.transaction - -let rollback cont tr = - if Stack.locked tr.transaction then - Util.anomaly - "Transitional_stack.rollback: cannot rollback a dead transaction" - else - Stack.unlock tr.t_stack; - Stack.lock tr.transaction; - cont (Stack.snapshot tr.transaction) - - - -let push action tr = Stack.push action tr.transaction - - -let pop cont t_st = - cont (Stack.pop t_st) diff --git a/proofs/transactional_stack.mli b/proofs/transactional_stack.mli deleted file mode 100644 index 9792641878..0000000000 --- a/proofs/transactional_stack.mli +++ /dev/null @@ -1,61 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a transaction - (** [start_transaction st] starts a new transaction bound to the - stack [st]. In addition [st] is frozen until the new transaction - ends. (While [st] is frozen you can't open any other transaction, - nor pop the last transaction, it would raise an anomaly) *) - -val commit : 'a transaction -> unit - (** [commit tr] commits the transaction [tr] to the stack it is bound - to. The transaction is then killed (you can't use it anymore, trying - to do so raises an anomaly) and the associated stack is released. *) - -val rollback : ('a list -> 'b) -> 'a transaction -> 'b - (** [rollback cont tr] rolls the transaction back, by executing - cont on the list representing the transaction. The transaction - is then killed and the associated stack released. *) - - -val push : 'a -> 'a transaction -> unit - (** [push a tr] pushes the action [a] onto the transaction [tr] *) - - -val pop : ('a list -> 'b) -> 'a transactional_stack -> 'b - (** [pop cont st] pops the last transaction out of [st] - and applies [cont] to the list representing it *) -- cgit v1.2.3