lambdapi
Library
Module
Module type
Parameter
Class
Class type
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.
type p_path = Common.Path.t Common.Pos.loc
Representation of a module name.
type p_qident = Core.Term.qident Common.Pos.loc
Representation of a possibly qualified (and located) identifier.
type p_term = p_term_aux Common.Pos.loc
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. *) |
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
p_get_args t
is like Core.Term.get_args
but on syntax-level terms.
type p_rule = p_rule_aux Common.Pos.loc
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 |
| 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_query = p_query_aux Common.Pos.loc
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.
type p_tactic = p_tactic_aux Common.Pos.loc
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.
type p_proof = p_subproof list
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.
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.
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;