TFL/usyntax.sig
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
     1 signature USyntax_sig =
     2 sig
     3   structure Utils : Utils_sig
     4 
     5   type Type
     6   type Term
     7   type Preterm
     8   type 'a binding
     9 
    10   datatype lambda = VAR   of {Name : string, Ty : Type}
    11                   | CONST of {Name : string, Ty : Type}
    12                   | COMB  of {Rator: Preterm, Rand : Preterm}
    13                   | LAMB  of {Bvar : Preterm, Body : Preterm}
    14 
    15   val alpha : Type
    16   val bool  : Type
    17   val mk_preterm : Term -> Preterm
    18   val drop_Trueprop : Preterm -> Preterm
    19 
    20   (* Types *)
    21   val type_vars  : Type -> Type list
    22   val type_varsl : Type list -> Type list
    23   val mk_type    : {Tyop: string, Args:Type list} -> Type
    24   val dest_type  : Type -> {Tyop : string, Args : Type list}
    25   val mk_vartype : string -> Type
    26   val is_vartype : Type -> bool
    27   val -->        : Type * Type -> Type
    28   val strip_type : Type -> Type list * Type
    29   val strip_prod_type : Type -> Type list
    30   val match_type: Type -> Type -> Type binding list
    31 
    32   (* Terms *)
    33   val free_vars  : Preterm -> Preterm list
    34   val free_varsl : Preterm list -> Preterm list
    35   val free_vars_lr : Preterm -> Preterm list
    36   val all_vars   : Preterm -> Preterm list
    37   val all_varsl  : Preterm list -> Preterm list
    38   val variant    : Preterm list -> Preterm -> Preterm
    39   val type_of    : Preterm -> Type
    40   val type_vars_in_term : Preterm -> Type list
    41   val dest_term  : Preterm -> lambda
    42   
    43   (* Prelogic *)
    44   val aconv     : Preterm -> Preterm -> bool
    45   val subst     : Preterm binding list -> Preterm -> Preterm
    46   val inst      : Type binding list -> Preterm -> Preterm
    47   val beta_conv : Preterm -> Preterm
    48 
    49   (* Construction routines *)
    50   val mk_prop   :Preterm -> Preterm
    51   val mk_var    :{Name : string, Ty : Type} -> Preterm
    52   val mk_const  :{Name : string, Ty : Type} -> Preterm
    53   val mk_comb   :{Rator : Preterm, Rand : Preterm} -> Preterm
    54   val mk_abs    :{Bvar  : Preterm, Body : Preterm} -> Preterm
    55 
    56   val mk_eq     :{lhs : Preterm, rhs : Preterm} -> Preterm
    57   val mk_imp    :{ant : Preterm, conseq :  Preterm} -> Preterm
    58   val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm
    59   val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm
    60   val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm
    61   val mk_conj   :{conj1 : Preterm, conj2 : Preterm} -> Preterm
    62   val mk_disj   :{disj1 : Preterm, disj2 : Preterm} -> Preterm
    63   val mk_pabs   :{varstruct : Preterm, body : Preterm} -> Preterm
    64 
    65   (* Destruction routines *)
    66   val dest_var  : Preterm -> {Name : string, Ty : Type}
    67   val dest_const: Preterm -> {Name : string, Ty : Type}
    68   val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm}
    69   val dest_abs  : Preterm -> {Bvar : Preterm, Body : Preterm}
    70   val dest_eq     : Preterm -> {lhs : Preterm, rhs : Preterm}
    71   val dest_imp    : Preterm -> {ant : Preterm, conseq : Preterm}
    72   val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm}
    73   val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm}
    74   val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm}
    75   val dest_neg    : Preterm -> Preterm
    76   val dest_conj   : Preterm -> {conj1 : Preterm, conj2 : Preterm}
    77   val dest_disj   : Preterm -> {disj1 : Preterm, disj2 : Preterm}
    78   val dest_pair   : Preterm -> {fst : Preterm, snd : Preterm}
    79   val dest_pabs   : Preterm -> {varstruct : Preterm, body : Preterm}
    80 
    81   val lhs   : Preterm -> Preterm
    82   val rhs   : Preterm -> Preterm
    83   val rator : Preterm -> Preterm
    84   val rand  : Preterm -> Preterm
    85   val bvar  : Preterm -> Preterm
    86   val body  : Preterm -> Preterm
    87   
    88 
    89   (* Query routines *)
    90   val is_var  : Preterm -> bool
    91   val is_const: Preterm -> bool
    92   val is_comb : Preterm -> bool
    93   val is_abs  : Preterm -> bool
    94   val is_eq     : Preterm -> bool
    95   val is_imp    : Preterm -> bool
    96   val is_forall : Preterm -> bool 
    97   val is_exists : Preterm -> bool 
    98   val is_neg    : Preterm -> bool
    99   val is_conj   : Preterm -> bool
   100   val is_disj   : Preterm -> bool
   101   val is_pair   : Preterm -> bool
   102   val is_pabs   : Preterm -> bool
   103 
   104   (* Construction of a Preterm from a list of Preterms *)
   105   val list_mk_comb   : (Preterm * Preterm list) -> Preterm
   106   val list_mk_abs    : (Preterm list * Preterm) -> Preterm
   107   val list_mk_imp    : (Preterm list * Preterm) -> Preterm
   108   val list_mk_forall : (Preterm list * Preterm) -> Preterm
   109   val list_mk_exists : (Preterm list * Preterm) -> Preterm
   110   val list_mk_conj   : Preterm list -> Preterm
   111   val list_mk_disj   : Preterm list -> Preterm
   112 
   113   (* Destructing a Preterm to a list of Preterms *)
   114   val strip_comb     : Preterm -> (Preterm * Preterm list)
   115   val strip_abs      : Preterm -> (Preterm list * Preterm)
   116   val strip_imp      : Preterm -> (Preterm list * Preterm)
   117   val strip_forall   : Preterm -> (Preterm list * Preterm)
   118   val strip_exists   : Preterm -> (Preterm list * Preterm)
   119   val strip_conj     : Preterm -> Preterm list
   120   val strip_disj     : Preterm -> Preterm list
   121   val strip_pair     : Preterm -> Preterm list
   122 
   123   (* Miscellaneous *)
   124   val mk_vstruct : Type -> Preterm list -> Preterm
   125   val gen_all    : Preterm -> Preterm
   126   val find_term  : (Preterm -> bool) -> Preterm -> Preterm
   127   val find_terms : (Preterm -> bool) -> Preterm -> Preterm list
   128   val dest_relation : Preterm -> Preterm * Preterm * Preterm
   129   val is_WFR : Preterm -> bool
   130   val ARB : Type -> Preterm
   131 
   132   (* Prettyprinting *)
   133   val Term_to_string : Term -> string
   134 end;