wenzelm@10769: (* Title: TFL/usyntax.ML wenzelm@10769: ID: $Id$ wenzelm@10769: Author: Konrad Slind, Cambridge University Computer Laboratory wenzelm@10769: Copyright 1997 University of Cambridge wenzelm@10769: wenzelm@10769: Emulation of HOL's abstract syntax functions. wenzelm@10769: *) wenzelm@10769: wenzelm@10769: signature USYNTAX = wenzelm@10769: sig wenzelm@10769: datatype lambda = VAR of {Name : string, Ty : typ} wenzelm@10769: | CONST of {Name : string, Ty : typ} wenzelm@10769: | COMB of {Rator: term, Rand : term} wenzelm@10769: | LAMB of {Bvar : term, Body : term} wenzelm@10769: wenzelm@10769: val alpha : typ wenzelm@10769: wenzelm@10769: (* Types *) wenzelm@10769: val type_vars : typ -> typ list wenzelm@10769: val type_varsl : typ list -> typ list wenzelm@10769: val mk_vartype : string -> typ wenzelm@10769: val is_vartype : typ -> bool wenzelm@10769: val strip_prod_type : typ -> typ list wenzelm@10769: wenzelm@10769: (* Terms *) wenzelm@10769: val free_vars_lr : term -> term list wenzelm@10769: val type_vars_in_term : term -> typ list wenzelm@10769: val dest_term : term -> lambda wenzelm@10769: wenzelm@10769: (* Prelogic *) wenzelm@10769: val inst : (typ*typ) list -> term -> term wenzelm@10769: wenzelm@10769: (* Construction routines *) wenzelm@10769: val mk_abs :{Bvar : term, Body : term} -> term wenzelm@10769: wenzelm@10769: val mk_imp :{ant : term, conseq : term} -> term wenzelm@10769: val mk_select :{Bvar : term, Body : term} -> term wenzelm@10769: val mk_forall :{Bvar : term, Body : term} -> term wenzelm@10769: val mk_exists :{Bvar : term, Body : term} -> term wenzelm@10769: val mk_conj :{conj1 : term, conj2 : term} -> term wenzelm@10769: val mk_disj :{disj1 : term, disj2 : term} -> term wenzelm@10769: val mk_pabs :{varstruct : term, body : term} -> term wenzelm@10769: wenzelm@10769: (* Destruction routines *) wenzelm@10769: val dest_const: term -> {Name : string, Ty : typ} wenzelm@10769: val dest_comb : term -> {Rator : term, Rand : term} wenzelm@10769: val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list wenzelm@10769: val dest_eq : term -> {lhs : term, rhs : term} wenzelm@10769: val dest_imp : term -> {ant : term, conseq : term} wenzelm@10769: val dest_forall : term -> {Bvar : term, Body : term} wenzelm@10769: val dest_exists : term -> {Bvar : term, Body : term} wenzelm@10769: val dest_neg : term -> term wenzelm@10769: val dest_conj : term -> {conj1 : term, conj2 : term} wenzelm@10769: val dest_disj : term -> {disj1 : term, disj2 : term} wenzelm@10769: val dest_pair : term -> {fst : term, snd : term} wenzelm@10769: val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list} wenzelm@10769: wenzelm@10769: val lhs : term -> term wenzelm@10769: val rhs : term -> term wenzelm@10769: val rand : term -> term wenzelm@10769: wenzelm@10769: (* Query routines *) wenzelm@10769: val is_imp : term -> bool wenzelm@10769: val is_forall : term -> bool wenzelm@10769: val is_exists : term -> bool wenzelm@10769: val is_neg : term -> bool wenzelm@10769: val is_conj : term -> bool wenzelm@10769: val is_disj : term -> bool wenzelm@10769: val is_pair : term -> bool wenzelm@10769: val is_pabs : term -> bool wenzelm@10769: wenzelm@10769: (* Construction of a term from a list of Preterms *) wenzelm@10769: val list_mk_abs : (term list * term) -> term wenzelm@10769: val list_mk_imp : (term list * term) -> term wenzelm@10769: val list_mk_forall : (term list * term) -> term wenzelm@10769: val list_mk_conj : term list -> term wenzelm@10769: wenzelm@10769: (* Destructing a term to a list of Preterms *) wenzelm@10769: val strip_comb : term -> (term * term list) wenzelm@10769: val strip_abs : term -> (term list * term) wenzelm@10769: val strip_imp : term -> (term list * term) wenzelm@10769: val strip_forall : term -> (term list * term) wenzelm@10769: val strip_exists : term -> (term list * term) wenzelm@10769: val strip_disj : term -> term list wenzelm@10769: wenzelm@10769: (* Miscellaneous *) wenzelm@10769: val mk_vstruct : typ -> term list -> term wenzelm@10769: val gen_all : term -> term wenzelm@10769: val find_term : (term -> bool) -> term -> term option wenzelm@10769: val dest_relation : term -> term * term * term wenzelm@10769: val is_WFR : term -> bool wenzelm@10769: val ARB : typ -> term wenzelm@10769: end; wenzelm@10769: wenzelm@10769: structure USyntax: USYNTAX = wenzelm@10769: struct wenzelm@10769: wenzelm@10769: infix 4 ##; wenzelm@10769: wenzelm@10769: fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; wenzelm@10769: wenzelm@10769: wenzelm@10769: (*--------------------------------------------------------------------------- wenzelm@10769: * wenzelm@10769: * Types wenzelm@10769: * wenzelm@10769: *---------------------------------------------------------------------------*) wenzelm@10769: val mk_prim_vartype = TVar; wenzelm@12340: fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS); wenzelm@10769: wenzelm@10769: (* But internally, it's useful *) wenzelm@10769: fun dest_vtype (TVar x) = x wenzelm@10769: | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; wenzelm@10769: wenzelm@10769: val is_vartype = can dest_vtype; wenzelm@10769: wenzelm@10769: val type_vars = map mk_prim_vartype o typ_tvars wenzelm@10769: fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []); wenzelm@10769: wenzelm@10769: val alpha = mk_vartype "'a" wenzelm@10769: val beta = mk_vartype "'b" wenzelm@10769: wenzelm@10769: val strip_prod_type = HOLogic.prodT_factors; wenzelm@10769: wenzelm@10769: wenzelm@10769: wenzelm@10769: (*--------------------------------------------------------------------------- wenzelm@10769: * wenzelm@10769: * Terms wenzelm@10769: * wenzelm@10769: *---------------------------------------------------------------------------*) wenzelm@10769: wenzelm@10769: (* Free variables, in order of occurrence, from left to right in the wenzelm@10769: * syntax tree. *) wenzelm@10769: fun free_vars_lr tm = wenzelm@10769: let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end wenzelm@10769: fun add (t, frees) = case t of wenzelm@10769: Free _ => if (memb t frees) then frees else t::frees wenzelm@10769: | Abs (_,_,body) => add(body,frees) wenzelm@10769: | f$t => add(t, add(f, frees)) wenzelm@10769: | _ => frees wenzelm@10769: in rev(add(tm,[])) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: wenzelm@10769: wenzelm@10769: val type_vars_in_term = map mk_prim_vartype o term_tvars; wenzelm@10769: wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Prelogic *) wenzelm@10769: fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) wenzelm@10769: fun inst theta = subst_vars (map dest_tybinding theta,[]) wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Construction routines *) wenzelm@10769: wenzelm@10769: fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) wenzelm@10769: | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) wenzelm@10769: | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable"; wenzelm@10769: wenzelm@10769: wenzelm@10769: fun mk_imp{ant,conseq} = wenzelm@10769: let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) wenzelm@10769: in list_comb(c,[ant,conseq]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun mk_select (r as {Bvar,Body}) = wenzelm@10769: let val ty = type_of Bvar berghofe@13182: val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty) wenzelm@10769: in list_comb(c,[mk_abs r]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun mk_forall (r as {Bvar,Body}) = wenzelm@10769: let val ty = type_of Bvar wenzelm@10769: val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT) wenzelm@10769: in list_comb(c,[mk_abs r]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun mk_exists (r as {Bvar,Body}) = wenzelm@10769: let val ty = type_of Bvar wenzelm@10769: val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT) wenzelm@10769: in list_comb(c,[mk_abs r]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: wenzelm@10769: fun mk_conj{conj1,conj2} = wenzelm@10769: let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) wenzelm@10769: in list_comb(c,[conj1,conj2]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun mk_disj{disj1,disj2} = wenzelm@10769: let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) wenzelm@10769: in list_comb(c,[disj1,disj2]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); wenzelm@10769: wenzelm@10769: local wenzelm@10769: fun mk_uncurry(xt,yt,zt) = wenzelm@10769: Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) wenzelm@10769: fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} wenzelm@10769: | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" wenzelm@10769: fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false wenzelm@10769: in wenzelm@10769: fun mk_pabs{varstruct,body} = wenzelm@10769: let fun mpa (varstruct, body) = wenzelm@10769: if is_var varstruct wenzelm@10769: then mk_abs {Bvar = varstruct, Body = body} wenzelm@10769: else let val {fst, snd} = dest_pair varstruct wenzelm@10769: in mk_uncurry (type_of fst, type_of snd, type_of body) $ wenzelm@10769: mpa (fst, mpa (snd, body)) wenzelm@10769: end wenzelm@10769: in mpa (varstruct, body) end wenzelm@10769: handle TYPE _ => raise USYN_ERR "mk_pabs" ""; wenzelm@10769: end; wenzelm@10769: wenzelm@10769: (* Destruction routines *) wenzelm@10769: wenzelm@10769: datatype lambda = VAR of {Name : string, Ty : typ} wenzelm@10769: | CONST of {Name : string, Ty : typ} wenzelm@10769: | COMB of {Rator: term, Rand : term} wenzelm@10769: | LAMB of {Bvar : term, Body : term}; wenzelm@10769: wenzelm@10769: wenzelm@10769: fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} wenzelm@10769: | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} wenzelm@10769: | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} wenzelm@10769: | dest_term(M$N) = COMB{Rator=M,Rand=N} wenzelm@10769: | dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) wenzelm@10769: in LAMB{Bvar = v, Body = betapply (M,v)} wenzelm@10769: end wenzelm@10769: | dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound"; wenzelm@10769: wenzelm@10769: fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} wenzelm@10769: | dest_const _ = raise USYN_ERR "dest_const" "not a constant"; wenzelm@10769: wenzelm@10769: fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} wenzelm@10769: | dest_comb _ = raise USYN_ERR "dest_comb" "not a comb"; wenzelm@10769: wenzelm@10769: fun dest_abs used (a as Abs(s, ty, M)) = wenzelm@10769: let wenzelm@10769: val s' = variant used s; wenzelm@10769: val v = Free(s', ty); wenzelm@10769: in ({Bvar = v, Body = betapply (a,v)}, s'::used) wenzelm@10769: end wenzelm@10769: | dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction"; wenzelm@10769: wenzelm@10769: fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} wenzelm@10769: | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality"; wenzelm@10769: wenzelm@10769: fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} wenzelm@10769: | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication"; wenzelm@10769: wenzelm@10769: fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a) wenzelm@10769: | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall"; wenzelm@10769: wenzelm@10769: fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a) wenzelm@10769: | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential"; wenzelm@10769: wenzelm@10769: fun dest_neg(Const("not",_) $ M) = M wenzelm@10769: | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; wenzelm@10769: wenzelm@10769: fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} wenzelm@10769: | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction"; wenzelm@10769: wenzelm@10769: fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} wenzelm@10769: | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction"; wenzelm@10769: wenzelm@10769: fun mk_pair{fst,snd} = wenzelm@10769: let val ty1 = type_of fst wenzelm@10769: val ty2 = type_of snd wenzelm@10769: val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2) wenzelm@10769: in list_comb(c,[fst,snd]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} wenzelm@10769: | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; wenzelm@10769: wenzelm@10769: wenzelm@10769: local fun ucheck t = (if #Name(dest_const t) = "split" then t wenzelm@10769: else raise Match) wenzelm@10769: in wenzelm@10769: fun dest_pabs used tm = wenzelm@10769: let val ({Bvar,Body}, used') = dest_abs used tm wenzelm@10769: in {varstruct = Bvar, body = Body, used = used'} wenzelm@10769: end handle Utils.ERR _ => wenzelm@10769: let val {Rator,Rand} = dest_comb tm wenzelm@10769: val _ = ucheck Rator wenzelm@10769: val {varstruct = lv, body, used = used'} = dest_pabs used Rand wenzelm@10769: val {varstruct = rv, body, used = used''} = dest_pabs used' body wenzelm@10769: in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} wenzelm@10769: end wenzelm@10769: end; wenzelm@10769: wenzelm@10769: wenzelm@10769: val lhs = #lhs o dest_eq wenzelm@10769: val rhs = #rhs o dest_eq wenzelm@10769: val rand = #Rand o dest_comb wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Query routines *) wenzelm@10769: val is_imp = can dest_imp wenzelm@10769: val is_forall = can dest_forall wenzelm@10769: val is_exists = can dest_exists wenzelm@10769: val is_neg = can dest_neg wenzelm@10769: val is_conj = can dest_conj wenzelm@10769: val is_disj = can dest_disj wenzelm@10769: val is_pair = can dest_pair wenzelm@10769: val is_pabs = can (dest_pabs []) wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Construction of a cterm from a list of Terms *) wenzelm@10769: wenzelm@10769: fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; wenzelm@10769: wenzelm@10769: (* These others are almost never used *) wenzelm@10769: fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; wenzelm@10769: fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t; wenzelm@10769: val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Need to reverse? *) wenzelm@10769: fun gen_all tm = list_mk_forall(term_frees tm, tm); wenzelm@10769: wenzelm@10769: (* Destructing a cterm to a list of Terms *) wenzelm@10769: fun strip_comb tm = wenzelm@10769: let fun dest(M$N, A) = dest(M, N::A) wenzelm@10769: | dest x = x wenzelm@10769: in dest(tm,[]) wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun strip_abs(tm as Abs _) = wenzelm@10769: let val ({Bvar,Body}, _) = dest_abs [] tm wenzelm@10769: val (bvs, core) = strip_abs Body wenzelm@10769: in (Bvar::bvs, core) wenzelm@10769: end wenzelm@10769: | strip_abs M = ([],M); wenzelm@10769: wenzelm@10769: wenzelm@10769: fun strip_imp fm = wenzelm@10769: if (is_imp fm) wenzelm@10769: then let val {ant,conseq} = dest_imp fm wenzelm@10769: val (was,wb) = strip_imp conseq wenzelm@10769: in ((ant::was), wb) wenzelm@10769: end wenzelm@10769: else ([],fm); wenzelm@10769: wenzelm@10769: fun strip_forall fm = wenzelm@10769: if (is_forall fm) wenzelm@10769: then let val {Bvar,Body} = dest_forall fm wenzelm@10769: val (bvs,core) = strip_forall Body wenzelm@10769: in ((Bvar::bvs), core) wenzelm@10769: end wenzelm@10769: else ([],fm); wenzelm@10769: wenzelm@10769: wenzelm@10769: fun strip_exists fm = wenzelm@10769: if (is_exists fm) wenzelm@10769: then let val {Bvar, Body} = dest_exists fm wenzelm@10769: val (bvs,core) = strip_exists Body wenzelm@10769: in (Bvar::bvs, core) wenzelm@10769: end wenzelm@10769: else ([],fm); wenzelm@10769: wenzelm@10769: fun strip_disj w = wenzelm@10769: if (is_disj w) wenzelm@10769: then let val {disj1,disj2} = dest_disj w wenzelm@10769: in (strip_disj disj1@strip_disj disj2) wenzelm@10769: end wenzelm@10769: else [w]; wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Miscellaneous *) wenzelm@10769: wenzelm@10769: fun mk_vstruct ty V = wenzelm@10769: let fun follow_prod_type (Type("*",[ty1,ty2])) vs = wenzelm@10769: let val (ltm,vs1) = follow_prod_type ty1 vs wenzelm@10769: val (rtm,vs2) = follow_prod_type ty2 vs1 wenzelm@10769: in (mk_pair{fst=ltm, snd=rtm}, vs2) end wenzelm@10769: | follow_prod_type _ (v::vs) = (v,vs) wenzelm@10769: in #1 (follow_prod_type ty V) end; wenzelm@10769: wenzelm@10769: wenzelm@10769: (* Search a term for a sub-term satisfying the predicate p. *) wenzelm@10769: fun find_term p = wenzelm@10769: let fun find tm = wenzelm@10769: if (p tm) then Some tm wenzelm@10769: else case tm of wenzelm@10769: Abs(_,_,body) => find body wenzelm@10769: | (t$u) => (case find t of None => find u | some => some) wenzelm@10769: | _ => None wenzelm@10769: in find wenzelm@10769: end; wenzelm@10769: wenzelm@10769: fun dest_relation tm = wenzelm@10769: if (type_of tm = HOLogic.boolT) wenzelm@10769: then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm wenzelm@10769: in (R,y,x) wenzelm@10769: end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" wenzelm@10769: else raise USYN_ERR "dest_relation" "not a boolean term"; wenzelm@10769: wenzelm@10769: fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true wenzelm@10769: | is_WFR _ = false; wenzelm@10769: wenzelm@10769: fun ARB ty = mk_select{Bvar=Free("v",ty), wenzelm@10769: Body=Const("True",HOLogic.boolT)}; wenzelm@10769: wenzelm@10769: end;