package lascar

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Valuation.MakeSource

Functor building an implementation of the Valuation structure given an implementation of values

Parameters

module V : VALUE

Signature

Sourcetype name = string

The type of variable names

Sourcetype value = V.t

The type for variable values

Sourcetype t = (name * value) list

The type of valuation. Basic, public implementation here

Sourceval compare : t -> t -> int
Sourceval to_string : t -> string
Sourceexception Invalid_valuation of t
Sourceval check : name list -> t -> unit

check names vs checks whether vs is a "complete" valuation wrt. to names. i.e. whether each variable listed in names has a valuation in vs and each variable listed in vs occurs in names. Raises Invalid_valuation in case of failure.

Sourceval empty : t
Sourceexception Duplicate of name
Sourceval add : name -> value -> t -> t
Sourceval remove : name -> t -> t
Sourceval mem : name -> t -> bool
Sourceval assoc : name -> t -> value
OCaml

Innovation. Community. Security.