# HG changeset patch # User Walther Neuper # Date 1282212522 -7200 # Node ID 862f35fdb09154a7eb708f806786771910345fe2 # Parent dfec2cf32f772d4f7e299a8c2994da147cbc4977 reduced ctxt_Isac and ctxt_HOL to fun thy2ctxt', thy2ctxt diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/ME/ctree.sml --- a/src/Tools/isac/ME/ctree.sml Thu Aug 19 12:00:46 2010 +0200 +++ b/src/Tools/isac/ME/ctree.sml Thu Aug 19 12:08:42 2010 +0200 @@ -233,10 +233,10 @@ (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*) fun subst2subs s = map (pair2str o - (apfst (Syntax.string_of_term (ctxt_Isac""))) o - (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s; -fun subst2subs' s = map ((apfst (Syntax.string_of_term (ctxt_Isac""))) o - (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s; + (apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o + (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s; +fun subst2subs' s = map ((apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o + (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s; fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s; (*> subs2subst thy ["(bdv,x)","(err,#0)"]; val it = @@ -679,8 +679,8 @@ "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*) | Rewrite_Set'(thy',pasm,rls',f,(f',asm)) => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^"," - ^(Syntax.string_of_term (ctxt_Isac"") f)^",("^(Syntax.string_of_term (ctxt_Isac"") f') - ^","^((strs2str o (map (Syntax.string_of_term (ctxt_Isac"")))) asm)^"))" + ^(Syntax.string_of_term (thy2ctxt' "Isac") f)^",("^(Syntax.string_of_term (thy2ctxt' "Isac") f') + ^","^((strs2str o (map (Syntax.string_of_term (thy2ctxt' "Isac")))) asm)^"))" | End_Detail' _ => "End_Detail' xxx" | Detail_Set' _ => "Detail_Set' xxx" @@ -724,8 +724,8 @@ "\n("^(loc_2str l)^",("^(tac_2str m)^ ",\n ens= "^(subst2str eno)^ ",\n env= "^(subst2str env)^ - ",\n iar= "^(Syntax.string_of_term (ctxt_Isac"") iar)^ - ",\n res= "^(Syntax.string_of_term (ctxt_Isac"") res)^ + ",\n iar= "^(Syntax.string_of_term (thy2ctxt' "Isac") iar)^ + ",\n res= "^(Syntax.string_of_term (thy2ctxt' "Isac") res)^ ",\n "^(safe2str s)^"))"; fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets; @@ -852,16 +852,16 @@ (* show hd origin or form only *) fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) = ((pr_pos p) ^ " ----- pblobj -----\n") -(* ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^ - (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^ +(* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^ + (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^ "\n") *) | pr_short p (PrfObj {form = form,...}) = ((pr_pos p) ^ (term2str form) ^ "\n"); (* fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) = ((ints2str c) ^" "^ - ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^ - (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^ + ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^ + (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^ "\n") | pr_cell p (PrfObj {cell = c, form = form,...}) = ((ints2str c) ^" "^ (term2str form) ^ "\n"); diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/ME/mstools.sml --- a/src/Tools/isac/ME/mstools.sml Thu Aug 19 12:00:46 2010 +0200 +++ b/src/Tools/isac/ME/mstools.sml Thu Aug 19 12:08:42 2010 +0200 @@ -643,7 +643,7 @@ | [t] => (case t of (*eg. eps=#0*) (Const ("op =",_) $ l $ r) => [r,l] | _ => raise error ("pbl_ids' Tools.nam: no equality " - ^(Syntax.string_of_term (ctxt_Isac"")t))) + ^(Syntax.string_of_term (thy2ctxt' "Isac")t))) | vs' => vs (*14.9.01: ???TODO *)) | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/ME/ptyps.sml --- a/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:00:46 2010 +0200 +++ b/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:08:42 2010 +0200 @@ -15,16 +15,16 @@ (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) fun itm_2item thy (Cor ((d,ts),_)) = - Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) + Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) | itm_2item _ (Syn c) = SyntaxE c | itm_2item _ (Typ c) = TypeE c | itm_2item thy (Inc ((d,ts),_)) = - Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) + Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) | itm_2item thy (Sup (d,ts)) = - Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) + Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) | itm_2item _ (Mis (d,pid)) = - Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^ - Syntax.string_of_term (ctxt_Isac"") pid); + Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ + Syntax.string_of_term (thy2ctxt' "Isac") pid); (* --- 8.3.00 @@ -99,7 +99,7 @@ else (e_term, [t]) (*??? 9.01 just copied*) end) handle _ => raise error ("split_dsc: called with "^ - (Syntax.string_of_term (ctxt_Isac"") t)); + (Syntax.string_of_term (thy2ctxt' "Isac") t)); (* > val t1 = (term_of o the o (parse thy)) "errorBound err_"; > split_dsc t1; @@ -134,14 +134,14 @@ (*create output-string for itm_*) -fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) | itm_out thy (Syn c) = c | itm_out thy (Typ c) = c - | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) - | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) + | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) + | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) | itm_out thy (Mis (d,pid)) = - Syntax.string_of_term (ctxt_Isac"") d ^" "^ - Syntax.string_of_term (ctxt_Isac"") pid; + Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ + Syntax.string_of_term (thy2ctxt' "Isac") pid; (*22.11.00 unused fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) @@ -163,15 +163,15 @@ *) (*--3.3.00 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = - Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) + Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) | itm2item (_,_,_,_,Syn (c)) = SyntaxE c | itm2item (_,_,_,_,Typ (c)) = TypeE c | itm2item (_,_,_,_,Fal (d,ts)) = - False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) + False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) | itm2item (_,_,_,_,Inc (d,ts)) = - Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) + Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) | itm2item (_,_,_,_,Sup (d,ts)) = - Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))); + Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))); *) fun boolterm2item (true, term) = Correct (term2str term) @@ -199,7 +199,7 @@ then ("#Relate",d,ts) else ("#undef",d,ts); (* 28.1.00 raise error ("add_field: '"^ - (Syntax.string_of_term (ctxt_Isac"") d)^ + (Syntax.string_of_term (thy2ctxt' "Isac") d)^ "' not in ppc-description "); *) ------9.3. *) @@ -211,7 +211,7 @@ [(fi,(dsc,_))] => (fi,d,ts) | [] => ("#undef",d,ts) (*may come with met.ppc*) | _ => raise error ("add_field: "^ - (Syntax.string_of_term (ctxt_Isac"") d)^ + (Syntax.string_of_term (thy2ctxt' "Isac") d)^ " more than once in pbt") end; @@ -226,10 +226,10 @@ [(fi,(dsc,_))] => [(i,v,fi,d,ts)] | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) (*raise error ("add_field': "^ - (Syntax.string_of_term (ctxt_Isac"") d)^ + (Syntax.string_of_term (thy2ctxt' "Isac") d)^ " not in met"*) | _ => raise error ("add_field': "^ - (Syntax.string_of_term (ctxt_Isac"") d)^ + (Syntax.string_of_term (thy2ctxt' "Isac") d)^ " more than once in met"); in (flat ((map (repl mpc)) ori)):ori list end; diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/Scripts/term_G.sml --- a/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 12:00:46 2010 +0200 +++ b/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 12:08:42 2010 +0200 @@ -714,7 +714,7 @@ fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm : val it = fn : Theory.theory -> xstring -> Thm.thm*) Thm (xstring, - num_str (ProofContext.get_thm (ctxt_Isac"") xstring)); + num_str (ProofContext.get_thm (thy2ctxt' "Isac") xstring)); (** get types of Free and Abs for parse' **) (*11.1.00: not used, fix-typed +,*,-,^ instead *) diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Thu Aug 19 12:00:46 2010 +0200 +++ b/src/Tools/isac/calcelems.sml Thu Aug 19 12:08:42 2010 +0200 @@ -136,12 +136,13 @@ (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) -val ctxt_HOL = thy2ctxt' "Complex_Main"; +(*val ctxt_HOL = thy2ctxt' "Complex_Main";*) (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) -fun ctxt_Isac _ = thy2ctxt' "Isac"; -fun Isac _ = ProofContext.theory_of (ctxt_Isac""); +(*fun ctxt_Isac _ = thy2ctxt' "Isac";*) +fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac"); -val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" ); +val e_rule = + Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" ); fun id_of_thm (Thm (id, _)) = id | id_of_thm _ = raise error "id_of_thm"; fun thm_of_thm (Thm (_, thm)) = thm @@ -599,13 +600,13 @@ "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t) | termopt2str NONE = "NONE";*) fun termopt2str (SOME t) = - "SOME " ^ (Syntax.string_of_term (ctxt_Isac"") t) + "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t) | termopt2str NONE = "NONE"; -fun term2str t = Syntax.string_of_term (ctxt_Isac"") t; +fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; fun terms2str ts= (strs2str o (map (Syntax.string_of_term - (ctxt_Isac"")))) ts; + (thy2ctxt' "Isac")))) ts; (*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*) -fun type2str typ = Syntax.string_of_typ (ctxt_Isac"") typ; +fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; val string_of_typ = type2str; fun subst2str (s:subst) =