New upstream version 8.8.0+1.gbp069dc3bupstream/8.8.0+1.gbp069dc3bupstream

1 files changed, 0 insertions, 197 deletions

diff --git a/theory.mli b/theory.mli
deleted file mode 100644
index fe79a11..0000000
--- a/theory.mli
+++ /dev/null
@@ -1,197 +0,0 @@
-(***************************************************************************)
-(*  This is part of aac_tactics, it is distributed under the terms of the  *)
-(*         GNU Lesser General Public License version 3                     *)
-(*              (see file LICENSE for more details)                        *)
-(*                                                                         *)
-(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
-(***************************************************************************)
-
-(** Bindings for Coq constants that are specific to the plugin;
-    reification and translation functions.
-   
-    Note: this module is highly correlated with the definitions of {i
-    AAC.v}.
-
-    This module interfaces with the above Coq module; it provides
-    facilities to interpret a term with arbitrary operators as an
-    abstract syntax tree, and to convert an AST into a Coq term
-    (either using the Coq "raw" terms, as written in the starting
-    goal, or using the reified Coq datatypes we define in {i
-    AAC.v}).
-*)
-
-(** Both in OCaml and Coq, we represent finite multisets using
-    weighted lists ([('a*int) list]), see {!Matcher.mset}.
-
-    [mk_mset ty l] constructs a Coq multiset from an OCaml multiset
-    [l] of Coq terms of type [ty] *)
-
-val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr
-
-(** {2 Packaging modules} *)
-
-(** Environments *)
-module Sigma:
-sig
-  (**  [add ty n x map] adds the value [x] of type [ty] with key [n] in [map]  *)
-  val add: Term.constr ->Term.constr ->Term.constr ->Term.constr ->Term.constr
-   
-  (** [empty ty] create an empty map of type [ty]  *)
-  val empty: Term.constr ->Term.constr
-
-  (** [of_list ty null l] translates an OCaml association list into a Coq one *)
-  val of_list: Term.constr -> Term.constr -> (int * Term.constr ) list -> Term.constr
-
-  (** [to_fun ty null map] converts a Coq association list into a Coq function (with default value [null]) *)
-  val to_fun: Term.constr ->Term.constr ->Term.constr ->Term.constr
-end
-
-
-(** Dynamically typed morphisms *)
-module Sym:
-sig
-  (** mimics the Coq record [Sym.pack] *)
-  type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr}
-
-  val typ: Term.constr lazy_t
-
-
-  (** [mk_pack rlt (ar,value,morph)]  *)
-  val mk_pack: Coq.Relation.t -> pack -> Term.constr
-   
-  (** [null] builds a dummy (identity) symbol, given an {!Coq.Relation.t} *)
-  val null: Coq.Relation.t -> Term.constr
- 
-end
-
-
-(** We need to export some Coq stubs out of this module. They are used
-    by the main tactic, see {!Rewrite} *)
-module Stubs : sig
-  val lift : Term.constr Lazy.t
-  val lift_proj_equivalence : Term.constr Lazy.t
-  val lift_transitivity_left : Term.constr Lazy.t
-  val lift_transitivity_right : Term.constr Lazy.t
-  val lift_reflexivity : Term.constr Lazy.t
-    (** The evaluation fonction, used to convert a reified coq term to a
-	raw coq term *)
-  val eval: Term.constr lazy_t
-   
-  (** The main lemma of our theory, that is
-      [compare (norm u) (norm v) = Eq -> eval u == eval v] *)
-  val decide_thm:Term.constr lazy_t 
-
-  val lift_normalise_thm : Term.constr lazy_t
-end
-
-(** {2 Building reified terms}
-   
-    We define a bundle of functions to build reified versions of the
-    terms (those that will be given to the reflexive decision
-    procedure). In particular, each field takes as first argument the
-    index of the symbol rather than the symbol itself. *)
- 
-(** Tranlations between Coq and OCaml  *)
-module Trans :  sig
-
-  (** This module provides facilities to interpret a term with
-      arbitrary operators as an instance of an abstract syntax tree
-      {!Matcher.Terms.t}.
-
-      For each Coq application [f x_1 ... x_n], this amounts to
-      deciding whether one of the partial applications [f x_1
-      ... x_i], [i<=n] is a proper morphism, whether the partial
-      application with [i=n-2] yields an A or AC binary operator, and
-      whether the whole term is the unit for some A or AC operator. We
-      use typeclass resolution to test each of these possibilities.
-
-      Note that there are ambiguous terms:
-      - a term like [f x y] might yield a unary morphism ([f x]) and a
-      binary one ([f]); we select the latter one (unless [f] is A or
-      AC, in which case we declare it accordingly);
-      - a term like [S O] can be considered as a morphism ([S])
-      applied to a unit for [(+)], or as a unit for [( * )]; we
-      chose to give priority to units, so that the latter
-      interpretation is selected in this case; 
-      - an element might be the unit for several operations
-  *)
- 
-  (** To achieve this reification, one need to record informations
-      about the collected operators (symbols, binary operators,
-      units). We use the following imperative internal data-structure to
-      this end. *)
- 
-  type envs
-  val empty_envs : unit -> envs
-   
-
-  (** {2 Reification: from Coq terms to AST {!Matcher.Terms.t}  } *)
-
-
-  (** [t_of_constr goal rlt envs (left,right)] builds the abstract
-      syntax tree of the terms [left] and [right]. We rely on the [goal]
-      to perform typeclasses resolutions to find morphisms compatible
-      with the relation [rlt]. Doing so, it modifies the reification
-      environment [envs]. Moreover, we need to create fresh
-      evars; this is why we give back the [goal], accordingly
-      updated. *)
-  
-  val t_of_constr : Coq.goal_sigma -> Coq.Relation.t -> envs -> (Term.constr * Term.constr) -> Matcher.Terms.t * Matcher.Terms.t * Coq.goal_sigma
-
-  (** [add_symbol] adds a given binary symbol to the environment of
-      known stuff. *)
-  val add_symbol : Coq.goal_sigma -> Coq.Relation.t -> envs -> Term.constr -> Coq.goal_sigma
-
-  (** {2 Reconstruction: from AST back to Coq terms  }
-     
-      The next functions allow one to map OCaml abstract syntax trees
-      to Coq terms. We need two functions to rebuild different kind of
-      terms: first, raw terms, like the one encountered by
-      {!t_of_constr}; second, reified Coq terms, that are required for
-      the reflexive decision procedure. *)
-
-  type ir
-  val ir_of_envs : Coq.goal_sigma -> Coq.Relation.t -> envs -> Coq.goal_sigma * ir
-  val ir_to_units : ir -> Matcher.ext_units
-
-  (** {2 Building raw, natural, terms} *)
-       
-  (** [raw_constr_of_t] rebuilds a term in the raw representation, and
-      reconstruct the named products on top of it. In particular, this
-      allow us to print the context put around the left (or right)
-      hand side of a pattern. *)
-  val raw_constr_of_t : ir ->  Coq.Relation.t -> (Context.Rel.t)  ->Matcher.Terms.t -> Term.constr
-
-  (** {2 Building reified terms} *)
-
-  (** The reification environments, as Coq constrs *)
-
-  type sigmas = {
-    env_sym : Term.constr;
-    env_bin : Term.constr;
-    env_units : Term.constr; 		(* the [idx -> X:constr] *)
-  }
-    
-
-
-  (** We need to reify two terms (left and right members of a goal)
-      that share the same reification envirnoment. Therefore, we need
-      to add letins to the proof context in order to ensure some
-      sharing in the proof terms we produce.
-
-      Moreover, in order to have as much sharing as possible, we also
-      add letins for various partial applications that are used
-      throughout the terms.
-     
-      To achieve this, we decompose the reconstruction function into
-      two steps: first, we build the reification environment and then
-      reify each term successively.*)
-  type reifier
-
-  val mk_reifier :   Coq.Relation.t -> Term.constr -> ir -> (sigmas * reifier -> Proof_type.tactic) -> Proof_type.tactic
-
-  (** [reif_constr_of_t  reifier t] rebuilds the term [t] in the
-      reified form. *)
-  val reif_constr_of_t : reifier -> Matcher.Terms.t -> Term.constr
-
-end