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