package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

doc/lambdapi.parsing/Parsing/Scope/index.html

Module Parsing.ScopeSource

Scoping. Convert parsed terms in core terms by finding out which identifiers are bound variables or function symbol declared in open modules.

Sourceval scope_term : ?find_sym:Core.Sig_state.find_sym -> ?typ:bool -> ?mok:(int -> Core.Term.meta option) -> bool -> Core.Sig_state.sig_state -> Core.Env.env -> Syntax.p_term -> Core.Term.term

scope_term ~find_sym ~typ ~mok prv ss env t turns a pterm t into a term in the signature state ss and environment env (for bound variables). If prv is true, then the term must not contain any private subterms. If ~typ is true, then t must be a type (defaults to false). No new metavariables may appear in t, but metavariables in the image of mok may be used. The function mok defaults to the function constant to None. The function ~find_sym is used to scope symbol identifiers.

Sourceval scope_search_pattern : ?find_sym:Core.Sig_state.find_sym -> ?typ:bool -> ?mok:(int -> Core.Term.meta option) -> Core.Sig_state.sig_state -> Core.Env.env -> Syntax.p_term -> Core.Term.term

scope_search_pattern ~find_sym ~typ prv ss env t turns a pterm t meant to be a search patter into a term in the signature state ss and environment env (for bound variables). If ~typ is true, then t must be a type (defaults to false). No new metavariables may appear in t, but metavariables in the image of mok may be used. The function mok defaults to the function constant to None. The function ~find_sym is used to scope symbol identifiers.

Sourcetype pre_rule = {
  1. pr_sym : Core.Term.sym;
    (*

    Head symbol of the LHS.

    *)
  2. pr_lhs : Core.Term.term list;
    (*

    Arguments of the LHS.

    *)
  3. pr_vars : Core.Term.term_env Bindlib.mvar;
    (*

    Pattern variables that appear in the RHS. The last pr_xvars_nb variables do not appear in the LHS.

    *)
  4. pr_rhs : Core.Term.tbox;
    (*

    Body of the RHS, should only be unboxed once.

    *)
  5. pr_names : (int, string) Hashtbl.t;
    (*

    Gives the original name (if any) of pattern variable at given index.

    *)
  6. pr_arities : int array;
    (*

    Gives the arity of all the pattern variables in field pr_vars.

    *)
  7. pr_xvars_nb : int;
    (*

    Number of variables that appear in the RHS but not in the LHS.

    *)
}

Representation of a rewriting rule prior to SR-checking.

Sourceval rule_of_pre_rule : pre_rule Common.Pos.loc -> Core.Term.rule

rule_of_pre_rule r converts a pre-rewrite rule into a rewrite rule.

scope_rule ~find_sym ur ss r turns a parser-level rewriting rule r, or a unification rule if ur is true, into a pre-rewriting rule. The function ~find_sym is used to scope symbol identifiers.

scope_rw_patt ss env t turns a parser-level rewrite tactic specification s into an actual rewrite specification (possibly containing variables of env and using ss for aliasing).