Imported Upstream version 0.2upstream/0.2

1 files changed, 0 insertions, 219 deletions

diff --git a/theory.mli b/theory.mli
deleted file mode 100644
index 85ad24b..0000000
--- a/theory.mli
+++ /dev/null
@@ -1,219 +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}).
-*)
-
-
-
-
-(** 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
-
-(** The constr associated with our typeclasses for AC or A operators *)
-val op_ac:Term.constr lazy_t
-val op_a: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
-
-(** {2 Packaging modules} *)
-
-(** 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_typeof rlt int]  *)
-  val mk_typeof: Coq.reltype ->int ->Term.constr
-
-  (** [mk_typeof rlt int]  *)
-  val mk_relof:  Coq.reltype ->int ->Term.constr
-
-  (** [mk_pack rlt (ar,value,morph)]  *)
-  val mk_pack: Coq.reltype -> pack -> Term.constr
-    
-  (** [null] builds a dummy symbol, given an {!Coq.eqtype} and a
-      constant *)
-  val null: Coq.eqtype -> Term.constr -> Term.constr
-  
-end
-
-(** Dynamically typed AC operations *)
-module Sum:
-sig
-
-  (** mimics the Coq record [Sum.pack] *)
-  type pack = {plus : Term.constr; zero: Term.constr ; opac: Term.constr}
-
-  val typ: Term.constr lazy_t
-
-  (** [mk_pack rlt (plus,zero,opac)]  *)
-  val mk_pack: Coq.reltype -> pack -> Term.constr
-    
-  (** [zero rlt pack]*)
-  val zero: Coq.reltype -> Term.constr -> Term.constr
-
-  (** [plus rlt pack]*)
-  val plus: Coq.reltype -> Term.constr -> Term.constr
-
-end
-
-
-(** Dynamically typed A operations *)
-module Prd:
-sig
-
-  (** mimics the Coq record [Prd.pack] *)
-  type pack = {dot: Term.constr; one: Term.constr ; opa: Term.constr}
-
-  val typ: Term.constr lazy_t
-
-  (** [mk_pack rlt (dot,one,opa)]  *)
-  val mk_pack: Coq.reltype -> pack -> Term.constr
-    
-  (** [one rlt pack]*)
-  val one: Coq.reltype -> Term.constr -> Term.constr
-
-  (** [dot rlt pack]*)
-  val dot: Coq.reltype -> Term.constr -> Term.constr
-    
-end
-
-
-(** [mk_equal rlt l r] builds the term [l == r] *)
-val mk_equal : Coq.reltype -> Term.constr -> Term.constr -> Term.constr
-
-
-(** {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; the
-      behaviour in this case is almost unspecified: we simply give
-      priority to AC 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
-
-  (** {1 Reification: from Coq terms to AST {!Matcher.Terms.t}  } *)
-
-  (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree
-      of the term [cstr]. 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 creates fresh evars; this is
-      why we give back the [goal], accordingly updated. *)
-  val t_of_constr : Coq.goal_sigma -> Coq.reltype -> envs -> Term.constr -> Matcher.Terms.t * Coq.goal_sigma
-
-  (** {1 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. *)
-
-  (** {2 Building raw, natural, terms} *)
-
-  (** [raw_constr_of_t] rebuilds a term in the raw representation *)
-  val raw_constr_of_t : envs -> Coq.reltype -> Matcher.Terms.t -> Term.constr
-
-  (** {2 Building reified terms} *)
- 
-  (** The reification environments, as Coq constrs *)
-  type sigmas = {
-    env_sym : Term.constr;
-    env_sum : Term.constr;
-    env_prd : Term.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.eqtype -> envs -> Coq.goal_sigma -> sigmas * reifier * 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