1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -6,29 +6,29 @@
1.4 sig
1.5 val assoc_thm': theory -> Celem.thm' -> thm
1.6 val assoc_thm'': theory -> Celem.thmID -> thm
1.7 - val calculate_: theory -> string * Celem.eval_fn -> term -> (term * (string * thm)) option
1.8 - val eval__true: theory -> int -> term list -> (term * term) list -> Celem.rls -> term list * bool
1.9 - val eval_listexpr_: theory -> Celem.rls -> term -> term
1.10 - val eval_true: theory -> term list -> Celem.rls -> bool
1.11 - val eval_true_: Celem.theory' -> Celem.rls -> term -> bool
1.12 + val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option
1.13 + val eval__true: theory -> int -> term list -> (term * term) list -> Rule.rls -> term list * bool
1.14 + val eval_listexpr_: theory -> Rule.rls -> term -> term
1.15 + val eval_true: theory -> term list -> Rule.rls -> bool
1.16 + val eval_true_: Rule.theory' -> Rule.rls -> term -> bool
1.17 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
1.18 - -> Celem.rls -> bool -> Celem.lrd list -> term -> term -> term * term list * Celem.lrd list * bool
1.19 - val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Celem.rls -> bool -> thm ->
1.20 + -> Rule.rls -> bool -> Celem.lrd list -> term -> term -> term * term list * Celem.lrd list * bool
1.21 + val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool -> thm ->
1.22 term -> (term * term list) option
1.23 - val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Celem.rls -> bool
1.24 + val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool
1.25 -> (term * term) list -> thm -> term -> (term * term list) option
1.26 - val rewrite_set_: theory -> bool -> Celem.rls -> term -> (term * term list) option
1.27 - val rewrite_set_inst_: theory -> bool -> (term * term) list -> Celem.rls -> term -> (term * term list) option
1.28 - val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Celem.rls -> term list
1.29 + val rewrite_set_: theory -> bool -> Rule.rls -> term -> (term * term list) option
1.30 + val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
1.31 + val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> term list
1.32 -> term -> (term * term list) option
1.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.34 (* NONE *)
1.35 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.36 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
1.37 - Celem.rls -> bool -> thm -> term -> (term * term list) option
1.38 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> Celem.rls -> term -> (term * term list) option
1.39 - val app_rev: theory -> int -> Celem.rls -> term -> term * term list * bool
1.40 - val app_sub: theory -> int -> Celem.rls -> term -> term * term list * bool
1.41 + Rule.rls -> bool -> thm -> term -> (term * term list) option
1.42 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
1.43 + val app_rev: theory -> int -> Rule.rls -> term -> term * term list * bool
1.44 + val app_sub: theory -> int -> Rule.rls -> term -> term * term list * bool
1.45 val mk_thm: theory -> string -> thm
1.46 val trace1: int -> string -> unit
1.47 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.48 @@ -62,7 +62,7 @@
1.49 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.50 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.51 val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
1.52 - then tracing (idt "#" (i + 1) ^ " eval asms: " ^ Celem.t2str thy r') else ()
1.53 + then tracing (idt "#" (i + 1) ^ " eval asms: " ^ Rule.t2str thy r') else ()
1.54 val (t'', p'') = (*conditional rewriting*)
1.55 let
1.56 val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
1.57 @@ -70,20 +70,20 @@
1.58 if nofalse
1.59 then
1.60 (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
1.61 - then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ Celem.ts2str thy p' ^
1.62 - " stored: " ^ Celem.ts2str thy simpl_p')
1.63 + then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ Rule.ts2str thy p' ^
1.64 + " stored: " ^ Rule.ts2str thy simpl_p')
1.65 else();
1.66 (t',simpl_p')) (* uncond.rew. from above*)
1.67 else
1.68 (if ! Celem.trace_rewrite andalso i < ! Celem.depth
1.69 - then tracing (idt "#" (i + 1) ^ " asms false: " ^ Celem.ts2str thy p')
1.70 + then tracing (idt "#" (i + 1) ^ " asms false: " ^ Rule.ts2str thy p')
1.71 else();
1.72 raise STOP_REW_SUB (* don't go into subterms of cond *))
1.73 end
1.74 in
1.75 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.76 then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
1.77 - then tracing (idt"#"i ^ " not: \"" ^ Celem.t2str thy t ^ "\" > \"" ^ Celem.t2str thy t' ^ "\"")
1.78 + then tracing (idt"#"i ^ " not: \"" ^ Rule.t2str thy t ^ "\" > \"" ^ Rule.t2str thy t' ^ "\"")
1.79 else ();
1.80 raise NO_REWRITE)
1.81 else (t'', p'', [], true)
1.82 @@ -121,11 +121,11 @@
1.83 (*asm false .. thm not applied ^^^; continue until False vvv*)
1.84 else chk (indets @ [t] @ a') asms);
1.85 in chk [] asms end
1.86 -and rewrite__set_ thy _ __ Celem.Erls t = (* rewrite with a rule set *)
1.87 - error ("rewrite__set_ called with 'Erls' for '" ^ Celem.t2str thy t ^ "'")
1.88 - | rewrite__set_ thy i _ _ (rrls as Celem.Rrls _) t = (* rewrite with a 'reverse rule set' *)
1.89 +and rewrite__set_ thy _ __ Rule.Erls t = (* rewrite with a rule set *)
1.90 + error ("rewrite__set_ called with 'Erls' for '" ^ Rule.t2str thy t ^ "'")
1.91 + | rewrite__set_ thy i _ _ (rrls as Rule.Rrls _) t = (* rewrite with a 'reverse rule set' *)
1.92 let
1.93 - val _= trace i (" rls: " ^ Celem.id_rls rrls ^ " on: " ^ Celem.t2str thy t)
1.94 + val _= trace i (" rls: " ^ Rule.id_rls rrls ^ " on: " ^ Rule.t2str thy t)
1.95 val (t', asm, rew) = app_rev thy (i + 1) rrls t
1.96 in if rew then SOME (t', distinct asm) else NONE end
1.97 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Calc, Cal1 *)
1.98 @@ -134,55 +134,55 @@
1.99 datatype switch = Appl | Noap;
1.100 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Tools.rew_once? *)
1.101 | rew_once ruls asm ct Appl [] =
1.102 - (case rls of Celem.Rls _ => rew_once ruls asm ct Noap ruls
1.103 - | Celem.Seq _ => (ct, asm)
1.104 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Celem.rls2str rls ^ "\""))
1.105 + (case rls of Rule.Rls _ => rew_once ruls asm ct Noap ruls
1.106 + | Rule.Seq _ => (ct, asm)
1.107 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
1.108 | rew_once ruls asm ct apno (rul :: thms) =
1.109 case rul of
1.110 - Celem.Thm (thmid, thm) =>
1.111 + Rule.Thm (thmid, thm) =>
1.112 (trace1 i (" try thm: " ^ thmid);
1.113 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Celem.rep_rls) rls)
1.114 - ((#erls o Celem.rep_rls) rls) put_asm thm ct of
1.115 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.116 + ((#erls o Rule.rep_rls) rls) put_asm thm ct of
1.117 NONE => rew_once ruls asm ct apno thms
1.118 | SOME (ct', asm') =>
1.119 - (trace1 i (" rewrites to: " ^ Celem.t2str thy ct');
1.120 + (trace1 i (" rewrites to: " ^ Rule.t2str thy ct');
1.121 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.122 (* once again try the same rule, e.g. associativity against "()"*)
1.123 - | Celem.Calc (cc as (op_, _)) =>
1.124 + | Rule.Calc (cc as (op_, _)) =>
1.125 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
1.126 val ct = TermC.uminus_to_string ct
1.127 in case Calc.adhoc_thm thy cc ct of
1.128 NONE => rew_once ruls asm ct apno thms
1.129 | SOME (_, thm') =>
1.130 let
1.131 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Celem.rep_rls) rls)
1.132 - ((#erls o Celem.rep_rls) rls) put_asm thm' ct;
1.133 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.134 + ((#erls o Rule.rep_rls) rls) put_asm thm' ct;
1.135 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.136 - Celem.string_of_thmI thm' ^ "\" " ^ Celem.t2str thy ct ^ " = NONE")
1.137 - val _ = trace1 i (" calc. to: " ^ Celem.t2str thy ((fst o the) pairopt))
1.138 + Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
1.139 + val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt))
1.140 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.141 end
1.142 - | Celem.Cal1 (cc as (op_, _)) =>
1.143 + | Rule.Cal1 (cc as (op_, _)) =>
1.144 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
1.145 val ct = TermC.uminus_to_string ct
1.146 in case Calc.adhoc_thm1_ thy cc ct of
1.147 NONE => (ct, asm)
1.148 | SOME (_, thm') =>
1.149 let
1.150 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Celem.rep_rls) rls)
1.151 - ((#erls o Celem.rep_rls) rls) put_asm thm' ct;
1.152 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.153 + ((#erls o Rule.rep_rls) rls) put_asm thm' ct;
1.154 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.155 - Celem.string_of_thmI thm' ^ "\" " ^ Celem.t2str thy ct ^ " = NONE")
1.156 - val _ = trace1 i (" cal1. to: " ^ Celem.t2str thy ((fst o the) pairopt))
1.157 + Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
1.158 + val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt))
1.159 in the pairopt end
1.160 end
1.161 - | Celem.Rls_ rls' =>
1.162 + | Rule.Rls_ rls' =>
1.163 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
1.164 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.165 | NONE => rew_once ruls asm ct apno thms)
1.166 - | r => raise ERROR ("rew_once not appl. to \"" ^ Celem.rule2str r ^ "\"");
1.167 - val ruls = (#rules o Celem.rep_rls) rls;
1.168 - val _ = trace i (" rls: " ^ Celem.id_rls rls ^ " on: " ^ Celem.t2str thy ct)
1.169 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
1.170 + val ruls = (#rules o Rule.rep_rls) rls;
1.171 + val _ = trace i (" rls: " ^ Rule.id_rls rls ^ " on: " ^ Rule.t2str thy ct)
1.172 val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.173 in if ct = ct' then NONE else SOME (ct', distinct asm') end
1.174 (*------------------------
1.175 @@ -204,9 +204,9 @@
1.176 if f pp then true else scan_ f pps;
1.177 in scan_ chk prepat end;
1.178 (* apply the normal_form of a rev-set *)
1.179 - fun app_rev' thy (Celem.Rrls {erls, prepat, scr = Celem.Rfuns {normal_form, ...}, ...}) t =
1.180 + fun app_rev' thy (Rule.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
1.181 if chk_prepat thy erls prepat t then normal_form t else NONE
1.182 - | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Celem.rls2str r ^ "\"");
1.183 + | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule.rls2str r ^ "\"");
1.184 val opt = app_rev' thy rrls t
1.185 in
1.186 case opt of
1.187 @@ -259,8 +259,8 @@
1.188 then rew_ (t'', asm' @ asm'') rules t''
1.189 else rew_ (t', asm') rs t'
1.190 end
1.191 - val (t'', asm'') = rew_ (Celem.e_term, []) equs t
1.192 - in if t'' = Celem.e_term then NONE else SOME (t'', asm'')
1.193 + val (t'', asm'') = rew_ (Rule.e_term, []) equs t
1.194 + in if t'' = Rule.e_term then NONE else SOME (t'', asm'')
1.195 end;
1.196
1.197 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
1.198 @@ -269,7 +269,7 @@
1.199 in case Calc.adhoc_thm thy isa_fn ct of
1.200 NONE => NONE
1.201 | SOME (thmID, thm) =>
1.202 - (let val rew = case rewrite_ thy Celem.dummy_ord Celem.e_rls false thm ct of
1.203 + (let val rew = case rewrite_ thy Rule.dummy_ord Rule.e_rls false thm ct of
1.204 SOME (rew, _) => rew
1.205 | NONE => raise ERROR ""
1.206 in SOME (rew, (thmID, thm)) end)
1.207 @@ -319,7 +319,7 @@
1.208 then mk_thm thy ct'
1.209 else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
1.210 ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
1.211 - error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Celem.theory2domID thy ^ "\" (and parents)")
1.212 + error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Rule.theory2domID thy ^ "\" (and parents)")
1.213
1.214 fun eval_listexpr_ thy srls t =
1.215 let val rew = rewrite_set_ thy false srls t;