author  berghofe 
Fri, 29 Jun 2012 09:45:48 +0200  
changeset 48167  da1a1eae93fa 
parent 47880  7e202f71a249 
child 48453  2421ff8c57a5 
permissions  rwrr 
41561  1 
(* Title: HOL/SPARK/Tools/spark_vcs.ML 
2 
Author: Stefan Berghofer 

3 
Copyright: secunet Security Networks AG 

4 

5 
Store for verification conditions generated by SPARK/Ada. 

6 
*) 

7 

8 
signature SPARK_VCS = 

9 
sig 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

10 
val set_vcs: Fdl_Parser.decls > Fdl_Parser.rules > 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

11 
(string * string) * Fdl_Parser.vcs > Path.T > string > theory > theory 
41561  12 
val add_proof_fun: (typ option > 'a > term) > 
13 
string * ((string list * string) option * 'a) > 

14 
theory > theory 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

15 
val add_type: string * (typ * (string * string) list) > theory > theory 
48167  16 
val lookup_vc: theory > bool > string > (Element.context_i list * 
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41878
diff
changeset

17 
(string * thm list option * Element.context_i * Element.statement_i)) option 
48167  18 
val get_vcs: theory > bool > 
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41878
diff
changeset

19 
Element.context_i list * (binding * thm) list * (string * 
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41878
diff
changeset

20 
(string * thm list option * Element.context_i * Element.statement_i)) list 
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41878
diff
changeset

21 
val mark_proved: string > thm list > theory > theory 
48167  22 
val close: bool > theory > theory 
41561  23 
val is_closed: theory > bool 
24 
end; 

25 

26 
structure SPARK_VCs: SPARK_VCS = 

27 
struct 

28 

29 
open Fdl_Parser; 

30 

31 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

32 
(** theory data **) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

33 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

34 
fun err_unfinished () = error "An unfinished SPARK environment is still open." 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

35 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

36 
val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode; 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

37 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

38 
val name_ord = prod_ord string_ord (option_ord int_ord) o 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

39 
pairself (strip_number ##> Int.fromString); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

40 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

41 
structure VCtab = Table(type key = string val ord = name_ord); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

42 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

43 
structure VCs = Theory_Data 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

44 
( 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

45 
type T = 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

46 
{pfuns: ((string list * string) option * term) Symtab.table, 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

47 
type_map: (typ * (string * string) list) Symtab.table, 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

48 
env: 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

49 
{ctxt: Element.context_i list, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

50 
defs: (binding * thm) list, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

51 
types: fdl_type tab, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

52 
funs: (string list * string) tab, 
46567  53 
pfuns: ((string list * string) option * term) Symtab.table, 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

54 
ids: (term * string) Symtab.table * Name.context, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

55 
proving: bool, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

56 
vcs: (string * thm list option * 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

57 
(string * expr) list * (string * expr) list) VCtab.table, 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

58 
path: Path.T, 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

59 
prefix: string} option} 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

60 
val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE} 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

61 
val extend = I 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

62 
fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE}, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

63 
{pfuns = pfuns2, type_map = type_map2, env = NONE}) = 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

64 
{pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

65 
type_map = Symtab.merge (op =) (type_map1, type_map2), 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

66 
env = NONE} 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

67 
 merge _ = err_unfinished () 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

68 
) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

69 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

70 

41561  71 
(** utilities **) 
72 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

73 
val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

74 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

75 
val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

76 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

77 
fun lookup_prfx "" tab s = Symtab.lookup tab s 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

78 
 lookup_prfx prfx tab s = (case Symtab.lookup tab s of 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

79 
NONE => Symtab.lookup tab (prfx ^ "__" ^ s) 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

80 
 x => x); 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

81 

0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

82 
fun strip_prfx s = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

83 
let 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

84 
fun strip ys [] = ("", implode ys) 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

85 
 strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys) 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

86 
 strip ys (x :: xs) = strip (x :: ys) xs 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

87 
in strip [] (rev (raw_explode s)) end; 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

88 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

89 
fun unprefix_pfun "" s = s 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

90 
 unprefix_pfun prfx s = 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

91 
let val (prfx', s') = strip_prfx s 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

92 
in if prfx = prfx' then s' else s end; 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

93 

41561  94 
fun mk_unop s t = 
95 
let val T = fastype_of t 

96 
in Const (s, T > T) $ t end; 

97 

98 
fun mk_times (t, u) = 

99 
let 

100 
val setT = fastype_of t; 

101 
val T = HOLogic.dest_setT setT; 

102 
val U = HOLogic.dest_setT (fastype_of u) 

103 
in 

104 
Const (@{const_name Sigma}, setT > (T > HOLogic.mk_setT U) > 

105 
HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) 

106 
end; 

107 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

108 
fun get_type thy prfx ty = 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

109 
let val {type_map, ...} = VCs.get thy 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

110 
in lookup_prfx prfx type_map ty end; 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

111 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

112 
fun mk_type' _ _ "integer" = (HOLogic.intT, []) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

113 
 mk_type' _ _ "boolean" = (HOLogic.boolT, []) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

114 
 mk_type' thy prfx ty = 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

115 
(case get_type thy prfx ty of 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

116 
NONE => 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

117 
(Syntax.check_typ (Proof_Context.init_global thy) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

118 
(Type (Sign.full_name thy (Binding.name ty), [])), 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

119 
[]) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

120 
 SOME p => p); 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

121 

d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

