paulson@3302: (*  Title:      TFL/usyntax
paulson@3302:     ID:         $Id$
paulson@3302:     Author:     Konrad Slind, Cambridge University Computer Laboratory
paulson@3302:     Copyright   1997  University of Cambridge
paulson@3302: 
paulson@3302: Emulation of HOL's abstract syntax functions
paulson@3302: *)
paulson@3302: 
paulson@2112: signature USyntax_sig =
paulson@2112: sig
paulson@2112:   structure Utils : Utils_sig
paulson@2112: 
paulson@3245:   datatype lambda = VAR   of {Name : string, Ty : typ}
paulson@3245:                   | CONST of {Name : string, Ty : typ}
paulson@3245:                   | COMB  of {Rator: term, Rand : term}
paulson@3245:                   | LAMB  of {Bvar : term, Body : term}
paulson@2112: 
paulson@3245:   val alpha : typ
paulson@2112: 
paulson@2112:   (* Types *)
paulson@3245:   val type_vars  : typ -> typ list
paulson@3245:   val type_varsl : typ list -> typ list
paulson@3245:   val mk_vartype : string -> typ
paulson@3245:   val is_vartype : typ -> bool
paulson@3245:   val strip_prod_type : typ -> typ list
paulson@2112: 
paulson@2112:   (* Terms *)
paulson@3245:   val free_vars_lr : term -> term list
paulson@3245:   val type_vars_in_term : term -> typ list
paulson@3245:   val dest_term  : term -> lambda
paulson@2112:   
paulson@2112:   (* Prelogic *)
paulson@3353:   val inst      : (typ*typ) list -> term -> term
paulson@2112: 
paulson@2112:   (* Construction routines *)
paulson@3245:   val mk_abs    :{Bvar  : term, Body : term} -> term
paulson@2112: 
paulson@3245:   val mk_imp    :{ant : term, conseq :  term} -> term
paulson@3245:   val mk_select :{Bvar : term, Body : term} -> term
paulson@3245:   val mk_forall :{Bvar : term, Body : term} -> term
paulson@3245:   val mk_exists :{Bvar : term, Body : term} -> term
paulson@3245:   val mk_conj   :{conj1 : term, conj2 : term} -> term
paulson@3245:   val mk_disj   :{disj1 : term, disj2 : term} -> term
paulson@3245:   val mk_pabs   :{varstruct : term, body : term} -> term
paulson@2112: 
paulson@2112:   (* Destruction routines *)
paulson@3245:   val dest_const: term -> {Name : string, Ty : typ}
paulson@3245:   val dest_comb : term -> {Rator : term, Rand : term}
paulson@3245:   val dest_abs  : term -> {Bvar : term, Body : term}
paulson@3245:   val dest_eq     : term -> {lhs : term, rhs : term}
paulson@3245:   val dest_imp    : term -> {ant : term, conseq : term}
paulson@3245:   val dest_forall : term -> {Bvar : term, Body : term}
paulson@3245:   val dest_exists : term -> {Bvar : term, Body : term}
paulson@3245:   val dest_neg    : term -> term
paulson@3245:   val dest_conj   : term -> {conj1 : term, conj2 : term}
paulson@3245:   val dest_disj   : term -> {disj1 : term, disj2 : term}
paulson@3245:   val dest_pair   : term -> {fst : term, snd : term}
paulson@3245:   val dest_pabs   : term -> {varstruct : term, body : term}
paulson@2112: 
paulson@3245:   val lhs   : term -> term
paulson@3245:   val rhs   : term -> term
paulson@3245:   val rand  : term -> term
paulson@2112: 
paulson@2112:   (* Query routines *)
paulson@3245:   val is_imp    : term -> bool
paulson@3245:   val is_forall : term -> bool 
paulson@3245:   val is_exists : term -> bool 
paulson@3245:   val is_neg    : term -> bool
paulson@3245:   val is_conj   : term -> bool
paulson@3245:   val is_disj   : term -> bool
paulson@3245:   val is_pair   : term -> bool
paulson@3245:   val is_pabs   : term -> bool
paulson@2112: 
paulson@3245:   (* Construction of a term from a list of Preterms *)
paulson@3245:   val list_mk_abs    : (term list * term) -> term
paulson@3245:   val list_mk_imp    : (term list * term) -> term
paulson@3245:   val list_mk_forall : (term list * term) -> term
paulson@3245:   val list_mk_conj   : term list -> term
paulson@2112: 
paulson@3245:   (* Destructing a term to a list of Preterms *)
paulson@3245:   val strip_comb     : term -> (term * term list)
paulson@3245:   val strip_abs      : term -> (term list * term)
paulson@3245:   val strip_imp      : term -> (term list * term)
paulson@3245:   val strip_forall   : term -> (term list * term)
paulson@3245:   val strip_exists   : term -> (term list * term)
paulson@3245:   val strip_disj     : term -> term list
paulson@2112: 
paulson@2112:   (* Miscellaneous *)
paulson@3245:   val mk_vstruct : typ -> term list -> term
paulson@3245:   val gen_all    : term -> term
paulson@3405:   val find_term  : (term -> bool) -> term -> term option
paulson@3245:   val dest_relation : term -> term * term * term
paulson@3245:   val is_WFR : term -> bool
paulson@3245:   val ARB : typ -> term
paulson@2112: end;