src/Pure/term.ML
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 35986 b7fcca3d9a44
child 38980 af73cf0dc31f
permissions -rw-r--r--
storing options for prolog code generation in the theory
     1 (*  Title:      Pure/term.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Simply typed lambda-calculus: types, terms, and basic operations.
     6 *)
     7 
     8 infix 9 $;
     9 infixr 5 -->;
    10 infixr --->;
    11 infix aconv;
    12 
    13 signature BASIC_TERM =
    14 sig
    15   type indexname = string * int
    16   type class = string
    17   type sort = class list
    18   type arity = string * sort list * sort
    19   datatype typ =
    20     Type  of string * typ list |
    21     TFree of string * sort |
    22     TVar  of indexname * sort
    23   datatype term =
    24     Const of string * typ |
    25     Free of string * typ |
    26     Var of indexname * typ |
    27     Bound of int |
    28     Abs of string * typ * term |
    29     $ of term * term
    30   exception TYPE of string * typ list * term list
    31   exception TERM of string * term list
    32   val dummyS: sort
    33   val dummyT: typ
    34   val no_dummyT: typ -> typ
    35   val --> : typ * typ -> typ
    36   val ---> : typ list * typ -> typ
    37   val dest_Type: typ -> string * typ list
    38   val dest_TVar: typ -> indexname * sort
    39   val dest_TFree: typ -> string * sort
    40   val is_Bound: term -> bool
    41   val is_Const: term -> bool
    42   val is_Free: term -> bool
    43   val is_Var: term -> bool
    44   val is_TVar: typ -> bool
    45   val dest_Const: term -> string * typ
    46   val dest_Free: term -> string * typ
    47   val dest_Var: term -> indexname * typ
    48   val dest_comb: term -> term * term
    49   val domain_type: typ -> typ
    50   val range_type: typ -> typ
    51   val binder_types: typ -> typ list
    52   val body_type: typ -> typ
    53   val strip_type: typ -> typ list * typ
    54   val type_of1: typ list * term -> typ
    55   val type_of: term -> typ
    56   val fastype_of1: typ list * term -> typ
    57   val fastype_of: term -> typ
    58   val list_abs: (string * typ) list * term -> term
    59   val strip_abs: term -> (string * typ) list * term
    60   val strip_abs_body: term -> term
    61   val strip_abs_vars: term -> (string * typ) list
    62   val strip_qnt_body: string -> term -> term
    63   val strip_qnt_vars: string -> term -> (string * typ) list
    64   val list_comb: term * term list -> term
    65   val strip_comb: term -> term * term list
    66   val head_of: term -> term
    67   val size_of_term: term -> int
    68   val size_of_typ: typ -> int
    69   val map_atyps: (typ -> typ) -> typ -> typ
    70   val map_aterms: (term -> term) -> term -> term
    71   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    72   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    73   val map_types: (typ -> typ) -> term -> term
    74   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    75   val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
    76   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    77   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    78   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    79   val burrow_types: (typ list -> typ list) -> term list -> term list
    80   val aconv: term * term -> bool
    81   val propT: typ
    82   val strip_all_body: term -> term
    83   val strip_all_vars: term -> (string * typ) list
    84   val incr_bv: int * int * term -> term
    85   val incr_boundvars: int -> term -> term
    86   val add_loose_bnos: term * int * int list -> int list
    87   val loose_bnos: term -> int list
    88   val loose_bvar: term * int -> bool
    89   val loose_bvar1: term * int -> bool
    90   val subst_bounds: term list * term -> term
    91   val subst_bound: term * term -> term
    92   val betapply: term * term -> term
    93   val betapplys: term * term list -> term
    94   val subst_free: (term * term) list -> term -> term
    95   val abstract_over: term * term -> term
    96   val lambda: term -> term -> term
    97   val absfree: string * typ * term -> term
    98   val absdummy: typ * term -> term
    99   val list_abs_free: (string * typ) list * term -> term
   100   val list_all_free: (string * typ) list * term -> term
   101   val list_all: (string * typ) list * term -> term
   102   val subst_atomic: (term * term) list -> term -> term
   103   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   104   val subst_atomic_types: (typ * typ) list -> term -> term
   105   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   106   val subst_TVars: (indexname * typ) list -> term -> term
   107   val subst_Vars: (indexname * term) list -> term -> term
   108   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   109   val is_first_order: string list -> term -> bool
   110   val maxidx_of_typ: typ -> int
   111   val maxidx_of_typs: typ list -> int
   112   val maxidx_of_term: term -> int
   113   val exists_subtype: (typ -> bool) -> typ -> bool
   114   val exists_type: (typ -> bool) -> term -> bool
   115   val exists_subterm: (term -> bool) -> term -> bool
   116   val exists_Const: (string * typ -> bool) -> term -> bool
   117   val show_question_marks: bool Unsynchronized.ref
   118 end;
   119 
   120 signature TERM =
   121 sig
   122   include BASIC_TERM
   123   val aT: sort -> typ
   124   val itselfT: typ -> typ
   125   val a_itselfT: typ
   126   val all: typ -> term
   127   val argument_type_of: term -> int -> typ
   128   val add_tvar_namesT: typ -> indexname list -> indexname list
   129   val add_tvar_names: term -> indexname list -> indexname list
   130   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   131   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   132   val add_var_names: term -> indexname list -> indexname list
   133   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   134   val add_tfree_namesT: typ -> string list -> string list
   135   val add_tfree_names: term -> string list -> string list
   136   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   137   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   138   val add_free_names: term -> string list -> string list
   139   val add_frees: term -> (string * typ) list -> (string * typ) list
   140   val add_const_names: term -> string list -> string list
   141   val add_consts: term -> (string * typ) list -> (string * typ) list
   142   val hidden_polymorphism: term -> (indexname * sort) list
   143   val declare_typ_names: typ -> Name.context -> Name.context
   144   val declare_term_names: term -> Name.context -> Name.context
   145   val declare_term_frees: term -> Name.context -> Name.context
   146   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   147   val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   148   val eq_ix: indexname * indexname -> bool
   149   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   150   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   151   val aconv_untyped: term * term -> bool
   152   val could_unify: term * term -> bool
   153   val strip_abs_eta: int -> term -> (string * typ) list * term
   154   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   155   val map_abs_vars: (string -> string) -> term -> term
   156   val rename_abs: term -> term -> term -> term option
   157   val lambda_name: string * term -> term -> term
   158   val close_schematic_term: term -> term
   159   val maxidx_typ: typ -> int -> int
   160   val maxidx_typs: typ list -> int -> int
   161   val maxidx_term: term -> int -> int
   162   val has_abs: term -> bool
   163   val dest_abs: string * typ * term -> string * term
   164   val dummy_patternN: string
   165   val dummy_pattern: typ -> term
   166   val is_dummy_pattern: term -> bool
   167   val free_dummy_patterns: term -> Name.context -> term * Name.context
   168   val no_dummy_patterns: term -> term
   169   val replace_dummy_patterns: term -> int -> term * int
   170   val is_replaced_dummy_pattern: indexname -> bool
   171   val show_dummy_patterns: term -> term
   172   val string_of_vname: indexname -> string
   173   val string_of_vname': indexname -> string
   174 end;
   175 
   176 structure Term: TERM =
   177 struct
   178 
   179 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   180   for resolution.*)
   181 type indexname = string * int;
   182 
   183 (* Types are classified by sorts. *)
   184 type class = string;
   185 type sort  = class list;
   186 type arity = string * sort list * sort;
   187 
   188 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   189 datatype typ = Type  of string * typ list
   190              | TFree of string * sort
   191              | TVar  of indexname * sort;
   192 
   193 (*Terms.  Bound variables are indicated by depth number.
   194   Free variables, (scheme) variables and constants have names.
   195   An term is "closed" if every bound variable of level "lev"
   196   is enclosed by at least "lev" abstractions.
   197 
   198   It is possible to create meaningless terms containing loose bound vars
   199   or type mismatches.  But such terms are not allowed in rules. *)
   200 
   201 datatype term =
   202     Const of string * typ
   203   | Free  of string * typ
   204   | Var   of indexname * typ
   205   | Bound of int
   206   | Abs   of string*typ*term
   207   | op $  of term*term;
   208 
   209 (*Errors involving type mismatches*)
   210 exception TYPE of string * typ list * term list;
   211 
   212 (*Errors errors involving terms*)
   213 exception TERM of string * term list;
   214 
   215 (*Note variable naming conventions!
   216     a,b,c: string
   217     f,g,h: functions (including terms of function type)
   218     i,j,m,n: int
   219     t,u: term
   220     v,w: indexnames
   221     x,y: any
   222     A,B,C: term (denoting formulae)
   223     T,U: typ
   224 *)
   225 
   226 
   227 (** Types **)
   228 
   229 (*dummies for type-inference etc.*)
   230 val dummyS = [""];
   231 val dummyT = Type ("dummy", []);
   232 
   233 fun no_dummyT typ =
   234   let
   235     fun check (T as Type ("dummy", _)) =
   236           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   237       | check (Type (_, Ts)) = List.app check Ts
   238       | check _ = ();
   239   in check typ; typ end;
   240 
   241 fun S --> T = Type("fun",[S,T]);
   242 
   243 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   244 val op ---> = Library.foldr (op -->);
   245 
   246 fun dest_Type (Type x) = x
   247   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   248 fun dest_TVar (TVar x) = x
   249   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
   250 fun dest_TFree (TFree x) = x
   251   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   252 
   253 
   254 (** Discriminators **)
   255 
   256 fun is_Bound (Bound _) = true
   257   | is_Bound _         = false;
   258 
   259 fun is_Const (Const _) = true
   260   | is_Const _ = false;
   261 
   262 fun is_Free (Free _) = true
   263   | is_Free _ = false;
   264 
   265 fun is_Var (Var _) = true
   266   | is_Var _ = false;
   267 
   268 fun is_TVar (TVar _) = true
   269   | is_TVar _ = false;
   270 
   271 
   272 (** Destructors **)
   273 
   274 fun dest_Const (Const x) =  x
   275   | dest_Const t = raise TERM("dest_Const", [t]);
   276 
   277 fun dest_Free (Free x) =  x
   278   | dest_Free t = raise TERM("dest_Free", [t]);
   279 
   280 fun dest_Var (Var x) =  x
   281   | dest_Var t = raise TERM("dest_Var", [t]);
   282 
   283 fun dest_comb (t1 $ t2) = (t1, t2)
   284   | dest_comb t = raise TERM("dest_comb", [t]);
   285 
   286 
   287 fun domain_type (Type("fun", [T,_])) = T
   288 and range_type  (Type("fun", [_,T])) = T;
   289 
   290 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   291 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   292   | binder_types _   =  [];
   293 
   294 (* maps  [T1,...,Tn]--->T  to T*)
   295 fun body_type (Type("fun",[S,T])) = body_type T
   296   | body_type T   =  T;
   297 
   298 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   299 fun strip_type T : typ list * typ =
   300   (binder_types T, body_type T);
   301 
   302 
   303 (*Compute the type of the term, checking that combinations are well-typed
   304   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   305 fun type_of1 (Ts, Const (_,T)) = T
   306   | type_of1 (Ts, Free  (_,T)) = T
   307   | type_of1 (Ts, Bound i) = (nth Ts i
   308         handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   309   | type_of1 (Ts, Var (_,T)) = T
   310   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   311   | type_of1 (Ts, f$u) =
   312       let val U = type_of1(Ts,u)
   313           and T = type_of1(Ts,f)
   314       in case T of
   315             Type("fun",[T1,T2]) =>
   316               if T1=U then T2  else raise TYPE
   317                     ("type_of: type mismatch in application", [T1,U], [f$u])
   318           | _ => raise TYPE
   319                     ("type_of: function type is expected in application",
   320                      [T,U], [f$u])
   321       end;
   322 
   323 fun type_of t : typ = type_of1 ([],t);
   324 
   325 (*Determines the type of a term, with minimal checking*)
   326 fun fastype_of1 (Ts, f$u) =
   327     (case fastype_of1 (Ts,f) of
   328         Type("fun",[_,T]) => T
   329         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   330   | fastype_of1 (_, Const (_,T)) = T
   331   | fastype_of1 (_, Free (_,T)) = T
   332   | fastype_of1 (Ts, Bound i) = (nth Ts i
   333          handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   334   | fastype_of1 (_, Var (_,T)) = T
   335   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   336 
   337 fun fastype_of t : typ = fastype_of1 ([],t);
   338 
   339 (*Determine the argument type of a function*)
   340 fun argument_type_of tm k =
   341   let
   342     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
   343       | argT _ T = raise TYPE ("argument_type_of", [T], []);
   344 
   345     fun arg 0 _ (Abs (_, T, _)) = T
   346       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
   347       | arg i Ts (t $ _) = arg (i + 1) Ts t
   348       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   349   in arg k [] tm end;
   350 
   351 
   352 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
   353 
   354 fun strip_abs (Abs (a, T, t)) =
   355       let val (a', t') = strip_abs t
   356       in ((a, T) :: a', t') end
   357   | strip_abs t = ([], t);
   358 
   359 (* maps  (x1,...,xn)t   to   t  *)
   360 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   361   | strip_abs_body u  =  u;
   362 
   363 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   364 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   365   | strip_abs_vars u  =  [] : (string*typ) list;
   366 
   367 
   368 fun strip_qnt_body qnt =
   369 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   370       | strip t = t
   371 in strip end;
   372 
   373 fun strip_qnt_vars qnt =
   374 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   375       | strip t  =  [] : (string*typ) list
   376 in strip end;
   377 
   378 
   379 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   380 val list_comb : term * term list -> term = Library.foldl (op $);
   381 
   382 
   383 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   384 fun strip_comb u : term * term list =
   385     let fun stripc (f$t, ts) = stripc (f, t::ts)
   386         |   stripc  x =  x
   387     in  stripc(u,[])  end;
   388 
   389 
   390 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   391 fun head_of (f$t) = head_of f
   392   | head_of u = u;
   393 
   394 (*number of atoms and abstractions in a term*)
   395 fun size_of_term tm =
   396   let
   397     fun add_size (t $ u) n = add_size t (add_size u n)
   398       | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
   399       | add_size _ n = n + 1;
   400   in add_size tm 0 end;
   401 
   402 (*number of atoms and constructors in a type*)
   403 fun size_of_typ ty =
   404   let
   405     fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
   406       | add_size _ n = n + 1;
   407   in add_size ty 0 end;
   408 
   409 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   410   | map_atyps f T = f T;
   411 
   412 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   413   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   414   | map_aterms f t = f t;
   415 
   416 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
   417 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
   418 
   419 fun map_types f =
   420   let
   421     fun map_aux (Const (a, T)) = Const (a, f T)
   422       | map_aux (Free (a, T)) = Free (a, f T)
   423       | map_aux (Var (v, T)) = Var (v, f T)
   424       | map_aux (t as Bound _)  = t
   425       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
   426       | map_aux (t $ u) = map_aux t $ map_aux u;
   427   in map_aux end;
   428 
   429 
   430 (* fold types and terms *)
   431 
   432 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   433   | fold_atyps f T = f T;
   434 
   435 fun fold_atyps_sorts f =
   436   fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
   437 
   438 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   439   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   440   | fold_aterms f a = f a;
   441 
   442 fun fold_term_types f (t as Const (_, T)) = f t T
   443   | fold_term_types f (t as Free (_, T)) = f t T
   444   | fold_term_types f (t as Var (_, T)) = f t T
   445   | fold_term_types f (Bound _) = I
   446   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   447   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   448 
   449 fun fold_types f = fold_term_types (K f);
   450 
   451 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
   452   | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
   453   | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
   454   | replace_types (Bound i) Ts = (Bound i, Ts)
   455   | replace_types (Abs (x, _, b)) (T :: Ts) =
   456       let val (b', Ts') = replace_types b Ts
   457       in (Abs (x, T, b'), Ts') end
   458   | replace_types (t $ u) Ts =
   459       let
   460         val (t', Ts') = replace_types t Ts;
   461         val (u', Ts'') = replace_types u Ts';
   462       in (t' $ u', Ts'') end;
   463 
   464 fun burrow_types f ts =
   465   let
   466     val Ts = rev (fold (fold_types cons) ts []);
   467     val Ts' = f Ts;
   468     val (ts', []) = fold_map replace_types ts Ts';
   469   in ts' end;
   470 
   471 (*collect variables*)
   472 val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
   473 val add_tvar_names = fold_types add_tvar_namesT;
   474 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   475 val add_tvars = fold_types add_tvarsT;
   476 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   477 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   478 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
   479 val add_tfree_names = fold_types add_tfree_namesT;
   480 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   481 val add_tfrees = fold_types add_tfreesT;
   482 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
   483 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   484 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
   485 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
   486 
   487 (*extra type variables in a term, not covered by its type*)
   488 fun hidden_polymorphism t =
   489   let
   490     val T = fastype_of t;
   491     val tvarsT = add_tvarsT T [];
   492     val extra_tvars = fold_types (fold_atyps
   493       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   494   in extra_tvars end;
   495 
   496 
   497 (* renaming variables *)
   498 
   499 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   500 
   501 fun declare_term_names tm =
   502   fold_aterms
   503     (fn Const (a, _) => Name.declare (Long_Name.base_name a)
   504       | Free (a, _) => Name.declare a
   505       | _ => I) tm #>
   506   fold_types declare_typ_names tm;
   507 
   508 val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
   509 
   510 fun variant_frees t frees =
   511   fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
   512 
   513 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   514 
   515 
   516 
   517 (** Comparing terms **)
   518 
   519 (* variables *)
   520 
   521 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   522 
   523 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   524 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   525 
   526 
   527 (* alpha equivalence *)
   528 
   529 fun tm1 aconv tm2 =
   530   pointer_eq (tm1, tm2) orelse
   531     (case (tm1, tm2) of
   532       (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
   533     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
   534     | (a1, a2) => a1 = a2);
   535 
   536 fun aconv_untyped (tm1, tm2) =
   537   pointer_eq (tm1, tm2) orelse
   538     (case (tm1, tm2) of
   539       (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
   540     | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
   541     | (Const (a, _), Const (b, _)) => a = b
   542     | (Free (x, _), Free (y, _)) => x = y
   543     | (Var (xi, _), Var (yj, _)) => xi = yj
   544     | (Bound i, Bound j) => i = j
   545     | _ => false);
   546 
   547 
   548 (*A fast unification filter: true unless the two terms cannot be unified.
   549   Terms must be NORMAL.  Treats all Vars as distinct. *)
   550 fun could_unify (t, u) =
   551   let
   552     fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
   553       | matchrands _ _ = true;
   554   in
   555     case (head_of t, head_of u) of
   556       (_, Var _) => true
   557     | (Var _, _) => true
   558     | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
   559     | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
   560     | (Bound i, Bound j) => i = j andalso matchrands t u
   561     | (Abs _, _) => true   (*because of possible eta equality*)
   562     | (_, Abs _) => true
   563     | _ => false
   564   end;
   565 
   566 
   567 
   568 (** Connectives of higher order logic **)
   569 
   570 fun aT S = TFree (Name.aT, S);
   571 
   572 fun itselfT ty = Type ("itself", [ty]);
   573 val a_itselfT = itselfT (TFree (Name.aT, []));
   574 
   575 val propT : typ = Type("prop",[]);
   576 
   577 fun all T = Const("all", (T-->propT)-->propT);
   578 
   579 (* maps  !!x1...xn. t   to   t  *)
   580 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   581   | strip_all_body t  =  t;
   582 
   583 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   584 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   585                 (a,T) :: strip_all_vars t
   586   | strip_all_vars t  =  [] : (string*typ) list;
   587 
   588 (*increments a term's non-local bound variables
   589   required when moving a term within abstractions
   590      inc is  increment for bound variables
   591      lev is  level at which a bound variable is considered 'loose'*)
   592 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   593   | incr_bv (inc, lev, Abs(a,T,body)) =
   594         Abs(a, T, incr_bv(inc,lev+1,body))
   595   | incr_bv (inc, lev, f$t) =
   596       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   597   | incr_bv (inc, lev, u) = u;
   598 
   599 fun incr_boundvars  0  t = t
   600   | incr_boundvars inc t = incr_bv(inc,0,t);
   601 
   602 (*Scan a pair of terms; while they are similar,
   603   accumulate corresponding bound vars in "al"*)
   604 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   605       match_bvs(s, t, if x="" orelse y="" then al
   606                                           else (x,y)::al)
   607   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   608   | match_bvs(_,_,al) = al;
   609 
   610 (* strip abstractions created by parameters *)
   611 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   612 
   613 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   614   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
   615   | map_abs_vars f t = t;
   616 
   617 fun rename_abs pat obj t =
   618   let
   619     val ren = match_bvs (pat, obj, []);
   620     fun ren_abs (Abs (x, T, b)) =
   621           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   622       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   623       | ren_abs t = t
   624   in if null ren then NONE else SOME (ren_abs t) end;
   625 
   626 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   627    (Bound 0) is loose at level 0 *)
   628 fun add_loose_bnos (Bound i, lev, js) =
   629         if i<lev then js else insert (op =) (i - lev) js
   630   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   631   | add_loose_bnos (f$t, lev, js) =
   632         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   633   | add_loose_bnos (_, _, js) = js;
   634 
   635 fun loose_bnos t = add_loose_bnos (t, 0, []);
   636 
   637 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   638    level k or beyond. *)
   639 fun loose_bvar(Bound i,k) = i >= k
   640   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   641   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   642   | loose_bvar _ = false;
   643 
   644 fun loose_bvar1(Bound i,k) = i = k
   645   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   646   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   647   | loose_bvar1 _ = false;
   648 
   649 (*Substitute arguments for loose bound variables.
   650   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   651   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   652         and the appropriate call is  subst_bounds([b,a], c) .
   653   Loose bound variables >=n are reduced by "n" to
   654      compensate for the disappearance of lambdas.
   655 *)
   656 fun subst_bounds (args: term list, t) : term =
   657   let
   658     val n = length args;
   659     fun subst (t as Bound i, lev) =
   660          (if i < lev then raise Same.SAME   (*var is locally bound*)
   661           else incr_boundvars lev (nth args (i - lev))
   662             handle Subscript => Bound (i - n))  (*loose: change it*)
   663       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   664       | subst (f $ t, lev) =
   665           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   666             handle Same.SAME => f $ subst (t, lev))
   667       | subst _ = raise Same.SAME;
   668   in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
   669 
   670 (*Special case: one argument*)
   671 fun subst_bound (arg, t) : term =
   672   let
   673     fun subst (Bound i, lev) =
   674           if i < lev then raise Same.SAME   (*var is locally bound*)
   675           else if i = lev then incr_boundvars lev arg
   676           else Bound (i - 1)   (*loose: change it*)
   677       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   678       | subst (f $ t, lev) =
   679           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   680             handle Same.SAME => f $ subst (t, lev))
   681       | subst _ = raise Same.SAME;
   682   in subst (t, 0) handle Same.SAME => t end;
   683 
   684 (*beta-reduce if possible, else form application*)
   685 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   686   | betapply (f,u) = f$u;
   687 
   688 val betapplys = Library.foldl betapply;
   689 
   690 
   691 (*unfolding abstractions with substitution
   692   of bound variables and implicit eta-expansion*)
   693 fun strip_abs_eta k t =
   694   let
   695     val used = fold_aterms declare_term_frees t Name.context;
   696     fun strip_abs t (0, used) = (([], t), (0, used))
   697       | strip_abs (Abs (v, T, t)) (k, used) =
   698           let
   699             val ([v'], used') = Name.variants [v] used;
   700             val t' = subst_bound (Free (v', T), t);
   701             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   702           in (((v', T) :: vs, t''), (k', used'')) end
   703       | strip_abs t (k, used) = (([], t), (k, used));
   704     fun expand_eta [] t _ = ([], t)
   705       | expand_eta (T::Ts) t used =
   706           let
   707             val ([v], used') = Name.variants [""] used;
   708             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   709           in ((v, T) :: vs, t') end;
   710     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   711     val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
   712     val (vs2, t'') = expand_eta Ts t' used';
   713   in (vs1 @ vs2, t'') end;
   714 
   715 
   716 (*Substitute new for free occurrences of old in a term*)
   717 fun subst_free [] = I
   718   | subst_free pairs =
   719       let fun substf u =
   720             case AList.lookup (op aconv) pairs u of
   721                 SOME u' => u'
   722               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   723                                  | t$u' => substf t $ substf u'
   724                                  | _ => u)
   725       in  substf  end;
   726 
   727 (*Abstraction of the term "body" over its occurrences of v,
   728     which must contain no loose bound variables.
   729   The resulting term is ready to become the body of an Abs.*)
   730 fun abstract_over (v, body) =
   731   let
   732     fun abs lev tm =
   733       if v aconv tm then Bound lev
   734       else
   735         (case tm of
   736           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   737         | t $ u =>
   738             (abs lev t $ (abs lev u handle Same.SAME => u)
   739               handle Same.SAME => t $ abs lev u)
   740         | _ => raise Same.SAME);
   741   in abs 0 body handle Same.SAME => body end;
   742 
   743 fun term_name (Const (x, _)) = Long_Name.base_name x
   744   | term_name (Free (x, _)) = x
   745   | term_name (Var ((x, _), _)) = x
   746   | term_name _ = Name.uu;
   747 
   748 fun lambda_name (x, v) t =
   749   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
   750 
   751 fun lambda v t = lambda_name ("", v) t;
   752 
   753 (*Form an abstraction over a free variable.*)
   754 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
   755 fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
   756 
   757 (*Abstraction over a list of free variables*)
   758 fun list_abs_free ([ ] ,     t) = t
   759   | list_abs_free ((a,T)::vars, t) =
   760       absfree(a, T, list_abs_free(vars,t));
   761 
   762 (*Quantification over a list of free variables*)
   763 fun list_all_free ([], t: term) = t
   764   | list_all_free ((a,T)::vars, t) =
   765         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   766 
   767 (*Quantification over a list of variables (already bound in body) *)
   768 fun list_all ([], t) = t
   769   | list_all ((a,T)::vars, t) =
   770         (all T) $ (Abs(a, T, list_all(vars,t)));
   771 
   772 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   773   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   774 fun subst_atomic [] tm = tm
   775   | subst_atomic inst tm =
   776       let
   777         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   778           | subst (t $ u) = subst t $ subst u
   779           | subst t = the_default t (AList.lookup (op aconv) inst t);
   780       in subst tm end;
   781 
   782 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   783 fun typ_subst_atomic [] ty = ty
   784   | typ_subst_atomic inst ty =
   785       let
   786         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   787           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
   788       in subst ty end;
   789 
   790 fun subst_atomic_types [] tm = tm
   791   | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
   792 
   793 fun typ_subst_TVars [] ty = ty
   794   | typ_subst_TVars inst ty =
   795       let
   796         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   797           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
   798           | subst T = T;
   799       in subst ty end;
   800 
   801 fun subst_TVars [] tm = tm
   802   | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
   803 
   804 fun subst_Vars [] tm = tm
   805   | subst_Vars inst tm =
   806       let
   807         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
   808           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   809           | subst (t $ u) = subst t $ subst u
   810           | subst t = t;
   811       in subst tm end;
   812 
   813 fun subst_vars ([], []) tm = tm
   814   | subst_vars ([], inst) tm = subst_Vars inst tm
   815   | subst_vars (instT, inst) tm =
   816       let
   817         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   818           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   819           | subst (Var (xi, T)) =
   820               (case AList.lookup (op =) inst xi of
   821                 NONE => Var (xi, typ_subst_TVars instT T)
   822               | SOME t => t)
   823           | subst (t as Bound _) = t
   824           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   825           | subst (t $ u) = subst t $ subst u;
   826       in subst tm end;
   827 
   828 fun close_schematic_term t =
   829   let
   830     val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
   831     val extra_terms = map Var (add_vars t []);
   832   in fold lambda (extra_terms @ extra_types) t end;
   833 
   834 
   835 
   836 (** Identifying first-order terms **)
   837 
   838 (*Differs from proofterm/is_fun in its treatment of TVar*)
   839 fun is_funtype (Type ("fun", [_, _])) = true
   840   | is_funtype _ = false;
   841 
   842 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
   843 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t)));
   844 
   845 (*First order means in all terms of the form f(t1,...,tn) no argument has a
   846   function type. The supplied quantifiers are excluded: their argument always
   847   has a function type through a recursive call into its body.*)
   848 fun is_first_order quants =
   849   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   850         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
   851             member (op =) quants q  andalso   (*it is a known quantifier*)
   852             not (is_funtype T)   andalso first_order1 (T::Ts) body
   853         | first_order1 Ts t =
   854             case strip_comb t of
   855                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   856                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   857                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   858                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   859                | (Abs _, ts) => false (*not in beta-normal form*)
   860                | _ => error "first_order: unexpected case"
   861     in  first_order1 []  end;
   862 
   863 
   864 (* maximum index of typs and terms *)
   865 
   866 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
   867   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
   868   | maxidx_typ (TFree _) i = i
   869 and maxidx_typs [] i = i
   870   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
   871 
   872 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
   873   | maxidx_term (Const (_, T)) i = maxidx_typ T i
   874   | maxidx_term (Free (_, T)) i = maxidx_typ T i
   875   | maxidx_term (Bound _) i = i
   876   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
   877   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
   878 
   879 fun maxidx_of_typ T = maxidx_typ T ~1;
   880 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
   881 fun maxidx_of_term t = maxidx_term t ~1;
   882 
   883 
   884 
   885 (** misc syntax operations **)
   886 
   887 (* substructure *)
   888 
   889 fun exists_subtype P =
   890   let
   891     fun ex ty = P ty orelse
   892       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   893   in ex end;
   894 
   895 fun exists_type P =
   896   let
   897     fun ex (Const (_, T)) = P T
   898       | ex (Free (_, T)) = P T
   899       | ex (Var (_, T)) = P T
   900       | ex (Bound _) = false
   901       | ex (Abs (_, T, t)) = P T orelse ex t
   902       | ex (t $ u) = ex t orelse ex u;
   903   in ex end;
   904 
   905 fun exists_subterm P =
   906   let
   907     fun ex tm = P tm orelse
   908       (case tm of
   909         t $ u => ex t orelse ex u
   910       | Abs (_, _, t) => ex t
   911       | _ => false);
   912   in ex end;
   913 
   914 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   915 
   916 fun has_abs (Abs _) = true
   917   | has_abs (t $ u) = has_abs t orelse has_abs u
   918   | has_abs _ = false;
   919 
   920 
   921 (* dest abstraction *)
   922 
   923 fun dest_abs (x, T, body) =
   924   let
   925     fun name_clash (Free (y, _)) = (x = y)
   926       | name_clash (t $ u) = name_clash t orelse name_clash u
   927       | name_clash (Abs (_, _, t)) = name_clash t
   928       | name_clash _ = false;
   929   in
   930     if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
   931     else (x, subst_bound (Free (x, T), body))
   932   end;
   933 
   934 
   935 (* dummy patterns *)
   936 
   937 val dummy_patternN = "dummy_pattern";
   938 
   939 fun dummy_pattern T = Const (dummy_patternN, T);
   940 
   941 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
   942   | is_dummy_pattern _ = false;
   943 
   944 fun no_dummy_patterns tm =
   945   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   946   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
   947 
   948 fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
   949       let val [x] = Name.invents used Name.uu 1
   950       in (Free (Name.internal x, T), Name.declare x used) end
   951   | free_dummy_patterns (Abs (x, T, b)) used =
   952       let val (b', used') = free_dummy_patterns b used
   953       in (Abs (x, T, b'), used') end
   954   | free_dummy_patterns (t $ u) used =
   955       let
   956         val (t', used') = free_dummy_patterns t used;
   957         val (u', used'') = free_dummy_patterns u used';
   958       in (t' $ u', used'') end
   959   | free_dummy_patterns a used = (a, used);
   960 
   961 fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
   962       (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   963   | replace_dummy Ts (Abs (x, T, t)) i =
   964       let val (t', i') = replace_dummy (T :: Ts) t i
   965       in (Abs (x, T, t'), i') end
   966   | replace_dummy Ts (t $ u) i =
   967       let
   968         val (t', i') = replace_dummy Ts t i;
   969         val (u', i'') = replace_dummy Ts u i';
   970       in (t' $ u', i'') end
   971   | replace_dummy _ a i = (a, i);
   972 
   973 val replace_dummy_patterns = replace_dummy [];
   974 
   975 fun is_replaced_dummy_pattern ("_dummy_", _) = true
   976   | is_replaced_dummy_pattern _ = false;
   977 
   978 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
   979   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
   980   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
   981   | show_dummy_patterns a = a;
   982 
   983 
   984 (* display variables *)
   985 
   986 val show_question_marks = Unsynchronized.ref true;
   987 
   988 fun string_of_vname (x, i) =
   989   let
   990     val question_mark = if ! show_question_marks then "?" else "";
   991     val idx = string_of_int i;
   992     val dot =
   993       (case rev (Symbol.explode x) of
   994         _ :: "\\<^isub>" :: _ => false
   995       | _ :: "\\<^isup>" :: _ => false
   996       | c :: _ => Symbol.is_digit c
   997       | _ => true);
   998   in
   999     if dot then question_mark ^ x ^ "." ^ idx
  1000     else if i <> 0 then question_mark ^ x ^ idx
  1001     else question_mark ^ x
  1002   end;
  1003 
  1004 fun string_of_vname' (x, ~1) = x
  1005   | string_of_vname' xi = string_of_vname xi;
  1006 
  1007 end;
  1008 
  1009 structure BasicTerm: BASIC_TERM = Term;
  1010 open BasicTerm;