diff options
author | 2001-03-29 14:27:11 +0000 | |
---|---|---|
committer | 2001-03-29 14:27:11 +0000 | |
commit | 02d7ec75988e2cd13ebf233b364e400309c605a3 (patch) | |
tree | 8fefa05c13d2b01bde733253a9fb890576753215 /contrib/correctness/prename.mli | |
parent | 6c543b9a2d6b14e083649a74511de192e65ca51a (diff) |
mise en place de Correctness (ne compile pas encore)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/prename.mli')
-rw-r--r-- | contrib/correctness/prename.mli | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli new file mode 100644 index 000000000..55b7f3886 --- /dev/null +++ b/contrib/correctness/prename.mli @@ -0,0 +1,57 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id$ *) + +open Names + +(* Abstract type for renamings + * + * Records the names of the mutables objets (ref, arrays) at the different + * moments of the evaluation, called dates + *) + +type t + +type date = string + + +val empty_ren : t +val update : t -> date -> identifier list -> t + (* assign new names for the given variables, associated to a new date *) +val next : t -> identifier list -> t + (* assign new names for the given variables, associated to a new + * date which is generated from an internal counter *) +val push_date : t -> date -> t + (* put a new date on top of the stack *) + +val valid_date : date -> t -> bool +val current_date : t -> date +val all_dates : t -> date list + +val current_var : t -> identifier -> identifier +val current_vars : t -> identifier list -> (identifier * identifier) list + (* gives the current names of some variables *) + +val avoid : t -> identifier list -> t +val fresh : t -> identifier list -> (identifier * identifier) list + (* introduces new names to avoid and renames some given variables *) + +val var_at_date : t -> date -> identifier -> identifier + (* gives the name of a variable at a given date *) +val vars_at_date : t -> date -> identifier list + -> (identifier * identifier) list + (* idem for a list of variables *) + +(* pretty-printers *) + +val pp : t -> Pp.std_ppcmds +val ppr : t -> unit + |