1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Jun 11 13:40:26 2014 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Jun 11 16:11:26 2014 +0200
1.3 @@ -273,78 +273,18 @@
1.4
1.5 (*.create the unique handles and filenames for the theory-data.*)
1.6 fun part2filename str = part2guh str ^ ".xml" : filename;
1.7 -
1.8 -fun thy2guh ([part, thyID]:theID) =
1.9 - (case part of
1.10 - "Isabelle" => "thy_isab_" ^ thyID : guh
1.11 - | "IsacScripts" => "thy_scri_" ^ thyID
1.12 - | "IsacKnowledge" => "thy_isac_" ^ thyID
1.13 - | str => error ("thy2guh: called with '"^str^"'"))
1.14 - | thy2guh theID = error ("thy2guh called with '"^strs2str' theID^"'");
1.15 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
1.16 -fun thypart2guh ([part, thyID, thypart]:theID) =
1.17 - case part of
1.18 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
1.19 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
1.20 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
1.21 - | str => error ("thypart2guh: called with '"^str^"'");
1.22 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
1.23
1.24 -(*.convert the data got via contextToThy to a globally unique handle
1.25 - there is another way to get the guh out of the 'theID' in the hierarchy.*)
1.26 -fun thm2guh (isa, thyID:thyID) (thmID:thmID) =
1.27 - case isa of
1.28 - "Isabelle" =>
1.29 - "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
1.30 - | "IsacKnowledge" =>
1.31 - "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.32 - | "IsacScripts" =>
1.33 - "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.34 - | str => error ("thm2guh called with isa = '"^isa^
1.35 - "' for thm = "^thmID^"'");
1.36 fun thm2filename (isa_thyID: string * thyID) thmID =
1.37 (thm2guh isa_thyID thmID) ^ ".xml" : filename;
1.38 -
1.39 -fun rls2guh (isa, thyID:thyID) (rls':rls') =
1.40 - case isa of
1.41 - "Isabelle" =>
1.42 - "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
1.43 - | "IsacKnowledge" =>
1.44 - "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.45 - | "IsacScripts" =>
1.46 - "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.47 - | str => error ("rls2guh called with isa = '"^isa^
1.48 - "' for rls = '"^rls'^"'");
1.49 - fun rls2filename (isa, thyID) rls' =
1.50 +fun rls2filename (isa, thyID) rls' =
1.51 rls2guh (isa, thyID) rls' ^ ".xml" : filename;
1.52 -
1.53 -fun cal2guh (isa, thyID:thyID) calID =
1.54 - case isa of
1.55 - "Isabelle" =>
1.56 - "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
1.57 - | "IsacKnowledge" =>
1.58 - "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.59 - | "IsacScripts" =>
1.60 - "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.61 - | str => error ("cal2guh called with isa = '"^isa^
1.62 - "' for cal = '"^calID^"'");
1.63 fun cal2filename (isa, thyID:thyID) calID =
1.64 cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
1.65 -
1.66 -fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =
1.67 - case isa of
1.68 - "Isabelle" =>
1.69 - "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
1.70 - | "IsacKnowledge" =>
1.71 - "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.72 - | "IsacScripts" =>
1.73 - "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.74 - | str => error ("ord2guh called with isa = '"^isa^
1.75 - "' for ord = '"^rew_ord'^"'");
1.76 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
1.77 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
1.78
1.79 -
1.80 (**.set up isab_thm_thy in Isac.ML.**)
1.81
1.82 fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, prop_of thm));
2.1 --- a/src/Tools/isac/calcelems.sml Wed Jun 11 13:40:26 2014 +0200
2.2 +++ b/src/Tools/isac/calcelems.sml Wed Jun 11 16:11:26 2014 +0200
2.3 @@ -493,6 +493,63 @@
2.4 | str => error ("thy2guh: called with '"^str^"'"))
2.5 | part2guh theID = error ("part2guh called with theID = " ^ theID2str theID);
2.6
2.7 +fun thy2guh ([part, thyID] : theID) = (case part of
2.8 + "Isabelle" => "thy_isab_" ^ thyID : guh
2.9 + | "IsacScripts" => "thy_scri_" ^ thyID
2.10 + | "IsacKnowledge" => "thy_isac_" ^ thyID
2.11 + | str => error ("thy2guh: called with '" ^ str ^ "'"))
2.12 + | thy2guh theID = error ("thy2guh called with '" ^ strs2str' theID ^ "'");
2.13 +
2.14 +fun thypart2guh ([part, thyID, thypart] : theID) = case part of
2.15 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
2.16 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
2.17 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
2.18 + | str => error ("thypart2guh: called with '" ^ str ^ "'");
2.19 +
2.20 +(* convert the data got via contextToThy to a globally unique handle
2.21 + there is another way to get the guh out of the 'theID' in the hierarchy *)
2.22 +fun thm2guh (isa, thyID:thyID) (thmID:thmID) = case isa of
2.23 + "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
2.24 + | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
2.25 + | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
2.26 + | str => error ("thm2guh called with isa = '" ^ isa ^ "' for thm = " ^ thmID ^ "'");
2.27 +
2.28 +fun rls2guh (isa, thyID:thyID) (rls':rls') = case isa of
2.29 + "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
2.30 + | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
2.31 + | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
2.32 + | str => error ("rls2guh called with isa = '" ^ isa ^ "' for rls = '" ^ rls' ^ "'");
2.33 +
2.34 +fun cal2guh (isa, thyID:thyID) calID = case isa of
2.35 + "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
2.36 + | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
2.37 + | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
2.38 + | str => error ("cal2guh called with isa = '" ^ isa ^ "' for cal = '" ^ calID ^ "'");
2.39 +
2.40 +fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') = case isa of
2.41 + "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
2.42 + | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
2.43 + | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
2.44 + | str => error ("ord2guh called with isa = '" ^ isa ^ "' for ord = '" ^ rew_ord' ^ "'");
2.45 +
2.46 +(* not only for thydata, but also for thy's etc *)
2.47 +fun theID2guh (theID : theID) = case length theID of
2.48 + 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
2.49 + | 1 => part2guh theID
2.50 + | 2 => thy2guh theID
2.51 + | 3 => thypart2guh theID
2.52 + | 4 =>
2.53 + let val [isa, thyID, typ, elemID] = theID
2.54 + in case typ of
2.55 + "Theorems" => thm2guh (isa, thyID) elemID
2.56 + | "Rulesets" => rls2guh (isa, thyID) elemID
2.57 + | "Calculations" => cal2guh (isa, thyID) elemID
2.58 + | "Orders" => ord2guh (isa, thyID) elemID
2.59 + | "Theorems" => thy2guh [isa, thyID]
2.60 + | str => error ("theID2guh: called with theID = " ^ strs2str' theID)
2.61 + end
2.62 + | n => error ("theID2guh called with theID = " ^ strs2str' theID);
2.63 +
2.64 (* an association list, gets the value once in Isac.ML.
2.65 stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
2.66 WN1-1-28 make this data arguments and del ref ?*)
2.67 @@ -904,7 +961,67 @@
2.68 "consider setting 'check_guhs_unique := false'")
2.69 else ();
2.70
2.71 +(* for preserving elements created by 'fun store_thy' *)
2.72 +fun exist_the (theID : theID) (thy_hie : thehier) =
2.73 + let
2.74 + fun node theID ids (Ptyp (id, _, ns)) =
2.75 + if theID = ids @ [id] then true else nodes theID (ids @ [id]) ns
2.76 + and nodes _ _ [] = false
2.77 + | nodes theID ids (n::ns) =
2.78 + if node theID ids n then true else nodes theID ids ns
2.79 + in nodes theID [] thy_hie end;
2.80
2.81 +(* insrt requires a parent; see 'fun fill_parents' *)
2.82 +fun can_insert (theID : theID) (thy_hie : thehier) =
2.83 + (insrt theID e_thydata theID thy_hie; true)
2.84 + handle _ => false;
2.85 +
2.86 +(* cut 'theID', the ID of theory elements from tail to head
2.87 + until insertion into the hierarchy of theory elements 'th' is possible
2.88 + (the hierarchy requires the parentnode to exist for insertion) *)
2.89 +fun cut_theID th ([] : theID) = error "could not insert into thy-hierarchy"
2.90 + | cut_theID th theID =
2.91 + if can_insert theID th
2.92 + then theID else cut_theID th (drop_last theID);
2.93 +
2.94 +(* insert empty parents 'Html' into the hierarchy of theory elements 'th'
2.95 + until the actual node can be inserted with key 'theID' *)
2.96 +fun fill_parents th cutID theID =
2.97 + let val cutID' = cut_theID th cutID
2.98 + in if cutID' = theID
2.99 + then th
2.100 + else
2.101 + let
2.102 + val th' = insrt cutID' (Html {guh=theID2guh theID, coursedesign = ["isac team 2006"],
2.103 + mathauthors = [], html = ""}) cutID' th
2.104 + val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
2.105 + in fill_parents th' cutID_ theID end
2.106 + end;
2.107 +
2.108 +(* argument 1 "th : thehier": contains some thydata from "setup {* KEStore_Elems.add_thes ..."
2.109 + argument 1 "th : thehier": contains some thydata from "store_thes ..."
2.110 + already in some "ProgLang/*.thy" or "Knowledge/*.thy"
2.111 + argument 2 "(theID, thydata)::_ : (theID * thydata) list: contains thydata collected
2.112 + automatically in Build_Thydata.thy finally.
2.113 + parents of thydata in list, missing in thehier, are inserted
2.114 + (causing msgs '*** insert: not found');
2.115 + (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
2.116 +fun the_hier th ([]: (theID * thydata) list) = th
2.117 + | the_hier th ((theID, thydata)::ths) =
2.118 + if can_insert theID th
2.119 + then
2.120 + let
2.121 + val th' =
2.122 + if exist_the theID th
2.123 + then (writeln ("*** insert: preserved " ^ strs2str theID); th)
2.124 + else insrt theID thydata theID th
2.125 + in the_hier th' ths end
2.126 + else
2.127 + let
2.128 + val th' = fill_parents th theID theID (*..*** insert: not found*)
2.129 + val th' = insrt theID thydata theID th'
2.130 + in the_hier th' ths end;
2.131 +
2.132 (*
2.133 end (*struct*)
2.134 *)
3.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Jun 11 13:40:26 2014 +0200
3.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Jun 11 16:11:26 2014 +0200
3.3 @@ -125,69 +125,6 @@
3.4 use the same mechanism as for pbl_hierarchy and met_hierarchy;
3.5 but check, if a thydata is already there (for auto-gen. Isabelle).**)
3.6
3.7 -(*.for preserving elements created by 'fun store_thy'.*)
3.8 -fun exist_the (theID:theID) (thy_hie:thehier) =
3.9 - let fun node theID ids (Ptyp (id,_,ns)) =
3.10 - if theID = ids @ [id] then true
3.11 - else nodes theID (ids @ [id]) ns
3.12 - and nodes _ _ [] = false
3.13 - | nodes theID ids (n::ns) = if node theID ids n then true
3.14 - else nodes theID ids ns
3.15 - in nodes theID [] thy_hie end;
3.16 -
3.17 -(*.insrt requires a parent; see 'fun fill_parents'.*)
3.18 -fun can_insert (theID:theID) (thy_hie:thehier) =
3.19 - (insrt theID e_thydata theID thy_hie; true)
3.20 - handle _ => false;
3.21 -
3.22 -(*.cut 'theID', the ID of theory elements from tail to head
3.23 - until insertion into the hierarchy of theory elements 'th' is possible
3.24 - (the hierarchy requires the parentnode to exist for insertion).*)
3.25 -fun cut_theID th ([]:theID) =
3.26 - error "could not insert into thy-hierarchy"
3.27 - | cut_theID th theID =
3.28 - if can_insert theID th
3.29 - then theID else cut_theID th (drop_last theID);
3.30 -
3.31 -(*.insert empty parents 'Html' into the hierarchy of theory elements 'th'
3.32 - until the actual node can be inserted with key 'theID'.*)
3.33 -fun fill_parents th cutID theID =
3.34 - let val cutID' = cut_theID th cutID
3.35 - in if cutID' = theID
3.36 - then th
3.37 - else let val th' = insrt cutID' (Html {guh=theID2guh theID,
3.38 - coursedesign=["isac team 2006"],
3.39 - mathauthors=[],
3.40 - html=""}) cutID' th
3.41 - val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
3.42 - in fill_parents th' cutID_ theID end
3.43 - end;
3.44 -
3.45 -(* argument 1 "th : thehier": contains some thydata from "setup {* KEStore_Elems.add_thes ..."
3.46 - argument 1 "th : thehier": contains some thydata from "store_thes ..."
3.47 - already in some "ProgLang/*.thy" or "Knowledge/*.thy"
3.48 - argument 2 "(theID, thydata)::_ : (theID * thydata) list: contains thydata collected
3.49 - automatically in Build_Thydata.thy finally.
3.50 - parents of thydata in list, missing in thehier, are inserted
3.51 - (causing msgs '*** insert: not found');
3.52 - (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
3.53 -fun the_hier th ([]: (theID * thydata) list) = th
3.54 - | the_hier th ((theID, thydata)::ths) =
3.55 - if can_insert theID th
3.56 - then
3.57 - let
3.58 - val th' =
3.59 - if exist_the theID th
3.60 - then (writeln ("*** insert: preserved " ^ strs2str theID); th)
3.61 - else insrt theID thydata theID th
3.62 - in the_hier th' ths end
3.63 - else
3.64 - let
3.65 - val th' = fill_parents th theID theID (*..*** insert: not found*)
3.66 - val th' = insrt theID thydata theID th'
3.67 - in the_hier th' ths end;
3.68 -
3.69 -
3.70 (*these files shall contain 'invisible' html
3.71 val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)
3.72 fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*)