TFL/usyntax.sml
author nipkow
Fri Oct 09 14:19:13 1998 +0200 (1998-10-09)
changeset 5633 fb7fa1b154c4
parent 3713 8a1f7d5b1eff
child 6498 1ebbe18fe236
permissions -rw-r--r--
Added a few breaks in error text.
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
structure USyntax : USyntax_sig =
paulson@2112
    10
struct
paulson@2112
    11
paulson@2112
    12
structure Utils = Utils;
paulson@2112
    13
open Utils;
paulson@2112
    14
paulson@2112
    15
infix 4 ##;
paulson@2112
    16
paulson@3353
    17
fun USYN_ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
paulson@2112
    18
paulson@2112
    19
paulson@2112
    20
(*---------------------------------------------------------------------------
paulson@2112
    21
 *
paulson@2112
    22
 *                            Types 
paulson@2112
    23
 *
paulson@2112
    24
 *---------------------------------------------------------------------------*)
paulson@2112
    25
val mk_prim_vartype = TVar;
paulson@2112
    26
fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
paulson@2112
    27
paulson@2112
    28
(* But internally, it's useful *)
paulson@2112
    29
fun dest_vtype (TVar x) = x
paulson@3353
    30
  | dest_vtype _ = raise USYN_ERR{func = "dest_vtype", 
paulson@2112
    31
                             mesg = "not a flexible type variable"};
paulson@2112
    32
paulson@2112
    33
val is_vartype = Utils.can dest_vtype;
paulson@2112
    34
paulson@2112
    35
val type_vars  = map mk_prim_vartype o typ_tvars
paulson@3391
    36
fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
paulson@2112
    37
paulson@2112
    38
val alpha  = mk_vartype "'a"
paulson@2112
    39
val beta   = mk_vartype "'b"
paulson@2112
    40
paulson@3245
    41
fun strip_prod_type (Type("*", [ty1,ty2])) =
paulson@3245
    42
	strip_prod_type ty1 @ strip_prod_type ty2
paulson@3245
    43
  | strip_prod_type ty = [ty];
paulson@2112
    44
paulson@2112
    45
paulson@2112
    46
paulson@2112
    47
(*---------------------------------------------------------------------------
paulson@2112
    48
 *
paulson@2112
    49
 *                              Terms 
paulson@2112
    50
 *
paulson@2112
    51
 *---------------------------------------------------------------------------*)
paulson@2112
    52
paulson@2112
    53
(* Free variables, in order of occurrence, from left to right in the 
paulson@2112
    54
 * syntax tree. *)
paulson@2112
    55
fun free_vars_lr tm = 
paulson@2112
    56
  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
paulson@2112
    57
      fun add (t, frees) = case t of
paulson@2112
    58
            Free   _ => if (memb t frees) then frees else t::frees
paulson@2112
    59
          | Abs (_,_,body) => add(body,frees)
paulson@2112
    60
          | f$t =>  add(t, add(f, frees))
paulson@2112
    61
          | _ => frees
paulson@2112
    62
  in rev(add(tm,[]))
paulson@2112
    63
  end;
paulson@2112
    64
paulson@2112
    65
paulson@2112
    66
paulson@2112
    67
val type_vars_in_term = map mk_prim_vartype o term_tvars;
paulson@2112
    68
paulson@2112
    69
paulson@2112
    70
paulson@2112
    71
(* Prelogic *)
paulson@3353
    72
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
paulson@2112
    73
fun inst theta = subst_vars (map dest_tybinding theta,[])
paulson@2112
    74
paulson@2112
    75
paulson@2112
    76
(* Construction routines *)
paulson@2112
    77
paulson@2112
    78
fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
paulson@2112
    79
  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
paulson@3353
    80
  | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
paulson@2112
    81
paulson@2112
    82
paulson@2112
    83
fun mk_imp{ant,conseq} = 
paulson@3391
    84
   let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
paulson@3245
    85
   in list_comb(c,[ant,conseq])
paulson@2112
    86
   end;
paulson@2112
    87
paulson@2112
    88
fun mk_select (r as {Bvar,Body}) = 
paulson@2112
    89
  let val ty = type_of Bvar
paulson@3391
    90
      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
paulson@3245
    91
  in list_comb(c,[mk_abs r])
paulson@2112
    92
  end;
paulson@2112
    93
paulson@2112
    94
fun mk_forall (r as {Bvar,Body}) = 
paulson@2112
    95
  let val ty = type_of Bvar
paulson@3391
    96
      val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
paulson@3245
    97
  in list_comb(c,[mk_abs r])
paulson@2112
    98
  end;
paulson@2112
    99
paulson@2112
   100
fun mk_exists (r as {Bvar,Body}) = 
paulson@2112
   101
  let val ty = type_of Bvar 
paulson@3391
   102
      val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
paulson@3245
   103
  in list_comb(c,[mk_abs r])
paulson@2112
   104
  end;
paulson@2112
   105
paulson@2112
   106
paulson@2112
   107
fun mk_conj{conj1,conj2} =
paulson@3391
   108
   let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
paulson@3245
   109
   in list_comb(c,[conj1,conj2])
paulson@2112
   110
   end;
paulson@2112
   111
paulson@2112
   112
fun mk_disj{disj1,disj2} =
paulson@3391
   113
   let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
paulson@3245
   114
   in list_comb(c,[disj1,disj2])
paulson@2112
   115
   end;
paulson@2112
   116
paulson@3245
   117
fun prod_ty ty1 ty2 = Type("*", [ty1,ty2]);
paulson@2112
   118
paulson@2112
   119
local
paulson@2112
   120
fun mk_uncurry(xt,yt,zt) =
paulson@3391
   121
    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
paulson@2112
   122
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
paulson@3353
   123
  | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}
