Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 40 insertions, 19 deletions

diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 51853089..131e4170 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 9032 2006-07-07 16:30:34Z herbelin $ i*)
+(*i $Id: topconstr.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -35,7 +35,7 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
-      (identifier list * cases_pattern list * aconstr) list
+      (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
@@ -43,30 +43,50 @@ type aconstr =
   | APatVar of patvar
   | ACast of aconstr * cast_type * aconstr
 
+(**********************************************************************)
+(* Translate a rawconstr into a notation given the list of variables  *)
+(* bound by the notation; also interpret recursive patterns           *) 
+
+val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+
+(* Name of the special identifier used to encode recursive notations  *)
+val ldots_var : identifier
+
+(* Equality of rawconstr (warning: only partially implemented) *)
+val eq_rawconstr : rawconstr -> rawconstr -> bool
+
+(**********************************************************************)
+(* Re-interpret a notation as a rawconstr, taking care of binders     *)
+
 val rawconstr_of_aconstr_with_binders : loc -> 
-  (identifier -> 'a -> identifier * 'a) ->
+  ('a -> identifier -> 'a * identifier) ->
   ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
 
-val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr
+(**********************************************************************)
+(* Substitution of kernel names, avoiding a list of bound identifiers *)
 
-val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr
 
-val eq_rawconstr : rawconstr -> rawconstr -> bool
+(**********************************************************************)
+(* [match_aconstr metas] matches a rawconstr against an aconstr with  *)
+(* metavariables in [metas]; raise [No_match] if the matching fails   *)
 
-(* [match_aconstr metas] match a rawconstr against an aconstr with
-   metavariables in [metas]; it raises [No_match] if the matching fails *)
 exception No_match
 
 type scope_name = string
+
+type tmp_scope_name = scope_name
+
 type interpretation = 
-    (identifier * (scope_name option * scope_name list)) list * aconstr
+    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
 
 val match_aconstr : rawconstr -> interpretation ->
-      (rawconstr * (scope_name option * scope_name list)) list
+      (rawconstr * (tmp_scope_name option * scope_name list)) list
 
-(*s Concrete syntax for terms *)
+(**********************************************************************)
+(*s Concrete syntax for terms                                         *)
 
 type notation = string
 
@@ -128,18 +148,21 @@ and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * constr_expr
 
+(**********************************************************************)
+(* Utilities on constr_expr                                           *)
 
 val constr_loc : constr_expr -> loc
 
-val cases_pattern_loc : cases_pattern_expr -> loc
+val cases_pattern_expr_loc : cases_pattern_expr -> loc
 
 val replace_vars_constr_expr :
   (identifier * identifier) list -> constr_expr -> constr_expr
 
+val free_vars_of_constr_expr : constr_expr -> Idset.t
 val occur_var_constr_expr : identifier -> constr_expr -> bool
 
 (* Specific function for interning "in indtype" syntax of "match" *)
-val names_of_cases_indtype : constr_expr -> identifier list
+val ids_of_cases_indtype : constr_expr -> identifier list
 
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
@@ -172,10 +195,11 @@ val names_of_local_binders : local_binder list -> name located list
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
 val map_constr_expr_with_binders :
-  ('a -> constr_expr -> constr_expr) ->
-      (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
+  (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
+      'a -> constr_expr -> constr_expr
 
-(* Concrete syntax for modules and modules types *)
+(**********************************************************************)
+(* Concrete syntax for modules and module types                       *)
 
 type with_declaration_ast = 
   | CWith_Module of identifier list located * qualid located
@@ -188,6 +212,3 @@ type module_type_ast =
 type module_ast = 
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
-
-(* Special identifier to encode recursive notations *)
-val ldots_var : identifier