package dedukti

  1. Overview
  2. Docs

Rewrite rules

Patterns

type 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

val get_loc_pat : pattern -> Basic.loc
val pattern_to_term : pattern -> Term.term
type 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

type 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

val pp_constr : constr Basic.printer

Rewrite Rules

type 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.

    *)
val rule_name_eq : rule_name -> rule_name -> bool
type '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
val get_loc_rule : 'a rule -> Basic.loc
type partially_typed_rule = Term.term option rule

Rule where context is partially annotated with types

type typed_rule = Term.term rule

Rule where context is fully annotated with types

type arity_rule = int rule

Rule where context is annotated with variable arities

Errors

type 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
exception Rule_error of rule_error

Rule infos

type 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

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

Extracts arity context from a rule info

val pattern_of_rule_infos : rule_infos -> pattern

Extracts LHS pattern from a rule info

val to_rule_infos : 'a rule -> rule_infos

Converts any rule (typed or untyped) to rule_infos

val 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

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