TFL/usyntax.sig
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 3713 8a1f7d5b1eff
permissions -rw-r--r--
adapted extend_trfunsT;
     1 (*  Title:      TFL/usyntax
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Emulation of HOL's abstract syntax functions
     7 *)
     8 
     9 signature USyntax_sig =
    10 sig
    11   structure Utils : Utils_sig
    12 
    13   datatype lambda = VAR   of {Name : string, Ty : typ}
    14                   | CONST of {Name : string, Ty : typ}
    15                   | COMB  of {Rator: term, Rand : term}
    16                   | LAMB  of {Bvar : term, Body : term}
    17 
    18   val alpha : typ
    19 
    20   (* Types *)
    21   val type_vars  : typ -> typ list
    22   val type_varsl : typ list -> typ list
    23   val mk_vartype : string -> typ
    24   val is_vartype : typ -> bool
    25   val strip_prod_type : typ -> typ list
    26 
    27   (* Terms *)
    28   val free_vars_lr : term -> term list
    29   val type_vars_in_term : term -> typ list
    30   val dest_term  : term -> lambda
    31   
    32   (* Prelogic *)
    33   val inst      : (typ*typ) list -> term -> term
    34 
    35   (* Construction routines *)
    36   val mk_abs    :{Bvar  : term, Body : term} -> term
    37 
    38   val mk_imp    :{ant : term, conseq :  term} -> term
    39   val mk_select :{Bvar : term, Body : term} -> term
    40   val mk_forall :{Bvar : term, Body : term} -> term
    41   val mk_exists :{Bvar : term, Body : term} -> term
    42   val mk_conj   :{conj1 : term, conj2 : term} -> term
    43   val mk_disj   :{disj1 : term, disj2 : term} -> term
    44   val mk_pabs   :{varstruct : term, body : term} -> term
    45 
    46   (* Destruction routines *)
    47   val dest_const: term -> {Name : string, Ty : typ}
    48   val dest_comb : term -> {Rator : term, Rand : term}
    49   val dest_abs  : term -> {Bvar : term, Body : term}
    50   val dest_eq     : term -> {lhs : term, rhs : term}
    51   val dest_imp    : term -> {ant : term, conseq : term}
    52   val dest_forall : term -> {Bvar : term, Body : term}
    53   val dest_exists : term -> {Bvar : term, Body : term}
    54   val dest_neg    : term -> term
    55   val dest_conj   : term -> {conj1 : term, conj2 : term}
    56   val dest_disj   : term -> {disj1 : term, disj2 : term}
    57   val dest_pair   : term -> {fst : term, snd : term}
    58   val dest_pabs   : term -> {varstruct : term, body : term}
    59 
    60   val lhs   : term -> term
    61   val rhs   : term -> term
    62   val rand  : term -> term
    63 
    64   (* Query routines *)
    65   val is_imp    : term -> bool
    66   val is_forall : term -> bool 
    67   val is_exists : term -> bool 
    68   val is_neg    : term -> bool
    69   val is_conj   : term -> bool
    70   val is_disj   : term -> bool
    71   val is_pair   : term -> bool
    72   val is_pabs   : term -> bool
    73 
    74   (* Construction of a term from a list of Preterms *)
    75   val list_mk_abs    : (term list * term) -> term
    76   val list_mk_imp    : (term list * term) -> term
    77   val list_mk_forall : (term list * term) -> term
    78   val list_mk_conj   : term list -> term
    79 
    80   (* Destructing a term to a list of Preterms *)
    81   val strip_comb     : term -> (term * term list)
    82   val strip_abs      : term -> (term list * term)
    83   val strip_imp      : term -> (term list * term)
    84   val strip_forall   : term -> (term list * term)
    85   val strip_exists   : term -> (term list * term)
    86   val strip_disj     : term -> term list
    87 
    88   (* Miscellaneous *)
    89   val mk_vstruct : typ -> term list -> term
    90   val gen_all    : term -> term
    91   val find_term  : (term -> bool) -> term -> term option
    92   val dest_relation : term -> term * term * term
    93   val is_WFR : term -> bool
    94   val ARB : typ -> term
    95 end;