dedukti 2.7 · OCaml Package

Rewrite rules

Patterns

type pattern =

| Var of Basic.loc * Basic.ident * int * pattern list
(*
Applied DB variable
*)
| Pattern of Basic.loc * Basic.name * pattern list
(*
Applied constant
*)
| Lambda of Basic.loc * Basic.ident * pattern
(*
Lambda abstraction
*)
| 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 =

| LJoker
| LVar of Basic.ident * int * int list
(*
Applied Miller variable
*)
| LLambda of Basic.ident * wf_pattern
(*
Lambda abstraction
*)
| LPattern of Basic.name * wf_pattern array
(*
Applied constant
*)
| LBoundVar of Basic.ident * int * wf_pattern array
(*
Locally bound variable
*)
| 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 =

| Beta
| Delta of Basic.name
(*
Rules associated to the definition of a constant
*)
| 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 = {

name : rule_name;
ctx : 'a Term.context;
pat : pattern;
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 =

| BoundVariableExpected of Basic.loc * pattern
| DistinctBoundVariablesExpected of Basic.loc * Basic.ident
| VariableBoundOutsideTheGuard of Basic.loc * Term.term
| UnboundVariable of Basic.loc * Basic.ident * pattern
| AVariableIsNotAPattern of Basic.loc * Basic.ident
| NonLinearNonEqArguments of Basic.loc * Basic.ident
| NotEnoughArguments of Basic.loc * Basic.ident * int * int * int
| NonLinearRule of Basic.loc * rule_name

exception Rule_error of rule_error

Rule infos

type rule_infos = {

l : Basic.loc;
(*
location of the rule
*)
name : rule_name;
(*
name of the rule
*)
nonlinear : int list;
(*
DB indices of non linear variables. Empty if the rule is linear ?
*)
cst : Basic.name;
(*
name of the pattern constant
*)
args : pattern list;
(*
arguments list of the pattern constant
*)
rhs : Term.term;
(*
right hand side of the rule
*)
ctx_size : int;
(*
size of the context of the non-linear version of the rule
*)
esize : int;
(*
size of the context of the linearized, bracket free version of the rule
*)
pats : wf_pattern array;
(*
free patterns without constraint
*)
arity : int array;
(*
arities of context variables
*)
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