122 
fun mk_type thy prfx ty = fst (mk_type' thy prfx ty); 
41561  123 

124 
val booleanN = "boolean"; 

125 
val integerN = "integer"; 

126 

127 
fun define_overloaded (def_name, eq) lthy = 

128 
let 

129 
val ((c, _), rhs) = eq > Syntax.check_term lthy > 

130 
Logic.dest_equals >> dest_Free; 

131 
val ((_, (_, thm)), lthy') = Local_Theory.define 

132 
((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy 

42361  133 
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); 
134 
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm 

41561  135 
in (thm', lthy') end; 
136 

137 
fun strip_underscores s = 

138 
strip_underscores (unsuffix "_" s) handle Fail _ => s; 

139 

140 
fun strip_tilde s = 

141 
unsuffix "~" s ^ "_init" handle Fail _ => s; 

142 

143 
val mangle_name = strip_underscores #> strip_tilde; 

144 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

145 
fun mk_variables thy prfx xs ty (tab, ctxt) = 
41561  146 
let 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

147 
val T = mk_type thy prfx ty; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42499
diff
changeset

148 
val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt; 
41561  149 
val zs = map (Free o rpair T) ys; 
150 
in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; 

151 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

152 
fun get_record_info thy T = (case Record.dest_recTs T of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

153 
[(tyname, [@{typ unit}])] => 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

154 
Record.get_info thy (Long_Name.qualifier tyname) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

155 
 _ => NONE); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

156 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

157 
fun find_field [] fname fields = 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

158 
find_first (curry lcase_eq fname o fst) fields 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

159 
 find_field cmap fname fields = 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

160 
(case AList.lookup (op =) cmap fname of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

161 
NONE => NONE 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

162 
 SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname'))); 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

163 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

164 
fun find_field' fname = get_first (fn (flds, fldty) => 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

165 
if member (op =) flds fname then SOME fldty else NONE); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

166 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

167 
fun assoc_ty_err thy T s msg = 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

168 
error ("Type " ^ Syntax.string_of_typ_global thy T ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

169 
" associated with SPARK type " ^ s ^ "\n" ^ msg); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

170 

41561  171 

172 
(** generate properties of enumeration types **) 

173 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

174 
fun add_enum_type tyname tyname' thy = 
41561  175 
let 
45906  176 
val {case_name, ...} = the (Datatype.get_info thy tyname'); 
177 
val cs = map Const (the (Datatype.get_constrs thy tyname')); 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

178 
val k = length cs; 
41561  179 
val T = Type (tyname', []); 
180 
val p = Const (@{const_name pos}, T > HOLogic.intT); 

181 
val v = Const (@{const_name val}, HOLogic.intT > T); 

182 
val card = Const (@{const_name card}, 

183 
HOLogic.mk_setT T > HOLogic.natT) $ HOLogic.mk_UNIV T; 

184 

185 
fun mk_binrel_def s f = Logic.mk_equals 

186 
(Const (s, T > T > HOLogic.boolT), 

187 
Abs ("x", T, Abs ("y", T, 

188 
Const (s, HOLogic.intT > HOLogic.intT > HOLogic.boolT) $ 

189 
(f $ Bound 1) $ (f $ Bound 0)))); 

190 

191 
val (((def1, def2), def3), lthy) = thy > 

192 

42416
a8a9f4d79196
 renamed enum type class to spark_enum, to avoid confusion with
berghofe
parents:
42396
diff
changeset

193 
Class.instantiation ([tyname'], [], @{sort spark_enum}) > 
41561  194 

195 
define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals 

196 
(p, 

197 
list_comb (Const (case_name, replicate k HOLogic.intT @ 

198 
[T] > HOLogic.intT), 

199 
map (HOLogic.mk_number HOLogic.intT) (0 upto k  1)))) >> 

200 

201 
define_overloaded ("less_eq_" ^ tyname ^ "_def", 

202 
mk_binrel_def @{const_name less_eq} p) >> 

203 
define_overloaded ("less_" ^ tyname ^ "_def", 

204 
mk_binrel_def @{const_name less} p); 

205 

206 
val UNIV_eq = Goal.prove lthy [] [] 

207 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

208 
(HOLogic.mk_UNIV T, HOLogic.mk_set T cs))) 

209 
(fn _ => 

210 
rtac @{thm subset_antisym} 1 THEN 

211 
rtac @{thm subsetI} 1 THEN 

45906  212 
Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info 
42361  213 
(Proof_Context.theory_of lthy) tyname'))) 1 THEN 
41561  214 
ALLGOALS (asm_full_simp_tac (simpset_of lthy))); 
215 

216 
val finite_UNIV = Goal.prove lthy [] [] 

217 
(HOLogic.mk_Trueprop (Const (@{const_name finite}, 

218 
HOLogic.mk_setT T > HOLogic.boolT) $ HOLogic.mk_UNIV T)) 

219 
(fn _ => simp_tac (simpset_of lthy addsimps [UNIV_eq]) 1); 

220 

221 
val card_UNIV = Goal.prove lthy [] [] 

222 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

223 
(card, HOLogic.mk_number HOLogic.natT k))) 

224 
(fn _ => simp_tac (simpset_of lthy addsimps [UNIV_eq]) 1); 

225 

226 
val range_pos = Goal.prove lthy [] [] 

227 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

228 
(Const (@{const_name image}, (T > HOLogic.intT) > 

229 
HOLogic.mk_setT T > HOLogic.mk_setT HOLogic.intT) $ 

230 
p $ HOLogic.mk_UNIV T, 

231 
Const (@{const_name atLeastLessThan}, HOLogic.intT > 

232 
HOLogic.intT > HOLogic.mk_setT HOLogic.intT) $ 

233 
HOLogic.mk_number HOLogic.intT 0 $ 

234 
(@{term int} $ card)))) 

235 
(fn _ => 

236 
simp_tac (simpset_of lthy addsimps [card_UNIV]) 1 THEN 

237 
simp_tac (simpset_of lthy addsimps [UNIV_eq, def1]) 1 THEN 

238 
rtac @{thm subset_antisym} 1 THEN 

239 
simp_tac (simpset_of lthy) 1 THEN 

240 
rtac @{thm subsetI} 1 THEN 

241 
asm_full_simp_tac (simpset_of lthy addsimps @{thms interval_expand} 

242 
delsimps @{thms atLeastLessThan_iff}) 1); 

243 

244 
val lthy' = 

245 
Class.prove_instantiation_instance (fn _ => 

246 
Class.intro_classes_tac [] THEN 

247 
rtac finite_UNIV 1 THEN 

248 
rtac range_pos 1 THEN 

249 
simp_tac (HOL_basic_ss addsimps [def3]) 1 THEN 

250 
simp_tac (HOL_basic_ss addsimps [def2]) 1) lthy; 

251 

252 
val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) => 

253 
let 

254 
val n = HOLogic.mk_number HOLogic.intT i; 

255 
val th = Goal.prove lthy' [] [] 

256 
(HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n))) 

257 
(fn _ => simp_tac (simpset_of lthy' addsimps [def1]) 1); 

258 
val th' = Goal.prove lthy' [] [] 

259 
(HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c))) 

260 
(fn _ => 

261 
rtac (@{thm inj_pos} RS @{thm injD}) 1 THEN 

262 
simp_tac (simpset_of lthy' addsimps 

263 
[@{thm pos_val}, range_pos, card_UNIV, th]) 1) 

264 
in (th, th') end) cs); 

265 

266 
val first_el = Goal.prove lthy' [] [] 

267 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

268 
(Const (@{const_name first_el}, T), hd cs))) 

269 
(fn _ => simp_tac (simpset_of lthy' addsimps 

270 
[@{thm first_el_def}, hd val_eqs]) 1); 

271 

272 
val last_el = Goal.prove lthy' [] [] 

273 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

274 
(Const (@{const_name last_el}, T), List.last cs))) 

