1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Dec 02 12:32:30 2020 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 07 17:39:21 2020 +0100
1.3 @@ -28,7 +28,7 @@
1.4 Proof.state -> bool * (string * string list)
1.5 end;
1.6
1.7 -structure Sledgehammer : SLEDGEHAMMER =
1.8 +structure Sledgehammer(**) : SLEDGEHAMMER(**) =
1.9 struct
1.10
1.11 open ATP_Util
1.12 @@ -246,12 +246,16 @@
1.13 0 => (error "No subgoal!"; (false, (noneN, [])))
1.14 | n =>
1.15 let
1.16 + val _ = @{print} {a = "//--- run_sledgehammer"}
1.17 val _ = Proof.assert_backward state
1.18 val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
1.19
1.20 val found_proof =
1.21 if mode = Normal then
1.22 - let val proof_found = Synchronized.var "proof_found" false in
1.23 + let val proof_found = Synchronized.var "proof_found" false
1.24 + (*val _ = @{print} {a = "### run_sledgehammer", proof_found = proof_found};
1.25 + proof_found is set herewith ^^^^^^^^^^^^^^^^^^^^^^*)
1.26 + in
1.27 fn () =>
1.28 if Synchronized.change_result proof_found (rpair true) then ()
1.29 else (writeln_result |> the_default writeln) "Proof found..."
1.30 @@ -298,6 +302,7 @@
1.31
1.32 fun launch_provers () =
1.33 let
1.34 + val _ = @{print} {z = "### run_sledgehammer > launch_provers"};
1.35 val factss = get_factss provers
1.36 val problem =
1.37 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
1.38 @@ -321,6 +326,8 @@
1.39 handle Timeout.TIMEOUT _ =>
1.40 (print "Sledgehammer ran out of time"; (unknownN, []))
1.41 end
1.42 - |> `(fn (outcome_code, _) => outcome_code = someN))
1.43 + |> `(fn (outcome_code, _) =>
1.44 + (@{print} {z = "\\--- run_sledgehammer", outcome_code = outcome_code};
1.45 + outcome_code = someN)))
1.46
1.47 end;
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Dec 02 12:32:30 2020 +0100
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Dec 07 17:39:21 2020 +0100
2.3 @@ -12,7 +12,7 @@
2.4 val default_params : theory -> (string * string) list -> params
2.5 end;
2.6
2.7 -structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =
2.8 +structure Sledgehammer_Commands(**) : SLEDGEHAMMER_COMMANDS(**) =
2.9 struct
2.10
2.11 open ATP_Util
2.12 @@ -301,6 +301,7 @@
2.13 even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice
2.14 but to insert it into the state as an additional hypothesis.
2.15 *)
2.16 + val _ = @{print} {a = "//--- hammer_away"}
2.17 val {facts = chained0, ...} = Proof.goal state0
2.18 val (inserts, keep_chained) =
2.19 if null chained0 orelse #only fact_override then
2.20 @@ -319,7 +320,9 @@
2.21 val override_params = override_params |> map (normalize_raw_param ctxt)
2.22 in
2.23 if subcommand = runN then
2.24 - let val i = the_default 1 opt_i in
2.25 + let val i = the_default 1 opt_i
2.26 + val _ = @{print} {a = "### hammer_away subcommand = \"run\""}
2.27 + in
2.28 ignore (run_sledgehammer
2.29 (get_params Normal thy override_params) Normal writeln_result i fact_override state)
2.30 end
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Wed Dec 02 12:32:30 2020 +0100
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Dec 07 17:39:21 2020 +0100
3.3 @@ -176,6 +176,7 @@
3.4 | get_time _ = NONE
3.5
3.6 val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
3.7 + val _ = @{print} {a = "### preplay_isar_step, step = step"} (*not yet reached*)
3.8 in
3.9 par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths
3.10 |> sort (play_outcome_ord o apply2 snd)
4.1 --- a/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Wed Dec 02 12:32:30 2020 +0100
4.2 +++ b/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Mon Dec 07 17:39:21 2020 +0100
4.3 @@ -9,5 +9,10 @@
4.4 imports Calculation
4.5 begin
4.6
4.7 +ML \<open>
4.8 +\<close> ML \<open>
4.9 +\<close> ML \<open>
4.10 +\<close>
4.11 +
4.12 end
4.13
5.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Dec 02 12:32:30 2020 +0100
5.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Dec 07 17:39:21 2020 +0100
5.3 @@ -2,13 +2,13 @@
5.4 Author: Walther Neuper, JKU Linz
5.5 (c) due to copyright terms
5.6
5.7 -Outer syntax for Isabelle/Isac. Compare src/Pure/Pure.thy
5.8 +Outer syntax for Isabelle/Isac's Calculation.
5.9 *)
5.10
5.11 theory Calculation
5.12 imports
5.13 "~~/src/Tools/isac/MathEngine/MathEngine"
5.14 - "HOL-SPARK.SPARK" (* for parsing Example files *)
5.15 +(**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)
5.16 keywords
5.17 "Example" :: thy_load ("str") and (* "spark_vc" :: thy_goal *)
5.18 "Problem" and (* root-problem + recursively in Solution *)
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Dec 02 12:32:30 2020 +0100
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Dec 07 17:39:21 2020 +0100
6.3 @@ -115,7 +115,7 @@
6.4 where
6.5 "maximum_value f_ix m_m r_s v_v itv_v e_rr =
6.6 (let e_e = (hd o (filterVar m_m)) r_s;
6.7 - t_t = if 1 < LENGTH r_s
6.8 + t_t = if 1 < Length r_s
6.9 then SubProblem (''DiffApp'', [''make'', ''function''],[''no_met''])
6.10 [REAL m_m, REAL v_v, BOOL_LIST r_s]
6.11 else (hd r_s);
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Dec 02 12:32:30 2020 +0100
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Dec 07 17:39:21 2020 +0100
7.3 @@ -423,7 +423,7 @@
7.4 (["2x2", "LINEAR", "system"],
7.5 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
7.6 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
7.7 - ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
7.8 + ("#Where" ,["Length (e_s:: bool list) = 2", "Length v_s = 2"]),
7.9 ("#Find" ,["solution ss'''"])],
7.10 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
7.11 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
7.12 @@ -450,7 +450,7 @@
7.13 (["3x3", "LINEAR", "system"],
7.14 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
7.15 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
7.16 - ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
7.17 + ("#Where" ,["Length (e_s:: bool list) = 3", "Length v_s = 3"]),
7.18 ("#Find" ,["solution ss'''"])],
7.19 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
7.20 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
7.21 @@ -462,7 +462,7 @@
7.22 (["4x4", "LINEAR", "system"],
7.23 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
7.24 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
7.25 - ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
7.26 + ("#Where" ,["Length (e_s:: bool list) = 4", "Length v_s = 4"]),
7.27 ("#Find" ,["solution ss'''"])],
7.28 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
7.29 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
7.30 @@ -486,7 +486,7 @@
7.31 (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
7.32 (["normalise", "4x4", "LINEAR", "system"],
7.33 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
7.34 - (*LENGTH is checked 1 level above*)
7.35 + (*Length is checked 1 level above*)
7.36 ("#Find" ,["solution ss'''"])],
7.37 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
7.38 SOME "solveSystem e_s v_s",
8.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Dec 02 12:32:30 2020 +0100
8.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Dec 07 17:39:21 2020 +0100
8.3 @@ -60,10 +60,10 @@
8.4 xfoldr_Nil: "xfoldr f {|| ||} = id" |
8.5 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
8.6
8.7 -primrec LENGTH :: "'a list => real"
8.8 +primrec Length :: "'a list => real"
8.9 where
8.10 -LENGTH_NIL: "LENGTH [] = 0" |
8.11 -LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
8.12 +LENGTH_NIL: "Length [] = 0" |
8.13 +LENGTH_CONS: "Length (x#xs) = 1 + Length xs"
8.14
8.15 subsection \<open>Functions for 'list'\<close>
8.16
9.1 --- a/test/HOL/Tools/Sledgehammer/Try_Sledgehammer.thy Wed Dec 02 12:32:30 2020 +0100
9.2 +++ b/test/HOL/Tools/Sledgehammer/Try_Sledgehammer.thy Mon Dec 07 17:39:21 2020 +0100
9.3 @@ -15,7 +15,16 @@
9.4 section \<open>Notes during development\<close>
9.5 text \<open>
9.6 Main question at the beginning:
9.7 - how present a structure comprising keywords and terms via PIDE?
9.8 + How present a structure comprising keywords and terms via PIDE?
9.9 +
9.10 + Preliminary conclusion:
9.11 + The above main question could not yet be answered due to the complexity of Isabelle:
9.12 + * typing "sledgehammer" into a theory, e.g. in lemma "inc \<noteq> (\<lambda>y. 0)" below
9.13 + creates an instance of isar_proofs.
9.14 + * this proof is displayed in an <Output> window
9.15 + * clicking the proof transfers to the theory, i.e. below lemma "inc \<noteq> (\<lambda>y. 0)"
9.16 + The latter is what we are interested in, but we cannot find the respective code,
9.17 + which we expect somewhere far off from Outer_Syntax.command..sledgehammer.
9.18 \<close>
9.19 subsection \<open>Documentation and papers\<close>
9.20 text \<open>
9.21 @@ -34,8 +43,6 @@
9.22 Reconstructing veriT Proofs in Isabelle/HOL
9.23 https://arxiv.org/pdf/1908.09480.pdf
9.24 http://fmv.jku.at/fleury/papers/Fleury-thesis.pdf
9.25 -
9.26 -
9.27 \<close>
9.28
9.29 subsection \<open>code\<close>
9.30 @@ -53,7 +60,7 @@
9.31 HOL/Sledgehammer.thy
9.32 keywords "sledgehammer" :: diag and
9.33 \<close>
9.34 -subsubsection \<open>survey earch: "sledgehammer" , search: "isar_proofs"\<close>
9.35 +subsubsection \<open>survey search: "sledgehammer" , search: "isar_proofs"\<close>
9.36 text \<open>
9.37 ALL hits concerning ML only (no calls from thy in proofs):
9.38 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML "isar_proofs" "sledgehammer"
9.39 @@ -67,24 +74,49 @@
9.40 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML "isar_proofs"
9.41 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML "sledgehammer"
9.42 \<close>
9.43 -subsubsection \<open>search: "sledgehammer"\<close>
9.44 +subsubsection \<open>Try to trace code from keywords down to isar_proofs\<close>
9.45 text \<open>
9.46 -
9.47 + HOL/Sledgehammer.thy
9.48 + "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
9.49 + HOL/Tools/Sledgehammer/sledgehammer_commands.ML
9.50 + Outer_Syntax.command
9.51 + val isar_proofs = lookup_option lookup_bool "isar_proofs"
9.52 + in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end
9.53 + val hammer_away: (string * string list) list -> (string -> unit) option -> string ->
9.54 + int option -> fact_override -> Proof.state -> unit
9.55 + ^^^^^^^^^^^
9.56 + .. called by (exclusively)
9.57 + Outer_Syntax.command command_keyword>\<open>sledgehammer\<close>
9.58 + Query_Operation.register {name = sledgehammerN, pri = 0}
9.59 + HOL/Tools/Sledgehammer/sledgehammer.ML
9.60 + val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
9.61 + Proof.state -> bool * (string * string list)
9.62 + ^^^^^^^^^^^
9.63 +
9.64 + HOL/Tools/Sledgehammer/sledgehammer_isar.ML
9.65 + fun isar_proof_text
9.66 + val ///
9.67 + fun proof_text
9.68 + val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
9.69 + int -> one_line_params -> string
9.70 + ^^^^^^^^^^ is called in ..
9.71 + HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
9.72 + fun run_atp ..calls fun proof_text
9.73 + HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
9.74 + fun run_smt_solver ..calls fun proof_text
9.75 +
9.76 + DIFFICULTY: see conclusion below section \<open>Notes during development\<close>
9.77 \<close>
9.78
9.79 -subsubsection \<open>search: "isar_proofs"\<close>
9.80 -text \<open>
9.81 -
9.82 -\<close>
9.83 -
9.84 -section \<open>Tests copied from various locations\<close>
9.85 +section \<open>Search for an appropriate example\<close>
9.86 text \<open>
9.87 Conclusion: from the locations checked the best example is lemma "inc \<noteq> (\<lambda>y. 0)"
9.88 + here at the bottom.
9.89 \<close>
9.90
9.91 subsection \<open>sledgehammer.pdf\<close>
9.92 text \<open>
9.93 - Summary: There are only two examples, where only one is working.
9.94 + Summary: There are only two examples and only one is working.
9.95 And there are no differences between sledgehammer with [isar_proofs] and without.
9.96 \<close>
9.97 subsubsection \<open>WITHOUT <Isar proofs> checked in Sledgehammer panel\<close>
9.98 @@ -150,7 +182,7 @@
9.99
9.100 subsection \<open>HOL/Metis_Examples/Proxies.thy\<close>
9.101 text \<open>
9.102 - Summary: We use sledgehammer [isar_proofs] + <Isar proofs> checked in Sledgehammer panel.
9.103 + We use sledgehammer [isar_proofs] + <Isar proofs> checked in Sledgehammer panel.
9.104 Little knowledge required: session "HOL-Metis_Examples" =
9.105 "HOL-Library" + "HOL-Decision_Procs" + "HOL-Algebra" + "HOL-Cardinals"
9.106 -- and the first "sledgehammer" is on 1st page.
9.107 @@ -176,4 +208,4 @@
9.108 qed
9.109
9.110
9.111 -end
9.112 \ No newline at end of file
9.113 +end
10.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Wed Dec 02 12:32:30 2020 +0100
10.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Mon Dec 07 17:39:21 2020 +0100
10.3 @@ -70,8 +70,9 @@
10.4 else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'")
10.5 ;
10.6 if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
10.7 - ("IsacKnowledge", "Base_Tools") then ()
10.8 -else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
10.9 +(*("IsacKnowledge", "Base_Tools") ...before session Isac builds on SPARK ?!?*)
10.10 + ("IsacScripts", "Prog_Expr")
10.11 +then () else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
10.12
10.13 "----------- fun thy_containing_cal ---------------------";
10.14 "----------- fun thy_containing_cal ---------------------";
11.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Dec 02 12:32:30 2020 +0100
11.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Dec 07 17:39:21 2020 +0100
11.3 @@ -80,7 +80,7 @@
11.4 "----------- problems --------------------------------------------";
11.5 "----------- problems --------------------------------------------";
11.6 "----------- problems --------------------------------------------";
11.7 -val t = str2term "LENGTH [x+y=1,y=2] = 2";
11.8 +val t = str2term "Length [x+y=1,y=2] = 2";
11.9 atomty t;
11.10 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
11.11 [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})),
12.1 --- a/test/Tools/isac/ProgLang/listC.sml Wed Dec 02 12:32:30 2020 +0100
12.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Dec 07 17:39:21 2020 +0100
12.3 @@ -9,7 +9,7 @@
12.4 "-----------------------------------------------------------------------------";
12.5 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
12.6 "--------------------- NTH ---------------------------------------------------";
12.7 -"--------------------- LENGTH ------------------------------------------------";
12.8 +"--------------------- Length ------------------------------------------------";
12.9 "--------------------- tl ----------------------------------------------------";
12.10 "-----------------------------------------------------------------------------";
12.11 "-----------------------------------------------------------------------------";
12.12 @@ -69,32 +69,32 @@
12.13 if UnparseC.term t' = "c" then ()
12.14 else error "NTH 3 [a,b,c,d,e] = c ..changed";
12.15
12.16 -"--------------------- LENGTH ------------------------------------------------";
12.17 -"--------------------- LENGTH ------------------------------------------------";
12.18 -"--------------------- LENGTH ------------------------------------------------";
12.19 +"--------------------- Length ------------------------------------------------";
12.20 +"--------------------- Length ------------------------------------------------";
12.21 +"--------------------- Length ------------------------------------------------";
12.22 val prog_expr = assoc_rls "prog_expr"
12.23
12.24 val thy = @{theory ListC};
12.25 -val t = str2term "LENGTH [1, 1, 1]";
12.26 +val t = str2term "Length [1, 1, 1]";
12.27 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
12.28 -UnparseC.term t = "1 + LENGTH [1, 1]";
12.29 +UnparseC.term t = "1 + Length [1, 1]";
12.30 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
12.31 -UnparseC.term t = "1 + (1 + LENGTH [1])";
12.32 +UnparseC.term t = "1 + (1 + Length [1])";
12.33 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
12.34 -UnparseC.term t = "1 + (1 + (1 + LENGTH []))";
12.35 +UnparseC.term t = "1 + (1 + (1 + Length []))";
12.36 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
12.37 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
12.38 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
12.39 if UnparseC.term t = "1 + (1 + (1 + 0))" then ()
12.40 -else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
12.41 +else error "Length [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
12.42
12.43 -val t = str2term "LENGTH [1, 1, 1]";
12.44 +val t = str2term "Length [1, 1, 1]";
12.45 val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
12.46 if UnparseC.term t = "3" then ()
12.47 -else error "LENGTH [1, 1, 1] = 3 ..prog_expr changed";
12.48 +else error "Length [1, 1, 1] = 3 ..prog_expr changed";
12.49
12.50 -val t = str2term "LENGTH [1, 1, 1]";
12.51 +val t = str2term "Length [1, 1, 1]";
12.52 val t = eval_prog_expr thy prog_expr t;
12.53 case t of Free ("3", _) => ()
12.54 -| _ => error "LENGTH [1, 1, 1] = 3 ..eval_prog_expr changed";
12.55 +| _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";
12.56
13.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Dec 02 12:32:30 2020 +0100
13.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Dec 07 17:39:21 2020 +0100
13.3 @@ -83,6 +83,7 @@
13.4 (**)"~~/test/Pure/Isar/Check_Outer_Syntax"
13.5 (**)"~~/test/Pure/Isar/Test_Parsers"
13.6 (**)"~~/test/Pure/Isar/Test_Parse_Term"
13.7 +(**)"~~/test/HOL/Tools/Sledgehammer/Try_Sledgehammer"
13.8 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
13.9 "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
13.10 "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)