1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Apr 18 15:02:50 2011 +0200
1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Apr 18 16:33:45 2011 +0200
1.3 @@ -13,7 +13,7 @@
1.4 structure SPARK_Commands: SPARK_COMMANDS =
1.5 struct
1.6
1.7 -fun spark_open vc_name thy =
1.8 +fun spark_open (vc_name, prfx) thy =
1.9 let
1.10 val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
1.11 val (base, header) =
1.12 @@ -28,7 +28,7 @@
1.13 (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
1.14 (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
1.15 (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))
1.16 - base thy
1.17 + base prfx thy
1.18 end;
1.19
1.20 fun add_proof_fun_cmd pf thy =
1.21 @@ -107,7 +107,7 @@
1.22 Outer_Syntax.command "spark_open"
1.23 "open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
1.24 Keyword.thy_decl
1.25 - (Parse.name >> (Toplevel.theory o spark_open));
1.26 + (Parse.name -- Parse.parname >> (Toplevel.theory o spark_open));
1.27
1.28 val pfun_type = Scan.option
1.29 (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
2.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Apr 18 15:02:50 2011 +0200
2.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Apr 18 16:33:45 2011 +0200
2.3 @@ -8,7 +8,7 @@
2.4 signature SPARK_VCS =
2.5 sig
2.6 val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
2.7 - (string * string) * Fdl_Parser.vcs -> Path.T -> theory -> theory
2.8 + (string * string) * Fdl_Parser.vcs -> Path.T -> string -> theory -> theory
2.9 val add_proof_fun: (typ option -> 'a -> term) ->
2.10 string * ((string list * string) option * 'a) ->
2.11 theory -> theory
2.12 @@ -54,7 +54,8 @@
2.13 proving: bool,
2.14 vcs: (string * thm list option *
2.15 (string * expr) list * (string * expr) list) VCtab.table,
2.16 - path: Path.T} option}
2.17 + path: Path.T,
2.18 + prefix: string} option}
2.19 val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
2.20 val extend = I
2.21 fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
2.22 @@ -72,6 +73,18 @@
2.23
2.24 val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name);
2.25
2.26 +fun lookup_prfx "" tab s = Symtab.lookup tab s
2.27 + | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
2.28 + NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
2.29 + | x => x);
2.30 +
2.31 +fun strip_prfx s =
2.32 + let
2.33 + fun strip ys [] = ("", implode ys)
2.34 + | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)
2.35 + | strip ys (x :: xs) = strip (x :: ys) xs
2.36 + in strip [] (rev (raw_explode s)) end;
2.37 +
2.38 fun mk_unop s t =
2.39 let val T = fastype_of t
2.40 in Const (s, T --> T) $ t end;
2.41 @@ -86,14 +99,14 @@
2.42 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
2.43 end;
2.44
2.45 -fun get_type thy ty =
2.46 +fun get_type thy prfx ty =
2.47 let val {type_map, ...} = VCs.get thy
2.48 - in Symtab.lookup type_map ty end;
2.49 + in lookup_prfx prfx type_map ty end;
2.50
2.51 -fun mk_type _ "integer" = HOLogic.intT
2.52 - | mk_type _ "boolean" = HOLogic.boolT
2.53 - | mk_type thy ty =
2.54 - (case get_type thy ty of
2.55 +fun mk_type _ _ "integer" = HOLogic.intT
2.56 + | mk_type _ _ "boolean" = HOLogic.boolT
2.57 + | mk_type thy prfx ty =
2.58 + (case get_type thy prfx ty of
2.59 NONE =>
2.60 Syntax.check_typ (Proof_Context.init_global thy)
2.61 (Type (Sign.full_name thy (Binding.name ty), []))
2.62 @@ -120,9 +133,9 @@
2.63
2.64 val mangle_name = strip_underscores #> strip_tilde;
2.65
2.66 -fun mk_variables thy xs ty (tab, ctxt) =
2.67 +fun mk_variables thy prfx xs ty (tab, ctxt) =
2.68 let
2.69 - val T = mk_type thy ty;
2.70 + val T = mk_type thy prfx ty;
2.71 val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
2.72 val zs = map (Free o rpair T) ys;
2.73 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
2.74 @@ -266,7 +279,7 @@
2.75 end;
2.76
2.77
2.78 -fun check_no_assoc thy s = case get_type thy s of
2.79 +fun check_no_assoc thy prfx s = case get_type thy prfx s of
2.80 NONE => ()
2.81 | SOME _ => error ("Cannot associate a type with " ^ s ^
2.82 "\nsince it is no record or enumeration type");
2.83 @@ -280,15 +293,15 @@
2.84 else SOME ("either has no element " ^ el ^
2.85 " or it is at the wrong position");
2.86
2.87 -fun add_type_def (s, Basic_Type ty) (ids, thy) =
2.88 - (check_no_assoc thy s;
2.89 +fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
2.90 + (check_no_assoc thy prfx s;
2.91 (ids,
2.92 Typedecl.abbrev_global (Binding.name s, [], NoSyn)
2.93 - (mk_type thy ty) thy |> snd))
2.94 + (mk_type thy prfx ty) thy |> snd))
2.95
2.96 - | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) =
2.97 + | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) =
2.98 let
2.99 - val (thy', tyname) = (case get_type thy s of
2.100 + val (thy', tyname) = (case get_type thy prfx s of
2.101 NONE =>
2.102 let
2.103 val tyb = Binding.name s;
2.104 @@ -304,9 +317,18 @@
2.105 | SOME (T as Type (tyname, [])) =>
2.106 (case Datatype_Data.get_constrs thy tyname of
2.107 NONE => assoc_ty_err thy T s "is not a datatype"
2.108 - | SOME cs => (case check_enum els cs of
2.109 - NONE => (thy, tyname)
2.110 - | SOME msg => assoc_ty_err thy T s msg)));
2.111 + | SOME cs =>
2.112 + let
2.113 + val (prfx', _) = strip_prfx s;
2.114 + val els' =
2.115 + if prfx' = "" then els
2.116 + else map (unprefix (prfx' ^ "__")) els
2.117 + handle Fail _ => error ("Bad enumeration type " ^ s)
2.118 + in
2.119 + case check_enum els' cs of
2.120 + NONE => (thy, tyname)
2.121 + | SOME msg => assoc_ty_err thy T s msg
2.122 + end));
2.123 val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
2.124 in
2.125 ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
2.126 @@ -314,18 +336,18 @@
2.127 thy')
2.128 end
2.129
2.130 - | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =
2.131 - (check_no_assoc thy s;
2.132 + | add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) =
2.133 + (check_no_assoc thy prfx s;
2.134 (ids,
2.135 Typedecl.abbrev_global (Binding.name s, [], NoSyn)
2.136 - (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
2.137 - mk_type thy resty) thy |> snd))
2.138 + (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->
2.139 + mk_type thy prfx resty) thy |> snd))
2.140
2.141 - | add_type_def (s, Record_Type fldtys) (ids, thy) =
2.142 + | add_type_def prfx (s, Record_Type fldtys) (ids, thy) =
2.143 (ids,
2.144 let val fldTs = maps (fn (flds, ty) =>
2.145 - map (rpair (mk_type thy ty)) flds) fldtys
2.146 - in case get_type thy s of
2.147 + map (rpair (mk_type thy prfx ty)) flds) fldtys
2.148 + in case get_type thy prfx s of
2.149 NONE =>
2.150 Record.add_record true ([], Binding.name s) NONE
2.151 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
2.152 @@ -349,12 +371,12 @@
2.153 thy))
2.154 end)
2.155
2.156 - | add_type_def (s, Pending_Type) (ids, thy) =
2.157 - (check_no_assoc thy s;
2.158 + | add_type_def prfx (s, Pending_Type) (ids, thy) =
2.159 + (check_no_assoc thy prfx s;
2.160 (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
2.161
2.162
2.163 -fun term_of_expr thy types funs pfuns =
2.164 +fun term_of_expr thy prfx types pfuns =
2.165 let
2.166 fun tm_of vs (Funct ("->", [e, e'])) =
2.167 (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.168 @@ -424,7 +446,7 @@
2.169
2.170 | tm_of vs (Quantifier (s, xs, ty, e)) =
2.171 let
2.172 - val (ys, vs') = mk_variables thy xs ty vs;
2.173 + val (ys, vs') = mk_variables thy prfx xs ty vs;
2.174 val q = (case s of
2.175 "for_all" => HOLogic.mk_all
2.176 | "for_some" => HOLogic.mk_exists)
2.177 @@ -442,7 +464,7 @@
2.178 [e] =>
2.179 let
2.180 val (t, rcdty) = tm_of vs e;
2.181 - val rT = mk_type thy rcdty
2.182 + val rT = mk_type thy prfx rcdty
2.183 in case (get_record_info thy rT, lookup types rcdty) of
2.184 (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
2.185 (case (find_field fname fields,
2.186 @@ -462,9 +484,9 @@
2.187 [e, e'] =>
2.188 let
2.189 val (t, rcdty) = tm_of vs e;
2.190 - val rT = mk_type thy rcdty;
2.191 + val rT = mk_type thy prfx rcdty;
2.192 val (u, fldty) = tm_of vs e';
2.193 - val fT = mk_type thy fldty
2.194 + val fT = mk_type thy prfx fldty
2.195 in case get_record_info thy rT of
2.196 SOME {fields, ...} =>
2.197 (case find_field fname fields of
2.198 @@ -490,7 +512,8 @@
2.199 (case try (unsuffix "__pos") s of
2.200 SOME tyname => (case es of
2.201 [e] => (Const (@{const_name pos},
2.202 - mk_type thy tyname --> HOLogic.intT) $ fst (tm_of vs e), integerN)
2.203 + mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
2.204 + integerN)
2.205 | _ => error ("Function " ^ s ^ " expects one argument"))
2.206 | NONE =>
2.207
2.208 @@ -498,7 +521,8 @@
2.209 (case try (unsuffix "__val") s of
2.210 SOME tyname => (case es of
2.211 [e] => (Const (@{const_name val},
2.212 - HOLogic.intT --> mk_type thy tyname) $ fst (tm_of vs e), tyname)
2.213 + HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
2.214 + tyname)
2.215 | _ => error ("Function " ^ s ^ " expects one argument"))
2.216 | NONE =>
2.217
2.218 @@ -507,7 +531,7 @@
2.219 [e] =>
2.220 let
2.221 val (t, tyname) = tm_of vs e;
2.222 - val T = mk_type thy tyname
2.223 + val T = mk_type thy prfx tyname
2.224 in (Const
2.225 (if s = "succ" then @{const_name succ}
2.226 else @{const_name pred}, T --> T) $ t, tyname)
2.227 @@ -516,7 +540,7 @@
2.228
2.229 (* user-defined proof function *)
2.230 else
2.231 - (case Symtab.lookup pfuns s of
2.232 + (case lookup_prfx prfx pfuns s of
2.233 SOME (SOME (_, resty), t) =>
2.234 (list_comb (t, map (fst o tm_of vs) es), resty)
2.235 | _ => error ("Undeclared proof function " ^ s))))))
2.236 @@ -534,8 +558,9 @@
2.237 in case lookup types ty of
2.238 SOME (Array_Type (idxtys, elty)) =>
2.239 let
2.240 - val T = foldr1 HOLogic.mk_prodT (map (mk_type thy) idxtys);
2.241 - val U = mk_type thy elty;
2.242 + val T = foldr1 HOLogic.mk_prodT
2.243 + (map (mk_type thy prfx) idxtys);
2.244 + val U = mk_type thy prfx elty;
2.245 val fT = T --> U
2.246 in
2.247 (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $
2.248 @@ -548,7 +573,7 @@
2.249
2.250 | tm_of vs (Record (s, flds)) =
2.251 let
2.252 - val T = mk_type thy s;
2.253 + val T = mk_type thy prfx s;
2.254 val {extension = (ext_name, _), fields, ...} =
2.255 (case get_record_info thy T of
2.256 NONE => error (s ^ " is not a record type")
2.257 @@ -572,7 +597,7 @@
2.258 in
2.259 (list_comb
2.260 (Const (ext_name,
2.261 - map (mk_type thy) ftys @ [HOLogic.unitT] ---> T),
2.262 + map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
2.263 fvals @ [HOLogic.unit]),
2.264 s)
2.265 end
2.266 @@ -581,9 +606,9 @@
2.267 (case lookup types s of
2.268 SOME (Array_Type (idxtys, elty)) =>
2.269 let
2.270 - val Ts = map (mk_type thy) idxtys;
2.271 + val Ts = map (mk_type thy prfx) idxtys;
2.272 val T = foldr1 HOLogic.mk_prodT Ts;
2.273 - val U = mk_type thy elty;
2.274 + val U = mk_type thy prfx elty;
2.275 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
2.276 | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},
2.277 T --> T --> HOLogic.mk_setT T) $
2.278 @@ -618,8 +643,8 @@
2.279 in tm_of end;
2.280
2.281
2.282 -fun term_of_rule thy types funs pfuns ids rule =
2.283 - let val tm_of = fst o term_of_expr thy types funs pfuns ids
2.284 +fun term_of_rule thy prfx types pfuns ids rule =
2.285 + let val tm_of = fst o term_of_expr thy prfx types pfuns ids
2.286 in case rule of
2.287 Inference_Rule (es, e) => Logic.list_implies
2.288 (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))
2.289 @@ -676,14 +701,14 @@
2.290
2.291 val add_expr_idents = fold_expr (K I) (insert (op =));
2.292
2.293 -fun pfun_type thy (argtys, resty) =
2.294 - map (mk_type thy) argtys ---> mk_type thy resty;
2.295 +fun pfun_type thy prfx (argtys, resty) =
2.296 + map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
2.297
2.298 -fun check_pfun_type thy s t optty1 optty2 =
2.299 +fun check_pfun_type thy prfx s t optty1 optty2 =
2.300 let
2.301 val T = fastype_of t;
2.302 fun check ty =
2.303 - let val U = pfun_type thy ty
2.304 + let val U = pfun_type thy prfx ty
2.305 in
2.306 T = U orelse
2.307 error ("Type\n" ^
2.308 @@ -698,11 +723,13 @@
2.309
2.310 fun upd_option x y = if is_some x then x else y;
2.311
2.312 -fun check_pfuns_types thy funs =
2.313 +fun check_pfuns_types thy prfx funs =
2.314 Symtab.map (fn s => fn (optty, t) =>
2.315 - let val optty' = lookup funs s
2.316 + let val optty' = lookup funs
2.317 + (if prfx = "" then s
2.318 + else unprefix (prfx ^ "__") s handle Fail _ => s)
2.319 in
2.320 - (check_pfun_type thy s t optty optty';
2.321 + (check_pfun_type thy prfx s t optty optty';
2.322 (NONE |> upd_option optty |> upd_option optty', t))
2.323 end);
2.324
2.325 @@ -713,9 +740,9 @@
2.326 (Pretty.big_list "The following verification conditions have not been proved:"
2.327 (map Pretty.str names)))
2.328
2.329 -fun set_env (env as {funs, ...}) thy = VCs.map (fn
2.330 +fun set_env (env as {funs, prefix, ...}) thy = VCs.map (fn
2.331 {pfuns, type_map, env = NONE} =>
2.332 - {pfuns = check_pfuns_types thy funs pfuns,
2.333 + {pfuns = check_pfuns_types thy prefix funs pfuns,
2.334 type_map = type_map,
2.335 env = SOME env}
2.336 | _ => err_unfinished ()) thy;
2.337 @@ -724,9 +751,9 @@
2.338 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
2.339 | NONE => error ("Bad conclusion identifier: C" ^ s));
2.340
2.341 -fun mk_vc thy types funs pfuns ids (tr, proved, ps, cs) =
2.342 +fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) =
2.343 let val prop_of =
2.344 - HOLogic.mk_Trueprop o fst o term_of_expr thy types funs pfuns ids
2.345 + HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
2.346 in
2.347 (tr, proved,
2.348 Element.Assumes (map (fn (s', e) =>
2.349 @@ -738,16 +765,16 @@
2.350 fun fold_vcs f vcs =
2.351 VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
2.352
2.353 -fun pfuns_of_vcs pfuns vcs =
2.354 +fun pfuns_of_vcs prfx pfuns vcs =
2.355 fold_vcs (add_expr_pfuns o snd) vcs [] |>
2.356 - filter_out (Symtab.defined pfuns);
2.357 + filter (is_none o lookup_prfx prfx pfuns);
2.358
2.359 -fun declare_missing_pfuns thy funs pfuns vcs (tab, ctxt) =
2.360 +fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
2.361 let
2.362 val (fs, (tys, Ts)) =
2.363 - pfuns_of_vcs pfuns vcs |>
2.364 + pfuns_of_vcs prfx pfuns vcs |>
2.365 map_filter (fn s => lookup funs s |>
2.366 - Option.map (fn ty => (s, (SOME ty, pfun_type thy ty)))) |>
2.367 + Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
2.368 split_list ||> split_list;
2.369 val (fs', ctxt') = Name.variants fs ctxt
2.370 in
2.371 @@ -762,11 +789,11 @@
2.372 {env = SOME {proving = true, ...}, ...} => err_unfinished ()
2.373 | {pfuns, type_map, env} =>
2.374 let
2.375 - val optty' = (case env of
2.376 - SOME {funs, ...} => lookup funs s
2.377 - | NONE => NONE);
2.378 + val (optty', prfx) = (case env of
2.379 + SOME {funs, prefix, ...} => (lookup funs s, prefix)
2.380 + | NONE => (NONE, ""));
2.381 val optty'' = NONE |> upd_option optty |> upd_option optty';
2.382 - val t = prep (Option.map (pfun_type thy) optty'') raw_t;
2.383 + val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
2.384 val _ = (case fold_aterms (fn u =>
2.385 if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
2.386 [] => ()
2.387 @@ -775,7 +802,7 @@
2.388 " contains free variable(s) " ^
2.389 commas (map (Syntax.string_of_term_global thy) ts)));
2.390 in
2.391 - (check_pfun_type thy s t optty optty';
2.392 + (check_pfun_type thy prfx s t optty optty';
2.393 if is_some optty'' orelse is_none env then
2.394 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
2.395 type_map = type_map,
2.396 @@ -813,29 +840,29 @@
2.397
2.398 fun lookup_vc thy name =
2.399 (case VCs.get thy of
2.400 - {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} =>
2.401 + {env = SOME {vcs, types, funs, ids, ctxt, prefix, ...}, pfuns, ...} =>
2.402 (case VCtab.lookup vcs name of
2.403 - SOME vc =>
2.404 + SOME vc =>
2.405 let val (pfuns', ctxt', ids') =
2.406 - declare_missing_pfuns thy funs pfuns vcs ids
2.407 - in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end
2.408 + declare_missing_pfuns thy prefix funs pfuns vcs ids
2.409 + in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' vc) end
2.410 | NONE => NONE)
2.411 | _ => NONE);
2.412
2.413 fun get_vcs thy = (case VCs.get thy of
2.414 - {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} =>
2.415 + {env = SOME {vcs, types, funs, ids, ctxt, defs, prefix, ...}, pfuns, ...} =>
2.416 let val (pfuns', ctxt', ids') =
2.417 - declare_missing_pfuns thy funs pfuns vcs ids
2.418 + declare_missing_pfuns thy prefix funs pfuns vcs ids
2.419 in
2.420 (ctxt @ [ctxt'], defs,
2.421 VCtab.dest vcs |>
2.422 - map (apsnd (mk_vc thy types funs pfuns' ids')))
2.423 + map (apsnd (mk_vc thy prefix types pfuns' ids')))
2.424 end
2.425 | _ => ([], [], []));
2.426
2.427 fun mark_proved name thms = VCs.map (fn
2.428 {pfuns, type_map,
2.429 - env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
2.430 + env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} =>
2.431 {pfuns = pfuns,
2.432 type_map = type_map,
2.433 env = SOME {ctxt = ctxt, defs = defs,
2.434 @@ -843,7 +870,8 @@
2.435 proving = true,
2.436 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
2.437 (trace, SOME thms, ps, cs)) vcs,
2.438 - path = path}}
2.439 + path = path,
2.440 + prefix = prefix}}
2.441 | x => x);
2.442
2.443 fun close thy =
2.444 @@ -878,9 +906,9 @@
2.445
2.446 fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);
2.447
2.448 -fun add_const (s, ty) ((tab, ctxt), thy) =
2.449 +fun add_const prfx (s, ty) ((tab, ctxt), thy) =
2.450 let
2.451 - val T = mk_type thy ty;
2.452 + val T = mk_type thy prfx ty;
2.453 val b = Binding.name s;
2.454 val c = Const (Sign.full_name thy b, T)
2.455 in
2.456 @@ -889,13 +917,13 @@
2.457 Sign.add_consts_i [(b, T, NoSyn)] thy))
2.458 end;
2.459
2.460 -fun add_def types funs pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
2.461 +fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
2.462 (case lookup consts s of
2.463 SOME ty =>
2.464 let
2.465 - val (t, ty') = term_of_expr thy types funs pfuns ids e;
2.466 - val T = mk_type thy ty;
2.467 - val T' = mk_type thy ty';
2.468 + val (t, ty') = term_of_expr thy prfx types pfuns ids e;
2.469 + val T = mk_type thy prfx ty;
2.470 + val T' = mk_type thy prfx ty';
2.471 val _ = T = T' orelse
2.472 error ("Declared type " ^ ty ^ " of " ^ s ^
2.473 "\ndoes not match type " ^ ty' ^ " in definition");
2.474 @@ -913,12 +941,12 @@
2.475 end
2.476 | NONE => error ("Undeclared constant " ^ s));
2.477
2.478 -fun add_var (s, ty) (ids, thy) =
2.479 - let val ([Free p], ids') = mk_variables thy [s] ty ids
2.480 +fun add_var prfx (s, ty) (ids, thy) =
2.481 + let val ([Free p], ids') = mk_variables thy prfx [s] ty ids
2.482 in (p, (ids', thy)) end;
2.483
2.484 -fun add_init_vars vcs (ids_thy as ((tab, _), _)) =
2.485 - fold_map add_var
2.486 +fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =
2.487 + fold_map (add_var prfx)
2.488 (map_filter
2.489 (fn s => case try (unsuffix "~") s of
2.490 SOME s' => (case Symtab.lookup tab s' of
2.491 @@ -935,20 +963,20 @@
2.492 (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
2.493
2.494 (* sort definitions according to their dependency *)
2.495 -fun sort_defs _ _ [] sdefs = rev sdefs
2.496 - | sort_defs pfuns consts defs sdefs =
2.497 +fun sort_defs _ _ _ [] sdefs = rev sdefs
2.498 + | sort_defs prfx pfuns consts defs sdefs =
2.499 (case find_first (fn (_, (_, e)) =>
2.500 - forall (Symtab.defined pfuns) (add_expr_pfuns e []) andalso
2.501 + forall (is_some o lookup_prfx prfx pfuns) (add_expr_pfuns e []) andalso
2.502 forall (fn id =>
2.503 member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
2.504 consts id)
2.505 (add_expr_idents e [])) defs of
2.506 - SOME d => sort_defs pfuns consts
2.507 + SOME d => sort_defs prfx pfuns consts
2.508 (remove (op =) d defs) (d :: sdefs)
2.509 | NONE => error ("Bad definitions: " ^ rulenames defs));
2.510
2.511 fun set_vcs ({types, vars, consts, funs} : decls)
2.512 - (rules, _) ((_, ident), vcs) path thy =
2.513 + (rules, _) ((_, ident), vcs) path prfx thy =
2.514 let
2.515 val {pfuns, ...} = VCs.get thy;
2.516 val (defs, rules') = partition_opt dest_def rules;
2.517 @@ -965,7 +993,7 @@
2.518 (filter_out (is_trivial_vc o snd) vcs)) vcs);
2.519
2.520 val _ = (case filter_out (is_some o lookup funs)
2.521 - (pfuns_of_vcs pfuns vcs') of
2.522 + (pfuns_of_vcs prfx pfuns vcs') of
2.523 [] => ()
2.524 | fs => error ("Undeclared proof function(s) " ^ commas fs));
2.525
2.526 @@ -975,27 +1003,27 @@
2.527 Symtab.update ("true", (HOLogic.true_const, booleanN)),
2.528 Name.context),
2.529 thy |> Sign.add_path (Long_Name.base_name ident)) |>
2.530 - fold add_type_def (items types) |>
2.531 - fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) =>
2.532 + fold (add_type_def prfx) (items types) |>
2.533 + fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
2.534 ids_thy |>
2.535 - fold_map (add_def types funs pfuns consts)
2.536 - (sort_defs pfuns (Symtab.defined tab) defs []) ||>>
2.537 - fold_map add_var (items vars) ||>>
2.538 - add_init_vars vcs');
2.539 + fold_map (add_def prfx types pfuns consts)
2.540 + (sort_defs prfx pfuns (Symtab.defined tab) defs []) ||>>
2.541 + fold_map (add_var prfx) (items vars) ||>>
2.542 + add_init_vars prfx vcs');
2.543
2.544 val ctxt =
2.545 [Element.Fixes (map (fn (s, T) =>
2.546 (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),
2.547 Element.Assumes (map (fn (id, rl) =>
2.548 ((mk_rulename id, []),
2.549 - [(term_of_rule thy' types funs pfuns ids rl, [])]))
2.550 + [(term_of_rule thy' prfx types pfuns ids rl, [])]))
2.551 other_rules),
2.552 Element.Notes (Thm.definitionK,
2.553 [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
2.554
2.555 in
2.556 set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
2.557 - ids = ids, proving = false, vcs = vcs', path = path} thy'
2.558 + ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy'
2.559 end;
2.560
2.561 end;