--- 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;