1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sat Feb 04 16:49:08 2023 +0100
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sat Feb 04 17:00:25 2023 +0100
1.3 @@ -104,11 +104,11 @@
1.4 then
1.5 let
1.6 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.7 - in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.8 + in SOME (UnparseC.term ctxt prop, prop) end
1.9 else
1.10 let
1.11 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
1.12 - in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.13 + in SOME (UnparseC.term ctxt prop, prop) end
1.14 | eval_matches _ _ _ _ = NONE;
1.15
1.16 (*.does a pattern match some subterm ?.*)
1.17 @@ -131,10 +131,10 @@
1.18 if matchsub (Proof_Context.theory_of ctxt) tst pat
1.19 then
1.20 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.21 - in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.22 + in SOME (UnparseC.term ctxt prop, prop) end
1.23 else
1.24 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
1.25 - in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
1.26 + in SOME (UnparseC.term ctxt prop, prop) end
1.27 | eval_matchsub _ _ _ _ = NONE;
1.28
1.29 (*get the variables in an isabelle-term*)
1.30 @@ -142,21 +142,21 @@
1.31 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt =
1.32 let
1.33 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
1.34 - val thmId = thmid ^ UnparseC.term_in_ctxt ctxt arg;
1.35 + val thmId = thmid ^ UnparseC.term ctxt arg;
1.36 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
1.37 | eval_var _ _ _ _ = NONE;
1.38
1.39 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
1.40 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
1.41 - SOME ((UnparseC.term_in_ctxt @{context} t) ^ " = " ^ (UnparseC.term_in_ctxt @{context} l),
1.42 + SOME ((UnparseC.term @{context} t) ^ " = " ^ (UnparseC.term @{context} l),
1.43 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
1.44 | eval_lhs _ _ _ _ = NONE;
1.45
1.46 fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
1.47 - | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term_in_ctxt @{context} t ^ ")");
1.48 + | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term @{context} t ^ ")");
1.49 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
1.50 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =
1.51 - SOME (UnparseC.term_in_ctxt @{context} t ^ " = " ^ UnparseC.term_in_ctxt @{context} r,
1.52 + SOME (UnparseC.term @{context} t ^ " = " ^ UnparseC.term @{context} r,
1.53 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
1.54 | eval_rhs _ _ _ _ = NONE;
1.55
1.56 @@ -164,12 +164,12 @@
1.57 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
1.58 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
1.59 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
1.60 - ((*tracing("#>@ eval_occurs_in: v= " ^ UnparseC.term_in_ctxt @{context} v);
1.61 - tracing("#>@ eval_occurs_in: t= " ^ UnparseC.term_in_ctxt @{context} t);*)
1.62 + ((*tracing("#>@ eval_occurs_in: v= " ^ UnparseC.term @{context} v);
1.63 + tracing("#>@ eval_occurs_in: t= " ^ UnparseC.term @{context} t);*)
1.64 if occurs_in v t
1.65 - then SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True",
1.66 + then SOME ((UnparseC.term @{context} p) ^ " = True",
1.67 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.68 - else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
1.69 + else SOME ((UnparseC.term @{context} p) ^ " = False",
1.70 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
1.71 | eval_occurs_in _ _ _ _ = NONE;
1.72
1.73 @@ -183,9 +183,9 @@
1.74 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
1.75 (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =
1.76 if some_occur_in (TermC.isalist2list vs) t
1.77 - then SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True",
1.78 + then SOME ((UnparseC.term @{context} p) ^ " = True",
1.79 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.80 - else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
1.81 + else SOME ((UnparseC.term @{context} p) ^ " = False",
1.82 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.83 | eval_some_occur_in _ _ _ _ = NONE;
1.84
1.85 @@ -270,11 +270,11 @@
1.86 ----------- thus needs Rule.Eval !
1.87 > val t = TermC.parse_test @{context} "0 = 0";
1.88 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
1.89 -> UnparseC.term_in_ctxt @{context} t';
1.90 +> UnparseC.term @{context} t';
1.91 val it = \<^const_name>\<open>True\<close>
1.92
1.93 val t = TermC.parse_test @{context} "Not (x = 0)";
1.94 -atomt t; UnparseC.term_in_ctxt @{context} t;
1.95 +atomt t; UnparseC.term @{context} t;
1.96 *** -------------
1.97 *** Const ( Not)
1.98 *** . Const ( op =)
1.99 @@ -289,28 +289,28 @@
1.100 (Const _(*op0, t0*) $ t1 $ t2 )) ctxt =
1.101 if t1 = t2
1.102 then SOME (TermC.mk_thmid thmid
1.103 - ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")")
1.104 - ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"),
1.105 + ("(" ^ (UnparseC.term ctxt t1) ^ ")")
1.106 + ("(" ^ (UnparseC.term ctxt t2) ^ ")"),
1.107 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.108 else SOME (TermC.mk_thmid thmid
1.109 - ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")")
1.110 - ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"),
1.111 + ("(" ^ (UnparseC.term ctxt t1) ^ ")")
1.112 + ("(" ^ (UnparseC.term ctxt t2) ^ ")"),
1.113 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.114 | eval_ident _ _ _ _ = NONE;
1.115 (* TODO
1.116 > val t = TermC.parse_test @{context} "x =!= 0";
1.117 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.118 -> UnparseC.term_in_ctxt @{context} t';
1.119 +> UnparseC.term @{context} t';
1.120 val str = "ident_(x)_(0)" : string
1.121 val it = "(x =!= 0) = False" : string
1.122 > val t = TermC.parse_test @{context} "1 =!= 0";
1.123 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.124 -> UnparseC.term_in_ctxt @{context} t';
1.125 +> UnparseC.term @{context} t';
1.126 val str = "ident_(1)_(0)" : string
1.127 val it = "(1 =!= 0) = False" : string
1.128 > val t = TermC.parse_test @{context} "0 =!= 0";
1.129 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.130 -> UnparseC.term_in_ctxt @{context} t';
1.131 +> UnparseC.term @{context} t';
1.132 val str = "ident_(0)_(0)" : string
1.133 val it = "(0 =!= 0) = True" : string
1.134 *)
1.135 @@ -323,7 +323,7 @@
1.136 if t1 = t2
1.137 then
1.138 SOME (TermC.mk_thmid thmid
1.139 - ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"),
1.140 + ("(" ^ UnparseC.term ctxt t1 ^ ")") ("(" ^ UnparseC.term ctxt t2 ^ ")"),
1.141 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.142 else
1.143 (case (TermC.is_atom t1, TermC.is_atom t2) of
1.144 @@ -331,7 +331,7 @@
1.145 if TermC.variable_constant_pair (t1, t2)
1.146 then NONE
1.147 else SOME (TermC.mk_thmid thmid
1.148 - ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"),
1.149 + ("(" ^ UnparseC.term ctxt t1 ^ ")") ("(" ^ UnparseC.term ctxt t2 ^ ")"),
1.150 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.151 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
1.152 | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.153 @@ -361,7 +361,7 @@
1.154 (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
1.155 if TermC.is_atom arg (*could be something to be simplified before*)
1.156 then
1.157 - SOME (UnparseC.term_in_ctxt @{context} t ^ " = " ^ UnparseC.term_in_ctxt @{context} arg,
1.158 + SOME (UnparseC.term @{context} t ^ " = " ^ UnparseC.term @{context} arg,
1.159 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
1.160 else NONE
1.161 | eval_argument_in _ _ _ _ = NONE;
1.162 @@ -372,9 +372,9 @@
1.163 fun eval_sameFunId _ "Prog_Expr.sameFunId"
1.164 (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) _ =
1.165 if f1 = f2
1.166 - then SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True",
1.167 + then SOME ((UnparseC.term @{context} p) ^ " = True",
1.168 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.169 - else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
1.170 + else SOME ((UnparseC.term @{context} p) ^ " = False",
1.171 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.172 | eval_sameFunId _ _ _ _ = NONE;
1.173
1.174 @@ -385,7 +385,7 @@
1.175 this is, because Isabelles filter takes more than 1 sec.*)
1.176 fun same_funid f1 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _) = f1 = f2
1.177 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
1.178 - ^ UnparseC.term_in_ctxt @{context} f1 ^ ") (" ^ UnparseC.term_in_ctxt @{context} t ^ ")");
1.179 + ^ UnparseC.term @{context} f1 ^ ") (" ^ UnparseC.term @{context} t ^ ")");
1.180 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
1.181 eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)
1.182 fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"
1.183 @@ -393,7 +393,7 @@
1.184 (fid $ _) $ fs) _ =
1.185 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
1.186 (filter (same_funid fid))) (TermC.isalist2list fs)
1.187 - in SOME (UnparseC.term_in_ctxt @{context} (TermC.mk_equality (p, fs')),
1.188 + in SOME (UnparseC.term @{context} (TermC.mk_equality (p, fs')),
1.189 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
1.190 | eval_filter_sameFunId _ _ _ _ = NONE;
1.191
1.192 @@ -418,7 +418,7 @@
1.193 val lhss = map TermC.lhs isal
1.194 val sum = list2sum lhss
1.195 in
1.196 - SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = " ^ (UnparseC.term_in_ctxt @{context} sum),
1.197 + SOME ((UnparseC.term @{context} p) ^ " = " ^ (UnparseC.term @{context} sum),
1.198 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
1.199 end
1.200 | eval_boollist2sum _ _ _ _ = NONE;