package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Lang.FSource

Sourcemodule QED : Qed.Logic.Term with module ADT = ADT and module Field = Field and module Fun = Fun

Types and Variables

Sourcetype var = QED.var
Sourcetype tau = QED.tau
Sourcetype pool = QED.pool
Sourcemodule Tau = QED.Tau
Sourcemodule Var = QED.Var
Sourcemodule Vars : Qed.Idxset.S with type elt = var
Sourcemodule Vmap : Qed.Idxmap.S with type key = var
Sourceval pool : ?copy:pool -> unit -> pool
Sourceval fresh : pool -> ?basename:string -> tau -> var
Sourceval alpha : pool -> var -> var
Sourceval add_var : pool -> var -> unit
Sourceval add_vars : pool -> Vars.t -> unit
Sourceval tau_of_var : var -> tau

Expressions

Sourcetype term = QED.term
Sourcetype record = (field * term) list
Sourceval hash : term -> int

Constant time

Sourceval equal : term -> term -> bool

Same as ==

Sourceval compare : term -> term -> int
Sourcemodule Tset : Qed.Idxset.S with type elt = term
Sourcemodule Tmap : Qed.Idxmap.S with type key = term
Sourcetype unop = term -> term
Sourcetype binop = term -> term -> term
Sourceval e_zero : term
Sourceval e_one : term
Sourceval e_minus_one : term
Sourceval e_minus_one_real : term
Sourceval e_one_real : term
Sourceval e_zero_real : term
Sourceval constant : term -> term
Sourceval e_fact : int -> term -> term
Sourceval e_int64 : int64 -> term
Sourceval e_float : float -> term
Sourceval e_setfield : term -> field -> term -> term
Sourceval e_range : term -> term -> term

e_range a b = b+1-a

Sourceval is_zero : term -> bool
Sourceval e_true : term
Sourceval e_false : term
Sourceval e_bool : bool -> term
Sourceval e_literal : bool -> term -> term
Sourceval e_int : int -> term
Sourceval e_zint : Z.t -> term
Sourceval e_real : Q.t -> term
Sourceval e_var : var -> term
Sourceval e_opp : term -> term
Sourceval e_times : Z.t -> term -> term
Sourceval e_sum : term list -> term
Sourceval e_prod : term list -> term
Sourceval e_add : term -> term -> term
Sourceval e_sub : term -> term -> term
Sourceval e_mul : term -> term -> term
Sourceval e_div : term -> term -> term
Sourceval e_mod : term -> term -> term
Sourceval e_eq : term -> term -> term
Sourceval e_neq : term -> term -> term
Sourceval e_leq : term -> term -> term
Sourceval e_lt : term -> term -> term
Sourceval e_imply : term list -> term -> term
Sourceval e_equiv : term -> term -> term
Sourceval e_and : term list -> term
Sourceval e_or : term list -> term
Sourceval e_not : term -> term
Sourceval e_if : term -> term -> term -> term
Sourceval e_const : tau -> term -> term
Sourceval e_get : term -> term -> term
Sourceval e_set : term -> term -> term -> term
Sourceval e_getfield : term -> Field.t -> term
Sourceval e_record : record -> term
Sourceval e_fun : ?result:tau -> Fun.t -> term list -> term
Sourceval e_bind : Qed.Logic.binder -> var -> term -> term
Sourceval 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.

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

Closes all specified binders

Predicates

