Searched refs:trace (Results 26 - 50 of 260) sorted by relevance

1234567891011

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DActive.sml36 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 DKnuthBendixOrder.sml186 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 DSubsume.sml282 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 DProof.sml172 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 DActive.sml36 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 DKnuthBendixOrder.sml186 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 DSubsume.sml282 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 DProof.sml172 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 DCond_rewr.sml150 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 DOpening.sml153 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 DboolSimps.sml28 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 DFeedback.sml185 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 Dho_proverTools.sml31 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 Dselftest.sml23 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 Drep_graph.py17 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 Dloop_bounds.py3 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 Dsearch.py23 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 Dobjdump.py51 from target_objects import symbols, sections, trace namespace
64 trace ('No %r section in objdump.' % nm)
H A Dgraph-refine.py21 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 Dstate_monadLib.sml41 Feedback.trace ("notify type variable guesses", 0) Parse.Term
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dselftest.sml48 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 DarmLib.sml17 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 DarmLib.sml16 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 Dsimplifier_trace_window.scala4 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 Dsimplifier_trace_window.scala4 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))

Completed in 188 milliseconds

1234567891011