1.1 --- a/src/Tools/isac/calcelems.sml Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -9,33 +9,6 @@
1.4
1.5 signature CALC_ELEMENT =
1.6 sig
1.7 - type eval_fn
1.8 - type rew_ord
1.9 - eqtype errpatID
1.10 - type calc
1.11 - datatype rule = Cal1 of string * eval_fn | Calc of string * eval_fn | Erule | Rls_ of rls
1.12 - | Thm of string * thm
1.13 - and scr
1.14 - = EmptyScr
1.15 - | Prog of term
1.16 - | Rfuns of
1.17 - {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
1.18 - init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
1.19 - locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
1.20 - next_rule: rule list list -> term -> rule option,
1.21 - normal_form: term -> (term * term list) option}
1.22 - and rls =
1.23 - Erls
1.24 - | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.25 - rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.26 - | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.27 - rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.28 - | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list,
1.29 - id: string, prepat: (term list * term) list, rew_ord: rew_ord, scr: scr}
1.30 -
1.31 - eqtype rls'
1.32 - eqtype prog_calcID
1.33 - eqtype calID
1.34 type cas_elem
1.35 type pbt
1.36 type ptyps
1.37 @@ -45,27 +18,23 @@
1.38 type met
1.39 datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
1.40
1.41 - type cal = calID * eval_fn
1.42 type authors
1.43 type guh
1.44 - type subst
1.45 - val env2str: subst -> string
1.46 - val subst2str: subst -> string
1.47 - val subst2str': subst -> string
1.48 + val env2str: Rule.subst -> string
1.49 + val subst2str: Rule.subst -> string
1.50 + val subst2str': Rule.subst -> string
1.51
1.52 type fillpat
1.53 datatype thydata
1.54 - = Hcal of {calc: calc, coursedesign: authors, guh: guh, mathauthors: authors}
1.55 - | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: subst -> term * term -> bool}
1.56 - | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * rls}
1.57 + = Hcal of {calc: Rule.calc, coursedesign: authors, guh: guh, mathauthors: authors}
1.58 + | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}
1.59 + | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule.rls}
1.60 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
1.61 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
1.62 type theID
1.63 type rlss_elem
1.64 val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list
1.65 val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
1.66 - type calc_elem
1.67 - val calc_eq: calc_elem * calc_elem -> bool
1.68 type spec
1.69 val cas_eq: cas_elem * cas_elem -> bool
1.70 val e_Ptyp: pbt ptyp
1.71 @@ -86,30 +55,21 @@
1.72 val thes2str: thydata list -> string
1.73 val theID2str: string list -> string
1.74 val the2str: thydata -> string
1.75 - val thy2ctxt: theory -> Proof.context
1.76 val trace_calc: bool Unsynchronized.ref
1.77 eqtype thmID
1.78 type thm'
1.79 datatype lrd = D | L | R
1.80 val trace_rewrite: bool Unsynchronized.ref
1.81 val depth: int Unsynchronized.ref
1.82 - val t2str: theory -> term -> string
1.83 - val id_rls: rls -> string
1.84 - val rls2str: rls -> string
1.85 + val id_rls: Rule.rls -> string
1.86 + val rls2str: Rule.rls -> string
1.87 type errpat
1.88 - val rep_rls: rls -> {calc: calc list, erls: rls, errpats: errpatID list, id: string,
1.89 - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.90 - val e_term: term
1.91 - val dummy_ord: subst -> term * term -> bool
1.92 val assoc_thy: Rule.theory' -> theory
1.93 - val id_rule: rule -> string
1.94 eqtype cterm'
1.95 - type rrlsstate = term * term * rule list list * (rule * (term * term list)) list
1.96 type loc_
1.97 val loc_2str: loc_ -> string
1.98 eqtype rew_ord'
1.99 type thm''
1.100 - type rew_ord_
1.101 val metID2str: string list -> string
1.102 val e_pblID: pblID
1.103 val e_metID: metID
1.104 @@ -122,28 +82,21 @@
1.105 val coll_pblguhs: pbt ptyp list -> guh list
1.106 val coll_metguhs: met ptyp list -> guh list
1.107 type pat
1.108 - val e_type: typ
1.109 val pats2str: pat list -> string
1.110 val maxthy: theory -> theory -> theory
1.111 - val e_evalfn: 'a -> term -> theory -> (string * term) option
1.112 - val assoc_rew_ord: string -> subst -> term * term -> bool
1.113 eqtype filename
1.114 val lim_deriv: int Unsynchronized.ref
1.115 - val id_of_thm: rule -> string
1.116 + val id_of_thm: Rule.rule -> string
1.117 val isabthys: unit -> theory list
1.118 val thyID_of_derivation_name: string -> string
1.119 val partID': Rule.theory' -> string
1.120 val thm2guh: string * Rule.thyID -> thmID -> guh
1.121 val thmID_of_derivation_name: string -> string
1.122 - val rls2guh: string * Rule.thyID -> rls' -> guh
1.123 - val eq_rule: rule * rule -> bool
1.124 - val e_rew_ordX: rew_ord
1.125 + val rls2guh: string * Rule.thyID -> Rule.rls' -> guh
1.126 val theID2guh: theID -> guh
1.127 - val e_rule: rule
1.128 - val type2str: typ -> string
1.129 eqtype fillpatID
1.130 type pbt_ = string * (term * term)
1.131 - val e_rew_ord: subst -> term * term -> bool
1.132 + val e_rew_ord: Rule.subst -> term * term -> bool
1.133 eqtype xml
1.134 val cal2guh: string * Rule.thyID -> string -> guh
1.135 val ketype2str': ketype -> string
1.136 @@ -154,13 +107,12 @@
1.137 val thy2guh: theID -> guh
1.138 val thypart2guh: theID -> guh
1.139 val ord2guh: string * Rule.thyID -> rew_ord' -> guh
1.140 - val update_hrls: thydata -> errpatID list -> thydata
1.141 + val update_hrls: thydata -> Rule.errpatID list -> thydata
1.142 eqtype iterID
1.143 eqtype calcID
1.144 val thm''_of_thm: thm -> thm''
1.145 - val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
1.146 - val e_rrlsstate: rrlsstate
1.147 - val thm_of_thm: rule -> thm
1.148 + val rew_ord': (rew_ord' * (Rule.subst -> term * term -> bool)) list Unsynchronized.ref
1.149 + val thm_of_thm: Rule.rule -> thm
1.150 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.151 val thm2str: thm -> string
1.152 val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
1.153 @@ -172,10 +124,10 @@
1.154 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.155
1.156 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.157 -val overwritelthy: theory -> (rls' * (string * rls)) list * (rls' * rls) list ->
1.158 - (rls' * (string * rls)) list end
1.159 +val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->
1.160 + (Rule.rls' * (string * Rule.rls)) list end
1.161
1.162 -
1.163 +
1.164 (**)
1.165 structure Celem(*: CALC_ELEMENT*) =
1.166 struct
1.167 @@ -206,7 +158,7 @@
1.168 type thm' = thmID * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
1.169 val thm'2xml : int -> Celem.thm' -> Celem.xml
1.170 val assoc_thm': theory -> Celem.thm' -> thm
1.171 -| Calculate' of Celem.theory' * string * term * (term * Celem.thm')
1.172 +| Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.173 *)
1.174 (* tricky combination of (string, term) for theorems in Isac:
1.175 * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
1.176 @@ -216,7 +168,6 @@
1.177 from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
1.178 *)
1.179 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
1.180 -type rls' = string;
1.181
1.182 (*.a 'guh'='globally unique handle' is a string unique for each element
1.183 of isac's KEStore and persistent over time
1.184 @@ -287,8 +238,6 @@
1.185 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
1.186 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
1.187
1.188 -type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
1.189 - (term * term * Rule.rule list list * (Rule.rule * (term * term list)) list);
1.190
1.191
1.192 (*the key into the hierarchy ob theory elements*)
1.193 @@ -344,16 +293,6 @@
1.194 | str2ketype' "met" = Met_
1.195 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
1.196
1.197 -(* rewrite orders, also stored in 'type met' and type 'and rls'
1.198 - The association list is required for 'rewrite.."rew_ord"..' *)
1.199 -val rew_ord' = Unsynchronized.ref
1.200 - ([("e_rew_ord", Rule.e_rew_ord), ("dummy_ord", Rule.dummy_ord)]
1.201 - : (Rule.rew_ord' * (* the key for the association list *)
1.202 - (Rule.subst (* the bound variables - they get high order*)
1.203 - -> (term * term) (* (t1, t2) to be compared *)
1.204 - -> bool)) (* if t1 <= t2 then true else false *)
1.205 - list); (* association list *)
1.206 -
1.207 (* A tree for storing data defined in different theories
1.208 for access from the Interpreter and from dialogue authoring
1.209 using a string list as key.
1.210 @@ -485,7 +424,7 @@
1.211
1.212 (* datastructure for KEStore_Elems, intermediate for thehier *)
1.213 type rlss_elem =
1.214 - (rls' * (* identifier unique within Isac *)
1.215 + (Rule.rls' * (* identifier unique within Isac *)
1.216 (Rule.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
1.217 Rule.rls)) (* ((#id o rep_rls) rls) = rls' by coding discipline *)
1.218 fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2
1.219 @@ -499,9 +438,6 @@
1.220 in list_update ys i (id, (thyID, r12)) end
1.221 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;
1.222
1.223 -fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
1.224 - | assoc' ((keyi, xi) :: pairs, key) =
1.225 - if key = keyi then SOME xi else assoc' (pairs, key);
1.226
1.227 fun assoc_thy thy =
1.228 if thy = "e_domID"
1.229 @@ -518,13 +454,10 @@
1.230 in scripts...
1.231 actually a hack to get alltogether run again with minimal effort *)
1.232 fun insthy thy' (rls', rls) = (rls', (thy', rls));
1.233 -fun overwritelthy thy (al, bl:(rls' * Rule.rls) list) =
1.234 +fun overwritelthy thy (al, bl: (Rule.rls' * Rule.rls) list) =
1.235 let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl
1.236 in overwritel (al, bl') end;
1.237
1.238 -fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
1.239 - handle _ => error ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
1.240 -
1.241 fun subst2str s =
1.242 (strs2str o
1.243 (map (
1.244 @@ -595,7 +528,7 @@
1.245 met : metID list} (* methods solving the pbt *)
1.246
1.247 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
1.248 - cas = NONE, prls = Rule.Erls, where_ = [], ppc = [], met = []}
1.249 + cas = NONE, prls = Rule.Erls, where_ = [], ppc = [], met = []} : pbt
1.250 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
1.251 prls = prls', thy = thy', where_ = w'} : pbt)
1.252 = "{cas = " ^ (Rule.termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
1.253 @@ -605,7 +538,7 @@
1.254 ^ (Rule.terms2str w') ^ "}" |> linefeed;
1.255 fun pbts2str pbts = map pbt2str pbts |> list2str;
1.256
1.257 -val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[])
1.258 +val e_Ptyp = Ptyp ("e_pblID", [e_pbt], [])
1.259 type ptyps = (pbt ptyp) list
1.260
1.261 fun coll_pblguhs pbls =