TFL/usyntax.sig
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
--- a/TFL/usyntax.sig	Tue May 20 11:47:33 1997 +0200
+++ b/TFL/usyntax.sig	Tue May 20 11:49:57 1997 +0200
@@ -2,133 +2,122 @@
 sig
   structure Utils : Utils_sig
 
-  type Type
-  type Term
-  type Preterm
   type 'a binding
 
-  datatype lambda = VAR   of {Name : string, Ty : Type}
-                  | CONST of {Name : string, Ty : Type}
-                  | COMB  of {Rator: Preterm, Rand : Preterm}
-                  | LAMB  of {Bvar : Preterm, Body : Preterm}
+  datatype lambda = VAR   of {Name : string, Ty : typ}
+                  | CONST of {Name : string, Ty : typ}
+                  | COMB  of {Rator: term, Rand : term}
+                  | LAMB  of {Bvar : term, Body : term}
 
-  val alpha : Type
-  val bool  : Type
-  val mk_preterm : Term -> Preterm
-  val drop_Trueprop : Preterm -> Preterm
+  val alpha : typ
+  val mk_preterm : cterm -> term
 
   (* Types *)
-  val type_vars  : Type -> Type list
-  val type_varsl : Type list -> Type list
-  val mk_type    : {Tyop: string, Args:Type list} -> Type
-  val dest_type  : Type -> {Tyop : string, Args : Type list}
-  val mk_vartype : string -> Type
-  val is_vartype : Type -> bool
-  val -->        : Type * Type -> Type
-  val strip_type : Type -> Type list * Type
-  val strip_prod_type : Type -> Type list
-  val match_type: Type -> Type -> Type binding list
+  val type_vars  : typ -> typ list
+  val type_varsl : typ list -> typ list
+  val mk_vartype : string -> typ
+  val is_vartype : typ -> bool
+  val -->        : typ * typ -> typ
+  val strip_type : typ -> typ list * typ
+  val strip_prod_type : typ -> typ list
+  val match_type: typ -> typ -> typ binding list
 
   (* Terms *)
-  val free_vars  : Preterm -> Preterm list
-  val free_varsl : Preterm list -> Preterm list
-  val free_vars_lr : Preterm -> Preterm list
-  val all_vars   : Preterm -> Preterm list
-  val all_varsl  : Preterm list -> Preterm list
-  val variant    : Preterm list -> Preterm -> Preterm
-  val type_of    : Preterm -> Type
-  val type_vars_in_term : Preterm -> Type list
-  val dest_term  : Preterm -> lambda
+  val free_vars  : term -> term list
+  val free_varsl : term list -> term list
+  val free_vars_lr : term -> term list
+  val all_vars   : term -> term list
+  val all_varsl  : term list -> term list
+  val variant    : term list -> term -> term
+  val type_vars_in_term : term -> typ list
+  val dest_term  : term -> lambda
   
   (* Prelogic *)
-  val aconv     : Preterm -> Preterm -> bool
-  val subst     : Preterm binding list -> Preterm -> Preterm
-  val inst      : Type binding list -> Preterm -> Preterm
-  val beta_conv : Preterm -> Preterm
+  val aconv     : term -> term -> bool
+  val subst     : term binding list -> term -> term
+  val inst      : typ binding list -> term -> term
+  val beta_conv : term -> term
 
   (* Construction routines *)
-  val mk_prop   :Preterm -> Preterm
-  val mk_var    :{Name : string, Ty : Type} -> Preterm
-  val mk_const  :{Name : string, Ty : Type} -> Preterm
-  val mk_comb   :{Rator : Preterm, Rand : Preterm} -> Preterm
-  val mk_abs    :{Bvar  : Preterm, Body : Preterm} -> Preterm
+  val mk_var    :{Name : string, Ty : typ} -> term
+  val mk_const  :{Name : string, Ty : typ} -> term
+  val mk_comb   :{Rator : term, Rand : term} -> term
+  val mk_abs    :{Bvar  : term, Body : term} -> term
 
-  val mk_eq     :{lhs : Preterm, rhs : Preterm} -> Preterm
-  val mk_imp    :{ant : Preterm, conseq :  Preterm} -> Preterm
-  val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm
-  val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm
-  val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm
-  val mk_conj   :{conj1 : Preterm, conj2 : Preterm} -> Preterm
-  val mk_disj   :{disj1 : Preterm, disj2 : Preterm} -> Preterm
-  val mk_pabs   :{varstruct : Preterm, body : Preterm} -> Preterm
+  val mk_imp    :{ant : term, conseq :  term} -> term
+  val mk_select :{Bvar : term, Body : term} -> term
+  val mk_forall :{Bvar : term, Body : term} -> term
+  val mk_exists :{Bvar : term, Body : term} -> term
+  val mk_conj   :{conj1 : term, conj2 : term} -> term
+  val mk_disj   :{disj1 : term, disj2 : term} -> term
+  val mk_pabs   :{varstruct : term, body : term} -> term
 
   (* Destruction routines *)
