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