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