Frama-C:
Plug-ins:
Libraries:

Frama-C API - QED

module ADT = ADT
module Field = Field
module Fun = Fun
type term
type lc_term

Loosely closed terms.

module Term : Qed.Logic.Symbol with type t = term
module Tset : Qed.Idxset.S with type elt = term

Non-structural, machine dependent, but fast comparison and efficient merges

module Tmap : Qed.Idxmap.S with type key = term

Non-structural, machine dependent, but fast comparison and efficient merges

module STset : Stdlib.Set.S with type elt = term

Structuraly ordered, but less efficient access and non-linear merges

module STmap : Stdlib.Map.S with type key = term

Structuraly ordered, but less efficient access and non-linear merges

Variables

type var = Var.t
module Tau : Qed.Logic.Data with type t = tau
module Vars : Qed.Idxset.S with type elt = var
module Vmap : Qed.Idxmap.S with type key = var
type pool
val pool : ?copy:pool -> unit -> pool
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
val add_term : pool -> term -> unit
val fresh : pool -> ?basename:string -> tau -> var
val alpha : pool -> var -> var
val tau_of_var : var -> tau
val sort_of_var : var -> Qed.Logic.sort
val base_of_var : var -> string

Terms

type 'a expression = (Field.t, ADT.t, Fun.t, var, lc_term, 'a) Qed.Logic.term_repr
type repr = term expression
type record = (Field.t * term) list
val decide : term -> bool

Return true if and only the term is e_true. Constant time.

val is_true : term -> Qed.Logic.maybe

Constant time.

val is_false : term -> Qed.Logic.maybe

Constant time.

val is_prop : term -> bool

Boolean or Property

val is_int : term -> bool

Integer sort

val is_real : term -> bool

Real sort

val is_arith : term -> bool

Integer or Real sort

val are_equal : term -> term -> Qed.Logic.maybe

Computes equality

val eval_eq : term -> term -> bool

Same as are_equal is Yes

val eval_neq : term -> term -> bool

Same as are_equal is No

val eval_lt : term -> term -> bool

Same as e_lt is e_true

val eval_leq : term -> term -> bool

Same as e_leq is e_true

val repr : term -> repr

Constant time

val sort : term -> Qed.Logic.sort

Constant time

val vars : term -> Vars.t

Constant time

Path-positioning access

This part of the API is DEPRECATED

type path = int list

position of a subterm in a term.

Basic constructors

val e_true : term
val e_false : term
val e_bool : bool -> term
val e_literal : bool -> term -> term
val e_int : int -> term
val e_float : float -> term
val e_zint : Z.t -> term
val e_real : Q.t -> term
val e_var : var -> term
val e_opp : term -> term
val e_times : Z.t -> term -> term
val e_sum : term list -> term
val e_prod : term list -> term
val e_add : term -> term -> term
val e_sub : term -> term -> term
val e_mul : term -> term -> term
val e_div : term -> term -> term
val e_mod : term -> term -> term
val e_eq : term -> term -> term
val e_neq : term -> term -> term
val e_leq : term -> term -> term
val e_lt : term -> term -> term
val e_imply : term list -> term -> term
val e_equiv : term -> term -> term
val e_and : term list -> term
val e_or : term list -> term
val e_not : term -> term
val e_if : term -> term -> term -> term
val e_const : tau -> term -> term
val e_get : term -> term -> term
val e_set : term -> term -> term -> term
val e_getfield : term -> Field.t -> term
val e_record : record -> term
val e_fun : ?result:tau -> Fun.t -> term list -> term
val e_repr : ?result:tau -> repr -> term
  • raises Invalid_argument

    on Bvar and Bind

Quantifiers and Binding

val e_forall : var list -> term -> term
val e_exists : var list -> term -> term
val e_lambda : var list -> term -> term
val e_close_forall : term -> term
val e_close_exists : term -> term
val e_close_lambda : term -> term
val e_apply : term -> term list -> term
val e_bind : Qed.Logic.binder -> var -> term -> term

Bind the given variable if it appears free in the term, or return the term unchanged.

val e_unbind : var -> lc_term -> term

Opens the top-most bound variable with a (fresh) variable. Can be only applied on top-most lc-term from `Bind(_,_,_)`, thanks to typing.

val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> term -> (Qed.Logic.binder * var) list * term

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default). The pool must contain all free variables of the term.

val e_close : (Qed.Logic.binder * var) list -> term -> term

Closes all specified binders

Generalized Substitutions

type sigma
val sigma : ?pool:pool -> unit -> sigma
module Subst : sig ... end
val e_subst : sigma -> term -> term

The environment sigma must be prepared with the desired substitution. Its pool of fresh variables must covers the entire domain and co-domain of the substitution, and the transformed values.

val e_subst_var : var -> term -> term -> term

Locally Nameless Representation

These functions can be unsafe because they might expose terms that contains non-bound b-vars. Never use such terms to build substitutions (sigma).

val lc_vars : term -> Qed.Bvars.t
val lc_closed : term -> bool

All bound variables are under their binder

val lc_repr : lc_term -> term

Calling this function is unsafe unless the term is lc_closed

val lc_iter : (term -> unit) -> term -> unit

Similar to f_iter but exposes non-closed sub-terms of `Bind` as regular term values instead of lc_term ones.

Iteration Scheme

val f_map : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> (term -> term) -> term -> term

Pass and open binders, maps its direct sub-terms and then close then opened binders Raises Invalid_argument in case of a bind-term without pool. The optional pool must contain all free variables of the term.

val f_iter : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> (term -> unit) -> term -> unit

Iterates over its direct sub-terms (pass and open binders) Raises Invalid_argument in case of a bind-term without pool. The optional pool must contain all free variables of the term.

Partial Typing

val typeof : ?field:(Field.t -> tau) -> ?record:(Field.t -> tau) -> ?call:(Fun.t -> tau option list -> tau) -> term -> tau

Try to extract a type of term. Parameterized by optional extractors for field and functions. Extractors may raise Not_found ; however, they are only used when the provided kinds for fields and functions are not precise enough.

  • parameter field

    type of a field value

  • parameter record

    type of the record containing a field

  • parameter call

    type of the values returned by the function

  • raises Not_found

    if no type is found.

Support for Builtins

val set_builtin : ?force:bool -> Fun.t -> (term list -> term) -> unit

Register a simplifier for function f. The computation code may raise Not_found, in which case the symbol is not interpreted.

If f is an operator with algebraic rules (see type operator), the children are normalized before builtin call.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

val set_builtin' : ?force:bool -> Fun.t -> (term list -> tau option -> term) -> unit
val set_builtin_map : ?force:bool -> Fun.t -> (term list -> term list) -> unit

Register a builtin for rewriting f a1..an into f b1..bm.

This is short cut for set_builtin, where the head application of f avoids to run into an infinite loop.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

val set_builtin_get : ?force:bool -> Fun.t -> (term list -> term list -> term) -> unit

set_builtin_get f rewrite register a builtin for rewriting (f a1..an)[k1]..[km] into rewrite (a1..an) (k1..km).

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

  • before 28.0-Nickel

    one-dimensional access only

val set_builtin_field : ?force:bool -> Fun.t -> Field.t -> (term list -> term) -> unit

Register a builtin for simplifying (f e…).fd expressions. Must only use recursive comparison for strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • since 28.0-Nickel
val set_builtin_eq : ?force:bool -> Fun.t -> (term -> term -> term) -> unit

Register a builtin equality for comparing any term with head-symbol. Must only use recursive comparison for strictly smaller terms. The recognized term with head function symbol is passed first.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

val set_builtin_leq : ?force:bool -> Fun.t -> (term -> term -> term) -> unit

Register a builtin for comparing any term with head-symbol. Must only use recursive comparison for strictly smaller terms. The recognized term with head function symbol can be on both sides. Strict comparison is automatically derived from the non-strict one.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

Specific Patterns

val consequence : term -> term -> term

Knowing h, consequence h a returns b such that h -> (a<->b)

val literal : term -> bool * term
val affine : term -> term Qed.Logic.affine
val record_with : record -> (term * record) option

Symbol

type t = term
val id : t -> int

unique identifier (stored in t)

val hash : t -> int

constant access (stored in t)

val equal : t -> t -> bool

physical equality

val compare : t -> t -> int

atoms are lower than complex terms ; otherwise, sorted by id.

val pretty : Stdlib.Format.formatter -> t -> unit
val weigth : t -> int

Informal size

Utilities

val is_closed : t -> bool

No bound variables

val is_simple : t -> bool

Constants, variables, functions of arity 0

val is_atomic : t -> bool

Constants and variables

val is_primitive : t -> bool

Constants only

val is_neutral : Fun.t -> t -> bool
val is_absorbant : Fun.t -> t -> bool
val size : t -> int
val basename : t -> string
val debug : Stdlib.Format.formatter -> t -> unit
val pp_id : Stdlib.Format.formatter -> t -> unit

internal id

val pp_rid : Stdlib.Format.formatter -> t -> unit

head symbol with children id's

val pp_repr : Stdlib.Format.formatter -> repr -> unit

head symbol with children id's

Shared sub-terms

val is_subterm : term -> term -> bool

Occurrence check. is_subterm a b returns true iff a is a subterm of b. Optimized wrt shared subterms, term size, and term variables.

val shared : ?shared:(term -> bool) -> ?shareable:(term -> bool) -> ?subterms:((term -> unit) -> term -> unit) -> term list -> term list

Computes the sub-terms that appear several times. shared marked linked e returns the shared subterms of e.

The list of shared subterms is consistent with order of definition: each trailing terms only depend on heading ones.

The traversal is controlled by two optional arguments:

  • shared those terms are not traversed (considered as atomic, default to none)
  • shareable those terms (is_simple excepted) that can be shared (default to all)
  • subterms those sub-terms a term to be considered during traversal (lc_iter by default)

Low-level shared primitives: shared is actually a combination of building marks, marking terms, and extracting definitions:

let share ?... e =
  let m = marks ?... () in
  List.iter (mark m) es ;
  defs m
type marks

Create a marking accumulator. Same defaults than shared.

val marks : ?shared:(term -> bool) -> ?shareable:(term -> bool) -> ?subterms:((term -> unit) -> term -> unit) -> unit -> marks
val mark : marks -> term -> unit

Mark a term to be printed

val share : marks -> term -> unit

Mark a term to be explicitly shared

val defs : marks -> term list

Returns a list of terms to be shared among all shared or marked subterms. The order of terms is consistent with definition order: head terms might be used in tail ones.