1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 09 17:16:48 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 09 18:21:09 2020 +0200
1.3 @@ -44,7 +44,7 @@
1.4 val spec2xml : int -> Celem.spec -> Celem.xml
1.5 val sub2xml : int -> Term.term * Term.term -> Celem.xml
1.6 val subs2xml : int -> Selem.subs -> Celem.xml
1.7 - val subst2xml : int -> Rule.subst -> Celem.xml
1.8 + val subst2xml : int -> UnparseC.subst -> Celem.xml
1.9 val tac2xml : int -> Tactic.input -> Celem.xml
1.10 val tacs2xml : int -> Tactic.input list -> Celem.xml
1.11 val theref2xml : int -> ThyC.thyID -> string -> xstring -> string
1.12 @@ -244,15 +244,15 @@
1.13 indt (j+i) ^"</ORDER>\n" ^
1.14 indt (j+i) ^"<ERLS>\n" ^
1.15 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.16 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id_rls erls ^ " </STRING>\n" ^
1.17 + indt (j+2*i) ^ "<STRING> " ^ Rule_Set.rls2str erls ^ " </STRING>\n" ^
1.18 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
1.19 - (Rule_Set.id_rls erls) ^ " </GUH>\n" ^
1.20 + (Rule_Set.rls2str erls) ^ " </GUH>\n" ^
1.21 indt (j+i) ^"</ERLS>\n" ^
1.22 indt (j+i) ^"<SRLS>\n" ^
1.23 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.24 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id_rls erls ^ " </STRING>\n" ^
1.25 + indt (j+2*i) ^ "<STRING> " ^ Rule_Set.rls2str erls ^ " </STRING>\n" ^
1.26 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
1.27 - (Rule_Set.id_rls srls) ^ " </GUH>\n" ^
1.28 + (Rule_Set.rls2str srls) ^ " </GUH>\n" ^
1.29 indt (j+i) ^"</SRLS>\n" ^
1.30 calcrefs2xml (j+i) (thyID, calc) ^
1.31 scr2xml (j+i) scr ^
1.32 @@ -275,8 +275,8 @@
1.33 indt (j+i) ^"</ORDER>\n" ^
1.34 indt (j+i) ^"<ERLS> " ^
1.35 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.36 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id_rls erls ^ " </STRING>\n" ^
1.37 - indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id_rls erls) ^ " </GUH>\n" ^
1.38 + indt (j+2*i) ^ "<STRING> " ^ Rule_Set.rls2str erls ^ " </STRING>\n" ^
1.39 + indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID) (Rule_Set.rls2str erls) ^ " </GUH>\n" ^
1.40 indt (j+i) ^"</ERLS>\n" ^
1.41 calcrefs2xml (j+i) (thyID, calc) ^
1.42 indt (j+i) ^"<SCRIPT>\n"^
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 09 17:16:48 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 09 18:21:09 2020 +0200
2.3 @@ -11,7 +11,7 @@
2.4
2.5 signature KERNEL =
2.6 sig
2.7 - val appendFormula : Celem.calcID -> Rule.cterm' -> XML.tree (*unit future*)
2.8 + val appendFormula : Celem.calcID -> UnparseC.cterm' -> XML.tree (*unit future*)
2.9 val autoCalculate : Celem.calcID -> Solve.auto -> XML.tree (*unit future*)
2.10 val applyTactic : Celem.calcID -> Pos.pos' -> Tactic.input -> XML.tree
2.11 val CalcTree : Selem.fmz list -> XML.tree
2.12 @@ -48,7 +48,7 @@
2.13 val moveUp : Celem.calcID -> Pos.pos' -> XML.tree
2.14 val refFormula : Celem.calcID -> Pos.pos' -> XML.tree
2.15 val refineProblem : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
2.16 - val replaceFormula : Celem.calcID -> Rule.cterm' -> XML.tree
2.17 + val replaceFormula : Celem.calcID -> UnparseC.cterm' -> XML.tree
2.18 val requestFillformula : Celem.calcID -> Error_Fill_Def.errpatID * Error_Fill_Def.fillpatID -> XML.tree
2.19 val resetCalcHead : Celem.calcID -> XML.tree
2.20 val setContext : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
2.21 @@ -439,7 +439,7 @@
2.22 handle _ => sysERROR2xml cI "error in kernel 16";
2.23
2.24 (* append a formula to the calculation *)
2.25 -fun appendFormula' cI (ifo: Rule.cterm') =
2.26 +fun appendFormula' cI (ifo: UnparseC.cterm') =
2.27 (let
2.28 val cs = get_calc cI
2.29 val pos = get_pos cI 1
3.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 09 17:16:48 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 09 18:21:09 2020 +0200
3.3 @@ -14,14 +14,14 @@
3.4 ad(2) decode "<" ---> "<", decode ">" ---> ">"
3.5 decode "&" ---> "&"
3.6 called for term2xml; + see "fun encode" below*)
3.7 -fun decode (str: Rule.cterm') =
3.8 +fun decode (str: UnparseC.cterm') =
3.9 let fun dec [] = []
3.10 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
3.11 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
3.12 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
3.13 | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
3.14 | dec (c::cs) = c::(dec cs)
3.15 - in (implode o dec o Symbol.explode) str: Rule.cterm' end;
3.16 + in (implode o dec o Symbol.explode) str: UnparseC.cterm' end;
3.17
3.18 fun dop_leading _ [] = []
3.19 | dop_leading c (c' :: cs) =
3.20 @@ -33,7 +33,7 @@
3.21 let val cs' = dop_leading "^" cs
3.22 in rm_doublets c (singled @ [c']) cs' end
3.23 else rm_doublets c (singled @ [c']) cs
3.24 -fun encode (str : Rule.cterm') =
3.25 +fun encode (str : UnparseC.cterm') =
3.26 let fun enc [] = []
3.27 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
3.28 | enc (c :: cs) = c :: (enc cs)
4.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Thu Apr 09 17:16:48 2020 +0200
4.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Thu Apr 09 18:21:09 2020 +0200
4.3 @@ -216,7 +216,7 @@
4.4 | Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.thyID * Rule_Set.T)}
4.5 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
4.6 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
4.7 - ord: (Rule.subst -> (term * term) -> bool)};
4.8 + ord: (UnparseC.subst -> (term * term) -> bool)};
4.9 fun the2str (Html {guh, ...}) = guh
4.10 | the2str (Hthm {guh, ...}) = guh
4.11 | the2str (Hrls {guh, ...}) = guh
5.1 --- a/src/Tools/isac/CalcElements/environment.sml Thu Apr 09 17:16:48 2020 +0200
5.2 +++ b/src/Tools/isac/CalcElements/environment.sml Thu Apr 09 18:21:09 2020 +0200
5.3 @@ -6,10 +6,10 @@
5.4 sig
5.5 (*Celem*)
5.6 type T
5.7 - val env2str: Rule.subst -> string
5.8 - val env2str': Rule.subst -> string
5.9 - val subst2str: Rule.subst -> string
5.10 - val subst2str': Rule.subst -> string
5.11 + val env2str: UnparseC.subst -> string
5.12 + val env2str': UnparseC.subst -> string
5.13 + val subst2str: UnparseC.subst -> string
5.14 + val subst2str': UnparseC.subst -> string
5.15 val update: T -> term * term -> T
5.16 val update': term -> term * T -> T
5.17 val update_opt: T -> term option * term -> T
6.1 --- a/src/Tools/isac/CalcElements/rule-set.sml Thu Apr 09 17:16:48 2020 +0200
6.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml Thu Apr 09 18:21:09 2020 +0200
6.3 @@ -9,6 +9,7 @@
6.4 datatype T = datatype Rule_Def.rule_set
6.5 eqtype identifier
6.6
6.7 + val rls2str: T -> string
6.8 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
6.9 preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
6.10
6.11 @@ -23,21 +24,13 @@
6.12
6.13 (*/------- this will disappear eventually -----------\*)
6.14 val empty: T
6.15 -
6.16 type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
6.17 val e_rrlsstate: rrlsstate
6.18 val e_rrls: T
6.19 (*\------- this will disappear eventually -----------/*)
6.20
6.21 -(*val id_rls: T -> string*)
6.22 -(*/------- back to rule.sml -----------------------\*)
6.23 - val rls2str: T(*Rule_Def.rule_set*) -> string
6.24 - val id_rls: T(*Rule_Def.rule_set*) -> string
6.25 - val id_rule: Rule_Def.rule -> string
6.26 - val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
6.27 val rule2str: Rule_Def.rule -> string
6.28 val rule2str': Rule_Def.rule -> string
6.29 -(*\------- back to rule.sml -----------------------/*)
6.30
6.31 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.32 (*NONE*)
6.33 @@ -60,6 +53,7 @@
6.34 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
6.35 (*\------- this will disappear eventually ----------------------------------------------------/*)
6.36
6.37 +fun rls2str xxx = Rule.id_rls xxx;
6.38 fun rep Rule_Def.Empty = rep empty
6.39 | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
6.40 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
6.41 @@ -88,24 +82,6 @@
6.42 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
6.43 end
6.44
6.45 -(*/------- back to rule.sml -----------------------\*)
6.46 -fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
6.47 - | id_rls (Rule_Def.Repeat {id, ...}) = id
6.48 - | id_rls (Rule_Def.Seqence {id, ...}) = id
6.49 - | id_rls (Rule_Def.Rrls {id, ...}) = id;
6.50 -val rls2str = id_rls; (*drop*)
6.51 -
6.52 -fun id_rule (Rule_Def.Thm (id, _)) = id
6.53 - | id_rule (Rule_Def.Num_Calc (id, _)) = id
6.54 - | id_rule (Rule_Def.Cal1 (id, _)) = id
6.55 - | id_rule (Rule_Def.Rls_ rls) = id_rls rls
6.56 - | id_rule Rule_Def.Erule = "Erule";
6.57 -fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
6.58 - | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
6.59 - | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
6.60 - | eq_rule _ = false;
6.61 -(*\------- back to rule.sml -----------------------/*)
6.62 -
6.63 fun merge _ Rule_Def.Empty rls = rls
6.64 | merge _ rls Rule_Def.Empty = rls
6.65 | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
6.66 @@ -121,7 +97,7 @@
6.67 erls = merge (merge_ids er1 er2) er1 er2,
6.68 srls = merge (merge_ids sr1 sr2) sr1 sr2,
6.69 calc = union Exec_Def.calc_eq ca1 ca2,
6.70 - rules = union eq_rule rs1 rs2,
6.71 + rules = union Rule.eq_rule rs1 rs2,
6.72 errpatts = union (op =) eps1 eps2}
6.73 | merge id
6.74 (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
6.75 @@ -134,48 +110,21 @@
6.76 erls = merge (merge_ids er1 er2) er1 er2,
6.77 srls = merge (merge_ids sr1 sr2) sr1 sr2,
6.78 calc = union Exec_Def.calc_eq ca1 ca2,
6.79 - rules = union eq_rule rs1 rs2,
6.80 + rules = union Rule.eq_rule rs1 rs2,
6.81 errpatts = union (op =) eps1 eps2}
6.82 | merge id _ _ = error ("merge: \"" ^ id ^
6.83 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
6.84
6.85 -(*/------- this will disappear eventually -----------\*)
6.86 -type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
6.87 - (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
6.88 -val e_rrlsstate = (UnparseC.e_term, UnparseC.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.e_term, []))]) : rrlsstate;
6.89 -local
6.90 - fun ii (_: term) = e_rrlsstate;
6.91 - fun no (_: term) = SOME (UnparseC.e_term, [UnparseC.e_term]);
6.92 - fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
6.93 - fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
6.94 - fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
6.95 -in
6.96 -val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
6.97 - next_rule = ne, attach_form = fo};
6.98 -end;
6.99 -val e_rrls =
6.100 - Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
6.101 - calc = [], errpatts = [], scr = e_rfuns}
6.102 -(*\------- this will disappear eventually -----------/*)
6.103 -
6.104 -(*/------- back to rule.sml -----------------------\*)
6.105 -fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
6.106 - | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
6.107 - | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
6.108 - | eq_rule _ = false;
6.109 -
6.110 fun rule2str Rule_Def.Erule = "Erule"
6.111 | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
6.112 | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
6.113 | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
6.114 - | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
6.115 + | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ rls2str rls ^ "\")";
6.116 fun rule2str' Rule_Def.Erule = "Erule"
6.117 | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
6.118 | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
6.119 | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
6.120 - | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
6.121 -(*\------- back to rule.sml -----------------------/*)
6.122 -
6.123 + | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ rls2str rls ^ "\")";
6.124
6.125 (* datastructure for KEStore_Elems, intermediate for thehier *)
6.126 type for_kestore =
6.127 @@ -198,14 +147,14 @@
6.128 (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.129 rules = rs, errpatts = eps, scr = sc}) r =
6.130 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.131 - rules = gen_rems eq_rule (rs, r),
6.132 + rules = gen_rems Rule.eq_rule (rs, r),
6.133 errpatts = eps,
6.134 scr = sc}
6.135 | keep_unique_rules id
6.136 (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.137 rules = rs, errpatts = eps, scr = sc}) r =
6.138 Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.139 - rules = gen_rems eq_rule (rs, r),
6.140 + rules = gen_rems Rule.eq_rule (rs, r),
6.141 errpatts = eps,
6.142 scr = sc}
6.143 | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
6.144 @@ -216,5 +165,24 @@
6.145 | get_rules (Rule_Def.Seqence {rules, ...}) = rules
6.146 | get_rules (Rule_Def.Rrls _) = [];
6.147
6.148 +(*/------- this will disappear eventually -----------\*)
6.149 +type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
6.150 + (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
6.151 +val e_rrlsstate = (UnparseC.e_term, UnparseC.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.e_term, []))]) : rrlsstate;
6.152 +local
6.153 + fun ii (_: term) = e_rrlsstate;
6.154 + fun no (_: term) = SOME (UnparseC.e_term, [UnparseC.e_term]);
6.155 + fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
6.156 + fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
6.157 + fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
6.158 +in
6.159 +val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
6.160 + next_rule = ne, attach_form = fo};
6.161 +end;
6.162 +val e_rrls =
6.163 + Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
6.164 + calc = [], errpatts = [], scr = e_rfuns}
6.165 +(*\------- this will disappear eventually -----------/*)
6.166 +
6.167
6.168 (**)end(**)
7.1 --- a/src/Tools/isac/CalcElements/rule.sml Thu Apr 09 17:16:48 2020 +0200
7.2 +++ b/src/Tools/isac/CalcElements/rule.sml Thu Apr 09 18:21:09 2020 +0200
7.3 @@ -11,11 +11,9 @@
7.4 datatype rule = datatype Rule_Def.rule
7.5 datatype program = datatype Rule_Def.program
7.6
7.7 -(*/------- to unparse.sml-------\*)
7.8 - eqtype cterm'
7.9 - type subst = (term * term) list
7.10 -(*\------- to unparse.sml-------/*)
7.11 -
7.12 + val id_rls: Rule_Def.rule_set -> string
7.13 + val id_rule: Rule_Def.rule -> string
7.14 + val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
7.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.16 (*NONE*)
7.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.18 @@ -41,43 +39,19 @@
7.19 Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)
7.20 type eval_fn = Rule_Def.eval_fn (*..from Rule_Def*)
7.21
7.22 -(*/------- to unparse.sml-------\*)
7.23 -type cterm' = string;
7.24 -type subst = (term * term) list;
7.25 +fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
7.26 + | id_rls (Rule_Def.Repeat {id, ...}) = id
7.27 + | id_rls (Rule_Def.Seqence {id, ...}) = id
7.28 + | id_rls (Rule_Def.Rrls {id, ...}) = id;
7.29
7.30 -fun term_to_string' ctxt t =
7.31 - let
7.32 - val ctxt' = Config.put show_markup false ctxt
7.33 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
7.34 -fun term_to_string'' thyID t =
7.35 - let
7.36 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
7.37 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
7.38 -fun term_to_string''' thy t =
7.39 - let
7.40 - val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
7.41 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
7.42 -
7.43 -fun term2str t = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") t;
7.44 -fun t2str thy t = term_to_string' (ThyC.thy2ctxt thy) t;
7.45 -fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
7.46 -fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
7.47 -val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
7.48 -val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *)
7.49 -fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
7.50 - | termopt2str NONE = "NONE";
7.51 -
7.52 -fun type_to_string'' (thyID : ThyC.thyID) t =
7.53 - let
7.54 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
7.55 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
7.56 -fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
7.57 -val string_of_typ = type2str; (*legacy*)
7.58 -fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
7.59 -
7.60 -val e_type = Type ("empty",[]);
7.61 -val e_term = Const ("empty", Type("'a", []));
7.62 -(*\------- to unparse.sml-------/*)
7.63 -
7.64 +fun id_rule (Rule_Def.Thm (id, _)) = id
7.65 + | id_rule (Rule_Def.Num_Calc (id, _)) = id
7.66 + | id_rule (Rule_Def.Cal1 (id, _)) = id
7.67 + | id_rule (Rule_Def.Rls_ rls) = id_rls rls
7.68 + | id_rule Rule_Def.Erule = "Erule";
7.69 +fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
7.70 + | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
7.71 + | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
7.72 + | eq_rule _ = false;
7.73
7.74 (**)end(**)
8.1 --- a/src/Tools/isac/CalcElements/thmC.sml Thu Apr 09 17:16:48 2020 +0200
8.2 +++ b/src/Tools/isac/CalcElements/thmC.sml Thu Apr 09 18:21:09 2020 +0200
8.3 @@ -49,7 +49,7 @@
8.4 activate : thmID_of_derivation_name'
8.5 *)
8.6 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
8.7 -type thm' = thmID * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
8.8 +type thm' = thmID * UnparseC.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
8.9 val thm'2xml : int -> ThmC.thm' -> Celem.xml
8.10 val assoc_thm': theory -> ThmC.thm' -> thm
8.11 | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
9.1 --- a/src/Tools/isac/CalcElements/unparseC.sml Thu Apr 09 17:16:48 2020 +0200
9.2 +++ b/src/Tools/isac/CalcElements/unparseC.sml Thu Apr 09 18:21:09 2020 +0200
9.3 @@ -8,6 +8,8 @@
9.4
9.5 signature UNPARSE_ISAC =
9.6 sig
9.7 + eqtype cterm'
9.8 + type subst = (term * term) list
9.9 val e_term: term
9.10 (**)
9.11 val e_type: typ
10.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 09 17:16:48 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 09 18:21:09 2020 +0200
10.3 @@ -28,7 +28,7 @@
10.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.5 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
10.6 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
10.7 - val check_err_patt : term * term -> Rule.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
10.8 + val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
10.9 val get_fillform :
10.10 'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
10.11 val get_fillpats :
10.12 @@ -45,7 +45,7 @@
10.13
10.14 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
10.15 | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule_Set.rule2str r);
10.16 -fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id_rls rls
10.17 +fun rule2rls' (Rule.Rls_ rls) = Rule_Set.rls2str rls
10.18 | rule2rls' r = error ("rule2rls': not defined for " ^ Rule_Set.rule2str r);
10.19
10.20 (*the lists contain eq-al elem-pairs at the beginning;
11.1 --- a/src/Tools/isac/Interpret/li-tool.sml Thu Apr 09 17:16:48 2020 +0200
11.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Thu Apr 09 18:21:09 2020 +0200
11.3 @@ -144,28 +144,28 @@
11.4 | _ => Not_Associated)
11.5 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
11.6 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
11.7 - if Rule_Set.id_rls rls = HOLogic.dest_string rls_ then
11.8 + if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
11.9 if f = f_ then
11.10 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
11.11 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
11.12 else Not_Associated
11.13 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
11.14 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
11.15 - if Rule_Set.id_rls rls = HOLogic.dest_string rls_ then
11.16 + if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
11.17 if f = f_ then
11.18 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
11.19 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
11.20 else Not_Associated
11.21 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
11.22 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
11.23 - if Rule_Set.id_rls rls = HOLogic.dest_string rls_ then
11.24 + if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
11.25 if f = f_ then
11.26 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
11.27 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
11.28 else Not_Associated
11.29 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
11.30 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
11.31 - if Rule_Set.id_rls rls = HOLogic.dest_string rls_ then
11.32 + if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
11.33 if f = f_ then
11.34 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
11.35 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
12.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Apr 09 17:16:48 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Apr 09 18:21:09 2020 +0200
12.3 @@ -14,14 +14,14 @@
12.4 val thy_containing_cal : ThyC.theory' -> Exec_Def.prog_calcID -> string * string
12.5 datatype contthy
12.6 = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: ThyC.thyID}
12.7 - | ContNOrewInst of {applto: term, bdvs: Rule.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.thyID}
12.8 + | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.thyID}
12.9 | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.thyID}
12.10 - | ContRlsInst of {applto: term, asms: term list, bdvs: Rule.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}
12.11 + | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}
12.12 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
12.13 lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
12.14 thm: Celem.guh, thyID: ThyC.thyID}
12.15 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
12.16 - bdvs: Rule.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
12.17 + bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
12.18 rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
12.19 | EContThy
12.20 val guh2filename : Celem.guh -> Celem.filename
12.21 @@ -42,7 +42,7 @@
12.22 term option -> term -> deriv
12.23 val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
12.24 term option -> term -> (Rule.rule * (term * term list)) list
12.25 - val get_bdv_subst : term -> (term * term) list -> Selem.subs option * Rule.subst
12.26 + val get_bdv_subst : term -> (term * term) list -> Selem.subs option * UnparseC.subst
12.27 val thy_containing_thm : string -> string * string
12.28 val guh2theID : Celem.guh -> Celem.theID
12.29 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.30 @@ -231,7 +231,7 @@
12.31
12.32 fun eq_Thm (Rule.Thm (id1, _), Rule.Thm (id2,_)) = id1 = id2
12.33 | eq_Thm (Rule.Thm (_, _), _) = false
12.34 - | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.id_rls r1 = Rule_Set.id_rls r2
12.35 + | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.rls2str r1 = Rule_Set.rls2str r2
12.36 | eq_Thm (Rule.Rls_ _, _) = false
12.37 | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule_Set.rule2str r1 ^ "' '" ^ Rule_Set.rule2str r2 ^ "'")
12.38 fun distinct_Thm r = gen_distinct eq_Thm r
12.39 @@ -290,7 +290,7 @@
12.40 | ContThmInst of (* a theorem with bdvs in contex ============ *)
12.41 {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
12.42 thm : Celem.guh, (*theorem in the context .*)
12.43 - bdvs : Rule.subst, (*bound variables to modify... .*)
12.44 + bdvs : UnparseC.subst, (*bound variables to modify... .*)
12.45 thminst : term, (*... theorem instantiated .*)
12.46 applto : term, (*applied to formula ... .*)
12.47 applat : term, (*... with lhs inserted .*)
12.48 @@ -315,7 +315,7 @@
12.49 | ContRlsInst of (* a rule set with bdvs in contex =========== *)
12.50 {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
12.51 rls : Celem.guh, (*rule set in the context .*)
12.52 - bdvs : Rule.subst, (*for bound variables in thms .*)
12.53 + bdvs : UnparseC.subst, (*for bound variables in thms .*)
12.54 applto : term, (*rewrite this formula .*)
12.55 result : term, (*resulting from the rewrite .*)
12.56 asms : term list (*... with asms stored .*)
12.57 @@ -328,7 +328,7 @@
12.58 | ContNOrewInst of (* no rewrite for some instantiation ====== *)
12.59 {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
12.60 thm_rls : Celem.guh, (*thm or rls in the context .*)
12.61 - bdvs : Rule.subst, (*for bound variables in thms .*)
12.62 + bdvs : UnparseC.subst, (*for bound variables in thms .*)
12.63 thminst : term, (*... theorem instantiated .*)
12.64 applto : term (*rewrite this formula .*)
12.65 }
12.66 @@ -352,7 +352,7 @@
12.67 thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
12.68 applto = f, applat = TermC.empty, reword = ord',
12.69 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
12.70 - result = res, resasms = asm, asmrls = Rule_Set.id_rls erls}
12.71 + result = res, resasms = asm, asmrls = Rule_Set.rls2str erls}
12.72 | Applicable.Notappl _ =>
12.73 let
12.74 val pp = Ctree.par_pblobj pt p
12.75 @@ -385,7 +385,7 @@
12.76 Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
12.77 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
12.78 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
12.79 - result = res, resasms = asm, asmrls = Rule_Set.id_rls erls}
12.80 + result = res, resasms = asm, asmrls = Rule_Set.rls2str erls}
12.81 end
12.82 | Applicable.Notappl _ =>
12.83 let
12.84 @@ -444,14 +444,14 @@
12.85 fun (*find (_, Rls_ rls) = finds (get_rules rls)
12.86 | find r12 = eq_rule r12
12.87 and*) finds [] = false
12.88 - | finds (r1 :: rs) = if Rule_Set.eq_rule (r, r1) then true else finds rs
12.89 + | finds (r1 :: rs) = if Rule.eq_rule (r, r1) then true else finds rs
12.90 in
12.91 finds (Rule_Set.get_rules rls)
12.92 end
12.93
12.94 (* try if a rewrite-rule is applicable to a given formula;
12.95 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
12.96 -fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : Rule.subst) f (thm' as Rule.Thm (_, thm)) =
12.97 +fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : UnparseC.subst) f (thm' as Rule.Thm (_, thm)) =
12.98 if Auto_Prog.contains_bdv thm
12.99 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
12.100 SOME _ => [Tactic.rule2tac thy subst thm']
12.101 @@ -619,7 +619,7 @@
12.102 | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
12.103 in
12.104 case scan prog of
12.105 - NONE => (NONE: Selem.subs option, []: Rule.subst)
12.106 + NONE => (NONE: Selem.subs option, []: UnparseC.subst)
12.107 | SOME tm =>
12.108 let val subst = subst_atomic env tm
12.109 in (SOME (Selem.subst'_to_sube subst), Selem.subst'_to_subst subst) end
13.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Apr 09 17:16:48 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Thu Apr 09 18:21:09 2020 +0200
13.3 @@ -42,8 +42,8 @@
13.4 local
13.5 open Term;
13.6 in
13.7 - fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
13.8 - fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
13.9 + fun termlessI (_: UnparseC.subst) uv = LibraryC.termless uv;
13.10 + fun term_ordI (_: UnparseC.subst) uv = Term_Ord.term_ord uv;
13.11 end;
13.12 \<close> ML \<open>
13.13 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
14.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Apr 09 17:16:48 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Apr 09 18:21:09 2020 +0200
14.3 @@ -505,7 +505,7 @@
14.4
14.5 in
14.6
14.7 -fun ord_make_polynomial (pr:bool) thy (_: Rule.subst) tu =
14.8 +fun ord_make_polynomial (pr:bool) thy (_: UnparseC.subst) tu =
14.9 (term_ord' pr thy(***) tu = LESS );
14.10
14.11 end;(*local*)
15.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Apr 09 17:16:48 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Apr 09 18:21:09 2020 +0200
15.3 @@ -151,7 +151,7 @@
15.4 thy:
15.5 subst: no bound variables, only Root.sqrt
15.6 tu: the terms to compare (t1, t2) ... *)
15.7 -fun sqrt_right (pr:bool) thy (_: Rule.subst) tu =
15.8 +fun sqrt_right (pr:bool) thy (_: UnparseC.subst) tu =
15.9 (term_ord' pr thy(***) tu = LESS );
15.10 end;
15.11
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Apr 09 17:16:48 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Apr 09 18:21:09 2020 +0200
16.3 @@ -345,7 +345,7 @@
16.4 list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
16.5 in
16.6
16.7 -fun ord_make_polytest (pr:bool) thy (_: Rule.subst) tu =
16.8 +fun ord_make_polytest (pr:bool) thy (_: UnparseC.subst) tu =
16.9 (term_ord' pr thy(***) tu = LESS );
16.10
16.11 end;(*local*)
16.12 @@ -353,7 +353,7 @@
16.13
16.14 section \<open>term order\<close>
16.15 ML \<open>
16.16 -fun term_order (_: Rule.subst) tu = (term_ordI [] tu = LESS);
16.17 +fun term_order (_: UnparseC.subst) tu = (term_ordI [] tu = LESS);
16.18 \<close>
16.19
16.20 section \<open>rulesets\<close>
17.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Thu Apr 09 17:16:48 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Thu Apr 09 18:21:09 2020 +0200
17.3 @@ -6,7 +6,7 @@
17.4
17.5 ML \<open>
17.6 open Rule
17.7 -fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
17.8 +fun termlessI (_: UnparseC.subst) uv = LibraryC.termless uv;
17.9 \<close>
17.10 axiomatization where
17.11 thm111: "thm111 = thm111 + (111::int)" and
18.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Thu Apr 09 17:16:48 2020 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Thu Apr 09 18:21:09 2020 +0200
18.3 @@ -59,11 +59,11 @@
18.4 fun topt2str NONE = "NONE"
18.5 | topt2str (SOME t) = "SOME " ^ UnparseC.term2str t;
18.6 fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)
18.7 - "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id_rls eval ^ ", " ^
18.8 + "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.rls2str eval ^ ", " ^
18.9 topt2str form_arg ^ ", \n" ^ UnparseC.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
18.10 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
18.11 fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)
18.12 - "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id_rls eval ^ ", " ^
18.13 + "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.rls2str eval ^ ", " ^
18.14 topt2str form_arg ^ ", " ^ UnparseC.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
18.15 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
18.16
19.1 --- a/src/Tools/isac/MathEngBasic/model.sml Thu Apr 09 17:16:48 2020 +0200
19.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Thu Apr 09 18:21:09 2020 +0200
19.3 @@ -12,11 +12,11 @@
19.4 val oris2str : ori list -> string
19.5 val e_ori : ori
19.6 datatype item
19.7 - = Correct of Rule.cterm' | False of Rule.cterm' | Incompl of Rule.cterm' | Missing of Rule.cterm' | Superfl of string
19.8 + = Correct of UnparseC.cterm' | False of UnparseC.cterm' | Incompl of UnparseC.cterm' | Missing of UnparseC.cterm' | Superfl of string
19.9 | SyntaxE of string | TypeE of string
19.10 datatype itm_ = Cor of (term * (term list)) * (term * (term list))
19.11 - | Syn of Rule.cterm' | Typ of Rule.cterm' | Inc of (term * (term list)) * (term * (term list))
19.12 - | Sup of (term * (term list)) | Mis of (term * term) | Par of Rule.cterm'
19.13 + | Syn of UnparseC.cterm' | Typ of UnparseC.cterm' | Inc of (term * (term list)) * (term * (term list))
19.14 + | Sup of (term * (term list)) | Mis of (term * term) | Par of UnparseC.cterm'
19.15 val itm_2str : itm_ -> string
19.16 val itm_2str_ : Proof.context -> itm_ -> string
19.17 type itm
19.18 @@ -255,13 +255,13 @@
19.19 Cor of (term * (* description *)
19.20 (term list)) * (* for list: elem-wise input *)
19.21 (term * (term list)) (* elem of penv ---- penv delayed to future *)
19.22 -| Syn of Rule.cterm'
19.23 -| Typ of Rule.cterm'
19.24 +| Syn of UnparseC.cterm'
19.25 +| Typ of UnparseC.cterm'
19.26 | Inc of (term * (term list)) * (term * (term list)) (*lists,
19.27 + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
19.28 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
19.29 | Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
19.30 -| Par of Rule.cterm'; (* internal state from fun parsitm *)
19.31 +| Par of UnparseC.cterm'; (* internal state from fun parsitm *)
19.32
19.33 type vats = int list; (* variants in formalizations *)
19.34
19.35 @@ -374,13 +374,13 @@
19.36
19.37 (* for _output_ of the items of a Model *)
19.38 datatype item =
19.39 - Correct of Rule.cterm' (* labels a correct formula (type cterm') *)
19.40 + Correct of UnparseC.cterm' (* labels a correct formula (type cterm') *)
19.41 | SyntaxE of string (**)
19.42 | TypeE of string (**)
19.43 - | False of Rule.cterm' (* WN050618 notexistent in itm_: only used in Where *)
19.44 - | Incompl of Rule.cterm' (**)
19.45 + | False of UnparseC.cterm' (* WN050618 notexistent in itm_: only used in Where *)
19.46 + | Incompl of UnparseC.cterm' (**)
19.47 | Superfl of string (**)
19.48 - | Missing of Rule.cterm';
19.49 + | Missing of UnparseC.cterm';
19.50 fun item2str (Correct s) ="Correct " ^ s
19.51 | item2str (SyntaxE s) ="SyntaxE " ^ s
19.52 | item2str (TypeE s) ="TypeE " ^ s
20.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Thu Apr 09 17:16:48 2020 +0200
20.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Thu Apr 09 18:21:09 2020 +0200
20.3 @@ -16,21 +16,21 @@
20.4 type subst' (* substitution in isac-programs; rename subst_prog [(bdv, x)] *)
20.5 (*type subst for rewriting, in Rule (+?Isabelle); rename subst_rew [(bools, x)] *)
20.6 (* TODO use these types in functions below and elsewhere; rename below according to types *)
20.7 - val subst'_to_sube : subst' -> Rule.cterm' list (* e.g. rename to subst_user_of_prog *)
20.8 - val subst_to_subst' : Rule.subst -> subst'
20.9 + val subst'_to_sube : subst' -> UnparseC.cterm' list (* e.g. rename to subst_user_of_prog *)
20.10 + val subst_to_subst' : UnparseC.subst -> subst'
20.11 val subst'_to_subst : subst' -> (term * term) list
20.12 - val sube2str : Rule.cterm' list -> string
20.13 - val sube2subst : theory -> Rule.cterm' list -> (term * term) list
20.14 - val sube2subte : Rule.cterm' list -> term list
20.15 - val subs2subst : theory -> Rule.cterm' list -> (term * term) list
20.16 - val subst2sube : (term * term) list -> Rule.cterm' list (* for datatypes.sml *)
20.17 - val subst2subs : (term * term) list -> Rule.cterm' list
20.18 + val sube2str : UnparseC.cterm' list -> string
20.19 + val sube2subst : theory -> UnparseC.cterm' list -> (term * term) list
20.20 + val sube2subte : UnparseC.cterm' list -> term list
20.21 + val subs2subst : theory -> UnparseC.cterm' list -> (term * term) list
20.22 + val subst2sube : (term * term) list -> UnparseC.cterm' list (* for datatypes.sml *)
20.23 + val subst2subs : (term * term) list -> UnparseC.cterm' list
20.24 val subst2subs' : (term * term) list -> (string * string) list
20.25 - val subte2sube : term list -> Rule.cterm' list
20.26 + val subte2sube : term list -> UnparseC.cterm' list
20.27
20.28 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
20.29 val e_fmz : fmz_ * Celem.spec (* for datatypes.sml *)
20.30 - val e_sube : Rule.cterm' list
20.31 + val e_sube : UnparseC.cterm' list
20.32 val e_subs : string list
20.33 val subte2subst : term list -> (term * term) list
20.34 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
20.35 @@ -49,7 +49,7 @@
20.36 (strs2str o
20.37 (map (
20.38 Celem.linefeed o pair2str o (apsnd UnparseC.term2str) o (apfst UnparseC.term2str)))) s;
20.39 -type fmz_ = Rule.cterm' list;
20.40 +type fmz_ = UnparseC.cterm' list;
20.41 (* a formalization of an example contains data
20.42 sufficient for mechanically finding the solution for the example.
20.43 FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
20.44 @@ -59,13 +59,13 @@
20.45 type result = term * term list
20.46 fun res2str (t, ts) = pair2str (UnparseC.term2str t, UnparseC.terms2str ts); (* for tests only *)
20.47
20.48 -type subs = Rule.cterm' list; (* substitution as seen by learner in tactics, in programs, etc.
20.49 +type subs = UnparseC.cterm' list; (* substitution as seen by learner in tactics, in programs, etc.
20.50 questionable design. rename to stubst_user *)
20.51 val e_subs = ["(''bdv'', x)"]; (* for tests only *)
20.52
20.53 (* argument type of tac Rewrite_Inst *)
20.54 -type sube = Rule.cterm' list; (* = subs. delete *)
20.55 -val e_sube = []: Rule.cterm' list; (* for tests only *)
20.56 +type sube = UnparseC.cterm' list; (* = subs. delete *)
20.57 +val e_sube = []: UnparseC.cterm' list; (* for tests only *)
20.58 fun sube2str s = strs2str s;
20.59
20.60 type subte = term list; (* _sub_stitution as _t_erms of _e_qualities: revise ! *)
20.61 @@ -77,7 +77,7 @@
20.62 |> HOLogic.dest_list
20.63 |> map HOLogic.dest_prod
20.64 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term2str e2))
20.65 - |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): Rule.cterm' list)
20.66 + |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): UnparseC.cterm' list)
20.67 handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])
20.68 fun subst_to_subst' subst = subst
20.69 |> map (apfst TermC.free2str)
21.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 17:16:48 2020 +0200
21.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 18:21:09 2020 +0200
21.3 @@ -10,8 +10,8 @@
21.4 signature TACTIC =
21.5 sig
21.6 datatype T =
21.7 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
21.8 - | Add_Relation' of Rule.cterm' * Model.itm list
21.9 + Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
21.10 + | Add_Relation' of UnparseC.cterm' * Model.itm list
21.11 | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
21.12
21.13 | Begin_Sequ' | Begin_Trans' of term
21.14 @@ -23,27 +23,27 @@
21.15 | CAScmd' of term
21.16 | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
21.17 | Check_Postcond' of Celem.pblID * term
21.18 - | Check_elementwise' of term * Rule.cterm' * Selem.result
21.19 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
21.20 + | Check_elementwise' of term * UnparseC.cterm' * Selem.result
21.21 + | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
21.22
21.23 | Derive' of Rule_Set.T
21.24 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
21.25 - | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
21.26 + | Detail_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
21.27 | End_Detail' of Selem.result
21.28
21.29 | Empty_Tac_
21.30 | Free_Solve'
21.31
21.32 - | Init_Proof' of Rule.cterm' list * Celem.spec
21.33 + | Init_Proof' of UnparseC.cterm' list * Celem.spec
21.34 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
21.35 | Or_to_List' of term * term
21.36 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
21.37 | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
21.38
21.39 | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
21.40 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * ThmC.thm'' * term * Selem.result
21.41 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
21.42 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
21.43 - | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
21.44 + | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
21.45
21.46 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
21.47 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
21.48 @@ -61,8 +61,8 @@
21.49 val string_of: T -> string
21.50
21.51 datatype input =
21.52 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
21.53 - | Apply_Assumption of Rule.cterm' list
21.54 + Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
21.55 + | Apply_Assumption of UnparseC.cterm' list
21.56 | Apply_Method of Celem.metID
21.57 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
21.58 | Begin_Sequ | Begin_Trans
21.59 @@ -71,11 +71,11 @@
21.60 | End_Sequ | End_Trans
21.61 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
21.62 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
21.63 - | CAScmd of Rule.cterm'
21.64 + | CAScmd of UnparseC.cterm'
21.65 | Calculate of string
21.66 | Check_Postcond of Celem.pblID
21.67 - | Check_elementwise of Rule.cterm'
21.68 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
21.69 + | Check_elementwise of UnparseC.cterm'
21.70 + | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
21.71
21.72 | Derive of Rule_Set.identifier
21.73 | Detail_Set of Rule_Set.identifier
21.74 @@ -85,7 +85,7 @@
21.75 | Empty_Tac
21.76 | Free_Solve
21.77
21.78 - | Init_Proof of Rule.cterm' list * Celem.spec
21.79 + | Init_Proof of UnparseC.cterm' list * Celem.spec
21.80 | Model_Problem
21.81 | Or_to_List
21.82 | Refine_Problem of Celem.pblID
21.83 @@ -103,7 +103,7 @@
21.84
21.85 | Substitute of Selem.sube
21.86 | Tac of string
21.87 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
21.88 + | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
21.89 val input_to_string : input -> string
21.90 val tac2IDstr : input -> string
21.91 val is_empty : input -> bool
21.92 @@ -144,8 +144,8 @@
21.93 see 'type tac_' for the internal representation of tactics
21.94 *)
21.95 datatype input =
21.96 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
21.97 - | Apply_Assumption of Rule.cterm' list
21.98 + Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
21.99 + | Apply_Assumption of UnparseC.cterm' list
21.100 | Apply_Method of Celem.metID
21.101 (* creates an "istate" in PblObj.env; in case of "implicit_take"
21.102 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
21.103 @@ -159,11 +159,11 @@
21.104 | End_Sequ | End_Trans
21.105 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
21.106 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
21.107 - | CAScmd of Rule.cterm'
21.108 + | CAScmd of UnparseC.cterm'
21.109 | Calculate of string
21.110 | Check_Postcond of Celem.pblID
21.111 - | Check_elementwise of Rule.cterm'
21.112 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
21.113 + | Check_elementwise of UnparseC.cterm'
21.114 + | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
21.115
21.116 | Derive of Rule_Set.identifier (* WN0509 drop *)
21.117 | Detail_Set of Rule_Set.identifier (* WN0509 drop *)
21.118 @@ -173,7 +173,7 @@
21.119 | Empty_Tac
21.120 | Free_Solve
21.121
21.122 - | Init_Proof of Rule.cterm' list * Celem.spec
21.123 + | Init_Proof of UnparseC.cterm' list * Celem.spec
21.124 | Model_Problem
21.125 | Or_to_List
21.126 | Refine_Problem of Celem.pblID
21.127 @@ -195,7 +195,7 @@
21.128
21.129 | Substitute of Selem.sube
21.130 | Tac of string (* WN0509 drop *)
21.131 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
21.132 + | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
21.133
21.134 fun input_to_string ma = case ma of
21.135 Init_Proof (ppc, spec) =>
21.136 @@ -315,9 +315,9 @@
21.137 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
21.138 | rule2tac _ subst (Rule.Thm thm'') =
21.139 Rewrite_Inst (Selem.subst2subs subst, thm'')
21.140 - | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id_rls rls)
21.141 + | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.rls2str rls)
21.142 | rule2tac _ subst (Rule.Rls_ rls) =
21.143 - Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id_rls rls))
21.144 + Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
21.145 | rule2tac _ _ rule =
21.146 error ("rule2tac: called with \"" ^ Rule_Set.rule2str rule ^ "\"");
21.147
21.148 @@ -334,8 +334,8 @@
21.149 TODO.WN161219: replace *every* cterm' by term
21.150 *)
21.151 datatype T =
21.152 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
21.153 - | Add_Relation' of Rule.cterm' * Model.itm list
21.154 + Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
21.155 + | Add_Relation' of UnparseC.cterm' * Model.itm list
21.156 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
21.157 * tactic Apply_Method metID
21.158 * formula term *)
21.159 @@ -358,17 +358,17 @@
21.160 term * (* (1) the current formula: [x=1,x=...] *)
21.161 string * (* (2) the pred from Check_elementwise *)
21.162 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
21.163 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
21.164 + | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
21.165
21.166 | Derive' of Rule_Set.T
21.167 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
21.168 - | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
21.169 + | Detail_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
21.170 | End_Detail' of Selem.result
21.171
21.172 | Empty_Tac_
21.173 | Free_Solve'
21.174
21.175 - | Init_Proof' of Rule.cterm' list * Celem.spec
21.176 + | Init_Proof' of UnparseC.cterm' list * Celem.spec
21.177 | Model_Problem' of (* first step in specifying *)
21.178 Celem.pblID * (* key into KEStore *)
21.179 Model.itm list * (* the 'untouched' pbl *)
21.180 @@ -382,9 +382,9 @@
21.181 Celem.metID * (* from new pbt?! filled in specify *)
21.182 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
21.183 | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
21.184 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * ThmC.thm'' * term * Selem.result
21.185 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
21.186 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
21.187 - | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
21.188 + | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
21.189
21.190 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
21.191 | Specify_Problem' of Celem.pblID *
21.192 @@ -437,12 +437,12 @@
21.193 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
21.194 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
21.195 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
21.196 - "," ^ Rule_Set.id_rls rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
21.197 + "," ^ Rule_Set.rls2str rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
21.198 | End_Detail' _ => "End_Detail' xxx"
21.199 | Detail_Set' _ => "Detail_Set' xxx"
21.200 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
21.201
21.202 - | Derive' rls => "Derive' " ^ Rule_Set.id_rls rls
21.203 + | Derive' rls => "Derive' " ^ Rule_Set.rls2str rls
21.204 | Calculate' _ => "Calculate' "
21.205 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
21.206
21.207 @@ -468,13 +468,13 @@
21.208 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
21.209 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
21.210
21.211 - | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id_rls rls)
21.212 - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id_rls rls)
21.213 + | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.rls2str rls)
21.214 + | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.rls2str rls)
21.215
21.216 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
21.217 - Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
21.218 + Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
21.219 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
21.220 - Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
21.221 + Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
21.222
21.223 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
21.224 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
22.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Apr 09 17:16:48 2020 +0200
22.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Apr 09 18:21:09 2020 +0200
22.3 @@ -133,7 +133,7 @@
22.4 fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
22.5 | rule2stac thy (Rule.Num_Calc (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
22.6 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))
22.7 - | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id_rls rls))
22.8 + | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.rls2str rls))
22.9 | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule_Set.rule2str r ^ "\"");
22.10 fun rule2stac_inst _ (Rule.Thm (thmID, _)) =
22.11 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
22.12 @@ -142,7 +142,7 @@
22.13 | rule2stac_inst thy (Rule.Cal1 (c, _)) =
22.14 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
22.15 | rule2stac_inst _ (Rule.Rls_ rls) =
22.16 - Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id_rls rls))
22.17 + Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.rls2str rls))
22.18 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule_Set.rule2str r ^ "\"");
22.19
22.20 (*for appropriate nesting take stacs in _reverse_ order*)
22.21 @@ -169,7 +169,7 @@
22.22 | contain_bdv (Rule.Rls_ rls :: rs) =
22.23 contain_bdv (Rule_Set.get_rules rls) orelse contain_bdv rs
22.24 | contain_bdv (r :: _) =
22.25 - error ("contain_bdv called with [" ^ Rule_Set.id_rule r ^ ",...]");
22.26 + error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]");
22.27
22.28 (* filter Frees for free_str and pair their respective types with typ *)
22.29 fun subst_typ free_str typ frees =
22.30 @@ -237,7 +237,7 @@
22.31 val prog = case rls of
22.32 Rule_Def.Repeat {rules, ...} => rules2scr_Rls thy rules
22.33 | Rule_Set.Seqence {rules, ...} => rules2scr_Seq thy rules
22.34 - | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule_Set.id_rls rls ^ "\"")
22.35 + | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule_Set.rls2str rls ^ "\"")
22.36 in
22.37 subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
22.38 end
23.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Apr 09 17:16:48 2020 +0200
23.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Apr 09 18:21:09 2020 +0200
23.3 @@ -125,7 +125,7 @@
23.4 error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.t2str thy t ^ "'")
23.5 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
23.6 let
23.7 - val _= trace i (" rls: " ^ Rule_Set.id_rls rrls ^ " on: " ^ UnparseC.t2str thy t)
23.8 + val _= trace i (" rls: " ^ Rule_Set.rls2str rrls ^ " on: " ^ UnparseC.t2str thy t)
23.9 val (t', asm, rew) = app_rev thy (i + 1) rrls t
23.10 in if rew then SOME (t', distinct asm) else NONE end
23.11 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
23.12 @@ -182,7 +182,7 @@
23.13 | NONE => rew_once ruls asm ct apno thms)
23.14 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rule2str r ^ "\"");
23.15 val ruls = (#rules o Rule_Set.rep) rls;
23.16 - val _ = trace i (" rls: " ^ Rule_Set.id_rls rls ^ " on: " ^ UnparseC.t2str thy ct)
23.17 + val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)
23.18 val (ct', asm') = rew_once ruls [] ct Noap ruls;
23.19 in if ct = ct' then NONE else SOME (ct', distinct asm') end
23.20 (*------------------------
24.1 --- a/src/Tools/isac/Specify/calchead.sml Thu Apr 09 17:16:48 2020 +0200
24.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu Apr 09 18:21:09 2020 +0200
24.3 @@ -100,13 +100,13 @@
24.4 -> string * Model.itm
24.5 val ppc2list : 'a Model.ppc -> 'a list
24.6 val mk_delete: theory -> string -> Model.itm_ -> Tactic.input
24.7 - val mk_additem: string -> Rule.cterm' -> Tactic.input
24.8 + val mk_additem: string -> UnparseC.cterm' -> Tactic.input
24.9 val nxt_add: theory -> Model.ori list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
24.10 val is_error: Model.itm_ -> bool
24.11 val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * Model.itm list -> Model.itm list * Model.itm list
24.12 - val nxt_specif_additem: string -> Rule.cterm' -> Calc.T -> calcstate'
24.13 + val nxt_specif_additem: string -> UnparseC.cterm' -> Calc.T -> calcstate'
24.14 val vals_of_oris : Model.ori list -> term list
24.15 - val specify_additem: string -> Rule.cterm' -> Calc.T -> string * calcstate'
24.16 + val specify_additem: string -> UnparseC.cterm' -> Calc.T -> string * calcstate'
24.17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24.18 val e_calcstate : Calc.T * Generate.taci list
24.19 val e_calcstate' : calcstate'
24.20 @@ -123,7 +123,7 @@
24.21 val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori
24.22 datatype additm = Add of Model.itm | Err of string
24.23 val appl_add: Proof.context -> string -> Model.ori list ->
24.24 - Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
24.25 + Model.itm list -> (string * (term * term)) list -> UnparseC.cterm' -> additm
24.26 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
24.27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24.28
25.1 --- a/src/Tools/isac/Specify/generate.sml Thu Apr 09 17:16:48 2020 +0200
25.2 +++ b/src/Tools/isac/Specify/generate.sml Thu Apr 09 18:21:09 2020 +0200
25.3 @@ -11,7 +11,7 @@
25.4 datatype mout =
25.5 EmptyMout
25.6 | Error' of string
25.7 - | FormKF of Rule.cterm'
25.8 + | FormKF of UnparseC.cterm'
25.9 | PpcKF of pblmet * Model.item Model.ppc
25.10 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
25.11 val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T
25.12 @@ -96,8 +96,8 @@
25.13 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
25.14 datatype foppFK = (* in DG cases div 2 *)
25.15 EmptyFoppFK (*DG internal*)
25.16 -| FormFK of Rule.cterm'
25.17 -| PpcFK of Rule.cterm' Model.ppc
25.18 +| FormFK of UnparseC.cterm'
25.19 +| PpcFK of UnparseC.cterm' Model.ppc
25.20 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
25.21 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc
25.22 | foppFK2str EmptyFoppFK ="EmptyFoppFK"
25.23 @@ -118,7 +118,7 @@
25.24
25.25 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
25.26 Error_ of string (*<--*)
25.27 -| FormKF of cellID * edit * indent * nest * Rule.cterm' (*<--*)
25.28 +| FormKF of cellID * edit * indent * nest * UnparseC.cterm' (*<--*)
25.29 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
25.30 | RefineKF of Stool.match list (*<--*)
25.31 | RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*)
25.32 @@ -127,7 +127,7 @@
25.33 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
25.34 *)
25.35 datatype mout =
25.36 - FormKF of Rule.cterm'
25.37 + FormKF of UnparseC.cterm'
25.38 | PpcKF of (pblmet * Model.item Model.ppc)
25.39 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
25.40 | Error' of string
25.41 @@ -264,7 +264,7 @@
25.42 | generate1 (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
25.43 let
25.44 val (pt, c) = cappend_atomic pt p (is, ctxt) f
25.45 - (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule_Set.id_rls rls')) (f', asm) Complete
25.46 + (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule_Set.rls2str rls')) (f', asm) Complete
25.47 val pt = update_branch pt p TransitiveB
25.48 in
25.49 ((p, Res), c, FormKF (UnparseC.term2str f'), pt)
25.50 @@ -273,7 +273,7 @@
25.51 let
25.52 val (pt, _) = cappend_form pt p (is, ctxt) f
25.53 val pt = update_branch pt p TransitiveB
25.54 - val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule_Set.id_rls rls)) f
25.55 + val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule_Set.rls2str rls)) f
25.56 val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
25.57 val pos' = ((lev_on o lev_dn) p, Frm)
25.58 in
25.59 @@ -282,7 +282,7 @@
25.60 | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
25.61 let
25.62 val (pt, c) = cappend_atomic pt p (is, ctxt) f
25.63 - (Tactic.Rewrite_Set (Rule_Set.id_rls rls')) (f', asm) Complete
25.64 + (Tactic.Rewrite_Set (Rule_Set.rls2str rls')) (f', asm) Complete
25.65 val pt = update_branch pt p TransitiveB
25.66 in
25.67 ((p, Res), c, FormKF (UnparseC.term2str f'), pt)
25.68 @@ -291,7 +291,7 @@
25.69 let
25.70 val (pt, _) = cappend_form pt p (is, ctxt) f
25.71 val pt = update_branch pt p TransitiveB
25.72 - val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id_rls rls)) f
25.73 + val is = init_istate (Tactic.Rewrite_Set (Rule_Set.rls2str rls)) f
25.74 val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
25.75 val pos' = ((lev_on o lev_dn) p, Frm)
25.76 in
25.77 @@ -401,7 +401,7 @@
25.78 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
25.79 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
25.80 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
25.81 - val pt = update_tac pt p (Tactic.Derive (Rule_Set.id_rls nrls))
25.82 + val pt = update_tac pt p (Tactic.Derive (Rule_Set.rls2str nrls))
25.83 val pt = update_branch pt p TransitiveB
25.84 in (c, (pt, pos: pos')) end
25.85 | embed_deriv tacis (pt, (p, Res)) =
25.86 @@ -418,7 +418,7 @@
25.87 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
25.88 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
25.89 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
25.90 - val pt = update_tac pt p (Tactic.Derive (Rule_Set.id_rls nrls))
25.91 + val pt = update_tac pt p (Tactic.Derive (Rule_Set.rls2str nrls))
25.92 val pt = update_branch pt p TransitiveB
25.93 in (c, (pt, pos)) end
25.94 | embed_deriv _ _ = error "embed_deriv: uncovered definition"
26.1 --- a/src/Tools/isac/Specify/input-calchead.sml Thu Apr 09 17:16:48 2020 +0200
26.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Thu Apr 09 18:21:09 2020 +0200
26.3 @@ -5,9 +5,9 @@
26.4
26.5 signature INPUT_CALCHEAD =
26.6 sig
26.7 - datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list
26.8 + datatype iitem = Find of UnparseC.cterm' list | Given of UnparseC.cterm' list | Relate of UnparseC.cterm' list
26.9 type imodel = iitem list
26.10 - type icalhd = Pos.pos' * Rule.cterm' * imodel * Pos.pos_ * Celem.spec
26.11 + type icalhd = Pos.pos' * UnparseC.cterm' * imodel * Pos.pos_ * Celem.spec
26.12 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
26.13 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
26.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26.15 @@ -87,23 +87,23 @@
26.16 (*** handle an input calc-head ***)
26.17
26.18 datatype iitem =
26.19 - Given of Rule.cterm' list
26.20 + Given of UnparseC.cterm' list
26.21 (*Where is never input*)
26.22 -| Find of Rule.cterm' list
26.23 -| Relate of Rule.cterm' list
26.24 +| Find of UnparseC.cterm' list
26.25 +| Relate of UnparseC.cterm' list
26.26
26.27 type imodel = iitem list
26.28
26.29 (*calc-head as input*)
26.30 type icalhd =
26.31 Pos.pos' * (*the position of the calc-head in the calc-tree*)
26.32 - Rule.cterm' * (*the headline*)
26.33 + UnparseC.cterm' * (*the headline*)
26.34 imodel * (*the model (without Find) of the calc-head*)
26.35 Pos.pos_ * (*model belongs to Pbl or Met*)
26.36 Celem.spec; (*specification: domID, pblID, metID*)
26.37 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
26.38
26.39 -fun is_casinput (hdf : Rule.cterm') ((fmz_, spec) : Selem.fmz) =
26.40 +fun is_casinput (hdf : UnparseC.cterm') ((fmz_, spec) : Selem.fmz) =
26.41 hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
26.42
26.43 (* re-parse itms with a new thy and prepare for checking with ori list *)
27.1 --- a/src/Tools/isac/Test_Code/test-code.sml Thu Apr 09 17:16:48 2020 +0200
27.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Thu Apr 09 18:21:09 2020 +0200
27.3 @@ -7,7 +7,7 @@
27.4 signature TEST_CODE =
27.5 sig
27.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
27.7 - val f2str : Generate.mout -> Rule.cterm'
27.8 + val f2str : Generate.mout -> UnparseC.cterm'
27.9 val TESTg_form : Calc.T -> Generate.mout
27.10 val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
27.11 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
28.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 09 17:16:48 2020 +0200
28.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 09 18:21:09 2020 +0200
28.3 @@ -1011,7 +1011,7 @@
28.4 (*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
28.5
28.6 "~~~~~ fun appendFormula , args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
28.7 -"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: Rule.cterm')) = (cI, ifo);
28.8 +"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: UnparseC.cterm')) = (cI, ifo);
28.9 val cs = get_calc cI
28.10 val pos = get_pos cI 1;
28.11 (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
29.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 09 17:16:48 2020 +0200
29.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 09 18:21:09 2020 +0200
29.3 @@ -513,7 +513,7 @@
29.4 ([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond..ERROR*)
29.5
29.6 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
29.7 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: Rule.cterm') = ((**) "x = 1");
29.8 +"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: UnparseC.cterm') = ((**) "x = 1");
29.9 val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
29.10 val pos = (*get_pos cI 1*) p
29.11
30.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Apr 09 17:16:48 2020 +0200
30.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Apr 09 18:21:09 2020 +0200
30.3 @@ -162,8 +162,8 @@
30.4 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
30.5 val fT = type_of f;
30.6 val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
30.7 - $ HOLogic.mk_string (Rule_Set.id_rls rls) $ f;
30.8 -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule_Set.id_rls rls, idT) *)
30.9 + $ HOLogic.mk_string (Rule_Set.rls2str rls) $ f;
30.10 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule_Set.rls2str rls, idT) *)
30.11
30.12 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
30.13 case nxt of (Rewrite_Set _) => ()
31.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Apr 09 17:16:48 2020 +0200
31.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Apr 09 18:21:09 2020 +0200
31.3 @@ -83,7 +83,7 @@
31.4 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
31.5 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);
31.6
31.7 -(*+*)if Rule_Set.id_rls rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
31.8 +(*+*)if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
31.9
31.10 "~~~~~ continue me[1] after Step.by_tactic";
31.11 val (pt, p) = ptp''''';
32.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu Apr 09 17:16:48 2020 +0200
32.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu Apr 09 18:21:09 2020 +0200
32.3 @@ -68,10 +68,10 @@
32.4
32.5 (** )val (pt, c) =( **)
32.6 cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
32.7 - (Tactic.Rewrite_Set (Rule_Set.id_rls rls')) (f',asm) Complete;
32.8 + (Tactic.Rewrite_Set (Rule_Set.rls2str rls')) (f',asm) Complete;
32.9 "~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
32.10 = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
32.11 - (Tactic.Rewrite_Set (Rule_Set.id_rls rls')), (f',asm), Complete);
32.12 + (Tactic.Rewrite_Set (Rule_Set.rls2str rls')), (f',asm), Complete);
32.13 (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
32.14 val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
32.15 val (pt, cs) = cut_tree(*!*)pt (p, Frm);
33.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Thu Apr 09 17:16:48 2020 +0200
33.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Thu Apr 09 18:21:09 2020 +0200
33.3 @@ -578,7 +578,7 @@
33.4 | NONE => rew_once ruls asm ct apno thms)
33.5 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
33.6 val ruls = (#rules o Rule.Rule_Set.rep) rls;
33.7 -(* val _ = trace i (" rls: " ^ Rule_Set.id_rls rls ^ " on: " ^ UnparseC.t2str thy ct)*)
33.8 +(* val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)*)
33.9 val (ct', asm') = rew_once ruls [] ct Noap ruls;
33.10 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
33.11 = (ruls, []:term list, ct, Noap, ruls);