package lambdapi

  1. Overview
  2. Docs
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parser-level abstract 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 =
  1. | P_Type
    (*

    TYPE constant.

    *)
  2. | P_Iden of p_qident * bool
    (*

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

    *)
  3. | P_Wild
    (*

    Underscore.

    *)
  4. | P_Meta of p_meta_ident * p_term array
    (*

    Meta-variable with explicit substitution.

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

    Pattern.

    *)
  6. | P_Appl of p_term * p_term
    (*

    Application.

    *)
  7. | P_Arro of p_term * p_term
    (*

    Arrow.

    *)
  8. | P_Abst of p_params list * p_term
    (*

    Abstraction.

    *)
  9. | P_Prod of p_params list * p_term
    (*

    Product.

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

    Let.

    *)
  11. | P_NLit of int
    (*

    Natural number literal.

    *)
  12. | P_Wrap of p_term
    (*

    Term between parentheses.

    *)
  13. | 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 =
  1. | Rw_Term of 'term
  2. | Rw_InTerm of 'term
  3. | Rw_InIdInTerm of 'binder
  4. | Rw_IdInTerm of 'binder
  5. | Rw_TermInIdInTerm of 'term * 'binder
  6. | 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_assertion =
  1. | P_assert_typing of p_term * p_term
    (*

    The given term should have the given type.

    *)
  2. | 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 =
  1. | P_query_verbose of int
    (*

    Sets the verbosity level.

    *)
  2. | P_query_debug of bool * string
    (*

    Toggles logging functions described by string according to boolean.

    *)
  3. | P_query_flag of string * bool
    (*

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

    *)
  4. | P_query_assert of bool * p_assertion
    (*

    Assertion (must fail if boolean is true).

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

    Type inference command.

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

    Normalisation command.

    *)
  7. | P_query_prover of string
    (*

    Set the prover to use inside a proof.

    *)
  8. | P_query_prover_timeout of int
    (*

    Set the timeout of the prover (in seconds).

    *)
  9. | P_query_print of p_qident option
    (*

    Print information about a symbol or the current goals.

    *)
  10. | P_query_proofterm
    (*

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

    *)

Parser-level representation of a query command.

type p_tactic_aux =
  1. | P_tac_admit
  2. | P_tac_apply of p_term
  3. | P_tac_assume of p_ident option list
  4. | P_tac_fail
  5. | P_tac_generalize of p_ident
  6. | P_tac_have of p_ident * p_term
  7. | P_tac_induction
  8. | P_tac_query of p_query
  9. | P_tac_refine of p_term
  10. | P_tac_refl
  11. | P_tac_rewrite of bool * p_rw_patt option * p_term
  12. | P_tac_simpl of p_qident option
  13. | P_tac_solve
  14. | P_tac_sym
  15. | 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 =
  1. | Tactic of p_tactic * p_subproof list
type p_proof = p_subproof list
type p_proof_end_aux =
  1. | P_proof_end
    (*

    The proof is done and fully checked.

    *)
  2. | P_proof_admitted
    (*

    Give up current state and admit the theorem.

    *)
  3. | P_proof_abort
    (*

    Abort the proof (theorem not admitted).

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

    pattern matching strategy

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

    visibility of symbol outside its modules

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

    symbol properties: constant, definable, ...

    *)
  4. | 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 = {
  1. p_sym_mod : p_modifier list;
    (*

    modifiers

    *)
  2. p_sym_nam : p_ident;
    (*

    symbol name

    *)
  3. p_sym_arg : p_params list;
    (*

    arguments before ":"

    *)
  4. p_sym_typ : p_term option;
    (*

    symbol type

    *)
  5. p_sym_trm : p_term option;
    (*

    symbol definition

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

    proof script

    *)
  7. p_sym_def : bool;
    (*

    is it a definition ?

    *)
}

Parser-level representation of symbol declarations.

type p_command_aux =
  1. | P_require of bool * p_path list
  2. | P_require_as of p_path * p_ident
  3. | P_open of p_path list
  4. | P_symbol of p_symbol
  5. | P_rules of p_rule list
  6. | P_inductive of p_modifier list * p_params list * p_inductive list
  7. | P_builtin of string * p_qident
  8. | P_notation of p_qident * Core.Sign.notation
  9. | P_unif_rule of p_rule
  10. | 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