package logtk

  1. Overview
  2. Docs
On This Page
  1. Scoped Value
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.ScopedSource

Scoped Value

A scoped value is a pair of the value and an (integer) scope. The value usually contains variables, but a value in a scope A share no variables with the same value in any scope B ≠ A.

This makes it possible to use an object (e.g. a clause) in two distinct scopes. Each scoped version of the object shares no variable with the other version; hence, there is no need for copying the object.

Sourcetype scope = int
Sourcetype +'a t = 'a * scope
Sourceval make : 'a -> int -> 'a t
Sourceval get : 'a t -> 'a
Sourceval scope : _ t -> int
Sourceval set : 'a t -> 'b -> 'b t

set v x is x with the same scope as v

Sourceval same_scope : _ t -> _ t -> bool
Sourceval equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
Sourceval compare : 'a CCOrd.t -> 'a t CCOrd.t
Sourceval hash : 'a Hash.t -> 'a t -> int
Sourceval map : ('a -> 'b) -> 'a t -> 'b t
Sourceval on : ('a -> 'b) -> 'a t -> 'b
Sourceval on2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c
Sourceval to_string : 'a CCFormat.printer -> 'a t -> string