1.1 --- a/src/Tools/isac/calcelems.sml Sat Mar 24 14:41:32 2018 +0100
1.2 +++ b/src/Tools/isac/calcelems.sml Sun Mar 25 11:57:33 2018 +0200
1.3 @@ -28,10 +28,10 @@
1.4 Erls
1.5 | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.6 rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.7 + | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.8 + rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.9 | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list,
1.10 id: string, prepat: (term list * term) list, rew_ord: rew_ord, scr: scr}
1.11 - | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, preconds: term list,
1.12 - rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.13
1.14 eqtype rls'
1.15 eqtype theory'
1.16 @@ -50,6 +50,10 @@
1.17 type authors
1.18 type guh
1.19 type subst
1.20 + val env2str: subst -> string
1.21 + val subst2str: subst -> string
1.22 + val subst2str': subst -> string
1.23 +
1.24 eqtype thyID
1.25 type fillpat
1.26 datatype thydata
1.27 @@ -103,7 +107,9 @@
1.28 val terms2str: term list -> string
1.29 val id_rls: rls -> string
1.30 val rls2str: rls -> string
1.31 - val rep_rls: rls -> {calc: calc list, erls: rls, id: string, preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.32 + type errpat
1.33 + val rep_rls: rls -> {calc: calc list, erls: rls, errpats: errpatID list, id: string,
1.34 + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
1.35 val string_of_thmI: thm -> string
1.36 val rule2str: rule -> string
1.37 val e_term: term
1.38 @@ -120,9 +126,6 @@
1.39 type rrlsstate = term * term * rule list list * (rule * (term * term list)) list
1.40 type loc_
1.41 val loc_2str: loc_ -> string
1.42 - val e_spec: spec
1.43 - val env2str: subst -> string
1.44 - val subst2str: subst -> string
1.45 val termopt2str: term option -> string
1.46 eqtype rew_ord'
1.47 type thm''
1.48 @@ -132,9 +135,9 @@
1.49 val e_pblID: pblID
1.50 val e_metID: metID
1.51 val empty_spec: spec
1.52 + val e_spec: spec
1.53 datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
1.54 type kestoreID
1.55 - type errpat
1.56 val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b
1.57 val ketype2str: ketype -> string
1.58 val coll_pblguhs: pbt ptyp list -> guh list
1.59 @@ -175,7 +178,6 @@
1.60 val ketype2str': ketype -> string
1.61 val str2ketype': string -> ketype
1.62 val thmID_of_derivation_name': thm -> string
1.63 - val subst2str': subst -> string
1.64 eqtype path
1.65 val theID2thyID: theID -> thyID
1.66 val thy2guh: theID -> guh
1.67 @@ -192,29 +194,35 @@
1.68 val thm_of_thm: rule -> thm
1.69 val remove_rls: string -> rls -> rule list -> rls
1.70 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.71 - (* NONE *)
1.72 + val thm2str: thm -> string
1.73 + val term_to_string'': thyID -> term -> string
1.74 + val terms2str': term list -> string
1.75 + val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
1.76 + thydata ptyp list
1.77 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.78 val terms2strs: term list -> string list
1.79 - val terms2str': term list -> string
1.80 - val term_to_string'': thyID -> term -> string
1.81 val string_of_thm': theory -> thm -> string
1.82 val string_of_thm: thm -> string
1.83 val knowthys: unit -> theory list
1.84 - val thm2str: thm -> string
1.85 val e_pbt: pbt
1.86 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.87 - end
1.88 +
1.89 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.90 +val overwritelthy: theory -> (rls' * (string * rls)) list * (rls' * rls) list ->
1.91 + (rls' * (string * rls)) list end
1.92 +
1.93
1.94 (**)
1.95 structure Celem(**): CALC_ELEMENT(**) =
1.96 struct
1.97 (**)
1.98
1.99 -val linefeed = (curry op^) "\n";
1.100 +val linefeed = (curry op^) "\n"; (* ?\<longrightarrow> libraryC ?*)
1.101 type authors = string list;
1.102
1.103 type cterm' = string;
1.104 -val empty_cterm' = "empty_cterm'";
1.105 +type iterID = int;
1.106 +type calcID = int;
1.107
1.108 (* TODO CLEANUP Thm:
1.109 type rule =
1.110 @@ -226,16 +234,17 @@
1.111 revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
1.112 activate : thmID_of_derivation_name'
1.113 *)
1.114 -type iterID = int;
1.115 -type calcID = int;
1.116 -
1.117 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
1.118 type thmDeriv = string; (* WN120524 deprecated
1.119 thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name
1.120 WN120524: dont use Thm.derivation_name, this is destroyed by num_str;
1.121 Thm.get_name_hint survives num_str and seems perfectly reliable *)
1.122
1.123 -type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
1.124 +type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
1.125 +val thm'2xml : int -> Celem.thm' -> Celem.xml
1.126 +val assoc_thm': theory -> Celem.thm' -> thm
1.127 +| Calculate' of Celem.theory' * string * term * (term * Celem.thm')
1.128 +*)
1.129 (* tricky combination of (string, term) for theorems in Isac:
1.130 * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
1.131 by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
1.132 @@ -256,12 +265,8 @@
1.133 (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
1.134 TODO: introduce to pbl, met.*)
1.135 type guh = string;
1.136 -val e_guh = "e_guh":guh;
1.137
1.138 type xml = string; (* rm together with old code replaced by XML.tree *)
1.139 -fun string_to_bool "true" = true
1.140 - | string_to_bool "false" = false
1.141 - | string_to_bool str = error ("string_to_bool: arg = " ^ str)
1.142
1.143 (* eval function calling sml code during rewriting.
1.144 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
1.145 @@ -270,28 +275,24 @@
1.146 would be better
1.147 Calc: prog_calcID * (calID * eval_fn)) -> rule*)
1.148 type eval_fn = (string -> term -> theory -> (string * term) option);
1.149 -fun e_evalfn (_:'a) (_:term) (_:theory) = NONE:(string * term) option;
1.150 -(*. op in isa-term 'Const(op,_)' .*)
1.151 +fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
1.152 +(* op in isa-term "Const(op,_)" *)
1.153 type calID = string;
1.154 -
1.155 -(* *)
1.156 -type cal = (calID * eval_fn);
1.157 -(*. fun calculate_ fetches the evaluation-function via this list. *)
1.158 +type cal = calID * eval_fn;
1.159 type prog_calcID = string;
1.160 type calc = (prog_calcID * cal);
1.161 -type calc_elem =
1.162 +type calc_elem = (* fun calculate_ fetches the evaluation-function via this list *)
1.163 prog_calcID * (* a simple identifier used in programs *)
1.164 (calID * (* a long identifier used in Const *)
1.165 eval_fn) (* an ML function *)
1.166 -fun calc_eq ((pi1, (ci1, _)) : calc_elem, (pi2, (ci2, _)) : calc_elem) =
1.167 +fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
1.168 if pi1 = pi2
1.169 then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
1.170 else false
1.171
1.172 -
1.173 +(*WN180324 TODO clean types subst, *)
1.174 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
1.175 type subst = (term * term) list; (*here for ets2str*)
1.176 -val e_subst = []:(term * term) list;
1.177
1.178 (*TODO.WN060610 make use of "type rew_ord" total*)
1.179 type rew_ord' = string;
1.180 @@ -425,6 +426,20 @@
1.181 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
1.182 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.183 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
1.184 +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Erls" *)
1.185 + | id_rls (Rls {id, ...}) = id
1.186 + | id_rls (Seq {id, ...}) = id
1.187 + | id_rls (Rrls {id, ...}) = id;
1.188 +val rls2str = id_rls;
1.189 +fun id_rule (Thm (id, _)) = id
1.190 + | id_rule (Calc (id, _)) = id
1.191 + | id_rule (Cal1 (id, _)) = id
1.192 + | id_rule (Rls_ rls) = id_rls rls
1.193 + | id_rule Erule = "Erule";
1.194 +fun eq_rule (Thm (thm1, _), Thm (thm2, _)) = thm1 = thm2
1.195 + | eq_rule (Calc (id1, _), Calc (id2, _)) = id1 = id2
1.196 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
1.197 + | eq_rule _ = false;
1.198
1.199 (*ad thm':
1.200 there are two kinds of theorems ...
1.201 @@ -435,186 +450,25 @@
1.202 and have a special assoc_thm / assoc_rls in this interface *)
1.203 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
1.204 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
1.205 -type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.206 +type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
1.207 +val e_domID = "e_domID" : domID;
1.208
1.209 (* Since Isabelle2017 sessions in theory identifiers are enforced.
1.210 However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
1.211 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
1.212 -
1.213 -fun thm2str thm =
1.214 - let
1.215 - val t = Thm.prop_of thm
1.216 - val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
1.217 - val ctxt' = Config.put show_markup false ctxt
1.218 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.219 -
1.220 -fun term_to_string' ctxt t =
1.221 - let
1.222 - val ctxt' = Config.put show_markup false ctxt
1.223 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.224 -fun term_to_string'' (thyID : thyID) t =
1.225 - let
1.226 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
1.227 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.228 -fun term_to_string''' thy t =
1.229 - let
1.230 - val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.231 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.232 -
1.233 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
1.234 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
1.235 -
1.236 -fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
1.237 -fun t2str thy t = term_to_string' (thy2ctxt thy) t;
1.238 -fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
1.239 -fun terms2strs ts = map term2str ts;
1.240 -(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
1.241 -val terms2str = strs2str o terms2strs;
1.242 -(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
1.243 -val terms2str' = strs2str' o terms2strs;
1.244 -(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
1.245 -
1.246 -
1.247 -fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
1.248 - | termopt2str NONE = "NONE";
1.249 -
1.250 -fun type_to_string' ctxt t =
1.251 - let
1.252 - val ctxt' = Config.put show_markup false ctxt
1.253 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.254 -fun type_to_string'' (thyID : thyID) t =
1.255 - let
1.256 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
1.257 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.258 -fun type_to_string''' thy t =
1.259 - let
1.260 - val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.261 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.262 -
1.263 -fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
1.264 -val string_of_typ = type2str; (*legacy*)
1.265 -fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
1.266 -
1.267 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
1.268 -
1.269 -val e_rule = Thm ("refl", @{thm refl});
1.270 -fun id_of_thm (Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
1.271 - | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
1.272 -fun thm_of_thm (Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
1.273 - | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
1.274 -fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm) (* TODO re-arrange code for rule2str *)
1.275 - | rep_thm_G' _ = raise ERROR ("rep_thm_G': uncovered case " (* ^ rule2str r *))
1.276 -
1.277 -fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
1.278 -fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
1.279 -fun thyID_of_derivation_name dn = hd (space_explode "." dn);
1.280 -fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
1.281 -
1.282 -fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
1.283 - (strip_thy thmid1) = (strip_thy thmid2);
1.284 -(*WN120201 weakened*)
1.285 -fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _)) = thmid1 = thmid2;
1.286 -(*version typed weaker WN100910*)
1.287 -fun eq_thmI' ((thmid1, _), (thmid2, _)) =
1.288 - (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
1.289 -
1.290 -
1.291 -(*check for [.] as caused by "fun assoc_thm'"*)
1.292 -fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (Thm.prop_of thm)
1.293 -fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
1.294 -fun string_of_thmI thm =
1.295 - let
1.296 - val str = (de_quote o string_of_thm) thm
1.297 - val (a, b) = split_nlast (5, Symbol.explode str)
1.298 - in
1.299 - case b of
1.300 - [" ", " ","[", ".", "]"] => implode a
1.301 - | _ => str
1.302 - end
1.303 -
1.304 -(*.id requested for all, Rls,Seq,Rrls.*)
1.305 -fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
1.306 - | id_rls (Rls {id,...}) = id
1.307 - | id_rls (Seq {id,...}) = id
1.308 - | id_rls (Rrls {id,...}) = id;
1.309 -val rls2str = id_rls;
1.310 -fun id_rule (Thm (id, _)) = id
1.311 - | id_rule (Calc (id, _)) = id
1.312 - | id_rule (Rls_ rls) = id_rls rls;
1.313 -
1.314 -fun get_rules (Rls {rules,...}) = rules
1.315 - | get_rules (Seq {rules,...}) = rules
1.316 - | get_rules (Rrls _) = [];
1.317 -
1.318 -fun rule2str Erule = "Erule"
1.319 - | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
1.320 - | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.321 - | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.322 - | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.323 -fun rule2str' Erule = "Erule"
1.324 - | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
1.325 - | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.326 - | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.327 - | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.328 -
1.329 -(*WN080102 compare eq_rule ?!?*)
1.330 -fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
1.331 - | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.332 - | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
1.333 - | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
1.334 - | eqrule _ = false;
1.335 -
1.336 -type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
1.337 - (term * term * rule list list * (rule * (term * term list)) list);
1.338 -
1.339 -val e_type = Type("empty",[]);
1.340 -val a_type = TFree("'a",[]);
1.341 -val e_term = Const("empty",e_type);
1.342 -val a_term = Free("empty",a_type);
1.343 -val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
1.344 -
1.345 -val e_term = Const("empty", Type("'a", []));
1.346 -val e_scr = Prog e_term;
1.347
1.348 fun string_of_thy thy = Context.theory_name thy: theory';
1.349 val theory2domID = string_of_thy;
1.350 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
1.351 val theory2theory' = string_of_thy;
1.352 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
1.353 -val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
1.354 -(* fun theory'2theory = fun thyID2thy ... see fun assoc_thy (...Thy_Info_get_theory string);
1.355 -al it = "Isac" : string
1.356 -*)
1.357
1.358 fun thyID2theory' (thyID:thyID) = thyID;
1.359 -(*
1.360 - let val ss = Symbol.explode thyID
1.361 - val ext = implode (takelast (4, ss))
1.362 - in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
1.363 - else thyID ^ ".thy"
1.364 - end;
1.365 -*)
1.366 -(* thyID2theory' "Isac" (*ok*);
1.367 -val it = "Isac" : theory'
1.368 - > thyID2theory' "Isac" (*abuse, goes ok...*);
1.369 -val it = "Isac" : theory'
1.370 -*)
1.371 -
1.372 fun theory'2thyID (theory':theory') = theory';
1.373 -(*
1.374 - let val ss = Symbol.explode theory'
1.375 - val ext = implode (takelast (4, ss))
1.376 - in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
1.377 - else theory' (*disarm abuse of theory'*)
1.378 - end;
1.379 -*)
1.380 -(* theory'2thyID "Isac";
1.381 -val it = "Isac" : thyID
1.382 -> theory'2thyID "Isac";
1.383 -val it = "Isac" : thyID*)
1.384 -
1.385 -
1.386 -(*. WN0509 discussion:
1.387 +(* WN0509 discussion:
1.388 #############################################################################
1.389 # How to manage theorys in subproblems wrt. the requirement, #
1.390 # that scripts should be re-usable ? #
1.391 @@ -635,50 +489,121 @@
1.392
1.393 Other solutions possible:
1.394 # always parse and type-check with Thy_Info_get_theory "Isac"
1.395 - (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.396 + (rejected due to the vague idea eg. to re-use equations for R in C etc.)
1.397 # regard the subthy-relation in specifying thys of subpbls
1.398 # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.399 # ???
1.400 -.*)
1.401 -(*WN0509 TODO "ProtoPure" ... would be more consistent
1.402 - with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
1.403 -val e_domID = "e_domID":domID;
1.404 +*)
1.405 +
1.406 +
1.407 +
1.408 +
1.409 +
1.410 +fun thm2str thm =
1.411 + let
1.412 + val t = Thm.prop_of thm
1.413 + val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
1.414 + val ctxt' = Config.put show_markup false ctxt
1.415 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.416 +fun term_to_string' ctxt t =
1.417 + let
1.418 + val ctxt' = Config.put show_markup false ctxt
1.419 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.420 +fun term_to_string'' thyID t =
1.421 + let
1.422 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
1.423 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.424 +fun term_to_string''' thy t =
1.425 + let
1.426 + val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.427 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.428 +
1.429 +fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
1.430 +fun t2str thy t = term_to_string' (thy2ctxt thy) t;
1.431 +fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
1.432 +fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
1.433 +val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
1.434 +val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *)
1.435 +fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
1.436 + | termopt2str NONE = "NONE";
1.437 +
1.438 +fun type_to_string'' (thyID : thyID) t =
1.439 + let
1.440 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
1.441 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.442 +fun type2str typ = type_to_string'' "Isac" typ; (*TODO legacy*)
1.443 +val string_of_typ = type2str; (*legacy*)
1.444 +fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
1.445 +
1.446 +val e_rule = Thm ("refl", @{thm refl});
1.447 +fun id_of_thm (Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
1.448 + | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
1.449 +fun thm_of_thm (Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
1.450 + | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
1.451 +
1.452 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
1.453 +fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
1.454 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
1.455 +fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
1.456 +
1.457 +(*check for [.] as caused by "fun assoc_thm'"*)
1.458 +fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (Thm.prop_of thm)
1.459 +fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
1.460 +fun string_of_thmI thm =
1.461 + let
1.462 + val str = (de_quote o string_of_thm) thm
1.463 + val (a, b) = split_nlast (5, Symbol.explode str)
1.464 + in
1.465 + case b of
1.466 + [" ", " ","[", ".", "]"] => implode a
1.467 + | _ => str
1.468 + end
1.469 +
1.470 +fun get_rules Erls = []
1.471 + | get_rules (Rls {rules, ...}) = rules
1.472 + | get_rules (Seq {rules, ...}) = rules
1.473 + | get_rules (Rrls _) = [];
1.474 +fun rule2str Erule = "Erule"
1.475 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
1.476 + | rule2str (Calc (str, _)) = "Calc (\""^str^"\",fn)"
1.477 + | rule2str (Cal1 (str, _)) = "Cal1 (\""^str^"\",fn)"
1.478 + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.479 +fun rule2str' Erule = "Erule"
1.480 + | rule2str' (Thm (str, _)) = "Thm (\""^str^"\",\"\")"
1.481 + | rule2str' (Calc (str, _)) = "Calc (\""^str^"\",fn)"
1.482 + | rule2str' (Cal1 (str, _)) = "Cal1 (\""^str^"\",fn)"
1.483 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.484 +
1.485 +type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
1.486 + (term * term * rule list list * (rule * (term * term list)) list);
1.487 +
1.488 +val e_type = Type ("empty",[]);
1.489 +val e_term = Const ("empty", e_type);
1.490 +val e_rrlsstate = (e_term,e_term, [[e_rule]], [(e_rule, (e_term, []))]);
1.491 +val e_term = Const ("empty", Type("'a", []));
1.492
1.493 (*the key into the hierarchy ob theory elements*)
1.494 type theID = string list;
1.495 -val e_theID = ["e_theID"];
1.496 -val theID2str = strs2str;
1.497 -(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
1.498 -fun theID2thyID (theID:theID) =
1.499 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
1.500 - else error ("theID2thyID called with "^ theID2str theID);
1.501 +val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
1.502 +fun theID2thyID theID =
1.503 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
1.504 + else error ("theID2thyID called with " ^ theID2str theID);
1.505
1.506 (*the key into the hierarchy ob problems*)
1.507 -type pblID = string list; (* domID::...*)
1.508 -val e_pblID = ["e_pblID"]:pblID;
1.509 -val pblID2str = strs2str;
1.510 +type pblID = string list; (* domID :: ...*)
1.511 +val e_pblID = ["e_pblID"];
1.512
1.513 (*the key into the hierarchy ob methods*)
1.514 type metID = string list;
1.515 -val e_metID = ["e_metID"]:metID;
1.516 +type spec = domID * pblID * metID;
1.517 +fun spec2str (dom, pbl, met) =
1.518 + "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
1.519 +val e_metID = ["e_metID"];
1.520 val metID2str = strs2str;
1.521 -
1.522 -type spec =
1.523 - domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
1.524 - specify (Init_Proof..), nxt_specify_init_calc,
1.525 - assod (.SubProblem...), stac2tac (.SubProblem...)*)
1.526 - pblID *
1.527 - metID;
1.528 -
1.529 -fun spec2str ((dom,pbl,met)(*:spec*)) =
1.530 - "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^
1.531 - ", " ^ (strs2str met) ^ ")";
1.532 -(*> spec2str empty_spec;
1.533 -val it = "(\"\", [], (\"\", \"\"))" : string *)
1.534 -val empty_spec = (e_domID,e_pblID,e_metID):spec;
1.535 +val empty_spec = (e_domID, e_pblID, e_metID);
1.536 val e_spec = empty_spec;
1.537
1.538 -(*.association list with cas-commands, for generating a complete calc-head.*)
1.539 +(* association list with cas-commands, for generating a complete calc-head *)
1.540 type generate_fn =
1.541 (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
1.542 (term * (* description of an element *)
1.543 @@ -692,10 +617,8 @@
1.544
1.545 (*either theID or pblID or metID*)
1.546 type kestoreID = string list;
1.547 -val e_kestoreID = ["e_kestoreID"];
1.548 -val kestoreID2str = strs2str;
1.549
1.550 -(*for distinction of contexts WN130621: disambiguate with Isabelle's Context !*)
1.551 +(* for distinction of contexts WN130621: disambiguate with Isabelle's Context *)
1.552 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
1.553 fun ketype2str Exp_ = "Exp_"
1.554 | ketype2str Thy_ = "Thy_"
1.555 @@ -705,11 +628,6 @@
1.556 | ketype2str' Thy_ = "Theory"
1.557 | ketype2str' Pbl_ = "Problem"
1.558 | ketype2str' Met_ = "Method";
1.559 -fun str2ketype "Exp_" = Exp_
1.560 - | str2ketype "Thy_" = Thy_
1.561 - | str2ketype "Pbl_" = Pbl_
1.562 - | str2ketype "Met_" = Met_
1.563 - | str2ketype str = raise ERROR ("str2ketype: WRONG arg = " ^ str)
1.564 (* for conversion from XML *)
1.565 fun str2ketype' "exp" = Exp_
1.566 | str2ketype' "thy" = Thy_
1.567 @@ -717,9 +635,8 @@
1.568 | str2ketype' "met" = Met_
1.569 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
1.570
1.571 -(*rewrite orders, also stored in 'type met' and type 'and rls'
1.572 - The association list is required for 'rewrite.."rew_ord"..'
1.573 - WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
1.574 +(* rewrite orders, also stored in 'type met' and type 'and rls'
1.575 + The association list is required for 'rewrite.."rew_ord"..' *)
1.576 val rew_ord' = Unsynchronized.ref
1.577 ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
1.578 : (rew_ord' * (* the key for the association list *)
1.579 @@ -728,51 +645,31 @@
1.580 -> bool)) (* if t1 <= t2 then true else false *)
1.581 list); (* association list *)
1.582
1.583 -(* NOT ACCEPTED BY struct
1.584 -rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
1.585 - ("dummy_ord", dummy_ord)]);
1.586 -*)
1.587 -
1.588 (* A tree for storing data defined in different theories
1.589 for access from the Interpreter and from dialogue authoring
1.590 using a string list as key.
1.591 - 'a is for pbt | met | thydata; after WN030424 naming became inappropriate *)
1.592 + 'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)
1.593 datatype 'a ptyp =
1.594 - Ptyp of string * (* element of the key *)
1.595 - 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
1.596 - presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
1.597 - ('a ptyp) list;(* the children nodes *)
1.598 + Ptyp of string * (* element of the key *)
1.599 + 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
1.600 + presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
1.601 + ('a ptyp) list; (* the children nodes *)
1.602
1.603 -(*.datatype for collecting thydata for hierarchy.*)
1.604 +(* datatype for collecting thydata for hierarchy *)
1.605 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
1.606 -(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
1.607 -datatype thydata = Html of {guh: guh,
1.608 - coursedesign: authors,
1.609 - mathauthors: authors,
1.610 - html: string} (*html; for demos before database*)
1.611 - | Hthm of {guh: guh,
1.612 - coursedesign: authors,
1.613 - mathauthors: authors,
1.614 - fillpats: fillpat list,
1.615 - thm: thm} (* here no sym_thm, thus no thmID required *)
1.616 - | Hrls of {guh: guh,
1.617 - coursedesign: authors,
1.618 - mathauthors: authors,
1.619 - thy_rls: (thyID * rls)}
1.620 - | Hcal of {guh: guh,
1.621 - coursedesign: authors,
1.622 - mathauthors: authors,
1.623 - calc: calc}
1.624 - | Hord of {guh: guh,
1.625 - coursedesign: authors,
1.626 - mathauthors: authors,
1.627 - ord: (subst -> (term * term) -> bool)};
1.628 -val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
1.629 -fun the2str (Html {guh, coursedesign, mathauthors, html}) = guh : string
1.630 - | the2str (Hthm {guh, coursedesign, mathauthors, fillpats, thm}) = guh
1.631 - | the2str (Hrls {guh, coursedesign, mathauthors, thy_rls}) = guh
1.632 - | the2str (Hcal {guh, coursedesign, mathauthors, calc}) = guh
1.633 - | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh
1.634 +datatype thydata =
1.635 + Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
1.636 +| Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,
1.637 + thm: thm} (* here no sym_thm, thus no thmID required *)
1.638 +| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (thyID * rls)}
1.639 +| Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: calc}
1.640 +| Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
1.641 + ord: (subst -> (term * term) -> bool)};
1.642 +fun the2str (Html {guh, ...}) = guh
1.643 + | the2str (Hthm {guh, ...}) = guh
1.644 + | the2str (Hrls {guh, ...}) = guh
1.645 + | the2str (Hcal {guh, ...}) = guh
1.646 + | the2str (Hord {guh, ...}) = guh
1.647 fun thes2str thes = map the2str thes |> list2str;
1.648
1.649 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
1.650 @@ -788,55 +685,61 @@
1.651 TODO (d1) lookup from from rule set in MiniBrowser *)
1.652 type thehier = (thydata ptyp) list;
1.653 (* required to determine sequence of main nodes of thehier in KEStore.thy *)
1.654 -fun part2guh ([str]:theID) =
1.655 - (case str of
1.656 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
1.657 +fun part2guh [str] = (case str of
1.658 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
1.659 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
1.660 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
1.661 - | str => error ("thy2guh: called with '"^str^"'"))
1.662 - | part2guh theID = error ("part2guh called with theID = " ^ theID2str theID);
1.663 + | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
1.664 + | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
1.665
1.666 -fun thy2guh ([part, thyID] : theID) = (case part of
1.667 - "Isabelle" => "thy_isab_" ^ thyID : guh
1.668 +fun thy2guh [part, thyID] = (case part of
1.669 + "Isabelle" => "thy_isab_" ^ thyID
1.670 | "IsacScripts" => "thy_scri_" ^ thyID
1.671 | "IsacKnowledge" => "thy_isac_" ^ thyID
1.672 - | str => error ("thy2guh: called with '" ^ str ^ "'"))
1.673 - | thy2guh theID = error ("thy2guh called with '" ^ strs2str' theID ^ "'");
1.674 + | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
1.675 + | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
1.676
1.677 -fun thypart2guh ([part, thyID, thypart] : theID) = case part of
1.678 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
1.679 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
1.680 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
1.681 - | str => error ("thypart2guh: called with '" ^ str ^ "'");
1.682 +fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
1.683 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
1.684 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
1.685 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
1.686 + | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
1.687 + | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
1.688 +
1.689
1.690 -(* convert the data got via contextToThy to a globally unique handle
1.691 - there is another way to get the guh out of the 'theID' in the hierarchy *)
1.692 -fun thm2guh (isa, thyID:thyID) (thmID:thmID) = case isa of
1.693 +(* convert the data got via contextToThy to a globally unique handle.
1.694 + there is another way to get the guh: get out of the 'theID' in the hierarchy *)
1.695 +fun thm2guh (isa, thyID) thmID = case isa of
1.696 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
1.697 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.698 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.699 - | str => error ("thm2guh called with isa = '" ^ isa ^ "' for thm = " ^ thmID ^ "'");
1.700 + | _ => raise ERROR
1.701 + ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
1.702
1.703 -fun rls2guh (isa, thyID:thyID) (rls':rls') = case isa of
1.704 +fun rls2guh (isa, thyID) rls' = case isa of
1.705 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
1.706 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.707 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.708 - | str => error ("rls2guh called with isa = '" ^ isa ^ "' for rls = '" ^ rls' ^ "'");
1.709 + | _ => raise ERROR
1.710 + ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
1.711
1.712 -fun cal2guh (isa, thyID:thyID) calID = case isa of
1.713 +fun cal2guh (isa, thyID) calID = case isa of
1.714 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
1.715 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.716 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.717 - | str => error ("cal2guh called with isa = '" ^ isa ^ "' for cal = '" ^ calID ^ "'");
1.718 + | _ => raise ERROR
1.719 + ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
1.720
1.721 -fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') = case isa of
1.722 +fun ord2guh (isa, thyID) rew_ord' = case isa of
1.723 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
1.724 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.725 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.726 - | str => error ("ord2guh called with isa = '" ^ isa ^ "' for ord = '" ^ rew_ord' ^ "'");
1.727 + | _ => raise ERROR
1.728 + ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
1.729
1.730 (* not only for thydata, but also for thy's etc *)
1.731 -fun theID2guh (theID : theID) = case length theID of
1.732 +(* TODO
1.733 +fun theID2guh theID = case length theID of
1.734 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
1.735 | 1 => part2guh theID
1.736 | 2 => thy2guh theID
1.737 @@ -849,25 +752,36 @@
1.738 | "Calculations" => cal2guh (isa, thyID) elemID
1.739 | "Orders" => ord2guh (isa, thyID) elemID
1.740 | "Theorems" => thy2guh [isa, thyID]
1.741 - | str => error ("theID2guh: called with theID = " ^ strs2str' theID)
1.742 + | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
1.743 end
1.744 - | n => error ("theID2guh called with theID = " ^ strs2str' theID);
1.745 + | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
1.746 +*)
1.747 +(* not only for thydata, but also for thy's etc *)
1.748 +fun theID2guh [] = raise ERROR ("theID2guh: called with []")
1.749 + | theID2guh [str] = part2guh [str]
1.750 + | theID2guh [s1, s2] = thy2guh [s1, s2]
1.751 + | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
1.752 + | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
1.753 + "Theorems" => thm2guh (isa, thyID) elemID
1.754 + | "Rulesets" => rls2guh (isa, thyID) elemID
1.755 + | "Calculations" => cal2guh (isa, thyID) elemID
1.756 + | "Orders" => ord2guh (isa, thyID) elemID
1.757 + | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
1.758 + | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
1.759
1.760 type path = string;
1.761 type filename = string;
1.762
1.763 -(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
1.764 local
1.765 - fun ii (_:term) = e_rrlsstate;
1.766 - fun no (_:term) = SOME (e_term,[e_term]);
1.767 - fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
1.768 - fun ne (_:rule list list) (_:term) = SOME e_rule;
1.769 - fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
1.770 + fun ii (_: term) = e_rrlsstate;
1.771 + fun no (_: term) = SOME (e_term, [e_term]);
1.772 + fun lo (_: rule list list) (_: term) (_: rule) = [(e_rule, (e_term, [e_term]))];
1.773 + fun ne (_: rule list list) (_: term) = SOME e_rule;
1.774 + fun fo (_: rule list list) (_: term) (_: term) = [(e_rule, (e_term, [e_term]))];
1.775 in
1.776 -val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
1.777 - next_rule=ne,attach_form=fo};
1.778 +val e_rfuns = Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
1.779 + next_rule = ne, attach_form = fo};
1.780 end;
1.781 -
1.782 val e_rls =
1.783 Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
1.784 srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls;
1.785 @@ -875,54 +789,33 @@
1.786 Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
1.787 calc = [], errpatts = [], scr=e_rfuns}:rls;
1.788
1.789 -fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
1.790 - {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.791 - (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.792 - | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
1.793 - {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.794 - (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.795 - | rep_rls Erls = rep_rls e_rls
1.796 - | rep_rls (Rrls {id,...}) = rep_rls e_rls
1.797 - (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.798 -(*| rep_rls (Seq {id,...}) =
1.799 - error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.800 ---1.7.03*)
1.801 -fun rep_rrls (Rrls {id, calc, erls, prepat, rew_ord, errpatts,
1.802 - scr = Rfuns {attach_form, init_state, locate_rule, next_rule, normal_form}}) =
1.803 - {id=id, calc=calc, erls=erls, prepat=prepat,
1.804 - rew_ord=rew_ord, errpatts=errpatts, attach_form=attach_form, init_state=init_state,
1.805 - locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.806 - | rep_rrls (Rls {id,...}) =
1.807 - error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.808 - | rep_rrls (Seq {id,...}) =
1.809 - error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.810 +fun rep_rls Erls = rep_rls e_rls
1.811 + | rep_rls (Rls {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
1.812 + {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
1.813 + calc = calc, rules = rules, scr = scr}
1.814 + | rep_rls (Seq {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
1.815 + {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
1.816 + calc = calc, rules = rules, scr = scr}
1.817 + | rep_rls (Rrls _) = rep_rls e_rls
1.818
1.819 -fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.820 - rules =rs, errpatts=errpatts, scr=sc}) r =
1.821 - (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.822 - rules = rs @ r, errpatts=errpatts, scr=sc}:rls)
1.823 - | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.824 - rules =rs, errpatts=errpatts, scr=sc}) r =
1.825 - (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.826 - rules = rs @ r, errpatts=errpatts, scr=sc}:rls)
1.827 - | append_rls id (Rrls _) _ =
1.828 - error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.829 +fun append_rls id Erls _ = raise ERROR ("append_rls: with \"" ^ id ^ "\" not for Erls")
1.830 + | append_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.831 + rules = rs, errpatts = errpatts, scr = sc}) r =
1.832 + Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.833 + rules = rs @ r, errpatts = errpatts, scr = sc}
1.834 + | append_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.835 + rules = rs, errpatts = errpatts, scr = sc}) r =
1.836 + Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.837 + rules = rs @ r, errpatts = errpatts, scr = sc}
1.838 + | append_rls id (Rrls _) _ = raise ERROR ("append_rls: not for reverse-rewrite-rule-set " ^ id);
1.839
1.840 -(*. are _atomic_ rules equal ?.*)
1.841 -(*WN080102 compare eqrule ?!?*)
1.842 -fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
1.843 - | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.844 - | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
1.845 - (*id_rls checks for Rls, Seq, Rrls*)
1.846 - | eq_rule _ = false;
1.847
1.848 fun merge_ids rls1 rls2 =
1.849 let
1.850 val id1 = (#id o rep_rls) rls1
1.851 val id2 = (#id o rep_rls) rls2
1.852 in
1.853 - if id1 = id2 then id1
1.854 - else "merged_" ^ id1 ^ "_" ^ id2
1.855 + if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
1.856 end
1.857 fun merge_rls _ Erls rls = rls
1.858 | merge_rls _ rls Erls = rls
1.859 @@ -934,43 +827,44 @@
1.860 (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
1.861 rules = rs2, errpatts = eps2, ...})
1.862 =
1.863 - (Rls {id = id, rew_ord = ro1, scr = sc1,
1.864 + Rls {id = id, rew_ord = ro1, scr = sc1,
1.865 preconds = union (op =) pc1 pc2,
1.866 erls = merge_rls (merge_ids er1 er2) er1 er2,
1.867 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
1.868 calc = union calc_eq ca1 ca2,
1.869 rules = union eq_rule rs1 rs2,
1.870 - errpatts = union (op =) eps1 eps2} : rls)
1.871 + errpatts = union (op =) eps1 eps2}
1.872 | merge_rls id
1.873 (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
1.874 rules = rs1, errpatts = eps1, scr = sc1, ...})
1.875 (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
1.876 rules = rs2, errpatts = eps2, ...})
1.877 =
1.878 - (Seq {id = id, rew_ord = ro1, scr = sc1,
1.879 + Seq {id = id, rew_ord = ro1, scr = sc1,
1.880 preconds = union (op =) pc1 pc2,
1.881 erls = merge_rls (merge_ids er1 er2) er1 er2,
1.882 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
1.883 calc = union calc_eq ca1 ca2,
1.884 rules = union eq_rule rs1 rs2,
1.885 - errpatts = union (op =) eps1 eps2} : rls)
1.886 + errpatts = union (op =) eps1 eps2}
1.887 | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^
1.888 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");
1.889
1.890 -fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.891 - rules=rs, errpatts=eps, scr=sc}) r =
1.892 - (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.893 - rules = gen_rems eq_rule (rs, r),
1.894 - errpatts = eps(*gen_rems op= (eps, TODO)*),
1.895 - scr=sc}:rls)
1.896 - | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.897 - rules =rs, errpatts=eps, scr=sc}) r =
1.898 - (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.899 - rules = gen_rems eq_rule (rs, r),
1.900 - errpatts = eps(*gen_rems op= (eps, TODO)*),
1.901 - scr=sc}:rls)
1.902 - | remove_rls id (Rrls _) _ = error
1.903 - ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.904 +(* used only for one hack TODO remove *)
1.905 +fun remove_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.906 + rules = rs, errpatts = eps, scr = sc}) r =
1.907 + Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.908 + rules = gen_rems eq_rule (rs, r),
1.909 + errpatts = eps,
1.910 + scr = sc}
1.911 + | remove_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.912 + rules = rs, errpatts = eps, scr = sc}) r =
1.913 + Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.914 + rules = gen_rems eq_rule (rs, r),
1.915 + errpatts = eps,
1.916 + scr = sc}
1.917 + | remove_rls id (Rrls _) _ = raise ERROR ("remove_rls: not for reverse-rewrite-rule-set "^id)
1.918 + | remove_rls _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
1.919
1.920 (* datastructure for KEStore_Elems, intermediate for thehier *)
1.921 type rlss_elem =
1.922 @@ -980,98 +874,80 @@
1.923 fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2
1.924
1.925 fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys =
1.926 - case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of
1.927 - NONE => re :: ys
1.928 - | SOME (i, (_, (_, r2))) =>
1.929 + case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of
1.930 + NONE => re :: ys
1.931 + | SOME (i, (_, (_, r2))) =>
1.932 let
1.933 val r12 = merge_rls id r1 r2
1.934 in list_update ys i (id, (thyID, r12)) end
1.935 -
1.936 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;
1.937
1.938 +fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
1.939 + | assoc' ((keyi, xi) :: pairs, key) =
1.940 + if key = keyi then SOME xi else assoc' (pairs, key);
1.941
1.942 -fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.943 - | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.944 - | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
1.945 +fun assoc_thy thy =
1.946 + if thy = "e_domID"
1.947 + then (Thy_Info_get_theory "Script") (*lower bound of Knowledge*)
1.948 + else (Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
1.949
1.950 -fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
1.951 - | assoc' ((keyi, xi) :: pairs, key) =
1.952 - if key = keyi then SOME xi else assoc' (pairs, key);
1.953 -
1.954 -fun assoc_thy (thy:theory') =
1.955 - if thy = "e_domID" then (Thy_Info_get_theory "Script") (*lower bound of Knowledge*)
1.956 - else (Thy_Info_get_theory thy)
1.957 - handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.958 -
1.959 -(*.overwrite an element in an association list and pair it with a thyID
1.960 +(* overwrite an element in an association list and pair it with a thyID
1.961 in order to create the thy_hierarchy;
1.962 overwrites existing rls' even if they are defined in a different thy;
1.963 - this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
1.964 -(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.965 + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc *)
1.966 +(* WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.967 they do NOT handle overlays by re-using an identifier in different thys;
1.968 "thyID.rlsID" would be a good solution, if the "." would be possible
1.969 in scripts...
1.970 - actually a hack to get alltogether run again with minimal effort*)
1.971 + actually a hack to get alltogether run again with minimal effort *)
1.972 fun insthy thy' (rls', rls) = (rls', (thy', rls));
1.973 fun overwritelthy thy (al, bl:(rls' * rls) list) =
1.974 let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
1.975 in overwritel (al, bl') end;
1.976
1.977 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
1.978 - handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.979 -(*get the string for stac from rule*)
1.980 + handle _ => error ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
1.981
1.982 -fun subst2str (s:subst) =
1.983 +fun subst2str s =
1.984 (strs2str o
1.985 - (map (linefeed o pair2str o
1.986 - (apsnd term2str) o
1.987 - (apfst term2str)))) s;
1.988 + (map (
1.989 + linefeed o pair2str o (apsnd term2str) o (apfst term2str)))) s;
1.990 fun subst2str' (s:subst) =
1.991 (strs2str' o
1.992 - (map (pair2str o
1.993 - (apsnd term2str) o
1.994 - (apfst term2str)))) s;
1.995 -(*> subst2str' [(str2term "bdv", str2term "x"),
1.996 - (str2term "bdv_2", str2term "y")];
1.997 -val it = "[(bdv, x)]" : string
1.998 -*)
1.999 + (map (
1.1000 + pair2str o (apsnd term2str) o (apfst term2str)))) s;
1.1001 val env2str = subst2str;
1.1002
1.1003 -
1.1004 -(*recursive defs:*)
1.1005 -fun scr2str (Prog s) = "Prog " ^ term2str s
1.1006 +fun scr2str EmptyScr = "EmptyScr"
1.1007 + | scr2str (Prog s) = "Prog " ^ term2str s
1.1008 | scr2str (Rfuns _) = "Rfuns";
1.1009
1.1010 -
1.1011 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
1.1012
1.1013
1.1014 (* trace internal steps of isac's numeral calculations *)
1.1015 val trace_calc = Unsynchronized.ref false;
1.1016 -(*.trace internal steps of isac's rewriter*)
1.1017 +(* trace internal steps of isac's rewriter *)
1.1018 val trace_rewrite = Unsynchronized.ref false;
1.1019 -(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
1.1020 +(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *)
1.1021 val depth = Unsynchronized.ref 99999;
1.1022 -(*.no of rewrites exceeding this int -> NO rewrite.*)
1.1023 -(*WN060829 still unused...*)
1.1024 -val lim_rewrite = Unsynchronized.ref 99999;
1.1025 -(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
1.1026 +(* no of rewrites exceeding this int -> NO rewrite *)
1.1027 val lim_deriv = Unsynchronized.ref 100;
1.1028 -(*.switch for checking guhs unique before storing a pbl or met;
1.1029 +(* switch for checking guhs unique before storing a pbl or met;
1.1030 set true at startup (done at begin of ROOT.ML)
1.1031 - set false for editing IsacKnowledge (done at end of ROOT.ML).*)
1.1032 + set false for editing IsacKnowledge (done at end of ROOT.ML) *)
1.1033 val check_guhs_unique = Unsynchronized.ref true;
1.1034
1.1035
1.1036 -datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
1.1037 - L (*go left at $*)
1.1038 - | R (*go right at $*)
1.1039 - | D; (*go down at Abs*)
1.1040 +datatype lrd = (*elements of "type loc_" into an Isabelle term*)
1.1041 + L (*go left at $*)
1.1042 +| R (*go right at $*)
1.1043 +| D; (*go down at Abs*)
1.1044 type loc_ = lrd list;
1.1045 fun ldr2str L = "L"
1.1046 | ldr2str R = "R"
1.1047 | ldr2str D = "D";
1.1048 -fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
1.1049 +fun loc_2str k = (strs2str' o (map ldr2str)) k;
1.1050
1.1051
1.1052 (* the pattern for an item of a problems model or a methods guard *)
1.1053 @@ -1088,68 +964,68 @@
1.1054 (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
1.1055 (term * (* description *)
1.1056 term)); (* id | struct-var *)
1.1057 -val e_pbt_ = ("#Undef", (e_term, e_term)) : pbt_
1.1058 type pbt =
1.1059 - {guh : guh, (* unique within this isac-knowledge *)
1.1060 - mathauthors : string list, (* copyright *)
1.1061 - init : pblID, (* to start refinement with *)
1.1062 + {guh : guh, (* unique within this isac-knowledge *)
1.1063 + mathauthors : string list, (* copyright *)
1.1064 + init : pblID, (* to start refinement with *)
1.1065 thy : theory, (* which allows to compile that pbt
1.1066 - TODO: search generalized for subthy (ref.p.69*)
1.1067 - (*^^^ WN050912 NOT used during application of the problem,
1.1068 - because applied terms may be from 'subthy' as well as from super;
1.1069 - thus we take 'maxthy'; see match_ags !*)
1.1070 - cas : term option, (* 'CAS-command'*)
1.1071 - prls : rls, (* for preds in where_*)
1.1072 - where_ : term list, (* where - predicates*)
1.1073 + TODO: search generalized for subthy (ref.p.69*)
1.1074 + (*^^^ WN050912 NOT used during application of the problem,
1.1075 + because applied terms may be from 'subthy' as well as from super;
1.1076 + thus we take 'maxthy'; see match_ags ! *)
1.1077 + cas : term option, (* 'CAS-command' *)
1.1078 + prls : rls, (* for preds in where_ *)
1.1079 + where_ : term list, (* where - predicates *)
1.1080 ppc : pat list, (* this is the model-pattern;
1.1081 - it contains "#Given","#Where","#Find","#Relate"-patterns
1.1082 - for constraints on identifiers see "fun cpy_nam" *)
1.1083 - met : metID list} (* methods solving the pbt*)
1.1084 + it contains "#Given","#Where","#Find","#Relate"-patterns
1.1085 + for constraints on identifiers see "fun cpy_nam" *)
1.1086 + met : metID list} (* methods solving the pbt *)
1.1087
1.1088 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
1.1089 - cas = NONE, prls = Erls, where_ = [], ppc = [], met = []} : pbt
1.1090 -fun pbt2str
1.1091 - ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
1.1092 - prls = prls', thy = thy', where_ = w'} : pbt) =
1.1093 - "{cas = " ^ (termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
1.1094 - ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
1.1095 - ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
1.1096 - ^ (rls2str prls' |> quote) ^ ", thy = {" ^ (theory2str thy') ^ "}, where_ = "
1.1097 - ^ (terms2str w') ^ "}" |> linefeed;
1.1098 + cas = NONE, prls = Erls, where_ = [], ppc = [], met = []}
1.1099 +fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
1.1100 + prls = prls', thy = thy', where_ = w'} : pbt)
1.1101 + = "{cas = " ^ (termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
1.1102 + ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
1.1103 + ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
1.1104 + ^ (rls2str prls' |> quote) ^ ", thy = {" ^ (theory2str thy') ^ "}, where_ = "
1.1105 + ^ (terms2str w') ^ "}" |> linefeed;
1.1106 fun pbts2str pbts = map pbt2str pbts |> list2str;
1.1107
1.1108 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[])
1.1109 type ptyps = (pbt ptyp) list
1.1110
1.1111 fun coll_pblguhs pbls =
1.1112 - let fun node coll (Ptyp (_,[n],ns)) =
1.1113 - [(#guh : pbt -> guh) n] @ (nodes coll ns)
1.1114 - and nodes coll [] = coll
1.1115 - | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.1116 - in nodes [] pbls end;
1.1117 -fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
1.1118 - if member op = (coll_pblguhs pbls) guh
1.1119 - then error ("check_guh_unique failed with '"^guh^"';\n"^
1.1120 - "use 'sort_pblguhs()' for a list of guhs;\n"^
1.1121 - "consider setting 'check_guhs_unique := false'")
1.1122 - else ();
1.1123 + let
1.1124 + fun node coll (Ptyp (_, [n], ns)) = [(#guh : pbt -> guh) n] @ (nodes coll ns)
1.1125 + | node _ _ = raise ERROR "coll_pblguhs - node"
1.1126 + and nodes coll [] = coll
1.1127 + | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
1.1128 + in nodes [] pbls end;
1.1129 +fun check_pblguh_unique guh pbls =
1.1130 + if member op = (coll_pblguhs pbls) guh
1.1131 + then error ("check_guh_unique failed with \""^ guh ^"\";\n"^
1.1132 + "use \"sort_pblguhs()\" for a list of guhs;\n"^
1.1133 + "consider setting \"check_guhs_unique := false\"")
1.1134 + else ();
1.1135
1.1136 fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
1.1137 | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
1.1138 - ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
1.1139 - if k = k'
1.1140 - then ((Ptyp (k', [pbt], ps)) :: pys)
1.1141 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
1.1142 - )
1.1143 - | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
1.1144 - ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
1.1145 - if k = k'
1.1146 - then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
1.1147 - else
1.1148 - if length pys = 0
1.1149 - then error ("insert: not found " ^ (strs2str (d : pblID)))
1.1150 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
1.1151 - );
1.1152 + ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
1.1153 + if k = k'
1.1154 + then ((Ptyp (k', [pbt], ps)) :: pys)
1.1155 + else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
1.1156 + )
1.1157 + | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =
1.1158 + ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
1.1159 + if k = k'
1.1160 + then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
1.1161 + else
1.1162 + if length pys = 0
1.1163 + then error ("insert: not found " ^ (strs2str (d : pblID)))
1.1164 + else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
1.1165 + )
1.1166 + | insrt _ _ _ _ = raise ERROR "";
1.1167
1.1168 fun update_ptyps ID _ _ [] =
1.1169 error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
1.1170 @@ -1164,16 +1040,16 @@
1.1171 if i = key
1.1172 then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
1.1173 else (py :: (update_ptyps ID (i :: is) data pyss))
1.1174 + | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
1.1175
1.1176 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
1.1177 function for trees / ptyps *)
1.1178 fun merge_ptyps ([], pt) = pt
1.1179 | merge_ptyps (pt, []) = pt
1.1180 - | merge_ptyps ((x' as Ptyp (k, x, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
1.1181 + | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
1.1182 if k = k'
1.1183 then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
1.1184 else x' :: merge_ptyps (xs, xs');
1.1185 -fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2)
1.1186
1.1187 (* data for methods stored in 'methods'-database*)
1.1188 type met =
1.1189 @@ -1200,40 +1076,33 @@
1.1190 pre : term list, (*preconditions in where *)
1.1191 scr : scr (*prep_met gets progam or string "empty_script"*)
1.1192 };
1.1193 -val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
1.1194 - rew_ord' = "e_rew_ord'": rew_ord',
1.1195 - erls = e_rls, srls = e_rls, prls = e_rls,
1.1196 - calc = [], crls = e_rls, errpats = [], nrls= e_rls,
1.1197 - ppc = []: (string * (term * term)) list,
1.1198 - pre = []: term list,
1.1199 - scr = EmptyScr: scr}:met;
1.1200 -
1.1201 -
1.1202 -val e_Mets = Ptyp ("e_metID",[e_met],[]);
1.1203 +val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
1.1204 + erls = e_rls, srls = e_rls, prls = e_rls, calc = [], crls = e_rls, errpats = [], nrls= e_rls,
1.1205 + ppc = [], pre = [], scr = EmptyScr};
1.1206 +val e_Mets = Ptyp ("e_metID", [e_met],[]);
1.1207
1.1208 type mets = (met ptyp) list;
1.1209 -
1.1210 fun coll_metguhs mets =
1.1211 - let fun node coll (Ptyp (_,[n],ns)) =
1.1212 - [(#guh : met -> guh) n] @ (nodes coll ns)
1.1213 - and nodes coll [] = coll
1.1214 - | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.1215 + let
1.1216 + fun node coll (Ptyp (_, [n], ns)) = [(#guh : met -> guh) n] @ (nodes coll ns)
1.1217 + | node _ _ = raise ERROR "coll_pblguhs - node"
1.1218 + and nodes coll [] = coll
1.1219 + | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
1.1220 in nodes [] mets end;
1.1221 -
1.1222 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
1.1223 if member op = (coll_metguhs mets) guh
1.1224 - then error ("check_guh_unique failed with '"^guh^"';\n"^
1.1225 - "use 'sort_metguhs()' for a list of guhs;\n"^
1.1226 - "consider setting 'check_guhs_unique := false'")
1.1227 + then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
1.1228 + "use \"sort_metguhs()\" for a list of guhs;\n" ^
1.1229 + "consider setting \"check_guhs_unique := false\"")
1.1230 else ();
1.1231
1.1232 fun Html_default exist = (Html {guh = theID2guh exist,
1.1233 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
1.1234
1.1235 -fun fill_parents (exist, [i]) thydata = Ptyp (i, [thydata], [])
1.1236 +fun fill_parents (_, [i]) thydata = Ptyp (i, [thydata], [])
1.1237 | fill_parents (exist, i :: is) thydata =
1.1238 Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
1.1239 - | fill_parents _ _ = error "Html_default: avoid ML warning: Matches are not exhaustive"
1.1240 + | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
1.1241
1.1242 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
1.1243 | add_thydata (exist, [i]) data (pys as (py as Ptyp (key, _, _)) :: pyss) =
1.1244 @@ -1247,49 +1116,49 @@
1.1245 then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
1.1246 else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
1.1247 else py :: add_thydata (exist, iss) data pyss
1.1248 - | add_thydata _ _ _ = error "add_thydata: avoid ML warning: Matches are not exhaustive"
1.1249 + | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
1.1250
1.1251 fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
1.1252 Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.1253 fillpats = fillpats', thm = thm}
1.1254 - | update_hthm _ _ = raise ERROR "wrong data";
1.1255 + | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
1.1256
1.1257 -(* for interface for dialog-authoring *)
1.1258 +(* for dialog-authoring *)
1.1259 fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
1.1260 + let
1.1261 + val rls' =
1.1262 + case rls of
1.1263 + Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
1.1264 + => Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1.1265 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1.1266 + | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
1.1267 + => Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1.1268 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1.1269 + | Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
1.1270 + => Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
1.1271 + scr = scr, errpatts = errpatIDs}
1.1272 + | Erls => Erls
1.1273 + in
1.1274 + Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.1275 + thy_rls = (thyID, rls')}
1.1276 + end
1.1277 + | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
1.1278 +
1.1279 +fun app_py p f (d:pblID) (k(*:pblRD*)) =
1.1280 let
1.1281 - val rls' =
1.1282 - case rls of
1.1283 - Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
1.1284 - Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1.1285 - calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1.1286 - | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
1.1287 - Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1.1288 - calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1.1289 - | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>
1.1290 - Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
1.1291 - scr = scr, errpatts = errpatIDs}
1.1292 - | Erls => Erls
1.1293 - in
1.1294 - Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.1295 - thy_rls = (thyID, rls')}
1.1296 - end
1.1297 - | update_hrls _ _ = raise ERROR "wrong data";
1.1298 -
1.1299 -fun app_py p f (d:pblID) (k(*:pblRD*)) = let
1.1300 - fun py_err _ =
1.1301 - error ("app_py: not found: " ^ (strs2str d));
1.1302 + fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);
1.1303 fun app_py' _ [] = py_err ()
1.1304 | app_py' [] _ = py_err ()
1.1305 - | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) =
1.1306 - if k0 = k' then f p' else app_py' [k0] ps
1.1307 - | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =
1.1308 - if k0 = k'' then app_py' ks ps else app_py' k' ps';
1.1309 + | app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) =
1.1310 + if k0 = k' then f p' else app_py' [k0] ps
1.1311 + | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =
1.1312 + if k0 = k'' then app_py' ks ps else app_py' k' ps';
1.1313 in app_py' k p end;
1.1314 -
1.1315 -fun get_py p = let
1.1316 - fun extract_py (Ptyp (_, [py], _)) = py
1.1317 - | extract_py _ = error ("extract_py: Ptyp has wrong format.");
1.1318 - in app_py p extract_py end;
1.1319 +fun get_py p =
1.1320 + let
1.1321 + fun extract_py (Ptyp (_, [py], _)) = py
1.1322 + | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");
1.1323 + in app_py p extract_py end;
1.1324
1.1325 fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)
1.1326 let
1.1327 @@ -1326,6 +1195,7 @@
1.1328 in
1.1329 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
1.1330 end
1.1331 +
1.1332 fun progthys () = (*["Isac", .., "Descript", "Delete"]*)
1.1333 let
1.1334 fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)