paulson@2112
   124
fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
paulson@2112
   125
in
paulson@2112
   126
fun mk_pabs{varstruct,body} = 
paulson@2112
   127
 let fun mpa(varstruct,body) =
paulson@2112
   128
       if (is_var varstruct)
paulson@2112
   129
       then mk_abs{Bvar = varstruct, Body = body}
paulson@2112
   130
       else let val {fst,snd} = dest_pair varstruct
paulson@3405
   131
            in mk_uncurry(type_of fst,type_of snd,type_of body) $
paulson@3405
   132
	       mpa(fst,mpa(snd,body))
paulson@2112
   133
            end
paulson@2112
   134
 in mpa(varstruct,body)
paulson@2112
   135
 end
paulson@3353
   136
 handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""};
paulson@2112
   137
end;
paulson@2112
   138
paulson@2112
   139
(* Destruction routines *)
paulson@2112
   140
paulson@3245
   141
datatype lambda = VAR   of {Name : string, Ty : typ}
paulson@3245
   142
                | CONST of {Name : string, Ty : typ}
paulson@3245
   143
                | COMB  of {Rator: term, Rand : term}
paulson@3245
   144
                | LAMB  of {Bvar : term, Body : term};
paulson@2112
   145
paulson@2112
   146
paulson@2112
   147
fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
paulson@2112
   148
  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
paulson@2112
   149
  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
paulson@2112
   150
  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
paulson@3391
   151
  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
paulson@2112
   152
                               in LAMB{Bvar = v, Body = betapply (M,v)}
paulson@2112
   153
                               end
paulson@3353
   154
  | dest_term(Bound _)       = raise USYN_ERR{func = "dest_term",mesg = "Bound"};
paulson@2112
   155
paulson@2112
   156
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
paulson@3353
   157
  | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"};
paulson@2112
   158
paulson@2112
   159
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
paulson@3353
   160
  | dest_comb _ =  raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
paulson@2112
   161
paulson@2112
   162
fun dest_abs(a as Abs(s,ty,M)) = 
paulson@3391
   163
     let val v = Free(s,ty)
paulson@2112
   164
     in {Bvar = v, Body = betapply (a,v)}
paulson@2112
   165
     end
paulson@3353
   166
  | dest_abs _ =  raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
paulson@2112
   167
paulson@2112
   168
fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
paulson@3353
   169
  | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
paulson@2112
   170
paulson@2112
   171
fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
paulson@3353
   172
  | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
paulson@2112
   173
paulson@2112
   174
fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
paulson@3353
   175
  | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
paulson@2112
   176
paulson@2112
   177
fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
paulson@3353
   178
  | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
paulson@2112
   179
paulson@2112
   180
fun dest_neg(Const("not",_) $ M) = M
paulson@3353
   181
  | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"};
paulson@2112
   182
paulson@2112
   183
fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
paulson@3353
   184
  | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"};
paulson@2112
   185
paulson@2112
   186
fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
paulson@3353
   187
  | dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"};
paulson@2112
   188
paulson@2112
   189
fun mk_pair{fst,snd} = 
paulson@2112
   190
   let val ty1 = type_of fst
paulson@2112
   191
       val ty2 = type_of snd
paulson@3391
   192
       val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
paulson@3245
   193
   in list_comb(c,[fst,snd])
paulson@2112
   194
   end;
paulson@2112
   195
paulson@2112
   196
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
paulson@3353
   197
  | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"};
paulson@2112
   198
paulson@2112
   199
paulson@3245
   200
local  fun ucheck t = (if #Name(dest_const t) = "split" then t
paulson@3245
   201
                       else raise Match)
paulson@2112
   202
in
paulson@2112
   203
fun dest_pabs tm =
paulson@2112
   204
   let val {Bvar,Body} = dest_abs tm
paulson@2112
   205
   in {varstruct = Bvar, body = Body}
paulson@3245
   206
   end 
paulson@3245
   207
    handle 
paulson@3245
   208
     _ => let val {Rator,Rand} = dest_comb tm
paulson@3245
   209
              val _ = ucheck Rator
paulson@3245
   210
              val {varstruct = lv,body} = dest_pabs Rand
paulson@3245
   211
              val {varstruct = rv,body} = dest_pabs body
paulson@3245
   212
          in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
paulson@3245
   213
          end
paulson@2112
   214
end;
paulson@2112
   215
paulson@2112
   216
paulson@2112
   217
(* Garbage - ought to be dropped *)
paulson@2112
   218
val lhs   = #lhs o dest_eq
paulson@2112
   219
val rhs   = #rhs o dest_eq
paulson@2112
   220
val rand  = #Rand o dest_comb
paulson@2112
   221
  
paulson@2112
   222
paulson@2112
   223
(* Query routines *)
paulson@2112
   224
val is_imp    = can dest_imp
paulson@2112
   225
val is_forall = can dest_forall
paulson@2112
   226
val is_exists = can dest_exists
paulson@2112
   227
val is_neg    = can dest_neg
paulson@2112
   228
val is_conj   = can dest_conj
paulson@2112
   229
val is_disj   = can dest_disj
paulson@2112
   230
val is_pair   = can dest_pair
paulson@2112
   231
val is_pabs   = can dest_pabs
paulson@2112
   232
paulson@2112
   233
paulson@3245
   234
(* Construction of a cterm from a list of Terms *)
paulson@2112
   235
paulson@2112
   236
fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
paulson@2112
   237
paulson@2112
   238
(* These others are almost never used *)
paulson@2112
   239
fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
paulson@2112
   240
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
paulson@2112
   241
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
paulson@2112
   242
paulson@2112
   243
paulson@2112
   244
(* Need to reverse? *)
paulson@3391
   245
fun gen_all tm = list_mk_forall(term_frees tm, tm);
paulson@2112
   246
paulson@3245
   247
(* Destructing a cterm to a list of Terms *)
paulson@2112
   248
fun strip_comb tm = 
paulson@2112
   249
   let fun dest(M$N, A) = dest(M, N::A)
paulson@2112
   250
         | dest x = x
paulson@2112
   251
   in dest(tm,[])
paulson@2112
   252
   end;
paulson@2112
   253
paulson@2112
   254
fun strip_abs(tm as Abs _) =
paulson@2112
   255
       let val {Bvar,Body} = dest_abs tm
