1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Apr 14 15:04:42 2011 +0200
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Apr 15 15:33:57 2011 +0200
1.3 @@ -7,11 +7,12 @@
1.4
1.5 signature SPARK_VCS =
1.6 sig
1.7 - val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> Fdl_Parser.vcs ->
1.8 - Path.T -> theory -> theory
1.9 + val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
1.10 + (string * string) * Fdl_Parser.vcs -> Path.T -> theory -> theory
1.11 val add_proof_fun: (typ option -> 'a -> term) ->
1.12 string * ((string list * string) option * 'a) ->
1.13 theory -> theory
1.14 + val add_type: string * typ -> theory -> theory
1.15 val lookup_vc: theory -> string -> (Element.context_i list *
1.16 (string * thm list option * Element.context_i * Element.statement_i)) option
1.17 val get_vcs: theory ->
1.18 @@ -28,8 +29,49 @@
1.19 open Fdl_Parser;
1.20
1.21
1.22 +(** theory data **)
1.23 +
1.24 +fun err_unfinished () = error "An unfinished SPARK environment is still open."
1.25 +
1.26 +val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
1.27 +
1.28 +val name_ord = prod_ord string_ord (option_ord int_ord) o
1.29 + pairself (strip_number ##> Int.fromString);
1.30 +
1.31 +structure VCtab = Table(type key = string val ord = name_ord);
1.32 +
1.33 +structure VCs = Theory_Data
1.34 +(
1.35 + type T =
1.36 + {pfuns: ((string list * string) option * term) Symtab.table,
1.37 + type_map: typ Symtab.table,
1.38 + env:
1.39 + {ctxt: Element.context_i list,
1.40 + defs: (binding * thm) list,
1.41 + types: fdl_type tab,
1.42 + funs: (string list * string) tab,
1.43 + ids: (term * string) Symtab.table * Name.context,
1.44 + proving: bool,
1.45 + vcs: (string * thm list option *
1.46 + (string * expr) list * (string * expr) list) VCtab.table,
1.47 + path: Path.T} option}
1.48 + val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
1.49 + val extend = I
1.50 + fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
1.51 + {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
1.52 + {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
1.53 + type_map = Symtab.merge (op =) (type_map1, type_map2),
1.54 + env = NONE}
1.55 + | merge _ = err_unfinished ()
1.56 +)
1.57 +
1.58 +
1.59 (** utilities **)
1.60
1.61 +val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
1.62 +
1.63 +val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name);
1.64 +
1.65 fun mk_unop s t =
1.66 let val T = fastype_of t
1.67 in Const (s, T --> T) $ t end;
1.68 @@ -44,17 +86,22 @@
1.69 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
1.70 end;
1.71
1.72 +fun get_type thy ty =
1.73 + let val {type_map, ...} = VCs.get thy
1.74 + in Symtab.lookup type_map ty end;
1.75 +
1.76 fun mk_type _ "integer" = HOLogic.intT
1.77 | mk_type _ "boolean" = HOLogic.boolT
1.78 - | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy)
1.79 - (Type (Sign.full_name thy (Binding.name ty), []));
1.80 + | mk_type thy ty =
1.81 + (case get_type thy ty of
1.82 + NONE =>
1.83 + Syntax.check_typ (ProofContext.init_global thy)
1.84 + (Type (Sign.full_name thy (Binding.name ty), []))
1.85 + | SOME T => T);
1.86
1.87 val booleanN = "boolean";
1.88 val integerN = "integer";
1.89
1.90 -fun mk_qual_name thy s s' =
1.91 - Sign.full_name thy (Binding.qualify true s (Binding.name s'));
1.92 -
1.93 fun define_overloaded (def_name, eq) lthy =
1.94 let
1.95 val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
1.96 @@ -80,17 +127,29 @@
1.97 val zs = map (Free o rpair T) ys;
1.98 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
1.99
1.100 +fun get_record_info thy T = (case Record.dest_recTs T of
1.101 + [(tyname, [@{typ unit}])] =>
1.102 + Record.get_info thy (Long_Name.qualifier tyname)
1.103 + | _ => NONE);
1.104 +
1.105 +fun find_field fname = find_first (curry lcase_eq fname o fst);
1.106 +
1.107 +fun find_field' fname = get_first (fn (flds, fldty) =>
1.108 + if member (op =) flds fname then SOME fldty else NONE);
1.109 +
1.110 +fun assoc_ty_err thy T s msg =
1.111 + error ("Type " ^ Syntax.string_of_typ_global thy T ^
1.112 + " associated with SPARK type " ^ s ^ "\n" ^ msg);
1.113 +
1.114
1.115 (** generate properties of enumeration types **)
1.116
1.117 -fun add_enum_type tyname els (tab, ctxt) thy =
1.118 +fun add_enum_type tyname tyname' thy =
1.119 let
1.120 - val tyb = Binding.name tyname;
1.121 - val tyname' = Sign.full_name thy tyb;
1.122 + val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
1.123 + val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
1.124 + val k = length cs;
1.125 val T = Type (tyname', []);
1.126 - val case_name = mk_qual_name thy tyname (tyname ^ "_case");
1.127 - val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els;
1.128 - val k = length els;
1.129 val p = Const (@{const_name pos}, T --> HOLogic.intT);
1.130 val v = Const (@{const_name val}, HOLogic.intT --> T);
1.131 val card = Const (@{const_name card},
1.132 @@ -103,9 +162,6 @@
1.133 (f $ Bound 1) $ (f $ Bound 0))));
1.134
1.135 val (((def1, def2), def3), lthy) = thy |>
1.136 - Datatype.add_datatype {strict = true, quiet = true} [tyname]
1.137 - [([], tyb, NoSyn,
1.138 - map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
1.139
1.140 Class.instantiation ([tyname'], [], @{sort enum}) |>
1.141
1.142 @@ -195,46 +251,107 @@
1.143 val simp_att = [Attrib.internal (K Simplifier.simp_add)]
1.144
1.145 in
1.146 - ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab,
1.147 - fold Name.declare els ctxt),
1.148 - lthy' |>
1.149 - Local_Theory.note
1.150 - ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
1.151 - Local_Theory.note
1.152 - ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
1.153 - Local_Theory.note
1.154 - ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
1.155 - Local_Theory.note
1.156 - ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
1.157 - Local_Theory.note
1.158 - ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
1.159 - Local_Theory.exit_global)
1.160 + lthy' |>
1.161 + Local_Theory.note
1.162 + ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
1.163 + Local_Theory.note
1.164 + ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
1.165 + Local_Theory.note
1.166 + ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
1.167 + Local_Theory.note
1.168 + ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
1.169 + Local_Theory.note
1.170 + ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
1.171 + Local_Theory.exit_global
1.172 end;
1.173
1.174
1.175 +fun check_no_assoc thy s = case get_type thy s of
1.176 + NONE => ()
1.177 + | SOME _ => error ("Cannot associate a type with " ^ s ^
1.178 + "\nsince it is no record or enumeration type");
1.179 +
1.180 +fun check_enum [] [] = NONE
1.181 + | check_enum els [] = SOME ("has no element(s) " ^ commas els)
1.182 + | check_enum [] cs = SOME ("has extra element(s) " ^
1.183 + commas (map (Long_Name.base_name o fst) cs))
1.184 + | check_enum (el :: els) ((cname, _) :: cs) =
1.185 + if lcase_eq (el, cname) then check_enum els cs
1.186 + else SOME ("either has no element " ^ el ^
1.187 + " or it is at the wrong position");
1.188 +
1.189 fun add_type_def (s, Basic_Type ty) (ids, thy) =
1.190 - (ids,
1.191 - Typedecl.abbrev_global (Binding.name s, [], NoSyn)
1.192 - (mk_type thy ty) thy |> snd)
1.193 + (check_no_assoc thy s;
1.194 + (ids,
1.195 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
1.196 + (mk_type thy ty) thy |> snd))
1.197
1.198 - | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy
1.199 + | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) =
1.200 + let
1.201 + val (thy', tyname) = (case get_type thy s of
1.202 + NONE =>
1.203 + let
1.204 + val tyb = Binding.name s;
1.205 + val tyname = Sign.full_name thy tyb
1.206 + in
1.207 + (thy |>
1.208 + Datatype.add_datatype {strict = true, quiet = true} [s]
1.209 + [([], tyb, NoSyn,
1.210 + map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
1.211 + add_enum_type s tyname,
1.212 + tyname)
1.213 + end
1.214 + | SOME (T as Type (tyname, [])) =>
1.215 + (case Datatype_Data.get_constrs thy tyname of
1.216 + NONE => assoc_ty_err thy T s "is not a datatype"
1.217 + | SOME cs => (case check_enum els cs of
1.218 + NONE => (thy, tyname)
1.219 + | SOME msg => assoc_ty_err thy T s msg)));
1.220 + val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
1.221 + in
1.222 + ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
1.223 + fold Name.declare els ctxt),
1.224 + thy')
1.225 + end
1.226
1.227 | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =
1.228 - (ids,
1.229 - Typedecl.abbrev_global (Binding.name s, [], NoSyn)
1.230 - (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
1.231 - mk_type thy resty) thy |> snd)
1.232 + (check_no_assoc thy s;
1.233 + (ids,
1.234 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
1.235 + (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
1.236 + mk_type thy resty) thy |> snd))
1.237
1.238 | add_type_def (s, Record_Type fldtys) (ids, thy) =
1.239 (ids,
1.240 - Record.add_record true ([], Binding.name s) NONE
1.241 - (maps (fn (flds, ty) =>
1.242 - let val T = mk_type thy ty
1.243 - in map (fn fld => (Binding.name fld, T, NoSyn)) flds
1.244 - end) fldtys) thy)
1.245 + let val fldTs = maps (fn (flds, ty) =>
1.246 + map (rpair (mk_type thy ty)) flds) fldtys
1.247 + in case get_type thy s of
1.248 + NONE =>
1.249 + Record.add_record true ([], Binding.name s) NONE
1.250 + (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
1.251 + | SOME rT =>
1.252 + (case get_record_info thy rT of
1.253 + NONE => assoc_ty_err thy rT s "is not a record type"
1.254 + | SOME {fields, ...} =>
1.255 + (case subtract (lcase_eq o pairself fst) fldTs fields of
1.256 + [] => ()
1.257 + | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
1.258 + commas (map (Long_Name.base_name o fst) flds));
1.259 + map (fn (fld, T) =>
1.260 + case AList.lookup lcase_eq fields fld of
1.261 + NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
1.262 + | SOME U => T = U orelse assoc_ty_err thy rT s
1.263 + ("has field " ^
1.264 + fld ^ " whose type\n" ^
1.265 + Syntax.string_of_typ_global thy U ^
1.266 + "\ndoes not match declared type\n" ^
1.267 + Syntax.string_of_typ_global thy T)) fldTs;
1.268 + thy))
1.269 + end)
1.270
1.271 | add_type_def (s, Pending_Type) (ids, thy) =
1.272 - (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd);
1.273 + (check_no_assoc thy s;
1.274 + (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
1.275
1.276
1.277 fun term_of_expr thy types funs pfuns =
1.278 @@ -323,17 +440,16 @@
1.279 (case try (unprefix "fld_") s of
1.280 SOME fname => (case es of
1.281 [e] =>
1.282 - let val (t, rcdty) = tm_of vs e
1.283 - in case lookup types rcdty of
1.284 - SOME (Record_Type fldtys) =>
1.285 - (case get_first (fn (flds, fldty) =>
1.286 - if member (op =) flds fname then SOME fldty
1.287 - else NONE) fldtys of
1.288 - SOME fldty =>
1.289 - (Const (mk_qual_name thy rcdty fname,
1.290 - mk_type thy rcdty --> mk_type thy fldty) $ t,
1.291 - fldty)
1.292 - | NONE => error ("Record " ^ rcdty ^
1.293 + let
1.294 + val (t, rcdty) = tm_of vs e;
1.295 + val rT = mk_type thy rcdty
1.296 + in case (get_record_info thy rT, lookup types rcdty) of
1.297 + (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
1.298 + (case (find_field fname fields,
1.299 + find_field' fname fldtys) of
1.300 + (SOME (fname', fT), SOME fldty) =>
1.301 + (Const (fname', rT --> fT) $ t, fldty)
1.302 + | _ => error ("Record " ^ rcdty ^
1.303 " has no field named " ^ fname))
1.304 | _ => error (rcdty ^ " is not a record type")
1.305 end
1.306 @@ -349,20 +465,20 @@
1.307 val rT = mk_type thy rcdty;
1.308 val (u, fldty) = tm_of vs e';
1.309 val fT = mk_type thy fldty
1.310 - in case lookup types rcdty of
1.311 - SOME (Record_Type fldtys) =>
1.312 - (case get_first (fn (flds, fldty) =>
1.313 - if member (op =) flds fname then SOME fldty
1.314 - else NONE) fldtys of
1.315 - SOME fldty' =>
1.316 - if fldty = fldty' then
1.317 - (Const (mk_qual_name thy rcdty (fname ^ "_update"),
1.318 + in case get_record_info thy rT of
1.319 + SOME {fields, ...} =>
1.320 + (case find_field fname fields of
1.321 + SOME (fname', fU) =>
1.322 + if fT = fU then
1.323 + (Const (fname' ^ "_update",
1.324 (fT --> fT) --> rT --> rT) $
1.325 Abs ("x", fT, u) $ t,
1.326 rcdty)
1.327 - else error ("Type " ^ fldty ^
1.328 - " does not match type " ^ fldty' ^ " of field " ^
1.329 - fname)
1.330 + else error ("Type\n" ^
1.331 + Syntax.string_of_typ_global thy fT ^
1.332 + "\ndoes not match type\n" ^
1.333 + Syntax.string_of_typ_global thy fU ^
1.334 + "\nof field " ^ fname)
1.335 | NONE => error ("Record " ^ rcdty ^
1.336 " has no field named " ^ fname))
1.337 | _ => error (rcdty ^ " is not a record type")
1.338 @@ -431,34 +547,35 @@
1.339 end
1.340
1.341 | tm_of vs (Record (s, flds)) =
1.342 - (case lookup types s of
1.343 - SOME (Record_Type fldtys) =>
1.344 - let
1.345 - val flds' = map (apsnd (tm_of vs)) flds;
1.346 - val fnames = maps fst fldtys;
1.347 - val fnames' = map fst flds;
1.348 - val (fvals, ftys) = split_list (map (fn s' =>
1.349 - case AList.lookup (op =) flds' s' of
1.350 - SOME fval_ty => fval_ty
1.351 - | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
1.352 - fnames);
1.353 - val _ = (case subtract (op =) fnames fnames' of
1.354 - [] => ()
1.355 - | xs => error ("Extra field(s) " ^ commas xs ^
1.356 - " in record " ^ s));
1.357 - val _ = (case duplicates (op =) fnames' of
1.358 - [] => ()
1.359 - | xs => error ("Duplicate field(s) " ^ commas xs ^
1.360 - " in record " ^ s))
1.361 - in
1.362 - (list_comb
1.363 - (Const (mk_qual_name thy s (s ^ "_ext"),
1.364 - map (mk_type thy) ftys @ [HOLogic.unitT] --->
1.365 - mk_type thy s),
1.366 - fvals @ [HOLogic.unit]),
1.367 - s)
1.368 - end
1.369 - | _ => error (s ^ " is not a record type"))
1.370 + let
1.371 + val T = mk_type thy s;
1.372 + val {extension = (ext_name, _), fields, ...} =
1.373 + (case get_record_info thy T of
1.374 + NONE => error (s ^ " is not a record type")
1.375 + | SOME info => info);
1.376 + val flds' = map (apsnd (tm_of vs)) flds;
1.377 + val fnames = map (Long_Name.base_name o fst) fields;
1.378 + val fnames' = map fst flds;
1.379 + val (fvals, ftys) = split_list (map (fn s' =>
1.380 + case AList.lookup lcase_eq flds' s' of
1.381 + SOME fval_ty => fval_ty
1.382 + | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
1.383 + fnames);
1.384 + val _ = (case subtract lcase_eq fnames fnames' of
1.385 + [] => ()
1.386 + | xs => error ("Extra field(s) " ^ commas xs ^
1.387 + " in record " ^ s));
1.388 + val _ = (case duplicates (op =) fnames' of
1.389 + [] => ()
1.390 + | xs => error ("Duplicate field(s) " ^ commas xs ^
1.391 + " in record " ^ s))
1.392 + in
1.393 + (list_comb
1.394 + (Const (ext_name,
1.395 + map (mk_type thy) ftys @ [HOLogic.unitT] ---> T),
1.396 + fvals @ [HOLogic.unit]),
1.397 + s)
1.398 + end
1.399
1.400 | tm_of vs (Array (s, default, assocs)) =
1.401 (case lookup types s of
1.402 @@ -592,44 +709,15 @@
1.403
1.404 (** the VC store **)
1.405
1.406 -fun err_unfinished () = error "An unfinished SPARK environment is still open."
1.407 -
1.408 fun err_vcs names = error (Pretty.string_of
1.409 (Pretty.big_list "The following verification conditions have not been proved:"
1.410 (map Pretty.str names)))
1.411
1.412 -val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
1.413 -
1.414 -val name_ord = prod_ord string_ord (option_ord int_ord) o
1.415 - pairself (strip_number ##> Int.fromString);
1.416 -
1.417 -structure VCtab = Table(type key = string val ord = name_ord);
1.418 -
1.419 -structure VCs = Theory_Data
1.420 -(
1.421 - type T =
1.422 - {pfuns: ((string list * string) option * term) Symtab.table,
1.423 - env:
1.424 - {ctxt: Element.context_i list,
1.425 - defs: (binding * thm) list,
1.426 - types: fdl_type tab,
1.427 - funs: (string list * string) tab,
1.428 - ids: (term * string) Symtab.table * Name.context,
1.429 - proving: bool,
1.430 - vcs: (string * thm list option *
1.431 - (string * expr) list * (string * expr) list) VCtab.table,
1.432 - path: Path.T} option}
1.433 - val empty : T = {pfuns = Symtab.empty, env = NONE}
1.434 - val extend = I
1.435 - fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) =
1.436 - {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
1.437 - env = NONE}
1.438 - | merge _ = err_unfinished ()
1.439 -)
1.440 -
1.441 fun set_env (env as {funs, ...}) thy = VCs.map (fn
1.442 - {pfuns, env = NONE} =>
1.443 - {pfuns = check_pfuns_types thy funs pfuns, env = SOME env}
1.444 + {pfuns, type_map, env = NONE} =>
1.445 + {pfuns = check_pfuns_types thy funs pfuns,
1.446 + type_map = type_map,
1.447 + env = SOME env}
1.448 | _ => err_unfinished ()) thy;
1.449
1.450 fun mk_pat s = (case Int.fromString s of
1.451 @@ -672,28 +760,60 @@
1.452 fun add_proof_fun prep (s, (optty, raw_t)) thy =
1.453 VCs.map (fn
1.454 {env = SOME {proving = true, ...}, ...} => err_unfinished ()
1.455 - | {pfuns, env} =>
1.456 + | {pfuns, type_map, env} =>
1.457 let
1.458 val optty' = (case env of
1.459 SOME {funs, ...} => lookup funs s
1.460 | NONE => NONE);
1.461 val optty'' = NONE |> upd_option optty |> upd_option optty';
1.462 - val t = prep (Option.map (pfun_type thy) optty'') raw_t
1.463 + val t = prep (Option.map (pfun_type thy) optty'') raw_t;
1.464 + val _ = (case fold_aterms (fn u =>
1.465 + if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
1.466 + [] => ()
1.467 + | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
1.468 + "\nto be associated with proof function " ^ s ^
1.469 + " contains free variable(s) " ^
1.470 + commas (map (Syntax.string_of_term_global thy) ts)));
1.471 in
1.472 (check_pfun_type thy s t optty optty';
1.473 if is_some optty'' orelse is_none env then
1.474 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
1.475 + type_map = type_map,
1.476 env = env}
1.477 handle Symtab.DUP _ => error ("Proof function " ^ s ^
1.478 " already associated with function")
1.479 else error ("Undeclared proof function " ^ s))
1.480 end) thy;
1.481
1.482 +fun add_type (s, T as Type (tyname, Ts)) thy =
1.483 + thy |>
1.484 + VCs.map (fn
1.485 + {env = SOME _, ...} => err_unfinished ()
1.486 + | {pfuns, type_map, env} =>
1.487 + {pfuns = pfuns,
1.488 + type_map = Symtab.update_new (s, T) type_map,
1.489 + env = env}
1.490 + handle Symtab.DUP _ => error ("SPARK type " ^ s ^
1.491 + " already associated with type")) |>
1.492 + (fn thy' =>
1.493 + case Datatype_Data.get_constrs thy' tyname of
1.494 + NONE => thy'
1.495 + | SOME cs =>
1.496 + if null Ts then
1.497 + (map
1.498 + (fn (_, Type (_, [])) => ()
1.499 + | (cname, _) => assoc_ty_err thy T s
1.500 + ("has illegal constructor " ^
1.501 + Long_Name.base_name cname)) cs;
1.502 + add_enum_type s tyname thy')
1.503 + else assoc_ty_err thy T s "is illegal")
1.504 + | add_type (s, T) thy = assoc_ty_err thy T s "is illegal";
1.505 +
1.506 val is_closed = is_none o #env o VCs.get;
1.507
1.508 fun lookup_vc thy name =
1.509 (case VCs.get thy of
1.510 - {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} =>
1.511 + {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} =>
1.512 (case VCtab.lookup vcs name of
1.513 SOME vc =>
1.514 let val (pfuns', ctxt', ids') =
1.515 @@ -703,7 +823,7 @@
1.516 | _ => NONE);
1.517
1.518 fun get_vcs thy = (case VCs.get thy of
1.519 - {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} =>
1.520 + {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} =>
1.521 let val (pfuns', ctxt', ids') =
1.522 declare_missing_pfuns thy funs pfuns vcs ids
1.523 in
1.524 @@ -714,8 +834,10 @@
1.525 | _ => ([], [], []));
1.526
1.527 fun mark_proved name thms = VCs.map (fn
1.528 - {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
1.529 + {pfuns, type_map,
1.530 + env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
1.531 {pfuns = pfuns,
1.532 + type_map = type_map,
1.533 env = SOME {ctxt = ctxt, defs = defs,
1.534 types = types, funs = funs, ids = ids,
1.535 proving = true,
1.536 @@ -724,18 +846,21 @@
1.537 path = path}}
1.538 | x => x);
1.539
1.540 -fun close thy = VCs.map (fn
1.541 - {pfuns, env = SOME {vcs, path, ...}} =>
1.542 - (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
1.543 - (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
1.544 - (proved, []) =>
1.545 - (Thm.join_proofs (maps (the o #2 o snd) proved);
1.546 - File.write (Path.ext "prv" path)
1.547 - (concat (map (fn (s, _) => snd (strip_number s) ^
1.548 - " -- proved by " ^ Distribution.version ^ "\n") proved));
1.549 - {pfuns = pfuns, env = NONE})
1.550 - | (_, unproved) => err_vcs (map fst unproved))
1.551 - | x => x) thy;
1.552 +fun close thy =
1.553 + thy |>
1.554 + VCs.map (fn
1.555 + {pfuns, type_map, env = SOME {vcs, path, ...}} =>
1.556 + (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
1.557 + (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
1.558 + (proved, []) =>
1.559 + (Thm.join_proofs (maps (the o #2 o snd) proved);
1.560 + File.write (Path.ext "prv" path)
1.561 + (concat (map (fn (s, _) => snd (strip_number s) ^
1.562 + " -- proved by " ^ Distribution.version ^ "\n") proved));
1.563 + {pfuns = pfuns, type_map = type_map, env = NONE})
1.564 + | (_, unproved) => err_vcs (map fst unproved))
1.565 + | _ => error "No SPARK environment is currently open") |>
1.566 + Sign.parent_path;
1.567
1.568
1.569 (** set up verification conditions **)
1.570 @@ -822,7 +947,8 @@
1.571 (remove (op =) d defs) (d :: sdefs)
1.572 | NONE => error ("Bad definitions: " ^ rulenames defs));
1.573
1.574 -fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy =
1.575 +fun set_vcs ({types, vars, consts, funs} : decls)
1.576 + (rules, _) ((_, ident), vcs) path thy =
1.577 let
1.578 val {pfuns, ...} = VCs.get thy;
1.579 val (defs, rules') = partition_opt dest_def rules;
1.580 @@ -847,7 +973,8 @@
1.581 ((Symtab.empty |>
1.582 Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
1.583 Symtab.update ("true", (HOLogic.true_const, booleanN)),
1.584 - Name.context), thy) |>
1.585 + Name.context),
1.586 + thy |> Sign.add_path (Long_Name.base_name ident)) |>
1.587 fold add_type_def (items types) |>
1.588 fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) =>
1.589 ids_thy |>