275 
(fn _ => simp_tac (simpset_of lthy' addsimps 

276 
[@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); 

277 
in 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

278 
lthy' > 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

279 
Local_Theory.note 
45592  280 
((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) >> 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

281 
Local_Theory.note 
45592  282 
((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) >> 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

283 
Local_Theory.note 
45592  284 
((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) >> 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

285 
Local_Theory.note 
45592  286 
((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) >> 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

287 
Local_Theory.note 
45592  288 
((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) > snd > 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

289 
Local_Theory.exit_global 
41561  290 
end; 
291 

292 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

293 
fun check_no_assoc thy prfx s = case get_type thy prfx s of 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

294 
NONE => () 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

295 
 SOME _ => error ("Cannot associate a type with " ^ s ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

296 
"\nsince it is no record or enumeration type"); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

297 

e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

298 
fun check_enum [] [] = NONE 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

299 
 check_enum els [] = SOME ("has no element(s) " ^ commas els) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

300 
 check_enum [] cs = SOME ("has extra element(s) " ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

301 
commas (map (Long_Name.base_name o fst) cs)) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

302 
 check_enum (el :: els) ((cname, _) :: cs) = 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

303 
if lcase_eq (el, cname) then check_enum els cs 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

304 
else SOME ("either has no element " ^ el ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

305 
" or it is at the wrong position"); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

306 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

307 
fun invert_map [] = I 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

308 
 invert_map cmap = 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

309 
map (apfst (the o AList.lookup (op =) (map swap cmap))); 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

310 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

311 
fun add_type_def prfx (s, Basic_Type ty) (ids, thy) = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

312 
(check_no_assoc thy prfx s; 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

313 
(ids, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

314 
Typedecl.abbrev_global (Binding.name s, [], NoSyn) 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

315 
(mk_type thy prfx ty) thy > snd)) 
41561  316 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

317 
 add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) = 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

318 
let 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

319 
val (thy', tyname) = (case get_type thy prfx s of 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

320 
NONE => 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

321 
let 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

322 
val tyb = Binding.name s; 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

323 
val tyname = Sign.full_name thy tyb 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

324 
in 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

325 
(thy > 
45701  326 
Datatype.add_datatype {strict = true, quiet = true} 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

327 
[((tyb, [], NoSyn), 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

328 
map (fn s => (Binding.name s, [], NoSyn)) els)] > snd > 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

329 
add_enum_type s tyname, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

330 
tyname) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

331 
end 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

332 
 SOME (T as Type (tyname, []), cmap) => 
45906  333 
(case Datatype.get_constrs thy tyname of 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

334 
NONE => assoc_ty_err thy T s "is not a datatype" 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

335 
 SOME cs => 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

336 
let val (prfx', _) = strip_prfx s 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

337 
in 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

338 
case check_enum (map (unprefix_pfun prfx') els) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

339 
(invert_map cmap cs) of 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

340 
NONE => (thy, tyname) 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

341 
 SOME msg => assoc_ty_err thy T s msg 
46567  342 
end) 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

343 
 SOME (T, _) => assoc_ty_err thy T s "is not a datatype"); 
45906  344 
val cs = map Const (the (Datatype.get_constrs thy' tyname)); 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

345 
in 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

346 
((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

347 
fold Name.declare els ctxt), 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

348 
thy') 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

349 
end 
41561  350 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

351 
 add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

352 
(check_no_assoc thy prfx s; 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

353 
(ids, 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

354 
Typedecl.abbrev_global (Binding.name s, [], NoSyn) 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

355 
(foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) > 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

356 
mk_type thy prfx resty) thy > snd)) 
41561  357 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

358 
 add_type_def prfx (s, Record_Type fldtys) (ids, thy) = 
41561  359 
(ids, 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

360 
let val fldTs = maps (fn (flds, ty) => 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

361 
map (rpair (mk_type thy prfx ty)) flds) fldtys 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

362 
in case get_type thy prfx s of 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

363 
NONE => 
44653
6d8d09b90398
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
wenzelm
parents:
44030
diff
changeset

364 
Record.add_record ([], Binding.name s) NONE 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

365 
(map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

366 
 SOME (rT, cmap) => 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

367 
(case get_record_info thy rT of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

368 
NONE => assoc_ty_err thy rT s "is not a record type" 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

369 
 SOME {fields, ...} => 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

370 
let val fields' = invert_map cmap fields 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

371 
in 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

372 
(case subtract (lcase_eq o pairself fst) fldTs fields' of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

373 
[] => () 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

374 
 flds => assoc_ty_err thy rT s ("has extra field(s) " ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

375 
commas (map (Long_Name.base_name o fst) flds)); 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

376 
map (fn (fld, T) => 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

377 
case AList.lookup lcase_eq fields' fld of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

378 
NONE => assoc_ty_err thy rT s ("has no field " ^ fld) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

379 
 SOME U => T = U orelse assoc_ty_err thy rT s 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

380 
("has field " ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

381 
fld ^ " whose type\n" ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

382 
Syntax.string_of_typ_global thy U ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

383 
"\ndoes not match declared type\n" ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

384 
Syntax.string_of_typ_global thy T)) fldTs; 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

385 
thy) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

386 
end) 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

387 
end) 
41561  388 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

389 
 add_type_def prfx (s, Pending_Type) (ids, thy) = 
44030
b63a6bc144cf
Pending FDL types may now be associated with Isabelle types as well.
berghofe
parents:
43703
diff
changeset

390 
(ids, 
b63a6bc144cf
Pending FDL types may now be associated with Isabelle types as well.
berghofe
parents:
43703
diff
changeset

391 
case get_type thy prfx s of 
b63a6bc144cf
Pending FDL types may now be associated with Isabelle types as well.
berghofe
parents:
43703
diff
changeset

392 
SOME _ => thy 
b63a6bc144cf
Pending FDL types may now be associated with Isabelle types as well.
berghofe
parents:
43703
diff
changeset

393 
 NONE => Typedecl.typedecl_global 
b63a6bc144cf
Pending FDL types may now be associated with Isabelle types as well.
berghofe
parents:
43703
diff
changeset

394 
(Binding.name s, [], NoSyn) thy > snd); 
41561  395 

396 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

397 
fun term_of_expr thy prfx types pfuns = 
41561  398 
let 
399 
fun tm_of vs (Funct (">", [e, e'])) = 

400 
(HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

401 

402 
 tm_of vs (Funct ("<>", [e, e'])) = 

403 
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

404 

405 
 tm_of vs (Funct ("or", [e, e'])) = 

406 
(HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

407 

408 
 tm_of vs (Funct ("and", [e, e'])) = 

409 
(HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

410 

411 
 tm_of vs (Funct ("not", [e])) = 

412 
(HOLogic.mk_not (fst (tm_of vs e)), booleanN) 

413 

414 
 tm_of vs (Funct ("=", [e, e'])) = 

415 
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

416 

417 
 tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not 

418 
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN) 

419 

420 
 tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel @{const_name less} 

421 
(fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

422 

423 
 tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel @{const_name less} 

424 
(fst (tm_of vs e'), fst (tm_of vs e)), booleanN) 

425 

426 
 tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq} 

427 
(fst (tm_of vs e), fst (tm_of vs e')), booleanN) 

428 

429 
 tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq} 

430 
(fst (tm_of vs e'), fst (tm_of vs e)), booleanN) 

431 

432 
 tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop @{const_name plus} 

433 
(fst (tm_of vs e), fst (tm_of vs e')), integerN) 

434 

435 
 tm_of vs (Funct ("", [e, e'])) = (HOLogic.mk_binop @{const_name minus} 

436 
(fst (tm_of vs e), fst (tm_of vs e')), integerN) 

437 

438 
 tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop @{const_name times} 

439 
(fst (tm_of vs e), fst (tm_of vs e')), integerN) 

440 

441 
 tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop @{const_name divide} 

442 
(fst (tm_of vs e), fst (tm_of vs e')), integerN) 

443 

444 
 tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv} 

445 
(fst (tm_of vs e), fst (tm_of vs e')), integerN) 

446 

41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

447 
 tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod} 
41561  448 
(fst (tm_of vs e), fst (tm_of vs e')), integerN) 
449 

450 
 tm_of vs (Funct ("", [e])) = 

451 
(mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN) 

452 

453 
 tm_of vs (Funct ("**", [e, e'])) = 

454 
(Const (@{const_name power}, HOLogic.intT > HOLogic.natT > 

455 
HOLogic.intT) $ fst (tm_of vs e) $ 

456 
(@{const nat} $ fst (tm_of vs e')), integerN) 

457 

458 
 tm_of (tab, _) (Ident s) = 

459 
(case Symtab.lookup tab s of 

460 
SOME t_ty => t_ty 

42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

461 
 NONE => (case lookup_prfx prfx pfuns s of 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

462 
SOME (SOME ([], resty), t) => (t, resty) 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

463 
 _ => error ("Undeclared identifier " ^ s))) 
41561  464 

465 
 tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN) 

466 

467 
 tm_of vs (Quantifier (s, xs, ty, e)) = 

468 
let 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

469 
val (ys, vs') = mk_variables thy prfx xs ty vs; 
41561  470 
val q = (case s of 
471 
"for_all" => HOLogic.mk_all 

472 
 "for_some" => HOLogic.mk_exists) 

473 
in 

474 
(fold_rev (fn Free (x, T) => fn t => q (x, T, t)) 

475 
ys (fst (tm_of vs' e)), 

476 
booleanN) 

477 
end 

478 

479 
 tm_of vs (Funct (s, es)) = 

480 

481 
(* record field selection *) 

482 
(case try (unprefix "fld_") s of 

483 
SOME fname => (case es of 

484 
[e] => 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

485 
let 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

486 
val (t, rcdty) = tm_of vs e; 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

487 
val (rT, cmap) = mk_type' thy prfx rcdty 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

488 
in case (get_record_info thy rT, lookup types rcdty) of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

489 
(SOME {fields, ...}, SOME (Record_Type fldtys)) => 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

490 
(case (find_field cmap fname fields, 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

491 
find_field' fname fldtys) of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

492 
(SOME (fname', fT), SOME fldty) => 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

493 
(Const (fname', rT > fT) $ t, fldty) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

494 
 _ => error ("Record " ^ rcdty ^ 
41561  495 
" has no field named " ^ fname)) 
496 
 _ => error (rcdty ^ " is not a record type") 

497 
end 

498 
 _ => error ("Function " ^ s ^ " expects one argument")) 

499 
 NONE => 

500 

501 
(* record field update *) 

502 
(case try (unprefix "upf_") s of 

503 
SOME fname => (case es of 

504 
[e, e'] => 

505 
let 

506 
val (t, rcdty) = tm_of vs e; 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

507 
val (rT, cmap) = mk_type' thy prfx rcdty; 
41561  508 
val (u, fldty) = tm_of vs e'; 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

509 
val fT = mk_type thy prfx fldty 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

510 
in case get_record_info thy rT of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

511 
SOME {fields, ...} => 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

512 
(case find_field cmap fname fields of 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

513 
SOME (fname', fU) => 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

514 
if fT = fU then 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

515 
(Const (fname' ^ "_update", 
41561  516 
(fT > fT) > rT > rT) $ 
517 
Abs ("x", fT, u) $ t, 

518 
rcdty) 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

519 
else error ("Type\n" ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

520 
Syntax.string_of_typ_global thy fT ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

521 
"\ndoes not match type\n" ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

522 
Syntax.string_of_typ_global thy fU ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

523 
"\nof field " ^ fname) 
41561  524 
 NONE => error ("Record " ^ rcdty ^ 
525 
" has no field named " ^ fname)) 

526 
 _ => error (rcdty ^ " is not a record type") 

527 
end 

528 
 _ => error ("Function " ^ s ^ " expects two arguments")) 

529 
 NONE => 

530 

531 
(* enumeration type to integer *) 

532 
(case try (unsuffix "__pos") s of 

533 
SOME tyname => (case es of 

534 
[e] => (Const (@{const_name pos}, 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

535 
mk_type thy prfx tyname > HOLogic.intT) $ fst (tm_of vs e), 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

536 
integerN) 
41561  537 
 _ => error ("Function " ^ s ^ " expects one argument")) 
538 
 NONE => 

539 

540 
(* integer to enumeration type *) 

541 
(case try (unsuffix "__val") s of 

542 
SOME tyname => (case es of 

543 
[e] => (Const (@{const_name val}, 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

544 
HOLogic.intT > mk_type thy prfx tyname) $ fst (tm_of vs e), 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

545 
tyname) 
41561  546 
 _ => error ("Function " ^ s ^ " expects one argument")) 
547 
 NONE => 

548 

549 
(* successor / predecessor of enumeration type element *) 

550 
if s = "succ" orelse s = "pred" then (case es of 

551 
[e] => 

552 
let 

553 
val (t, tyname) = tm_of vs e; 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

554 
val T = mk_type thy prfx tyname 
41561  555 
in (Const 
556 
(if s = "succ" then @{const_name succ} 

557 
else @{const_name pred}, T > T) $ t, tyname) 

558 
end 

559 
 _ => error ("Function " ^ s ^ " expects one argument")) 

560 

561 
(* userdefined proof function *) 

562 
else 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

563 
(case lookup_prfx prfx pfuns s of 
41561  564 
SOME (SOME (_, resty), t) => 
565 
(list_comb (t, map (fst o tm_of vs) es), resty) 

566 
 _ => error ("Undeclared proof function " ^ s)))))) 

567 

568 
 tm_of vs (Element (e, es)) = 

569 
let val (t, ty) = tm_of vs e 

570 
in case lookup types ty of 

571 
SOME (Array_Type (_, elty)) => 

572 
(t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty) 

573 
 _ => error (ty ^ " is not an array type") 

574 
end 

575 

576 
 tm_of vs (Update (e, es, e')) = 

577 
let val (t, ty) = tm_of vs e 

578 
in case lookup types ty of 

579 
SOME (Array_Type (idxtys, elty)) => 

580 
let 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

581 
val T = foldr1 HOLogic.mk_prodT 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

582 
(map (mk_type thy prfx) idxtys); 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

583 
val U = mk_type thy prfx elty; 
41561  584 
val fT = T > U 
585 
in 

586 
(Const (@{const_name fun_upd}, fT > T > U > fT) $ 

587 
t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $ 

588 
fst (tm_of vs e'), 

589 
ty) 

590 
end 

591 
 _ => error (ty ^ " is not an array type") 

592 
end 

593 

594 
 tm_of vs (Record (s, flds)) = 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

595 
let 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

596 
val (T, cmap) = mk_type' thy prfx s; 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

597 
val {extension = (ext_name, _), fields, ...} = 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

598 
(case get_record_info thy T of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

599 
NONE => error (s ^ " is not a record type") 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

600 
 SOME info => info); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

601 
val flds' = map (apsnd (tm_of vs)) flds; 
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

602 
val fnames = fields > invert_map cmap > 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

603 
map (Long_Name.base_name o fst); 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

604 
val fnames' = map fst flds; 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

605 
val (fvals, ftys) = split_list (map (fn s' => 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

606 
case AList.lookup lcase_eq flds' s' of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

607 
SOME fval_ty => fval_ty 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

608 
 NONE => error ("Field " ^ s' ^ " missing in record " ^ s)) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

609 
fnames); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

610 
val _ = (case subtract lcase_eq fnames fnames' of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

611 
[] => () 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

612 
 xs => error ("Extra field(s) " ^ commas xs ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

613 
" in record " ^ s)); 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

614 
val _ = (case duplicates (op =) fnames' of 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

615 
[] => () 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

616 
 xs => error ("Duplicate field(s) " ^ commas xs ^ 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

617 
" in record " ^ s)) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

618 
in 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

619 
(list_comb 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

620 
(Const (ext_name, 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

621 
map (mk_type thy prfx) ftys @ [HOLogic.unitT] > T), 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

622 
fvals @ [HOLogic.unit]), 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

623 
s) 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

624 
end 
41561  625 

626 
 tm_of vs (Array (s, default, assocs)) = 

627 
(case lookup types s of 

628 
SOME (Array_Type (idxtys, elty)) => 

629 
let 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

630 
val Ts = map (mk_type thy prfx) idxtys; 
41561  631 
val T = foldr1 HOLogic.mk_prodT Ts; 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

632 
val U = mk_type thy prfx elty; 
41561  633 
fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)] 
634 
 mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost}, 

635 
T > T > HOLogic.mk_setT T) $ 

636 
fst (tm_of vs e) $ fst (tm_of vs e'); 

637 
fun mk_idx idx = 

638 
if length Ts <> length idx then 

639 
error ("Arity mismatch in construction of array " ^ s) 

640 
else foldr1 mk_times (map2 mk_idx' Ts idx); 

641 
fun mk_upd (idxs, e) t = 

642 
if length idxs = 1 andalso forall (is_none o snd) (hd idxs) 

643 
then 

644 
Const (@{const_name fun_upd}, (T > U) > 

645 
T > U > T > U) $ t $ 

646 
foldl1 HOLogic.mk_prod 

647 
(map (fst o tm_of vs o fst) (hd idxs)) $ 

648 
fst (tm_of vs e) 

649 
else 

650 
Const (@{const_name fun_upds}, (T > U) > 

651 
HOLogic.mk_setT T > U > T > U) $ t $ 

652 
foldl1 (HOLogic.mk_binop @{const_name sup}) 

653 
(map mk_idx idxs) $ 

654 
fst (tm_of vs e) 

655 
in 

656 
(fold mk_upd assocs 

657 
(case default of 

658 
SOME e => Abs ("x", T, fst (tm_of vs e)) 

659 
 NONE => Const (@{const_name undefined}, T > U)), 

660 
s) 

661 
end 

662 
 _ => error (s ^ " is not an array type")) 

663 

664 
in tm_of end; 

665 

666 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

667 
fun term_of_rule thy prfx types pfuns ids rule = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

668 
let val tm_of = fst o term_of_expr thy prfx types pfuns ids 
41561  669 
in case rule of 
670 
Inference_Rule (es, e) => Logic.list_implies 

671 
(map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e)) 

672 
 Substitution_Rule (es, e, e') => Logic.list_implies 

673 
(map (HOLogic.mk_Trueprop o tm_of) es, 

674 
HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e'))) 

675 
end; 

676 

677 

678 
val builtin = Symtab.make (map (rpair ()) 

679 
[">", "<>", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=", 

680 
"+", "", "*", "/", "div", "mod", "**"]); 

681 

682 
fun complex_expr (Number _) = false 

683 
 complex_expr (Ident _) = false 

684 
 complex_expr (Funct (s, es)) = 

685 
not (Symtab.defined builtin s) orelse exists complex_expr es 

686 
 complex_expr (Quantifier (_, _, _, e)) = complex_expr e 

687 
 complex_expr _ = true; 

688 

689 
fun complex_rule (Inference_Rule (es, e)) = 

690 
complex_expr e orelse exists complex_expr es 

691 
 complex_rule (Substitution_Rule (es, e, e')) = 

692 
complex_expr e orelse complex_expr e' orelse 

693 
exists complex_expr es; 

694 

695 
val is_pfun = 

696 
Symtab.defined builtin orf 

697 
can (unprefix "fld_") orf can (unprefix "upf_") orf 

698 
can (unsuffix "__pos") orf can (unsuffix "__val") orf 

699 
equal "succ" orf equal "pred"; 

700 

701 
fun fold_opt f = the_default I o Option.map f; 

702 
fun fold_pair f g (x, y) = f x #> g y; 

703 

704 
fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es 

705 
 fold_expr f g (Ident s) = g s 

706 
 fold_expr f g (Number _) = I 

707 
 fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e 

708 
 fold_expr f g (Element (e, es)) = 

709 
fold_expr f g e #> fold (fold_expr f g) es 

710 
 fold_expr f g (Update (e, es, e')) = 

711 
fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e' 

712 
 fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds 

713 
 fold_expr f g (Array (_, default, assocs)) = 

714 
fold_opt (fold_expr f g) default #> 

715 
fold (fold_pair 

716 
(fold (fold (fold_pair 

717 
(fold_expr f g) (fold_opt (fold_expr f g))))) 

718 
(fold_expr f g)) assocs; 

719 

42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

720 
fun add_expr_pfuns funs = fold_expr 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

721 
(fn s => if is_pfun s then I else insert (op =) s) 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

722 
(fn s => if is_none (lookup funs s) then I else insert (op =) s); 
41561  723 

724 
val add_expr_idents = fold_expr (K I) (insert (op =)); 

725 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

726 
fun pfun_type thy prfx (argtys, resty) = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

727 
map (mk_type thy prfx) argtys > mk_type thy prfx resty; 
41561  728 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

729 
fun check_pfun_type thy prfx s t optty1 optty2 = 
41561  730 
let 
731 
val T = fastype_of t; 

732 
fun check ty = 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

733 
let val U = pfun_type thy prfx ty 
41561  734 
in 
735 
T = U orelse 

736 
error ("Type\n" ^ 

737 
Syntax.string_of_typ_global thy T ^ 

738 
"\nof function " ^ 

739 
Syntax.string_of_term_global thy t ^ 

740 
" associated with proof function " ^ s ^ 

741 
"\ndoes not match declared type\n" ^ 

742 
Syntax.string_of_typ_global thy U) 

743 
end 

744 
in (Option.map check optty1; Option.map check optty2; ()) end; 

745 

746 
fun upd_option x y = if is_some x then x else y; 

747 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

748 
fun check_pfuns_types thy prfx funs = 
41561  749 
Symtab.map (fn s => fn (optty, t) => 
46567  750 
let val optty' = lookup funs (unprefix_pfun prfx s) 
41561  751 
in 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

752 
(check_pfun_type thy prfx s t optty optty'; 
41561  753 
(NONE > upd_option optty > upd_option optty', t)) 
754 
end); 

755 

756 

757 
(** the VC store **) 

758 

48167  759 
fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs); 
760 

761 
fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved." 

762 
 pp_open_vcs vcs = pp_vcs 

763 
"The following verification conditions remain to be proved:" vcs; 

764 

765 
fun partition_vcs vcs = VCtab.fold_rev 

766 
(fn (name, (trace, SOME thms, ps, cs)) => 

767 
apfst (cons (name, (trace, thms, ps, cs))) 

768 
 (name, (trace, NONE, ps, cs)) => 

769 
apsnd (cons (name, (trace, ps, cs)))) 

770 
vcs ([], []); 

771 

772 
fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]); 

773 

774 
fun print_open_vcs f vcs = 

775 
(Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs); 

41561  776 

46567  777 
fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

778 
{pfuns, type_map, env = NONE} => 
46567  779 
{pfuns = pfuns, 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

780 
type_map = type_map, 
46567  781 
env = SOME 
782 
{ctxt = ctxt, defs = defs, types = types, funs = funs, 

783 
pfuns = check_pfuns_types thy prefix funs pfuns, 

48167  784 
ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path, 
46567  785 
prefix = prefix}} 
41561  786 
 _ => err_unfinished ()) thy; 
787 

788 
fun mk_pat s = (case Int.fromString s of 

789 
SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))] 

790 
 NONE => error ("Bad conclusion identifier: C" ^ s)); 

791 

48167  792 
fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) = 
41561  793 
let val prop_of = 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

794 
HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids 
41561  795 
in 
796 
(tr, proved, 

797 
Element.Assumes (map (fn (s', e) => 

798 
((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps), 

799 
Element.Shows (map (fn (s', e) => 

48167  800 
(if name_concl then (Binding.name ("C" ^ s'), []) 
801 
else Attrib.empty_binding, 

802 
[(prop_of e, mk_pat s')])) cs)) 

41561  803 
end; 
804 

805 
fun fold_vcs f vcs = 

806 
VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs; 

807 

42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

808 
fun pfuns_of_vcs prfx funs pfuns vcs = 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

809 
fold_vcs (add_expr_pfuns funs o snd) vcs [] > 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

810 
filter (is_none o lookup_prfx prfx pfuns); 
41561  811 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

812 
fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) = 
41561  813 
let 
814 
val (fs, (tys, Ts)) = 

42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

815 
pfuns_of_vcs prfx funs pfuns vcs > 
41561  816 
map_filter (fn s => lookup funs s > 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

817 
Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) > 
41561  818 
split_list > split_list; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42499
diff
changeset

819 
val (fs', ctxt') = fold_map Name.variant fs ctxt 
41561  820 
in 
821 
(fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns, 

822 
Element.Fixes (map2 (fn s => fn T => 

823 
(Binding.name s, SOME T, NoSyn)) fs' Ts), 

824 
(tab, ctxt')) 

825 
end; 

826 

46567  827 
fun map_pfuns f {pfuns, type_map, env} = 
828 
{pfuns = f pfuns, type_map = type_map, env = env} 

829 

830 
fun map_pfuns_env f {pfuns, type_map, 

831 
env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env, 

832 
ids, proving, vcs, path, prefix}} = 

833 
if proving then err_unfinished () 

834 
else 

835 
{pfuns = pfuns, type_map = type_map, 

836 
env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs, 

837 
pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs, 

838 
path = path, prefix = prefix}}; 

839 

41561  840 
fun add_proof_fun prep (s, (optty, raw_t)) thy = 
46567  841 
VCs.map (fn data as {env, ...} => 
842 
let 

843 
val (optty', prfx, map_pf) = (case env of 

844 
SOME {funs, prefix, ...} => 

845 
(lookup funs (unprefix_pfun prefix s), 

846 
prefix, map_pfuns_env) 

847 
 NONE => (NONE, "", map_pfuns)); 

848 
val optty'' = NONE > upd_option optty > upd_option optty'; 

849 
val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t; 

850 
val _ = (case fold_aterms (fn u => 

851 
if is_Var u orelse is_Free u then insert (op =) u else I) t [] of 

852 
[] => () 

853 
 ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^ 

854 
"\nto be associated with proof function " ^ s ^ 

855 
" contains free variable(s) " ^ 

856 
commas (map (Syntax.string_of_term_global thy) ts))); 

857 
in 

858 
(check_pfun_type thy prfx s t optty optty'; 

859 
if is_some optty'' orelse is_none env then 

860 
map_pf (Symtab.update_new (s, (optty'', t))) data 

861 
handle Symtab.DUP _ => error ("Proof function " ^ s ^ 

862 
" already associated with function") 

863 
else error ("Undeclared proof function " ^ s)) 

864 
end) thy; 

41561  865 

46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

866 
fun check_mapping _ _ [] _ = () 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

867 
 check_mapping err s cmap cs = 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

868 
(case duplicates (op = o pairself fst) cmap of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

869 
[] => (case duplicates (op = o pairself snd) cmap of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

870 
[] => (case subtract (op = o apsnd snd) cs cmap of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

871 
[] => (case subtract (op = o apfst snd) cmap cs of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

872 
[] => () 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

873 
 zs => err ("has extra " ^ s ^ "(s) " ^ commas zs)) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

874 
 zs => err ("does not have " ^ s ^ "(s) " ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

875 
commas (map snd zs))) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

876 
 zs => error ("Several SPARK names are mapped to " ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

877 
commas (map snd zs))) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

878 
 zs => error ("The SPARK names " ^ commas (map fst zs) ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

879 
" are mapped to more than one name")); 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

880 

d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

881 
fun add_type (s, (T as Type (tyname, Ts), cmap)) thy = 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

882 
let val cmap' = map (apsnd (Sign.intern_const thy)) cmap 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

883 
in 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

884 
thy > 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

885 
VCs.map (fn 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

886 
{env = SOME _, ...} => err_unfinished () 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

887 
 {pfuns, type_map, env} => 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

888 
{pfuns = pfuns, 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

889 
type_map = Symtab.update_new (s, (T, cmap')) type_map, 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

890 
env = env} 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

891 
handle Symtab.DUP _ => error ("SPARK type " ^ s ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

892 
" already associated with type")) > 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

893 
(fn thy' => 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

894 
case Datatype.get_constrs thy' tyname of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

895 
NONE => (case get_record_info thy' T of 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

896 
NONE => thy' 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

897 
 SOME {fields, ...} => 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

898 
(check_mapping (assoc_ty_err thy' T s) "field" 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

899 
cmap' (map fst fields); 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

900 
thy')) 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

901 
 SOME cs => 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

902 
if null Ts then 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

903 
(map 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

904 
(fn (_, Type (_, [])) => () 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

905 
 (cname, _) => assoc_ty_err thy' T s 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

906 
("has illegal constructor " ^ 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

907 
Long_Name.base_name cname)) cs; 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

908 
check_mapping (assoc_ty_err thy' T s) "constructor" 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

909 
cmap' (map fst cs); 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

910 
add_enum_type s tyname thy') 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

911 
else assoc_ty_err thy' T s "is illegal") 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

912 
end 
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
46724
diff
changeset

913 
 add_type (s, (T, _)) thy = assoc_ty_err thy T s "is illegal"; 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

914 

41561  915 
val is_closed = is_none o #env o VCs.get; 
916 

48167  917 
fun lookup_vc thy name_concl name = 
41561  918 
(case VCs.get thy of 
46567  919 
{env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} => 
41561  920 
(case VCtab.lookup vcs name of 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

921 
SOME vc => 
41561  922 
let val (pfuns', ctxt', ids') = 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

923 
declare_missing_pfuns thy prefix funs pfuns vcs ids 
48167  924 
in 
925 
SOME (ctxt @ [ctxt'], 

926 
mk_vc thy prefix types pfuns' ids' name_concl vc) 

927 
end 

41561  928 
 NONE => NONE) 
929 
 _ => NONE); 

930 

48167  931 
fun get_vcs thy name_concl = (case VCs.get thy of 
46567  932 
{env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} => 
41561  933 
let val (pfuns', ctxt', ids') = 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

934 
declare_missing_pfuns thy prefix funs pfuns vcs ids 
41561  935 
in 
936 
(ctxt @ [ctxt'], defs, 

937 
VCtab.dest vcs > 

48167  938 
map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl))) 
41561  939 
end 
940 
 _ => ([], [], [])); 

941 

41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41878
diff
changeset

942 
fun mark_proved name thms = VCs.map (fn 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

943 
{pfuns, type_map, 
46567  944 
env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env, 
945 
ids, vcs, path, prefix, ...}} => 

41561  946 
{pfuns = pfuns, 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

947 
type_map = type_map, 
41561  948 
env = SOME {ctxt = ctxt, defs = defs, 
46567  949 
types = types, funs = funs, pfuns = pfuns_env, 
950 
ids = ids, 

41561  951 
proving = true, 
48167  952 
vcs = print_open_vcs insert_break (VCtab.map_entry name 
953 
(fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs), 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

954 
path = path, 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

955 
prefix = prefix}} 
41561  956 
 x => x); 
957 

48167  958 
fun close incomplete thy = 
42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

959 
thy > 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

960 
VCs.map (fn 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

961 
{pfuns, type_map, env = SOME {vcs, path, ...}} => 
48167  962 
let 
963 
val (proved, unproved) = partition_vcs vcs; 

964 
val _ = Thm.join_proofs (maps (#2 o snd) proved); 

965 
val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) => 

966 
exists (#oracle o Thm.status_of) thms) proved 

967 
in 

968 
(if null unproved then () 

969 
else (if incomplete then warning else error) 

970 
(Pretty.string_of (pp_open_vcs unproved)); 

971 
if null proved' then () 

972 
else warning (Pretty.string_of (pp_vcs 

973 
"The following VCs are not marked as proved \ 

974 
\because their proofs contain oracles:" proved')); 

975 
File.write (Path.ext "prv" path) 

976 
(implode (map (fn (s, _) => snd (strip_number s) ^ 

977 
"  proved by " ^ Distribution.version ^ "\n") proved'')); 

978 
{pfuns = pfuns, type_map = type_map, env = NONE}) 

979 
end 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

980 
 _ => error "No SPARK environment is currently open") > 
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

981 
Sign.parent_path; 
41561  982 

983 

984 
(** set up verification conditions **) 

985 

986 
fun partition_opt f = 

987 
let 

988 
fun part ys zs [] = (rev ys, rev zs) 

989 
 part ys zs (x :: xs) = (case f x of 

990 
SOME y => part (y :: ys) zs xs 

991 
 NONE => part ys (x :: zs) xs) 

992 
in part [] [] end; 

993 

994 
fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs)) 

995 
 dest_def _ = NONE; 

996 

997 
fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i); 

998 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

999 
fun add_const prfx (s, ty) ((tab, ctxt), thy) = 
41561  1000 
let 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1001 
val T = mk_type thy prfx ty; 
41561  1002 
val b = Binding.name s; 
1003 
val c = Const (Sign.full_name thy b, T) 

1004 
in 

1005 
(c, 

1006 
((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt), 

1007 
Sign.add_consts_i [(b, T, NoSyn)] thy)) 

1008 
end; 

1009 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1010 
fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) = 
41561  1011 
(case lookup consts s of 
1012 
SOME ty => 

1013 
let 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1014 
val (t, ty') = term_of_expr thy prfx types pfuns ids e; 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1015 
val T = mk_type thy prfx ty; 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1016 
val T' = mk_type thy prfx ty'; 
41878
0778ade00b06
 Made sure that sort_defs is aware of constants introduced by add_type_def
berghofe
parents:
41635
diff
changeset

1017 
val _ = T = T' orelse 
41561  1018 
error ("Declared type " ^ ty ^ " of " ^ s ^ 
1019 
"\ndoes not match type " ^ ty' ^ " in definition"); 

1020 
val id' = mk_rulename id; 

1021 
val lthy = Named_Target.theory_init thy; 

1022 
val ((t', (_, th)), lthy') = Specification.definition 

1023 
(NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq 

41878
0778ade00b06
 Made sure that sort_defs is aware of constants introduced by add_type_def
berghofe
parents:
41635
diff
changeset

1024 
(Free (s, T), t)))) lthy; 
42361  1025 
val phi = Proof_Context.export_morphism lthy' lthy 
41561  1026 
in 
1027 
((id', Morphism.thm phi th), 

1028 
((Symtab.update (s, (Morphism.term phi t', ty)) tab, 

1029 
Name.declare s ctxt), 

1030 
Local_Theory.exit_global lthy')) 

1031 
end 

1032 
 NONE => error ("Undeclared constant " ^ s)); 

1033 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1034 
fun add_var prfx (s, ty) (ids, thy) = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1035 
let val ([Free p], ids') = mk_variables thy prfx [s] ty ids 
41561  1036 
in (p, (ids', thy)) end; 
1037 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1038 
fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) = 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1039 
fold_map (add_var prfx) 
41561  1040 
(map_filter 
1041 
(fn s => case try (unsuffix "~") s of 

1042 
SOME s' => (case Symtab.lookup tab s' of 

1043 
SOME (_, ty) => SOME (s, ty) 

1044 
 NONE => error ("Undeclared identifier " ^ s')) 

1045 
 NONE => NONE) 

1046 
(fold_vcs (add_expr_idents o snd) vcs [])) 

1047 
ids_thy; 

1048 

1049 
fun is_trivial_vc ([], [(_, Ident "true")]) = true 

1050 
 is_trivial_vc _ = false; 

1051 

1052 
fun rulenames rules = commas 

1053 
(map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules); 

1054 

1055 
(* sort definitions according to their dependency *) 

42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1056 
fun sort_defs _ _ _ _ [] sdefs = rev sdefs 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1057 
 sort_defs prfx funs pfuns consts defs sdefs = 
41561  1058 
(case find_first (fn (_, (_, e)) => 
42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1059 
forall (is_some o lookup_prfx prfx pfuns) 
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1060 
(add_expr_pfuns funs e []) andalso 
41561  1061 
forall (fn id => 
1062 
member (fn (s, (_, (s', _))) => s = s') sdefs id orelse 

41878
0778ade00b06
 Made sure that sort_defs is aware of constants introduced by add_type_def
berghofe
parents:
41635
diff
changeset

1063 
consts id) 
41561  1064 
(add_expr_idents e [])) defs of 
42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1065 
SOME d => sort_defs prfx funs pfuns consts 
41561  1066 
(remove (op =) d defs) (d :: sdefs) 
1067 
 NONE => error ("Bad definitions: " ^ rulenames defs)); 

1068 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

1069 
fun set_vcs ({types, vars, consts, funs} : decls) 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1070 
(rules, _) ((_, ident), vcs) path prfx thy = 
41561  1071 
let 
1072 
val {pfuns, ...} = VCs.get thy; 

41878
0778ade00b06
 Made sure that sort_defs is aware of constants introduced by add_type_def
berghofe
parents:
41635
diff
changeset

1073 
val (defs, rules') = partition_opt dest_def rules; 
41561  1074 
val consts' = 
41878
0778ade00b06
 Made sure that sort_defs is aware of constants introduced by add_type_def
berghofe
parents:
41635
diff
changeset

1075 
subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts); 
41561  1076 
(* ignore all complex rules in rls files *) 
1077 
val (rules'', other_rules) = 

1078 
List.partition (complex_rule o snd) rules'; 

1079 
val _ = if null rules'' then () 

1080 
else warning ("Ignoring rules: " ^ rulenames rules''); 

1081 

1082 
val vcs' = VCtab.make (maps (fn (tr, vcs) => 

41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41878
diff
changeset

1083 
map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs))) 
41561  1084 
(filter_out (is_trivial_vc o snd) vcs)) vcs); 
1085 

1086 
val _ = (case filter_out (is_some o lookup funs) 

42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1087 
(pfuns_of_vcs prfx funs pfuns vcs') of 
41561  1088 
[] => () 
1089 
 fs => error ("Undeclared proof function(s) " ^ commas fs)); 

1090 

1091 
val (((defs', vars''), ivars), (ids, thy')) = 

1092 
((Symtab.empty > 

45740  1093 
Symtab.update ("false", (@{term False}, booleanN)) > 
1094 
Symtab.update ("true", (@{term True}, booleanN)), 

42356
e8777e3ea6ef
Added command for associating userdefined types with SPARK types.
berghofe
parents:
41896
diff
changeset

1095 
Name.context), 
46724
5759ecd5c905
Use long prefix rather than short package name to disambiguate constant names
berghofe
parents:
46567
diff
changeset

1096 
thy > Sign.add_path 
47880
7e202f71a249
Fixed disambiguation of names (cf. 5759ecd5c905)
berghofe
parents:
46725
diff
changeset

1097 
((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) > 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1098 
fold (add_type_def prfx) (items types) > 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1099 
fold (snd oo add_const prfx) consts' > (fn ids_thy as ((tab, _), _) => 
41878
0778ade00b06
 Made sure that sort_defs is aware of constants introduced by add_type_def
berghofe
parents:
41635
diff
changeset

1100 
ids_thy > 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1101 
fold_map (add_def prfx types pfuns consts) 
42499
adfa6ad43ab6
Properly treat proof functions with no arguments.
berghofe
parents:
42440
diff
changeset

1102 
(sort_defs prfx funs pfuns (Symtab.defined tab) defs []) >> 
42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1103 
fold_map (add_var prfx) (items vars) >> 
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1104 
add_init_vars prfx vcs'); 
41561  1105 

1106 
val ctxt = 

1107 
[Element.Fixes (map (fn (s, T) => 

1108 
(Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)), 

1109 
Element.Assumes (map (fn (id, rl) => 

1110 
((mk_rulename id, []), 

42396
0869ce2006eb
Package prefix is now taken into account when looking up userdefined
berghofe
parents:
42361
diff
changeset

1111 
[(term_of_rule thy' prfx types pfuns ids rl, [])])) 
41561  1112 
other_rules), 
42440
5e7a7343ab11
discontinuend obsolete Thm.definitionK, which was hardly ever welldefined;
wenzelm
parents:
42416
diff
changeset

1113 
Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])] 
41561  1114 

1115 
in 

46567  1116 
set_env ctxt defs' types funs ids vcs' path prfx thy' 
41561  1117 
end; 
1118 

1119 
end; 