TFL/usyntax.ML
changeset 10769 70b9b0cfe05f
child 12340 24d31d47af1a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/usyntax.ML	Wed Jan 03 21:20:40 2001 +0100
     1.3 @@ -0,0 +1,409 @@
     1.4 +(*  Title:      TFL/usyntax.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +
     1.9 +Emulation of HOL's abstract syntax functions.
    1.10 +*)
    1.11 +
    1.12 +signature USYNTAX =
    1.13 +sig
    1.14 +  datatype lambda = VAR   of {Name : string, Ty : typ}
    1.15 +                  | CONST of {Name : string, Ty : typ}
    1.16 +                  | COMB  of {Rator: term, Rand : term}
    1.17 +                  | LAMB  of {Bvar : term, Body : term}
    1.18 +
    1.19 +  val alpha : typ
    1.20 +
    1.21 +  (* Types *)
    1.22 +  val type_vars  : typ -> typ list
    1.23 +  val type_varsl : typ list -> typ list
    1.24 +  val mk_vartype : string -> typ
    1.25 +  val is_vartype : typ -> bool
    1.26 +  val strip_prod_type : typ -> typ list
    1.27 +
    1.28 +  (* Terms *)
    1.29 +  val free_vars_lr : term -> term list
    1.30 +  val type_vars_in_term : term -> typ list
    1.31 +  val dest_term  : term -> lambda
    1.32 +
    1.33 +  (* Prelogic *)
    1.34 +  val inst      : (typ*typ) list -> term -> term
    1.35 +
    1.36 +  (* Construction routines *)
    1.37 +  val mk_abs    :{Bvar  : term, Body : term} -> term
    1.38 +
    1.39 +  val mk_imp    :{ant : term, conseq :  term} -> term
    1.40 +  val mk_select :{Bvar : term, Body : term} -> term
    1.41 +  val mk_forall :{Bvar : term, Body : term} -> term
    1.42 +  val mk_exists :{Bvar : term, Body : term} -> term
    1.43 +  val mk_conj   :{conj1 : term, conj2 : term} -> term
    1.44 +  val mk_disj   :{disj1 : term, disj2 : term} -> term
    1.45 +  val mk_pabs   :{varstruct : term, body : term} -> term
    1.46 +
    1.47 +  (* Destruction routines *)
    1.48 +  val dest_const: term -> {Name : string, Ty : typ}
    1.49 +  val dest_comb : term -> {Rator : term, Rand : term}
    1.50 +  val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
    1.51 +  val dest_eq     : term -> {lhs : term, rhs : term}
    1.52 +  val dest_imp    : term -> {ant : term, conseq : term}
    1.53 +  val dest_forall : term -> {Bvar : term, Body : term}
    1.54 +  val dest_exists : term -> {Bvar : term, Body : term}
    1.55 +  val dest_neg    : term -> term
    1.56 +  val dest_conj   : term -> {conj1 : term, conj2 : term}
    1.57 +  val dest_disj   : term -> {disj1 : term, disj2 : term}
    1.58 +  val dest_pair   : term -> {fst : term, snd : term}
    1.59 +  val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
    1.60 +
    1.61 +  val lhs   : term -> term
    1.62 +  val rhs   : term -> term
    1.63 +  val rand  : term -> term
    1.64 +
    1.65 +  (* Query routines *)
    1.66 +  val is_imp    : term -> bool
    1.67 +  val is_forall : term -> bool
    1.68 +  val is_exists : term -> bool
    1.69 +  val is_neg    : term -> bool
    1.70 +  val is_conj   : term -> bool
    1.71 +  val is_disj   : term -> bool
    1.72 +  val is_pair   : term -> bool
    1.73 +  val is_pabs   : term -> bool
    1.74 +
    1.75 +  (* Construction of a term from a list of Preterms *)
    1.76 +  val list_mk_abs    : (term list * term) -> term
    1.77 +  val list_mk_imp    : (term list * term) -> term
    1.78 +  val list_mk_forall : (term list * term) -> term
    1.79 +  val list_mk_conj   : term list -> term
    1.80 +
    1.81 +  (* Destructing a term to a list of Preterms *)
    1.82 +  val strip_comb     : term -> (term * term list)
    1.83 +  val strip_abs      : term -> (term list * term)
    1.84 +  val strip_imp      : term -> (term list * term)
    1.85 +  val strip_forall   : term -> (term list * term)
    1.86 +  val strip_exists   : term -> (term list * term)
    1.87 +  val strip_disj     : term -> term list
    1.88 +
    1.89 +  (* Miscellaneous *)
    1.90 +  val mk_vstruct : typ -> term list -> term
    1.91 +  val gen_all    : term -> term
    1.92 +  val find_term  : (term -> bool) -> term -> term option
    1.93 +  val dest_relation : term -> term * term * term
    1.94 +  val is_WFR : term -> bool
    1.95 +  val ARB : typ -> term
    1.96 +end;
    1.97 +
    1.98 +structure USyntax: USYNTAX =
    1.99 +struct
   1.100 +
   1.101 +infix 4 ##;
   1.102 +
   1.103 +fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
   1.104 +
   1.105 +
   1.106 +(*---------------------------------------------------------------------------
   1.107 + *
   1.108 + *                            Types
   1.109 + *
   1.110 + *---------------------------------------------------------------------------*)
   1.111 +val mk_prim_vartype = TVar;
   1.112 +fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.termS);
   1.113 +
   1.114 +(* But internally, it's useful *)
   1.115 +fun dest_vtype (TVar x) = x
   1.116 +  | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
   1.117 +
   1.118 +val is_vartype = can dest_vtype;
   1.119 +
   1.120 +val type_vars  = map mk_prim_vartype o typ_tvars
   1.121 +fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
   1.122 +
   1.123 +val alpha  = mk_vartype "'a"
   1.124 +val beta   = mk_vartype "'b"
   1.125 +
   1.126 +val strip_prod_type = HOLogic.prodT_factors;
   1.127 +
   1.128 +
   1.129 +
   1.130 +(*---------------------------------------------------------------------------
   1.131 + *
   1.132 + *                              Terms
   1.133 + *
   1.134 + *---------------------------------------------------------------------------*)
   1.135 +
   1.136 +(* Free variables, in order of occurrence, from left to right in the
   1.137 + * syntax tree. *)
   1.138 +fun free_vars_lr tm =
   1.139 +  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
   1.140 +      fun add (t, frees) = case t of
   1.141 +            Free   _ => if (memb t frees) then frees else t::frees
   1.142 +          | Abs (_,_,body) => add(body,frees)
   1.143 +          | f$t =>  add(t, add(f, frees))
   1.144 +          | _ => frees
   1.145 +  in rev(add(tm,[]))
   1.146 +  end;
   1.147 +
   1.148 +
   1.149 +
   1.150 +val type_vars_in_term = map mk_prim_vartype o term_tvars;
   1.151 +
   1.152 +
   1.153 +
   1.154 +(* Prelogic *)
   1.155 +fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
   1.156 +fun inst theta = subst_vars (map dest_tybinding theta,[])
   1.157 +
   1.158 +
   1.159 +(* Construction routines *)
   1.160 +
   1.161 +fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   1.162 +  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   1.163 +  | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
   1.164 +
   1.165 +
   1.166 +fun mk_imp{ant,conseq} =
   1.167 +   let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   1.168 +   in list_comb(c,[ant,conseq])
   1.169 +   end;
   1.170 +
   1.171 +fun mk_select (r as {Bvar,Body}) =
   1.172 +  let val ty = type_of Bvar
   1.173 +      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
   1.174 +  in list_comb(c,[mk_abs r])
   1.175 +  end;
   1.176 +
   1.177 +fun mk_forall (r as {Bvar,Body}) =
   1.178 +  let val ty = type_of Bvar
   1.179 +      val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
   1.180 +  in list_comb(c,[mk_abs r])
   1.181 +  end;
   1.182 +
   1.183 +fun mk_exists (r as {Bvar,Body}) =
   1.184 +  let val ty = type_of Bvar
   1.185 +      val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
   1.186 +  in list_comb(c,[mk_abs r])
   1.187 +  end;
   1.188 +
   1.189 +
   1.190 +fun mk_conj{conj1,conj2} =
   1.191 +   let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   1.192 +   in list_comb(c,[conj1,conj2])
   1.193 +   end;
   1.194 +
   1.195 +fun mk_disj{disj1,disj2} =
   1.196 +   let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   1.197 +   in list_comb(c,[disj1,disj2])
   1.198 +   end;
   1.199 +
   1.200 +fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
   1.201 +
   1.202 +local
   1.203 +fun mk_uncurry(xt,yt,zt) =
   1.204 +    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
   1.205 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   1.206 +  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   1.207 +fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   1.208 +in
   1.209 +fun mk_pabs{varstruct,body} =
   1.210 + let fun mpa (varstruct, body) =
   1.211 +       if is_var varstruct
   1.212 +       then mk_abs {Bvar = varstruct, Body = body}
   1.213 +       else let val {fst, snd} = dest_pair varstruct
   1.214 +            in mk_uncurry (type_of fst, type_of snd, type_of body) $
   1.215 +               mpa (fst, mpa (snd, body))
   1.216 +            end
   1.217 + in mpa (varstruct, body) end
   1.218 + handle TYPE _ => raise USYN_ERR "mk_pabs" "";
   1.219 +end;
   1.220 +
   1.221 +(* Destruction routines *)
   1.222 +
   1.223 +datatype lambda = VAR   of {Name : string, Ty : typ}
   1.224 +                | CONST of {Name : string, Ty : typ}
   1.225 +                | COMB  of {Rator: term, Rand : term}
   1.226 +                | LAMB  of {Bvar : term, Body : term};
   1.227 +
   1.228 +
   1.229 +fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
   1.230 +  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
   1.231 +  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
   1.232 +  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
   1.233 +  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
   1.234 +                               in LAMB{Bvar = v, Body = betapply (M,v)}
   1.235 +                               end
   1.236 +  | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
   1.237 +
   1.238 +fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
   1.239 +  | dest_const _ = raise USYN_ERR "dest_const" "not a constant";
   1.240 +
   1.241 +fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
   1.242 +  | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
   1.243 +
   1.244 +fun dest_abs used (a as Abs(s, ty, M)) =
   1.245 +     let
   1.246 +       val s' = variant used s;
   1.247 +       val v = Free(s', ty);
   1.248 +     in ({Bvar = v, Body = betapply (a,v)}, s'::used)
   1.249 +     end
   1.250 +  | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
   1.251 +
   1.252 +fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
   1.253 +  | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
   1.254 +
   1.255 +fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
   1.256 +  | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
   1.257 +
   1.258 +fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
   1.259 +  | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
   1.260 +
   1.261 +fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
   1.262 +  | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
   1.263 +
   1.264 +fun dest_neg(Const("not",_) $ M) = M
   1.265 +  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
   1.266 +
   1.267 +fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
   1.268 +  | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
   1.269 +
   1.270 +fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
   1.271 +  | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
   1.272 +
   1.273 +fun mk_pair{fst,snd} =
   1.274 +   let val ty1 = type_of fst
   1.275 +       val ty2 = type_of snd
   1.276 +       val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
   1.277 +   in list_comb(c,[fst,snd])
   1.278 +   end;
   1.279 +
   1.280 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   1.281 +  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   1.282 +
   1.283 +
   1.284 +local  fun ucheck t = (if #Name(dest_const t) = "split" then t
   1.285 +                       else raise Match)
   1.286 +in
   1.287 +fun dest_pabs used tm =
   1.288 +   let val ({Bvar,Body}, used') = dest_abs used tm
   1.289 +   in {varstruct = Bvar, body = Body, used = used'}
   1.290 +   end handle Utils.ERR _ =>
   1.291 +          let val {Rator,Rand} = dest_comb tm
   1.292 +              val _ = ucheck Rator
   1.293 +              val {varstruct = lv, body, used = used'} = dest_pabs used Rand
   1.294 +              val {varstruct = rv, body, used = used''} = dest_pabs used' body
   1.295 +          in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
   1.296 +          end
   1.297 +end;
   1.298 +
   1.299 +
   1.300 +val lhs   = #lhs o dest_eq
   1.301 +val rhs   = #rhs o dest_eq
   1.302 +val rand  = #Rand o dest_comb
   1.303 +
   1.304 +
   1.305 +(* Query routines *)
   1.306 +val is_imp    = can dest_imp
   1.307 +val is_forall = can dest_forall
   1.308 +val is_exists = can dest_exists
   1.309 +val is_neg    = can dest_neg
   1.310 +val is_conj   = can dest_conj
   1.311 +val is_disj   = can dest_disj
   1.312 +val is_pair   = can dest_pair
   1.313 +val is_pabs   = can (dest_pabs [])
   1.314 +
   1.315 +
   1.316 +(* Construction of a cterm from a list of Terms *)
   1.317 +
   1.318 +fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
   1.319 +
   1.320 +(* These others are almost never used *)
   1.321 +fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
   1.322 +fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
   1.323 +val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
   1.324 +
   1.325 +
   1.326 +(* Need to reverse? *)
   1.327 +fun gen_all tm = list_mk_forall(term_frees tm, tm);
   1.328 +
   1.329 +(* Destructing a cterm to a list of Terms *)
   1.330 +fun strip_comb tm =
   1.331 +   let fun dest(M$N, A) = dest(M, N::A)
   1.332 +         | dest x = x
   1.333 +   in dest(tm,[])
   1.334 +   end;
   1.335 +
   1.336 +fun strip_abs(tm as Abs _) =
   1.337 +       let val ({Bvar,Body}, _) = dest_abs [] tm
   1.338 +           val (bvs, core) = strip_abs Body
   1.339 +       in (Bvar::bvs, core)
   1.340 +       end
   1.341 +  | strip_abs M = ([],M);
   1.342 +
   1.343 +
   1.344 +fun strip_imp fm =
   1.345 +   if (is_imp fm)
   1.346 +   then let val {ant,conseq} = dest_imp fm
   1.347 +            val (was,wb) = strip_imp conseq
   1.348 +        in ((ant::was), wb)
   1.349 +        end
   1.350 +   else ([],fm);
   1.351 +
   1.352 +fun strip_forall fm =
   1.353 +   if (is_forall fm)
   1.354 +   then let val {Bvar,Body} = dest_forall fm
   1.355 +            val (bvs,core) = strip_forall Body
   1.356 +        in ((Bvar::bvs), core)
   1.357 +        end
   1.358 +   else ([],fm);
   1.359 +
   1.360 +
   1.361 +fun strip_exists fm =
   1.362 +   if (is_exists fm)
   1.363 +   then let val {Bvar, Body} = dest_exists fm
   1.364 +            val (bvs,core) = strip_exists Body
   1.365 +        in (Bvar::bvs, core)
   1.366 +        end
   1.367 +   else ([],fm);
   1.368 +
   1.369 +fun strip_disj w =
   1.370 +   if (is_disj w)
   1.371 +   then let val {disj1,disj2} = dest_disj w
   1.372 +        in (strip_disj disj1@strip_disj disj2)
   1.373 +        end
   1.374 +   else [w];
   1.375 +
   1.376 +
   1.377 +(* Miscellaneous *)
   1.378 +
   1.379 +fun mk_vstruct ty V =
   1.380 +  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
   1.381 +              let val (ltm,vs1) = follow_prod_type ty1 vs
   1.382 +                  val (rtm,vs2) = follow_prod_type ty2 vs1
   1.383 +              in (mk_pair{fst=ltm, snd=rtm}, vs2) end
   1.384 +        | follow_prod_type _ (v::vs) = (v,vs)
   1.385 +  in #1 (follow_prod_type ty V)  end;
   1.386 +
   1.387 +
   1.388 +(* Search a term for a sub-term satisfying the predicate p. *)
   1.389 +fun find_term p =
   1.390 +   let fun find tm =
   1.391 +      if (p tm) then Some tm
   1.392 +      else case tm of
   1.393 +          Abs(_,_,body) => find body
   1.394 +        | (t$u)         => (case find t of None => find u | some => some)
   1.395 +        | _             => None
   1.396 +   in find
   1.397 +   end;
   1.398 +
   1.399 +fun dest_relation tm =
   1.400 +   if (type_of tm = HOLogic.boolT)
   1.401 +   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
   1.402 +        in (R,y,x)
   1.403 +        end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
   1.404 +   else raise USYN_ERR "dest_relation" "not a boolean term";
   1.405 +
   1.406 +fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
   1.407 +  | is_WFR _                 = false;
   1.408 +
   1.409 +fun ARB ty = mk_select{Bvar=Free("v",ty),
   1.410 +                       Body=Const("True",HOLogic.boolT)};
   1.411 +
   1.412 +end;