package dedukti

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

Install 

dune-project
 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