Functor Infsys.Trace


module Trace: functor (I : EQ) -> functor (L : sig  end) -> sig  end
Tracing rule applications.
Parameters:
I : Infsys.EQ
L : sig end


type e
val current : unit -> e
Parameters:
? : unit
val initialize : e -> unit
Intitialize inference system with equality set.
Parameters:
? : e
val finalize : unit -> e
Retrieve modified equality set.
Parameters:
? : unit
val abstract : Term.t -> unit
(g[a]; e; p) ==> (g[x]; e, x = a; p) with
Parameters:
? : Term.t
val merge : Fact.Equal.t -> unit
(g, a = b; e; p) ==> (g; e'; p') with
Parameters:
? : Fact.Equal.t
val propagate : Fact.Equal.t -> unit
(g, e; p) ==> (g; e'; p) with
Parameters:
? : Fact.Equal.t
val dismerge : Fact.Diseq.t -> unit
(g, a <> a; e; p) ==> (g; e'; p') with a, b i-pure, |= e', p' <=> |= e, p, a <> b.
Parameters:
? : Fact.Diseq.t
val propagate_diseq : Fact.Diseq.t -> unit
(g; e; p) ==> (g; e'; p') with
Parameters:
? : Fact.Diseq.t
val branch : unit -> unit
(g; e; p) ==> (g, c1; e; p) | ... | (g, cn; e; p) with
Parameters:
? : unit
val normalize : unit -> unit
(g; e; p) ==> (g'; e'; p') where source and target configuration are equivalent.
Parameters:
? : unit