1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jan 22 11:27:47 2021 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jan 22 12:31:19 2021 +0100
1.3 @@ -28,39 +28,6 @@
1.4
1.5 section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
1.6
1.7 -subsection \<open>code for Example, also needed for keyword \<open>Problem\<close>\<close>
1.8 -ML \<open>
1.9 -\<close> ML \<open> (*also needed for keyword \<open>Problem\<close>*)
1.10 -structure Refs_Data = Theory_Data
1.11 -(
1.12 - type T = References.T
1.13 - val empty : T = References.empty
1.14 - val extend = I
1.15 - fun merge (_, refs) = refs
1.16 -);
1.17 -structure OMod_Data = Theory_Data
1.18 -(
1.19 - type T = O_Model.T
1.20 - val empty : T = []
1.21 - val extend = I
1.22 - fun merge (_, o_model) = o_model
1.23 -);
1.24 -structure Ctxt_Data = Theory_Data
1.25 -(
1.26 - type T = Proof.context
1.27 - val empty : T = ContextC.empty
1.28 - val extend = I
1.29 - fun merge (_, ctxt) = ctxt
1.30 -);
1.31 -\<close>
1.32 -
1.33 -subsection \<open>code to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>
1.34 -ML \<open>
1.35 -\<close> ML \<open>
1.36 -\<close> ML \<open>
1.37 -\<close> ML \<open>
1.38 -\<close>
1.39 -
1.40 subsection \<open>code for Problem\<close>
1.41 text \<open>
1.42 Again, we copy code from spark_vc into Calculation.thy and
1.43 @@ -70,563 +37,21 @@
1.44 \<close> ML \<open>
1.45 \<close>
1.46
1.47 -subsubsection \<open>copied from fdl_parser.ML\<close>
1.48 +subsubsection \<open>TODO\<close>
1.49 ML \<open>
1.50 \<close> ML \<open>
1.51 -datatype expr =
1.52 - Ident of string
1.53 - | Number of int
1.54 - | Quantifier of string * string list * string * expr
1.55 - | Funct of string * expr list
1.56 - | Element of expr * expr list
1.57 - | Update of expr * expr list * expr
1.58 - | Record of string * (string * expr) list
1.59 - | Array of string * expr option *
1.60 - ((expr * expr option) list list * expr) list;
1.61 -\<close> ML \<open>
1.62 - datatype fdl_type =
1.63 - Basic_Type of string
1.64 - | Enum_Type of string list
1.65 - | Array_Type of string list * string
1.66 - | Record_Type of (string list * string) list
1.67 - | Pending_Type;
1.68 -\<close> ML \<open>
1.69 -(* also store items in a list to preserve order *)
1.70 -type 'a tab = 'a Symtab.table * (string * 'a) list;
1.71 -\<close> ML \<open>
1.72 -fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;
1.73 \<close> ML \<open>
1.74 \<close>
1.75 -subsubsection \<open>copied from spark_vcs.ML\<close>
1.76 +
1.77 +subsubsection \<open>TODO\<close>
1.78 ML \<open>
1.79 \<close> ML \<open>
1.80 -(**)
1.81 -fun err_unfinished () = error "An unfinished SPARK environment is still open."
1.82 \<close> ML \<open>
1.83 -val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
1.84 -\<close> ML \<open>
1.85 -val name_ord = prod_ord string_ord (option_ord int_ord) o
1.86 - apply2 (strip_number ##> Int.fromString);
1.87 -\<close> ML \<open>
1.88 -structure VCtab = Table(type key = string val ord = name_ord);
1.89 -\<close> ML \<open>
1.90 -val builtin = Symtab.make (map (rpair ())
1.91 - ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
1.92 - "+", "-", "*", "/", "div", "mod", "**"]);
1.93 -\<close> ML \<open>
1.94 -val is_pfun =
1.95 - Symtab.defined builtin orf
1.96 - can (unprefix "fld_") orf can (unprefix "upf_") orf
1.97 - can (unsuffix "__pos") orf can (unsuffix "__val") orf
1.98 - equal "succ" orf equal "pred";
1.99 -\<close> ML \<open>
1.100 -fun fold_opt f = the_default I o Option.map f;
1.101 -fun fold_pair f g (x, y) = f x #> g y;
1.102 -\<close> ML \<open>
1.103 -fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
1.104 - | fold_expr f g (Ident s) = g s
1.105 - | fold_expr f g (Number _) = I
1.106 - | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
1.107 - | fold_expr f g (Element (e, es)) =
1.108 - fold_expr f g e #> fold (fold_expr f g) es
1.109 - | fold_expr f g (Update (e, es, e')) =
1.110 - fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
1.111 - | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
1.112 - | fold_expr f g (Array (_, default, assocs)) =
1.113 - fold_opt (fold_expr f g) default #>
1.114 - fold (fold_pair
1.115 - (fold (fold (fold_pair
1.116 - (fold_expr f g) (fold_opt (fold_expr f g)))))
1.117 - (fold_expr f g)) assocs;
1.118 -\<close> ML \<open>
1.119 -fun add_expr_pfuns funs = fold_expr
1.120 - (fn s => if is_pfun s then I else insert (op =) s)
1.121 - (fn s => if is_none (lookup funs s) then I else insert (op =) s);
1.122 -\<close> ML \<open>
1.123 -fun fold_vcs f vcs =
1.124 - VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
1.125 -\<close> ML \<open>
1.126 -fun lookup_prfx "" tab s = Symtab.lookup tab s
1.127 - | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
1.128 - NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
1.129 - | x => x);
1.130 -\<close> ML \<open>
1.131 -fun pfuns_of_vcs prfx funs pfuns vcs =
1.132 - fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
1.133 - filter (is_none o lookup_prfx prfx pfuns);
1.134 -\<close> ML \<open>
1.135 -fun pfuns_of_vcs prfx funs pfuns vcs =
1.136 - fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
1.137 - filter (is_none o lookup_prfx prfx pfuns);
1.138 -\<close> ML \<open>
1.139 -structure VCs = Theory_Data
1.140 -(
1.141 - type T =
1.142 - {pfuns: ((string list * string) option * term) Symtab.table,
1.143 - type_map: (typ * (string * string) list) Symtab.table,
1.144 - env:
1.145 - {ctxt: Element.context_i list,
1.146 - defs: (binding * thm) list,
1.147 - types: fdl_type tab,
1.148 - funs: (string list * string) tab,
1.149 - pfuns: ((string list * string) option * term) Symtab.table,
1.150 - ids: (term * string) Symtab.table * Name.context,
1.151 - proving: bool,
1.152 - vcs: (string * thm list option *
1.153 - (string * expr) list * (string * expr) list) VCtab.table,
1.154 - path: Path.T,
1.155 - prefix: string} option}
1.156 - val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
1.157 - val extend = I
1.158 - fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
1.159 - {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
1.160 - {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
1.161 - type_map = Symtab.merge (op =) (type_map1, type_map2),
1.162 - env = NONE}
1.163 - | merge _ = err_unfinished ()
1.164 -)
1.165 -\<close> ML \<open>
1.166 -fun get_type thy prfx ty =
1.167 - let val {type_map, ...} = VCs.get thy
1.168 - in lookup_prfx prfx type_map ty end;
1.169 -\<close> ML \<open>
1.170 -fun mk_type' _ _ "integer" = (HOLogic.intT, [])
1.171 - | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
1.172 - | mk_type' thy prfx ty =
1.173 - (case get_type thy prfx ty of
1.174 - NONE =>
1.175 - (Syntax.check_typ (Proof_Context.init_global thy)
1.176 - (Type (Sign.full_name thy (Binding.name ty), [])),
1.177 - [])
1.178 - | SOME p => p);
1.179 -\<close> ML \<open>
1.180 -fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
1.181 -\<close> ML \<open>
1.182 -fun pfun_type thy prfx (argtys, resty) =
1.183 - map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
1.184 -\<close> ML \<open>
1.185 -fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
1.186 - let
1.187 - val (fs, (tys, Ts)) =
1.188 - pfuns_of_vcs prfx funs pfuns vcs |>
1.189 - map_filter (fn s => lookup funs s |>
1.190 - Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
1.191 - split_list ||> split_list;
1.192 - val (fs', ctxt') = fold_map Name.variant fs ctxt
1.193 - in
1.194 - (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
1.195 - Element.Fixes (map2 (fn s => fn T =>
1.196 - (Binding.name s, SOME T, NoSyn)) fs' Ts),
1.197 - (tab, ctxt'))
1.198 - end;
1.199 -\<close> ML \<open>
1.200 -fun strip_underscores s =
1.201 - strip_underscores (unsuffix "_" s) handle Fail _ => s;
1.202 +\<close>
1.203
1.204 -fun strip_tilde s =
1.205 - unsuffix "~" s ^ "_init" handle Fail _ => s;
1.206 -\<close> ML \<open>
1.207 -val mangle_name = strip_underscores #> strip_tilde;
1.208 -\<close> ML \<open>
1.209 -fun mk_variables thy prfx xs ty (tab, ctxt) =
1.210 - let
1.211 - val T = mk_type thy prfx ty;
1.212 - val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
1.213 - val zs = map (Free o rpair T) ys;
1.214 - in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
1.215 -\<close> ML \<open>
1.216 -fun mk_unop s t =
1.217 - let val T = fastype_of t
1.218 - in Const (s, T --> T) $ t end;
1.219 -\<close> ML \<open>
1.220 -val booleanN = "boolean";
1.221 -val integerN = "integer";
1.222 -\<close> ML \<open>
1.223 -val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
1.224 -val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
1.225 -\<close> ML \<open>
1.226 -fun find_field [] fname fields =
1.227 - find_first (curry lcase_eq fname o fst) fields
1.228 - | find_field cmap fname fields =
1.229 - (case AList.lookup (op =) cmap fname of
1.230 - NONE => NONE
1.231 - | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
1.232 -\<close> ML \<open>
1.233 -fun get_record_info thy T = (case Record.dest_recTs T of
1.234 - [(tyname, [\<^typ>\<open>unit\<close>])] =>
1.235 - Record.get_info thy (Long_Name.qualifier tyname)
1.236 - | _ => NONE);
1.237 -\<close> ML \<open>
1.238 -fun find_field' fname = get_first (fn (flds, fldty) =>
1.239 - if member (op =) flds fname then SOME fldty else NONE);
1.240 -\<close> ML \<open>
1.241 -fun invert_map [] = I
1.242 - | invert_map cmap =
1.243 - map (apfst (the o AList.lookup (op =) (map swap cmap)));
1.244 -\<close> ML \<open>
1.245 -fun mk_times (t, u) =
1.246 - let
1.247 - val setT = fastype_of t;
1.248 - val T = HOLogic.dest_setT setT;
1.249 - val U = HOLogic.dest_setT (fastype_of u)
1.250 - in
1.251 - Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
1.252 - HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
1.253 - end;
1.254 -\<close> ML \<open>
1.255 -fun term_of_expr thy prfx types pfuns =
1.256 - let
1.257 - fun tm_of vs (Funct ("->", [e, e'])) =
1.258 - (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.259 -
1.260 - | tm_of vs (Funct ("<->", [e, e'])) =
1.261 - (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.262 -
1.263 - | tm_of vs (Funct ("or", [e, e'])) =
1.264 - (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.265 -
1.266 - | tm_of vs (Funct ("and", [e, e'])) =
1.267 - (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.268 -
1.269 - | tm_of vs (Funct ("not", [e])) =
1.270 - (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
1.271 -
1.272 - | tm_of vs (Funct ("=", [e, e'])) =
1.273 - (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.274 -
1.275 - | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
1.276 - (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
1.277 -
1.278 - | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
1.279 - (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.280 -
1.281 - | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
1.282 - (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
1.283 -
1.284 - | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
1.285 - (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.286 -
1.287 - | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
1.288 - (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
1.289 -
1.290 - | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
1.291 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.292 -
1.293 - | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
1.294 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.295 -
1.296 - | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
1.297 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.298 -
1.299 - | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
1.300 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.301 -
1.302 - | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
1.303 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.304 -
1.305 - | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
1.306 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.307 -
1.308 - | tm_of vs (Funct ("-", [e])) =
1.309 - (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
1.310 -
1.311 - | tm_of vs (Funct ("**", [e, e'])) =
1.312 - (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
1.313 - HOLogic.intT) $ fst (tm_of vs e) $
1.314 - (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
1.315 -
1.316 - | tm_of (tab, _) (Ident s) =
1.317 - (case Symtab.lookup tab s of
1.318 - SOME t_ty => t_ty
1.319 - | NONE => (case lookup_prfx prfx pfuns s of
1.320 - SOME (SOME ([], resty), t) => (t, resty)
1.321 - | _ => error ("Undeclared identifier " ^ s)))
1.322 -
1.323 - | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
1.324 -
1.325 - | tm_of vs (Quantifier (s, xs, ty, e)) =
1.326 - let
1.327 - val (ys, vs') = mk_variables thy prfx xs ty vs;
1.328 - val q = (case s of
1.329 - "for_all" => HOLogic.mk_all
1.330 - | "for_some" => HOLogic.mk_exists)
1.331 - in
1.332 - (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
1.333 - ys (fst (tm_of vs' e)),
1.334 - booleanN)
1.335 - end
1.336 -
1.337 - | tm_of vs (Funct (s, es)) =
1.338 -
1.339 - (* record field selection *)
1.340 - (case try (unprefix "fld_") s of
1.341 - SOME fname => (case es of
1.342 - [e] =>
1.343 - let
1.344 - val (t, rcdty) = tm_of vs e;
1.345 - val (rT, cmap) = mk_type' thy prfx rcdty
1.346 - in case (get_record_info thy rT, lookup types rcdty) of
1.347 - (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
1.348 - (case (find_field cmap fname fields,
1.349 - find_field' fname fldtys) of
1.350 - (SOME (fname', fT), SOME fldty) =>
1.351 - (Const (fname', rT --> fT) $ t, fldty)
1.352 - | _ => error ("Record " ^ rcdty ^
1.353 - " has no field named " ^ fname))
1.354 - | _ => error (rcdty ^ " is not a record type")
1.355 - end
1.356 - | _ => error ("Function " ^ s ^ " expects one argument"))
1.357 - | NONE =>
1.358 -
1.359 - (* record field update *)
1.360 - (case try (unprefix "upf_") s of
1.361 - SOME fname => (case es of
1.362 - [e, e'] =>
1.363 - let
1.364 - val (t, rcdty) = tm_of vs e;
1.365 - val (rT, cmap) = mk_type' thy prfx rcdty;
1.366 - val (u, fldty) = tm_of vs e';
1.367 - val fT = mk_type thy prfx fldty
1.368 - in case get_record_info thy rT of
1.369 - SOME {fields, ...} =>
1.370 - (case find_field cmap fname fields of
1.371 - SOME (fname', fU) =>
1.372 - if fT = fU then
1.373 - (Const (fname' ^ "_update",
1.374 - (fT --> fT) --> rT --> rT) $
1.375 - Abs ("x", fT, u) $ t,
1.376 - rcdty)
1.377 - else error ("Type\n" ^
1.378 - Syntax.string_of_typ_global thy fT ^
1.379 - "\ndoes not match type\n" ^
1.380 - Syntax.string_of_typ_global thy fU ^
1.381 - "\nof field " ^ fname)
1.382 - | NONE => error ("Record " ^ rcdty ^
1.383 - " has no field named " ^ fname))
1.384 - | _ => error (rcdty ^ " is not a record type")
1.385 - end
1.386 - | _ => error ("Function " ^ s ^ " expects two arguments"))
1.387 - | NONE =>
1.388 -
1.389 - (* enumeration type to integer *)
1.390 - (case try (unsuffix "__pos") s of
1.391 - SOME tyname => (case es of
1.392 - [e] => (Const (\<^const_name>\<open>pos\<close>,
1.393 - mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
1.394 - integerN)
1.395 - | _ => error ("Function " ^ s ^ " expects one argument"))
1.396 - | NONE =>
1.397 -
1.398 - (* integer to enumeration type *)
1.399 - (case try (unsuffix "__val") s of
1.400 - SOME tyname => (case es of
1.401 - [e] => (Const (\<^const_name>\<open>val\<close>,
1.402 - HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
1.403 - tyname)
1.404 - | _ => error ("Function " ^ s ^ " expects one argument"))
1.405 - | NONE =>
1.406 -
1.407 - (* successor / predecessor of enumeration type element *)
1.408 - if s = "succ" orelse s = "pred" then (case es of
1.409 - [e] =>
1.410 - let
1.411 - val (t, tyname) = tm_of vs e;
1.412 - val T = mk_type thy prfx tyname
1.413 - in (Const
1.414 - (if s = "succ" then \<^const_name>\<open>succ\<close>
1.415 - else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
1.416 - end
1.417 - | _ => error ("Function " ^ s ^ " expects one argument"))
1.418 -
1.419 - (* user-defined proof function *)
1.420 - else
1.421 - (case lookup_prfx prfx pfuns s of
1.422 - SOME (SOME (_, resty), t) =>
1.423 - (list_comb (t, map (fst o tm_of vs) es), resty)
1.424 - | _ => error ("Undeclared proof function " ^ s))))))
1.425 -
1.426 - | tm_of vs (Element (e, es)) =
1.427 - let val (t, ty) = tm_of vs e
1.428 - in case lookup types ty of
1.429 - SOME (Array_Type (_, elty)) =>
1.430 - (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
1.431 - | _ => error (ty ^ " is not an array type")
1.432 - end
1.433 -
1.434 - | tm_of vs (Update (e, es, e')) =
1.435 - let val (t, ty) = tm_of vs e
1.436 - in case lookup types ty of
1.437 - SOME (Array_Type (idxtys, elty)) =>
1.438 - let
1.439 - val T = foldr1 HOLogic.mk_prodT
1.440 - (map (mk_type thy prfx) idxtys);
1.441 - val U = mk_type thy prfx elty;
1.442 - val fT = T --> U
1.443 - in
1.444 - (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
1.445 - t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
1.446 - fst (tm_of vs e'),
1.447 - ty)
1.448 - end
1.449 - | _ => error (ty ^ " is not an array type")
1.450 - end
1.451 -
1.452 - | tm_of vs (Record (s, flds)) =
1.453 - let
1.454 - val (T, cmap) = mk_type' thy prfx s;
1.455 - val {extension = (ext_name, _), fields, ...} =
1.456 - (case get_record_info thy T of
1.457 - NONE => error (s ^ " is not a record type")
1.458 - | SOME info => info);
1.459 - val flds' = map (apsnd (tm_of vs)) flds;
1.460 - val fnames = fields |> invert_map cmap |>
1.461 - map (Long_Name.base_name o fst);
1.462 - val fnames' = map fst flds;
1.463 - val (fvals, ftys) = split_list (map (fn s' =>
1.464 - case AList.lookup lcase_eq flds' s' of
1.465 - SOME fval_ty => fval_ty
1.466 - | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
1.467 - fnames);
1.468 - val _ = (case subtract lcase_eq fnames fnames' of
1.469 - [] => ()
1.470 - | xs => error ("Extra field(s) " ^ commas xs ^
1.471 - " in record " ^ s));
1.472 - val _ = (case duplicates (op =) fnames' of
1.473 - [] => ()
1.474 - | xs => error ("Duplicate field(s) " ^ commas xs ^
1.475 - " in record " ^ s))
1.476 - in
1.477 - (list_comb
1.478 - (Const (ext_name,
1.479 - map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
1.480 - fvals @ [HOLogic.unit]),
1.481 - s)
1.482 - end
1.483 -
1.484 - | tm_of vs (Array (s, default, assocs)) =
1.485 - (case lookup types s of
1.486 - SOME (Array_Type (idxtys, elty)) =>
1.487 - let
1.488 - val Ts = map (mk_type thy prfx) idxtys;
1.489 - val T = foldr1 HOLogic.mk_prodT Ts;
1.490 - val U = mk_type thy prfx elty;
1.491 - fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
1.492 - | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
1.493 - T --> T --> HOLogic.mk_setT T) $
1.494 - fst (tm_of vs e) $ fst (tm_of vs e');
1.495 - fun mk_idx idx =
1.496 - if length Ts <> length idx then
1.497 - error ("Arity mismatch in construction of array " ^ s)
1.498 - else foldr1 mk_times (map2 mk_idx' Ts idx);
1.499 - fun mk_upd (idxs, e) t =
1.500 - if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
1.501 - then
1.502 - Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
1.503 - T --> U --> T --> U) $ t $
1.504 - foldl1 HOLogic.mk_prod
1.505 - (map (fst o tm_of vs o fst) (hd idxs)) $
1.506 - fst (tm_of vs e)
1.507 - else
1.508 - Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
1.509 - HOLogic.mk_setT T --> U --> T --> U) $ t $
1.510 - foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
1.511 - (map mk_idx idxs) $
1.512 - fst (tm_of vs e)
1.513 - in
1.514 - (fold mk_upd assocs
1.515 - (case default of
1.516 - SOME e => Abs ("x", T, fst (tm_of vs e))
1.517 - | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
1.518 - s)
1.519 - end
1.520 - | _ => error (s ^ " is not an array type"))
1.521 -
1.522 - in tm_of end;
1.523 -\<close> ML \<open>
1.524 -fun mk_pat s = (case Int.fromString s of
1.525 - SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
1.526 - | NONE => error ("Bad conclusion identifier: C" ^ s));
1.527 -\<close> ML \<open>
1.528 -fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
1.529 - let val prop_of =
1.530 - HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
1.531 - in
1.532 - (tr, proved,
1.533 - Element.Assumes (map (fn (s', e) =>
1.534 - ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
1.535 - Element.Shows (map (fn (s', e) =>
1.536 - (if name_concl then (Binding.name ("C" ^ s'), [])
1.537 - else Binding.empty_atts,
1.538 - [(prop_of e, mk_pat s')])) cs))
1.539 - end;
1.540 -\<close> ML \<open>
1.541 -(*val lookup_vc: theory -> bool -> string -> (Element.context_i list *
1.542 - (string * thm list option * Element.context_i * Element.statement_i)) option
1.543 -*)
1.544 -fun lookup_vc thy name_concl name =
1.545 - (case VCs.get thy of
1.546 - {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
1.547 - (case VCtab.lookup vcs name of
1.548 - SOME vc =>
1.549 - let val (pfuns', ctxt', ids') =
1.550 - declare_missing_pfuns thy prefix funs pfuns vcs ids
1.551 - in
1.552 - SOME (ctxt @ [ctxt'],
1.553 - mk_vc thy prefix types pfuns' ids' name_concl vc)
1.554 - end
1.555 - | NONE => NONE)
1.556 - | _ => NONE);
1.557 -\<close> ML \<open>
1.558 -\<close>
1.559 -subsubsection \<open>copied from spark_commands.ML\<close>
1.560 +subsubsection \<open>TODO\<close>
1.561 ML \<open>
1.562 \<close> ML \<open>
1.563 -fun get_vc thy vc_name =
1.564 - (case SPARK_VCs.lookup_vc thy false vc_name of
1.565 - SOME (ctxt, (_, proved, ctxt', stmt)) =>
1.566 - if is_some proved then
1.567 - error ("The verification condition " ^
1.568 - quote vc_name ^ " has already been proved.")
1.569 - else (ctxt @ [ctxt'], stmt)
1.570 - | NONE => error ("There is no verification condition " ^
1.571 - quote vc_name ^ "."));
1.572 -\<close> ML \<open>
1.573 -(*
1.574 -val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T
1.575 -*)
1.576 -fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =
1.577 - if inthy = thy andalso inpbl = pbl
1.578 - then ((thy, pbl, met_id) : References.T, o_model)
1.579 - else ((inthy, inpbl, Method.id_empty), [])
1.580 -\<close> ML \<open>
1.581 -(*
1.582 -val prove_vc: ParseC.problem -> Proof.context -> Proof.state
1.583 -*)
1.584 -fun prove_vc (*vc_name*)problem lthy =
1.585 - let
1.586 - val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}
1.587 - val thy = Proof_Context.theory_of lthy;
1.588 - val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
1.589 - val (ctxt, stmt) = get_vc thy vc_name
1.590 -(*//--------------------------------- new code --------------------------------\\*)
1.591 - val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem
1.592 - val refs' = Refs_Data.get thy
1.593 - val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
1.594 - val i_model = I_Model.initPIDE pbl_id
1.595 -(*
1.596 - TODO: present Specification = i_model () + refs via PIDE
1.597 -*)
1.598 -(*----------------------------------- new code ----------------------------------*)
1.599 - val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
1.600 -(*\\--------------------------------- new code --------------------------------//*)
1.601 - in
1.602 - Specification.theorem true Thm.theoremK NONE
1.603 - (fn thmss => (Local_Theory.background_theory
1.604 - (SPARK_VCs.mark_proved vc_name (flat thmss))))
1.605 - (Binding.name vc_name, []) [] ctxt stmt false lthy
1.606 - end;
1.607 -\<close> ML \<open>
1.608 -prove_vc: ParseC.problem -> Proof.context -> Proof.state
1.609 \<close> ML \<open>
1.610 \<close>
1.611
1.612 @@ -641,9 +66,9 @@
1.613 val _ =
1.614 Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
1.615 "start a Specification, either from scratch or from preceding 'Example'"
1.616 - (ParseC.problem >> prove_vc);
1.617 + (ParseC.problem >> Preliminary.prove_vc);
1.618 \<close> ML \<open>
1.619 -prove_vc: ParseC.problem -> Proof.context -> Proof.state;
1.620 +Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;
1.621 SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
1.622 \<close> ML \<open>
1.623 \<close>
1.624 @@ -703,7 +128,7 @@
1.625 ( *\\------------------- outcomment before creating session Isac ----------------------------//*)
1.626
1.627
1.628 -section \<open>adapt spark_vc to Problem using Naproche as model\<close>
1.629 +section \<open>Notes: adapt spark_vc to Problem using Naproche as model\<close>
1.630
1.631 subsection \<open>survey on steps of investigation\<close>
1.632 text \<open>
1.633 @@ -727,22 +152,6 @@
1.634 see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
1.635 \<close>
1.636
1.637 -subsection \<open>notes and testbed for Naproche in preliminary spark_vcs\<close>
1.638 -text \<open>
1.639 - tracing "spark_vc procedure_g_c_d_4" see SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
1.640 -\<close> ML \<open>
1.641 -\<close> ML \<open>
1.642 -\<close> ML \<open>
1.643 -\<close>
1.644 -
1.645 -subsection \<open>testbed for Problem\<close>
1.646 -ML \<open>
1.647 -\<close> ML \<open>
1.648 -\<close> ML \<open>
1.649 -\<close> ML \<open>
1.650 -\<close>
1.651 -
1.652 -
1.653 end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..
1.654 ERROR: Found the end of the theory, but the last SPARK environment is still open.
1.655 ..is acceptable for testing spark_vc .. proof - ...
2.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Fri Jan 22 11:27:47 2021 +0100
2.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Fri Jan 22 12:31:19 2021 +0100
2.3 @@ -8,15 +8,20 @@
2.4
2.5 signature PRELIMINARY =
2.6 sig
2.7 + (* for keyword Example *)
2.8 val store_and_show: Formalise.T list -> theory -> theory;
2.9 val load_formalisation: (Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
2.10 (theory -> Token.file list * theory) * 'c -> theory -> theory
2.11
2.12 + (* for keyword Problem*)
2.13 + val prove_vc: ParseC.problem -> Proof.context -> Proof.state
2.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.16 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.17 end
2.18
2.19 +(** code for keyword Example **)
2.20 +
2.21 structure Refs_Data = Theory_Data
2.22 (
2.23 type T = References.T
2.24 @@ -42,7 +47,7 @@
2.25 (**)
2.26 structure Preliminary(**): PRELIMINARY(**) =
2.27 struct
2.28 -
2.29 +(**)
2.30
2.31 fun store_and_show formalise thy =
2.32 let
2.33 @@ -90,5 +95,536 @@
2.34 formalise thy'
2.35 end;
2.36
2.37 +(*** code for keyword Problem ***)
2.38 +(*
2.39 + Code for Isac's keyword Problem is added to SPARK code copied here, too.
2.40 + We leave SPARK code here as long as Isac does not yet adopt SPARK's functionality
2.41 + w.r.t. Outer_Syntax.command.
2.42 +*)
2.43
2.44 -end
2.45 +(** copied from fdl_parser.ML **)
2.46 +
2.47 +datatype expr =
2.48 + Ident of string
2.49 + | Number of int
2.50 + | Quantifier of string * string list * string * expr
2.51 + | Funct of string * expr list
2.52 + | Element of expr * expr list
2.53 + | Update of expr * expr list * expr
2.54 + | Record of string * (string * expr) list
2.55 + | Array of string * expr option *
2.56 + ((expr * expr option) list list * expr) list;
2.57 + datatype fdl_type =
2.58 + Basic_Type of string
2.59 + | Enum_Type of string list
2.60 + | Array_Type of string list * string
2.61 + | Record_Type of (string list * string) list
2.62 + | Pending_Type;
2.63 +(* also store items in a list to preserve order *)
2.64 +type 'a tab = 'a Symtab.table * (string * 'a) list;
2.65 +fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;
2.66 +
2.67 +
2.68 +(** copied from spark_vcs.ML **)
2.69 +
2.70 +fun err_unfinished () = error "An unfinished SPARK environment is still open."
2.71 +val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
2.72 +
2.73 +val name_ord = prod_ord string_ord (option_ord int_ord) o
2.74 + apply2 (strip_number ##> Int.fromString);
2.75 +structure VCtab = Table(type key = string val ord = name_ord);
2.76 +val builtin = Symtab.make (map (rpair ())
2.77 + ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
2.78 + "+", "-", "*", "/", "div", "mod", "**"]);
2.79 +
2.80 +val is_pfun =
2.81 + Symtab.defined builtin orf
2.82 + can (unprefix "fld_") orf can (unprefix "upf_") orf
2.83 + can (unsuffix "__pos") orf can (unsuffix "__val") orf
2.84 + equal "succ" orf equal "pred";
2.85 +
2.86 +fun fold_opt f = the_default I o Option.map f;
2.87 +fun fold_pair f g (x, y) = f x #> g y;
2.88 +
2.89 +fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
2.90 + | fold_expr f g (Ident s) = g s
2.91 + | fold_expr f g (Number _) = I
2.92 + | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
2.93 + | fold_expr f g (Element (e, es)) =
2.94 + fold_expr f g e #> fold (fold_expr f g) es
2.95 + | fold_expr f g (Update (e, es, e')) =
2.96 + fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
2.97 + | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
2.98 + | fold_expr f g (Array (_, default, assocs)) =
2.99 + fold_opt (fold_expr f g) default #>
2.100 + fold (fold_pair
2.101 + (fold (fold (fold_pair
2.102 + (fold_expr f g) (fold_opt (fold_expr f g)))))
2.103 + (fold_expr f g)) assocs;
2.104 +
2.105 +fun add_expr_pfuns funs = fold_expr
2.106 + (fn s => if is_pfun s then I else insert (op =) s)
2.107 + (fn s => if is_none (lookup funs s) then I else insert (op =) s);
2.108 +fun fold_vcs f vcs =
2.109 + VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
2.110 +fun lookup_prfx "" tab s = Symtab.lookup tab s
2.111 + | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
2.112 + NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
2.113 + | x => x);
2.114 +
2.115 +fun pfuns_of_vcs prfx funs pfuns vcs =
2.116 + fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
2.117 + filter (is_none o lookup_prfx prfx pfuns);
2.118 +structure VCs = Theory_Data
2.119 +(
2.120 + type T =
2.121 + {pfuns: ((string list * string) option * term) Symtab.table,
2.122 + type_map: (typ * (string * string) list) Symtab.table,
2.123 + env:
2.124 + {ctxt: Element.context_i list,
2.125 + defs: (binding * thm) list,
2.126 + types: fdl_type tab,
2.127 + funs: (string list * string) tab,
2.128 + pfuns: ((string list * string) option * term) Symtab.table,
2.129 + ids: (term * string) Symtab.table * Name.context,
2.130 + proving: bool,
2.131 + vcs: (string * thm list option *
2.132 + (string * expr) list * (string * expr) list) VCtab.table,
2.133 + path: Path.T,
2.134 + prefix: string} option}
2.135 + val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
2.136 + val extend = I
2.137 + fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
2.138 + {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
2.139 + {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
2.140 + type_map = Symtab.merge (op =) (type_map1, type_map2),
2.141 + env = NONE}
2.142 + | merge _ = err_unfinished ()
2.143 +)
2.144 +
2.145 +fun get_type thy prfx ty =
2.146 + let val {type_map, ...} = VCs.get thy
2.147 + in lookup_prfx prfx type_map ty end;
2.148 +fun mk_type' _ _ "integer" = (HOLogic.intT, [])
2.149 + | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
2.150 + | mk_type' thy prfx ty =
2.151 + (case get_type thy prfx ty of
2.152 + NONE =>
2.153 + (Syntax.check_typ (Proof_Context.init_global thy)
2.154 + (Type (Sign.full_name thy (Binding.name ty), [])),
2.155 + [])
2.156 + | SOME p => p);
2.157 +fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
2.158 +fun pfun_type thy prfx (argtys, resty) =
2.159 + map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
2.160 +fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
2.161 + let
2.162 + val (fs, (tys, Ts)) =
2.163 + pfuns_of_vcs prfx funs pfuns vcs |>
2.164 + map_filter (fn s => lookup funs s |>
2.165 + Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
2.166 + split_list ||> split_list;
2.167 + val (fs', ctxt') = fold_map Name.variant fs ctxt
2.168 + in
2.169 + (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
2.170 + Element.Fixes (map2 (fn s => fn T =>
2.171 + (Binding.name s, SOME T, NoSyn)) fs' Ts),
2.172 + (tab, ctxt'))
2.173 + end;
2.174 +
2.175 +fun strip_underscores s =
2.176 + strip_underscores (unsuffix "_" s) handle Fail _ => s;
2.177 +fun strip_tilde s =
2.178 + unsuffix "~" s ^ "_init" handle Fail _ => s;
2.179 +val mangle_name = strip_underscores #> strip_tilde;
2.180 +
2.181 +fun mk_variables thy prfx xs ty (tab, ctxt) =
2.182 + let
2.183 + val T = mk_type thy prfx ty;
2.184 + val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
2.185 + val zs = map (Free o rpair T) ys;
2.186 + in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
2.187 +fun mk_unop s t =
2.188 + let val T = fastype_of t
2.189 + in Const (s, T --> T) $ t end;
2.190 +
2.191 +val booleanN = "boolean";
2.192 +val integerN = "integer";
2.193 +
2.194 +val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
2.195 +val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
2.196 +
2.197 +fun find_field [] fname fields =
2.198 + find_first (curry lcase_eq fname o fst) fields
2.199 + | find_field cmap fname fields =
2.200 + (case AList.lookup (op =) cmap fname of
2.201 + NONE => NONE
2.202 + | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
2.203 +fun get_record_info thy T = (case Record.dest_recTs T of
2.204 + [(tyname, [\<^typ>\<open>unit\<close>])] =>
2.205 + Record.get_info thy (Long_Name.qualifier tyname)
2.206 + | _ => NONE);
2.207 +fun find_field' fname = get_first (fn (flds, fldty) =>
2.208 + if member (op =) flds fname then SOME fldty else NONE);
2.209 +
2.210 +fun invert_map [] = I
2.211 + | invert_map cmap =
2.212 + map (apfst (the o AList.lookup (op =) (map swap cmap)));
2.213 +
2.214 +fun mk_times (t, u) =
2.215 + let
2.216 + val setT = fastype_of t;
2.217 + val T = HOLogic.dest_setT setT;
2.218 + val U = HOLogic.dest_setT (fastype_of u)
2.219 + in
2.220 + Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
2.221 + HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
2.222 + end;
2.223 +fun term_of_expr thy prfx types pfuns =
2.224 + let
2.225 + fun tm_of vs (Funct ("->", [e, e'])) =
2.226 + (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.227 +
2.228 + | tm_of vs (Funct ("<->", [e, e'])) =
2.229 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.230 +
2.231 + | tm_of vs (Funct ("or", [e, e'])) =
2.232 + (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.233 +
2.234 + | tm_of vs (Funct ("and", [e, e'])) =
2.235 + (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.236 +
2.237 + | tm_of vs (Funct ("not", [e])) =
2.238 + (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
2.239 +
2.240 + | tm_of vs (Funct ("=", [e, e'])) =
2.241 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.242 +
2.243 + | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
2.244 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
2.245 +
2.246 + | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
2.247 + (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.248 +
2.249 + | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
2.250 + (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
2.251 +
2.252 + | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
2.253 + (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
2.254 +
2.255 + | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
2.256 + (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
2.257 +
2.258 + | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
2.259 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
2.260 +
2.261 + | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
2.262 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
2.263 +
2.264 + | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
2.265 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
2.266 +
2.267 + | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
2.268 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
2.269 +
2.270 + | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
2.271 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
2.272 +
2.273 + | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
2.274 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
2.275 +
2.276 + | tm_of vs (Funct ("-", [e])) =
2.277 + (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
2.278 +
2.279 + | tm_of vs (Funct ("**", [e, e'])) =
2.280 + (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
2.281 + HOLogic.intT) $ fst (tm_of vs e) $
2.282 + (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
2.283 +
2.284 + | tm_of (tab, _) (Ident s) =
2.285 + (case Symtab.lookup tab s of
2.286 + SOME t_ty => t_ty
2.287 + | NONE => (case lookup_prfx prfx pfuns s of
2.288 + SOME (SOME ([], resty), t) => (t, resty)
2.289 + | _ => error ("Undeclared identifier " ^ s)))
2.290 +
2.291 + | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
2.292 +
2.293 + | tm_of vs (Quantifier (s, xs, ty, e)) =
2.294 + let
2.295 + val (ys, vs') = mk_variables thy prfx xs ty vs;
2.296 + val q = (case s of
2.297 + "for_all" => HOLogic.mk_all
2.298 + | "for_some" => HOLogic.mk_exists)
2.299 + in
2.300 + (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
2.301 + ys (fst (tm_of vs' e)),
2.302 + booleanN)
2.303 + end
2.304 +
2.305 + | tm_of vs (Funct (s, es)) =
2.306 +
2.307 + (* record field selection *)
2.308 + (case try (unprefix "fld_") s of
2.309 + SOME fname => (case es of
2.310 + [e] =>
2.311 + let
2.312 + val (t, rcdty) = tm_of vs e;
2.313 + val (rT, cmap) = mk_type' thy prfx rcdty
2.314 + in case (get_record_info thy rT, lookup types rcdty) of
2.315 + (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
2.316 + (case (find_field cmap fname fields,
2.317 + find_field' fname fldtys) of
2.318 + (SOME (fname', fT), SOME fldty) =>
2.319 + (Const (fname', rT --> fT) $ t, fldty)
2.320 + | _ => error ("Record " ^ rcdty ^
2.321 + " has no field named " ^ fname))
2.322 + | _ => error (rcdty ^ " is not a record type")
2.323 + end
2.324 + | _ => error ("Function " ^ s ^ " expects one argument"))
2.325 + | NONE =>
2.326 +
2.327 + (* record field update *)
2.328 + (case try (unprefix "upf_") s of
2.329 + SOME fname => (case es of
2.330 + [e, e'] =>
2.331 + let
2.332 + val (t, rcdty) = tm_of vs e;
2.333 + val (rT, cmap) = mk_type' thy prfx rcdty;
2.334 + val (u, fldty) = tm_of vs e';
2.335 + val fT = mk_type thy prfx fldty
2.336 + in case get_record_info thy rT of
2.337 + SOME {fields, ...} =>
2.338 + (case find_field cmap fname fields of
2.339 + SOME (fname', fU) =>
2.340 + if fT = fU then
2.341 + (Const (fname' ^ "_update",
2.342 + (fT --> fT) --> rT --> rT) $
2.343 + Abs ("x", fT, u) $ t,
2.344 + rcdty)
2.345 + else error ("Type\n" ^
2.346 + Syntax.string_of_typ_global thy fT ^
2.347 + "\ndoes not match type\n" ^
2.348 + Syntax.string_of_typ_global thy fU ^
2.349 + "\nof field " ^ fname)
2.350 + | NONE => error ("Record " ^ rcdty ^
2.351 + " has no field named " ^ fname))
2.352 + | _ => error (rcdty ^ " is not a record type")
2.353 + end
2.354 + | _ => error ("Function " ^ s ^ " expects two arguments"))
2.355 + | NONE =>
2.356 +
2.357 + (* enumeration type to integer *)
2.358 + (case try (unsuffix "__pos") s of
2.359 + SOME tyname => (case es of
2.360 + [e] => (Const (\<^const_name>\<open>pos\<close>,
2.361 + mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
2.362 + integerN)
2.363 + | _ => error ("Function " ^ s ^ " expects one argument"))
2.364 + | NONE =>
2.365 +
2.366 + (* integer to enumeration type *)
2.367 + (case try (unsuffix "__val") s of
2.368 + SOME tyname => (case es of
2.369 + [e] => (Const (\<^const_name>\<open>val\<close>,
2.370 + HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
2.371 + tyname)
2.372 + | _ => error ("Function " ^ s ^ " expects one argument"))
2.373 + | NONE =>
2.374 +
2.375 + (* successor / predecessor of enumeration type element *)
2.376 + if s = "succ" orelse s = "pred" then (case es of
2.377 + [e] =>
2.378 + let
2.379 + val (t, tyname) = tm_of vs e;
2.380 + val T = mk_type thy prfx tyname
2.381 + in (Const
2.382 + (if s = "succ" then \<^const_name>\<open>succ\<close>
2.383 + else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
2.384 + end
2.385 + | _ => error ("Function " ^ s ^ " expects one argument"))
2.386 +
2.387 + (* user-defined proof function *)
2.388 + else
2.389 + (case lookup_prfx prfx pfuns s of
2.390 + SOME (SOME (_, resty), t) =>
2.391 + (list_comb (t, map (fst o tm_of vs) es), resty)
2.392 + | _ => error ("Undeclared proof function " ^ s))))))
2.393 +
2.394 + | tm_of vs (Element (e, es)) =
2.395 + let val (t, ty) = tm_of vs e
2.396 + in case lookup types ty of
2.397 + SOME (Array_Type (_, elty)) =>
2.398 + (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
2.399 + | _ => error (ty ^ " is not an array type")
2.400 + end
2.401 +
2.402 + | tm_of vs (Update (e, es, e')) =
2.403 + let val (t, ty) = tm_of vs e
2.404 + in case lookup types ty of
2.405 + SOME (Array_Type (idxtys, elty)) =>
2.406 + let
2.407 + val T = foldr1 HOLogic.mk_prodT
2.408 + (map (mk_type thy prfx) idxtys);
2.409 + val U = mk_type thy prfx elty;
2.410 + val fT = T --> U
2.411 + in
2.412 + (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
2.413 + t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
2.414 + fst (tm_of vs e'),
2.415 + ty)
2.416 + end
2.417 + | _ => error (ty ^ " is not an array type")
2.418 + end
2.419 +
2.420 + | tm_of vs (Record (s, flds)) =
2.421 + let
2.422 + val (T, cmap) = mk_type' thy prfx s;
2.423 + val {extension = (ext_name, _), fields, ...} =
2.424 + (case get_record_info thy T of
2.425 + NONE => error (s ^ " is not a record type")
2.426 + | SOME info => info);
2.427 + val flds' = map (apsnd (tm_of vs)) flds;
2.428 + val fnames = fields |> invert_map cmap |>
2.429 + map (Long_Name.base_name o fst);
2.430 + val fnames' = map fst flds;
2.431 + val (fvals, ftys) = split_list (map (fn s' =>
2.432 + case AList.lookup lcase_eq flds' s' of
2.433 + SOME fval_ty => fval_ty
2.434 + | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
2.435 + fnames);
2.436 + val _ = (case subtract lcase_eq fnames fnames' of
2.437 + [] => ()
2.438 + | xs => error ("Extra field(s) " ^ commas xs ^
2.439 + " in record " ^ s));
2.440 + val _ = (case duplicates (op =) fnames' of
2.441 + [] => ()
2.442 + | xs => error ("Duplicate field(s) " ^ commas xs ^
2.443 + " in record " ^ s))
2.444 + in
2.445 + (list_comb
2.446 + (Const (ext_name,
2.447 + map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
2.448 + fvals @ [HOLogic.unit]),
2.449 + s)
2.450 + end
2.451 +
2.452 + | tm_of vs (Array (s, default, assocs)) =
2.453 + (case lookup types s of
2.454 + SOME (Array_Type (idxtys, elty)) =>
2.455 + let
2.456 + val Ts = map (mk_type thy prfx) idxtys;
2.457 + val T = foldr1 HOLogic.mk_prodT Ts;
2.458 + val U = mk_type thy prfx elty;
2.459 + fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
2.460 + | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
2.461 + T --> T --> HOLogic.mk_setT T) $
2.462 + fst (tm_of vs e) $ fst (tm_of vs e');
2.463 + fun mk_idx idx =
2.464 + if length Ts <> length idx then
2.465 + error ("Arity mismatch in construction of array " ^ s)
2.466 + else foldr1 mk_times (map2 mk_idx' Ts idx);
2.467 + fun mk_upd (idxs, e) t =
2.468 + if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
2.469 + then
2.470 + Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
2.471 + T --> U --> T --> U) $ t $
2.472 + foldl1 HOLogic.mk_prod
2.473 + (map (fst o tm_of vs o fst) (hd idxs)) $
2.474 + fst (tm_of vs e)
2.475 + else
2.476 + Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
2.477 + HOLogic.mk_setT T --> U --> T --> U) $ t $
2.478 + foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
2.479 + (map mk_idx idxs) $
2.480 + fst (tm_of vs e)
2.481 + in
2.482 + (fold mk_upd assocs
2.483 + (case default of
2.484 + SOME e => Abs ("x", T, fst (tm_of vs e))
2.485 + | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
2.486 + s)
2.487 + end
2.488 + | _ => error (s ^ " is not an array type"))
2.489 +
2.490 + in tm_of end;
2.491 +
2.492 +fun mk_pat s = (case Int.fromString s of
2.493 + SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
2.494 + | NONE => error ("Bad conclusion identifier: C" ^ s));
2.495 +fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
2.496 + let val prop_of =
2.497 + HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
2.498 + in
2.499 + (tr, proved,
2.500 + Element.Assumes (map (fn (s', e) =>
2.501 + ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
2.502 + Element.Shows (map (fn (s', e) =>
2.503 + (if name_concl then (Binding.name ("C" ^ s'), [])
2.504 + else Binding.empty_atts,
2.505 + [(prop_of e, mk_pat s')])) cs))
2.506 + end;
2.507 +(*val lookup_vc: theory -> bool -> string -> (Element.context_i list *
2.508 + (string * thm list option * Element.context_i * Element.statement_i)) option
2.509 +*)
2.510 +fun lookup_vc thy name_concl name =
2.511 + (case VCs.get thy of
2.512 + {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
2.513 + (case VCtab.lookup vcs name of
2.514 + SOME vc =>
2.515 + let val (pfuns', ctxt', ids') =
2.516 + declare_missing_pfuns thy prefix funs pfuns vcs ids
2.517 + in
2.518 + SOME (ctxt @ [ctxt'],
2.519 + mk_vc thy prefix types pfuns' ids' name_concl vc)
2.520 + end
2.521 + | NONE => NONE)
2.522 + | _ => NONE);
2.523 +
2.524 +
2.525 +(** copied from spark_commands.ML **)
2.526 +
2.527 +fun get_vc thy vc_name =
2.528 + (case SPARK_VCs.lookup_vc thy false vc_name of
2.529 + SOME (ctxt, (_, proved, ctxt', stmt)) =>
2.530 + if is_some proved then
2.531 + error ("The verification condition " ^
2.532 + quote vc_name ^ " has already been proved.")
2.533 + else (ctxt @ [ctxt'], stmt)
2.534 + | NONE => error ("There is no verification condition " ^
2.535 + quote vc_name ^ "."));
2.536 +(*
2.537 +val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T
2.538 +*)
2.539 +fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =
2.540 + if inthy = thy andalso inpbl = pbl
2.541 + then ((thy, pbl, met_id) : References.T, o_model)
2.542 + else ((inthy, inpbl, Method.id_empty), [])
2.543 +(*
2.544 +val prove_vc: ParseC.problem -> Proof.context -> Proof.state
2.545 +*)
2.546 +fun prove_vc (*vc_name*)problem lthy =
2.547 + let
2.548 + val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}
2.549 + val thy = Proof_Context.theory_of lthy;
2.550 + val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
2.551 + val (ctxt, stmt) = get_vc thy vc_name
2.552 +(*//--------------------------------- new code --------------------------------\\*)
2.553 + val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem
2.554 + val refs' = Refs_Data.get thy
2.555 + val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
2.556 + val i_model = I_Model.initPIDE pbl_id
2.557 +(*
2.558 + TODO: present Specification = i_model () + refs via PIDE
2.559 +*)
2.560 +(*----------------------------------- new code ----------------------------------*)
2.561 + val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
2.562 +(*\\--------------------------------- new code --------------------------------//*)
2.563 + in
2.564 + Specification.theorem true Thm.theoremK NONE
2.565 + (fn thmss => (Local_Theory.background_theory
2.566 + (SPARK_VCs.mark_proved vc_name (flat thmss))))
2.567 + (Binding.name vc_name, []) [] ctxt stmt false lthy
2.568 + end;
2.569 +
2.570 +(**)end(**)