1.1 --- a/src/Tools/isac/Frontend/interface.sml Tue Jan 11 15:28:03 2011 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Feb 21 19:40:36 2011 +0100
1.3 @@ -69,7 +69,7 @@
1.4 let fun enc [] = []
1.5 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
1.6 | enc (c :: cs) = c :: (enc cs)
1.7 - in (implode o enc o explode) str:cterm' end;
1.8 + in (implode o enc o Symbol.explode) str:cterm' end;
1.9 fun encode_imodel (imodel:imodel) =
1.10 let fun enc (Given ifos) = Given (map encode ifos)
1.11 | enc (Find ifos) = Find (map encode ifos)
1.12 @@ -402,7 +402,7 @@
1.13
1.14 (*.set the context determined on a knowledgebrowser to the current calc.*)
1.15 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
1.16 - (case (implode o (take_fromto 1 4) o explode) guh of
1.17 + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.18 "thy_" =>
1.19 (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
1.20 *)
1.21 @@ -775,7 +775,7 @@
1.22 (1, ([1], Res), "thy_isac_Test-rls-Test_simplify");
1.23 *)
1.24 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
1.25 - (case (implode o (take_fromto 1 4) o explode) guh of
1.26 + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.27 "thy_" =>
1.28 if member op = [Pbl,Met] p_
1.29 then message2xml cI "thy-context not to calchead"
2.1 --- a/src/Tools/isac/Interpret/appl.sml Tue Jan 11 15:28:03 2011 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Feb 21 19:40:36 2011 +0100
2.3 @@ -207,7 +207,7 @@
2.4 let fun scan s' [] = (implode s', "")
2.5 | scan s' (s::ss) = if s=" " then (implode s', implode ss)
2.6 else scan (s'@[s]) ss;
2.7 -in ((scan []) o explode) str end;
2.8 +in ((scan []) o Symbol.explode) str end;
2.9 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
2.10 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
2.11 > split_dummy "x=-#5//#12";
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Tue Jan 11 15:28:03 2011 +0100
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Feb 21 19:40:36 2011 +0100
3.3 @@ -850,17 +850,17 @@
3.4 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
3.5 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
3.6 fun is_copy_named_idstr str =
3.7 - case (rev o explode) str of
3.8 - "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode))
3.9 + case (rev o Symbol.explode) str of
3.10 + "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
3.11 "is_copy_named_idstr: " ^ str ^ " T"); true)
3.12 - | _ => (tracing ((strs2str o (rev o explode))
3.13 + | _ => (tracing ((strs2str o (rev o Symbol.explode))
3.14 "is_copy_named_idstr: " ^ str ^ " F"); false);
3.15 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
3.16
3.17 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
3.18 fun is_copy_named_generating_idstr str =
3.19 if is_copy_named_idstr str
3.20 - then case (rev o explode) str of
3.21 + then case (rev o Symbol.explode) str of
3.22 "'"::"'"::"'"::_ => false
3.23 | _ => true
3.24 else false;
3.25 @@ -934,8 +934,8 @@
3.26 (if is_copy_named_generating p
3.27 then (*WN051014 kept strange old code ...*)
3.28 let fun sel (_,_,d,ts) = comp_ts (d, ts)
3.29 - val cy' = (implode o (drop_last_n 3) o explode o free2str) t
3.30 - val ext = (last_elem o drop_last o explode o free2str) t
3.31 + val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
3.32 + val ext = (last_elem o drop_last o Symbol.explode o free2str) t
3.33 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
3.34 val vals = map sel oris
3.35 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
3.36 @@ -1334,7 +1334,7 @@
3.37 (*TODO.WN03 pass error-msgs to the frontend..
3.38 FIXME ..and dont abuse a tactic for that purpose*)
3.39 ([(Tac msg,
3.40 - Tac_ (theory "Pure", msg,msg,msg),
3.41 + Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
3.42 (e_pos', e_istate))], [], ptp)
3.43 end
3.44
4.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Jan 11 15:28:03 2011 +0100
4.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Feb 21 19:40:36 2011 +0100
4.3 @@ -219,7 +219,7 @@
4.4 in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end
4.5 end;
4.6
4.7 -(*lazy evaluation for (theory "Isac")*)
4.8 +(*lazy evaluation for (Thy_Info.get_theory "Isac")*)
4.9 fun Isac _ = assoc_thy "Isac";
4.10
4.11 (*re-parse itms with a new thy and prepare for checking with ori list*)
5.1 --- a/src/Tools/isac/Interpret/mstools.sml Tue Jan 11 15:28:03 2011 +0100
5.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Feb 21 19:40:36 2011 +0100
5.3 @@ -158,8 +158,8 @@
5.4 structure SpecifyTools : SPECIFY_TOOLS =
5.5 struct
5.6 (*----------------------------------------------------------*)
5.7 -val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)";
5.8 -val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)";
5.9 +val e_listReal = (term_of o the o (parse (Thy_Info.get_theory "Script"))) "[]::(real list)";
5.10 +val e_listBool = (term_of o the o (parse (Thy_Info.get_theory "Script"))) "[]::(bool list)";
5.11
5.12 (*.take list-term apart w.r.t. handling elementwise input.*)
5.13 fun take_apart t =
5.14 @@ -197,17 +197,17 @@
5.15 (*.revert split_.
5.16 WN050903 we do NOT know which is from subtheory, description or term;
5.17 typecheck thus may lead to TYPE-error 'unknown constant';
5.18 - solution: typecheck with (theory "Isac"); i.e. arg 'thy' superfluous*)
5.19 + solution: typecheck with (Thy_Info.get_theory "Isac"); i.e. arg 'thy' superfluous*)
5.20 (*fun comp_dts thy (d,[]) =
5.21 cterm_of (*(sign_of o assoc_thy) "Isac"*)
5.22 - (theory "Isac")
5.23 + (Thy_Info.get_theory "Isac")
5.24 (*comp_dts:FIXXME stay with term for efficiency !!!*)
5.25 (if is_reall_dsc d then (d $ e_listReal)
5.26 else if is_booll_dsc d then (d $ e_listBool)
5.27 else d)
5.28 | comp_dts thy (d,ts) =
5.29 (cterm_of (*(sign_of o assoc_thy) "Isac"*)
5.30 - (theory "Isac")
5.31 + (Thy_Info.get_theory "Isac")
5.32 (*comp_dts:FIXXME stay with term for efficiency !!*)
5.33 (d $ (comp_ts (d, ts)))
5.34 handle _ => error ("comp_dts: "^(term2str d)^
5.35 @@ -301,7 +301,7 @@
5.36 fun dest_list' t = if is_list t then isalist2list t else [t];
5.37
5.38 (*fun is_metavar (Free (str, _)) =
5.39 - if (last_elem o explode) str = "_" then true else false
5.40 + if (last_elem o Symbol.explode) str = "_" then true else false
5.41 | is_metavar _ = false;*)
5.42 fun is_var (Free _) = true
5.43 | is_var _ = false;
5.44 @@ -909,7 +909,7 @@
5.45 | ts_in (Mis _) = [];
5.46 (*WN050629 unused*)
5.47 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
5.48 -val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM";
5.49 +val unique = (term_of o the o (parse (Thy_Info.get_theory "Real"))) "UnIqE_tErM";
5.50 fun d_in (Cor ((d,_),_)) = d
5.51 | d_in (Syn (c)) = (tracing("*** d_in: Syn ("^c^")"); unique)
5.52 | d_in (Typ (c)) = (tracing("*** d_in: Typ ("^c^")"); unique)
6.1 --- a/src/Tools/isac/Interpret/ptyps.sml Tue Jan 11 15:28:03 2011 +0100
6.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Feb 21 19:40:36 2011 +0100
6.3 @@ -388,7 +388,7 @@
6.4 it contains "#Given","#Where","#Find","#Relate"-patterns
6.5 for constraints on identifiers see "fun cpy_nam"*)
6.6 met : metID list}; (* methods solving the pbt*)
6.7 -val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure",
6.8 +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=Thy_Info.get_theory "Pure",
6.9 cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
6.10 fun pbt2 (str, (t1, t2)) =
6.11 pair2str (str, pair2str (term2str t1, term2str t2));
6.12 @@ -437,15 +437,15 @@
6.13 (*TODO: search generalized for subthy*)
6.14 fun get_pbt (pblID:pblID) =
6.15 let val pblRD = rev pblID;
6.16 - in get_py (theory "Pure") pblID pblRD (!ptyps) end;
6.17 + in get_py (Thy_Info.get_theory "Pure") pblID pblRD (!ptyps) end;
6.18 (* get_pbt thy ["1"];
6.19 get_pbt thy ["21","2"];
6.20 *)
6.21
6.22 (*TODO: throws exn 'get_pbt not found: ' ... confusing !!
6.23 take 'ketype' as an argument !!!!!*)
6.24 -fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets);
6.25 -fun get_the (theID:theID) = get_py (theory "Pure") theID theID (! thehier);
6.26 +fun get_met (metID:metID) = get_py (Thy_Info.get_theory "Pure") metID metID (!mets);
6.27 +fun get_the (theID:theID) = get_py (Thy_Info.get_theory "Pure") theID theID (! thehier);
6.28
6.29
6.30
6.31 @@ -491,7 +491,7 @@
6.32
6.33 (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
6.34 fun guh2kestoreID (guh:guh) =
6.35 - case (implode o (take_fromto 1 4) o explode) guh of
6.36 + case (implode o (take_fromto 1 4) o Symbol.explode) guh of
6.37 "pbl_" =>
6.38 let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
6.39 if gu = guh
7.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Jan 11 15:28:03 2011 +0100
7.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Feb 21 19:40:36 2011 +0100
7.3 @@ -195,7 +195,7 @@
7.4
7.5 (*.toggles the marker for 'fun sym_thm'.*)
7.6 fun sym_thmID (thmID : thmID) =
7.7 - case explode thmID of
7.8 + case Symbol.explode thmID of
7.9 "s"::"y"::"m"::"_"::id => implode id : thmID
7.10 | id => "sym_"^thmID;
7.11 (*
7.12 @@ -206,11 +206,11 @@
7.13 > sym_thmID thmID;
7.14 val it = "sym_real_num_collect" : string*)
7.15 fun sym_drop (thmID : thmID) =
7.16 - case explode thmID of
7.17 + case Symbol.explode thmID of
7.18 "s"::"y"::"m"::"_"::id => implode id : thmID
7.19 | id => thmID;
7.20 fun is_sym (thmID : thmID) =
7.21 - case explode thmID of
7.22 + case Symbol.explode thmID of
7.23 "s"::"y"::"m"::"_"::id => true
7.24 | id => false;
7.25
7.26 @@ -763,7 +763,7 @@
7.27 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
7.28
7.29 fun guh2theID (guh:guh) =
7.30 - let val guh' = explode guh
7.31 + let val guh' = Symbol.explode guh
7.32 val part = implode (take_fromto 1 4 guh')
7.33 val isa = implode (take_fromto 5 9 guh')
7.34 in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
8.1 --- a/src/Tools/isac/Interpret/script.sml Tue Jan 11 15:28:03 2011 +0100
8.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Feb 21 19:40:36 2011 +0100
8.3 @@ -97,7 +97,7 @@
8.4 let fun scan [] = []
8.5 | scan (s::ss) = if s = "'" then (scan ss)
8.6 else (s::(scan ss))
8.7 - in (implode o scan o explode) str end;
8.8 + in (implode o scan o Symbol.explode) str end;
8.9 (*
8.10 > val str = "Rewrite_Set_Inst";
8.11 > val esc = esc_underscore str;
8.12 @@ -159,7 +159,7 @@
8.13
8.14 fun test_negotiable t =
8.15 member op = (!negotiable)
8.16 - ((strip_thy o (term_str (theory "Script")) o head_of) t);
8.17 + ((strip_thy o (term_str (Thy_Info.get_theory "Script")) o head_of) t);
8.18
8.19 (*.get argument of first stactic in a script for init_form.*)
8.20 fun get_stac thy (h $ body) =
8.21 @@ -381,7 +381,7 @@
8.22 stac2tac_ pt thy mm;
8.23
8.24 assoc_thm' (assoc_thy "Isac") (tid,"");
8.25 - assoc_thm' (theory "Isac") (tid,"");
8.26 + assoc_thm' (Thy_Info.get_theory "Isac") (tid,"");
8.27 *)
8.28 | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $
8.29 sub $ Free (thmID,_) $ _ $ f) =
8.30 @@ -443,7 +443,7 @@
8.31 Free (dI',_) $
8.32 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
8.33 (*compare "| assod _ (Subproblem'"*)
8.34 - let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^""*);
8.35 + let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
8.36 val thy = maxthy (assoc_thy dI) (rootthy pt);
8.37 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
8.38 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
8.39 @@ -654,7 +654,7 @@
8.40 Free (dI',_) $
8.41 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
8.42 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
8.43 - let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^""*);
8.44 + let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
8.45 val thy = maxthy (assoc_thy dI) (rootthy pt);
8.46 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
8.47 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
8.48 @@ -1074,7 +1074,7 @@
8.49 assy ya ((E,(l@[R]),a,v,S,b),ss) e2
8.50 | ay => (ay))
8.51 (* val ((m,_,pt,(p,p_),c)::ss) = [(m,EmptyMout,pt,p,[])];
8.52 - val t = (term_of o the o (parse (theory "Isac"))) "Rewrite rmult_1 False";
8.53 + val t = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "Rewrite rmult_1 False";
8.54
8.55 val (ap,(p,p_),c,ss) = (Aundef,p,[],[]);
8.56 assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t;
8.57 @@ -1928,8 +1928,8 @@
8.58 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
8.59 (*
8.60 > val Script sc = (#scr o get_met) ("SqRoot","sqrt-equ-test");
8.61 -> val env = [((term_of o the o (parse (theory "Isac"))) "bdv",
8.62 - (term_of o the o (parse (theory "Isac"))) "x")];
8.63 +> val env = [((term_of o the o (parse (Thy_Info.get_theory "Isac"))) "bdv",
8.64 + (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "x")];
8.65 > map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc);
8.66 *)
8.67
9.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Jan 11 15:28:03 2011 +0100
9.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Feb 21 19:40:36 2011 +0100
9.3 @@ -112,7 +112,7 @@
9.4
9.5 fun dest_hd' (Const (a, T)) = (((a, 0), T), 0)
9.6 | dest_hd' (Free (ccc, T)) =
9.7 - (case explode ccc of
9.8 + (case Symbol.explode ccc of
9.9 "c"::[] => ((("|||||||||||||||||||||", 0), T), 1)(*greatest string WN*)
9.10 | "c"::"_"::_ => ((("|||||||||||||||||||||", 0), T), 1)
9.11 | _ => (((ccc, 0), T), 1))
9.12 @@ -121,7 +121,7 @@
9.13 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
9.14
9.15 fun size_of_term' (Free (ccc, _)) =
9.16 - (case explode ccc of (*WN0510 hack for the bound variables*)
9.17 + (case Symbol.explode ccc of (*WN0510 hack for the bound variables*)
9.18 "c"::[] => 1000
9.19 | "c"::"_"::is => 1000 * ((str2int o implode) is)
9.20 | _ => 1)
9.21 @@ -190,7 +190,7 @@
9.22 val order_add_mult_System =
9.23 Rls{id = "order_add_mult_System", preconds = [],
9.24 rew_ord = ("ord_simplify_System",
9.25 - ord_simplify_System false (theory "Integrate")),
9.26 + ord_simplify_System false (Thy_Info.get_theory "Integrate")),
9.27 erls = e_rls,srls = Erls, calc = [],
9.28 rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
9.29 (* z * w = w * z *)
10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Tue Jan 11 15:28:03 2011 +0100
10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Mon Feb 21 19:40:36 2011 +0100
10.3 @@ -62,7 +62,7 @@
10.4 (** problem type **)
10.5
10.6 store_pbt
10.7 - (prep_pbt (theory "InsSort")
10.8 + (prep_pbt (Thy_Info.get_theory "InsSort")
10.9 (["functional"]:pblID,
10.10 [("#Given" ,["unsorted u_"]),
10.11 ("#Find" ,["sorted s_"])
10.12 @@ -70,7 +70,7 @@
10.13 []));
10.14
10.15 store_pbt
10.16 - (prep_pbt (theory "InsSort")
10.17 + (prep_pbt (Thy_Info.get_theory "InsSort")
10.18 (["inssort","functional"]:pblID,
10.19 [("#Given" ,["unsorted u_"]),
10.20 ("#Find" ,["sorted s_"])
10.21 @@ -81,14 +81,14 @@
10.22 todo: implementation needs extra object-level lists **)
10.23
10.24 store_met
10.25 - (prep_met (theory "Diff")
10.26 + (prep_met (Thy_Info.get_theory "Diff")
10.27 (["InsSort"],
10.28 [],
10.29 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
10.30 crls = Atools_rls, nrls=norm_Rational
10.31 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
10.32 store_met
10.33 - (prep_met (theory "InsSort") (*test-version for [#1,#3,#2] only: see *.sml*)
10.34 + (prep_met (Thy_Info.get_theory "InsSort") (*test-version for [#1,#3,#2] only: see *.sml*)
10.35 (["InsSort""sort"]:metID,
10.36 [("#Given" ,["unsorted u_"]),
10.37 ("#Find" ,["sorted s_"])
11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Jan 11 15:28:03 2011 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Feb 21 19:40:36 2011 +0100
11.3 @@ -56,13 +56,13 @@
11.4 from a variable, but the value '(new_c es__)' itself.*)
11.5 fun new_c term =
11.6 let fun selc var =
11.7 - case (explode o id_of) var of
11.8 + case (Symbol.explode o id_of) var of
11.9 "c"::[] => true
11.10 | "c"::"_"::is => (case (int_of_str o implode) is of
11.11 SOME _ => true
11.12 | NONE => false)
11.13 | _ => false;
11.14 - fun get_coeff c = case (explode o id_of) c of
11.15 + fun get_coeff c = case (Symbol.explode o id_of) c of
11.16 "c"::"_"::is => (the o int_of_str o implode) is
11.17 | _ => 0;
11.18 val cs = filter selc (vars term);
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Jan 11 15:28:03 2011 +0100
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Feb 21 19:40:36 2011 +0100
12.3 @@ -1,7 +1,7 @@
12.4 (* theory collecting all knowledge
12.5 (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
12.6 for PolynomialEquations.
12.7 - alternative dependencies see (theory "Isac")
12.8 + alternative dependencies see (Thy_Info.get_theory "Isac")
12.9 created by: rlang
12.10 date: 02.07
12.11 changed by: rlang
12.12 @@ -1384,7 +1384,7 @@
12.13 val order_add_mult_in = prep_rls(
12.14 Rls{id = "order_add_mult_in", preconds = [],
12.15 rew_ord = ("ord_make_polynomial_in",
12.16 - ord_make_polynomial_in false (theory "Poly")),
12.17 + ord_make_polynomial_in false (Thy_Info.get_theory "Poly")),
12.18 erls = e_rls,srls = Erls,
12.19 calc = [],
12.20 (*asm_thm = [],*)
13.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jan 11 15:28:03 2011 +0100
13.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Feb 21 19:40:36 2011 +0100
13.3 @@ -113,7 +113,7 @@
13.4 (*. get the identifier from specific monomials; see fun ist_monom .*)
13.5 (*HACK.WN080107*)
13.6 fun increase str =
13.7 - let val s::ss = explode str
13.8 + let val s::ss = Symbol.explode str
13.9 in implode ((chr (ord s + 1))::ss) end;
13.10 fun identifier (Free (id,_)) = id (* 2, a *)
13.11 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Jan 11 15:28:03 2011 +0100
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Feb 21 19:40:36 2011 +0100
14.3 @@ -159,7 +159,7 @@
14.4
14.5 rew_ord' := overwritel (!rew_ord',
14.6 [("termlessI", termlessI),
14.7 - ("sqrt_right", sqrt_right false (theory "Pure"))
14.8 + ("sqrt_right", sqrt_right false (Thy_Info.get_theory "Pure"))
14.9 ]);
14.10
14.11 (*-------------------------rulse-------------------------*)
15.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jan 11 15:28:03 2011 +0100
15.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Feb 21 19:40:36 2011 +0100
15.3 @@ -152,7 +152,7 @@
15.4 ML {*
15.5 (*-------------------------Methode-----------------------*)
15.6 store_met
15.7 - (prep_met (theory "LinEq") "met_rootrateq" [] e_metID
15.8 + (prep_met (Thy_Info.get_theory "LinEq") "met_rootrateq" [] e_metID
15.9 (["RootRatEq"],
15.10 [],
15.11 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
16.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Tue Jan 11 15:28:03 2011 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Mon Feb 21 19:40:36 2011 +0100
16.3 @@ -70,7 +70,7 @@
16.4 (*.function for handling the cas-input "Simplify (2*a + 3*a)":
16.5 make a model which is already in ptree-internal format.*)
16.6 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
16.7 - val (h,argl) = strip_comb ((term_of o the o (parse (theory "Simplify")))
16.8 + val (h,argl) = strip_comb ((term_of o the o (parse (Thy_Info.get_theory "Simplify")))
16.9 "Simplify (2*a + 3*a)");
16.10 *)
16.11 fun argl2dtss t =
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Jan 11 15:28:03 2011 +0100
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Feb 21 19:40:36 2011 +0100
17.3 @@ -244,7 +244,7 @@
17.4 (*FIXXXXXXME 10.8.02: handle like _simplify*)
17.5 val tval_rls =
17.6 Rls{id = "tval_rls", preconds = [],
17.7 - rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
17.8 + rew_ord = ("sqrt_right",sqrt_right false (Thy_Info.get_theory "Pure")),
17.9 erls=testerls,srls = e_rls,
17.10 calc=[],
17.11 rules = [Thm ("refl",num_str @{thm refl}),
17.12 @@ -383,7 +383,7 @@
17.13 (* expects * distributed over + *)
17.14 val Test_simplify =
17.15 Rls{id = "Test_simplify", preconds = [],
17.16 - rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
17.17 + rew_ord = ("sqrt_right",sqrt_right false (Thy_Info.get_theory "Pure")),
17.18 erls = tval_rls, srls = e_rls,
17.19 calc=[(*since 040209 filled by prep_rls*)],
17.20 (*asm_thm = [],*)
17.21 @@ -566,7 +566,7 @@
17.22 []));
17.23
17.24
17.25 -val ttt = (term_of o the o (parse (theory "Isac"))) "(matches ( v_v = 0) e_e)";
17.26 +val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
17.27
17.28 ------ 25.8.01*)
17.29
17.30 @@ -574,7 +574,7 @@
17.31 ML {*
17.32 (** methods **)
17.33 store_met
17.34 - (prep_met (theory "Diff") "met_test" [] e_metID
17.35 + (prep_met (Thy_Info.get_theory "Diff") "met_test" [] e_metID
17.36 (["Test"],
17.37 [],
17.38 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
17.39 @@ -582,7 +582,7 @@
17.40 asm_rls=[],asm_thm=[]*)}, "empty_script"));
17.41 (*
17.42 store_met
17.43 - (prep_met (theory "Script")
17.44 + (prep_met (Thy_Info.get_theory "Script")
17.45 (e_metID,(*empty method*)
17.46 [],
17.47 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
17.48 @@ -1290,7 +1290,7 @@
17.49
17.50 val make_polytest =
17.51 Rls{id = "make_polytest", preconds = []:term list,
17.52 - rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),
17.53 + rew_ord = ("ord_make_polytest", ord_make_polytest false (Thy_Info.get_theory "Poly")),
17.54 erls = testerls, srls = Erls,
17.55 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
17.56 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
18.1 --- a/src/Tools/isac/ProgLang/ListC.thy Tue Jan 11 15:28:03 2011 +0100
18.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Feb 21 19:40:36 2011 +0100
18.3 @@ -4,15 +4,15 @@
18.4 *)
18.5
18.6 theory ListC imports Complex_Main
18.7 -uses ("library.sml")("calcelems.sml")
18.8 -("ProgLang/termC.sml")("ProgLang/calculate.sml")
18.9 -("ProgLang/rewrite.sml")
18.10 +uses ("../library.sml")("../calcelems.sml")
18.11 +("termC.sml")("calculate.sml")
18.12 +("rewrite.sml")
18.13 begin
18.14 -use "library.sml" (*indent,...*)
18.15 -use "calcelems.sml" (*str_of_type, Thm,...*)
18.16 -use "ProgLang/termC.sml" (*num_str,...*)
18.17 -use "ProgLang/calculate.sml" (*???*)
18.18 -use "ProgLang/rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*)
18.19 +use "../library.sml" (*indent,...*)
18.20 +use "../calcelems.sml" (*str_of_type, Thm,...*)
18.21 +use "termC.sml" (*num_str,...*)
18.22 +use "calculate.sml" (*???*)
18.23 +use "rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*)
18.24
18.25 text {* 'nat' in List.thy replaced by 'real' *}
18.26
19.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Jan 11 15:28:03 2011 +0100
19.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Mon Feb 21 19:40:36 2011 +0100
19.3 @@ -215,7 +215,7 @@
19.4 *)
19.5
19.6 (* val ((op_, eval_fn),ct)=(cc,pre);
19.7 - (get_calculation_ (theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
19.8 + (get_calculation_ (Thy_Info.get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
19.9 parse thy ""
19.10 *)
19.11 (*.get a thm from an op_ somewhere in the term;
19.12 @@ -240,7 +240,7 @@
19.13 val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
19.14
19.15 > val ct = (the o (parse thy)) "#4<#4";
19.16 -> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o explode) str = "#";
19.17 +> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";
19.18
19.19 val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
19.20
20.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Tue Jan 11 15:28:03 2011 +0100
20.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Feb 21 19:40:36 2011 +0100
20.3 @@ -395,7 +395,7 @@
20.4 identifiers starting with "#" come from Calc and
20.5 get a hand-made theorem (containing numerals only).*)
20.6 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
20.7 - (case explode thmid of
20.8 + (case Symbol.explode thmid of
20.9 "s"::"y"::"m"::"_"::id =>
20.10 if hd id = "#"
20.11 then mk_thm thy ct'
20.12 @@ -407,13 +407,13 @@
20.13 ) handle _ =>
20.14 error ("assoc_thm': '"^thmid^"' not in '"^
20.15 (theory2domID thy)^"' (and parents)");
20.16 -(*> assoc_thm' (theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
20.17 +(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
20.18 val it = "6 = 2 * 3" : thm
20.19
20.20 -> assoc_thm' (theory "Isac") ("add_0_left","");
20.21 +> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
20.22 val it = "0 + ?z = ?z" : thm
20.23
20.24 -> assoc_thm' (theory "Isac") ("sym_real_add_zero_left","");
20.25 +> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
20.26 val it = "?t = 0 + ?t" [.] : thm
20.27
20.28 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
20.29 @@ -514,7 +514,7 @@
20.30 end;
20.31 (*
20.32 fun instantiate'' thy' subs ((thmid,ct'):thm') =
20.33 - let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
20.34 + let val thmid_ = implode ("#"::(Symbol.explode thmid)) (*see type thm'*)
20.35 in (thmid_, (string_of_thmI o (read_instantiate subs))
20.36 ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
20.37
20.38 @@ -539,7 +539,7 @@
20.39 (* instantiate''
20.40 fun instantiate'' thy' subs ((thmid,ct'):thm') =
20.41 let
20.42 - val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*)
20.43 + val thmid_ = implode ("#"::(Symbol.explode thmid)); (*see type thm'*)
20.44 val thy = assoc_thy thy';
20.45 val typs = map (#T o rep_cterm o the o (parse thy))
20.46 ((snd o split_list) subs);
20.47 @@ -642,7 +642,7 @@
20.48
20.49
20.50
20.51 - rewrite_set_ (theory "Isac") eval_rls false test_rls
20.52 + rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls
20.53 ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
20.54 val xxx = (term_of o the o (parse thy))
20.55 "matches (?a = ?b) (x = #0)";
20.56 @@ -652,7 +652,7 @@
20.57
20.58
20.59
20.60 - rewrite_set_ (theory "Isac") eval_rls false eval_rls
20.61 + rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls
20.62 ((the o (parse thy)) "contains_root (sqrt #0)");
20.63 val it = SOME ("True",[]) : (cterm * cterm list) option
20.64
21.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Jan 11 15:28:03 2011 +0100
21.2 +++ b/src/Tools/isac/ProgLang/termC.sml Mon Feb 21 19:40:36 2011 +0100
21.3 @@ -130,14 +130,14 @@
21.4 *)
21.5
21.6 (*fun int_of_str str =
21.7 - let val ss = explode str
21.8 + let val ss = Symbol.explode str
21.9 val str' = case ss of
21.10 "("::s => drop_last s | _ => ss
21.11 in case BasisLibrary.Int.fromString (implode str') of
21.12 SOME i => SOME i
21.13 | NONE => NONE end;*)
21.14 fun int_of_str str =
21.15 - let val ss = explode str
21.16 + let val ss = Symbol.explode str
21.17 val str' = case ss of
21.18 "("::s => drop_last s | _ => ss
21.19 in (SOME (Thy_Output.integer (implode str'))) handle _ => NONE end;
21.20 @@ -221,7 +221,7 @@
21.21 | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
21.22 in (distinct o (scan [])) t end;
21.23 fun is_bdv str =
21.24 - case explode str of
21.25 + case Symbol.explode str of
21.26 "b"::"d"::"v"::_ => true
21.27 | _ => false;
21.28 fun is_bdv_ (Free (s,_)) = is_bdv s
21.29 @@ -295,8 +295,8 @@
21.30 fun mk_prop t = Trueprop $ t;
21.31 val true_as_term = Const("True",bool);
21.32 val false_as_term = Const("False",bool);
21.33 -val true_as_cterm = cterm_of (theory "HOL") true_as_term;
21.34 -val false_as_cterm = cterm_of (theory "HOL") false_as_term;
21.35 +val true_as_cterm = cterm_of (Thy_Info.get_theory "HOL") true_as_term;
21.36 +val false_as_cterm = cterm_of (Thy_Info.get_theory "HOL") false_as_term;
21.37
21.38 infixr 5 -->; (*2002 /Pure/term.ML *)
21.39 infixr --->; (*2002 /Pure/term.ML *)
21.40 @@ -1073,9 +1073,9 @@
21.41
21.42 (*version for testing local to theories*)
21.43 fun str2term_ thy str = (term_of o the o (parse thy)) str;
21.44 -fun str2term str = (term_of o the o (parse (theory "Isac"))) str;
21.45 +fun str2term str = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) str;
21.46 fun strs2terms ss = map str2term ss;
21.47 -fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str;
21.48 +fun str2termN str = (term_of o the o (parseN (Thy_Info.get_theory "Isac"))) str;
21.49
21.50 (*+ makes a substitution from the output of Pattern.match +*)
21.51 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)
21.52 @@ -1089,7 +1089,7 @@
21.53 fun inst_bdv [] t = t : term
21.54 | inst_bdv (instl: (term*term) list) t =
21.55 let fun subst (v as Var((s,_),T)) =
21.56 - (case explode s of
21.57 + (case Symbol.explode s of
21.58 "b"::"d"::"v"::_ =>
21.59 if_none (assoc(instl,Free(s,T))) (Free(s,T))
21.60 | _ => v)
22.1 --- a/src/Tools/isac/Test_Isac.thy Tue Jan 11 15:28:03 2011 +0100
22.2 +++ b/src/Tools/isac/Test_Isac.thy Mon Feb 21 19:40:36 2011 +0100
22.3 @@ -125,7 +125,7 @@
22.4 use"algein.sml";
22.5 *)
22.6 ML {*
22.7 -theory "Isac"
22.8 +Thy_Info.get_theory "Isac"
22.9 *}
22.10 use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)
22.11
22.12 @@ -139,7 +139,7 @@
22.13 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
22.14 :
22.15 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
22.16 -*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
22.17 +*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language"
22.18
22.19 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
22.20 *)
23.1 --- a/src/Tools/isac/Test_Some.thy Tue Jan 11 15:28:03 2011 +0100
23.2 +++ b/src/Tools/isac/Test_Some.thy Mon Feb 21 19:40:36 2011 +0100
23.3 @@ -13,7 +13,7 @@
23.4
23.5 ML {*
23.6 fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
23.7 -(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t;
23.8 +(ProofContext.init_global (Thy_Info.get_Thy_Info.get_theory "Rational"))) t;
23.9 (*..............................................########......................*)
23.10 *}
23.11
24.1 --- a/src/Tools/isac/calcelems.sml Tue Jan 11 15:28:03 2011 +0100
24.2 +++ b/src/Tools/isac/calcelems.sml Mon Feb 21 19:40:36 2011 +0100
24.3 @@ -20,15 +20,15 @@
24.4 type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
24.5 type thm'' = thmID * term;
24.6 type rls' = string;
24.7 -(*.a 'guh'='globally unique handle' is a string unique for each element
24.8 +(*.a 'guh'='globally unique handle' is a string unique for each element
24.9 of isac's KEStore and persistent over time
24.10 (in particular under shifts within the respective hierarchy);
24.11 - specialty for thys:
24.12 + specialty for thys:
24.13 # guh NOT resistant agains shifts from one thy to another
24.14 (which is the price for Isabelle's design: thy's overwrite ids of subthy's)
24.15 # requirement for matchTheory: induce guh from tac + current thy
24.16 (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
24.17 - TODO: introduce to pbl, met.*)
24.18 + TODO: introduce to pbl, met.*)
24.19 type guh = string;
24.20 val e_guh = "e_guh":guh;
24.21
24.22 @@ -59,20 +59,20 @@
24.23 val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
24.24
24.25
24.26 -datatype rule =
24.27 +datatype rule =
24.28 Erule (*.the empty rule .*)
24.29 -| Thm of (string * thm)(*.a theorem, ie (identifier, Thm.thm).*)
24.30 +| Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*)
24.31 | Calc of string * (*.sml-code manipulating a (sub)term .*)
24.32 (string -> term -> theory -> (string * term) option)
24.33 | Cal1 of string * (*.sml-code applied only to whole term
24.34 or left/right-hand-side of eqality .*)
24.35 (string -> term -> theory -> (string * term) option)
24.36 | Rls_ of rls (*.ie. rule sets may be nested.*)
24.37 -and scr =
24.38 - EmptyScr
24.39 +and scr =
24.40 + EmptyScr
24.41 | Script of term (*for met*)
24.42 - | Rfuns of {init_state : term ->
24.43 - (term * (*the current formula:
24.44 + | Rfuns of {init_state : term ->
24.45 + (term * (*the current formula:
24.46 goes locate_gen -> next_tac via istate*)
24.47 term * (*the final formula*)
24.48 rule list (*of reverse rewrite set (#1#)*)
24.49 @@ -81,18 +81,19 @@
24.50 (term * (*... rewrite with ...*)
24.51 term list)) (*... assumptions*)
24.52 list), (*derivation from given term to normalform
24.53 - in reverse order with sym_thm;
24.54 + in reverse order with sym_thm;
24.55 (#1#) could be extracted from here #1*)
24.56
24.57 normal_form: term -> (term * term list) option,
24.58 - locate_rule: rule list list -> term -> rule
24.59 + locate_rule: rule list list -> term -> rule
24.60 -> (rule * (term * term list)) list,
24.61 next_rule : rule list list -> term -> rule option,
24.62 - attach_form: rule list list -> term -> term
24.63 + attach_form: rule list list -> term -> term
24.64 -> (rule * (term * term list)) list}
24.65 +
24.66 and rls =
24.67 Erls (*for init e_rls*)
24.68 -
24.69 +
24.70 | Rls of (*a confluent and terminating ruleset, in general *)
24.71 {id : string, (*for trace_rewrite:=true *)
24.72 preconds : term list, (*unused WN020820 *)
24.73 @@ -112,16 +113,16 @@
24.74 rew_ord : rew_ord, (*for rules *)
24.75 erls : rls, (*for the conditions in rules *)
24.76 srls : rls, (*for evaluation of list_fns in script *)
24.77 - calc : calc list, (*for Calculate in scr, set by prep_rls *)
24.78 + calc : calc list, (*for Calculate in scr, set by prep_rls *)
24.79 rules : rule list,
24.80 scr : scr} (*Script term (how to restrict type ???)*)
24.81 (*Rrls call SML-code and simulate an rls
24.82 difference: there is always _ONE_ redex rewritten in 1 call,
24.83 thus wrap Rrls by: Rls (Rls_ ...)*)
24.84 -
24.85 +
24.86 | Rrls of (* for 'reverse rewriting' by SML-functions instead Script *)
24.87 {id : string, (* for trace_rewrite := true *)
24.88 - prepat : (term list *(* preconds, eval with subst from pattern;
24.89 + prepat : (term list *(* preconds, eval with subst from pattern;
24.90 if [HOLogic.true_const], match decides alone *)
24.91 term ) (* pattern matched with current (sub)term *)
24.92 list, (* meta-conjunction is or *)
24.93 @@ -132,18 +133,17 @@
24.94 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
24.95 from rls, and then contain both Script _AND_ Rfuns !!!*)
24.96
24.97 -fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*)
24.98 +fun thy2ctxt' thy' = ProofContext.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
24.99 fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*)
24.100
24.101 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
24.102 -(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
24.103 +(*val ctxt_HOL = ProofContext.init_global (Thy_Info.get_theory "Complex_Main");*)
24.104 (*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
24.105 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
24.106 (*fun ctxt_Isac _ = thy2ctxt' "Isac";*)
24.107 fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
24.108
24.109 -val e_rule =
24.110 - Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
24.111 +val e_rule = Thm ("refl", @{thm refl});
24.112 fun id_of_thm (Thm (id, _)) = id
24.113 | id_of_thm _ = error "id_of_thm";
24.114 fun thm_of_thm (Thm (_, thm)) = thm
24.115 @@ -164,8 +164,8 @@
24.116 (*check for [.] as caused by "fun assoc_thm'"*)
24.117 fun string_of_thmI thm =
24.118 let val ct' = (de_quote o string_of_thm) thm
24.119 - val (a, b) = split_nlast (5, explode ct')
24.120 - in case b of
24.121 + val (a, b) = split_nlast (5, Symbol.explode ct')
24.122 + in case b of
24.123 [" ", " ","[", ".", "]"] => implode a
24.124 | _ => ct'
24.125 end;
24.126 @@ -204,7 +204,7 @@
24.127
24.128
24.129 type rrlsstate = (*state for reverse rewriting*)
24.130 - (term * (*the current formula:
24.131 + (term * (*the current formula:
24.132 goes locate_gen -> next_tac via istate*)
24.133 term * (*the final formula*)
24.134 rule list (*of reverse rewrite set (#1#)*)
24.135 @@ -213,7 +213,7 @@
24.136 (term * (*... rewrite with ...*)
24.137 term list)) (*... assumptions*)
24.138 list); (*derivation from given term to normalform
24.139 - in reverse order with sym_thm;
24.140 + in reverse order with sym_thm;
24.141 (#1#) could be extracted from here #1*)
24.142 val e_type = Type("empty",[]);
24.143 val a_type = TFree("'a",[]);
24.144 @@ -246,14 +246,14 @@
24.145 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
24.146 val theory2theory' = string_of_thy;
24.147 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
24.148 -val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;
24.149 -(*> theory2str' (theory "Isac");
24.150 +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
24.151 +(*> theory2str' (Thy_Info.get_theory "Isac");
24.152 al it = "Isac" : string
24.153 *)
24.154
24.155 fun thyID2theory' (thyID:thyID) = thyID;
24.156 (*
24.157 - let val ss = explode thyID
24.158 + let val ss = Symbol.explode thyID
24.159 val ext = implode (takelast (4, ss))
24.160 in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
24.161 else thyID ^ ".thy"
24.162 @@ -267,7 +267,7 @@
24.163
24.164 fun theory'2thyID (theory':theory') = theory';
24.165 (*
24.166 - let val ss = explode theory'
24.167 + let val ss = Symbol.explode theory'
24.168 val ext = implode (takelast (4, ss))
24.169 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
24.170 else theory' (*disarm abuse of theory'*)
24.171 @@ -287,25 +287,25 @@
24.172
24.173 eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
24.174 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
24.175 - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
24.176 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
24.177 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
24.178 (see match_ags).
24.179
24.180 Preliminary solution:
24.181 # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
24.182 # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
24.183 - # however, a thy specified by the user in the rootpbl may lead to
24.184 - errors in far-off subpbls (which are not yet reported properly !!!)
24.185 + # however, a thy specified by the user in the rootpbl may lead to
24.186 + errors in far-off subpbls (which are not yet reported properly !!!)
24.187 and interactively specifiying thys in subpbl is not very relevant.
24.188
24.189 Other solutions possible:
24.190 - # always parse and type-check with theory "Isac"
24.191 + # always parse and type-check with Thy_Info.get_theory "Isac"
24.192 (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
24.193 # regard the subthy-relation in specifying thys of subpbls
24.194 # specifically handle 'SubProblem (undefined, pbl, arglist)'
24.195 # ???
24.196 .*)
24.197 -(*WN0509 TODO "ProtoPure" ... would be more consistent
24.198 +(*WN0509 TODO "ProtoPure" ... would be more consistent
24.199 with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
24.200 val e_domID = "e_domID":domID;
24.201
24.202 @@ -336,18 +336,18 @@
24.203 (*for distinction of contexts*)
24.204 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
24.205 fun ketype2str Exp_ = "Exp_"
24.206 - | ketype2str Thy_ = "Thy_"
24.207 - | ketype2str Pbl_ = "Pbl_"
24.208 + | ketype2str Thy_ = "Thy_"
24.209 + | ketype2str Pbl_ = "Pbl_"
24.210 | ketype2str Met_ = "Met_";
24.211 fun ketype2str' Exp_ = "Example"
24.212 - | ketype2str' Thy_ = "Theory"
24.213 - | ketype2str' Pbl_ = "Problem"
24.214 + | ketype2str' Thy_ = "Theory"
24.215 + | ketype2str' Pbl_ = "Problem"
24.216 | ketype2str' Met_ = "Method";
24.217
24.218 (*see 'How to manage theorys in subproblems' at 'type thyID'*)
24.219 val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
24.220
24.221 -(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
24.222 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
24.223 in order to distinguish them from general IsacKnowledge defined later on.*)
24.224 val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
24.225
24.226 @@ -379,7 +379,7 @@
24.227
24.228 (*.'a is for pbt | met.*)
24.229 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
24.230 -datatype 'a ptyp =
24.231 +datatype 'a ptyp =
24.232 Ptyp of string * (*element within pblID*)
24.233 'a list * (*several pbts with different domIDs/thy
24.234 TODO: select by subthy (isaref.p.69)
24.235 @@ -416,7 +416,7 @@
24.236 type thehier = (thydata ptyp) list;
24.237 val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
24.238
24.239 -(* an association list, gets the value once in Isac.ML.
24.240 +(* an association list, gets the value once in Isac.ML.
24.241 stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
24.242 WN1-1-28 make this data arguments and del ref ?*)
24.243 val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
24.244 @@ -437,9 +437,9 @@
24.245 next_rule=ne,attach_form=fo};
24.246 end;
24.247
24.248 -val e_rls =
24.249 +val e_rls =
24.250 Rls{id = "e_rls",
24.251 - preconds = [],
24.252 + preconds = [],
24.253 rew_ord = ("dummy_ord", dummy_ord),
24.254 erls = Erls,srls = Erls,
24.255 calc = [],
24.256 @@ -464,20 +464,20 @@
24.257 | rep_rls Erls = rep_rls e_rls
24.258 | rep_rls (Rrls {id,...}) = rep_rls e_rls
24.259 (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
24.260 -(*| rep_rls (Seq {id,...}) =
24.261 +(*| rep_rls (Seq {id,...}) =
24.262 error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
24.263 --1.7.03*)
24.264 -fun rep_rrls
24.265 - (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
24.266 +fun rep_rrls
24.267 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
24.268 scr=Rfuns
24.269 {attach_form,init_state,locate_rule,
24.270 next_rule,normal_form}}) =
24.271 - {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
24.272 - rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
24.273 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
24.274 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
24.275 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
24.276 - | rep_rrls (Rls {id,...}) =
24.277 + | rep_rrls (Rls {id,...}) =
24.278 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
24.279 - | rep_rrls (Seq {id,...}) =
24.280 + | rep_rrls (Seq {id,...}) =
24.281 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
24.282
24.283 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.284 @@ -488,7 +488,7 @@
24.285 rules =rs,scr=sc}) r =
24.286 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.287 rules = rs @ r,scr=sc}:rls)
24.288 - | append_rls id (Rrls _) _ =
24.289 + | append_rls id (Rrls _) _ =
24.290 error ("append_rls: not for reverse-rewrite-rule-set "^id);
24.291
24.292 (*. are _atomic_ rules equal ?.*)
24.293 @@ -503,12 +503,12 @@
24.294 | merge_rls _ rls Erls = rls
24.295 | merge_rls id
24.296 (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
24.297 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.298 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.299 (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
24.300 (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
24.301 (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
24.302 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
24.303 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.304 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.305 ((#srls o rep_rls) r2),
24.306 calc=ca1 @ ((#calc o rep_rls) r2),
24.307 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
24.308 @@ -516,18 +516,18 @@
24.309 scr=sc1}:rls)
24.310 | merge_rls id
24.311 (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
24.312 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.313 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.314 (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
24.315 (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
24.316 (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
24.317 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
24.318 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.319 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.320 ((#srls o rep_rls) r2),
24.321 calc=ca1 @ ((#calc o rep_rls) r2),
24.322 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
24.323 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
24.324 scr=sc1}:rls)
24.325 - | merge_rls _ _ _ =
24.326 + | merge_rls _ _ _ =
24.327 error "merge_rls: not for reverse-rewrite-rule-sets\
24.328 \and not for mixed Rls -- Seq";
24.329 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.330 @@ -540,21 +540,21 @@
24.331 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.332 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
24.333 scr=sc}:rls)
24.334 - | remove_rls id (Rrls _) _ = error
24.335 + | remove_rls id (Rrls _) _ = error
24.336 ("remove_rls: not for reverse-rewrite-rule-set "^id);
24.337
24.338 (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
24.339 val it = [1, 2] : int list*)
24.340
24.341 (*elder version: migrated 3 calls in smtest to memrls
24.342 -fun mem_rls id rls =
24.343 +fun mem_rls id rls =
24.344 case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
24.345 SOME _ => true | NONE => false;*)
24.346 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
24.347 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
24.348 | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
24.349 fun rls_get_thm rls (id: xstring) =
24.350 - case find_first (curry eq_rule e_rule)
24.351 + case find_first (curry eq_rule e_rule)
24.352 ((#rules o rep_rls) rls) of
24.353 SOME thm => SOME thm | NONE => NONE;
24.354
24.355 @@ -565,10 +565,10 @@
24.356 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
24.357 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
24.358 fun assoc_thy (thy:theory') =
24.359 - if thy = "e_domID" then (theory "Script") (*lower bound of Knowledge*)
24.360 - else (theory thy)
24.361 + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
24.362 + else (Thy_Info.get_theory thy)
24.363 handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
24.364 -
24.365 +
24.366 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
24.367 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
24.368 overlays by re-using an identifier in different thys.*)
24.369 @@ -581,7 +581,7 @@
24.370 in order to create the thy_hierarchy;
24.371 overwrites existing rls' even if they are defined in a different thy;
24.372 this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
24.373 -(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
24.374 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
24.375 they do NOT handle overlays by re-using an identifier in different thys;
24.376 "thyID.rlsID" would be a good solution, if the "." would be possible
24.377 in scripts...
24.378 @@ -598,13 +598,13 @@
24.379 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
24.380 if key = keyi then calc else assoc_calc (pairs, key);
24.381 (*only used for !calclist'...*)
24.382 -fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
24.383 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
24.384 ^"' not found")
24.385 | assoc1 ((all as (keyi, _)) :: pairs, key) =
24.386 if key = keyi then all else assoc1 (pairs, key);
24.387
24.388 (*TODO.WN080102 clarify usage of type cal and type calc..*)
24.389 -fun calID2calcID (calID : calID) =
24.390 +fun calID2calcID (calID : calID) =
24.391 let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
24.392 | ass ((calci, (cali, eval_fn))::ids) =
24.393 if calID = cali then calci
24.394 @@ -624,19 +624,19 @@
24.395 fun termopt2str (SOME t) = "SOME " ^ term2str t
24.396 | termopt2str NONE = "NONE";
24.397
24.398 -fun type2str typ =
24.399 +fun type2str typ =
24.400 Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
24.401 val string_of_typ = type2str;
24.402
24.403 -fun subst2str (s:subst) =
24.404 - (strs2str o
24.405 +fun subst2str (s:subst) =
24.406 + (strs2str o
24.407 (map (linefeed o pair2str o
24.408 - (apsnd term2str) o
24.409 + (apsnd term2str) o
24.410 (apfst term2str)))) s;
24.411 -fun subst2str' (s:subst) =
24.412 - (strs2str' o
24.413 +fun subst2str' (s:subst) =
24.414 + (strs2str' o
24.415 (map (pair2str o
24.416 - (apsnd term2str) o
24.417 + (apsnd term2str) o
24.418 (apfst term2str)))) s;
24.419 (*> subst2str' [(str2term "bdv", str2term "x"),
24.420 (str2term "bdv_2", str2term "y")];
24.421 @@ -669,7 +669,7 @@
24.422
24.423
24.424 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
24.425 - L (*go left at $*)
24.426 + L (*go left at $*)
24.427 | R (*go right at $*)
24.428 | D; (*go down at Abs*)
24.429 type loc_ = lrd list;
24.430 @@ -681,3 +681,1089 @@
24.431 (*
24.432 end (*struct*)
24.433 *)
24.434 +
24.435 +
24.436 +
24.437 +val e_rule =
24.438 + Thm ("refl", @{thm refl});
24.439 +fun id_of_thm (Thm (id, _)) = id
24.440 + | id_of_thm _ = error "id_of_thm";
24.441 +fun thm_of_thm (Thm (_, thm)) = thm
24.442 + | thm_of_thm _ = error "thm_of_thm";
24.443 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
24.444 +
24.445 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
24.446 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
24.447 +
24.448 +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
24.449 + (strip_thy thmid1) = (strip_thy thmid2);
24.450 +(*version typed weaker WN100910*)
24.451 +fun eq_thmI' ((thmid1, _), (thmid2, _)) =
24.452 + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
24.453 +
24.454 +
24.455 +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
24.456 +(*check for [.] as caused by "fun assoc_thm'"*)
24.457 +fun string_of_thmI thm =
24.458 + let val ct' = (de_quote o string_of_thm) thm
24.459 + val (a, b) = split_nlast (5, Symbol.explode ct')
24.460 + in case b of
24.461 + [" ", " ","[", ".", "]"] => implode a
24.462 + | _ => ct'
24.463 + end;
24.464 +
24.465 +(*.id requested for all, Rls,Seq,Rrls.*)
24.466 +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
24.467 + | id_rls (Rls {id,...}) = id
24.468 + | id_rls (Seq {id,...}) = id
24.469 + | id_rls (Rrls {id,...}) = id;
24.470 +val rls2str = id_rls;
24.471 +fun id_rule (Thm (id, _)) = id
24.472 + | id_rule (Calc (id, _)) = id
24.473 + | id_rule (Rls_ rls) = id_rls rls;
24.474 +
24.475 +fun get_rules (Rls {rules,...}) = rules
24.476 + | get_rules (Seq {rules,...}) = rules
24.477 + | get_rules (Rrls _) = [];
24.478 +
24.479 +fun rule2str Erule = "Erule"
24.480 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
24.481 + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
24.482 + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
24.483 + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
24.484 +fun rule2str' Erule = "Erule"
24.485 + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
24.486 + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
24.487 + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
24.488 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
24.489 +
24.490 +(*WN080102 compare eq_rule ?!?*)
24.491 +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
24.492 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
24.493 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
24.494 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
24.495 + | eqrule _ = false;
24.496 +
24.497 +
24.498 +type rrlsstate = (*state for reverse rewriting*)
24.499 + (term * (*the current formula:
24.500 + goes locate_gen -> next_tac via istate*)
24.501 + term * (*the final formula*)
24.502 + rule list (*of reverse rewrite set (#1#)*)
24.503 + list * (*may be serveral, eg. in norm_rational*)
24.504 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
24.505 + (term * (*... rewrite with ...*)
24.506 + term list)) (*... assumptions*)
24.507 + list); (*derivation from given term to normalform
24.508 + in reverse order with sym_thm;
24.509 + (#1#) could be extracted from here #1*)
24.510 +val e_type = Type("empty",[]);
24.511 +val a_type = TFree("'a",[]);
24.512 +val e_term = Const("empty",e_type);
24.513 +val a_term = Free("empty",a_type);
24.514 +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
24.515 +
24.516 +
24.517 +
24.518 +
24.519 +(*22.2.02: ging auf Linux nicht (Stefan)
24.520 +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
24.521 +val e_term = Const("empty", Type("'a", []));
24.522 +val e_scr = Script e_term;
24.523 +
24.524 +
24.525 +(*ad thm':
24.526 + there are two kinds of theorems ...
24.527 + (1) known by isabelle
24.528 + (2) not known, eg. calc_thm, instantiated rls
24.529 + the latter have a thmid "#..."
24.530 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
24.531 + and have a special assoc_thm / assoc_rls in this interface *)
24.532 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
24.533 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
24.534 +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
24.535 +
24.536 +fun string_of_thy thy = Context.theory_name thy: theory';
24.537 +val theory2domID = string_of_thy;
24.538 +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
24.539 +val theory2theory' = string_of_thy;
24.540 +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
24.541 +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
24.542 +(*> theory2str' (Thy_Info.get_theory "Isac");
24.543 +al it = "Isac" : string
24.544 +*)
24.545 +
24.546 +fun thyID2theory' (thyID:thyID) = thyID;
24.547 +(*
24.548 + let val ss = Symbol.explode thyID
24.549 + val ext = implode (takelast (4, ss))
24.550 + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
24.551 + else thyID ^ ".thy"
24.552 + end;
24.553 +*)
24.554 +(* thyID2theory' "Isac" (*ok*);
24.555 +val it = "Isac" : theory'
24.556 + > thyID2theory' "Isac" (*abuse, goes ok...*);
24.557 +val it = "Isac" : theory'
24.558 +*)
24.559 +
24.560 +fun theory'2thyID (theory':theory') = theory';
24.561 +(*
24.562 + let val ss = Symbol.explode theory'
24.563 + val ext = implode (takelast (4, ss))
24.564 + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
24.565 + else theory' (*disarm abuse of theory'*)
24.566 + end;
24.567 +*)
24.568 +(* theory'2thyID "Isac";
24.569 +val it = "Isac" : thyID
24.570 +> theory'2thyID "Isac";
24.571 +val it = "Isac" : thyID*)
24.572 +
24.573 +
24.574 +(*. WN0509 discussion:
24.575 +#############################################################################
24.576 +# How to manage theorys in subproblems wrt. the requirement, #
24.577 +# that scripts should be re-usable ? #
24.578 +#############################################################################
24.579 +
24.580 + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
24.581 + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
24.582 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
24.583 + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
24.584 + (see match_ags).
24.585 +
24.586 + Preliminary solution:
24.587 + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
24.588 + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
24.589 + # however, a thy specified by the user in the rootpbl may lead to
24.590 + errors in far-off subpbls (which are not yet reported properly !!!)
24.591 + and interactively specifiying thys in subpbl is not very relevant.
24.592 +
24.593 + Other solutions possible:
24.594 + # always parse and type-check with Thy_Info.get_theory "Isac"
24.595 + (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
24.596 + # regard the subthy-relation in specifying thys of subpbls
24.597 + # specifically handle 'SubProblem (undefined, pbl, arglist)'
24.598 + # ???
24.599 +.*)
24.600 +(*WN0509 TODO "ProtoPure" ... would be more consistent
24.601 + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
24.602 +val e_domID = "e_domID":domID;
24.603 +
24.604 +(*the key into the hierarchy ob theory elements*)
24.605 +type theID = string list;
24.606 +val e_theID = ["e_theID"];
24.607 +val theID2str = strs2str;
24.608 +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
24.609 +fun theID2thyID (theID:theID) =
24.610 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
24.611 + else error ("theID2thyID called with "^ theID2str theID);
24.612 +
24.613 +(*the key into the hierarchy ob problems*)
24.614 +type pblID = string list; (* domID::...*)
24.615 +val e_pblID = ["e_pblID"]:pblID;
24.616 +val pblID2str = strs2str;
24.617 +
24.618 +(*the key into the hierarchy ob methods*)
24.619 +type metID = string list;
24.620 +val e_metID = ["e_metID"]:metID;
24.621 +val metID2str = strs2str;
24.622 +
24.623 +(*either theID or pblID or metID*)
24.624 +type kestoreID = string list;
24.625 +val e_kestoreID = ["e_kestoreID"];
24.626 +val kestoreID2str = strs2str;
24.627 +
24.628 +(*for distinction of contexts*)
24.629 +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
24.630 +fun ketype2str Exp_ = "Exp_"
24.631 + | ketype2str Thy_ = "Thy_"
24.632 + | ketype2str Pbl_ = "Pbl_"
24.633 + | ketype2str Met_ = "Met_";
24.634 +fun ketype2str' Exp_ = "Example"
24.635 + | ketype2str' Thy_ = "Theory"
24.636 + | ketype2str' Pbl_ = "Problem"
24.637 + | ketype2str' Met_ = "Method";
24.638 +
24.639 +(*see 'How to manage theorys in subproblems' at 'type thyID'*)
24.640 +val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
24.641 +
24.642 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
24.643 + in order to distinguish them from general IsacKnowledge defined later on.*)
24.644 +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
24.645 +
24.646 +
24.647 +(*rewrite orders, also stored in 'type met' and type 'and rls'
24.648 + The association list is required for 'rewrite.."rew_ord"..'
24.649 + WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
24.650 +val rew_ord' =
24.651 + Unsynchronized.ref
24.652 + ([]:(rew_ord' * (*the key for the association list *)
24.653 + (subst (*the bound variables - they get high order*)
24.654 + -> (term * term) (*(t1, t2) to be compared *)
24.655 + -> bool)) (*if t1 <= t2 then true else false *)
24.656 + list); (*association list *)
24.657 +
24.658 +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
24.659 + ("dummy_ord", dummy_ord)]);
24.660 +
24.661 +
24.662 +(*WN060120 a hack to get alltogether run again with minimal effort:
24.663 + theory' is inserted for creating thy_hierarchy; calls for assoc_rls
24.664 + need not be called*)
24.665 +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
24.666 +
24.667 +(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
24.668 +val calclist'= Unsynchronized.ref ([]: calc list);
24.669 +
24.670 +(*.the hierarchy of thydata.*)
24.671 +
24.672 +(*.'a is for pbt | met.*)
24.673 +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
24.674 +datatype 'a ptyp =
24.675 + Ptyp of string * (*element within pblID*)
24.676 + 'a list * (*several pbts with different domIDs/thy
24.677 + TODO: select by subthy (isaref.p.69)
24.678 + presently only _ONE_ elem*)
24.679 + ('a ptyp) list; (*the children nodes*)
24.680 +
24.681 +(*.datatype for collecting thydata for hierarchy.*)
24.682 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
24.683 +(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
24.684 +datatype thydata = Html of {guh: guh,
24.685 + coursedesign: authors,
24.686 + mathauthors: authors,
24.687 + html: string} (*html; for demos before database*)
24.688 + | Hthm of {guh: guh,
24.689 + coursedesign: authors,
24.690 + mathauthors: authors,
24.691 + thm: term}
24.692 + | Hrls of {guh: guh,
24.693 + coursedesign: authors,
24.694 + mathauthors: authors,
24.695 + (*like vvvvvvvvvvvvv val ruleset'
24.696 + WN060711 redesign together !*)
24.697 + thy_rls: (thyID * rls)}
24.698 + | Hcal of {guh: guh,
24.699 + coursedesign: authors,
24.700 + mathauthors: authors,
24.701 + calc: calc}
24.702 + | Hord of {guh: guh,
24.703 + coursedesign: authors,
24.704 + mathauthors: authors,
24.705 + ord: (subst -> (term * term) -> bool)};
24.706 +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
24.707 +
24.708 +type thehier = (thydata ptyp) list;
24.709 +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
24.710 +
24.711 +(* an association list, gets the value once in Isac.ML.
24.712 + stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
24.713 + WN1-1-28 make this data arguments and del ref ?*)
24.714 +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
24.715 +
24.716 +
24.717 +type path = string;
24.718 +type filename = string;
24.719 +
24.720 +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
24.721 +local
24.722 + fun ii (_:term) = e_rrlsstate;
24.723 + fun no (_:term) = SOME (e_term,[e_term]);
24.724 + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
24.725 + fun ne (_:rule list list) (_:term) = SOME e_rule;
24.726 + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
24.727 +in
24.728 +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
24.729 + next_rule=ne,attach_form=fo};
24.730 +end;
24.731 +
24.732 +val e_rls =
24.733 + Rls{id = "e_rls",
24.734 + preconds = [],
24.735 + rew_ord = ("dummy_ord", dummy_ord),
24.736 + erls = Erls,srls = Erls,
24.737 + calc = [],
24.738 + rules = [], scr = EmptyScr}:rls;
24.739 +val e_rrls = Rrls {id = "e_rrls",
24.740 + prepat = [],
24.741 + rew_ord = ("dummy_ord", dummy_ord),
24.742 + erls = Erls,
24.743 + calc = [],
24.744 + (*asm_thm=[],*)
24.745 + scr=e_rfuns}:rls;
24.746 +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
24.747 + ("e_rrls",("Tools",e_rrls))
24.748 + ]);
24.749 +
24.750 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
24.751 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
24.752 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
24.753 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
24.754 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
24.755 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
24.756 + | rep_rls Erls = rep_rls e_rls
24.757 + | rep_rls (Rrls {id,...}) = rep_rls e_rls
24.758 + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
24.759 +(*| rep_rls (Seq {id,...}) =
24.760 + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
24.761 +--1.7.03*)
24.762 +fun rep_rrls
24.763 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
24.764 + scr=Rfuns
24.765 + {attach_form,init_state,locate_rule,
24.766 + next_rule,normal_form}}) =
24.767 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
24.768 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
24.769 + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
24.770 + | rep_rrls (Rls {id,...}) =
24.771 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
24.772 + | rep_rrls (Seq {id,...}) =
24.773 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
24.774 +
24.775 +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.776 + rules =rs,scr=sc}) r =
24.777 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.778 + rules = rs @ r,scr=sc}:rls)
24.779 + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.780 + rules =rs,scr=sc}) r =
24.781 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.782 + rules = rs @ r,scr=sc}:rls)
24.783 + | append_rls id (Rrls _) _ =
24.784 + error ("append_rls: not for reverse-rewrite-rule-set "^id);
24.785 +
24.786 +(*. are _atomic_ rules equal ?.*)
24.787 +(*WN080102 compare eqrule ?!?*)
24.788 +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
24.789 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
24.790 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
24.791 + (*id_rls checks for Rls, Seq, Rrls*)
24.792 + | eq_rule _ = false;
24.793 +
24.794 +fun merge_rls _ Erls rls = rls
24.795 + | merge_rls _ rls Erls = rls
24.796 + | merge_rls id
24.797 + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
24.798 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.799 + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
24.800 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
24.801 + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
24.802 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
24.803 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.804 + ((#srls o rep_rls) r2),
24.805 + calc=ca1 @ ((#calc o rep_rls) r2),
24.806 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
24.807 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
24.808 + scr=sc1}:rls)
24.809 + | merge_rls id
24.810 + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
24.811 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.812 + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
24.813 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
24.814 + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
24.815 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
24.816 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.817 + ((#srls o rep_rls) r2),
24.818 + calc=ca1 @ ((#calc o rep_rls) r2),
24.819 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
24.820 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
24.821 + scr=sc1}:rls)
24.822 + | merge_rls _ _ _ =
24.823 + error "merge_rls: not for reverse-rewrite-rule-sets\
24.824 + \and not for mixed Rls -- Seq";
24.825 +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.826 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
24.827 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.828 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
24.829 + scr=sc}:rls)
24.830 + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.831 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
24.832 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.833 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
24.834 + scr=sc}:rls)
24.835 + | remove_rls id (Rrls _) _ = error
24.836 + ("remove_rls: not for reverse-rewrite-rule-set "^id);
24.837 +
24.838 +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
24.839 +val it = [1, 2] : int list*)
24.840 +
24.841 +(*elder version: migrated 3 calls in smtest to memrls
24.842 +fun mem_rls id rls =
24.843 + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
24.844 + SOME _ => true | NONE => false;*)
24.845 +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
24.846 + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
24.847 + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
24.848 +fun rls_get_thm rls (id: xstring) =
24.849 + case find_first (curry eq_rule e_rule)
24.850 + ((#rules o rep_rls) rls) of
24.851 + SOME thm => SOME thm | NONE => NONE;
24.852 +
24.853 +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
24.854 + | assoc' ((keyi, xi) :: pairs, key) =
24.855 + if key = keyi then SOME xi else assoc' (pairs, key);
24.856 +
24.857 +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
24.858 + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
24.859 +fun assoc_thy (thy:theory') =
24.860 + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
24.861 + else (Thy_Info.get_theory thy)
24.862 + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
24.863 +
24.864 +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
24.865 + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
24.866 + overlays by re-using an identifier in different thys.*)
24.867 +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
24.868 + handle _ => error ("ME_Isa: '"^rls^"' not in system");
24.869 +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
24.870 + handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
24.871 +
24.872 +(*.overwrite an element in an association list and pair it with a thyID
24.873 + in order to create the thy_hierarchy;
24.874 + overwrites existing rls' even if they are defined in a different thy;
24.875 + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
24.876 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
24.877 + they do NOT handle overlays by re-using an identifier in different thys;
24.878 + "thyID.rlsID" would be a good solution, if the "." would be possible
24.879 + in scripts...
24.880 + actually a hack to get alltogether run again with minimal effort*)
24.881 +fun insthy thy' (rls', rls) = (rls', (thy', rls));
24.882 +fun overwritelthy thy (al, bl:(rls' * rls) list) =
24.883 + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
24.884 + in overwritel (al, bl') end;
24.885 +
24.886 +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
24.887 + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
24.888 +(*get the string for stac from rule*)
24.889 +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
24.890 + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
24.891 + if key = keyi then calc else assoc_calc (pairs, key);
24.892 +(*only used for !calclist'...*)
24.893 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
24.894 + ^"' not found")
24.895 + | assoc1 ((all as (keyi, _)) :: pairs, key) =
24.896 + if key = keyi then all else assoc1 (pairs, key);
24.897 +
24.898 +(*TODO.WN080102 clarify usage of type cal and type calc..*)
24.899 +fun calID2calcID (calID : calID) =
24.900 + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
24.901 + | ass ((calci, (cali, eval_fn))::ids) =
24.902 + if calID = cali then calci
24.903 + else ass ids
24.904 + in ass (!calclist') : calcID end;
24.905 +
24.906 +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
24.907 +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
24.908 +
24.909 +fun terms2str ts = (strs2str o (map term2str )) ts;
24.910 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
24.911 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
24.912 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
24.913 +fun terms2strs ts = (map term2str) ts;
24.914 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
24.915 +
24.916 +fun termopt2str (SOME t) = "SOME " ^ term2str t
24.917 + | termopt2str NONE = "NONE";
24.918 +
24.919 +fun type2str typ =
24.920 + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
24.921 +val string_of_typ = type2str;
24.922 +
24.923 +fun subst2str (s:subst) =
24.924 + (strs2str o
24.925 + (map (linefeed o pair2str o
24.926 + (apsnd term2str) o
24.927 + (apfst term2str)))) s;
24.928 +fun subst2str' (s:subst) =
24.929 + (strs2str' o
24.930 + (map (pair2str o
24.931 + (apsnd term2str) o
24.932 + (apfst term2str)))) s;
24.933 +(*> subst2str' [(str2term "bdv", str2term "x"),
24.934 + (str2term "bdv_2", str2term "y")];
24.935 +val it = "[(bdv, x)]" : string
24.936 +*)
24.937 +val env2str = subst2str;
24.938 +
24.939 +
24.940 +(*recursive defs:*)
24.941 +fun scr2str (Script s) = "Script "^(term2str s)
24.942 + | scr2str (Rfuns _) = "Rfuns";
24.943 +
24.944 +
24.945 +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
24.946 +
24.947 +
24.948 +(*.trace internal steps of isac's rewriter*)
24.949 +val trace_rewrite = Unsynchronized.ref false;
24.950 +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
24.951 +val depth = Unsynchronized.ref 99999;
24.952 +(*.no of rewrites exceeding this int -> NO rewrite.*)
24.953 +(*WN060829 still unused...*)
24.954 +val lim_rewrite = Unsynchronized.ref 99999;
24.955 +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
24.956 +val lim_deriv = Unsynchronized.ref 100;
24.957 +(*.switch for checking guhs unique before storing a pbl or met;
24.958 + set true at startup (done at begin of ROOT.ML)
24.959 + set false for editing IsacKnowledge (done at end of ROOT.ML).*)
24.960 +val check_guhs_unique = Unsynchronized.ref false;
24.961 +
24.962 +
24.963 +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
24.964 + L (*go left at $*)
24.965 + | R (*go right at $*)
24.966 + | D; (*go down at Abs*)
24.967 +type loc_ = lrd list;
24.968 +fun ldr2str L = "L"
24.969 + | ldr2str R = "R"
24.970 + | ldr2str D = "D";
24.971 +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
24.972 +
24.973 +(*
24.974 +end (*struct*)
24.975 +*)
24.976 +
24.977 +
24.978 +val e_rule =
24.979 + Thm ("refl", @{thm refl});
24.980 +fun id_of_thm (Thm (id, _)) = id
24.981 + | id_of_thm _ = error "id_of_thm";
24.982 +fun thm_of_thm (Thm (_, thm)) = thm
24.983 + | thm_of_thm _ = error "thm_of_thm";
24.984 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
24.985 +
24.986 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
24.987 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
24.988 +
24.989 +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
24.990 + (strip_thy thmid1) = (strip_thy thmid2);
24.991 +(*version typed weaker WN100910*)
24.992 +fun eq_thmI' ((thmid1, _), (thmid2, _)) =
24.993 + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
24.994 +
24.995 +
24.996 +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
24.997 +(*check for [.] as caused by "fun assoc_thm'"*)
24.998 +fun string_of_thmI thm =
24.999 + let val ct' = (de_quote o string_of_thm) thm
24.1000 + val (a, b) = split_nlast (5, Symbol.explode ct')
24.1001 + in case b of
24.1002 + [" ", " ","[", ".", "]"] => implode a
24.1003 + | _ => ct'
24.1004 + end;
24.1005 +
24.1006 +(*.id requested for all, Rls,Seq,Rrls.*)
24.1007 +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
24.1008 + | id_rls (Rls {id,...}) = id
24.1009 + | id_rls (Seq {id,...}) = id
24.1010 + | id_rls (Rrls {id,...}) = id;
24.1011 +val rls2str = id_rls;
24.1012 +fun id_rule (Thm (id, _)) = id
24.1013 + | id_rule (Calc (id, _)) = id
24.1014 + | id_rule (Rls_ rls) = id_rls rls;
24.1015 +
24.1016 +fun get_rules (Rls {rules,...}) = rules
24.1017 + | get_rules (Seq {rules,...}) = rules
24.1018 + | get_rules (Rrls _) = [];
24.1019 +
24.1020 +fun rule2str Erule = "Erule"
24.1021 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
24.1022 + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
24.1023 + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
24.1024 + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
24.1025 +fun rule2str' Erule = "Erule"
24.1026 + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
24.1027 + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
24.1028 + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
24.1029 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
24.1030 +
24.1031 +(*WN080102 compare eq_rule ?!?*)
24.1032 +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
24.1033 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
24.1034 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
24.1035 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
24.1036 + | eqrule _ = false;
24.1037 +
24.1038 +
24.1039 +type rrlsstate = (*state for reverse rewriting*)
24.1040 + (term * (*the current formula:
24.1041 + goes locate_gen -> next_tac via istate*)
24.1042 + term * (*the final formula*)
24.1043 + rule list (*of reverse rewrite set (#1#)*)
24.1044 + list * (*may be serveral, eg. in norm_rational*)
24.1045 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
24.1046 + (term * (*... rewrite with ...*)
24.1047 + term list)) (*... assumptions*)
24.1048 + list); (*derivation from given term to normalform
24.1049 + in reverse order with sym_thm;
24.1050 + (#1#) could be extracted from here #1*)
24.1051 +val e_type = Type("empty",[]);
24.1052 +val a_type = TFree("'a",[]);
24.1053 +val e_term = Const("empty",e_type);
24.1054 +val a_term = Free("empty",a_type);
24.1055 +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
24.1056 +
24.1057 +
24.1058 +
24.1059 +
24.1060 +(*22.2.02: ging auf Linux nicht (Stefan)
24.1061 +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
24.1062 +val e_term = Const("empty", Type("'a", []));
24.1063 +val e_scr = Script e_term;
24.1064 +
24.1065 +
24.1066 +(*ad thm':
24.1067 + there are two kinds of theorems ...
24.1068 + (1) known by isabelle
24.1069 + (2) not known, eg. calc_thm, instantiated rls
24.1070 + the latter have a thmid "#..."
24.1071 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
24.1072 + and have a special assoc_thm / assoc_rls in this interface *)
24.1073 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
24.1074 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
24.1075 +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
24.1076 +
24.1077 +fun string_of_thy thy = Context.theory_name thy: theory';
24.1078 +val theory2domID = string_of_thy;
24.1079 +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
24.1080 +val theory2theory' = string_of_thy;
24.1081 +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
24.1082 +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
24.1083 +(*> theory2str' (Thy_Info.get_theory "Isac");
24.1084 +al it = "Isac" : string
24.1085 +*)
24.1086 +
24.1087 +fun thyID2theory' (thyID:thyID) = thyID;
24.1088 +(*
24.1089 + let val ss = Symbol.explode thyID
24.1090 + val ext = implode (takelast (4, ss))
24.1091 + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
24.1092 + else thyID ^ ".thy"
24.1093 + end;
24.1094 +*)
24.1095 +(* thyID2theory' "Isac" (*ok*);
24.1096 +val it = "Isac" : theory'
24.1097 + > thyID2theory' "Isac" (*abuse, goes ok...*);
24.1098 +val it = "Isac" : theory'
24.1099 +*)
24.1100 +
24.1101 +fun theory'2thyID (theory':theory') = theory';
24.1102 +(*
24.1103 + let val ss = Symbol.explode theory'
24.1104 + val ext = implode (takelast (4, ss))
24.1105 + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
24.1106 + else theory' (*disarm abuse of theory'*)
24.1107 + end;
24.1108 +*)
24.1109 +(* theory'2thyID "Isac";
24.1110 +val it = "Isac" : thyID
24.1111 +> theory'2thyID "Isac";
24.1112 +val it = "Isac" : thyID*)
24.1113 +
24.1114 +
24.1115 +(*. WN0509 discussion:
24.1116 +#############################################################################
24.1117 +# How to manage theorys in subproblems wrt. the requirement, #
24.1118 +# that scripts should be re-usable ? #
24.1119 +#############################################################################
24.1120 +
24.1121 + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
24.1122 + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
24.1123 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
24.1124 + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
24.1125 + (see match_ags).
24.1126 +
24.1127 + Preliminary solution:
24.1128 + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
24.1129 + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
24.1130 + # however, a thy specified by the user in the rootpbl may lead to
24.1131 + errors in far-off subpbls (which are not yet reported properly !!!)
24.1132 + and interactively specifiying thys in subpbl is not very relevant.
24.1133 +
24.1134 + Other solutions possible:
24.1135 + # always parse and type-check with Thy_Info.get_theory "Isac"
24.1136 + (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
24.1137 + # regard the subthy-relation in specifying thys of subpbls
24.1138 + # specifically handle 'SubProblem (undefined, pbl, arglist)'
24.1139 + # ???
24.1140 +.*)
24.1141 +(*WN0509 TODO "ProtoPure" ... would be more consistent
24.1142 + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
24.1143 +val e_domID = "e_domID":domID;
24.1144 +
24.1145 +(*the key into the hierarchy ob theory elements*)
24.1146 +type theID = string list;
24.1147 +val e_theID = ["e_theID"];
24.1148 +val theID2str = strs2str;
24.1149 +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
24.1150 +fun theID2thyID (theID:theID) =
24.1151 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
24.1152 + else error ("theID2thyID called with "^ theID2str theID);
24.1153 +
24.1154 +(*the key into the hierarchy ob problems*)
24.1155 +type pblID = string list; (* domID::...*)
24.1156 +val e_pblID = ["e_pblID"]:pblID;
24.1157 +val pblID2str = strs2str;
24.1158 +
24.1159 +(*the key into the hierarchy ob methods*)
24.1160 +type metID = string list;
24.1161 +val e_metID = ["e_metID"]:metID;
24.1162 +val metID2str = strs2str;
24.1163 +
24.1164 +(*either theID or pblID or metID*)
24.1165 +type kestoreID = string list;
24.1166 +val e_kestoreID = ["e_kestoreID"];
24.1167 +val kestoreID2str = strs2str;
24.1168 +
24.1169 +(*for distinction of contexts*)
24.1170 +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
24.1171 +fun ketype2str Exp_ = "Exp_"
24.1172 + | ketype2str Thy_ = "Thy_"
24.1173 + | ketype2str Pbl_ = "Pbl_"
24.1174 + | ketype2str Met_ = "Met_";
24.1175 +fun ketype2str' Exp_ = "Example"
24.1176 + | ketype2str' Thy_ = "Theory"
24.1177 + | ketype2str' Pbl_ = "Problem"
24.1178 + | ketype2str' Met_ = "Method";
24.1179 +
24.1180 +(*see 'How to manage theorys in subproblems' at 'type thyID'*)
24.1181 +val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
24.1182 +
24.1183 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
24.1184 + in order to distinguish them from general IsacKnowledge defined later on.*)
24.1185 +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
24.1186 +
24.1187 +
24.1188 +(*rewrite orders, also stored in 'type met' and type 'and rls'
24.1189 + The association list is required for 'rewrite.."rew_ord"..'
24.1190 + WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
24.1191 +val rew_ord' =
24.1192 + Unsynchronized.ref
24.1193 + ([]:(rew_ord' * (*the key for the association list *)
24.1194 + (subst (*the bound variables - they get high order*)
24.1195 + -> (term * term) (*(t1, t2) to be compared *)
24.1196 + -> bool)) (*if t1 <= t2 then true else false *)
24.1197 + list); (*association list *)
24.1198 +
24.1199 +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
24.1200 + ("dummy_ord", dummy_ord)]);
24.1201 +
24.1202 +
24.1203 +(*WN060120 a hack to get alltogether run again with minimal effort:
24.1204 + theory' is inserted for creating thy_hierarchy; calls for assoc_rls
24.1205 + need not be called*)
24.1206 +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
24.1207 +
24.1208 +(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
24.1209 +val calclist'= Unsynchronized.ref ([]: calc list);
24.1210 +
24.1211 +(*.the hierarchy of thydata.*)
24.1212 +
24.1213 +(*.'a is for pbt | met.*)
24.1214 +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
24.1215 +datatype 'a ptyp =
24.1216 + Ptyp of string * (*element within pblID*)
24.1217 + 'a list * (*several pbts with different domIDs/thy
24.1218 + TODO: select by subthy (isaref.p.69)
24.1219 + presently only _ONE_ elem*)
24.1220 + ('a ptyp) list; (*the children nodes*)
24.1221 +
24.1222 +(*.datatype for collecting thydata for hierarchy.*)
24.1223 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
24.1224 +(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
24.1225 +datatype thydata = Html of {guh: guh,
24.1226 + coursedesign: authors,
24.1227 + mathauthors: authors,
24.1228 + html: string} (*html; for demos before database*)
24.1229 + | Hthm of {guh: guh,
24.1230 + coursedesign: authors,
24.1231 + mathauthors: authors,
24.1232 + thm: term}
24.1233 + | Hrls of {guh: guh,
24.1234 + coursedesign: authors,
24.1235 + mathauthors: authors,
24.1236 + (*like vvvvvvvvvvvvv val ruleset'
24.1237 + WN060711 redesign together !*)
24.1238 + thy_rls: (thyID * rls)}
24.1239 + | Hcal of {guh: guh,
24.1240 + coursedesign: authors,
24.1241 + mathauthors: authors,
24.1242 + calc: calc}
24.1243 + | Hord of {guh: guh,
24.1244 + coursedesign: authors,
24.1245 + mathauthors: authors,
24.1246 + ord: (subst -> (term * term) -> bool)};
24.1247 +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
24.1248 +
24.1249 +type thehier = (thydata ptyp) list;
24.1250 +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
24.1251 +
24.1252 +(* an association list, gets the value once in Isac.ML.
24.1253 + stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
24.1254 + WN1-1-28 make this data arguments and del ref ?*)
24.1255 +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
24.1256 +
24.1257 +
24.1258 +type path = string;
24.1259 +type filename = string;
24.1260 +
24.1261 +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
24.1262 +local
24.1263 + fun ii (_:term) = e_rrlsstate;
24.1264 + fun no (_:term) = SOME (e_term,[e_term]);
24.1265 + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
24.1266 + fun ne (_:rule list list) (_:term) = SOME e_rule;
24.1267 + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
24.1268 +in
24.1269 +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
24.1270 + next_rule=ne,attach_form=fo};
24.1271 +end;
24.1272 +
24.1273 +val e_rls =
24.1274 + Rls{id = "e_rls",
24.1275 + preconds = [],
24.1276 + rew_ord = ("dummy_ord", dummy_ord),
24.1277 + erls = Erls,srls = Erls,
24.1278 + calc = [],
24.1279 + rules = [], scr = EmptyScr}:rls;
24.1280 +val e_rrls = Rrls {id = "e_rrls",
24.1281 + prepat = [],
24.1282 + rew_ord = ("dummy_ord", dummy_ord),
24.1283 + erls = Erls,
24.1284 + calc = [],
24.1285 + (*asm_thm=[],*)
24.1286 + scr=e_rfuns}:rls;
24.1287 +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
24.1288 + ("e_rrls",("Tools",e_rrls))
24.1289 + ]);
24.1290 +
24.1291 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
24.1292 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
24.1293 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
24.1294 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
24.1295 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
24.1296 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
24.1297 + | rep_rls Erls = rep_rls e_rls
24.1298 + | rep_rls (Rrls {id,...}) = rep_rls e_rls
24.1299 + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
24.1300 +(*| rep_rls (Seq {id,...}) =
24.1301 + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
24.1302 +--1.7.03*)
24.1303 +fun rep_rrls
24.1304 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
24.1305 + scr=Rfuns
24.1306 + {attach_form,init_state,locate_rule,
24.1307 + next_rule,normal_form}}) =
24.1308 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
24.1309 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
24.1310 + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
24.1311 + | rep_rrls (Rls {id,...}) =
24.1312 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
24.1313 + | rep_rrls (Seq {id,...}) =
24.1314 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
24.1315 +
24.1316 +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1317 + rules =rs,scr=sc}) r =
24.1318 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1319 + rules = rs @ r,scr=sc}:rls)
24.1320 + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1321 + rules =rs,scr=sc}) r =
24.1322 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1323 + rules = rs @ r,scr=sc}:rls)
24.1324 + | append_rls id (Rrls _) _ =
24.1325 + error ("append_rls: not for reverse-rewrite-rule-set "^id);
24.1326 +
24.1327 +(*. are _atomic_ rules equal ?.*)
24.1328 +(*WN080102 compare eqrule ?!?*)
24.1329 +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
24.1330 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
24.1331 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
24.1332 + (*id_rls checks for Rls, Seq, Rrls*)
24.1333 + | eq_rule _ = false;
24.1334 +
24.1335 +fun merge_rls _ Erls rls = rls
24.1336 + | merge_rls _ rls Erls = rls
24.1337 + | merge_rls id
24.1338 + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
24.1339 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.1340 + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
24.1341 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
24.1342 + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
24.1343 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
24.1344 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.1345 + ((#srls o rep_rls) r2),
24.1346 + calc=ca1 @ ((#calc o rep_rls) r2),
24.1347 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
24.1348 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
24.1349 + scr=sc1}:rls)
24.1350 + | merge_rls id
24.1351 + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
24.1352 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
24.1353 + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
24.1354 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
24.1355 + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
24.1356 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
24.1357 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
24.1358 + ((#srls o rep_rls) r2),
24.1359 + calc=ca1 @ ((#calc o rep_rls) r2),
24.1360 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
24.1361 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
24.1362 + scr=sc1}:rls)
24.1363 + | merge_rls _ _ _ =
24.1364 + error "merge_rls: not for reverse-rewrite-rule-sets\
24.1365 + \and not for mixed Rls -- Seq";
24.1366 +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1367 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
24.1368 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1369 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
24.1370 + scr=sc}:rls)
24.1371 + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1372 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
24.1373 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
24.1374 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
24.1375 + scr=sc}:rls)
24.1376 + | remove_rls id (Rrls _) _ = error
24.1377 + ("remove_rls: not for reverse-rewrite-rule-set "^id);
24.1378 +
24.1379 +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
24.1380 +val it = [1, 2] : int list*)
24.1381 +
24.1382 +(*elder version: migrated 3 calls in smtest to memrls
24.1383 +fun mem_rls id rls =
24.1384 + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
24.1385 + SOME _ => true | NONE => false;*)
24.1386 +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
24.1387 + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
24.1388 + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
24.1389 +fun rls_get_thm rls (id: xstring) =
24.1390 + case find_first (curry eq_rule e_rule)
24.1391 + ((#rules o rep_rls) rls) of
24.1392 + SOME thm => SOME thm | NONE => NONE;
24.1393 +
24.1394 +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
24.1395 + | assoc' ((keyi, xi) :: pairs, key) =
24.1396 + if key = keyi then SOME xi else assoc' (pairs, key);
24.1397 +
24.1398 +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
24.1399 + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
24.1400 +fun assoc_thy (thy:theory') =
24.1401 + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
24.1402 + else (Thy_Info.get_theory thy)
24.1403 + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
24.1404 +
24.1405 +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
24.1406 + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
24.1407 + overlays by re-using an identifier in different thys.*)
24.1408 +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
24.1409 + handle _ => error ("ME_Isa: '"^rls^"' not in system");
24.1410 +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
24.1411 + handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
24.1412 +
24.1413 +(*.overwrite an element in an association list and pair it with a thyID
24.1414 + in order to create the thy_hierarchy;
24.1415 + overwrites existing rls' even if they are defined in a different thy;
24.1416 + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
24.1417 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
24.1418 + they do NOT handle overlays by re-using an identifier in different thys;
24.1419 + "thyID.rlsID" would be a good solution, if the "." would be possible
24.1420 + in scripts...
24.1421 + actually a hack to get alltogether run again with minimal effort*)
24.1422 +fun insthy thy' (rls', rls) = (rls', (thy', rls));
24.1423 +fun overwritelthy thy (al, bl:(rls' * rls) list) =
24.1424 + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
24.1425 + in overwritel (al, bl') end;
24.1426 +
24.1427 +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
24.1428 + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
24.1429 +(*get the string for stac from rule*)
24.1430 +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
24.1431 + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
24.1432 + if key = keyi then calc else assoc_calc (pairs, key);
24.1433 +(*only used for !calclist'...*)
24.1434 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
24.1435 + ^"' not found")
24.1436 + | assoc1 ((all as (keyi, _)) :: pairs, key) =
24.1437 + if key = keyi then all else assoc1 (pairs, key);
24.1438 +
24.1439 +(*TODO.WN080102 clarify usage of type cal and type calc..*)
24.1440 +fun calID2calcID (calID : calID) =
24.1441 + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
24.1442 + | ass ((calci, (cali, eval_fn))::ids) =
24.1443 + if calID = cali then calci
24.1444 + else ass ids
24.1445 + in ass (!calclist') : calcID end;
24.1446 +
24.1447 +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
24.1448 +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
24.1449 +
24.1450 +fun terms2str ts = (strs2str o (map term2str )) ts;
24.1451 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
24.1452 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
24.1453 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
24.1454 +fun terms2strs ts = (map term2str) ts;
24.1455 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
24.1456 +
24.1457 +fun termopt2str (SOME t) = "SOME " ^ term2str t
24.1458 + | termopt2str NONE = "NONE";
24.1459 +
24.1460 +fun type2str typ =
24.1461 + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
24.1462 +val string_of_typ = type2str;
24.1463 +
24.1464 +fun subst2str (s:subst) =
24.1465 + (strs2str o
24.1466 + (map (linefeed o pair2str o
24.1467 + (apsnd term2str) o
24.1468 + (apfst term2str)))) s;
24.1469 +fun subst2str' (s:subst) =
24.1470 + (strs2str' o
24.1471 + (map (pair2str o
24.1472 + (apsnd term2str) o
24.1473 + (apfst term2str)))) s;
24.1474 +(*> subst2str' [(str2term "bdv", str2term "x"),
24.1475 + (str2term "bdv_2", str2term "y")];
24.1476 +val it = "[(bdv, x)]" : string
24.1477 +*)
24.1478 +val env2str = subst2str;
24.1479 +
24.1480 +
24.1481 +(*recursive defs:*)
24.1482 +fun scr2str (Script s) = "Script "^(term2str s)
24.1483 + | scr2str (Rfuns _) = "Rfuns";
24.1484 +
24.1485 +
24.1486 +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
24.1487 +
24.1488 +
24.1489 +(*.trace internal steps of isac's rewriter*)
24.1490 +val trace_rewrite = Unsynchronized.ref false;
24.1491 +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
24.1492 +val depth = Unsynchronized.ref 99999;
24.1493 +(*.no of rewrites exceeding this int -> NO rewrite.*)
24.1494 +(*WN060829 still unused...*)
24.1495 +val lim_rewrite = Unsynchronized.ref 99999;
24.1496 +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
24.1497 +val lim_deriv = Unsynchronized.ref 100;
24.1498 +(*.switch for checking guhs unique before storing a pbl or met;
24.1499 + set true at startup (done at begin of ROOT.ML)
24.1500 + set false for editing IsacKnowledge (done at end of ROOT.ML).*)
24.1501 +val check_guhs_unique = Unsynchronized.ref false;
24.1502 +
24.1503 +
24.1504 +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
24.1505 + L (*go left at $*)
24.1506 + | R (*go right at $*)
24.1507 + | D; (*go down at Abs*)
24.1508 +type loc_ = lrd list;
24.1509 +fun ldr2str L = "L"
24.1510 + | ldr2str R = "R"
24.1511 + | ldr2str D = "D";
24.1512 +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
24.1513 +
24.1514 +(*
24.1515 +end (*struct*)
24.1516 +*)
24.1517 +
24.1518 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
24.1519 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
25.1 --- a/src/Tools/isac/library.sml Tue Jan 11 15:28:03 2011 +0100
25.2 +++ b/src/Tools/isac/library.sml Mon Feb 21 19:40:36 2011 +0100
25.3 @@ -174,7 +174,7 @@
25.4 let fun scan ss' [] = ss'
25.5 | scan ss' ("\""::ss) = scan ss' ss
25.6 | scan ss' (s::ss) = scan (ss' @ [s]) ss;
25.7 - in (implode o (scan []) o explode) str end;
25.8 + in (implode o (scan []) o Symbol.explode) str end;
25.9 (*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
25.10 val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)
25.11
25.12 @@ -224,13 +224,13 @@
25.13 let fun get strl [] = strl
25.14 | get strl ("."::ss) = strl
25.15 | get strl ( s ::ss) = get (strl @ [s]) ss
25.16 - in implode( get [] (explode str)) end;
25.17 + in implode( get [] (Symbol.explode str)) end;
25.18
25.19 fun strip_thy str =
25.20 let fun strip bdVar [] = implode (rev bdVar)
25.21 | strip bdVar ("."::_ ) = implode (rev bdVar)
25.22 | strip bdVar (c ::cs) = strip (bdVar @[c]) cs
25.23 - in strip [] (rev(explode str)) end;
25.24 + in strip [] (rev(Symbol.explode str)) end;
25.25
25.26 fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix)
25.27 | id_of (Free (id ,_)) = id
25.28 @@ -326,14 +326,14 @@
25.29 | if_none (SOME x) _ = x;
25.30
25.31 (* redirect tracing, following The Isabelle Cookbook *)
25.32 -(* TODO: how redirect tracing to emacs buffer again ? *)
25.33 +(* TODO: how redirect tracing to emacs buffer again ?
25.34 val strip_specials =
25.35 let
25.36 fun strip ("\^A" :: _ :: cs) = strip cs
25.37 | strip (c :: cs) = c :: strip cs
25.38 | strip [] = [];
25.39 in
25.40 - implode o strip o explode
25.41 + implode o strip o Symbol.explode
25.42 end
25.43 fun redir stream =
25.44 Output.tracing_fn := (fn s =>
25.45 @@ -341,9 +341,10 @@
25.46 TextIO.output (stream, "\n");
25.47 TextIO.flushOut stream));
25.48 fun redirect_tracing path = redir (TextIO.openOut path);
25.49 +WN110221-----*)
25.50
25.51 fun compare_strs str1 str2 =
25.52 let fun comp_char (c1, c2) =
25.53 tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^
25.54 bool2str (c1 = c2))
25.55 - in map comp_char ((explode str1) ~~ (explode str2)) end;
25.56 + in map comp_char ((Symbol.explode str1) ~~ (Symbol.explode str2)) end;
26.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Tue Jan 11 15:28:03 2011 +0100
26.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Feb 21 19:40:36 2011 +0100
26.3 @@ -628,7 +628,7 @@
26.4 fun posformheads2xml j [] = ("":xml)
26.5 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
26.6
26.7 -val e_pblterm = (term_of o the o (parse (theory "Script")))
26.8 +val e_pblterm = (term_of o the o (parse (Thy_Info.get_theory "Script")))
26.9 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
26.10
26.11 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
26.12 @@ -666,7 +666,7 @@
26.13 *)
26.14 fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
26.15 let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
26.16 - val typ' = (implode o (drop_last_n 1) o explode) typ
26.17 + val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
26.18 in indt j ^ "<KESTOREREF>\n" ^
26.19 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
26.20 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
27.1 --- a/src/Tools/isac/xmlsrc/mathml.sml Tue Jan 11 15:28:03 2011 +0100
27.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml Mon Feb 21 19:40:36 2011 +0100
27.3 @@ -24,7 +24,7 @@
27.4 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
27.5 | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
27.6 | dec (c::cs) = c::(dec cs)
27.7 - in (implode o dec o explode) str:cterm' end;
27.8 + in (implode o dec o Symbol.explode) str:cterm' end;
27.9
27.10
27.11 fun strs2xml strs = foldl (op ^) ("", strs);
28.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Jan 11 15:28:03 2011 +0100
28.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Feb 21 19:40:36 2011 +0100
28.3 @@ -108,7 +108,7 @@
28.4 str2term ("Problem (" ^
28.5 (get_thy o theory2domID) thy ^ "_, " ^
28.6 (strs2str' o rev) pblRD ^ ")");
28.7 -(* term2str (pbl2term (theory "Isac") ["equations","univariate","normalize"]);
28.8 +(* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]);
28.9 val it = "Problem (Isac, [normalize, univariate, equations])" : string
28.10 *)
28.11