@@ -396,6 +396,29 @@ object Semantic {
396396
397397 inline def cache (using c : Cache ): Cache = c
398398
399+ // ----- Checker State -----------------------------------
400+
401+ /** The state that threads through the interpreter */
402+ type Contextual [T ] = (Env , Context , Trace , Promoted , Cache , Reporter ) ?=> T
403+
404+ // ----- Error Handling -----------------------------------
405+
406+ object Trace {
407+ opaque type Trace = Vector [Tree ]
408+
409+ val empty : Trace = Vector .empty
410+
411+ extension (trace : Trace )
412+ def add (node : Tree ): Trace = trace :+ node
413+ def toVector : Vector [Tree ] = trace
414+ }
415+
416+ type Trace = Trace .Trace
417+
418+ import Trace ._
419+ def trace (using t : Trace ): Trace = t
420+ inline def withTrace [T ](t : Trace )(op : Trace ?=> T ): T = op(using t)
421+
399422 /** Error reporting */
400423 trait Reporter :
401424 def report (err : Error ): Unit
@@ -429,29 +452,6 @@ object Semantic {
429452
430453 inline def reporter (using r : Reporter ): Reporter = r
431454
432- // ----- Checker State -----------------------------------
433-
434- /** The state that threads through the interpreter */
435- type Contextual [T ] = (Env , Context , Trace , Promoted , Cache , Reporter ) ?=> T
436-
437- // ----- Error Handling -----------------------------------
438-
439- object Trace {
440- opaque type Trace = Vector [Tree ]
441-
442- val empty : Trace = Vector .empty
443-
444- extension (trace : Trace )
445- def add (node : Tree ): Trace = trace :+ node
446- def toVector : Vector [Tree ] = trace
447- }
448-
449- type Trace = Trace .Trace
450-
451- import Trace ._
452- def trace (using t : Trace ): Trace = t
453- inline def withTrace [T ](t : Trace )(op : Trace ?=> T ): T = op(using t)
454-
455455// ----- Operations on domains -----------------------------
456456 extension (a : Value )
457457 def join (b : Value ): Value =
0 commit comments