Sourcetype pred
Sourcetype cmp = term -> term -> pred
Sourcetype operator = pred -> pred -> pred
Sourcemodule Pmap : Qed.Idxmap.S with type key = pred
Sourcemodule Pset : Qed.Idxset.S with type elt = pred
Sourceval p_true : pred
Sourceval p_false : pred
Sourceval p_equal : term -> term -> pred
Sourceval p_equals : (term * term) list -> pred list
Sourceval p_neq : term -> term -> pred
Sourceval p_leq : term -> term -> pred
Sourceval p_lt : term -> term -> pred
Sourceval p_positive : term -> pred
Sourceval is_ptrue : pred -> Qed.Logic.maybe
Sourceval is_pfalse : pred -> Qed.Logic.maybe
Sourceval is_equal : term -> term -> Qed.Logic.maybe
Sourceval eqp : pred -> pred -> bool
Sourceval comparep : pred -> pred -> int
Sourceval p_bool : term -> pred
Sourceval e_prop : pred -> term
Sourceval p_bools : term list -> pred list
Sourceval e_props : pred list -> term list
Sourceval e_lift : (term -> term) -> pred -> pred
Sourceval p_lift : (pred -> pred) -> term -> term
Sourceval p_not : pred -> pred
Sourceval p_and : pred -> pred -> pred
Sourceval p_or : pred -> pred -> pred
Sourceval p_imply : pred -> pred -> pred
Sourceval p_equiv : pred -> pred -> pred
Sourceval p_hyps : pred list -> pred -> pred
Sourceval p_if : pred -> pred -> pred -> pred
Sourceval p_conj : pred list -> pred
Sourceval p_disj : pred list -> pred
Sourceval p_any : ('a -> pred) -> 'a list -> pred
Sourceval p_all : ('a -> pred) -> 'a list -> pred
Sourceval p_call : lfun -> term list -> pred
Sourceval e_lambda : var list -> term -> term
Sourceval e_apply : term -> term list -> term
Sourceval p_forall : var list -> pred -> pred
Sourceval p_exists : var list -> pred -> pred
Sourceval p_bind : Qed.Logic.binder -> var -> pred -> pred
Sourcetype sigma
Sourcemodule Subst : sig ... end
Sourceval e_subst : sigma -> term -> term
Sourceval p_subst : sigma -> pred -> pred
Sourceval p_subst_var : var -> term -> pred -> pred
Sourceval e_vars : term -> var list

Sorted

Sourceval p_vars : pred -> var list

Sorted

Sourceval p_close : pred -> pred

Quantify over (sorted) free variables

Sourceval pp_tau : Format.formatter -> tau -> unit
Sourceval pp_var : Format.formatter -> var -> unit
Sourceval pp_vars : Format.formatter -> Vars.t -> unit
Sourceval pp_term : Format.formatter -> term -> unit
Sourceval pp_pred : Format.formatter -> pred -> unit
Sourceval debugp : Format.formatter -> pred -> unit
Sourcetype env
Sourceval context_pp : env Context.value

Context used by pp_term, pp_pred, pp_var, ppvars for printing the term. Allows to keep the same disambiguation.

Sourcetype marks = QED.marks
Sourceval env : Vars.t -> env
Sourceval marker : env -> marks
Sourceval mark_e : marks -> term -> unit
Sourceval mark_p : marks -> pred -> unit

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.

Sourceval defs : marks -> term list
Sourceval define : (env -> string -> term -> unit) -> env -> marks -> env
Sourceval pp_eterm : env -> Format.formatter -> term -> unit
Sourceval pp_epred : env -> Format.formatter -> pred -> unit

Binders

Sourceval lc_closed : term -> bool
Sourceval lc_iter : (term -> unit) -> term -> unit

Utilities

Sourceval decide : term -> bool

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

Sourceval basename : term -> string
Sourceval is_true : term -> Qed.Logic.maybe

Constant time.

Sourceval is_false : term -> Qed.Logic.maybe

Constant time.

Sourceval is_prop : term -> bool

Boolean or Property

Sourceval is_int : term -> bool

Integer sort

Sourceval is_real : term -> bool

Real sort

Sourceval is_arith : term -> bool

Integer or Real sort

Sourceval is_closed : term -> bool

No bound variables

Sourceval is_simple : term -> bool

Constants, variables, functions of arity 0

Sourceval is_atomic : term -> bool

Constants and variables

Sourceval is_primitive : term -> bool

Constants only

Sourceval is_neutral : Fun.t -> term -> bool
Sourceval is_absorbant : Fun.t -> term -> bool
Sourceval record_with : record -> (term * record) option
Sourceval are_equal : term -> term -> Qed.Logic.maybe

Computes equality

Sourceval eval_eq : term -> term -> bool

Same as are_equal is Yes

Sourceval eval_neq : term -> term -> bool

Same as are_equal is No

Sourceval eval_lt : term -> term -> bool

Same as e_lt is e_true

Sourceval eval_leq : term -> term -> bool

Same as e_leq is e_true

Sourceval repr : term -> QED.repr

Constant time

Constant time

Sourceval vars : term -> Vars.t

Constant time

Sourceval varsp : pred -> Vars.t

Constant time

Sourceval occurs : var -> term -> bool
Sourceval occursp : var -> pred -> bool
Sourceval intersect : term -> term -> bool
Sourceval intersectp : pred -> pred -> bool
Sourceval is_subterm : term -> term -> bool
Sourceval 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

Builtins

The functions below register simplifiers 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.

Sourceval set_builtin : lfun -> (term list -> term) -> unit
Sourceval set_builtin_get : lfun -> (term list -> term list -> term) -> unit
Sourceval set_builtin_field : lfun -> field -> (term list -> term) -> unit
Sourceval set_builtin_1 : lfun -> unop -> unit
Sourceval set_builtin_2 : lfun -> binop -> unit
Sourceval set_builtin_2' : lfun -> (term -> term -> tau option -> term) -> unit
Sourceval set_builtin_eq : lfun -> binop -> unit
Sourceval set_builtin_leq : lfun -> binop -> unit
Sourceval set_builtin_eqp : lfun -> cmp -> unit
Sourceval release : unit -> unit

Empty local caches

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct