package dedukti

  1. Overview
  2. Docs
An implementation of The Lambda-Pi Modulo Theory

Install

Dune Dependency

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

Authors

  1. D
    dedukti-dev@inria.fr

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/dedukti.kernel/Kernel/Rule/index.html

Module Kernel.RuleSource

Rewrite rules

Patterns

Sourcetype pattern =
  1. | Var of Basic.loc * Basic.ident * int * pattern list
    (*

    Applied DB variable

    *)
  2. | Pattern of Basic.loc * Basic.name * pattern list
    (*

    Applied constant

    *)
  3. | Lambda of Basic.loc * Basic.ident * pattern
    (*

    Lambda abstraction

    *)
  4. | Brackets of Term.term
    (*

    Bracket of a term

    *)

Basic representation of pattern

Sourceval get_loc_pat : pattern -> Basic.loc
Sourceval pattern_to_term : pattern -> Term.term
Sourcetype wf_pattern =
  1. | LJoker
  2. | LVar of Basic.ident * int * int list
    (*

    Applied Miller variable

    *)
  3. | LLambda of Basic.ident * wf_pattern
    (*

    Lambda abstraction

    *)
  4. | LPattern of Basic.name * wf_pattern array
    (*

    Applied constant

    *)
  5. | LBoundVar of Basic.ident * int * wf_pattern array
    (*

    Locally bound variable

    *)
  6. | LACSet of Basic.name * wf_pattern list

Efficient representation for well-formed linear Miller pattern

Brackets

Sourcetype constr = int * Term.term

constr is the type of brackets (aka "dot") pattern constraints. They are generated by the function check_patterns. (i,te) means meta variable of DB index i should be convertible with te

Sourceval pp_constr : constr Basic.printer

Rewrite Rules

Sourcetype rule_name =
  1. | Beta
  2. | Delta of Basic.name
    (*

    Rules associated to the definition of a constant

    *)
  3. | Gamma of bool * Basic.name
    (*

    Rules of lambda pi modulo. The first parameter indicates whether the name of the rule has been given by the user.

    *)
Sourceval rule_name_eq : rule_name -> rule_name -> bool
Sourcetype 'a rule = {
  1. name : rule_name;
  2. ctx : 'a Term.context;
  3. pat : pattern;
  4. rhs : Term.term;
}

A rule is formed with

  • a name
  • an annotated context
  • a left-hand side pattern
  • a right-hand side term
Sourceval get_loc_rule : 'a rule -> Basic.loc
Sourcetype partially_typed_rule = Term.term option rule

Rule where context is partially annotated with types

Sourcetype typed_rule = Term.term rule

Rule where context is fully annotated with types

Sourcetype arity_rule = int rule

Rule where context is annotated with variable arities

Errors

Sourcetype rule_error =
  1. | BoundVariableExpected of Basic.loc * pattern
  2. | DistinctBoundVariablesExpected of Basic.loc * Basic.ident
  3. | VariableBoundOutsideTheGuard of Basic.loc * Term.term
  4. | UnboundVariable of Basic.loc * Basic.ident * pattern
  5. | AVariableIsNotAPattern of Basic.loc * Basic.ident
  6. | NonLinearNonEqArguments of Basic.loc * Basic.ident
  7. | NotEnoughArguments of Basic.loc * Basic.ident * int * int * int
  8. | NonLinearRule of Basic.loc * rule_name
Sourceexception Rule_error of rule_error

Rule infos

Sourcetype rule_infos = {
  1. l : Basic.loc;
    (*

    location of the rule

    *)
  2. name : rule_name;
    (*

    name of the rule

    *)
  3. nonlinear : int list;
    (*

    DB indices of non linear variables. Empty if the rule is linear ?

    *)
  4. cst : Basic.name;
    (*

    name of the pattern constant

    *)
  5. args : pattern list;
    (*

    arguments list of the pattern constant

    *)
  6. rhs : Term.term;
    (*

    right hand side of the rule

    *)
  7. ctx_size : int;
    (*

    size of the context of the non-linear version of the rule

    *)
  8. esize : int;
    (*

    size of the context of the linearized, bracket free version of the rule

    *)
  9. pats : wf_pattern array;
    (*

    free patterns without constraint

    *)
  10. arity : int array;
    (*

    arities of context variables

    *)
  11. constraints : constr list;
    (*

    constraints generated from the pattern to the free pattern

    *)
}
Sourceval infer_rule_context : rule_infos -> Term.arity_context

Extracts arity context from a rule info

Sourceval pattern_of_rule_infos : rule_infos -> pattern

Extracts LHS pattern from a rule info

Sourceval to_rule_infos : 'a rule -> rule_infos

Converts any rule (typed or untyped) to rule_infos

Sourceval untyped_rule_of_rule_infos : rule_infos -> partially_typed_rule

Converts rule_infos representation to a rule where the context is annotated with the variables' arity

Printing

Sourceval pp_rule_name : rule_name Basic.printer
Sourceval pp_untyped_rule : 'a rule Basic.printer
Sourceval pp_typed_rule : typed_rule Basic.printer
Sourceval pp_part_typed_rule : partially_typed_rule Basic.printer
Sourceval pp_pattern : pattern Basic.printer
Sourceval pp_wf_pattern : wf_pattern Basic.printer
Sourceval pp_rule_infos : rule_infos Basic.printer
Sourceval check_arity : rule_infos -> unit
Sourceval check_linearity : rule_infos -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct