1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Nov 02 15:16:07 2020 +0100
1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Wed Nov 04 09:59:30 2020 +0100
1.3 @@ -14,8 +14,8 @@
1.4 (**)val _ = @{print} {a = "//--- ##1# spark_open", files = files, header = header, prfx = prfx};(**)
1.5 val xxx as ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,(*.siv*)
1.6 {lines = fdl_lines, pos = fdl_pos, ...}, (*.fld*)
1.7 - {lines = rls_lines, pos = rls_pos, ...}], thy') = (*.rls*)
1.8 - (@{print} {a = "##1# spark_open: before call \"files thy\", files = siv_header"}; files thy);
1.9 + {lines = rls_lines, pos = rls_pos, ...}], thy') (*.rls*)
1.10 + = (@{print} {a = "##1# spark_open: before call <files thy>, files = siv_header !"}; files thy);
1.11 (* ^^^^^ arg!*)
1.12 val path = fst (Path.split_ext src_path);
1.13 in
2.1 --- a/src/Pure/PIDE/resources.ML Mon Nov 02 15:16:07 2020 +0100
2.2 +++ b/src/Pure/PIDE/resources.ML Wed Nov 04 09:59:30 2020 +0100
2.3 @@ -238,6 +238,7 @@
2.4 parse_files cmd >> (fn files => fn thy =>
2.5 let
2.6 val fs = files thy;
2.7 + (*WN*)val _ = @{print} {a = "### provide_parse_files", fs = fs}
2.8 val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
2.9 in (fs, thy') end);
2.10
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Nov 02 15:16:07 2020 +0100
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Nov 04 09:59:30 2020 +0100
3.3 @@ -6,7 +6,7 @@
3.4 *)
3.5
3.6 theory Calculation
3.7 - imports "~~/src/Tools/isac/MathEngine/MathEngine" (** )"HOL-SPARK.SPARK"( **prelim.for devel.*)
3.8 + imports "~~/src/Tools/isac/MathEngine/MathEngine" (** )"HOL-SPARK.SPARK"( **HIDE for Test_Isac*)
3.9 keywords
3.10 "Example" :: thy_load ("str") and (* "spark_vc" :: thy_goal *)
3.11 "Problem" and (* root-problem + recursively in Solution *)
3.12 @@ -20,42 +20,139 @@
3.13 ML_file parseC.sml
3.14
3.15 section \<open>derive Outer_Syntax.command..Example from ..spark_open\<close>
3.16 -ML \<open> (*===== dummies for Outer_Syntax.command..spark_open*)
3.17 +subsection \<open>trials 1\<close>
3.18 +ML \<open>
3.19 +val form_single_str = (
3.20 + "( " ^
3.21 + " [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\", " ^
3.22 + " \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\", " ^
3.23 + " \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\", " ^
3.24 + " \"AbleitungBiegelinie dy\"], " ^
3.25 + " (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])" ^
3.26 + ")")
3.27 +\<close> ML \<open>
3.28 +\<close> text \<open> (*/------------------------ def. Fdl_Lexer.$$$ ----------------------------------\*)
3.29 +val form_single =
3.30 + Fdl_Lexer.$$$ "(" --
3.31 + Fdl_Lexer.$$$ "[" (* |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --*)
3.32 +\<close> text \<open>
3.33 +form_single: (string * Position.T) list ->
3.34 + ((string * Position.T) list * (string * Position.T) list) * (string * Position.T) list
3.35 +\<close> text \<open> (*\------------------------ def. Fdl_Lexer.$$$ ----------------------------------*)
3.36 +\<close> text \<open>
3.37 +form_single [("(", Position.none), ("[", Position.none)](* = (([("(", {})], [("[", {})]), [])*)
3.38 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ...........................OK: ^^ *)
3.39 +\<close> text \<open>
3.40 + (* |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --*)
3.41 + ..would need to understand Fdl_Lexer + Fdl_Parser ?!?
3.42 +\<close> ML \<open>
3.43 +\<close> ML \<open> (*/------------------------ Resources.parse_files -------------------------------\*)
3.44 +Resources.provide_parse_files "spark_open"
3.45 +\<close> ML \<open>
3.46 +Resources.parse_files "spark_open": (theory -> Token.file list) parser;
3.47 +Resources.parse_files "spark_open": Token.T list -> (theory -> Token.file list) * Token.T list;
3.48 +\<close> ML \<open>
3.49 +val toks = ParseC.tokenize form_single_str;
3.50 +\<close> text \<open>
3.51 + (Resources.parse_files "Example") toks;
3.52 +ParseC.parse (Resources.parse_files "Example") toks;
3.53 +(*exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
3.54 +\<close> ML \<open> (*\------------------------ Resources.parse_files -------------------------------/*)
3.55 +\<close> ML \<open>
3.56 +\<close> ML \<open>
3.57 +\<close> ML \<open> (*/------------------------ Parse.path ------------------------------------------\*)
3.58 +Parse.path: string parser;
3.59 +\<close> ML \<open>
3.60 +val toks = ParseC.tokenize
3.61 + "/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv"
3.62 +\<close> text \<open>
3.63 +(Scan.ahead Parse.not_eof -- Parse.path) toks
3.64 +(*exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
3.65 +\<close> ML \<open> (*\------------------------ Parse.path ------------------------------------------/*)
3.66 +\<close> ML \<open>
3.67 +\<close>
3.68 +
3.69 +subsection \<open>code for spark_open\<close>
3.70 +text \<open>
3.71 + We minimally change code for Example, until all works.
3.72 +
3.73 + The code is separated from Calculation.thy into files cp_spark_vcs.ML and cp_spark_commands.ML,
3.74 + because text\<open>...\<close> and (*...*) for const_name>\<open>...\<close> etc and @ {thms ...} causes errors.
3.75 +
3.76 + Thus for Test_Isac (**)ML_file "cp_spark_vcs.ML", ""(*cp_spark_commands.ML*) must be outcommented.
3.77 +\<close>
3.78 +(*HIDE for Test_Isac** )
3.79 +ML_file "cp_spark_vcs.ML"
3.80 +
3.81 +ML_file "cp_spark_commands.ML"
3.82 +( **HIDE for Test_Isac*)
3.83 +
3.84 +subsubsection \<open>cp. HOL/SPARK/Tools/spark_vcs.ML\<close>
3.85 + ML \<open>
3.86 +\<close> ML \<open>
3.87 +(*/--------------------------------- cp_spark_vcs.ML -----------------------------------------\*)
3.88 +(*\--------------------------------- cp_spark_vcs.ML -----------------------------------------/*)
3.89 +\<close> ML \<open>
3.90 +\<close>
3.91 +
3.92 +subsubsection \<open>cp. HOL/SPARK/Tools/spark_commands.ML\<close>
3.93 +ML \<open>
3.94 +\<close> ML \<open>
3.95 +(*/--------------------------------- cp_spark_commands.ML ------------------------------------\*)
3.96 +(*\--------------------------------- cp_spark_commands.ML ------------------------------------/*)
3.97 +\<close> ML \<open>
3.98 +\<close>
3.99 +
3.100 +section \<open>setup command_keyword \<close>
3.101 +subsection \<open>hide for development, use for Test_Isac\<close>
3.102 +ML \<open>
3.103 type chars = (string * Position.T) list;
3.104 val e_chars = []: (string * Position.T) list;
3.105
3.106 fun spark_open (_: ((*Fdl_Lexer.*)chars -> 'a * (*Fdl_Lexer.*)chars))
3.107 - (_: ('b -> Token.file list * theory) * string) (_: 'b) = @{theory};
3.108 -spark_open: ((*Fdl_Lexer.*)chars -> 'a * (*Fdl_Lexer.*)chars) -> ('b -> Token.file list * theory) * string -> 'b -> theory;
3.109 + (_: ('b -> Token.file list * theory) * string) (_: 'b) = @{theory}
3.110
3.111 -(*===== dummy cp.from SPARK/Tools/fdl_lexer.ML *)
3.112 type banner = string * string * string; val e_banner = ("b1", "b2", "b3")
3.113 type date = string * string * string; val e_date = ("d1", "d2", "d3")
3.114 type time = string * string * string * string option; val e_time = ("t1", "t2", "t3", SOME "t4")
3.115
3.116 fun siv_header (_: chars) =
3.117 ((e_banner, (e_date, e_time), (e_date, e_time), ("", "")), e_chars);
3.118 -siv_header: chars ->
3.119 - (banner * (date * time) * (date * time) * (string * string)) * chars;
3.120 \<close> ML \<open>
3.121 +\<close>
3.122 +subsection \<open>def.for Build_Isac; for Test_Isac outcomment SPARK_Commands, Fdl_Lexer below\<close>
3.123 +ML \<open>
3.124 \<close> ML \<open>
3.125 -\<close> ML \<open>
3.126 -\<close> ML \<open>
3.127 -\<close> ML \<open>
3.128 +val _ =
3.129 + Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start Isac Calculation from a Formalise-file"
3.130 + (*preliminary from spark_open*)
3.131 + (Resources.provide_parse_files "spark_open" -- Parse.parname
3.132 +(** ) >> (Toplevel.theory o ((*SPARK_Commands.*)spark_open Fdl_Lexer.siv_header)));( **)
3.133 +(**) >> (Toplevel.theory o ((*SPARK_Commands.*)spark_open (*Fdl_Lexer.*)siv_header)));(**)
3.134 \<close> ML \<open>
3.135 \<close>
3.136
3.137 -section \<open>setup command_keyword \<close>
3.138 -(** ISAC **)
3.139 -ML \<open>
3.140 -\<close> ML \<open>
3.141 -val _ =
3.142 - Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start Isac Calculation from a Formalise-file"
3.143 - (*preliminary from spark_open*)
3.144 - (Resources.provide_parse_files "spark_open" -- Parse.parname
3.145 - >> (Toplevel.theory o (spark_open siv_header)));
3.146 -\<close> ML \<open>
3.147 -\<close> ML \<open>
3.148 -\<close>
3.149 +section \<open>Test: compare Example .. spark_open\<close>
3.150 +(** )
3.151 +Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close> ( *.str*)
3.152 +(*Output + ERROR:
3.153 +{a = "//--- ##1# spark_open", files = fn, header = fn, prfx = ""} (line 14 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")
3.154 +{a = "##1# spark_open: before call <files thy>, files = siv_header !"} (line 18 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")
3.155 +{a = "### provide_parse_files", fs =
3.156 + [{digest = "b34ac56c90f483e9cdd0f14dc45d5f703e40aa26", lines =
3.157 + ["[", " (", " [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\",", "\t \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\",",
3.158 + "\t \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\",", " \"AbleitungBiegelinie dy\"],", " (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])", " )",
3.159 + "]"],
3.160 + pos = {line=1, offset=1, file=~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str, id=-1818}, src_path =
3.161 + "/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str"}]} (line 241 of "PIDE/resources.ML")
3.162 +exception Bind raised (line 15 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")*)
3.163
3.164 +
3.165 +(*set theory imports "HOL-SPARK.SPARK"..* )
3.166 +spark_open \<open>/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
3.167 +( *Output + ERROR:
3.168 +{a = "//--- ##1# spark_open", files = fn, header = fn, prfx = ""} (line 14 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")
3.169 +{a = "##1# spark_open: before call \"files thy\", files = siv_header"} (line 18 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")
3.170 +No such file: "/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.str"\<^here>
3.171 +*)
3.172 end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/BridgeJEdit/cp_spark_commands.ML Wed Nov 04 09:59:30 2020 +0100
4.3 @@ -0,0 +1,40 @@
4.4 +(*/--------------------------------- cp_spark_commands.ML ------------------------------------\*)
4.5 +(* Title: src/Tools/isac/BridgeJEdit/cp_spark_commands.ML
4.6 + Author: Walther Neuper, JKU Linz
4.7 + (c) due to copyright terms
4.8 +
4.9 +Preliminary file for developing Outer_Syntax.command..Example from spark_open as a model.
4.10 +
4.11 +The file contains code from HOL/SPARK/Tools/spark_commands.ML, minimal for spark_open.
4.12 +The code is separated from Calculation.thy into this file,
4.13 +because text\<open>...\<close> and (*...*) for const_name>\<open>...\<close> etc and @{thms ...} causes errors.
4.14 +
4.15 +For Test_Isac (**)ML_file "cp_spark_commands.ML"(**) must be outcommented in Calculation.thy.
4.16 +*)
4.17 +
4.18 +fun spark_open header (files, prfx) thy =
4.19 +(*Fdl_Lexer.vcg_header ..^^^^^^ ^^^^^^^^^^^^^..from Resources.provide_parse_files: are all funs!*)
4.20 + let
4.21 +(**)val _ = @{print} {a = "//--- ##1# spark_open", files = files, header = header, prfx = prfx};(**)
4.22 + val xxx as ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file (*,.siv*)
4.23 +(* {lines = fdl_lines, pos = fdl_pos, ...}, ( *.fld*)
4.24 +(* {lines = rls_lines, pos = rls_pos, ...} ( *.rls*)
4.25 + ], thy') =
4.26 + (@{print} {a = "##1# spark_open: before call <files thy>, files = siv_header !"}; files thy);
4.27 +(* ^^^^^ arg!*)
4.28 + val path = fst (Path.split_ext src_path);
4.29 + in
4.30 +(**)@{print} {a = "##1# spark_open: result from siv_header, without thy'", fst_xxx = fst xxx};(**)
4.31 +(** )@{print} {a = "##1# spark_open: 3 args for SPARK_VCs.set_vcs",
4.32 + arg1 = (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines))),
4.33 + arg2 = (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines)),
4.34 + arg3 = (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines))),
4.35 + z = "\\--- ##1# spark_open"};( **)
4.36 +(** )(*SPARK_VCs.*)set_vcs
4.37 + (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
4.38 + (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines))
4.39 + (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines)))
4.40 + path prfx thy'
4.41 +( **) @{theory}
4.42 + end;
4.43 +(*\--------------------------------- cp_spark_commands.ML ------------------------------------/*)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Tools/isac/BridgeJEdit/cp_spark_vcs.ML Wed Nov 04 09:59:30 2020 +0100
5.3 @@ -0,0 +1,1015 @@
5.4 +(*/--------------------------------- cp_spark_vcs.ML -----------------------------------------\*)
5.5 +(* Title: src/Tools/isac/BridgeJEdit/cp_spark_vcs.ML
5.6 + Author: Walther Neuper, JKU Linz
5.7 + (c) due to copyright terms
5.8 +
5.9 +Preliminary file for developing Outer_Syntax.command..Example from spark_open as a model.
5.10 +
5.11 +The file contains code from HOL/SPARK/Tools/set_vcs.ML, minimal for set_vcs.
5.12 +The code is separated from Calculation.thy into this file,
5.13 +because text\<open>...\<close> and (*...*) for const_name>\<open>...\<close> etc and @{thms ...} causes errors.
5.14 +
5.15 +For Test_Isac (**)ML_file "cp_set_vcs.ML"(**) must be outcommented in Calculation.thy.
5.16 +*)
5.17 +
5.18 +(** theory data **)
5.19 +
5.20 +fun err_unfinished () = error "An unfinished SPARK environment is still open."
5.21 +
5.22 +val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
5.23 +
5.24 +val name_ord = prod_ord string_ord (option_ord int_ord) o
5.25 + apply2 (strip_number ##> Int.fromString);
5.26 +
5.27 +structure VCtab = Table(type key = string val ord = name_ord);
5.28 +
5.29 +structure VCs = Theory_Data
5.30 +(
5.31 + type T =
5.32 + {pfuns: ((string list * string) option * term) Symtab.table,
5.33 + type_map: (typ * (string * string) list) Symtab.table,
5.34 + env:
5.35 + {ctxt: Element.context_i list,
5.36 + defs: (binding * thm) list,
5.37 + types: Fdl_Parser.fdl_type Fdl_Parser.tab,
5.38 + funs: (string list * string) Fdl_Parser.tab,
5.39 + pfuns: ((string list * string) option * term) Symtab.table,
5.40 + ids: (term * string) Symtab.table * Name.context,
5.41 + proving: bool,
5.42 + vcs: (string * thm list option *
5.43 + (string * Fdl_Parser.expr) list * (string * Fdl_Parser.expr) list) VCtab.table,
5.44 + path: Path.T,
5.45 + prefix: string} option}
5.46 + val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
5.47 + val extend = I
5.48 + fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
5.49 + {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
5.50 + {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
5.51 + type_map = Symtab.merge (op =) (type_map1, type_map2),
5.52 + env = NONE}
5.53 + | merge _ = err_unfinished ()
5.54 +)
5.55 +
5.56 +(** utilities **)
5.57 +
5.58 +val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
5.59 +
5.60 +
5.61 +(** set up verification conditions **)
5.62 +
5.63 +fun partition_opt f =
5.64 + let
5.65 + fun part ys zs [] = (rev ys, rev zs)
5.66 + | part ys zs (x :: xs) = (case f x of
5.67 + SOME y => part (y :: ys) zs xs
5.68 + | NONE => part ys (x :: zs) xs)
5.69 + in part [] [] end;
5.70 +
5.71 +fun dest_def (id, (Fdl_Parser.Substitution_Rule ([], Fdl_Parser.Ident s, rhs))) = SOME (id, (s, rhs))
5.72 + | dest_def _ = NONE;
5.73 +
5.74 +
5.75 +val builtin = Symtab.make (map (rpair ())
5.76 + ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
5.77 + "+", "-", "*", "/", "div", "mod", "**"]);
5.78 +
5.79 +fun complex_expr (Fdl_Parser.Number _) = false
5.80 + | complex_expr (Fdl_Parser.Ident _) = false
5.81 + | complex_expr (Fdl_Parser.Funct (s, es)) =
5.82 + not (Symtab.defined builtin s) orelse exists complex_expr es
5.83 + | complex_expr (Fdl_Parser.Quantifier (_, _, _, e)) = complex_expr e
5.84 + | complex_expr _ = true;
5.85 +
5.86 +fun complex_rule (Fdl_Parser.Inference_Rule (es, e)) =
5.87 + complex_expr e orelse exists complex_expr es
5.88 + | complex_rule (Fdl_Parser.Substitution_Rule (es, e, e')) =
5.89 + complex_expr e orelse complex_expr e' orelse
5.90 + exists complex_expr es;
5.91 +
5.92 +fun is_trivial_vc ([], [(_, Fdl_Parser.Ident "true")]) = true
5.93 + | is_trivial_vc _ = false;
5.94 +
5.95 +
5.96 +fun rulenames rules = commas
5.97 + (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
5.98 +
5.99 +
5.100 +val is_pfun =
5.101 + Symtab.defined builtin orf
5.102 + can (unprefix "fld_") orf can (unprefix "upf_") orf
5.103 + can (unsuffix "__pos") orf can (unsuffix "__val") orf
5.104 + equal "succ" orf equal "pred";
5.105 +
5.106 +fun fold_opt f = the_default I o Option.map f;
5.107 +fun fold_pair f g (x, y) = f x #> g y;
5.108 +
5.109 +fun fold_expr f g (Fdl_Parser.Funct (s, es)) = f s #> fold (fold_expr f g) es
5.110 + | fold_expr f g (Fdl_Parser.Ident s) = g s
5.111 + | fold_expr f g (Fdl_Parser.Number _) = I
5.112 + | fold_expr f g (Fdl_Parser.Quantifier (_, _, _, e)) = fold_expr f g e
5.113 + | fold_expr f g (Fdl_Parser.Element (e, es)) =
5.114 + fold_expr f g e #> fold (fold_expr f g) es
5.115 + | fold_expr f g (Fdl_Parser.Update (e, es, e')) =
5.116 + fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
5.117 + | fold_expr f g (Fdl_Parser.Record (_, flds)) = fold (fold_expr f g o snd) flds
5.118 + | fold_expr f g (Fdl_Parser.Array (_, default, assocs)) =
5.119 + fold_opt (fold_expr f g) default #>
5.120 + fold (fold_pair
5.121 + (fold (fold (fold_pair
5.122 + (fold_expr f g) (fold_opt (fold_expr f g)))))
5.123 + (fold_expr f g)) assocs;
5.124 +
5.125 +
5.126 +fun add_expr_pfuns funs = fold_expr
5.127 + (fn s => if is_pfun s then I else insert (op =) s)
5.128 + (fn s => if is_none (Fdl_Parser.lookup funs s) then I else insert (op =) s);
5.129 +
5.130 +fun lookup_prfx "" tab s = Symtab.lookup tab s
5.131 + | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
5.132 + NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
5.133 + | x => x);
5.134 +
5.135 +fun fold_vcs f vcs =
5.136 + VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
5.137 +
5.138 +fun pfuns_of_vcs prfx funs pfuns vcs =
5.139 + fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
5.140 + filter (is_none o lookup_prfx prfx pfuns);
5.141 +
5.142 +val booleanN = "boolean";
5.143 +val integerN = "integer";
5.144 +
5.145 +
5.146 +fun get_type thy prfx ty =
5.147 + let val {type_map, ...} = VCs.get thy
5.148 + in lookup_prfx prfx type_map ty end;
5.149 +
5.150 +fun mk_type' _ _ "integer" = (HOLogic.intT, [])
5.151 + | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
5.152 + | mk_type' thy prfx ty =
5.153 + (case get_type thy prfx ty of
5.154 + NONE =>
5.155 + (Syntax.check_typ (Proof_Context.init_global thy)
5.156 + (Type (Sign.full_name thy (Binding.name ty), [])),
5.157 + [])
5.158 + | SOME p => p);
5.159 +
5.160 +fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
5.161 +
5.162 +fun check_no_assoc thy prfx s = case get_type thy prfx s of
5.163 + NONE => ()
5.164 + | SOME _ => error ("Cannot associate a type with " ^ s ^
5.165 + "\nsince it is no record or enumeration type");
5.166 +
5.167 +
5.168 +fun define_overloaded (def_name, eq) lthy =
5.169 + let
5.170 + val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
5.171 + Logic.dest_equals |>> dest_Free;
5.172 + val ((_, (_, thm)), lthy') = Local_Theory.define
5.173 + ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy
5.174 + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
5.175 + val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm
5.176 + in (thm', lthy') end;
5.177 +
5.178 +(** generate properties of enumeration types **)
5.179 +
5.180 +fun add_enum_type tyname tyname' thy =
5.181 + let
5.182 + val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname');
5.183 + val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
5.184 + val k = length cs;
5.185 + val T = Type (tyname', []);
5.186 + val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);
5.187 + val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);
5.188 + val card = Const (\<^const_name>\<open>card\<close>,
5.189 + HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
5.190 +
5.191 + fun mk_binrel_def s f = Logic.mk_equals
5.192 + (Const (s, T --> T --> HOLogic.boolT),
5.193 + Abs ("x", T, Abs ("y", T,
5.194 + Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $
5.195 + (f $ Bound 1) $ (f $ Bound 0))));
5.196 +
5.197 + val (((def1, def2), def3), lthy) = thy |>
5.198 +
5.199 + Class.instantiation ([tyname'], [], \<^sort>\<open>spark_enum\<close>) |>
5.200 +
5.201 + define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
5.202 + (p,
5.203 + list_comb (Const (case_name, replicate k HOLogic.intT @
5.204 + [T] ---> HOLogic.intT),
5.205 + map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
5.206 +
5.207 + define_overloaded ("less_eq_" ^ tyname ^ "_def",
5.208 + mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>
5.209 + define_overloaded ("less_" ^ tyname ^ "_def",
5.210 + mk_binrel_def \<^const_name>\<open>less\<close> p);
5.211 +
5.212 + val UNIV_eq = Goal.prove lthy [] []
5.213 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
5.214 + (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
5.215 + (fn {context = ctxt, ...} =>
5.216 + resolve_tac ctxt @{thms subset_antisym} 1 THEN
5.217 + resolve_tac ctxt @{thms subsetI} 1 THEN
5.218 + Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info
5.219 + (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
5.220 + ALLGOALS (asm_full_simp_tac ctxt));
5.221 +
5.222 + val finite_UNIV = Goal.prove lthy [] []
5.223 + (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,
5.224 + HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
5.225 + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
5.226 +
5.227 + val card_UNIV = Goal.prove lthy [] []
5.228 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
5.229 + (card, HOLogic.mk_number HOLogic.natT k)))
5.230 + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
5.231 +
5.232 + val range_pos = Goal.prove lthy [] []
5.233 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
5.234 + (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->
5.235 + HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
5.236 + p $ HOLogic.mk_UNIV T,
5.237 + Const (\<^const_name>\<open>atLeastLessThan\<close>, HOLogic.intT -->
5.238 + HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
5.239 + HOLogic.mk_number HOLogic.intT 0 $
5.240 + (\<^term>\<open>int\<close> $ card))))
5.241 + (fn {context = ctxt, ...} =>
5.242 + simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
5.243 + simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
5.244 + resolve_tac ctxt @{thms subset_antisym} 1 THEN
5.245 + simp_tac ctxt 1 THEN
5.246 + resolve_tac ctxt @{thms subsetI} 1 THEN
5.247 + asm_full_simp_tac (ctxt addsimps @{thms interval_expand}
5.248 + delsimps @{thms atLeastLessThan_iff}) 1);
5.249 +
5.250 + val lthy' =
5.251 + Class.prove_instantiation_instance (fn ctxt =>
5.252 + Class.intro_classes_tac ctxt [] THEN
5.253 + resolve_tac ctxt [finite_UNIV] 1 THEN
5.254 + resolve_tac ctxt [range_pos] 1 THEN
5.255 + simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN
5.256 + simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;
5.257 +
5.258 + val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>
5.259 + let
5.260 + val n = HOLogic.mk_number HOLogic.intT i;
5.261 + val th = Goal.prove lthy' [] []
5.262 + (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))
5.263 + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1);
5.264 + val th' = Goal.prove lthy' [] []
5.265 + (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))
5.266 + (fn {context = ctxt, ...} =>
5.267 + resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN
5.268 + simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
5.269 + in (th, th') end) cs);
5.270 +
5.271 + val first_el = Goal.prove lthy' [] []
5.272 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
5.273 + (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))
5.274 + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
5.275 +
5.276 + val last_el = Goal.prove lthy' [] []
5.277 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
5.278 + (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))
5.279 + (fn {context = ctxt, ...} =>
5.280 + simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
5.281 + in
5.282 + lthy' |>
5.283 + Local_Theory.note
5.284 + ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>>
5.285 + Local_Theory.note
5.286 + ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>>
5.287 + Local_Theory.note
5.288 + ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>>
5.289 + Local_Theory.note
5.290 + ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>>
5.291 + Local_Theory.note
5.292 + ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |>
5.293 + Local_Theory.exit_global
5.294 + end;
5.295 +
5.296 +
5.297 +val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
5.298 +
5.299 +fun check_enum [] [] = NONE
5.300 + | check_enum els [] = SOME ("has no element(s) " ^ commas els)
5.301 + | check_enum [] cs = SOME ("has extra element(s) " ^
5.302 + commas (map (Long_Name.base_name o fst) cs))
5.303 + | check_enum (el :: els) ((cname, _) :: cs) =
5.304 + if lcase_eq (el, cname) then check_enum els cs
5.305 + else SOME ("either has no element " ^ el ^
5.306 + " or it is at the wrong position");
5.307 +
5.308 +fun strip_prfx s =
5.309 + let
5.310 + fun strip ys [] = ("", implode ys)
5.311 + | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)
5.312 + | strip ys (x :: xs) = strip (x :: ys) xs
5.313 + in strip [] (rev (raw_explode s)) end;
5.314 +
5.315 +fun assoc_ty_err thy T s msg =
5.316 + error ("Type " ^ Syntax.string_of_typ_global thy T ^
5.317 + " associated with SPARK type " ^ s ^ "\n" ^ msg);
5.318 +
5.319 +fun check_enum [] [] = NONE
5.320 + | check_enum els [] = SOME ("has no element(s) " ^ commas els)
5.321 + | check_enum [] cs = SOME ("has extra element(s) " ^
5.322 + commas (map (Long_Name.base_name o fst) cs))
5.323 + | check_enum (el :: els) ((cname, _) :: cs) =
5.324 + if lcase_eq (el, cname) then check_enum els cs
5.325 + else SOME ("either has no element " ^ el ^
5.326 + " or it is at the wrong position");
5.327 +
5.328 +fun unprefix_pfun "" s = s
5.329 + | unprefix_pfun prfx s =
5.330 + let val (prfx', s') = strip_prfx s
5.331 + in if prfx = prfx' then s' else s end;
5.332 +
5.333 +fun invert_map [] = I
5.334 + | invert_map cmap =
5.335 + map (apfst (the o AList.lookup (op =) (map swap cmap)));
5.336 +
5.337 +fun get_record_info thy T = (case Record.dest_recTs T of
5.338 + [(tyname, [\<^typ>\<open>unit\<close>])] =>
5.339 + Record.get_info thy (Long_Name.qualifier tyname)
5.340 + | _ => NONE);
5.341 +
5.342 +
5.343 +
5.344 +fun add_type_def prfx (s, Fdl_Parser.Basic_Type ty) (ids, thy) =
5.345 + (check_no_assoc thy prfx s;
5.346 + (ids,
5.347 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
5.348 + (mk_type thy prfx ty) thy |> snd))
5.349 +
5.350 + | add_type_def prfx (s, Fdl_Parser.Enum_Type els) ((tab, ctxt), thy) =
5.351 + let
5.352 + val (thy', tyname) = (case get_type thy prfx s of
5.353 + NONE =>
5.354 + let
5.355 + val tyb = Binding.name s;
5.356 + val tyname = Sign.full_name thy tyb
5.357 + in
5.358 + (thy |>
5.359 + BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
5.360 + [((tyb, [], NoSyn),
5.361 + map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
5.362 + add_enum_type s tyname,
5.363 + tyname)
5.364 + end
5.365 + | SOME (T as Type (tyname, []), cmap) =>
5.366 + (case BNF_LFP_Compat.get_constrs thy tyname of
5.367 + NONE => assoc_ty_err thy T s "is not a datatype"
5.368 + | SOME cs =>
5.369 + let val (prfx', _) = strip_prfx s
5.370 + in
5.371 + case check_enum (map (unprefix_pfun prfx') els)
5.372 + (invert_map cmap cs) of
5.373 + NONE => (thy, tyname)
5.374 + | SOME msg => assoc_ty_err thy T s msg
5.375 + end)
5.376 + | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
5.377 + val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));
5.378 + in
5.379 + ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
5.380 + fold Name.declare els ctxt),
5.381 + thy')
5.382 + end
5.383 +
5.384 + | add_type_def prfx (s, Fdl_Parser.Array_Type (argtys, resty)) (ids, thy) =
5.385 + (check_no_assoc thy prfx s;
5.386 + (ids,
5.387 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
5.388 + (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->
5.389 + mk_type thy prfx resty) thy |> snd))
5.390 +
5.391 + | add_type_def prfx (s, Fdl_Parser.Record_Type fldtys) (ids, thy) =
5.392 + (ids,
5.393 + let val fldTs = maps (fn (flds, ty) =>
5.394 + map (rpair (mk_type thy prfx ty)) flds) fldtys
5.395 + in case get_type thy prfx s of
5.396 + NONE =>
5.397 + Record.add_record {overloaded = false} ([], Binding.name s) NONE
5.398 + (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
5.399 + | SOME (rT, cmap) =>
5.400 + (case get_record_info thy rT of
5.401 + NONE => assoc_ty_err thy rT s "is not a record type"
5.402 + | SOME {fields, ...} =>
5.403 + let val fields' = invert_map cmap fields
5.404 + in
5.405 + (case subtract (lcase_eq o apply2 fst) fldTs fields' of
5.406 + [] => ()
5.407 + | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
5.408 + commas (map (Long_Name.base_name o fst) flds));
5.409 + map (fn (fld, T) =>
5.410 + case AList.lookup lcase_eq fields' fld of
5.411 + NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
5.412 + | SOME U => T = U orelse assoc_ty_err thy rT s
5.413 + ("has field " ^
5.414 + fld ^ " whose type\n" ^
5.415 + Syntax.string_of_typ_global thy U ^
5.416 + "\ndoes not match declared type\n" ^
5.417 + Syntax.string_of_typ_global thy T)) fldTs;
5.418 + thy)
5.419 + end)
5.420 + end)
5.421 +
5.422 + | add_type_def prfx (s, Fdl_Parser.Pending_Type) (ids, thy) =
5.423 + (ids,
5.424 + case get_type thy prfx s of
5.425 + SOME _ => thy
5.426 + | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);
5.427 +
5.428 +fun add_type_def prfx (s, Fdl_Parser.Basic_Type ty) (ids, thy) =
5.429 + (check_no_assoc thy prfx s;
5.430 + (ids,
5.431 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
5.432 + (mk_type thy prfx ty) thy |> snd))
5.433 +
5.434 + | add_type_def prfx (s, Fdl_Parser.Enum_Type els) ((tab, ctxt), thy) =
5.435 + let
5.436 + val (thy', tyname) = (case get_type thy prfx s of
5.437 + NONE =>
5.438 + let
5.439 + val tyb = Binding.name s;
5.440 + val tyname = Sign.full_name thy tyb
5.441 + in
5.442 + (thy |>
5.443 + BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
5.444 + [((tyb, [], NoSyn),
5.445 + map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
5.446 + add_enum_type s tyname,
5.447 + tyname)
5.448 + end
5.449 + | SOME (T as Type (tyname, []), cmap) =>
5.450 + (case BNF_LFP_Compat.get_constrs thy tyname of
5.451 + NONE => assoc_ty_err thy T s "is not a datatype"
5.452 + | SOME cs =>
5.453 + let val (prfx', _) = strip_prfx s
5.454 + in
5.455 + case check_enum (map (unprefix_pfun prfx') els)
5.456 + (invert_map cmap cs) of
5.457 + NONE => (thy, tyname)
5.458 + | SOME msg => assoc_ty_err thy T s msg
5.459 + end)
5.460 + | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
5.461 + val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));
5.462 + in
5.463 + ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
5.464 + fold Name.declare els ctxt),
5.465 + thy')
5.466 + end
5.467 +
5.468 + | add_type_def prfx (s, Fdl_Parser.Array_Type (argtys, resty)) (ids, thy) =
5.469 + (check_no_assoc thy prfx s;
5.470 + (ids,
5.471 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
5.472 + (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->
5.473 + mk_type thy prfx resty) thy |> snd))
5.474 +
5.475 + | add_type_def prfx (s, Fdl_Parser.Record_Type fldtys) (ids, thy) =
5.476 + (ids,
5.477 + let val fldTs = maps (fn (flds, ty) =>
5.478 + map (rpair (mk_type thy prfx ty)) flds) fldtys
5.479 + in case get_type thy prfx s of
5.480 + NONE =>
5.481 + Record.add_record {overloaded = false} ([], Binding.name s) NONE
5.482 + (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
5.483 + | SOME (rT, cmap) =>
5.484 + (case get_record_info thy rT of
5.485 + NONE => assoc_ty_err thy rT s "is not a record type"
5.486 + | SOME {fields, ...} =>
5.487 + let val fields' = invert_map cmap fields
5.488 + in
5.489 + (case subtract (lcase_eq o apply2 fst) fldTs fields' of
5.490 + [] => ()
5.491 + | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
5.492 + commas (map (Long_Name.base_name o fst) flds));
5.493 + map (fn (fld, T) =>
5.494 + case AList.lookup lcase_eq fields' fld of
5.495 + NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
5.496 + | SOME U => T = U orelse assoc_ty_err thy rT s
5.497 + ("has field " ^
5.498 + fld ^ " whose type\n" ^
5.499 + Syntax.string_of_typ_global thy U ^
5.500 + "\ndoes not match declared type\n" ^
5.501 + Syntax.string_of_typ_global thy T)) fldTs;
5.502 + thy)
5.503 + end)
5.504 + end)
5.505 +
5.506 + | add_type_def prfx (s, Fdl_Parser.Pending_Type) (ids, thy) =
5.507 + (ids,
5.508 + case get_type thy prfx s of
5.509 + SOME _ => thy
5.510 + | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);
5.511 +
5.512 +fun add_const prfx (s, ty) ((tab, ctxt), thy) =
5.513 + let
5.514 + val T = mk_type thy prfx ty;
5.515 + val b = Binding.name s;
5.516 + val c = Const (Sign.full_name thy b, T)
5.517 + in
5.518 + (c,
5.519 + ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
5.520 + Sign.add_consts [(b, T, NoSyn)] thy))
5.521 + end;
5.522 +
5.523 +fun mk_unop s t =
5.524 + let val T = fastype_of t
5.525 + in Const (s, T --> T) $ t end;
5.526 +
5.527 +fun strip_underscores s =
5.528 + strip_underscores (unsuffix "_" s) handle Fail _ => s;
5.529 +
5.530 +fun strip_tilde s =
5.531 + unsuffix "~" s ^ "_init" handle Fail _ => s;
5.532 +
5.533 +val mangle_name = strip_underscores #> strip_tilde;
5.534 +
5.535 +fun mk_variables thy prfx xs ty (tab, ctxt) =
5.536 + let
5.537 + val T = mk_type thy prfx ty;
5.538 + val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
5.539 + val zs = map (Free o rpair T) ys;
5.540 + in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
5.541 +
5.542 +fun find_field [] fname fields =
5.543 + find_first (curry lcase_eq fname o fst) fields
5.544 + | find_field cmap fname fields =
5.545 + (case AList.lookup (op =) cmap fname of
5.546 + NONE => NONE
5.547 + | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
5.548 +
5.549 +fun find_field' fname = get_first (fn (flds, fldty) =>
5.550 + if member (op =) flds fname then SOME fldty else NONE);
5.551 +
5.552 +fun mk_times (t, u) =
5.553 + let
5.554 + val setT = fastype_of t;
5.555 + val T = HOLogic.dest_setT setT;
5.556 + val U = HOLogic.dest_setT (fastype_of u)
5.557 + in
5.558 + Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
5.559 + HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
5.560 + end;
5.561 +
5.562 +
5.563 +fun term_of_expr thy prfx types pfuns =
5.564 + let
5.565 + fun tm_of vs (Fdl_Parser.Funct ("->", [e, e'])) =
5.566 + (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.567 +
5.568 + | tm_of vs (Fdl_Parser.Funct ("<->", [e, e'])) =
5.569 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.570 +
5.571 + | tm_of vs (Fdl_Parser.Funct ("or", [e, e'])) =
5.572 + (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.573 +
5.574 + | tm_of vs (Fdl_Parser.Funct ("and", [e, e'])) =
5.575 + (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.576 +
5.577 + | tm_of vs (Fdl_Parser.Funct ("not", [e])) =
5.578 + (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
5.579 +
5.580 + | tm_of vs (Fdl_Parser.Funct ("=", [e, e'])) =
5.581 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.582 +
5.583 + | tm_of vs (Fdl_Parser.Funct ("<>", [e, e'])) = (HOLogic.mk_not
5.584 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
5.585 +
5.586 + | tm_of vs (Fdl_Parser.Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
5.587 + (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.588 +
5.589 + | tm_of vs (Fdl_Parser.Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
5.590 + (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
5.591 +
5.592 + | tm_of vs (Fdl_Parser.Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
5.593 + (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
5.594 +
5.595 + | tm_of vs (Fdl_Parser.Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
5.596 + (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
5.597 +
5.598 + | tm_of vs (Fdl_Parser.Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
5.599 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
5.600 +
5.601 + | tm_of vs (Fdl_Parser.Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
5.602 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
5.603 +
5.604 + | tm_of vs (Fdl_Parser.Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
5.605 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
5.606 +
5.607 + | tm_of vs (Fdl_Parser.Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
5.608 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
5.609 +
5.610 + | tm_of vs (Fdl_Parser.Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
5.611 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
5.612 +
5.613 + | tm_of vs (Fdl_Parser.Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
5.614 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
5.615 +
5.616 + | tm_of vs (Fdl_Parser.Funct ("-", [e])) =
5.617 + (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
5.618 +
5.619 + | tm_of vs (Fdl_Parser.Funct ("**", [e, e'])) =
5.620 + (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
5.621 + HOLogic.intT) $ fst (tm_of vs e) $
5.622 + (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
5.623 +
5.624 + | tm_of (tab, _) (Fdl_Parser.Ident s) =
5.625 + (case Symtab.lookup tab s of
5.626 + SOME t_ty => t_ty
5.627 + | NONE => (case lookup_prfx prfx pfuns s of
5.628 + SOME (SOME ([], resty), t) => (t, resty)
5.629 + | _ => error ("Undeclared identifier " ^ s)))
5.630 +
5.631 + | tm_of _ (Fdl_Parser.Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
5.632 +
5.633 + | tm_of vs (Fdl_Parser.Quantifier (s, xs, ty, e)) =
5.634 + let
5.635 + val (ys, vs') = mk_variables thy prfx xs ty vs;
5.636 + val q = (case s of
5.637 + "for_all" => HOLogic.mk_all
5.638 + | "for_some" => HOLogic.mk_exists)
5.639 + in
5.640 + (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
5.641 + ys (fst (tm_of vs' e)),
5.642 + booleanN)
5.643 + end
5.644 +
5.645 + | tm_of vs (Fdl_Parser.Funct (s, es)) =
5.646 +
5.647 + (* record field selection *)
5.648 + (case try (unprefix "fld_") s of
5.649 + SOME fname => (case es of
5.650 + [e] =>
5.651 + let
5.652 + val (t, rcdty) = tm_of vs e;
5.653 + val (rT, cmap) = mk_type' thy prfx rcdty
5.654 + in case (get_record_info thy rT, Fdl_Parser.lookup types rcdty) of
5.655 + (SOME {fields, ...}, SOME (Fdl_Parser.Record_Type fldtys)) =>
5.656 + (case (find_field cmap fname fields,
5.657 + find_field' fname fldtys) of
5.658 + (SOME (fname', fT), SOME fldty) =>
5.659 + (Const (fname', rT --> fT) $ t, fldty)
5.660 + | _ => error ("Record " ^ rcdty ^
5.661 + " has no field named " ^ fname))
5.662 + | _ => error (rcdty ^ " is not a record type")
5.663 + end
5.664 + | _ => error ("Function " ^ s ^ " expects one argument"))
5.665 + | NONE =>
5.666 +
5.667 + (* record field update *)
5.668 + (case try (unprefix "upf_") s of
5.669 + SOME fname => (case es of
5.670 + [e, e'] =>
5.671 + let
5.672 + val (t, rcdty) = tm_of vs e;
5.673 + val (rT, cmap) = mk_type' thy prfx rcdty;
5.674 + val (u, fldty) = tm_of vs e';
5.675 + val fT = mk_type thy prfx fldty
5.676 + in case get_record_info thy rT of
5.677 + SOME {fields, ...} =>
5.678 + (case find_field cmap fname fields of
5.679 + SOME (fname', fU) =>
5.680 + if fT = fU then
5.681 + (Const (fname' ^ "_update",
5.682 + (fT --> fT) --> rT --> rT) $
5.683 + Abs ("x", fT, u) $ t,
5.684 + rcdty)
5.685 + else error ("Type\n" ^
5.686 + Syntax.string_of_typ_global thy fT ^
5.687 + "\ndoes not match type\n" ^
5.688 + Syntax.string_of_typ_global thy fU ^
5.689 + "\nof field " ^ fname)
5.690 + | NONE => error ("Record " ^ rcdty ^
5.691 + " has no field named " ^ fname))
5.692 + | _ => error (rcdty ^ " is not a record type")
5.693 + end
5.694 + | _ => error ("Function " ^ s ^ " expects two arguments"))
5.695 + | NONE =>
5.696 +
5.697 + (* enumeration type to integer *)
5.698 + (case try (unsuffix "__pos") s of
5.699 + SOME tyname => (case es of
5.700 + [e] => (Const (\<^const_name>\<open>pos\<close>,
5.701 + mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
5.702 + integerN)
5.703 + | _ => error ("Function " ^ s ^ " expects one argument"))
5.704 + | NONE =>
5.705 +
5.706 + (* integer to enumeration type *)
5.707 + (case try (unsuffix "__val") s of
5.708 + SOME tyname => (case es of
5.709 + [e] => (Const (\<^const_name>\<open>val\<close>,
5.710 + HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
5.711 + tyname)
5.712 + | _ => error ("Function " ^ s ^ " expects one argument"))
5.713 + | NONE =>
5.714 +
5.715 + (* successor / predecessor of enumeration type element *)
5.716 + if s = "succ" orelse s = "pred" then (case es of
5.717 + [e] =>
5.718 + let
5.719 + val (t, tyname) = tm_of vs e;
5.720 + val T = mk_type thy prfx tyname
5.721 + in (Const
5.722 + (if s = "succ" then \<^const_name>\<open>succ\<close>
5.723 + else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
5.724 + end
5.725 + | _ => error ("Function " ^ s ^ " expects one argument"))
5.726 +
5.727 + (* user-defined proof function *)
5.728 + else
5.729 + (case lookup_prfx prfx pfuns s of
5.730 + SOME (SOME (_, resty), t) =>
5.731 + (list_comb (t, map (fst o tm_of vs) es), resty)
5.732 + | _ => error ("Undeclared proof function " ^ s))))))
5.733 +
5.734 + | tm_of vs (Fdl_Parser.Element (e, es)) =
5.735 + let val (t, ty) = tm_of vs e
5.736 + in case Fdl_Parser.lookup types ty of
5.737 + SOME (Fdl_Parser.Array_Type (_, elty)) =>
5.738 + (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
5.739 + | _ => error (ty ^ " is not an array type")
5.740 + end
5.741 +
5.742 + | tm_of vs (Fdl_Parser.Update (e, es, e')) =
5.743 + let val (t, ty) = tm_of vs e
5.744 + in case Fdl_Parser.lookup types ty of
5.745 + SOME (Fdl_Parser.Array_Type (idxtys, elty)) =>
5.746 + let
5.747 + val T = foldr1 HOLogic.mk_prodT
5.748 + (map (mk_type thy prfx) idxtys);
5.749 + val U = mk_type thy prfx elty;
5.750 + val fT = T --> U
5.751 + in
5.752 + (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
5.753 + t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
5.754 + fst (tm_of vs e'),
5.755 + ty)
5.756 + end
5.757 + | _ => error (ty ^ " is not an array type")
5.758 + end
5.759 +
5.760 + | tm_of vs (Fdl_Parser.Record (s, flds)) =
5.761 + let
5.762 + val (T, cmap) = mk_type' thy prfx s;
5.763 + val {extension = (ext_name, _), fields, ...} =
5.764 + (case get_record_info thy T of
5.765 + NONE => error (s ^ " is not a record type")
5.766 + | SOME info => info);
5.767 + val flds' = map (apsnd (tm_of vs)) flds;
5.768 + val fnames = fields |> invert_map cmap |>
5.769 + map (Long_Name.base_name o fst);
5.770 + val fnames' = map fst flds;
5.771 + val (fvals, ftys) = split_list (map (fn s' =>
5.772 + case AList.lookup lcase_eq flds' s' of
5.773 + SOME fval_ty => fval_ty
5.774 + | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
5.775 + fnames);
5.776 + val _ = (case subtract lcase_eq fnames fnames' of
5.777 + [] => ()
5.778 + | xs => error ("Extra field(s) " ^ commas xs ^
5.779 + " in record " ^ s));
5.780 + val _ = (case duplicates (op =) fnames' of
5.781 + [] => ()
5.782 + | xs => error ("Duplicate field(s) " ^ commas xs ^
5.783 + " in record " ^ s))
5.784 + in
5.785 + (list_comb
5.786 + (Const (ext_name,
5.787 + map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
5.788 + fvals @ [HOLogic.unit]),
5.789 + s)
5.790 + end
5.791 +
5.792 + | tm_of vs (Fdl_Parser.Array (s, default, assocs)) =
5.793 + (case Fdl_Parser.lookup types s of
5.794 + SOME (Fdl_Parser.Array_Type (idxtys, elty)) =>
5.795 + let
5.796 + val Ts = map (mk_type thy prfx) idxtys;
5.797 + val T = foldr1 HOLogic.mk_prodT Ts;
5.798 + val U = mk_type thy prfx elty;
5.799 + fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
5.800 + | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
5.801 + T --> T --> HOLogic.mk_setT T) $
5.802 + fst (tm_of vs e) $ fst (tm_of vs e');
5.803 + fun mk_idx idx =
5.804 + if length Ts <> length idx then
5.805 + error ("Arity mismatch in construction of array " ^ s)
5.806 + else foldr1 mk_times (map2 mk_idx' Ts idx);
5.807 + fun mk_upd (idxs, e) t =
5.808 + if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
5.809 + then
5.810 + Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
5.811 + T --> U --> T --> U) $ t $
5.812 + foldl1 HOLogic.mk_prod
5.813 + (map (fst o tm_of vs o fst) (hd idxs)) $
5.814 + fst (tm_of vs e)
5.815 + else
5.816 + Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
5.817 + HOLogic.mk_setT T --> U --> T --> U) $ t $
5.818 + foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
5.819 + (map mk_idx idxs) $
5.820 + fst (tm_of vs e)
5.821 + in
5.822 + (fold mk_upd assocs
5.823 + (case default of
5.824 + SOME e => Abs ("x", T, fst (tm_of vs e))
5.825 + | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
5.826 + s)
5.827 + end
5.828 + | _ => error (s ^ " is not an array type"))
5.829 +
5.830 + in tm_of end;
5.831 +
5.832 +
5.833 +fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);
5.834 +
5.835 +
5.836 +fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
5.837 + (case Fdl_Parser.lookup consts s of
5.838 + SOME ty =>
5.839 + let
5.840 + val (t, ty') = term_of_expr thy prfx types pfuns ids e;
5.841 + val T = mk_type thy prfx ty;
5.842 + val T' = mk_type thy prfx ty';
5.843 + val _ = T = T' orelse
5.844 + error ("Declared type " ^ ty ^ " of " ^ s ^
5.845 + "\ndoes not match type " ^ ty' ^ " in definition");
5.846 + val id' = mk_rulename id;
5.847 + val ((t', (_, th)), lthy') = Named_Target.theory_init thy
5.848 + |> Specification.definition NONE [] []
5.849 + ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
5.850 + val phi =
5.851 + Proof_Context.export_morphism lthy'
5.852 + (Proof_Context.init_global (Proof_Context.theory_of lthy'));
5.853 + in
5.854 + ((id', Morphism.thm phi th),
5.855 + ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt),
5.856 + Local_Theory.exit_global lthy'))
5.857 + end
5.858 + | NONE => error ("Undeclared constant " ^ s));
5.859 +
5.860 +
5.861 +
5.862 +val add_expr_idents = fold_expr (K I) (insert (op =));
5.863 +
5.864 +(* sort definitions according to their dependency *)
5.865 +fun sort_defs _ _ _ _ [] sdefs = rev sdefs
5.866 + | sort_defs prfx funs pfuns consts defs sdefs =
5.867 + (case find_first (fn (_, (_, e)) =>
5.868 + forall (is_some o lookup_prfx prfx pfuns)
5.869 + (add_expr_pfuns funs e []) andalso
5.870 + forall (fn id =>
5.871 + member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
5.872 + consts id)
5.873 + (add_expr_idents e [])) defs of
5.874 + SOME d => sort_defs prfx funs pfuns consts
5.875 + (remove (op =) d defs) (d :: sdefs)
5.876 + | NONE => error ("Bad definitions: " ^ rulenames defs));
5.877 +
5.878 +fun add_var prfx (s, ty) (ids, thy) =
5.879 + let val ([Free p], ids') = mk_variables thy prfx [s] ty ids
5.880 + in (p, (ids', thy)) end;
5.881 +
5.882 +fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =
5.883 + fold_map (add_var prfx)
5.884 + (map_filter
5.885 + (fn s => case try (unsuffix "~") s of
5.886 + SOME s' => (case Symtab.lookup tab s' of
5.887 + SOME (_, ty) => SOME (s, ty)
5.888 + | NONE => error ("Undeclared identifier " ^ s'))
5.889 + | NONE => NONE)
5.890 + (fold_vcs (add_expr_idents o snd) vcs []))
5.891 + ids_thy;
5.892 +
5.893 +fun term_of_rule thy prfx types pfuns ids rule =
5.894 + let val tm_of = fst o term_of_expr thy prfx types pfuns ids
5.895 + in case rule of
5.896 + Fdl_Parser.Inference_Rule (es, e) => Logic.list_implies
5.897 + (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))
5.898 + | Fdl_Parser.Substitution_Rule (es, e, e') => Logic.list_implies
5.899 + (map (HOLogic.mk_Trueprop o tm_of) es,
5.900 + HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e')))
5.901 + end;
5.902 +
5.903 +
5.904 +fun pfun_type thy prfx (argtys, resty) =
5.905 + map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
5.906 +
5.907 +fun check_pfun_type thy prfx s t optty1 optty2 =
5.908 + let
5.909 + val T = fastype_of t;
5.910 + fun check ty =
5.911 + let val U = pfun_type thy prfx ty
5.912 + in
5.913 + T = U orelse
5.914 + error ("Type\n" ^
5.915 + Syntax.string_of_typ_global thy T ^
5.916 + "\nof function " ^
5.917 + Syntax.string_of_term_global thy t ^
5.918 + " associated with proof function " ^ s ^
5.919 + "\ndoes not match declared type\n" ^
5.920 + Syntax.string_of_typ_global thy U)
5.921 + end
5.922 + in (Option.map check optty1; Option.map check optty2; ()) end;
5.923 +
5.924 +fun upd_option x y = if is_some x then x else y;
5.925 +
5.926 +fun check_pfuns_types thy prfx funs =
5.927 + Symtab.map (fn s => fn (optty, t) =>
5.928 + let val optty' = Fdl_Parser.lookup funs (unprefix_pfun prfx s)
5.929 + in
5.930 + (check_pfun_type thy prfx s t optty optty';
5.931 + (NONE |> upd_option optty |> upd_option optty', t))
5.932 + end);
5.933 +
5.934 +
5.935 +
5.936 +
5.937 +fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);
5.938 +
5.939 +fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
5.940 + | pp_open_vcs vcs = pp_vcs
5.941 + "The following verification conditions remain to be proved:" vcs;
5.942 +
5.943 +fun partition_vcs vcs = VCtab.fold_rev
5.944 + (fn (name, (trace, SOME thms, ps, cs)) =>
5.945 + apfst (cons (name, (trace, thms, ps, cs)))
5.946 + | (name, (trace, NONE, ps, cs)) =>
5.947 + apsnd (cons (name, (trace, ps, cs))))
5.948 + vcs ([], []);
5.949 +
5.950 +fun print_open_vcs f vcs =
5.951 + (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
5.952 +
5.953 +fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
5.954 + {pfuns, type_map, env = NONE} =>
5.955 + {pfuns = pfuns,
5.956 + type_map = type_map,
5.957 + env = SOME
5.958 + {ctxt = ctxt, defs = defs, types = types, funs = funs,
5.959 + pfuns = check_pfuns_types thy prefix funs pfuns,
5.960 + ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,
5.961 + prefix = prefix}}
5.962 + | _ => err_unfinished ()) thy;
5.963 +
5.964 +fun set_vcs ({types, vars, consts, funs} : Fdl_Parser.decls)
5.965 + (rules, _) ((_, ident), vcs) path opt_prfx thy =
5.966 + let
5.967 + val prfx' =
5.968 + if opt_prfx = "" then
5.969 + space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))
5.970 + else opt_prfx;
5.971 + val prfx = to_lower prfx';
5.972 + val {pfuns, ...} = VCs.get thy;
5.973 + val (defs, rules') = partition_opt dest_def rules;
5.974 + val consts' =
5.975 + subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (Fdl_Parser.items consts);
5.976 + (* ignore all complex rules in rls files *)
5.977 + val (rules'', other_rules) =
5.978 + List.partition (complex_rule o snd) rules';
5.979 + val _ = if null rules'' then ()
5.980 + else warning ("Ignoring rules: " ^ rulenames rules'');
5.981 +
5.982 + val vcs' = VCtab.make (maps (fn (tr, vcs) =>
5.983 + map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))
5.984 + (filter_out (is_trivial_vc o snd) vcs)) vcs);
5.985 +
5.986 + val _ = (case filter_out (is_some o Fdl_Parser.lookup funs)
5.987 + (pfuns_of_vcs prfx funs pfuns vcs') of
5.988 + [] => ()
5.989 + | fs => error ("Undeclared proof function(s) " ^ commas fs));
5.990 +
5.991 + val (((defs', vars''), ivars), (ids, thy')) =
5.992 + ((Symtab.empty |>
5.993 + Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
5.994 + Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),
5.995 + Name.context),
5.996 + thy |> Sign.add_path
5.997 + ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
5.998 + fold (add_type_def prfx) (Fdl_Parser.items types) |>
5.999 + fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
5.1000 + ids_thy |>
5.1001 + fold_map (add_def prfx types pfuns consts)
5.1002 + (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
5.1003 + fold_map (add_var prfx) (Fdl_Parser.items vars) ||>>
5.1004 + add_init_vars prfx vcs');
5.1005 +
5.1006 + val ctxt =
5.1007 + [Element.Fixes (map (fn (s, T) =>
5.1008 + (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),
5.1009 + Element.Assumes (map (fn (id, rl) =>
5.1010 + ((mk_rulename id, []),
5.1011 + [(term_of_rule thy' prfx types pfuns ids rl, [])]))
5.1012 + other_rules),
5.1013 + Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
5.1014 +
5.1015 + in
5.1016 + set_env ctxt defs' types funs ids vcs' path prfx thy'
5.1017 + end;
5.1018 +(*\--------------------------------- cp_spark_vcs.ML -----------------------------------------/*)
6.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Mon Nov 02 15:16:07 2020 +0100
6.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Wed Nov 04 09:59:30 2020 +0100
6.3 @@ -213,6 +213,12 @@
6.4
6.5 (**** parse Formalise ****)
6.6
6.7 +(*** tools from HOL/SPARK/Tools/fdl_lexer.ML, fdl_parser.ML ***)
6.8 +
6.9 +(* TODO *)
6.10 +
6.11 +(*** the parser ***)
6.12 +
6.13 val form_single =
6.14 Parse.$$$ "(" --
6.15 (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --
6.16 @@ -227,8 +233,18 @@
6.17 Parse.$$$ ")"
6.18
6.19 type formalise =
6.20 - ((((((((((string * string list) * string) * string) * string) * string) * string list) *
6.21 - string) * string list) * string) * string) list
6.22 +( (((((((((string(*.."("*)*
6.23 + string list(*..Formalise.model*)) *
6.24 + string(*..","*)) *
6.25 + string(*.."("*)) *
6.26 + string(*..theory*)) *
6.27 + string(*..","*)) *
6.28 + string list(*..Problem.id*)) *
6.29 + string(*..","*)) *
6.30 + string list(*..Method.id*)) *
6.31 + string(*..")"*)) *
6.32 + string(*..")"*))
6.33 +list; (*..form_single list*)
6.34
6.35 val formalise = (Parse.$$$ "[" |-- Parse.list1 form_single --| Parse.$$$ "]")
6.36
7.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Nov 02 15:16:07 2020 +0100
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Nov 04 09:59:30 2020 +0100
7.3 @@ -22,10 +22,10 @@
7.4 val keref2xml : int -> Ptool.ketype -> Ptool.kestoreID -> xml
7.5 val model2xml :
7.6 int -> I_Model.T -> (bool * Term.term) list -> xml
7.7 - val modspec2xml : int -> Specification.T -> xml
7.8 + val modspec2xml : int -> SpecificationC.T -> xml
7.9 val pattern2xml : int -> Model_Pattern.T -> Term.term list -> string
7.10 val pos'2xml : int -> string * Pos.pos' -> string
7.11 - val pos'calchead2xml : int -> Pos.pos' * Specification.T -> xml
7.12 + val pos'calchead2xml : int -> Pos.pos' * SpecificationC.T -> xml
7.13 val pos_2xml : int -> Pos.pos_ -> string
7.14 val posform2xml : int -> Pos.pos' * Term.term -> xml
7.15 val posformhead2xml : int -> Pos.pos' * Ctree.ptform -> string
7.16 @@ -402,7 +402,7 @@
7.17 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
7.18 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
7.19
7.20 -fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Specification.T) =
7.21 +fun xml_of_modspec ((b, p_, head, gfr, pre, spec): SpecificationC.T) =
7.22 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
7.23 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
7.24 xml_of_model gfr pre,
7.25 @@ -410,7 +410,7 @@
7.26 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
7.27 xml_of_spec spec])
7.28
7.29 -fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): Specification.T)) =
7.30 +fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): SpecificationC.T)) =
7.31 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
7.32 xml_of_pos "POSITION" p,
7.33 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
8.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Mon Nov 02 15:16:07 2020 +0100
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Wed Nov 04 09:59:30 2020 +0100
8.3 @@ -158,7 +158,7 @@
8.4 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
8.5 "@@@@@end@@@@@");
8.6
8.7 -fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : Specification.T) =
8.8 +fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : SpecificationC.T) =
8.9 XML.Elem (("MODIFYCALCHEAD", []), [
8.10 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
8.11 XML.Elem (("STATUS", []), [
9.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Nov 02 15:16:07 2020 +0100
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Nov 04 09:59:30 2020 +0100
9.3 @@ -300,17 +300,17 @@
9.4 fun resetCalcHead cI =
9.5 (let
9.6 val (ptp,_) = get_calc cI
9.7 - val ptp = Specification.reset ptp
9.8 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get ptp)) end)
9.9 + val ptp = SpecificationC.reset ptp
9.10 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
9.11 handle _ => sysERROR2xml cI "error in kernel 10";
9.12
9.13 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
9.14 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
9.15 fun modelProblem cI =
9.16 (let val (ptp, _) = get_calc cI
9.17 - val ptp = Specification.reset ptp
9.18 + val ptp = SpecificationC.reset ptp
9.19 val (_, (_, _, ptp)) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
9.20 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get ptp)) end)
9.21 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
9.22 handle _ => sysERROR2xml cI "error in kernel 11";
9.23
9.24 (* set the UContext determined on a knowledgebrowser to the current calc
10.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Nov 02 15:16:07 2020 +0100
10.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Nov 04 09:59:30 2020 +0100
10.3 @@ -14,9 +14,9 @@
10.4 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * Pre_Conds.T
10.5 val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * I_Model.T * Pre_Conds.T
10.6 val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
10.7 - val set_method : Method.id -> Calc.T -> Ctree.ctree * Specification.T
10.8 - val set_problem : Problem.id -> Calc.T -> Ctree.ctree * Specification.T
10.9 - val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Specification.T
10.10 + val set_method : Method.id -> Calc.T -> Ctree.ctree * SpecificationC.T
10.11 + val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T
10.12 + val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
10.13 val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
10.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.15 (*NONE*)
10.16 @@ -52,7 +52,7 @@
10.17 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
10.18 | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered"
10.19 in
10.20 - (pt, (complete, Pos.Met, hdf, mits, pre, spec) : Specification.T)
10.21 + (pt, (complete, Pos.Met, hdf, mits, pre, spec) : SpecificationC.T)
10.22 end
10.23
10.24 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
10.25 @@ -69,7 +69,7 @@
10.26 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
10.27 | Ctree.PrfObj _ => raise ERROR "set_problem: case 2 uncovered"
10.28 in
10.29 - (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Specification.T)
10.30 + (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T)
10.31 end
10.32
10.33 fun set_theory tI ptp =
10.34 @@ -84,7 +84,7 @@
10.35 case Ctree.get_obj I pt p of
10.36 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
10.37 | Ctree.PrfObj _ => raise ERROR "set_theory: case 2 uncovered"
10.38 - in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Specification.T) end;
10.39 + in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T) end;
10.40
10.41 (* does several steps within one calculation as given by "type auto";
10.42 the steps may arbitrarily go into and leave different phases,
10.43 @@ -109,7 +109,7 @@
10.44 else
10.45 if member op = [Pos.Pbl, Pos.Met] p_
10.46 then
10.47 - if not (Specification.is_complete (pt, pos))
10.48 + if not (SpecificationC.is_complete (pt, pos))
10.49 then
10.50 let val ptp = Specify.finish_phase (pt, pos) (*... auto = 2 | 3 *)
10.51 in
11.1 --- a/src/Tools/isac/Specify/cas-command.sml Mon Nov 02 15:16:07 2020 +0100
11.2 +++ b/src/Tools/isac/Specify/cas-command.sml Wed Nov 04 09:59:30 2020 +0100
11.3 @@ -6,7 +6,7 @@
11.4 signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
11.5 sig
11.6 type T = CAS_Def.T
11.7 - val input : term -> (Ctree.ctree * Specification.T) option
11.8 + val input : term -> (Ctree.ctree * SpecificationC.T) option
11.9 val is_from: TermC.as_string -> Formalise.T -> bool
11.10
11.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.12 @@ -83,7 +83,7 @@
11.13 val pt = Ctree.update_pbl pt [] pits
11.14 val pt = Ctree.update_met pt [] mits
11.15 in
11.16 - SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T)
11.17 + SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : SpecificationC.T)
11.18 end
11.19 end
11.20
12.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Nov 02 15:16:07 2020 +0100
12.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Nov 04 09:59:30 2020 +0100
12.3 @@ -15,7 +15,7 @@
12.4 type imodel = iitem list
12.5 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
12.6 val empty: icalhd
12.7 - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
12.8 + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T
12.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.10 (* NONE *)
12.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.12 @@ -235,12 +235,12 @@
12.13 then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
12.14 val (_, pre) = Pre_Conds.check prls where_ pits 0
12.15 in (Ctree.update_pbl pt p pits,
12.16 - (Specification.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
12.17 + (SpecificationC.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)
12.18 end
12.19 else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
12.20 val (_, pre) = Pre_Conds.check prls pre mits 0
12.21 in (Ctree.update_met pt p mits,
12.22 - (Specification.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
12.23 + (SpecificationC.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
12.24 end
12.25 end
12.26 end
13.1 --- a/src/Tools/isac/Specify/specification.sml Mon Nov 02 15:16:07 2020 +0100
13.2 +++ b/src/Tools/isac/Specify/specification.sml Wed Nov 04 09:59:30 2020 +0100
13.3 @@ -74,7 +74,7 @@
13.4 end
13.5
13.6 (**)
13.7 -structure Specification(**): SPECIFICATION(**) =
13.8 +structure SpecificationC(**): SPECIFICATION(**) =
13.9 struct
13.10 (**)
13.11
14.1 --- a/src/Tools/isac/Specify/specify.sml Mon Nov 02 15:16:07 2020 +0100
14.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Nov 04 09:59:30 2020 +0100
14.3 @@ -159,7 +159,7 @@
14.4
14.5 fun by_Add_ m_field ct (pt, pos as (_, p_)) =
14.6 let
14.7 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = Specification.get_data (pt, pos)
14.8 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
14.9 val (i_model, m_patt) =
14.10 if p_ = Pos.Met then
14.11 (met,
15.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Nov 02 15:16:07 2020 +0100
15.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Nov 04 09:59:30 2020 +0100
15.3 @@ -153,7 +153,7 @@
15.4 (*8*) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
15.5 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
15.6 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
15.7 - Specification.is_complete ptp;
15.8 + SpecificationC.is_complete ptp;
15.9 References.are_complete ptp;
15.10
15.11 (*8*) autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*)
16.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Nov 02 15:16:07 2020 +0100
16.2 +++ b/test/Tools/isac/Specify/i-model.sml Wed Nov 04 09:59:30 2020 +0100
16.3 @@ -45,7 +45,7 @@
16.4 Specify.by_Add_ "#Given" ct (pt, p);
16.5 "~~~~~ fun by_Add_ , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
16.6 ("#Given", ct, (pt, p));
16.7 - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
16.8 + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
16.9 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
16.10 val cpI = if pI = Problem.id_empty then pI' else pI
16.11 val cmI = if mI = Method.id_empty then mI' else mI
17.1 --- a/test/Tools/isac/Specify/specify.sml Mon Nov 02 15:16:07 2020 +0100
17.2 +++ b/test/Tools/isac/Specify/specify.sml Wed Nov 04 09:59:30 2020 +0100
17.3 @@ -492,7 +492,7 @@
17.4 val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
17.5 Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
17.6 "~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
17.7 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = Specification.get_data (pt, pos);
17.8 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
17.9 (*if*) p_ = Pos.Met (*then*);
17.10 val (i_model, m_patt) = (met,
17.11 (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
17.12 @@ -775,7 +775,7 @@
17.13
17.14 Specify.by_Add_ "#Given" ct ptp;
17.15 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
17.16 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = Specification.get_data (pt, pos);
17.17 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
17.18 (*if*) p_ = Pos.Met (*then*);
17.19 val (i_model, m_patt) = (met,
17.20 (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)