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