lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library lambdapi.parsing
Module Parsing . Syntax
type p_ident = Common.Pos.strloc

Representation of a (located) identifier.

val check_notin : string -> p_ident option list -> unit

notin id idopts checks that id does not occur in idopts.

val check_distinct : p_ident option list -> unit

are_distinct idopts checks that the elements of idopts of the form Some _ are pairwise distinct.

type p_meta_ident = int Common.Pos.loc

Identifier of a metavariable.

Representation of a module name.

Representation of a possibly qualified (and located) identifier.

Parser-level (located) term representation.

and p_term_aux =
| P_Type(*

TYPE constant.

*)
| P_Iden of p_qident * bool(*

Identifier. The boolean indicates whether the identifier is prefixed by "@".

*)
| P_Wild(*

Underscore.

*)
| P_Meta of p_meta_ident * p_term array(*

Meta-variable with explicit substitution.

*)
| P_Patt of p_ident option * p_term array option(*

Pattern.

*)
| P_Appl of p_term * p_term(*

Application.

*)
| P_Arro of p_term * p_term(*

Arrow.

*)
| P_Abst of p_params list * p_term(*

Abstraction.

*)
| P_Prod of p_params list * p_term(*

Product.

*)
| P_LLet of p_ident * p_params list * p_term option * p_term * p_term(*

Let.

*)
| P_NLit of int(*

Natural number literal.

*)
| P_Wrap of p_term(*

Term between parentheses.

*)
| P_Expl of p_term(*

Term between curly brackets.

*)
and p_params = p_ident option list * p_term option * bool

Parser-level representation of a function argument. The boolean is true if the argument is marked as implicit (i.e., between curly braces).

val nb_params : p_params list -> int

nb_params ps returns the number of parameters in a list of parameters ps.

val get_impl_params_list : p_params list -> bool list

get_impl_params_list l gives the implicitness of l.

val get_impl_term : p_term -> bool list

get_impl_term t gives the implicitness of t.

val get_impl_term_aux : p_term_aux -> bool list
val p_get_args : p_term -> p_term * p_term list

p_get_args t is like Core.Term.get_args but on syntax-level terms.

type p_rule_aux = p_term * p_term

Parser-level rewriting rule representation.

type p_inductive_aux = p_ident * p_term * (p_ident * p_term) list

Parser-level inductive type representation.

type p_inductive = p_inductive_aux Common.Pos.loc
module P : sig ... end

Module to create p_term's with no positions.

type ('term, 'binder) rw_patt =
| Rw_Term of 'term
| Rw_InTerm of 'term
| Rw_InIdInTerm of 'binder
| Rw_IdInTerm of 'binder
| Rw_TermInIdInTerm of 'term * 'binder
| Rw_TermAsIdInTerm of 'term * 'binder

Rewrite patterns as in Coq/SSReflect. See "A Small Scale Reflection Extension for the Coq system", by Georges Gonthier, Assia Mahboubi and Enrico Tassi, INRIA Research Report 6455, 2016,

type p_rw_patt = ( p_term, p_ident * p_term ) rw_patt Common.Pos.loc
type p_assertion =
| P_assert_typing of p_term * p_term(*

The given term should have the given type.

*)
| P_assert_conv of p_term * p_term(*

The two given terms should be convertible.

*)

Parser-level representation of an assertion.

type p_query_aux =
| P_query_verbose of int(*

Sets the verbosity level.

*)
| P_query_debug of bool * string(*

Toggles logging functions described by string according to boolean.

*)
| P_query_flag of string * bool(*

Sets the boolean flag registered under the given name (if any).

*)
| P_query_assert of bool * p_assertion(*

Assertion (must fail if boolean is true).

*)
| P_query_infer of p_term * Core.Eval.strat(*

Type inference command.

*)
| P_query_normalize of p_term * Core.Eval.strat(*

Normalisation command.

*)
| P_query_prover of string(*

Set the prover to use inside a proof.

*)
| P_query_prover_timeout of int(*

Set the timeout of the prover (in seconds).

*)
| P_query_print of p_qident option(*

Print information about a symbol or the current goals.

*)
| P_query_proofterm(*

Print the current proof term (possibly containing open goals).

*)

Parser-level representation of a query command.

type p_tactic_aux =
| P_tac_admit
| P_tac_apply of p_term
| P_tac_assume of p_ident option list
| P_tac_fail
| P_tac_generalize of p_ident
| P_tac_have of p_ident * p_term
| P_tac_induction
| P_tac_query of p_query
| P_tac_refine of p_term
| P_tac_refl
| P_tac_rewrite of bool * p_rw_patt option * p_term
| P_tac_simpl of p_qident option
| P_tac_solve
| P_tac_sym
| P_tac_why3 of string option

