dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Rule
type pattern =
| Var of Basic.loc * Basic.ident * int * pattern list
| Pattern of Basic.loc * Basic.name * pattern list
| Lambda of Basic.loc * Basic.ident * pattern
| Brackets of Term.term
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
| LLambda of Basic.ident * wf_pattern
| LPattern of Basic.name * wf_pattern array
| LBoundVar of Basic.ident * int * wf_pattern array
val allow_non_linear : bool ref
type constr =
| Linearity of int * int
| Bracket of int * Term.term
type rule_name =
| Delta of Basic.name
| Gamma of bool * Basic.name
type !'a rule = {
name : rule_name;
ctx : 'a;
pat : pattern;
rhs : Term.term;
}
type untyped_rule = Term.untyped_context rule
type typed_rule = Term.typed_context rule
type rule_error =
| BoundVariableExpected of pattern
| DistinctBoundVariablesExpected of Basic.loc * Basic.ident
| VariableBoundOutsideTheGuard of Term.term
| UnboundVariable of Basic.loc * Basic.ident * pattern
| AVariableIsNotAPattern of Basic.loc * Basic.ident
| NonLinearRule of untyped_rule
| NotEnoughArguments of Basic.loc * Basic.ident * int * int * int
| NonLinearNonEqArguments of Basic.loc * Basic.ident
type rule_infos = {
l : Basic.loc;
name : rule_name;
cst : Basic.name;
args : pattern list;
rhs : Term.term;
esize : int;
pats : wf_pattern array;
constraints : constr list;
}
val pattern_of_rule_infos : rule_infos -> pattern
val to_rule_infos : untyped_rule -> ( rule_infos, rule_error ) Basic.error
val pp_rule_name : rule_name Basic.printer
val pp_untyped_rule : untyped_rule Basic.printer
val pp_typed_rule : typed_rule Basic.printer
val pp_pattern : pattern Basic.printer
val pp_wf_pattern : wf_pattern Basic.printer
val pp_untyped_context : Term.untyped_context Basic.printer
val pp_typed_context : Term.typed_context Basic.printer
val pp_rule_infos : rule_infos Basic.printer