generic, term et evd

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

1 files changed, 520 insertions, 0 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
new file mode 100644
index 0000000000..d5a9b11d35
--- /dev/null
+++ b/kernel/term.mli
@@ -0,0 +1,520 @@
+
+(* $Id$ *)
+
+open Names
+open Generic
+
+(* The Type of Constructions Terms. *)
+
+(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
+
+type 'a oper = 
+  (* DOP0 *)
+  | Meta of int
+  | Sort of 'a
+  | Implicit
+  (* DOP2 *)
+  | Cast | Prod | Lambda
+  (* DOPN *)
+  | AppL | Const of section_path | Abst of section_path
+  | MutInd of section_path * int
+  | MutConstruct of (section_path * int) * int
+  | MutCase of case_info
+  | Fix of int array * int
+  | CoFix of int
+
+  | XTRA of string * Coqast.t list
+      (* an extra slot, for putting in whatever sort of
+         operator we need for whatever sort of application *)
+
+and case_info = (section_path * int) option
+
+type contents = Pos | Null
+
+val str_of_contents : contents -> string
+val contents_of_str : string -> contents
+
+type sorts =
+  | Prop of contents       (* Prop and Set *)
+  | Type of Univ.universe  (* Type *)
+
+val mk_Set  : sorts
+val mk_Prop : sorts
+
+type constr = sorts oper term
+
+type 'a judge = { body : constr; typ : 'a }
+
+type type_judgment = sorts judge
+type term_judgment = type_judgment judge
+
+type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
+
+
+(****************************************************************************)
+(*              Functions for dealing with constr terms                     *)
+(****************************************************************************)
+
+(* The following functions are intended to simplify and to uniform the 
+   manipulation of terms. Some of these functions may be overlapped with
+   previous ones. *)
+
+(* Concrete type for making pattern-matching *)
+
+type kindOfTerm =
+  | IsRel          of int
+  | IsMeta         of int
+  | IsVar          of identifier
+  | IsXtra         of string * Coqast.t list
+  | IsSort         of sorts
+  | IsImplicit
+  | IsCast         of constr * constr
+  | IsProd         of name * constr * constr
+  | IsLambda       of name * constr * constr
+  | IsAppL         of constr array
+  | IsConst        of section_path  * constr array
+  | IsAbst         of section_path  * constr array
+  | IsMutInd       of section_path * int * constr array
+  | IsMutConstruct of section_path * int * int * constr array
+  | IsMutCase      of case_info * constr * constr * constr array
+  | IsFix          of int array * int * constr array * name list *
+                      constr array
+  | IsCoFix        of int * constr array * name list * constr array
+
+(* Discriminates which kind of term is it.  
+   Note that there is no cases for [[DLAM] and [DLAMV].  These terms do not
+   make sense alone, but they must be preceeded by the application of
+   an operator.  
+*)
+
+val kind_of_term : constr -> kindOfTerm
+
+(*********************)
+(* Term constructors *)
+(*********************)
+
+(* Constructs a DeBrujin index *)
+val mkRel          : int -> constr
+
+(* Constructs an existential variable named "?" *)
+val mkExistential  : constr
+
+(* Constructs an existential variable named "?n" *)
+val mkMeta         : int -> constr
+
+(* Constructs a Variable *)
+val mkVar          : identifier -> constr
+
+(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
+val mkXtra         : string -> Coqast.t list -> constr
+
+(* Construct a type *)
+val mkSort         : sorts -> constr
+val mkProp         : constr
+val mkSet          : constr 
+val mkType         : Univ.universe -> constr
+val prop : sorts
+val spec : sorts
+val types : sorts 
+val type_0 : sorts
+val type_1 : sorts
+
+(* Construct an implicit (see implicit arguments in the RefMan) *)
+(* Used for extraction *)
+val mkImplicit     : constr
+val implicit_sort  : sorts
+
+(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
+(* (that means t2 is declared as the type of t1) *)
+val mkCast         : constr -> constr -> constr
+
+(* Constructs the product (x:t1)t2  -- x may be anonymous *)
+val mkProd         : name -> constr -> constr -> constr
+
+(* non-dependant product t1 -> t2 *)
+val mkArrow : constr -> constr -> constr
+
+(* named product *)
+val mkNamedProd : identifier -> constr -> constr -> constr
+
+(* Constructs the abstraction [x:t1]t2 *)
+val mkLambda       : name -> constr -> constr -> constr
+val mkNamedLambda : identifier -> constr -> constr -> constr
+
+(* If a = [| t1; ...; tn |], constructs the application (t1 ... tn) *)
+val mkAppL         : constr array -> constr
+val mkAppList      : constr list  -> constr
+
+(* Constructs a constant *) 
+(* The array of terms correspond to the variables introduced in the section *)
+val mkConst        : section_path -> constr array -> constr
+
+(* Constructs an abstract object *)
+val mkAbst         : section_path -> constr array -> constr
+
+(* Constructs the ith (co)inductive type of the block named sp *)
+(* The array of terms correspond to the variables introduced in the section *)
+val mkMutInd       : section_path -> int -> constr array -> constr
+
+(* Constructs the jth constructor of the ith (co)inductive type of the 
+   block named sp. The array of terms correspond to the variables
+   introduced in the section *)
+val mkMutConstruct : section_path -> int -> int -> constr array -> constr
+
+(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
+val mkMutCase      : case_info -> constr -> constr -> constr list -> constr
+val mkMutCaseA     : case_info -> constr -> constr -> constr array -> constr
+
+(* If recindxs = [|i1,...in|] 
+      typarray = [|t1,...tn|]
+      funnames = [f1,.....fn]
+      bodies   = [b1,.....bn]
+   then    
+
+      mkFix recindxs i typarray funnames bodies
+   
+   constructs the ith function of the block  
+
+    Fixpoint f1 [ctx1] = b1
+    with     f2 [ctx2] = b2
+    ...
+    with     fn [ctxn] = bn.
+
+   where the lenght of the jth context is ij.
+*)
+val mkFix          : int array -> int -> type_judgment array -> name list 
+                      -> constr array -> constr
+
+(* Similarly, but we assume the body already constructed *)
+val mkFixDlam      : int array -> int -> type_judgment array
+                     -> constr array -> constr 
+
+(* If typarray = [|t1,...tn|]
+      funnames = [f1,.....fn]
+      bodies   = [b1,.....bn]
+   then
+
+      mkCoFix i typsarray funnames bodies 
+
+   constructs the ith function of the block  
+   
+    CoFixpoint f1 = b1
+    with       f2 = b2
+    ...
+    with       fn = bn.
+
+*)
+val mkCoFix        : int -> type_judgment array -> name list 
+                     -> constr array -> constr
+
+(* Similarly, but we assume the body already constructed *)
+val mkCoFixDlam    : int -> type_judgment array -> constr array -> constr
+
+(********************)
+(* Term destructors *)
+(********************)
+
+(* Destructor operations : partial functions 
+   Raise invalid_arg "dest*" if the const has not the expected form *)
+
+(* Destructs a DeBrujin index *)
+val destRel          : constr -> int
+
+(* Destructs an existential variable *)
+val destMeta         : constr -> int
+val isMETA : constr -> bool
+
+(* Destructs a variable *)
+val destVar          : constr -> identifier
+
+(* Destructs an XTRA *)
+val destXtra        : constr -> string * Coqast.t list
+
+(* Destructs a sort *)
+val destSort         : constr -> sorts
+val contents_of_kind : constr -> contents
+val is_Prop          : constr -> bool (* true for Prop *) 
+val is_Set           : constr -> bool  (* true for Set *)
+val isprop           : constr -> bool (* true for DOP0 (Sort (Prop _)) *)
+val is_Type          : constr -> bool (* true for DOP0 (Sort (Type _)) *)
+val iskind           : constr -> bool (* true for Prop, Set and Type(_) *)
+
+val isType           : sorts -> bool (* true for Type(_) *)
+val is_small         : sorts -> bool (* true for Prop and Set *)
+
+(* Destructs a casted term *)
+val destCast         : constr -> constr * constr
+val cast_type : constr -> constr (* 2nd proj *)
+val cast_term : constr -> constr (* 1st proj *)
+val isCast : constr -> bool
+(* removes recursively the casts around a term *)
+(* strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c *)
+val strip_outer_cast : constr -> constr
+
+(* Destructs the product (x:t1)t2 *)
+val destProd          : constr -> name * constr * constr
+val hd_of_prod        : constr -> constr
+val hd_is_constructor : constr -> bool
+
+(* Destructs the abstraction [x:t1]t2 *)
+val destLambda       : constr -> name * constr * constr
+
+(* Destructs an application *)
+val destAppL   : constr -> constr array
+val isAppL     : constr -> bool
+val hd_app     : constr -> constr 
+val args_app   : constr -> constr array
+
+(* Destructs a constant *)
+val destConst     : constr -> section_path * constr array
+val path_of_const : constr -> section_path
+val args_of_const : constr -> constr array
+
+(* Destrucy an abstract term *)
+val destAbst         : constr -> section_path * constr array
+val path_of_abst : constr -> section_path
+val args_of_abst : constr -> constr array
+
+(* Destructs a (co)inductive type *)
+val destMutInd    : constr -> section_path * int * constr array
+val op_of_mind    : constr -> section_path * int
+val args_of_mind  : constr -> constr array
+val ci_of_mind    : constr -> case_info
+
+(* Destructs a constructor *)
+val destMutConstruct : constr -> section_path * int * int * constr array
+val op_of_mconstr    : constr -> (section_path * int) * int
+val args_of_mconstr  : constr -> constr array
+
+(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
+val destCase         : constr -> case_info * constr * constr * constr array
+
+(* Destructs the ith function of the block  
+    Fixpoint f1 [ctx1] = b1
+    with     f2 [ctx2] = b2
+    ...
+    with     fn [ctxn] = bn.
+
+   where the lenght of the jth context is ij.
+*)
+val destGralFix      : constr array -> constr array * Names.name list 
+                                        * constr array
+val destFix          : constr -> int array * int * type_judgment array
+                                  * Names.name list * constr array
+val destCoFix        : constr -> int * type_judgment array * Names.name list 
+                                  * constr array
+
+(* Provisoire, le temps de maitriser les cast *)
+val destUntypedFix          : constr -> int array * int * constr array
+                                  * Names.name list * constr array
+val destUntypedCoFix        : constr -> int * constr array * Names.name list 
+                                  * constr array
+
+(***********************************)
+(* Other term constructors         *)
+(***********************************)
+
+val abs_implicit : constr -> constr
+val lambda_implicit : constr -> constr
+val lambda_implicit_lift : int -> constr -> constr
+
+val applist : constr * constr list -> constr
+val applistc : constr -> constr list -> constr
+val appvect : constr * constr array -> constr
+val appvectc : constr -> constr array -> constr
+(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *)
+val prodn   : int -> (name * constr) list -> constr -> constr
+(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *)
+val lamn : int -> (name * constr) list -> constr -> constr
+
+(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *)
+val prod_it : constr -> (name * constr) list -> constr
+(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *)
+val lam_it : constr -> (name * constr) list -> constr
+
+
+(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
+   [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
+val to_lambda : int -> constr -> constr
+val to_prod : int -> constr -> constr
+
+(*********************************)
+(* Other term destructors        *)
+(*********************************)
+
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+val decompose_prod  : constr -> (name*constr) list * constr
+
+(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
+val decompose_lam   : constr -> (name*constr) list * constr
+
+(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+val decompose_prod_n  : int -> constr -> (name*constr) list * constr
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+val decompose_lam_n   : int -> constr -> (name*constr) list * constr
+
+(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
+ * gives n (casts are ignored) *)
+val nb_lam : constr -> int
+
+(* similar to nb_lam, but gives the number of products instead *)
+val nb_prod : constr -> int
+
+(********************************************************************)
+(*   various utility functions for implementing terms with bindings *)
+(********************************************************************)
+
+val extract_lifted : int * constr -> constr
+val insert_lifted : constr -> int * constr
+
+(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr)
+   push_and_lift adds a component to env and lifts l one step *)
+val push_and_lift :
+  name * constr -> (name * constr) list -> (int * constr) list 
+    -> (name * constr) list * (int * constr) list
+
+(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l)
+   raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')
+   where l' is l lifted n steps *)
+val push_and_liftl :
+  int -> (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* if T is not [x1:A1][x2:A2]....[xn:An]T' then (push_lam_and_liftl n env T l)
+   raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')
+   where l' is l lifted n steps *)
+val push_lam_and_liftl :
+  int -> (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of
+(na:name,T:constr), B : constr, na : name
+(prod_and_pop ((na,T)::tlenv) B l) gives (tlenv, (na:T)B, l')
+where l' is l lifted down one step *)
+val prod_and_pop :
+  (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* recusively applies prod_and_pop :
+if env = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv
+then
+(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)T,l') where
+l' is l lifted down n steps *)
+val prod_and_popl :
+  int -> (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *)
+val lam_and_pop :
+  (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
+ * (nan:Tan)...(na1:Ta1)B *)
+val lam_and_popl :
+  int -> (name * constr) list -> constr -> (int * constr) list
+    -> (name * constr) list * constr * (int * constr) list
+
+(* similar to lamn_and_pop but generates new names whenever the name is 
+ * Anonymous *)
+val lam_and_pop_named :
+  (name * constr) list -> constr ->(int * constr) list ->identifier list 
+    -> (name * constr) list * constr * (int * constr) list * identifier list
+
+(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
+ * but it generates names whenever nai=Anonymous *)
+val lam_and_popl_named :
+ int ->  (name * constr) list -> constr ->  (int * constr) list 
+  -> (name * constr) list * constr * (int * constr) list 
+(* [lambda_ize n T endpt]
+ * will pop off the first n products in T, then stick in endpt,
+ * properly lifted, and then push back the products, but as lambda-
+ * abstractions
+ *)
+val lambda_ize :int ->'a oper term -> 'a oper term -> 'a oper term
+
+(******************************************************************)
+(* Flattening and unflattening of embedded applications and casts *)
+(******************************************************************)
+
+(* if c is not an AppL, it is transformed into mkAppL [| c |] *)
+val ensure_appl : constr -> constr
+
+(* unflattens application lists *)
+val telescope_appl : constr -> constr
+(* flattens application lists *)
+val collapse_appl : constr -> constr
+val decomp_app : constr -> constr * constr list
+
+
+(********************************************)
+(* Misc functions on terms, judgments, etc  *)
+(********************************************)
+
+(* Level comparison for information extraction : Prop <= Type *)
+val same_kind : constr -> constr -> bool
+val le_kind : constr -> constr -> bool
+val le_kind_implicit : constr -> constr -> bool
+
+val pb_is_univ_adjust : conv_pb -> bool
+val pb_is_equal : conv_pb -> bool
+val pb_equal : conv_pb -> conv_pb
+val sort_hdchar : sorts -> string
+(* val sort_cmp : conv_pb -> sorts -> sorts -> bool *)
+
+
+(***************************)
+(* occurs check functions  *)                         
+(***************************)
+val occur_meta : constr -> bool
+val rel_vect : int -> int -> constr array
+
+(* (occur_const (s:section_path) c) -> true if constant s occurs in c,
+ * false otherwise *)
+val occur_const : section_path -> constr -> bool
+
+(* strips head casts and flattens head applications *)
+val strip_head_cast : constr -> constr
+val whd_castapp_stack : constr -> constr list -> constr * constr list
+val whd_castapp : constr -> constr
+val rename_bound_var : identifier list -> constr -> constr
+val eta_reduce_head : constr -> constr
+val eq_constr : constr -> constr -> bool
+val eta_eq_constr : constr -> constr -> bool
+val rename_rels : int -> constr -> (identifier * constr) list -> constr
+val clean_rhs : constr -> (identifier * constr) list -> constr
+val subst_term : constr -> constr -> constr
+val subst_term_eta_eq : constr -> constr -> constr
+val replace_consts :
+  (section_path * (identifier list * constr) option) list -> constr -> constr
+
+(* bl : (int,constr) Listmap.t = (int * constr) list *)
+(* c : constr *)
+(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *)
+(* Raises Not_found if c contains a meta that is not in the association list *)
+
+val subst_meta : (int * constr) list -> constr -> constr
+
+(* Transforms a constr into a matchable constr *)
+val matchable : constr -> constr
+val unmatchable: constr -> constr
+
+(* New hash-cons functions *)
+
+val hcons_constr:
+  (section_path -> section_path) *
+  (section_path -> section_path) *
+  (name -> name) *
+  (identifier -> identifier) *
+  (string -> string) 
+  ->
+    (constr -> constr) *
+    (constr -> constr) *
+    (type_judgment -> type_judgment)
+
+val hcons1_constr : constr -> constr