-  val dest_var  : Preterm -> {Name : string, Ty : Type}
-  val dest_const: Preterm -> {Name : string, Ty : Type}
-  val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm}
-  val dest_abs  : Preterm -> {Bvar : Preterm, Body : Preterm}
-  val dest_eq     : Preterm -> {lhs : Preterm, rhs : Preterm}
-  val dest_imp    : Preterm -> {ant : Preterm, conseq : Preterm}
-  val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm}
-  val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm}
-  val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm}
-  val dest_neg    : Preterm -> Preterm
-  val dest_conj   : Preterm -> {conj1 : Preterm, conj2 : Preterm}
-  val dest_disj   : Preterm -> {disj1 : Preterm, disj2 : Preterm}
-  val dest_pair   : Preterm -> {fst : Preterm, snd : Preterm}
-  val dest_pabs   : Preterm -> {varstruct : Preterm, body : Preterm}
+  val dest_var  : term -> {Name : string, Ty : typ}
+  val dest_const: term -> {Name : string, Ty : typ}
+  val dest_comb : term -> {Rator : term, Rand : term}
+  val dest_abs  : term -> {Bvar : term, Body : term}
+  val dest_eq     : term -> {lhs : term, rhs : term}
+  val dest_imp    : term -> {ant : term, conseq : term}
+  val dest_select : term -> {Bvar : term, Body : term}
+  val dest_forall : term -> {Bvar : term, Body : term}
+  val dest_exists : term -> {Bvar : term, Body : term}
+  val dest_neg    : term -> term
+  val dest_conj   : term -> {conj1 : term, conj2 : term}
+  val dest_disj   : term -> {disj1 : term, disj2 : term}
+  val dest_pair   : term -> {fst : term, snd : term}
+  val dest_pabs   : term -> {varstruct : term, body : term}
 
-  val lhs   : Preterm -> Preterm
-  val rhs   : Preterm -> Preterm
-  val rator : Preterm -> Preterm
-  val rand  : Preterm -> Preterm
-  val bvar  : Preterm -> Preterm
-  val body  : Preterm -> Preterm
+  val lhs   : term -> term
+  val rhs   : term -> term
+  val rator : term -> term
+  val rand  : term -> term
+  val bvar  : term -> term
+  val body  : term -> term
   
 
   (* Query routines *)
-  val is_var  : Preterm -> bool
-  val is_const: Preterm -> bool
-  val is_comb : Preterm -> bool
-  val is_abs  : Preterm -> bool
-  val is_eq     : Preterm -> bool
-  val is_imp    : Preterm -> bool
-  val is_forall : Preterm -> bool 
-  val is_exists : Preterm -> bool 
-  val is_neg    : Preterm -> bool
-  val is_conj   : Preterm -> bool
-  val is_disj   : Preterm -> bool
-  val is_pair   : Preterm -> bool
-  val is_pabs   : Preterm -> bool
+  val is_var  : term -> bool
+  val is_const: term -> bool
+  val is_comb : term -> bool
+  val is_abs  : term -> bool
+  val is_eq     : term -> bool
+  val is_imp    : term -> bool
+  val is_forall : term -> bool 
+  val is_exists : term -> bool 
+  val is_neg    : term -> bool
+  val is_conj   : term -> bool
+  val is_disj   : term -> bool
+  val is_pair   : term -> bool
+  val is_pabs   : term -> bool
 
-  (* Construction of a Preterm from a list of Preterms *)
-  val list_mk_comb   : (Preterm * Preterm list) -> Preterm
-  val list_mk_abs    : (Preterm list * Preterm) -> Preterm
-  val list_mk_imp    : (Preterm list * Preterm) -> Preterm
-  val list_mk_forall : (Preterm list * Preterm) -> Preterm
-  val list_mk_exists : (Preterm list * Preterm) -> Preterm
-  val list_mk_conj   : Preterm list -> Preterm
-  val list_mk_disj   : Preterm list -> Preterm
+  (* Construction of a term from a list of Preterms *)
+  val list_mk_abs    : (term list * term) -> term
+  val list_mk_imp    : (term list * term) -> term
+  val list_mk_forall : (term list * term) -> term
+  val list_mk_exists : (term list * term) -> term
+  val list_mk_conj   : term list -> term
+  val list_mk_disj   : term list -> term
 
-  (* Destructing a Preterm to a list of Preterms *)
-  val strip_comb     : Preterm -> (Preterm * Preterm list)
-  val strip_abs      : Preterm -> (Preterm list * Preterm)
-  val strip_imp      : Preterm -> (Preterm list * Preterm)
-  val strip_forall   : Preterm -> (Preterm list * Preterm)
-  val strip_exists   : Preterm -> (Preterm list * Preterm)
-  val strip_conj     : Preterm -> Preterm list
-  val strip_disj     : Preterm -> Preterm list
-  val strip_pair     : Preterm -> Preterm list
+  (* Destructing a term to a list of Preterms *)
+  val strip_comb     : term -> (term * term list)
+  val strip_abs      : term -> (term list * term)
+  val strip_imp      : term -> (term list * term)
+  val strip_forall   : term -> (term list * term)
+  val strip_exists   : term -> (term list * term)
+  val strip_conj     : term -> term list
+  val strip_disj     : term -> term list
+  val strip_pair     : term -> term list
 
   (* Miscellaneous *)
-  val mk_vstruct : Type -> Preterm list -> Preterm
-  val gen_all    : Preterm -> Preterm
-  val find_term  : (Preterm -> bool) -> Preterm -> Preterm
-  val find_terms : (Preterm -> bool) -> Preterm -> Preterm list
-  val dest_relation : Preterm -> Preterm * Preterm * Preterm
-  val is_WFR : Preterm -> bool
-  val ARB : Type -> Preterm
+  val mk_vstruct : typ -> term list -> term
+  val gen_all    : term -> term
+  val find_term  : (term -> bool) -> term -> term
+  val find_terms : (term -> bool) -> term -> term list
+  val dest_relation : term -> term * term * term
+  val is_WFR : term -> bool
+  val ARB : typ -> term
 
   (* Prettyprinting *)
-  val Term_to_string : Term -> string
+  val Term_to_string : cterm -> string
 end;