1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Dec 21 11:27:22 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 10:25:49 2016 +0100
1.3 @@ -7,7 +7,7 @@
1.4 sig
1.5 type deriv
1.6 val contains_rule : rule -> rls -> bool
1.7 - val atomic_appl_tacs : theory -> string -> rls -> term -> tac -> tac list
1.8 + val atomic_appl_tacs : theory -> string -> rls -> term -> Ctree.tac -> Ctree.tac list
1.9 val thy_containing_rls : theory' -> rls' -> string * theory'
1.10 val thy_containing_cal : theory' -> prog_calcID -> string * string
1.11 datatype contthy
1.12 @@ -29,17 +29,17 @@
1.13 val thms_of_rls : rls -> rule list
1.14 val theID2filename : theID -> filename
1.15 val no_thycontext : guh -> bool
1.16 - val subs_from : istate -> 'a -> guh -> subs
1.17 - val guh2rewtac : guh -> subs -> tac
1.18 - val get_tac_checked : ptree -> pos' -> tac
1.19 - val context_thy : ptree * (pos * pos_) -> tac -> contthy
1.20 + val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
1.21 + val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
1.22 + val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac
1.23 + val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy
1.24 val distinct_Thm : rule list -> rule list
1.25 val eq_Thms : string list -> rule -> bool
1.26 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
1.27 term option -> term -> deriv
1.28 val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
1.29 term option -> term -> (rule * (term * term list)) list
1.30 - val get_bdv_subst : term -> (term * term) list -> subs option * subst
1.31 + val get_bdv_subst : term -> (term * term) list -> Ctree.subs option * subst
1.32 val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename
1.33 val guh2theID : guh -> theID
1.34 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.35 @@ -353,18 +353,18 @@
1.36
1.37 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
1.38 pass other tacs unchanged.*)
1.39 -fun get_tac_checked pt ((p, _) : pos') = get_obj g_tac pt p;
1.40 +fun get_tac_checked pt ((p, _) : Ctree.pos') = Ctree.get_obj Ctree.g_tac pt p;
1.41
1.42 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
1.43 fun deriv_of_thm'' ((thmID, _) : thm'') =
1.44 thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint
1.45
1.46 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
1.47 -fun context_thy (pt, pos as (p,p_)) (tac as Rewrite thm'') =
1.48 +fun context_thy (pt, pos as (p,p_)) (tac as Ctree.Rewrite thm'') =
1.49 let val thm_deriv = deriv_of_thm'' thm''
1.50 in
1.51 (case Applicable.applicable_in pos pt tac of
1.52 - Chead.Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
1.53 + Chead.Appl (Ctree.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
1.54 ContThm
1.55 {thyID = theory'2thyID thy',
1.56 thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
1.57 @@ -373,11 +373,11 @@
1.58 result = res, resasms = asm, asmrls = id_rls erls}
1.59 | Chead.Notappl _ =>
1.60 let
1.61 - val pp = par_pblobj pt p
1.62 - val thy' = get_obj g_domID pt pp
1.63 + val pp = Ctree.par_pblobj pt p
1.64 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
1.65 val f = case p_ of
1.66 - Frm => get_obj g_form pt p
1.67 - | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy: uncovered position"
1.68 + Frm => Ctree.get_obj Ctree.g_form pt p
1.69 + | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p | _ => error "context_thy: uncovered position"
1.70 in
1.71 ContNOrew
1.72 {thyID = theory'2thyID thy',
1.73 @@ -387,11 +387,11 @@
1.74 end
1.75 | _ => error "context_thy..Rewrite: uncovered case 2")
1.76 end
1.77 - | context_thy (pt, pos as (p, p_)) (tac as Rewrite_Inst (subs, (thmID, _))) =
1.78 + | context_thy (pt, pos as (p, p_)) (tac as Ctree.Rewrite_Inst (subs, (thmID, _))) =
1.79 let val thm = Global_Theory.get_thm (Isac ()) thmID
1.80 in
1.81 (case Applicable.applicable_in pos pt tac of
1.82 - Chead.Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
1.83 + Chead.Appl (Ctree.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
1.84 let
1.85 val thm_deriv = Thm.get_name_hint thm
1.86 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
1.87 @@ -408,13 +408,13 @@
1.88 let
1.89 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
1.90 val thm_deriv = Thm.get_name_hint thm
1.91 - val pp = par_pblobj pt p
1.92 - val thy' = get_obj g_domID pt pp
1.93 - val subst = subs2subst (assoc_thy thy') subs
1.94 + val pp = Ctree.par_pblobj pt p
1.95 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
1.96 + val subst = Ctree.subs2subst (assoc_thy thy') subs
1.97 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
1.98 val f = case p_ of
1.99 - Frm => get_obj g_form pt p
1.100 - | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy: uncovered case 3"
1.101 + Frm => Ctree.get_obj Ctree.g_form pt p
1.102 + | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p | _ => error "context_thy: uncovered case 3"
1.103 in
1.104 ContNOrewInst
1.105 {thyID = theory'2thyID thy',
1.106 @@ -423,24 +423,24 @@
1.107 end
1.108 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
1.109 end
1.110 - | context_thy (pt, p) (tac as Rewrite_Set rls') =
1.111 + | context_thy (pt, p) (tac as Ctree.Rewrite_Set rls') =
1.112 (case Applicable.applicable_in p pt tac of
1.113 - Chead.Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
1.114 + Chead.Appl (Ctree.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
1.115 ContRls
1.116 {thyID = theory'2thyID thy',
1.117 rls = rls2guh (thy_containing_rls thy' rls') rls',
1.118 applto = f, result = res, asms = asm}
1.119 | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
1.120 - | context_thy (pt,p) (tac as Rewrite_Set_Inst (_(*subs*), rls')) =
1.121 + | context_thy (pt,p) (tac as Ctree.Rewrite_Set_Inst (_(*subs*), rls')) =
1.122 (case Applicable.applicable_in p pt tac of
1.123 - Chead.Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
1.124 + Chead.Appl (Ctree.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
1.125 ContRlsInst
1.126 {thyID = theory'2thyID thy',
1.127 rls = rls2guh (thy_containing_rls thy' rls') rls',
1.128 bdvs = subst, applto = f, result = res, asms = asm}
1.129 | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))
1.130 | context_thy (_, p) tac =
1.131 - error ("context_thy: not for tac " ^ tac2str tac ^ " at " ^ pos'2str p)
1.132 + error ("context_thy: not for tac " ^ Ctree.tac2str tac ^ " at " ^ Ctree.pos'2str p)
1.133
1.134 (* get all theorems in a rule set (recursivley containing rule sets) *)
1.135 fun thm_of_rule Erule = []
1.136 @@ -470,43 +470,43 @@
1.137 fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =
1.138 if contains_bdv thm
1.139 then case rewrite_inst_ thy ro erls false subst thm f of
1.140 - SOME _ => [rule2tac thy subst thm']
1.141 + SOME _ => [Ctree.rule2tac thy subst thm']
1.142 | NONE => []
1.143 else (case rewrite_ thy ro erls false thm f of
1.144 - SOME _ => [rule2tac thy [] thm']
1.145 + SOME _ => [Ctree.rule2tac thy [] thm']
1.146 | NONE => [])
1.147 | try_rew thy _ _ _ f (cal as Calc c) =
1.148 (case adhoc_thm thy c f of
1.149 - SOME _ => [rule2tac thy [] cal]
1.150 + SOME _ => [Ctree.rule2tac thy [] cal]
1.151 | NONE => [])
1.152 | try_rew thy _ _ _ f (cal as Cal1 c) =
1.153 (case adhoc_thm thy c f of
1.154 - SOME _ => [rule2tac thy [] cal]
1.155 + SOME _ => [Ctree.rule2tac thy [] cal]
1.156 | NONE => [])
1.157 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
1.158 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
1.159 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules, ...}) =
1.160 - gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
1.161 + gen_distinct Ctree.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
1.162 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
1.163 - gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
1.164 + gen_distinct Ctree.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
1.165 | filter_appl_rews _ _ _ (Rrls _) = []
1.166 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
1.167
1.168 (* decide if a tactic is applicable to a given formula;
1.169 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
1.170 -fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
1.171 +fun atomic_appl_tacs thy _ _ f (Ctree.Calculate scrID) =
1.172 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
1.173 - | atomic_appl_tacs thy ro erls f (Rewrite thm'') =
1.174 + | atomic_appl_tacs thy ro erls f (Ctree.Rewrite thm'') =
1.175 try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')
1.176 - | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'')) =
1.177 - try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f (Thm thm'')
1.178 + | atomic_appl_tacs thy ro erls f (Ctree.Rewrite_Inst (subs, thm'')) =
1.179 + try_rew thy (ro, assoc_rew_ord ro) erls (Ctree.subs2subst thy subs) f (Thm thm'')
1.180
1.181 - | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
1.182 + | atomic_appl_tacs thy _ _ f (Ctree.Rewrite_Set rls') =
1.183 filter_appl_rews thy [] f (assoc_rls rls')
1.184 - | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
1.185 - filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
1.186 + | atomic_appl_tacs thy _ _ f (Ctree.Rewrite_Set_Inst (subs, rls')) =
1.187 + filter_appl_rews thy (Ctree.subs2subst thy subs) f (assoc_rls rls')
1.188 | atomic_appl_tacs _ _ _ _ tac =
1.189 - (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ tac2str tac ^ "'"); []);
1.190 + (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Ctree.tac2str tac ^ "'"); []);
1.191
1.192 (* filenames not only for thydata, but also for thy's etc *)
1.193 fun theID2filename (theID : theID) = theID2guh theID ^ ".xml" : filename
1.194 @@ -554,14 +554,14 @@
1.195
1.196 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
1.197
1.198 -fun guh2rewtac (guh : guh) ([] : subs) =
1.199 +fun guh2rewtac (guh : guh) ([] : Ctree.subs) =
1.200 let
1.201 val (_, thy, sect, xstr) = case guh2theID guh of
1.202 [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
1.203 | _ => error "guh2rewtac: uncovered case"
1.204 in case sect of
1.205 - "Theorems" => Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
1.206 - | "Rulesets" => Rewrite_Set xstr
1.207 + "Theorems" => Ctree.Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
1.208 + | "Rulesets" => Ctree.Rewrite_Set xstr
1.209 | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
1.210 end
1.211 | guh2rewtac guh subs =
1.212 @@ -571,8 +571,8 @@
1.213 | _ => error "guh2rewtac: uncovered case"
1.214 in case sect of
1.215 "Theorems" =>
1.216 - Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
1.217 - | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
1.218 + Ctree.Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
1.219 + | "Rulesets" => Ctree.Rewrite_Set_Inst (subs, xstr)
1.220 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
1.221 end
1.222
1.223 @@ -587,7 +587,7 @@
1.224 # otherwise []
1.225 WN060617 hack assuming that all scripts use only one bound variable
1.226 and use 'v_' as the formal argument for this bound variable*)
1.227 -fun subs_from (ScrState (env, _, _, _, _, _)) _ (guh : guh) =
1.228 +fun subs_from (Ctree.ScrState (env, _, _, _, _, _)) _ (guh : guh) =
1.229 let
1.230 val (_, _, thyID, sect, xstr) = case guh2theID guh of
1.231 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
1.232 @@ -602,7 +602,7 @@
1.233 let
1.234 val formal_arg = str2term "v_"
1.235 val value = subst_atomic env formal_arg
1.236 - in ["(bdv," ^ term2str value ^ ")"] : subs end
1.237 + in ["(bdv," ^ term2str value ^ ")"] : Ctree.subs end
1.238 else []
1.239 end
1.240 | "Rulesets" =>
1.241 @@ -614,7 +614,7 @@
1.242 let
1.243 val formal_arg = str2term "v_"
1.244 val value = subst_atomic env formal_arg
1.245 - in ["(bdv," ^ term2str value ^ ")"] : subs end
1.246 + in ["(bdv," ^ term2str value ^ ")"] : Ctree.subs end
1.247 else []
1.248 end
1.249 | str => error ("subs_from: uncovered case with " ^ str)
1.250 @@ -635,13 +635,13 @@
1.251 | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
1.252 in
1.253 case scan prog of
1.254 - NONE => (NONE: subs option, []: subst)
1.255 + NONE => (NONE: Ctree.subs option, []: subst)
1.256 | SOME tm =>
1.257 let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair
1.258 (* "[(bdv,v_v)]": term
1.259 |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
1.260 |> [("bdv","x")]: (term * term) list *)
1.261 - in (SOME (subst2subs subst), subst) end
1.262 + in (SOME (Ctree.subst2subs subst), subst) end
1.263 (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)
1.264 end
1.265