97 val vars': term list -> term list |
97 val vars': term list -> term list |
98 val vars_of: term -> term list (* deprecated TODOO: see differences in test/../termC.sml*) |
98 val vars_of: term -> term list (* deprecated TODOO: see differences in test/../termC.sml*) |
99 val dest_list': term -> term list |
99 val dest_list': term -> term list |
100 val negates: term -> term -> bool |
100 val negates: term -> term -> bool |
101 |
101 |
102 \<^isac_test>\<open> |
102 val contains_one_of: thm * (string * typ) list -> bool |
|
103 val contains_Const_typeless: term list -> term -> bool |
|
104 val sym_trm : term -> term (* unused code, kept as hints to design ideas *) |
|
105 |
|
106 (*isac_test*) |
103 val mk_negative: typ -> term -> term |
107 val mk_negative: typ -> term -> term |
|
108 val free2var: term -> term |
104 val scala_of_term: term -> string |
109 val scala_of_term: term -> string |
105 val atomtyp(*<-- atom_typ TODO*): typ -> unit |
110 |
|
111 (*val atom_typ: typ -> unit RENAME*) |
|
112 val atomtyp: typ -> unit |
106 val atomty: term -> unit |
113 val atomty: term -> unit |
107 val atomw: term -> unit |
114 val atomw: term -> unit |
108 val atomt: term -> unit |
115 val atomt: term -> unit |
109 val atomwy: term -> unit |
116 val atomwy: term -> unit |
110 val atomty_thy: ThyC.id -> term -> unit |
117 |
111 val free2var: term -> term |
118 \<^isac_test>\<open> |
112 \<close> |
119 \<close> |
113 val contains_one_of: thm * (string * typ) list -> bool |
|
114 val contains_Const_typeless: term list -> term -> bool |
|
115 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
|
116 val sym_trm : term -> term |
|
117 end |
120 end |
118 |
121 |
119 (**) |
122 (**) |
120 structure TermC(**): TERM_ISAC(**) = |
123 structure TermC(**): TERM_ISAC(**) = |
121 struct |
124 struct |
146 fun matches thy tm pa = |
149 fun matches thy tm pa = |
147 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true) |
150 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true) |
148 handle Pattern.MATCH => false |
151 handle Pattern.MATCH => false |
149 |
152 |
150 (** transform typ / term to a String to be parsed by Scala after transport via libisabelle **) |
153 (** transform typ / term to a String to be parsed by Scala after transport via libisabelle **) |
151 |
154 (*isac_test*) |
152 \<^isac_test>\<open> |
|
153 fun scala_of_typ (Type (s, typs)) = |
155 fun scala_of_typ (Type (s, typs)) = |
154 enclose "Type(" ")" (quote s ^ ", " ^ |
156 enclose "Type(" ")" (quote s ^ ", " ^ |
155 (typs |> map scala_of_typ |> commas |> enclose "List(" ")")) |
157 (typs |> map scala_of_typ |> commas |> enclose "List(" ")")) |
156 | scala_of_typ (TFree (s, sort)) = |
158 | scala_of_typ (TFree (s, sort)) = |
157 enclose "TFree(" ")" (quote s ^ ", " ^ (sort |> map quote |> commas |> enclose "List(" ")")) |
159 enclose "TFree(" ")" (quote s ^ ", " ^ (sort |> map quote |> commas |> enclose "List(" ")")) |
200 | ato (f $ t) n = (ato f n ^ ato t (n + 1)) |
202 | ato (f $ t) n = (ato f n ^ ato t (n + 1)) |
201 in |
203 in |
202 fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
204 fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
203 fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
205 fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
204 end; |
206 end; |
|
207 |
|
208 \<^isac_test>\<open> |
205 \<close> |
209 \<close> |
206 |
210 |
207 fun term_detail2str t = |
211 fun term_detail2str t = |
208 let |
212 let |
209 fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ T ^ ")" |
213 val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global |
210 | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ T ^ ")" |
214 fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")" |
|
215 | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")" |
211 | ato (Var ((a, i), T)) n = |
216 | ato (Var ((a, i), T)) n = |
212 "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ T ^ ")" |
217 "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")" |
213 | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i |
218 | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i |
214 | ato (Abs(a, T, body)) n = |
219 | ato (Abs(a, T, body)) n = |
215 "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ T ^ ",.." ^ ato body (n + 1) |
220 "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1) |
216 | ato (f $ t) n = ato f n ^ ato t (n + 1) |
221 | ato (f $ t) n = ato f n ^ ato t (n + 1) |
217 in "\n*** " ^ ato t 0 ^ "\n***" end; |
222 in "\n*** " ^ ato t 0 ^ "\n***" end; |
218 |
223 |
219 \<^isac_test>\<open> |
224 (*isac_test*) |
220 fun term_detail2str_thy thy t = |
|
221 let |
|
222 fun ato (Const (a, T)) n = |
|
223 "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")" |
|
224 | ato (Free (a, T)) n = |
|
225 "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")" |
|
226 | ato (Var ((a, i), T)) n = |
|
227 "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ |
|
228 UnparseC.typ_by_thyID thy T ^ ")" |
|
229 | ato (Bound i) n = |
|
230 "\n*** " ^ indent n ^ "Bound " ^ string_of_int i |
|
231 | ato (Abs(a, T, body)) n = |
|
232 "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ",.." ^ |
|
233 ato body (n + 1) |
|
234 | ato (f $ t) n = ato f n ^ ato t (n + 1) |
|
235 in "\n*** " ^ ato t 0 ^ "\n***" end; |
|
236 fun atomwy t = (writeln o term_detail2str) t; |
225 fun atomwy t = (writeln o term_detail2str) t; |
237 fun atomty t = (tracing o term_detail2str) t; |
226 fun atomty t = (tracing o term_detail2str) t; |
238 fun atomty_thy thy t = (tracing o (term_detail2str_thy thy)) t; |
227 |
|
228 \<^isac_test>\<open> |
239 \<close> |
229 \<close> |
240 |
230 |
241 (* contains the term a VAR(("*",_),_) ? *) |
231 (* contains the term a VAR(("*",_),_) ? *) |
242 fun contains_Var (Abs(_,_,body)) = contains_Var body |
232 fun contains_Var (Abs(_,_,body)) = contains_Var body |
243 | contains_Var (f $ f') = contains_Var f orelse contains_Var f' |
233 | contains_Var (f $ f') = contains_Var f orelse contains_Var f' |
373 | var2free (Var((s, _), T)) = Free (s,T) |
363 | var2free (Var((s, _), T)) = Free (s,T) |
374 | var2free (t as Bound _) = t |
364 | var2free (t as Bound _) = t |
375 | var2free (Abs(s, T, t)) = Abs(s, T, var2free t) |
365 | var2free (Abs(s, T, t)) = Abs(s, T, var2free t) |
376 | var2free (t1 $ t2) = (var2free t1) $ (var2free t2); |
366 | var2free (t1 $ t2) = (var2free t1) $ (var2free t2); |
377 |
367 |
378 \<^isac_test>\<open> |
368 (*isac_test*) |
379 (* Logic.varify does NOT take care of 'Free ("1", _)'*) |
369 (* Logic.varify does NOT take care of 'Free ("1", _)'*) |
380 fun free2var (t as Const _) = t |
370 fun free2var (t as Const _) = t |
381 | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T) |
371 | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T) |
382 | free2var (t as Var _) = t |
372 | free2var (t as Var _) = t |
383 | free2var (t as Bound _) = t |
373 | free2var (t as Bound _) = t |
384 | free2var (Abs (s, T, t)) = Abs (s, T, free2var t) |
374 | free2var (Abs (s, T, t)) = Abs (s, T, free2var t) |
385 | free2var (t1 $ t2) = (free2var t1) $ (free2var t2); |
375 | free2var (t1 $ t2) = (free2var t1) $ (free2var t2); |
|
376 |
|
377 \<^isac_test>\<open> |
386 \<close> |
378 \<close> |
387 |
379 |
388 fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]); |
380 fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]); |
389 fun list_const T = Const (\<^const_name>\<open>Cons\<close>, [T, mk_listT T] ---> mk_listT T); |
381 fun list_const T = Const (\<^const_name>\<open>Cons\<close>, [T, mk_listT T] ---> mk_listT T); |
390 fun list2isalist T [] = Const (\<^const_name>\<open>Nil\<close>, mk_listT T) |
382 fun list2isalist T [] = Const (\<^const_name>\<open>Nil\<close>, mk_listT T) |