package logtk

You can search for identifiers within the package.

in-package search v0.2.0

Core types and algorithms for logic

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

1.6.tar.gz

md5=97cdb2f90468e9e27c7bbe3b4fb160bb

sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d

doc/logtk.parsers/Logtk_parsers/Ast_dk/index.html

Module `Logtk_parsers.Ast_dk`Source

AST utils for dedukti

Sourcemodule A = Logtk.UntypedAST

Sourcemodule T = Logtk.STerm

include module type of struct include T end

Simple Terms

.

Simple terms, that are not hashconsed, nor typed.

Those do not use De Bruijn indices for variable binding, but simply names (scoping is done later). Their simplicity make them good for heavy AST transformations, output of parsing, etc.

Terms are only compared, hashsed, etc. by their "term" component (the algebraic variant). Additional fields (location…) are ignored for almost every operation.

Sourcetype location = Logtk.ParseLocation.t

Sourcetype var = Logtk.STerm.var =

| V of string
| Wildcard

Sourcetype t = private Logtk.STerm.t = {

term : view;
loc : location option;

}

Sourceand match_branch = Logtk.STerm.match_branch =

| Match_case of string * var list * t
| Match_default of t

Sourceand view = Logtk.STerm.view =

| Var of var
(*
variable
*)
| Const of string
(*
constant
*)
| AppBuiltin of Logtk.Builtin.t * t list
| App of t * t list
(*
apply term
*)
| Ite of t * t * t
| Match of t * match_branch list
| Let of (var * t) list * t
| Bind of Logtk.Binder.t * typed_var list * t
(*
bind n variables
*)
| List of t list
(*
special constructor for lists
*)
| Record of (string * t) list * var option
(*
extensible record
*)

Sourceand typed_var = var * t option

Sourcetype term = t

Sourceval view : t -> view

Sourceval loc : t -> location option

include Logtk.Interfaces.HASH with type t := t

include Logtk.Interfaces.EQ with type t := t

Sourceval equal : t -> t -> bool

Sourceval hash : t -> int

include Logtk.Interfaces.ORD with type t := t

Sourceval compare : t -> t -> int

Sourceval v_wild : t

wildcard

Sourceval app : ?loc:location -> t -> t list -> t

Sourceval app_const : ?loc:location -> string -> t list -> t

Sourceval builtin : ?loc:location -> Logtk.Builtin.t -> t

Sourceval app_builtin : ?loc:location -> Logtk.Builtin.t -> t list -> t

Sourceval bind : ?loc:location -> Logtk.Binder.t -> typed_var list -> t -> t

Sourceval ite : ?loc:location -> t -> t -> t -> t

Sourceval match_ : ?loc:location -> t -> match_branch list -> t

Sourceval let_ : ?loc:location -> (var * t) list -> t -> t

Sourceval list_ : ?loc:location -> t list -> t

Sourceval nil : t

Sourceval record : ?loc:location -> (string * t) list -> rest:var option -> t

Sourceval at_loc : loc:location -> t -> t

Sourceval wildcard : t

Sourceval is_app : t -> bool

Sourceval is_var : t -> bool

Sourceval true_ : t

Sourceval false_ : t

Sourceval and_ : ?loc:location -> t list -> t

Sourceval or_ : ?loc:location -> t list -> t

Sourceval not_ : ?loc:location -> t -> t

Sourceval equiv : ?loc:location -> t -> t -> t

Sourceval xor : ?loc:location -> t -> t -> t

Sourceval imply : ?loc:location -> t -> t -> t

Sourceval eq : ?loc:location -> t -> t -> t

Sourceval neq : ?loc:location -> t -> t -> t

Sourceval forall : ?loc:location -> typed_var list -> t -> t

Sourceval exists : ?loc:location -> typed_var list -> t -> t

Sourceval lambda : ?loc:location -> typed_var list -> t -> t

Sourceval int_ : Z.t -> t

Sourceval of_int : int -> t

Sourceval rat : Q.t -> t

Sourceval real : string -> t

Sourceval tType : t

Sourceval term : t

Sourceval prop : t

Sourceval ty_int : t

Sourceval ty_rat : t

Sourceval ty_real : t

Sourceval fun_ty : ?loc:location -> t list -> t -> t

Sourceval forall_ty : ?loc:location -> typed_var list -> t -> t

Sourceval ty_unfold : t -> t list * t

Sourceval unfold_bind : Logtk.Binder.t -> t -> typed_var list * t

Sourcemodule Set = T.Set

Sourcemodule Map = T.Map

Sourcemodule Tbl = T.Tbl

Sourcemodule StringSet = T.StringSet

Sourcemodule Seq = T.Seq

Sourceval ground : t -> bool

Sourceval close_all : Logtk.Binder.t -> t -> t

Bind all free vars with the symbol

Sourceval subterm : strict:bool -> t -> sub:t -> bool

is sub a (strict?) subterm of the other arg?

Print

include Logtk.Interfaces.PRINT with type t := t

Sourceval pp : t CCFormat.printer

Sourceval to_string : t -> string

Sourceval pp_typed_var : typed_var CCFormat.printer

Sourceval pp_var : var CCFormat.printer

Formats

Sourcemodule TPTP = T.TPTP

Sourcemodule TPTP_THF = T.TPTP_THF

Sourcemodule ZF = T.ZF

Sourceval pp_in : Logtk.Output_format.t -> t CCFormat.printer

Subst

Sourcemodule StrMap = T.StrMap

Sourcetype subst = t StrMap.t

Sourceval empty_subst : subst

Sourceval merge_subst : subst -> subst -> subst

merge a b merges a into b, but favors b in case of conflict

Sourceval apply_subst : subst -> term -> term

Sourcetype statement = Logtk.UntypedAST.statement

Sourcetype ty = T.t

Sourceval cast : T.t -> T.t -> term

Sourceval const : string -> T.t

Sourceval mk_const : string -> T.t -> term

Sourceval mk_const_t : string -> term

Sourceval var : string -> T.t

Sourceval mk_var : string -> T.t -> term

Sourceval mk_var_t : string -> term

Sourceval v : string -> var

Sourceval ty_aliases : (string, ty) Hashtbl.t

Sourceval find_alias : or_else:ty -> string -> ty

Sourceval add_alias : string -> T.t -> unit

Sourceval type_nat : term

Sourceexception Unknown_builtin of string

Sourceexception Bad_arity of string * int

Sourceexception Application_head_is_not_a_var of term

Sourceval mk_app : T.t -> T.t list -> T.t

Sourceval mk_app_const : string -> T.t list -> T.t

Sourceval mk_arrow_l : T.t list -> T.t -> T.t

Sourceval mk_arrow : T.t -> T.t -> T.t

Sourceval mk_fun : T.typed_var list -> T.t -> T.t

Sourceval mk_forall : T.typed_var list -> T.t -> T.t

Sourceval mk_int : string -> T.t

Sourceval ty_prop : T.t

Sourceval mk_ty_decl : ?loc:A.Loc.t -> string -> A.ty -> A.statement

Sourceval mk_assert : ?loc:A.Loc.t -> name:string -> A.term -> A.statement

Sourceval mk_goal : ?loc:A.Loc.t -> name:string -> A.term -> A.statement

Sourceval mk_def : ?loc:A.Loc.t -> string -> A.ty -> T.t -> A.statement

Sourceval mk_rewrite : ?loc:A.Loc.t -> A.term -> A.statement

On This Page

AST utils for dedukti