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