equal
deleted
inserted
replaced
101 val contains_one_of: thm * (string * typ) list -> bool |
101 val contains_one_of: thm * (string * typ) list -> bool |
102 val contains_Const_typeless: term list -> term -> bool |
102 val contains_Const_typeless: term list -> term -> bool |
103 val sym_trm : term -> term (* unused code, kept as hints to design ideas *) |
103 val sym_trm : term -> term (* unused code, kept as hints to design ideas *) |
104 |
104 |
105 val string_of_detail: Proof.context -> term -> string |
105 val string_of_detail: Proof.context -> term -> string |
|
106 (*from isac_test for Minisubpbl*) |
|
107 val atom_typ: Proof.context -> typ -> unit |
106 |
108 |
107 \<^isac_test>\<open> |
109 \<^isac_test>\<open> |
108 val mk_negative: typ -> term -> term |
110 val mk_negative: typ -> term -> term |
109 val mk_Var: term -> term |
111 val mk_Var: term -> term |
110 val scala_of_term: term -> string |
112 val scala_of_term: term -> string |
111 |
113 |
112 val atom_typ: Proof.context -> typ -> unit |
|
113 val atom_write: Proof.context -> term -> unit |
114 val atom_write: Proof.context -> term -> unit |
114 val atom_trace: Proof.context -> term -> unit |
115 val atom_trace: Proof.context -> term -> unit |
115 |
116 |
116 val atom_write_detail: Proof.context -> term -> unit |
117 val atom_write_detail: Proof.context -> term -> unit |
117 val atom_trace_detail: Proof.context -> term -> unit |
118 val atom_trace_detail: Proof.context -> term -> unit |
188 quote s ^ ", " ^ |
189 quote s ^ ", " ^ |
189 scala_of_typ T ^ ", " ^ |
190 scala_of_typ T ^ ", " ^ |
190 scala_of_term t) |
191 scala_of_term t) |
191 | scala_of_term (t1 $ t2) = |
192 | scala_of_term (t1 $ t2) = |
192 enclose "App(" ")" (scala_of_term t1 ^ ", " ^ scala_of_term t2) |
193 enclose "App(" ")" (scala_of_term t1 ^ ", " ^ scala_of_term t2) |
|
194 \<close> |
193 |
195 |
194 (* see structure's bare bones. |
196 (* see structure's bare bones. |
195 for Isabelle standard output compare 2017 "structure ML_PP" *) |
197 for Isabelle standard output compare 2017 "structure ML_PP" *) |
196 fun atom_typ ctxt t = |
198 fun atom_typ ctxt t = |
197 let |
199 let |
202 "\n*** " ^ indent n ^ "TVar ((" ^ s ^ ", " ^ string_of_int i ^ strs2str' sort |
204 "\n*** " ^ indent n ^ "TVar ((" ^ s ^ ", " ^ string_of_int i ^ strs2str' sort |
203 and atol n [] = "\n*** " ^ indent n ^ "]" |
205 and atol n [] = "\n*** " ^ indent n ^ "]" |
204 | atol n (T :: Ts) = (ato n T ^ atol n Ts) |
206 | atol n (T :: Ts) = (ato n T ^ atol n Ts) |
205 in tracing (ato 0 t ^ "\n") end; |
207 in tracing (ato 0 t ^ "\n") end; |
206 |
208 |
|
209 |
|
210 \<^isac_test>\<open> |
207 local |
211 local |
208 fun ato (Const (a, _)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)" |
212 fun ato (Const (a, _)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)" |
209 | ato (Free (a, _)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)" |
213 | ato (Free (a, _)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)" |
210 | ato (Var ((a, i), _)) n = |
214 | ato (Var ((a, i), _)) n = |
211 "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^ string_of_int i ^ "), _)" |
215 "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^ string_of_int i ^ "), _)" |
523 case parseNEW (Proof_Context.init_global thy) str of |
527 case parseNEW (Proof_Context.init_global thy) str of |
524 SOME t => t |
528 SOME t => t |
525 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
529 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
526 (*\----- old versions to be eliminated -------------------------------------------------------/*) |
530 (*\----- old versions to be eliminated -------------------------------------------------------/*) |
527 |
531 |
528 (* to be replaced by parse..*) |
532 (* to be replaced by Syntax.read_term..*) |
529 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str; |
533 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str; |
530 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *) |
534 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *) |
531 fun parse_patt thy str = (thy, str) |
535 fun parse_patt thy str = (thy, str) |
532 |>> Proof_Context.init_global |
536 |>> Proof_Context.init_global |
533 |-> Proof_Context.read_term_pattern |
537 |-> Proof_Context.read_term_pattern |