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.2.17@m4x.org

Sources

2.1.tar.gz

md5=e72de75e9f0f87da9e6e8c0a4d4c89f9

sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

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

Module `Logtk_parsers.Ast_dk`

AST utils for dedukti

module A = Logtk.UntypedAST

module 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.

type location = Logtk.ParseLocation.t

type var = Logtk.STerm.var =

| V of string
| Wildcard

type t = private Logtk.STerm.t = {

term : view;
loc : location option;
attrs : attr list;

}

and match_branch = Logtk.STerm.match_branch =

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

and 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
| With 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
*)

and typed_var = var * t option

and attr = Logtk.STerm.attr =

| Attr_distinct_const

type term = t

val view : t -> view

val loc : t -> location option

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

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

val equal : t -> t -> bool

val hash : t -> int

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

val compare : t -> t -> int

val v_wild : t

wildcard

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

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

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

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

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

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

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

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

val with_ : ?loc:location -> (var * t) list -> t -> t

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

val nil : t

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

val at_loc : loc:location -> t -> t

val wildcard : t

val is_app : t -> bool

val is_var : t -> bool

val is_lam : t -> bool

val true_ : t

val false_ : t

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

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

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

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

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

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

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

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

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

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

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

val int_ : Logtk_arith.Z.t -> t

val of_int : int -> t

val rat : Logtk_arith.Q.t -> t

val real : string -> t

val tType : t

val term : t

val prop : t

val ty_int : t

val ty_rat : t

val ty_real : t

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

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

val ty_unfold : t -> t list * t

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

module Set = T.Set

module Map = T.Map

module Tbl = T.Tbl

module StringSet = T.StringSet

module Seq = T.Seq

val ground : t -> bool

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

Bind all free vars with the symbol

val 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

val pp : t CCFormat.printer

val to_string : t -> string

val pp_typed_var : typed_var CCFormat.printer

val pp_var : var CCFormat.printer

Formats

module TPTP = T.TPTP

module TPTP_THF = T.TPTP_THF

module ZF = T.ZF

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

Subst

module StrMap = T.StrMap

type subst = t StrMap.t

val empty_subst : subst

val merge_subst : subst -> subst -> subst

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

val apply_subst : subst -> term -> term

type statement = Logtk.UntypedAST.statement

type ty = T.t

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

val const : string -> T.t

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

val mk_const_t : string -> term

val var : string -> T.t

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

val mk_var_t : string -> term

val v : string -> var

val ty_aliases : (string, ty) Hashtbl.t

val find_alias : or_else:ty -> string -> ty

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

val type_nat : term

exception Unknown_builtin of string

exception Bad_arity of string * int

exception Application_head_is_not_a_var of term

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

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

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

val mk_arrow : T.t -> T.t -> T.t

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

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

val mk_int : string -> T.t

val ty_prop : T.t

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

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

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

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

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

On This Page

AST utils for dedukti