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/Dtree/index.html

Module Kernel.DtreeSource

Error

Sourcetype dtree_error =
  1. | HeadSymbolMismatch of Basic.loc * Basic.name * Basic.name
  2. | ArityInnerMismatch of Basic.loc * Basic.ident * Basic.ident
  3. | ACSymbolRewritten of Basic.loc * Basic.name * int
Sourceexception Dtree_error of dtree_error
Sourcetype miller_var = {
  1. arity : int;
    (*

    Arity of the meta variable

    *)
  2. depth : int;
    (*

    Depth under which this occurence of the meta variable is considered

    *)
  3. vars : int list;
    (*

    The list of local DB indices of argument variables

    *)
  4. mapping : int array;
    (*

    The mapping from all local DB indices for either -1 or position in the list of argument variables (starting from the end)

    *)
}

This represent a meta variables applied to distinct locally bounded variables: X x_1 ... x_n.

  • arity is the number of arguments
  • depth is the number of locally bounded variables available
  • vars is the list of successive arguments in order
  • mapping is a mapping for all available bounded variable n to
  • either -1 is this variable is absent from the list of arguments
  • or the index of that integer in the vars list

The following invariants should therefore be verified:

  • arity is the length of vars
  • depth is the length of mapping
  • All elements of vars are between 0 and depth-1
  • Non negative elements of mapping are between 0 and arity-1
  • mapping.(i) = n >= 0 iff List.nth vars (arity-n-1) = i
  • This means exactly arity elements of mapping are non negative

An example: { arity = 2; depth = 5; vars = 4; 2; mapping = | (-1) ; (-1) ; 0 ; (-1) ; 1 | }

Sourceval mapping_of_vars : int -> int -> int list -> int array

mapping_of_vars depth arity vars build a reverse mapping from the list vars of DB indices arguments of a Miller variable. For instance the pattern x => y => z => F y x produces a call to mapping_of_vars 3 2 [1; 0] which returns the array | 1 ; 0 ; (-1) |

Sourceval fo_var : miller_var

Pre-Matching problems

Abstract matching problems. This can be instantiated with

  • When building a decision tree 'a = int refers to positions in the stack
  • When matching against a term, 'a = term Lazy.t refers to actual terms
Sourcetype 'a eq_problem = miller_var * 'a

(vars, matched) is the higher order equational problem: X x1 ... xn = matched with vars=[ x1 ; ... ; xn ]

Sourcetype var_p = int * miller_var

(n, vars) represents the n-th variable applied to the vars bound variables.

Sourcetype 'a ac_problem = int * Ac.ac_ident * int * var_p list * 'a

(depth, symb, njoks, vars, terms) Represents the flattenned equality under AC symbol symb of:

  • njoks jokers and the given variables vars
  • The given terms e.g. +{ X[x] , _, Y[y,z] } = +{ f(a), f(y), f(x)} the depth field in all elements of vars should be equal to depth FIXME: do we need depth here then ?
Sourcetype pre_matching_problem = {
  1. pm_eq_problems : int eq_problem list Basic.LList.t;
    (*

    For each variable of a rewrite rule (array), a list of equational problems under various depths

    *)
  2. pm_ac_problems : int ac_problem list;
    (*

    A list of AC-matching problems under a certain depth

    *)
  3. pm_arity : int array;
    (*

    Constant time access to a variable's arity

    *)
}

A problem with int indices referencing positions in the stack

Sourceval pp_var_type : var_p Basic.printer
Sourceval pp_eq_problems : string -> 'a Basic.printer -> (int * 'a eq_problem list) Basic.printer
Sourceval pp_ac_problem : 'a Basic.printer -> 'a ac_problem Basic.printer
Sourceval pp_pre_matching_problem : string -> pre_matching_problem Basic.printer

int matching problem printing function (for dtree).

Decision Trees

Sourcetype case =
  1. | CConst of int * Basic.name * bool
    (*

    (size,name,ac) where size is the number of arguments expected for the constant c and ac is true iff the constant is a definable AC(U) symbol.

    *)
  2. | CDB of int * int
    (*

    (size,db_index) where size is the number of *static* arguments expected for the bounded variable db_index

    *)
  3. | CLam
    (*

    A lambda headed term

    *)

Arguments of a pattern may be the following:

  • a constant
  • a variable
  • a lambda expression
Sourcetype atomic_problem = {
  1. a_pos : int;
    (*

    position of the term to match in the stack.

    *)
  2. a_depth : int;
    (*

    depth of the argument regarding absractions

    *)
  3. a_args : int array;
    (*

    Arguments DB indices (distinct bound variables)

    *)
}

An atomic matching problem. stack.(pos) ~? X DB(args_0), ..., DB(args_n) where X is the variable and the problem is considered under depth abstractions.

Sourcetype matching_problem = atomic_problem Basic.LList.t

A matching problem to build a solution context from the stack

Sourcetype dtree =
  1. | Switch of int * (case * dtree) list * dtree option
    (*

    Switch i [(case_0,tree_0) ; ... ; (case_n, tree_n)] default_tree tests whether the i-th argument in the stack matches with one of the given cases. If it does then proceed with the corresponding tree Otherwise, branch to the given default tree.

    *)
  2. | Test of Rule.rule_name * pre_matching_problem * Rule.constr list * Term.term * dtree option
    (*

    Test name pb cstrs rhs default_tree are the leaves of the tree. Checks that each problem can be solved such that constraints are satisfied. If it does then return a local context for the term rhs.

    *)
  3. | Fetch of int * case * dtree * dtree option
    (*

    Fetch i case tree_suc tree_def assumes the i-th argument of a pattern is a * flattened AC symbols and checks that it contains a term that can be matched with the given * case. * If so then look at the corresponding tree, otherwise/afterwise, look at the default tree

    *)
  4. | ACEmpty of int * dtree * dtree option
    (*

    ACEmpty i tree_suc tree_def assumes the i-th argument of a pattern is a * flattened AC symbols and checks that it is now empty.

    *)

Type of decision trees

Sourcetype t

Type mapping arities to decision trees (also called "forest")

Sourceval empty : t

Empty forest for a free algebra

Sourceval find_dtree : int -> t -> Term.algebra * (int * dtree) option

find_dtree ar forest returns a pair (arity,dtree) in given forest such that arity <= ar. Returns None when not found.

Sourceval pp_dtree : dtree Basic.printer

Printer for a single decision tree.

Sourceval pp_dforest : t Basic.printer

Printer for forests of decision trees.

Sourceval of_rules : Basic.name -> (Basic.name -> Term.algebra) -> Rule.rule_infos list -> t

Compilation of rewrite rules into decision trees. Returns a list of arities and corresponding decision trees. Invariant : arities must be sorted in decreasing order. (see use case in state_whnf in reduction.ml) May raise Dtree_error.