# HG changeset patch # User Walther Neuper # Date 1282225316 -7200 # Node ID b65c6037eb6da8b27cfb563fc655657895a629c8 # Parent 722c19bfb6bab554de88fb4bcc7003897c4e9ad3 sed -i s/"Sign.string_of_term (sign_of thy)"/"Syntax.string_of_term (thy2ctxt thy)" diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/IsacKnowledge/Atools.ML --- a/src/Tools/isac/IsacKnowledge/Atools.ML Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/IsacKnowledge/Atools.ML Thu Aug 19 15:41:56 2010 +0200 @@ -280,12 +280,12 @@ (Const (op0,t0) $ t1 $ t2 )) thy = if t1 = t2 then SOME (mk_thmid thmid op0 - ("("^(Sign.string_of_term (sign_of thy) t1)^")") - ("("^(Sign.string_of_term (sign_of thy) t2)^")"), + ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")") + ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), Trueprop $ (mk_equality (t, true_as_term))) else SOME (mk_thmid thmid op0 - ("("^(Sign.string_of_term (sign_of thy) t1)^")") - ("("^(Sign.string_of_term (sign_of thy) t2)^")"), + ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")") + ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), Trueprop $ (mk_equality (t, false_as_term))) | eval_ident _ _ _ _ = NONE; (* TODO @@ -314,8 +314,8 @@ if t1 = t2 then ((*writeln"... eval_equal: t1 = t2 --> True";*) SOME (mk_thmid thmid op0 - ("("^(Sign.string_of_term (sign_of thy) t1)^")") - ("("^(Sign.string_of_term (sign_of thy) t2)^")"), + ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")") + ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), Trueprop $ (mk_equality (t, true_as_term))) ) else (case (is_atom t1, is_atom t2) of diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/IsacKnowledge/Rational-WN.sml --- a/src/Tools/isac/IsacKnowledge/Rational-WN.sml Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/IsacKnowledge/Rational-WN.sml Thu Aug 19 15:41:56 2010 +0200 @@ -210,7 +210,7 @@ val _ = if pairopt <> NONE then () else raise error("rewrite_set_, rewrite_ \""^ (string_of_thmI thm')^"\" \""^ - (Sign.string_of_term (sign_of thy) ct)^"\" = NONE") + (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE") in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); val ruls = (#rules o rep_rls) ruless; val (ct',asm') = rew_once ruls [] ct Noap ruls; @@ -246,7 +246,7 @@ val _ = if pairopt <> NONE then () else raise error("rewrite_set_, rewrite_ \""^ (string_of_thmI thm')^"\" \""^ - (Sign.string_of_term (sign_of thy) ct)^"\" = NONE") + (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE") in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); val ruls = (#rules o rep_rls) ruless; val (ct',asm') = rew_once ruls [] ct Noap ruls; diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/Isac_Mathengine.thy --- a/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 19 15:41:56 2010 +0200 @@ -37,9 +37,17 @@ use "ME/ptyps.sml" use "ME/generate.sml" + +ML {* +thy2ctxt; +thy2ctxt'; +SOME 111; +*} + use "ME/calchead.sml" ML {* +thy2ctxt; SOME 111; *} diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/ME/appl.sml --- a/src/Tools/isac/ME/appl.sml Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/ME/appl.sml Thu Aug 19 15:41:56 2010 +0200 @@ -105,7 +105,7 @@ | mk_set thy _ _ l _ = raise error ("check_elementwise: no set "^ - (Sign.string_of_term (sign_of thy) l)); + (Syntax.string_of_term (thy2ctxt thy) l)); (*> val consts = str2term "[x=#4]"; > val pred = str2term "Assumptions"; > val pt = union_asm pt p @@ -113,7 +113,7 @@ ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; > val p = []; > val (sss,ttt) = mk_set thy pt p consts pred; -> (Sign.string_of_term (sign_of thy) sss,Sign.string_of_term(sign_of thy) ttt); +> (Syntax.string_of_term (thy2ctxt thy) sss,Sign.string_of_term(sign_of thy) ttt); val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... val consts = str2term "UniversalList"; diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/ME/script.sml --- a/src/Tools/isac/ME/script.sml Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/ME/script.sml Thu Aug 19 15:41:56 2010 +0200 @@ -224,7 +224,7 @@ fun init_form thy (Script sc) env = (case get_stac thy sc of NONE => NONE (*raise error ("init_form: no 1st stac in "^ - (Sign.string_of_term (sign_of thy) sc))*) + (Syntax.string_of_term (thy2ctxt thy) sc))*) | SOME stac => SOME (subst_atomic env stac)) | init_form _ _ _ = raise error "init_form: no match"; @@ -301,7 +301,7 @@ (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*) fun mk_arg thy d [] = raise error ("mk_arg: no data for "^ - (Sign.string_of_term (sign_of thy) d)) + (Syntax.string_of_term (thy2ctxt thy) d)) | mk_arg thy d [t] = (case dsc_valT d of "una" => [t] @@ -310,7 +310,7 @@ r as (Const ("op =",_) $ _ $ _) => r | _ => raise error ("mk_arg: dsc-typ 'nam' applied to non-equality "^ - (Sign.string_of_term (sign_of thy) t))] + (Syntax.string_of_term (thy2ctxt thy) t))] | s => raise error ("mk_arg: not impl. for "^s)) | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts); @@ -350,7 +350,7 @@ > val mI = ("Script.thy","sqrt-equ-test"); > val PblObj{meth={ppc=itms,...},...} = get_obj I pt []; > val ts = itms2args thy mI itms; -> map (Sign.string_of_term (sign_of thy)) ts; +> map (Syntax.string_of_term (thy2ctxt thy)) ts; ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list *) @@ -420,7 +420,7 @@ (*12.1.01.*) | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ (set as Const ("Collect",_) $ Abs (_,_,pred))) = - (Check_elementwise (Sign.string_of_term (sign_of thy) pred), + (Check_elementwise (Syntax.string_of_term (thy2ctxt thy) pred), (*set*)Empty_Tac_) | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = @@ -475,7 +475,7 @@ | stac2tac_ pt thy t = raise error ("stac2tac_ TODO: no match for "^ - (Sign.string_of_term (sign_of thy) t)); + (Syntax.string_of_term (thy2ctxt thy) t)); (* > val t = (term_of o the o (parse thy)) "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)"; @@ -541,7 +541,7 @@ in (bdv, pred) end | rep_set thy _ _ set = raise error ("check_elementwise: no set "^ (*from script*) - (Sign.string_of_term (sign_of thy) set)); + (Syntax.string_of_term (thy2ctxt thy) set)); (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}"; > val p = []; > val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]), @@ -550,7 +550,7 @@ ("#0 <= #2 + x",[44])]; > val (bdv,pred) = rep_set thy pt p set; val bdv = Free ("x","RealDef.real") : term -> writeln (Sign.string_of_term (sign_of thy) pred); +> writeln (Syntax.string_of_term (thy2ctxt thy) pred); ((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & #0 <= x ^^^ #2 + #5 * x) & #0 <= #2 + x @@ -834,16 +834,16 @@ in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end (*Fehlersuche 25.4.01 (a)----- als String zusammensetzen: -ML> Sign.string_of_term (sign_of thy)f; +ML> Syntax.string_of_term (thy2ctxt thy)f; val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string -ML> Sign.string_of_term (sign_of thy)f'; +ML> Syntax.string_of_term (thy2ctxt thy)f'; val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string ML> subs; val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst > val tt = (term_of o the o (parse thy)) "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))"; > atomty tt; -ML> writeln(Sign.string_of_term (sign_of thy)tt); +ML> writeln(Syntax.string_of_term (thy2ctxt thy)tt); (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) = #0 + d_d x (x ^^^ #2 + #3 * x) diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/Scripts/Tools.sml --- a/src/Tools/isac/Scripts/Tools.sml Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/Scripts/Tools.sml Thu Aug 19 15:41:56 2010 +0200 @@ -6,7 +6,7 @@ (t as (Const(op0,t0) $ arg)) thy = let val t' = ((list2isalist HOLogic.realT) o vars) t; - val thmId = thmid^(Sign.string_of_term (sign_of thy) arg); + val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end | eval_var _ _ _ _ = raise GO_ON; (* @@ -21,14 +21,14 @@ > val (SOME(thmId,t')) = eval_var thmid op0 t; val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #)) : (string * term) option -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string *) fun eval_Length (thmid:string) (op_:string) (t as (Const(op0,t0) $ arg)) thy = let val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg; - val thmId = thmid^(Sign.string_of_term (sign_of thy) arg); + val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end | eval_Length _ _ _ _ = raise GO_ON; (* @@ -77,9 +77,9 @@ let val t' = (nth (num_of_term t1) (isalist2list t2)) handle _ => raise GO_ON; - val thmId = thmid^(Sign.string_of_term (sign_of thy) t1)^ - "_"^(Sign.string_of_term (sign_of thy) t2)^ - " = "^(Sign.string_of_term (sign_of thy) t'); + val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^ + "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^ + " = "^(Syntax.string_of_term (thy2ctxt thy) t'); in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end else raise GO_ON ) diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/Scripts/calculate.sml --- a/src/Tools/isac/Scripts/calculate.sml Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/Scripts/calculate.sml Thu Aug 19 15:41:56 2010 +0200 @@ -139,79 +139,79 @@ > val t = (term_of o the o (parse thy)) "#3 + #4"; > val eval_fn = the (assoc (!eval_list, "op +")); > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > atomty t'; > > val t = (term_of o the o (parse thy)) "(a + #3) + #4"; > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; > atomty t; > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > val it = "#3 + (#4 + a) = #7 + a" : string > > > val t = (term_of o the o (parse thy)) "#-4//#-2"; > val eval_fn = the (assoc (!eval_list, "cancel")); > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "#2^^^#3"; > eval_binop "xxx" "pow" t thy; > val eval_fn = (eval_binop "xxx") > : string -> term -> theory -> (string * term) option; > val SOME (id,t') = get_pair thy "pow" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > val eval_fn = the (assoc (!eval_list, "pow")); > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; > val eval_fn = the (assoc (!eval_list, "op *")); > val (SOME (id,t')) = get_pair thy "op *" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "#0 < #4"; > val eval_fn = the (assoc (!eval_list, "op <")); > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > val t = (term_of o the o (parse thy)) "#0 < #-4"; > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "#3 is_const"; > val eval_fn = the (assoc (!eval_list, "is'_const")); > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > val t = (term_of o the o (parse thy)) "a is_const"; > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "#6//(#8::real)"; > val eval_fn = the (assoc (!eval_list, "cancel")); > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "sqrt #12"; > val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt")); > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > val it = "sqrt #12 = #2 * sqrt #3 " : string > > val t = (term_of o the o (parse thy)) "sqrt #9"; > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]"; > val eval_fn = the (assoc (!eval_list, "Tools.Nth")); > val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t; -> Sign.string_of_term (sign_of thy) t'; +> Syntax.string_of_term (thy2ctxt thy) t'; *) (* val ((op_, eval_fn),ct)=(cc,pre); diff -r 722c19bfb6ba -r b65c6037eb6d src/Tools/isac/Scripts/rewrite.sml --- a/src/Tools/isac/Scripts/rewrite.sml Thu Aug 19 15:36:02 2010 +0200 +++ b/src/Tools/isac/Scripts/rewrite.sml Thu Aug 19 15:41:56 2010 +0200 @@ -354,8 +354,8 @@ (* for test-printouts: -val _ = writeln("in rew_sub : "^( Sign.string_of_term (sign_of thy) t)) -val _ = writeln("in eval_true: prems= "^(commas (map (Sign.string_of_term (sign_of thy)) prems'))) +val _ = writeln("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t)) +val _ = writeln("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems'))) *)