1 2(* this contains all info about the model, including the properties to be checked, and th eventual results *) 3(* the main reason for having this as an opaque type is to give holCheck a clean and stable signature *) 4(* otherwise there is no pressing reason to not allow users to modify models directly *) 5(* FIXME: allow a get_ks type ability at least*) 6structure modelTools :> modelTools = 7struct 8 9local 10 11open Globals HolKernel Parse 12open PrimitiveBddRules pairSyntax 13open internalCacheTools commonTools muSyntax 14 15in 16 17open Abbrev 18 19type ic = internalCacheTools.ic 20type term_bdd = PrimitiveBddRules.term_bdd 21type model = {init: term option, 22 trans: (string * term) list option, 23 ric: bool option, 24 name: string option, 25 vord: string list option, 26 state: term option, 27 props: (string*term) list option, 28 results: (term_bdd * thm option * term list option) list option, 29 ic:internalCacheTools.ic option, 30 flags: {abs:bool}} 31 32val empty_model = {init=NONE,trans=NONE,ric=NONE,name=NONE,vord=NONE,state=NONE,props=NONE,results=NONE,ic=NONE, 33 flags={abs=true}} 34 35(* getters *) 36 37fun get_name (m:model) = #name(m) 38fun get_init (m:model) = valOf (#init(m)) 39fun get_trans (m:model) = valOf (#trans(m)) 40fun get_flag_ric (m:model) = valOf (#ric(m)) 41fun get_vord (m:model) = #vord(m) 42fun get_state (m:model) = #state(m) 43fun get_props (m:model) = valOf (#props(m)) 44fun get_results (m:model) = #results(m) 45fun get_ic (m:model) = #ic(m) 46 47fun get_flag_abs (m:model) = #abs (#flags m) (*if true, hc will try to do abstraction if possible and worthwhile; otherwise no abs *) 48 49(* setters *) 50fun set_name nm (m:model) = 51 (if Lexis.allowed_term_constant nm then () else failwith ("modelTools.set_name: name must be a legal HOL constant name"); 52 {init= #init(m),trans= #trans(m),ric= #ric(m),name= SOME nm,vord= #vord(m), 53 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)}) 54 55fun set_init i (m:model) = 56 (if is_prop_tm i then () else failwith ("modelTools.set_init: non-propositional term (contains non-T/F bool constants?)"); 57 {init= SOME i,trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 58 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)}) 59 60fun set_flag_ric r (m:model) = 61 {init= #init(m),trans= #trans(m),ric= SOME r,name= #name(m),vord= #vord(m), 62 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)} 63 64fun set_vord v (m:model) = (* no point in any vetting here since it is easy to get around *) 65 {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= SOME v, 66 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)} 67 68fun set_state s (m:model) = (* no point in any vetting here since it is easy to get around *) 69 {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 70 state= SOME s,props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)} 71 72fun set_trans t (m:model) = 73 (let val (nm,R) = ListPair.unzip t 74 val nms = HOLset.addList(HOLset.empty String.compare,nm) 75 in 76 if List.foldl (fn (t,v) => is_prop_tm t andalso v) true R 77 then 78 if (HOLset.numItems nms=List.length t) 79 then 80 if not (HOLset.member(nms,".")) orelse List.length t=1 81 then 82 if List.length t>0 83 then () 84 else failwith ("modelTools.set_trans: no transitions specified") 85 else failwith ("modelTools.set_trans: non-singleton transition list contains \".\" as transition label") 86 else failwith ("modelTools.set_trans: transition labels are not unique") 87 else failwith ("modelTools.set_trans: non-propositional term") end; 88 {init= #init(m),trans= SOME t,ric= #ric(m),name= #name(m),vord= #vord(m), 89 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)}) 90 91fun set_props p (m:model) = 92 (let val (nm,fl) = ListPair.unzip p 93 val nms = HOLset.addList(HOLset.empty String.compare,nm) 94 val aps = List.concat (List.map holCheckTools.find_aps fl) 95 in if (HOLset.numItems nms=List.length p) 96 then if List.length p>0 97 then 98 if List.foldl (fn (t,v) => Lexis.allowed_term_constant t andalso v) true nm 99 then if null aps orelse List.foldl (fn (f,v) => is_pabs f andalso v) true aps 100 then if null aps orelse List.foldl (fn ((s,p),v) => is_bool_var p andalso v) true (List.map dest_pabs aps) 101 then if null aps orelse fst(List.foldl (fn ((s,p),(v,st)) => (Term.compare(s,st)=EQUAL andalso v,st)) 102 (true,fst (dest_pabs (hd aps))) (List.map dest_pabs aps)) 103 then () 104 else failwith ("modelTools.set_props: different state tuples used in atomic propositions") 105 else failwith ("modelTools.set_props: atomic proposition value must be a boolean variable") 106 else failwith ("modelTools.set_props: atomic proposition is not a paired abstraction") 107 else failwith ("modelTools.set_props: property names must be legal HOL constant names") 108 else failwith ("modelTools.set_props: no properties specified") 109 else failwith ("modelTools.set_props: property names are not unique") end; 110 {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 111 state= #state(m),props= SOME p,results= #results(m),ic= #ic(m),flags = #flags(m)}) 112 113fun set_results res (m:model) = 114 {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 115 state= #state(m),props= #props(m),results = SOME res,ic= #ic(m),flags = #flags(m)} 116 117fun set_ic ic (m:model) = 118 {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 119 state= #state(m),props= #props(m),results= #results(m) ,ic=SOME ic,flags = #flags(m)} 120 121fun set_flag_abs abs (m:model) = 122 {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 123 state= #state(m),props= #props(m),results= #results(m) ,ic= #ic(m), 124 flags={abs=abs}} 125 126fun add_trans t (m:model) = (*FIXME: expose this (need more infrastructure to handle invalidation of results since model has changed) *) 127 let val t' = #trans(m) 128 in if isSome t' 129 then {init= #init(m),trans= SOME (t::(valOf t')),ric= #ric(m),name= #name(m),vord= #vord(m), 130 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)} 131 else {init= #init(m),trans= SOME [t],ric= #ric(m),name= #name(m),vord= #vord(m), 132 state= #state(m),props= #props(m),results= #results(m),ic= #ic(m),flags = #flags(m)} 133 end 134 135fun add_prop p (m:model) = 136 let val p' = #props(m) 137 in if isSome p' 138 then {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 139 state= #state(m),props= SOME (p::(valOf p')),results= #results(m),ic= #ic(m),flags = #flags(m)} 140 else {init= #init(m),trans= #trans(m),ric= #ric(m),name= #name(m),vord= #vord(m), 141 state= #state(m),props= SOME [p],results= #results(m),ic= #ic(m),flags = #flags(m)} 142 end 143 144(* destruction (does not return flags) *) 145 146fun dest_model m = (get_init m,get_trans m,get_flag_ric m,get_name m,get_vord m, 147 get_state m,get_props m,get_results m,get_ic m) 148 149(* unlazify *) 150 151fun prove_model (m:model) = 152 let val res = get_results m 153 in if isSome res 154 then set_results (List.map (fn r => if isSome (#2 r) 155 then let val (tb,th,tr) = r 156 in (lazyTools.prove_ltb tb,SOME (lazyTools.prove_lthm (valOf th)),tr) end 157 else r) 158 (valOf res)) m 159 else m 160 end 161 162end 163end 164