wneuper/isa: comparison src/Tools/isac/Interpret/rewtools.sml

equal deleted inserted replaced

-:e5a83a9fe58d
+:3163e63a5111
 case Rewrite.rewrite_ thy ro erls true tm t of
 NONE => rew_once lim rts t apno rs'
 | SOME (t', a') =>
 (if ! Celem.trace_rewrite then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
 rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
-| Rule.Num_Calc (c as (op_, _)) =>
+| Rule.Eval (c as (op_, _)) =>
 let
 val _ = if not (! Celem.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
 val t = TermC.uminus_to_string t
 in
-case Num_Calc.adhoc_thm thy c t of
+case Eval.adhoc_thm thy c t of
 NONE => rew_once lim rts t apno rs'
 | SOME (thmid, tm) =>
 (let
 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
 SOME ta => ta
 | NONE => error "adhoc_thm: NONE"
 val _ = if not (! Celem.trace_rewrite) then () else tracing("=== calc. to: " ^ UnparseC.term t')
 val r' = Rule.Thm (thmid, tm)
 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
-handle _ => error "derive_norm, Num_Calc: no rewrite"
+handle _ => error "derive_norm, Eval: no rewrite"
 end
 (*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)
 | Rule.Rls_ rls =>           (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
 (case Rewrite.rewrite_set_ thy true rls t of
 NONE => rew_once lim rts t apno rs'
 in
 	  (case Applicable.applicable_in pos pt tac of
 	     Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
 	       let
 val thm_deriv = Thm.get_name_hint thm
-val thminst = TermC.inst_bdv subst ((Num_Calc.norm o #prop o Thm.rep_thm) thm)
+val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
 	       in
 	         ContThmInst
 	          {thyID = ThyC.theory'2thyID thy',
 	           thm =
 	             Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
 val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
 val thm_deriv = Thm.get_name_hint thm
 val pp = Ctree.par_pblobj pt p
 val thy' = Ctree.get_obj Ctree.g_domID pt pp
 val subst = Selem.subs2subst (Celem.assoc_thy thy') subs
-val thminst = TermC.inst_bdv subst ((Num_Calc.norm o #prop o Thm.rep_thm) thm)
+val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
 val f = case p_ of
 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
 | _ => error "context_thy: uncovered case 3"
 in
 error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)
 (* get all theorems in a rule set (recursivley containing rule sets) *)
 fun thm_of_rule Rule.Erule = []
 | thm_of_rule (thm as Rule.Thm _) = [thm]
-| thm_of_rule (Rule.Num_Calc _) = []
+| thm_of_rule (Rule.Eval _) = []
 | thm_of_rule (Rule.Cal1 _) = []
 | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
 and thms_of_rls Rule_Set.Empty = []
 | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map  thm_of_rule)) rules
-| thms_of_rls (Rule_Set.Seqence {rules,...}) = (flat o (map  thm_of_rule)) rules
+| thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map  thm_of_rule)) rules
 | thms_of_rls (Rule_Set.Rrls _) = []
 (* check if a rule is contained in a rule-set (recursivley down in Rls_);
 this rule can even be a rule-set itself                             *)
 fun contains_rule r rls =
 	    SOME _ => [Tactic.rule2tac thy subst thm']
 	  | NONE => []
 else (case Rewrite.rewrite_ thy ro erls false thm f of
 	    SOME _ => [Tactic.rule2tac thy [] thm']
 	  | NONE => [])
-| try_rew thy _ _ _ f (cal as Rule.Num_Calc c) =
+| try_rew thy _ _ _ f (cal as Rule.Eval c) =
-(case Num_Calc.adhoc_thm thy c f of
+(case Eval.adhoc_thm thy c f of
 	    SOME _ => [Tactic.rule2tac thy [] cal]
 | NONE => [])
 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
-(case Num_Calc.adhoc_thm thy c f of
+(case Eval.adhoc_thm thy c f of
 	      SOME _ => [Tactic.rule2tac thy [] cal]
 | NONE => [])
 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
 gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
-| filter_appl_rews thy subst f (Rule_Set.Seqence {rew_ord = ro, erls, rules,...}) =
+| filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
 gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
 (* decide if a tactic is applicable to a given formula;
 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
 fun atomic_appl_tacs thy _ _ f (Tactic.Calculate scrID) =
-try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Num_Calc (assoc_calc' thy scrID |> snd))
+try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
 | atomic_appl_tacs thy ro erls f (Tactic.Rewrite thm'') =
 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
 | atomic_appl_tacs thy ro erls f (Tactic.Rewrite_Inst (subs, thm'')) =
 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Selem.subs2subst thy subs) f (Rule.Thm thm'')

changeset 59878	3163e63a5111
parent 59876	eff0b9fc6caa
child 59879	33449c96d99f