1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -136,11 +136,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_to_string''' thy prop, prop) end
1.8 + in SOME (UnparseC.term_thy thy 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_to_string''' thy prop, prop) end
1.13 + in SOME (UnparseC.term_thy thy prop, prop) end
1.14 | eval_matches _ _ _ _ = NONE;
1.15 (*
1.16 > val t = (Thm.term_of o the o (parse thy))
1.17 @@ -215,10 +215,10 @@
1.18 if matchsub thy tst pat
1.19 then
1.20 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.21 - in SOME (UnparseC.term_to_string''' thy prop, prop) end
1.22 + in SOME (UnparseC.term_thy thy 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_to_string''' thy prop, prop) end
1.26 + in SOME (UnparseC.term_thy thy prop, prop) end
1.27 | eval_matchsub _ _ _ _ = NONE;
1.28
1.29 (*get the variables in an isabelle-term*)
1.30 @@ -226,15 +226,15 @@
1.31 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =
1.32 let
1.33 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
1.34 - val thmId = thmid ^ UnparseC.term_to_string''' thy arg;
1.35 + val thmId = thmid ^ UnparseC.term_thy thy arg;
1.36 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
1.37 | eval_var _ _ _ _ = NONE;
1.38
1.39 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
1.40 - | lhs t = error("lhs called with (" ^ UnparseC.term2str t ^ ")");
1.41 + | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
1.42 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
1.43 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
1.44 - SOME ((UnparseC.term2str t) ^ " = " ^ (UnparseC.term2str l),
1.45 + SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
1.46 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
1.47 | eval_lhs _ _ _ _ = NONE;
1.48 (*
1.49 @@ -246,10 +246,10 @@
1.50 *)
1.51
1.52 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
1.53 - | rhs t = error("rhs called with (" ^ UnparseC.term2str t ^ ")");
1.54 + | rhs t = error("rhs called with (" ^ UnparseC.term t ^ ")");
1.55 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
1.56 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
1.57 - SOME (UnparseC.term2str t ^ " = " ^ UnparseC.term2str r,
1.58 + SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
1.59 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
1.60 | eval_rhs _ _ _ _ = NONE;
1.61 (*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
1.62 @@ -259,12 +259,12 @@
1.63
1.64 (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
1.65 fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
1.66 - ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term2str v));
1.67 - tracing("#>@ eval_occurs_in: t= "^(UnparseC.term2str t));*)
1.68 + ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
1.69 + tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
1.70 if occurs_in v t
1.71 - then SOME ((UnparseC.term2str p) ^ " = True",
1.72 + then SOME ((UnparseC.term p) ^ " = True",
1.73 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.74 - else SOME ((UnparseC.term2str p) ^ " = False",
1.75 + else SOME ((UnparseC.term p) ^ " = False",
1.76 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
1.77 | eval_occurs_in _ _ _ _ = NONE;
1.78
1.79 @@ -278,9 +278,9 @@
1.80 fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
1.81 (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =
1.82 if some_occur_in (TermC.isalist2list vs) t
1.83 - then SOME ((UnparseC.term2str p) ^ " = True",
1.84 + then SOME ((UnparseC.term p) ^ " = True",
1.85 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.86 - else SOME ((UnparseC.term2str p) ^ " = False",
1.87 + else SOME ((UnparseC.term p) ^ " = False",
1.88 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.89 | eval_some_occur_in _ _ _ _ = NONE;
1.90
1.91 @@ -321,7 +321,7 @@
1.92 then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.93 else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.94 | _ => (*NONE*)
1.95 - SOME (TermC.mk_thmid thmid (UnparseC.term2str arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
1.96 + SOME (TermC.mk_thmid thmid (UnparseC.term arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
1.97 | eval_const _ _ _ _ = NONE;
1.98
1.99 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
1.100 @@ -367,11 +367,11 @@
1.101 ----------- thus needs Rule.Num_Calc !
1.102 > val t = str2term "0 = 0";
1.103 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
1.104 -> UnparseC.term2str t';
1.105 +> UnparseC.term t';
1.106 val it = "HOL.True"
1.107
1.108 val t = str2term "Not (x = 0)";
1.109 -atomt t; UnparseC.term2str t;
1.110 +atomt t; UnparseC.term t;
1.111 *** -------------
1.112 *** Const ( Not)
1.113 *** . Const ( op =)
1.114 @@ -386,28 +386,28 @@
1.115 (Const _(*op0, t0*) $ t1 $ t2 )) thy =
1.116 if t1 = t2
1.117 then SOME (TermC.mk_thmid thmid
1.118 - ("(" ^ (UnparseC.term_to_string''' thy t1) ^ ")")
1.119 - ("(" ^ (UnparseC.term_to_string''' thy t2) ^ ")"),
1.120 + ("(" ^ (UnparseC.term_thy thy t1) ^ ")")
1.121 + ("(" ^ (UnparseC.term_thy thy t2) ^ ")"),
1.122 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.123 else SOME (TermC.mk_thmid thmid
1.124 - ("(" ^ (UnparseC.term_to_string''' thy t1) ^ ")")
1.125 - ("(" ^ (UnparseC.term_to_string''' thy t2) ^ ")"),
1.126 + ("(" ^ (UnparseC.term_thy thy t1) ^ ")")
1.127 + ("(" ^ (UnparseC.term_thy thy t2) ^ ")"),
1.128 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.129 | eval_ident _ _ _ _ = NONE;
1.130 (* TODO
1.131 > val t = str2term "x =!= 0";
1.132 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.133 -> UnparseC.term2str t';
1.134 +> UnparseC.term t';
1.135 val str = "ident_(x)_(0)" : string
1.136 val it = "(x =!= 0) = False" : string
1.137 > val t = str2term "1 =!= 0";
1.138 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.139 -> UnparseC.term2str t';
1.140 +> UnparseC.term t';
1.141 val str = "ident_(1)_(0)" : string
1.142 val it = "(1 =!= 0) = False" : string
1.143 > val t = str2term "0 =!= 0";
1.144 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.145 -> UnparseC.term2str t';
1.146 +> UnparseC.term t';
1.147 val str = "ident_(0)_(0)" : string
1.148 val it = "(0 =!= 0) = True" : string
1.149 *)
1.150 @@ -420,7 +420,7 @@
1.151 if t1 = t2
1.152 then
1.153 SOME (TermC.mk_thmid thmid
1.154 - ("(" ^ UnparseC.term_to_string''' thy t1 ^ ")") ("(" ^ UnparseC.term_to_string''' thy t2 ^ ")"),
1.155 + ("(" ^ UnparseC.term_thy thy t1 ^ ")") ("(" ^ UnparseC.term_thy thy t2 ^ ")"),
1.156 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.157 else
1.158 (case (TermC.is_atom t1, TermC.is_atom t2) of
1.159 @@ -428,7 +428,7 @@
1.160 if TermC.variable_constant_pair (t1, t2)
1.161 then NONE
1.162 else SOME (TermC.mk_thmid thmid
1.163 - ("(" ^ UnparseC.term_to_string''' thy t1 ^ ")") ("(" ^ UnparseC.term_to_string''' thy t2 ^ ")"),
1.164 + ("(" ^ UnparseC.term_thy thy t1 ^ ")") ("(" ^ UnparseC.term_thy thy t2 ^ ")"),
1.165 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.166 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
1.167 | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.168 @@ -462,7 +462,7 @@
1.169 (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =
1.170 if is_Free arg (*could be something to be simplified before*)
1.171 then
1.172 - SOME (UnparseC.term2str t ^ " = " ^ UnparseC.term2str arg,
1.173 + SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,
1.174 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
1.175 else NONE
1.176 | eval_argument_in _ _ _ _ = NONE;
1.177 @@ -473,9 +473,9 @@
1.178 fun eval_sameFunId _ "Prog_Expr.sameFunId"
1.179 (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
1.180 if f1 = f2
1.181 - then SOME ((UnparseC.term2str p) ^ " = True",
1.182 + then SOME ((UnparseC.term p) ^ " = True",
1.183 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.184 - else SOME ((UnparseC.term2str p) ^ " = False",
1.185 + else SOME ((UnparseC.term p) ^ " = False",
1.186 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.187 | eval_sameFunId _ _ _ _ = NONE;
1.188
1.189 @@ -486,7 +486,7 @@
1.190 this is, because Isabelles filter takes more than 1 sec.*)
1.191 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
1.192 | same_funid f1 t = error ("same_funid called with t = ("
1.193 - ^ UnparseC.term2str f1 ^ ") (" ^ UnparseC.term2str t ^ ")");
1.194 + ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
1.195 (*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
1.196 eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
1.197 fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"
1.198 @@ -494,7 +494,7 @@
1.199 (fid $ _) $ fs) _ =
1.200 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
1.201 (filter (same_funid fid))) (TermC.isalist2list fs)
1.202 - in SOME (UnparseC.term2str (TermC.mk_equality (p, fs')),
1.203 + in SOME (UnparseC.term (TermC.mk_equality (p, fs')),
1.204 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
1.205 | eval_filter_sameFunId _ _ _ _ = NONE;
1.206
1.207 @@ -519,7 +519,7 @@
1.208 val lhss = map lhs isal
1.209 val sum = list2sum lhss
1.210 in
1.211 - SOME ((UnparseC.term2str p) ^ " = " ^ (UnparseC.term2str sum),
1.212 + SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum),
1.213 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
1.214 end
1.215 | eval_boollist2sum _ _ _ _ = NONE;