Parser-level representation of a tactic.

val is_destructive : p_tactic_aux Common.Pos.loc -> bool

is_destructive t says whether tactic t changes the current goal.

type p_subproof = p_proofstep list

Parser-level representation of a proof.

and p_proofstep =
| Tactic of p_tactic * p_subproof list
type p_proof = p_subproof list
type p_proof_end_aux =
| P_proof_end(*

The proof is done and fully checked.

*)
| P_proof_admitted(*

Give up current state and admit the theorem.

*)
| P_proof_abort(*

Abort the proof (theorem not admitted).

*)
type p_proof_end = p_proof_end_aux Common.Pos.loc
type p_modifier_aux =
| P_mstrat of Core.Term.match_strat(*

pattern matching strategy

*)
| P_expo of Core.Term.expo(*

visibility of symbol outside its modules

*)
| P_prop of Core.Term.prop(*

symbol properties: constant, definable, ...

*)
| P_opaq(*

opacity

*)

Parser-level representation of modifiers.

type p_modifier = p_modifier_aux Common.Pos.loc
val is_prop : p_modifier_aux Common.Pos.loc -> bool
val is_opaq : p_modifier_aux Common.Pos.loc -> bool
val is_expo : p_modifier_aux Common.Pos.loc -> bool
val is_mstrat : p_modifier_aux Common.Pos.loc -> bool
type p_symbol = {
p_sym_mod : p_modifier list;(*

modifiers

*)
p_sym_nam : p_ident;(*

symbol name

*)
p_sym_arg : p_params list;(*

arguments before ":"

*)
p_sym_typ : p_term option;(*

symbol type

*)
p_sym_trm : p_term option;(*

symbol definition

*)
p_sym_prf : (p_proof * p_proof_end) option;(*

proof script

*)
p_sym_def : bool;(*

is it a definition ?

*)
}

Parser-level representation of symbol declarations.

type p_command_aux =
| P_require of bool * p_path list
| P_require_as of p_path * p_ident
| P_open of p_path list
| P_symbol of p_symbol
| P_rules of p_rule list
| P_inductive of p_modifier list * p_params list * p_inductive list
| P_builtin of string * p_qident
| P_notation of p_qident * Core.Sign.notation
| P_unif_rule of p_rule
| P_query of p_query

Parser-level representation of a single command.

type p_command = p_command_aux Common.Pos.loc

Parser-level representation of a single (located) command.

type ast = p_command Stream.t

Top level AST returned by the parser.

Equality functions on the syntactic expressions ignoring positions.

val eq_p_ident : p_ident Lplib.Base.eq
val eq_p_meta_ident : p_meta_ident Lplib.Base.eq
val eq_p_qident : p_qident Lplib.Base.eq
val eq_p_path : p_path Lplib.Base.eq
val eq_p_term : p_term Lplib.Base.eq
val eq_p_params : p_params Lplib.Base.eq
val eq_p_rule : p_rule Lplib.Base.eq
val eq_p_inductive : p_inductive Lplib.Base.eq
val eq_p_rw_patt : p_rw_patt Lplib.Base.eq
val eq_p_assertion : p_assertion Lplib.Base.eq
val eq_p_query : p_query Lplib.Base.eq
val eq_p_tactic : p_tactic Lplib.Base.eq
val eq_p_subproof : p_subproof Lplib.Base.eq
val eq_p_proofstep : p_proofstep Lplib.Base.eq
val eq_p_proof : p_proof Lplib.Base.eq
val eq_p_sym_prf : (p_proof * p_proof_end) Lplib.Base.eq
val eq_p_symbol : p_symbol Lplib.Base.eq
val eq_p_command : p_command Lplib.Base.eq

eq_command c1 c2 tells whether c1 and c2 are the same commands. They are compared up to source code positions.

val fold_proof : ( 'a -> p_tactic -> int -> 'a ) -> 'a -> p_proof -> 'a

fold_proof f acc p recursively builds a value of type 'a by starting from acc and by applying f to every tactic of p.

fold_idents f a ast allows to recursively build a value of type 'a starting from a and by applying f on each identifier occurring in ast corresponding to a function symbol: variables (term variables or assumption names) are excluded.

NOTE: This function is incomplete if an assumption name hides a function symbol. Example:

symbol A:TYPE; symbol a:A; symbol p:((A->A)->A->A)->A := begin assume h apply h // proof of A->A assume a apply a // here a is an assumption // proof of A apply a // here a is a function symbol end;

val fold_idents : ( 'a -> p_qident -> 'a ) -> 'a -> p_command list -> 'a