/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Active.sml | 36 val () = Print.trace Clause.pp 57 val () = Print.trace Clause.pp 72 val () = Print.trace Clause.pp 100 val () = Print.trace Literal.pp 109 val () = Print.trace Clause.pp 112 val () = Print.trace Rewrite.ppOrient 133 val () = Print.trace Literal.pp 142 val () = Print.trace Clause.pp 166 val () = Print.trace Clause.pp 176 val () = Print.trace Claus [all...] |
H A D | KnuthBendixOrder.sml | 186 val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm1" tm1 187 val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm2" tm2 191 NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n" 193 Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x
|
H A D | Subsume.sml | 282 val () = Print.trace ppCl "Subsume.subsumes: cl" cl 286 NONE => trace "Subsume.subsumes: not subsumed\n" 288 (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl; 289 Print.trace ppSub "Subsume.subsumes: subsuming sub" sub) 298 val () = Print.trace ppCl "Subsume.strictlySubsumes: cl" cl 302 NONE => trace "Subsume.subsumes: not subsumed\n" 304 (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl; 305 Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
|
H A D | Proof.sml | 172 val () = Print.trace LiteralSet.pp "reconstructSubst: cl" cl 173 val () = Print.trace LiteralSet.pp "reconstructSubst: cl'" cl' 221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl 271 val () = Print.trace ppCands 309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th 318 val () = Print.trace ppThmInf "Proof.thmToInference: thmInf" thmInf 324 val () = Print.trace ppInference "Proof.thmToInference: inf" inf 395 val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths) 404 val () = Print.trace Thm.pp "Proof.proof: th" th 409 val () = Print.trace Prin [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Active.sml | 36 val () = Print.trace Clause.pp 57 val () = Print.trace Clause.pp 72 val () = Print.trace Clause.pp 100 val () = Print.trace Literal.pp 109 val () = Print.trace Clause.pp 112 val () = Print.trace Rewrite.ppOrient 133 val () = Print.trace Literal.pp 142 val () = Print.trace Clause.pp 166 val () = Print.trace Clause.pp 176 val () = Print.trace Claus [all...] |
H A D | KnuthBendixOrder.sml | 186 val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm1" tm1 187 val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm2" tm2 191 NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n" 193 Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x
|
H A D | Subsume.sml | 282 val () = Print.trace ppCl "Subsume.subsumes: cl" cl 286 NONE => trace "Subsume.subsumes: not subsumed\n" 288 (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl; 289 Print.trace ppSub "Subsume.subsumes: subsuming sub" sub) 298 val () = Print.trace ppCl "Subsume.strictlySubsumes: cl" cl 302 NONE => trace "Subsume.subsumes: not subsumed\n" 304 (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl; 305 Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
|
H A D | Proof.sml | 172 val () = Print.trace LiteralSet.pp "reconstructSubst: cl" cl 173 val () = Print.trace LiteralSet.pp "reconstructSubst: cl'" cl' 221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl 271 val () = Print.trace ppCands 309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th 318 val () = Print.trace ppThmInf "Proof.thmToInference: thmInf" thmInf 324 val () = Print.trace ppInference "Proof.thmToInference: inf" inf 395 val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths) 404 val () = Print.trace Thm.pp "Proof.proof: th" th 409 val () = Print.trace Prin [all...] |
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Cond_rewr.sml | 150 then (trace(1, TEXT "looping - cut"); 153 then (trace(1, TEXT "looping - stack limit reached"); 158 (trace(4, IGNORE ("Rewrite loops", conditional_eqn)); 165 (trace(4, IGNORE("possibly looping",conditional_eqn)); 169 else trace(if isperm then 2 else 1, REWRITING(tm,th)) 172 let val _ = trace(2,SIDECOND_ATTEMPT condition) 175 => (trace(1,SIDECOND_NOT_SOLVED condition); raise e) 176 in trace(2,SIDECOND_SOLVED res); 184 trace(if isperm then 2 else 1, REWRITING(tm,th)) 189 in trace(i [all...] |
H A D | Opening.sml | 153 val _ = trace(3,OPENING(tm,match_thm)) 188 (trace(5,PRODUCE(concl thm,"UNCHANGED",thm));thm) 195 in (trace(5,PRODUCE(orig,"UNCHANGED",thm));thm) 211 val _ = trace (6, LZ_TEXT output) 225 else (trace(3,PRODUCE(tm,"congruence rule",final_thm)); final_thm) 250 => (trace(0,REDUCE("SIMPLIFIER ERROR: bug when alpha converting",tm)); 251 trace(0,REDUCE("trying to alpha convert to",v)); 260 else let val _ = trace(4,TEXT "no alpha conversion")
|
H A D | boolSimps.sml | 28 trace = 2, 32 trace = 2, 66 trace=2, 131 trace=1, 135 trace=1, 252 trace = 2}, 257 trace = 2}], 268 trace = 2}, 272 trace = 2}], 319 trace [all...] |
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Feedback.sml | 185 then raise ERR "register_trace" "Can't have trace values less than zero." 189 WARN "register_trace" ("Replacing a trace with name " ^ quote nm) 200 ("Original trace: \""^original^"\" doesn't exist") 220 ("Cannot replace existing genuine trace info for \""^ 231 "Can't have trace values less than zero." 235 ("Replacing a trace with name " ^ quote nm) 247 ("Replacing a trace with name "^ quote nm) 273 fun registered_err f nm = err f ["No trace ", quote nm, " is registered"] 307 fun trace (nm, i) f x = function 309 NONE => registered_err "trace" n [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 31 fun trace _ _ = (); function 188 val _ = trace "trace_frule: f" (fn () => printVal f) 240 val _ = trace "crule_to_frule: cl'" (fn () => printVal cl') 247 trace "crule_to_frule: ((cl, th), cls')" 404 val _ = trace "rewr_conv: d" (fn () => printVal (dest_ski_discrim d)) 412 val _ = trace "rewr_conv: rw: tm" (fn () => printVal tm) 414 val _ = trace "rewr_conv: rw: res" (fn () => printVal res) 420 val _ = trace "rewr_conv: RW: tm" (fn () => printVal tm) 422 val _ = trace "rewr_conv: RW: res" (fn () => printVal res) 435 val _ = trace "literal_con [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | selftest.sml | 23 val res = trace ("PP.catch_withpp_err", 0) term_to_string ``foo(x,y)`` 43 trace ("PP.print_firstcasebar", 1) tpp "case e of | 0 => 1 | SUC n => n + 2"; 44 trace ("PP.print_firstcasebar", 1) tpp
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | rep_graph.py | 17 from target_objects import functions, pairings, sections, trace, printout namespace 507 trace ('is_synt_const: %d iterations' % count) 508 trace ('visit length %d' % len (visit)) 509 trace ('visit tail %s' % visit[-20:]) 757 trace ('substituted %s at %s.' % (y, n_vc)) 840 trace ('skipped emitting func pairing %s -> %s' 842 trace (' ' + s) 972 trace ('Skipped inlining at %d.' % n) 975 trace ('Inlining at %d.' % n) 997 trace ('No [all...] |
H A D | loop_bounds.py | 3 from target_objects import functions, trace namespace 353 trace ('Found bound %s for 0x%x in %s.' % (bound, split_bin_addr, 407 trace ('Getting bound for 0x%x in context %s.' % (split, call_ctxt)) 461 trace ('Searching for bound for 0x%x in %s.', (split, p.name)) 544 trace ('no C bounds found (%s).' % c_bounds) 559 trace ('no split found (%s).' % repr (split)) 569 trace ('split check failed!') 570 trace ('failed at %s' % el) 578 trace ('key split was not bounded (%r, %r).' % (c_split, c_bounds)) 701 trace ('avoidin [all...] |
H A D | search.py | 23 from target_objects import trace, printout namespace 60 trace ('Built proof for %s' % p.name) 77 trace ('Finding split limit: %d (%s)' % (n, tag)) 99 trace ('split limit found: %d' % i) 113 trace ('No split limit found for %d (%s).' % (n, tag)) 216 trace ('WARNING: EqSearchKnowledge: premise unsat.') 217 trace (" ... learning procedure isn't going to work.") 289 trace ('WARNING: SearchKnowledge: premise unsat.') 290 trace (" ... learning procedure isn't going to work.") 321 trace ('Doin [all...] |
H A D | objdump.py | 51 from target_objects import symbols, sections, trace namespace 64 trace ('No %r section in objdump.' % nm)
|
H A D | graph-refine.py | 21 from target_objects import trace, tracer, printout namespace 53 trace (time.asctime ()) 88 trace ('EXCEPTION in checking %s:' % p.name) 101 trace ('EXCEPTION in handling %s:' % pair) 258 trace ('Saving %s' % f) 285 elif arg.startswith ('trace-to:'):
|
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/ |
H A D | state_monadLib.sml | 41 Feedback.trace ("notify type variable guesses", 0) Parse.Term
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | selftest.sml | 48 val _ = (trace ("Univ pretty-printing", 0) testutils.tpp) "UNIV" 84 print "Testing loads with Unicode trace off\n";
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | armLib.sml | 17 fun conv_rec t = {name = "ICLASS_CONV",trace = 3,conv = K (K ICLASS_CONV), 77 simpLib.conv_ss {name="PBETA", trace = 3, conv=K (K PBETA_CONV), key = NONE};
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | armLib.sml | 16 fun conv_rec t = {name = "ICLASS_CONV",trace = 3,conv = K (K ICLASS_CONV), 60 convs = [{name="PBETA",trace = 3,conv=K (K PairRules.PBETA_CONV),
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | simplifier_trace_window.scala | 4 Trace window with tree-style view of the simplifier trace. 137 view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame 149 private val tree = trace.entries.headOption match { 152 Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | simplifier_trace_window.scala | 4 Trace window with tree-style view of the simplifier trace. 137 view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame 149 private val tree = trace.entries.headOption match { 152 Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
|