paulson@2112
   256
           val (bvs, core) = strip_abs Body
paulson@2112
   257
       in (Bvar::bvs, core)
paulson@2112
   258
       end
paulson@2112
   259
  | strip_abs M = ([],M);
paulson@2112
   260
paulson@2112
   261
paulson@2112
   262
fun strip_imp fm =
paulson@2112
   263
   if (is_imp fm)
paulson@2112
   264
   then let val {ant,conseq} = dest_imp fm
paulson@3245
   265
            val (was,wb) = strip_imp conseq
paulson@2112
   266
        in ((ant::was), wb)
paulson@2112
   267
        end
paulson@2112
   268
   else ([],fm);
paulson@2112
   269
paulson@2112
   270
fun strip_forall fm =
paulson@2112
   271
   if (is_forall fm)
paulson@2112
   272
   then let val {Bvar,Body} = dest_forall fm
paulson@2112
   273
            val (bvs,core) = strip_forall Body
paulson@2112
   274
        in ((Bvar::bvs), core)
paulson@2112
   275
        end
paulson@2112
   276
   else ([],fm);
paulson@2112
   277
paulson@2112
   278
paulson@2112
   279
fun strip_exists fm =
paulson@2112
   280
   if (is_exists fm)
paulson@2112
   281
   then let val {Bvar, Body} = dest_exists fm 
paulson@2112
   282
            val (bvs,core) = strip_exists Body
paulson@2112
   283
        in (Bvar::bvs, core)
paulson@2112
   284
        end
paulson@2112
   285
   else ([],fm);
paulson@2112
   286
paulson@2112
   287
fun strip_disj w =
paulson@2112
   288
   if (is_disj w)
paulson@2112
   289
   then let val {disj1,disj2} = dest_disj w 
paulson@2112
   290
        in (strip_disj disj1@strip_disj disj2)
paulson@2112
   291
        end
paulson@2112
   292
   else [w];
paulson@2112
   293
paulson@2112
   294
paulson@2112
   295
(* Miscellaneous *)
paulson@2112
   296
paulson@2112
   297
fun mk_vstruct ty V =
paulson@3245
   298
  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
paulson@3245
   299
	      let val (ltm,vs1) = follow_prod_type ty1 vs
paulson@3245
   300
		  val (rtm,vs2) = follow_prod_type ty2 vs1
paulson@3245
   301
	      in (mk_pair{fst=ltm, snd=rtm}, vs2) end
paulson@3245
   302
	| follow_prod_type _ (v::vs) = (v,vs)
paulson@3245
   303
  in #1 (follow_prod_type ty V)  end;
paulson@2112
   304
paulson@2112
   305
paulson@2112
   306
(* Search a term for a sub-term satisfying the predicate p. *)
paulson@2112
   307
fun find_term p =
paulson@2112
   308
   let fun find tm =
paulson@3405
   309
      if (p tm) then Some tm 
paulson@3405
   310
      else case tm of
paulson@3405
   311
	  Abs(_,_,body) => find body
paulson@3405
   312
	| (t$u)         => (Some (the (find t)) handle _ => find u)
paulson@3405
   313
	| _             => None
paulson@2112
   314
   in find
paulson@2112
   315
   end;
paulson@2112
   316
paulson@2112
   317
fun dest_relation tm =
paulson@3245
   318
   if (type_of tm = HOLogic.boolT)
paulson@2112
   319
   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
paulson@2112
   320
        in (R,y,x)
paulson@3353
   321
        end handle _ => raise USYN_ERR{func="dest_relation",
paulson@2112
   322
                                  mesg="unexpected term structure"}
paulson@3353
   323
   else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
paulson@2112
   324
paulson@3405
   325
fun is_WFR (Const("wf",_)$_) = true
paulson@3405
   326
  | is_WFR _                 = false;
paulson@2112
   327
paulson@3391
   328
fun ARB ty = mk_select{Bvar=Free("v",ty),
paulson@3391
   329
                       Body=Const("True",HOLogic.boolT)};
paulson@2112
   330
paulson@2112
   331
end; (* Syntax *)