1.1 --- a/README.md Sun May 29 19:05:14 2022 +0200
1.2 +++ b/README.md Tue May 31 09:16:12 2022 +0200
1.3 @@ -52,6 +52,9 @@
1.4
1.5 isabisac/bin/isabelle jedit -l HOL isa/src/Tools/isac/Build_Isac.thy &
1.6 ====isabisac$ ./bin/isabelle jedit -l HOL ../isa/src/Tools/isac/Build_Isac.thy &
1.7 + isabisac$ ./bin/isabelle build -o browser_info -v -c Specify &
1.8 + isabisac$ ./bin/isabelle build -o browser_info -v -c Interpret &
1.9 + isabisac$ ./bin/isabelle build -o browser_info -v -c Isac &
1.10
1.11 * Test:
1.12
2.1 --- a/TODO.md Sun May 29 19:05:14 2022 +0200
2.2 +++ b/TODO.md Tue May 31 09:16:12 2022 +0200
2.3 @@ -66,6 +66,7 @@
2.4 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
2.5 \<close>
2.6
2.7 -* WN: for calculation by use of Makarius' "problem" as boilerplate clarify
2.8 - - reasons to have some parsers local (initially parse_cas, parse_methods, ml in Outer_Syntax.command..problem)
2.9 - -
2.10 +* WN: for calculation by use of Makarius' "problem" as boilerplate clarify:
2.11 + - How inspect Token lists, e.g. from ML_Lex.read OR ML_Lex.read_source ?
2.12 + - Why the ERROR in Demo_Example.thy at: \<open>problem pbl_bieg : "Biegelinien" = ..\<close> ?
2.13 + - TODO: remove test code written in this changeset
3.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Sun May 29 19:05:14 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Tue May 31 09:16:12 2022 +0200
3.3 @@ -1,8 +1,6 @@
3.4 (* Title: BaseDefinitions/rewrite-order.sml
3.5 Author: Walther Neuper
3.6 (c) due to copyright terms
3.7 -
3.8 -TODO: use "Rewrite_Ord" for renaming identifiers.
3.9 *)
3.10 signature REWRITE_ORDER =
3.11 sig
3.12 @@ -13,6 +11,7 @@
3.13
3.14 type rew_ord = Rule_Def.rew_ord
3.15 val e_rew_ordX: rew_ord
3.16 + val to_string: rew_ord -> string
3.17
3.18 type rew_ord' = Rule_Def.rew_ord'
3.19 val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
3.20 @@ -33,6 +32,7 @@
3.21 type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
3.22 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
3.23 val e_rew_ordX = (e_rew_ord', e_rew_ord_)
3.24 +fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
3.25
3.26 type rew_ord' = Rule_Def.rew_ord'
3.27 (* rewrite orders, also stored in 'type met' and type 'and rls'
4.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Sun May 29 19:05:14 2022 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Tue May 31 09:16:12 2022 +0200
4.3 @@ -34,6 +34,7 @@
4.4 locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
4.5 next_rule: rule list list -> term -> rule option, normal_form: term ->
4.6 (term * term list) option}
4.7 + val rule_to_string: program -> string
4.8 end
4.9
4.10 (**)
4.11 @@ -126,5 +127,9 @@
4.12 list, (* meta-conjunction in guarding is or *)
4.13 rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
4.14
4.15 +fun rule_to_string Empty_Prog = "Empty_Prog"
4.16 + | rule_to_string (Prog s) = "Prog " ^ UnparseC.term s
4.17 + | rule_to_string (Rfuns _) = "Rfuns";
4.18 +
4.19 (**)end(**)
4.20
5.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Sun May 29 19:05:14 2022 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Tue May 31 09:16:12 2022 +0200
5.3 @@ -12,13 +12,13 @@
5.4 val id: T -> string
5.5 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
5.6 preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
5.7 + val to_string: T -> string
5.8
5.9 val append_rules: string -> T -> Rule_Def.rule list -> T
5.10 val append_erls_rules: string -> T -> Rule_Def.rule list -> T
5.11 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
5.12 val merge: string -> T -> T -> T
5.13 val get_rules: T -> Rule_Def.rule list
5.14 -(*val rule2rls': Rule.rule -> string*)
5.15 val id_from_rule: Rule.rule -> string
5.16 val contains: Rule.rule -> T -> bool
5.17
5.18 @@ -60,6 +60,18 @@
5.19 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
5.20 calc = calc, rules = rules, scr = scr}
5.21 | rep (Rule_Def.Rrls _) = rep empty
5.22 +fun to_string Rule_Def.Empty = "Rule_Set.Empty"
5.23 + | to_string (Rule_Def.Repeat {id, preconds, rew_ord, erls = _, srls = _, calc = _, errpatts = _, rules, scr}) =
5.24 + "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord
5.25 + ^ ",\n erls = _, srls = _, calc = _, errpatts = _, "
5.26 + ^ ",\n rules = " ^ Rule.s_to_string rules
5.27 + ^ ",\n rules = " ^ Rule_Def.rule_to_string scr ^ "})"
5.28 + | to_string (Rule_Def.Sequence {id, preconds, rew_ord, erls = _, srls = _, calc = _, errpatts = _, rules, scr}) =
5.29 + "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord
5.30 + ^ ",\n erls = _, srls = _, calc = _, errpatts = _, "
5.31 + ^ ",\n rules = " ^ Rule.s_to_string rules
5.32 + ^ ",\n rules = " ^ Rule_Def.rule_to_string scr ^ "})"
5.33 + | to_string (Rule_Def.Rrls _) = "Rule_Def.Rrls _"
5.34
5.35 fun append_rules id Rule_Def.Empty r = (*.. required for append_erls_rules *)
5.36 Rule_Def.Repeat {id = id, preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
6.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Sun May 29 19:05:14 2022 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Tue May 31 09:16:12 2022 +0200
6.3 @@ -16,6 +16,7 @@
6.4 val equal: Rule_Def.rule * Rule_Def.rule -> bool
6.5 val to_string: Rule_Def.rule -> string
6.6 val to_string_short: Rule_Def.rule -> string
6.7 + val s_to_string: rule list -> string
6.8
6.9 val thm: rule -> thm
6.10 val distinct' : rule list -> rule list
6.11 @@ -66,6 +67,7 @@
6.12 | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
6.13 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
6.14 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
6.15 +fun s_to_string rules = rules |> map to_string_short |> commas |> enclose "[" "]"
6.16
6.17 fun thm_id (Rule_Def.Thm (id, _)) = id
6.18 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
7.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Sun May 29 19:05:14 2022 +0200
7.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Tue May 31 09:16:12 2022 +0200
7.3 @@ -34,11 +34,29 @@
7.4 fun merge _ = NONE;
7.5 );
7.6
7.7 -val set_data = Data.put o SOME;
7.8 -val the_data = the o Data.get;
7.9 +val set_data = (writeln "=== set_data"; Data.put o SOME);
7.10 +val the_data = (writeln "=== the_data"; the o Data.get);
7.11
7.12 \<close> ML \<open>
7.13 \<close> ML \<open>
7.14 +set_data: Rule_Def.rule_set -> theory -> theory
7.15 +\<close> ML \<open>
7.16 +fun set_data rls thy =
7.17 + ((case rls of
7.18 + Rule_Def.Empty => writeln "=== Rule_Def.Empty"
7.19 + | Rule_Def.Repeat _ => writeln "=== Rule_Def.Repeat _"
7.20 + | Rule_Def.Sequence _ => writeln "=== Rule_Def.RepSequenceeat _"
7.21 + | Rule_Def.Rrls _ => writeln "=== Rule_Def.Rrls _"
7.22 + );
7.23 + (Data.put o SOME) rls thy)
7.24 +\<close> ML \<open>
7.25 +the_data: theory -> Rule_Def.rule_set
7.26 +\<close> ML \<open>
7.27 +(*+*)fun the_data thy =
7.28 + case Data.get thy of
7.29 + SOME rls => (writeln ("=== the_data thy \<Rightarrow> " ^ Rule_Set.to_string rls); rls)
7.30 + | NONE => raise ERROR "=== the_data thy \<Rightarrow> NONE"
7.31 +\<close> ML \<open>
7.32 \<close> ML \<open>
7.33
7.34 \<close> ML \<open>
7.35 @@ -62,12 +80,50 @@
7.36 (Problem.ml "Theory.setup (Problem.set_data ("
7.37 @ ML_Lex.read_source source @ Problem.ml "))")
7.38 |> Context.theory_map;
7.39 +val _ = writeln "=== Outer_Syntax.command 4"
7.40 val input = the_data (set_data thy);
7.41 +val _ = writeln "=== Outer_Syntax.command 5"
7.42 val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs);
7.43 - in KEStore_Elems.add_pbts [arg] thy end)))
7.44 -
7.45 + in KEStore_Elems.add_pbts [arg] thy end
7.46 + )
7.47 + )
7.48 + )
7.49 in end;
7.50 \<close> ML \<open>
7.51 +ML_Context.expression:
7.52 + Position.T -> ML_Lex.token Antiquote.antiquote list -> Context.generic
7.53 + -> Context.generic
7.54 +\<close> ML \<open>
7.55 +Problem.ml "Theory.setup (Problem.set_data (" (* =
7.56 + [Text (Token (({}, {}), (Long_Ident, "Theory.setup"))),
7.57 + Text (Token (({}, {}), (Space, " "))),
7.58 + Text (Token (({}, {}), (Keyword, "("))),
7.59 + Text (Token (({}, {}), (Long_Ident, "Problem.set_data"))),
7.60 + Text (Token (({}, {}), (Space, " "))),
7.61 + Text (Token (({}, {}), (Keyword, "("))),
7.62 + Text (Token (({}, {}), (Space, " ")))]:
7.63 + ML_Lex.token Antiquote.antiquote list*)
7.64 +\<close> text \<open>
7.65 +@
7.66 +ML_Lex.read_source source:
7.67 + ML_Lex.token Antiquote.antiquote list
7.68 +@
7.69 +\<close> ML \<open>
7.70 +Problem.ml "))" (* =
7.71 + [Text (Token (({}, {}), (Keyword, ")"))),
7.72 + Text (Token (({}, {}), (Keyword, ")"))),
7.73 + Text (Token (({}, {}), (Space, " ")))]:
7.74 + ML_Lex.token Antiquote.antiquote list*)
7.75 +\<close> ML \<open>
7.76 +Context.theory_map: (Context.generic -> Context.generic) -> theory -> theory
7.77 +\<close> ML \<open>
7.78 +\<close> ML \<open>
7.79 +\<close> ML \<open>
7.80 +\<close> ML \<open>
7.81 +\<close> ML \<open>
7.82 +\<close> ML \<open>
7.83 +\<close> ML \<open>
7.84 +\<close> ML \<open>
7.85 \<close> ML \<open>
7.86 \<close> ML \<open>
7.87 \<close>
8.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun May 29 19:05:14 2022 +0200
8.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy Tue May 31 09:16:12 2022 +0200
8.3 @@ -82,8 +82,8 @@
8.4 * Although the application below with \<open>problem\<close> works?
8.5 * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!?
8.6 HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ?
8.7 - *)
8.8 -Example pbl_bieg : "Biegelinien" =
8.9 +Example problem*)
8.10 +problem pbl_bieg : "Biegelinien" =
8.11 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
8.12 Method: "IntegrierenUndKonstanteBestimmen2"
8.13 Given: "Traegerlaenge l_l" "Streckenlast q_q"
8.14 @@ -91,7 +91,36 @@
8.15 Find: "Biegelinie b_b"
8.16 Relate: "Randbedingungen r_b"
8.17
8.18 -ML \<open>
8.19 +text \<open> (*Output from: Example pbl_bieg : "Biegelinien" = .. *)
8.20 +=== Outer_Syntax.command 4
8.21 +=== the_data thy \<Rightarrow> NONE
8.22 +
8.23 + (*Output from: problem pbl_bieg : "Biegelinien" = .. *)
8.24 +--- Outer_Syntax.command 4
8.25 +--- the_data thy \<Rightarrow> (Rule_Def.Repeat {id = empty, preconds = [], rew_ord = (dummy_ord, _: fn),
8.26 + erls = _, srls = _, calc = _, errpatts = _, ,
8.27 + rules = [],
8.28 + rules = Empty_Prog})
8.29 +--- Outer_Syntax.command 5
8.30 +\<close> ML \<open>
8.31 +Rule_Set.append_rules "empty" Rule_Set.empty []
8.32 +\<close>
8.33 +text \<open> (*Output from: Example pbl_bieg : "Biegelinien" = .. HERE*)
8.34 +val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [],
8.35 + rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set
8.36 +
8.37 + (*Output from: problem pbl_bieg : "Biegelinien" = .. HERE*)
8.38 +val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [],
8.39 + rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set
8.40 +
8.41 + (*Output from: problem pbl_bieg : "Biegelinien" = .. IN Biegelinie.thy*)
8.42 +val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [],
8.43 + rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set
8.44 +
8.45 + (*^^^ all the same*)
8.46 +\<close> ML \<open>
8.47 +\<close> ML \<open>
8.48 +\<close> ML \<open>
8.49 \<close> ML \<open>
8.50 \<close> ML \<open>
8.51 \<close>
9.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun May 29 19:05:14 2022 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue May 31 09:16:12 2022 +0200
9.3 @@ -109,6 +109,9 @@
9.4 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
9.5 Find: "Biegelinie b_b"
9.6 Relate: "Randbedingungen r_b"
9.7 +ML \<open>
9.8 +Rule_Set.append_rules "empty" Rule_Set.empty []
9.9 +\<close>
9.10
9.11 problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =
9.12 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
10.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Sun May 29 19:05:14 2022 +0200
10.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Tue May 31 09:16:12 2022 +0200
10.3 @@ -139,6 +139,10 @@
10.4 val set_data = Data.put o SOME;
10.5 val the_data = the o Data.get;
10.6
10.7 +(*+*)fun the_data thy =
10.8 + case Data.get thy of
10.9 + SOME rls => (writeln ("--- the_data thy \<Rightarrow> " ^ Rule_Set.to_string rls); rls)
10.10 + | NONE => raise ERROR "--- the_data thy \<Rightarrow> NONE"
10.11
10.12 (* auxiliary parsers *)
10.13
10.14 @@ -185,7 +189,9 @@
10.15 ML_Context.expression (Input.pos_of source)
10.16 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
10.17 |> Context.theory_map;
10.18 +val _ = writeln "--- Outer_Syntax.command 4"
10.19 val input = the_data (set_data thy);
10.20 +val _ = writeln "--- Outer_Syntax.command 5"
10.21 val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
10.22 in KEStore_Elems.add_pbts [arg] thy end)))
10.23
11.1 --- a/src/Tools/isac/ProgLang/Program.thy Sun May 29 19:05:14 2022 +0200
11.2 +++ b/src/Tools/isac/ProgLang/Program.thy Tue May 31 09:16:12 2022 +0200
11.3 @@ -89,9 +89,7 @@
11.4 |> snd)
11.5 handle TERM _ => raise TERM ("body_of", [tm])
11.6
11.7 -fun to_string Rule_Def.Empty_Prog = "Empty_Prog"
11.8 - | to_string (Rule_Def.Prog s) = "Prog " ^ UnparseC.term s
11.9 - | to_string (Rule_Def.Rfuns _) = "Rfuns";
11.10 +val to_string = Rule_Def.rule_to_string;
11.11
11.12
11.13 (**)end(**)
11.14 @@ -99,4 +97,4 @@
11.15 \<close> ML \<open>
11.16 \<close>
11.17
11.18 -end
11.19 \ No newline at end of file
11.20 +end