lambdapi 2.3.1 · OCaml Package

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.

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 string
(*
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_rule = p_rule_aux Common.Pos.loc

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,

see http://hal.inria.fr/inria-00258384
, section 8, p. 48.

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 string
(*
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 string
(*
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.

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 * string Core.Sign.notation
| P_unif_rule of p_rule
| P_coercion 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

package lambdapi