1.1 --- a/etc/isar-keywords.el Thu Apr 14 15:04:42 2011 +0200
1.2 +++ b/etc/isar-keywords.el Fri Apr 15 15:33:57 2011 +0200
1.3 @@ -227,6 +227,7 @@
1.4 "spark_open"
1.5 "spark_proof_functions"
1.6 "spark_status"
1.7 + "spark_types"
1.8 "spark_vc"
1.9 "specification"
1.10 "statespace"
1.11 @@ -520,6 +521,7 @@
1.12 "spark_end"
1.13 "spark_open"
1.14 "spark_proof_functions"
1.15 + "spark_types"
1.16 "statespace"
1.17 "syntax"
1.18 "syntax_declaration"
2.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Apr 14 15:04:42 2011 +0200
2.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Apr 15 15:33:57 2011 +0200
2.3 @@ -27,7 +27,7 @@
2.4 SPARK_VCs.set_vcs
2.5 (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
2.6 (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
2.7 - (snd (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path))))
2.8 + (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))
2.9 base thy
2.10 end;
2.11
2.12 @@ -39,6 +39,9 @@
2.13 Syntax.check_term ctxt) pf thy
2.14 end;
2.15
2.16 +fun add_spark_type_cmd (s, raw_typ) thy =
2.17 + SPARK_VCs.add_type (s, Syntax.read_typ_global thy raw_typ) thy;
2.18 +
2.19 fun get_vc thy vc_name =
2.20 (case SPARK_VCs.lookup_vc thy vc_name of
2.21 SOME (ctxt, (_, proved, ctxt', stmt)) =>
2.22 @@ -117,6 +120,13 @@
2.23 (Toplevel.theory o fold add_proof_fun_cmd));
2.24
2.25 val _ =
2.26 + Outer_Syntax.command "spark_types"
2.27 + "associate SPARK types with types"
2.28 + Keyword.thy_decl
2.29 + (Scan.repeat1 (Parse.name --| Args.$$$ "=" -- Parse.typ) >>
2.30 + (Toplevel.theory o fold add_spark_type_cmd));
2.31 +
2.32 +val _ =
2.33 Outer_Syntax.command "spark_vc"
2.34 "enter into proof mode for a specific verification condition"
2.35 Keyword.thy_goal
3.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Apr 14 15:04:42 2011 +0200
3.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Apr 15 15:33:57 2011 +0200
3.3 @@ -7,11 +7,12 @@
3.4
3.5 signature SPARK_VCS =
3.6 sig
3.7 - val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> Fdl_Parser.vcs ->
3.8 - Path.T -> theory -> theory
3.9 + val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
3.10 + (string * string) * Fdl_Parser.vcs -> Path.T -> theory -> theory
3.11 val add_proof_fun: (typ option -> 'a -> term) ->
3.12 string * ((string list * string) option * 'a) ->
3.13 theory -> theory
3.14 + val add_type: string * typ -> theory -> theory
3.15 val lookup_vc: theory -> string -> (Element.context_i list *
3.16 (string * thm list option * Element.context_i * Element.statement_i)) option
3.17 val get_vcs: theory ->
3.18 @@ -28,8 +29,49 @@
3.19 open Fdl_Parser;
3.20
3.21
3.22 +(** theory data **)
3.23 +
3.24 +fun err_unfinished () = error "An unfinished SPARK environment is still open."
3.25 +
3.26 +val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
3.27 +
3.28 +val name_ord = prod_ord string_ord (option_ord int_ord) o
3.29 + pairself (strip_number ##> Int.fromString);
3.30 +
3.31 +structure VCtab = Table(type key = string val ord = name_ord);
3.32 +
3.33 +structure VCs = Theory_Data
3.34 +(
3.35 + type T =
3.36 + {pfuns: ((string list * string) option * term) Symtab.table,
3.37 + type_map: typ Symtab.table,
3.38 + env:
3.39 + {ctxt: Element.context_i list,
3.40 + defs: (binding * thm) list,
3.41 + types: fdl_type tab,
3.42 + funs: (string list * string) tab,
3.43 + ids: (term * string) Symtab.table * Name.context,
3.44 + proving: bool,
3.45 + vcs: (string * thm list option *
3.46 + (string * expr) list * (string * expr) list) VCtab.table,
3.47 + path: Path.T} option}
3.48 + val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
3.49 + val extend = I
3.50 + fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
3.51 + {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
3.52 + {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
3.53 + type_map = Symtab.merge (op =) (type_map1, type_map2),
3.54 + env = NONE}
3.55 + | merge _ = err_unfinished ()
3.56 +)
3.57 +
3.58 +
3.59 (** utilities **)
3.60
3.61 +val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
3.62 +
3.63 +val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name);
3.64 +
3.65 fun mk_unop s t =
3.66 let val T = fastype_of t
3.67 in Const (s, T --> T) $ t end;
3.68 @@ -44,17 +86,22 @@
3.69 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
3.70 end;
3.71
3.72 +fun get_type thy ty =
3.73 + let val {type_map, ...} = VCs.get thy
3.74 + in Symtab.lookup type_map ty end;
3.75 +
3.76 fun mk_type _ "integer" = HOLogic.intT
3.77 | mk_type _ "boolean" = HOLogic.boolT
3.78 - | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy)
3.79 - (Type (Sign.full_name thy (Binding.name ty), []));
3.80 + | mk_type thy ty =
3.81 + (case get_type thy ty of
3.82 + NONE =>
3.83 + Syntax.check_typ (ProofContext.init_global thy)
3.84 + (Type (Sign.full_name thy (Binding.name ty), []))
3.85 + | SOME T => T);
3.86
3.87 val booleanN = "boolean";
3.88 val integerN = "integer";
3.89
3.90 -fun mk_qual_name thy s s' =
3.91 - Sign.full_name thy (Binding.qualify true s (Binding.name s'));
3.92 -
3.93 fun define_overloaded (def_name, eq) lthy =
3.94 let
3.95 val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
3.96 @@ -80,17 +127,29 @@
3.97 val zs = map (Free o rpair T) ys;
3.98 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
3.99
3.100 +fun get_record_info thy T = (case Record.dest_recTs T of
3.101 + [(tyname, [@{typ unit}])] =>
3.102 + Record.get_info thy (Long_Name.qualifier tyname)
3.103 + | _ => NONE);
3.104 +
3.105 +fun find_field fname = find_first (curry lcase_eq fname o fst);
3.106 +
3.107 +fun find_field' fname = get_first (fn (flds, fldty) =>
3.108 + if member (op =) flds fname then SOME fldty else NONE);
3.109 +
3.110 +fun assoc_ty_err thy T s msg =
3.111 + error ("Type " ^ Syntax.string_of_typ_global thy T ^
3.112 + " associated with SPARK type " ^ s ^ "\n" ^ msg);
3.113 +
3.114
3.115 (** generate properties of enumeration types **)
3.116
3.117 -fun add_enum_type tyname els (tab, ctxt) thy =
3.118 +fun add_enum_type tyname tyname' thy =
3.119 let
3.120 - val tyb = Binding.name tyname;
3.121 - val tyname' = Sign.full_name thy tyb;
3.122 + val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
3.123 + val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
3.124 + val k = length cs;
3.125 val T = Type (tyname', []);
3.126 - val case_name = mk_qual_name thy tyname (tyname ^ "_case");
3.127 - val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els;
3.128 - val k = length els;
3.129 val p = Const (@{const_name pos}, T --> HOLogic.intT);
3.130 val v = Const (@{const_name val}, HOLogic.intT --> T);
3.131 val card = Const (@{const_name card},
3.132 @@ -103,9 +162,6 @@
3.133 (f $ Bound 1) $ (f $ Bound 0))));
3.134
3.135 val (((def1, def2), def3), lthy) = thy |>
3.136 - Datatype.add_datatype {strict = true, quiet = true} [tyname]
3.137 - [([], tyb, NoSyn,
3.138 - map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
3.139
3.140 Class.instantiation ([tyname'], [], @{sort enum}) |>
3.141
3.142 @@ -195,46 +251,107 @@
3.143 val simp_att = [Attrib.internal (K Simplifier.simp_add)]
3.144
3.145 in
3.146 - ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab,
3.147 - fold Name.declare els ctxt),
3.148 - lthy' |>
3.149 - Local_Theory.note
3.150 - ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
3.151 - Local_Theory.note
3.152 - ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
3.153 - Local_Theory.note
3.154 - ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
3.155 - Local_Theory.note
3.156 - ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
3.157 - Local_Theory.note
3.158 - ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
3.159 - Local_Theory.exit_global)
3.160 + lthy' |>
3.161 + Local_Theory.note
3.162 + ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
3.163 + Local_Theory.note
3.164 + ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
3.165 + Local_Theory.note
3.166 + ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
3.167 + Local_Theory.note
3.168 + ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
3.169 + Local_Theory.note
3.170 + ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
3.171 + Local_Theory.exit_global
3.172 end;
3.173
3.174
3.175 +fun check_no_assoc thy s = case get_type thy s of
3.176 + NONE => ()
3.177 + | SOME _ => error ("Cannot associate a type with " ^ s ^
3.178 + "\nsince it is no record or enumeration type");
3.179 +
3.180 +fun check_enum [] [] = NONE
3.181 + | check_enum els [] = SOME ("has no element(s) " ^ commas els)
3.182 + | check_enum [] cs = SOME ("has extra element(s) " ^
3.183 + commas (map (Long_Name.base_name o fst) cs))
3.184 + | check_enum (el :: els) ((cname, _) :: cs) =
3.185 + if lcase_eq (el, cname) then check_enum els cs
3.186 + else SOME ("either has no element " ^ el ^
3.187 + " or it is at the wrong position");
3.188 +
3.189 fun add_type_def (s, Basic_Type ty) (ids, thy) =
3.190 - (ids,
3.191 - Typedecl.abbrev_global (Binding.name s, [], NoSyn)
3.192 - (mk_type thy ty) thy |> snd)
3.193 + (check_no_assoc thy s;
3.194 + (ids,
3.195 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
3.196 + (mk_type thy ty) thy |> snd))
3.197
3.198 - | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy
3.199 + | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) =
3.200 + let
3.201 + val (thy', tyname) = (case get_type thy s of
3.202 + NONE =>
3.203 + let
3.204 + val tyb = Binding.name s;
3.205 + val tyname = Sign.full_name thy tyb
3.206 + in
3.207 + (thy |>
3.208 + Datatype.add_datatype {strict = true, quiet = true} [s]
3.209 + [([], tyb, NoSyn,
3.210 + map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
3.211 + add_enum_type s tyname,
3.212 + tyname)
3.213 + end
3.214 + | SOME (T as Type (tyname, [])) =>
3.215 + (case Datatype_Data.get_constrs thy tyname of
3.216 + NONE => assoc_ty_err thy T s "is not a datatype"
3.217 + | SOME cs => (case check_enum els cs of
3.218 + NONE => (thy, tyname)
3.219 + | SOME msg => assoc_ty_err thy T s msg)));
3.220 + val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
3.221 + in
3.222 + ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
3.223 + fold Name.declare els ctxt),
3.224 + thy')
3.225 + end
3.226
3.227 | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =
3.228 - (ids,
3.229 - Typedecl.abbrev_global (Binding.name s, [], NoSyn)
3.230 - (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
3.231 - mk_type thy resty) thy |> snd)
3.232 + (check_no_assoc thy s;
3.233 + (ids,
3.234 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
3.235 + (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
3.236 + mk_type thy resty) thy |> snd))
3.237
3.238 | add_type_def (s, Record_Type fldtys) (ids, thy) =
3.239 (ids,
3.240 - Record.add_record true ([], Binding.name s) NONE
3.241 - (maps (fn (flds, ty) =>
3.242 - let val T = mk_type thy ty
3.243 - in map (fn fld => (Binding.name fld, T, NoSyn)) flds
3.244 - end) fldtys) thy)
3.245 + let val fldTs = maps (fn (flds, ty) =>
3.246 + map (rpair (mk_type thy ty)) flds) fldtys
3.247 + in case get_type thy s of
3.248 + NONE =>
3.249 + Record.add_record true ([], Binding.name s) NONE
3.250 + (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
3.251 + | SOME rT =>
3.252 + (case get_record_info thy rT of
3.253 + NONE => assoc_ty_err thy rT s "is not a record type"
3.254 + | SOME {fields, ...} =>
3.255 + (case subtract (lcase_eq o pairself fst) fldTs fields of
3.256 + [] => ()
3.257 + | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
3.258 + commas (map (Long_Name.base_name o fst) flds));
3.259 + map (fn (fld, T) =>
3.260 + case AList.lookup lcase_eq fields fld of
3.261 + NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
3.262 + | SOME U => T = U orelse assoc_ty_err thy rT s
3.263 + ("has field " ^
3.264 + fld ^ " whose type\n" ^
3.265 + Syntax.string_of_typ_global thy U ^
3.266 + "\ndoes not match declared type\n" ^
3.267 + Syntax.string_of_typ_global thy T)) fldTs;
3.268 + thy))
3.269 + end)
3.270
3.271 | add_type_def (s, Pending_Type) (ids, thy) =
3.272 - (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd);
3.273 + (check_no_assoc thy s;
3.274 + (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
3.275
3.276
3.277 fun term_of_expr thy types funs pfuns =
3.278 @@ -323,17 +440,16 @@
3.279 (case try (unprefix "fld_") s of
3.280 SOME fname => (case es of
3.281 [e] =>
3.282 - let val (t, rcdty) = tm_of vs e
3.283 - in case lookup types rcdty of
3.284 - SOME (Record_Type fldtys) =>
3.285 - (case get_first (fn (flds, fldty) =>
3.286 - if member (op =) flds fname then SOME fldty
3.287 - else NONE) fldtys of
3.288 - SOME fldty =>
3.289 - (Const (mk_qual_name thy rcdty fname,
3.290 - mk_type thy rcdty --> mk_type thy fldty) $ t,
3.291 - fldty)
3.292 - | NONE => error ("Record " ^ rcdty ^
3.293 + let
3.294 + val (t, rcdty) = tm_of vs e;
3.295 + val rT = mk_type thy rcdty
3.296 + in case (get_record_info thy rT, lookup types rcdty) of
3.297 + (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
3.298 + (case (find_field fname fields,
3.299 + find_field' fname fldtys) of
3.300 + (SOME (fname', fT), SOME fldty) =>
3.301 + (Const (fname', rT --> fT) $ t, fldty)
3.302 + | _ => error ("Record " ^ rcdty ^
3.303 " has no field named " ^ fname))
3.304 | _ => error (rcdty ^ " is not a record type")
3.305 end
3.306 @@ -349,20 +465,20 @@
3.307 val rT = mk_type thy rcdty;
3.308 val (u, fldty) = tm_of vs e';
3.309 val fT = mk_type thy fldty
3.310 - in case lookup types rcdty of
3.311 - SOME (Record_Type fldtys) =>
3.312 - (case get_first (fn (flds, fldty) =>
3.313 - if member (op =) flds fname then SOME fldty
3.314 - else NONE) fldtys of
3.315 - SOME fldty' =>
3.316 - if fldty = fldty' then
3.317 - (Const (mk_qual_name thy rcdty (fname ^ "_update"),
3.318 + in case get_record_info thy rT of
3.319 + SOME {fields, ...} =>
3.320 + (case find_field fname fields of
3.321 + SOME (fname', fU) =>
3.322 + if fT = fU then
3.323 + (Const (fname' ^ "_update",
3.324 (fT --> fT) --> rT --> rT) $
3.325 Abs ("x", fT, u) $ t,
3.326 rcdty)
3.327 - else error ("Type " ^ fldty ^
3.328 - " does not match type " ^ fldty' ^ " of field " ^
3.329 - fname)
3.330 + else error ("Type\n" ^
3.331 + Syntax.string_of_typ_global thy fT ^
3.332 + "\ndoes not match type\n" ^
3.333 + Syntax.string_of_typ_global thy fU ^
3.334 + "\nof field " ^ fname)
3.335 | NONE => error ("Record " ^ rcdty ^
3.336 " has no field named " ^ fname))
3.337 | _ => error (rcdty ^ " is not a record type")
3.338 @@ -431,34 +547,35 @@
3.339 end
3.340
3.341 | tm_of vs (Record (s, flds)) =
3.342 - (case lookup types s of
3.343 - SOME (Record_Type fldtys) =>
3.344 - let
3.345 - val flds' = map (apsnd (tm_of vs)) flds;
3.346 - val fnames = maps fst fldtys;
3.347 - val fnames' = map fst flds;
3.348 - val (fvals, ftys) = split_list (map (fn s' =>
3.349 - case AList.lookup (op =) flds' s' of
3.350 - SOME fval_ty => fval_ty
3.351 - | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
3.352 - fnames);
3.353 - val _ = (case subtract (op =) fnames fnames' of
3.354 - [] => ()
3.355 - | xs => error ("Extra field(s) " ^ commas xs ^
3.356 - " in record " ^ s));
3.357 - val _ = (case duplicates (op =) fnames' of
3.358 - [] => ()
3.359 - | xs => error ("Duplicate field(s) " ^ commas xs ^
3.360 - " in record " ^ s))
3.361 - in
3.362 - (list_comb
3.363 - (Const (mk_qual_name thy s (s ^ "_ext"),
3.364 - map (mk_type thy) ftys @ [HOLogic.unitT] --->
3.365 - mk_type thy s),
3.366 - fvals @ [HOLogic.unit]),
3.367 - s)
3.368 - end
3.369 - | _ => error (s ^ " is not a record type"))
3.370 + let
3.371 + val T = mk_type thy s;
3.372 + val {extension = (ext_name, _), fields, ...} =
3.373 + (case get_record_info thy T of
3.374 + NONE => error (s ^ " is not a record type")
3.375 + | SOME info => info);
3.376 + val flds' = map (apsnd (tm_of vs)) flds;
3.377 + val fnames = map (Long_Name.base_name o fst) fields;
3.378 + val fnames' = map fst flds;
3.379 + val (fvals, ftys) = split_list (map (fn s' =>
3.380 + case AList.lookup lcase_eq flds' s' of
3.381 + SOME fval_ty => fval_ty
3.382 + | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
3.383 + fnames);
3.384 + val _ = (case subtract lcase_eq fnames fnames' of
3.385 + [] => ()
3.386 + | xs => error ("Extra field(s) " ^ commas xs ^
3.387 + " in record " ^ s));
3.388 + val _ = (case duplicates (op =) fnames' of
3.389 + [] => ()
3.390 + | xs => error ("Duplicate field(s) " ^ commas xs ^
3.391 + " in record " ^ s))
3.392 + in
3.393 + (list_comb
3.394 + (Const (ext_name,
3.395 + map (mk_type thy) ftys @ [HOLogic.unitT] ---> T),
3.396 + fvals @ [HOLogic.unit]),
3.397 + s)
3.398 + end
3.399
3.400 | tm_of vs (Array (s, default, assocs)) =
3.401 (case lookup types s of
3.402 @@ -592,44 +709,15 @@
3.403
3.404 (** the VC store **)
3.405
3.406 -fun err_unfinished () = error "An unfinished SPARK environment is still open."
3.407 -
3.408 fun err_vcs names = error (Pretty.string_of
3.409 (Pretty.big_list "The following verification conditions have not been proved:"
3.410 (map Pretty.str names)))
3.411
3.412 -val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
3.413 -
3.414 -val name_ord = prod_ord string_ord (option_ord int_ord) o
3.415 - pairself (strip_number ##> Int.fromString);
3.416 -
3.417 -structure VCtab = Table(type key = string val ord = name_ord);
3.418 -
3.419 -structure VCs = Theory_Data
3.420 -(
3.421 - type T =
3.422 - {pfuns: ((string list * string) option * term) Symtab.table,
3.423 - env:
3.424 - {ctxt: Element.context_i list,
3.425 - defs: (binding * thm) list,
3.426 - types: fdl_type tab,
3.427 - funs: (string list * string) tab,
3.428 - ids: (term * string) Symtab.table * Name.context,
3.429 - proving: bool,
3.430 - vcs: (string * thm list option *
3.431 - (string * expr) list * (string * expr) list) VCtab.table,
3.432 - path: Path.T} option}
3.433 - val empty : T = {pfuns = Symtab.empty, env = NONE}
3.434 - val extend = I
3.435 - fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) =
3.436 - {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
3.437 - env = NONE}
3.438 - | merge _ = err_unfinished ()
3.439 -)
3.440 -
3.441 fun set_env (env as {funs, ...}) thy = VCs.map (fn
3.442 - {pfuns, env = NONE} =>
3.443 - {pfuns = check_pfuns_types thy funs pfuns, env = SOME env}
3.444 + {pfuns, type_map, env = NONE} =>
3.445 + {pfuns = check_pfuns_types thy funs pfuns,
3.446 + type_map = type_map,
3.447 + env = SOME env}
3.448 | _ => err_unfinished ()) thy;
3.449
3.450 fun mk_pat s = (case Int.fromString s of
3.451 @@ -672,28 +760,60 @@
3.452 fun add_proof_fun prep (s, (optty, raw_t)) thy =
3.453 VCs.map (fn
3.454 {env = SOME {proving = true, ...}, ...} => err_unfinished ()
3.455 - | {pfuns, env} =>
3.456 + | {pfuns, type_map, env} =>
3.457 let
3.458 val optty' = (case env of
3.459 SOME {funs, ...} => lookup funs s
3.460 | NONE => NONE);
3.461 val optty'' = NONE |> upd_option optty |> upd_option optty';
3.462 - val t = prep (Option.map (pfun_type thy) optty'') raw_t
3.463 + val t = prep (Option.map (pfun_type thy) optty'') raw_t;
3.464 + val _ = (case fold_aterms (fn u =>
3.465 + if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
3.466 + [] => ()
3.467 + | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
3.468 + "\nto be associated with proof function " ^ s ^
3.469 + " contains free variable(s) " ^
3.470 + commas (map (Syntax.string_of_term_global thy) ts)));
3.471 in
3.472 (check_pfun_type thy s t optty optty';
3.473 if is_some optty'' orelse is_none env then
3.474 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
3.475 + type_map = type_map,
3.476 env = env}
3.477 handle Symtab.DUP _ => error ("Proof function " ^ s ^
3.478 " already associated with function")
3.479 else error ("Undeclared proof function " ^ s))
3.480 end) thy;
3.481
3.482 +fun add_type (s, T as Type (tyname, Ts)) thy =
3.483 + thy |>
3.484 + VCs.map (fn
3.485 + {env = SOME _, ...} => err_unfinished ()
3.486 + | {pfuns, type_map, env} =>
3.487 + {pfuns = pfuns,
3.488 + type_map = Symtab.update_new (s, T) type_map,
3.489 + env = env}
3.490 + handle Symtab.DUP _ => error ("SPARK type " ^ s ^
3.491 + " already associated with type")) |>
3.492 + (fn thy' =>
3.493 + case Datatype_Data.get_constrs thy' tyname of
3.494 + NONE => thy'
3.495 + | SOME cs =>
3.496 + if null Ts then
3.497 + (map
3.498 + (fn (_, Type (_, [])) => ()
3.499 + | (cname, _) => assoc_ty_err thy T s
3.500 + ("has illegal constructor " ^
3.501 + Long_Name.base_name cname)) cs;
3.502 + add_enum_type s tyname thy')
3.503 + else assoc_ty_err thy T s "is illegal")
3.504 + | add_type (s, T) thy = assoc_ty_err thy T s "is illegal";
3.505 +
3.506 val is_closed = is_none o #env o VCs.get;
3.507
3.508 fun lookup_vc thy name =
3.509 (case VCs.get thy of
3.510 - {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} =>
3.511 + {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} =>
3.512 (case VCtab.lookup vcs name of
3.513 SOME vc =>
3.514 let val (pfuns', ctxt', ids') =
3.515 @@ -703,7 +823,7 @@
3.516 | _ => NONE);
3.517
3.518 fun get_vcs thy = (case VCs.get thy of
3.519 - {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} =>
3.520 + {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} =>
3.521 let val (pfuns', ctxt', ids') =
3.522 declare_missing_pfuns thy funs pfuns vcs ids
3.523 in
3.524 @@ -714,8 +834,10 @@
3.525 | _ => ([], [], []));
3.526
3.527 fun mark_proved name thms = VCs.map (fn
3.528 - {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
3.529 + {pfuns, type_map,
3.530 + env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
3.531 {pfuns = pfuns,
3.532 + type_map = type_map,
3.533 env = SOME {ctxt = ctxt, defs = defs,
3.534 types = types, funs = funs, ids = ids,
3.535 proving = true,
3.536 @@ -724,18 +846,21 @@
3.537 path = path}}
3.538 | x => x);
3.539
3.540 -fun close thy = VCs.map (fn
3.541 - {pfuns, env = SOME {vcs, path, ...}} =>
3.542 - (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
3.543 - (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
3.544 - (proved, []) =>
3.545 - (Thm.join_proofs (maps (the o #2 o snd) proved);
3.546 - File.write (Path.ext "prv" path)
3.547 - (concat (map (fn (s, _) => snd (strip_number s) ^
3.548 - " -- proved by " ^ Distribution.version ^ "\n") proved));
3.549 - {pfuns = pfuns, env = NONE})
3.550 - | (_, unproved) => err_vcs (map fst unproved))
3.551 - | x => x) thy;
3.552 +fun close thy =
3.553 + thy |>
3.554 + VCs.map (fn
3.555 + {pfuns, type_map, env = SOME {vcs, path, ...}} =>
3.556 + (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
3.557 + (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
3.558 + (proved, []) =>
3.559 + (Thm.join_proofs (maps (the o #2 o snd) proved);
3.560 + File.write (Path.ext "prv" path)
3.561 + (concat (map (fn (s, _) => snd (strip_number s) ^
3.562 + " -- proved by " ^ Distribution.version ^ "\n") proved));
3.563 + {pfuns = pfuns, type_map = type_map, env = NONE})
3.564 + | (_, unproved) => err_vcs (map fst unproved))
3.565 + | _ => error "No SPARK environment is currently open") |>
3.566 + Sign.parent_path;
3.567
3.568
3.569 (** set up verification conditions **)
3.570 @@ -822,7 +947,8 @@
3.571 (remove (op =) d defs) (d :: sdefs)
3.572 | NONE => error ("Bad definitions: " ^ rulenames defs));
3.573
3.574 -fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy =
3.575 +fun set_vcs ({types, vars, consts, funs} : decls)
3.576 + (rules, _) ((_, ident), vcs) path thy =
3.577 let
3.578 val {pfuns, ...} = VCs.get thy;
3.579 val (defs, rules') = partition_opt dest_def rules;
3.580 @@ -847,7 +973,8 @@
3.581 ((Symtab.empty |>
3.582 Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
3.583 Symtab.update ("true", (HOLogic.true_const, booleanN)),
3.584 - Name.context), thy) |>
3.585 + Name.context),
3.586 + thy |> Sign.add_path (Long_Name.base_name ident)) |>
3.587 fold add_type_def (items types) |>
3.588 fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) =>
3.589 ids_thy |>