package dedukti

An environment is created from a Parser.input. Environment is the module which interacts with the kernel. An environment allows you to change at runtime the reduction engine and the printer. The current version of Dedukti offers you one reduction engine, but this feature is mainly aim to be used with the dkmeta tool. The printer of Env is different from Pp in a sense that the module of a constant is not printed if it is the same as the current module.

dummy ?m () returns a dummy environment. If m is provided, the environment is built from module m, but without file.

Sets multiple debugging flags from a string: q : disables d_Warn n : enables d_Notice o : enables d_Module c : enables d_Confluence u : enables d_Rule t : enables d_TypeChecking r : enables d_Reduce m : enables d_Matching May raise DebugFlagNotRecognized.

Flag to check for variables arity. Default is true.

Flag to check for rules left linearity. Default is false

init input initializes a new global environement from the input

get_input env returns the input used to create env

get_input env returns the filename associated to the input of env. We return a fake filename if the input was not create from a filename.

get_signature env returns the signature used by this module.

get_name env returns the name of the module.

set_reduction_egine env changes the reduction engine of env. The new environment shares the same signature than env.

get_reduction_engine env returns the reduction engine of env

get_print env returns a pretty printer associated to env

get_symbols env returns the content of the signature sg. Each name in the current signature is associated to a rw_infos.

get_type env l md id returns the type of the constant md.id.

is_injective env l cst returns true if the symbol is declared as static or injective, false otherwise

is_static env l cst returns true if the symbol is declared as static, false otherwise

get_dtree env l md id returns the decision/matching tree associated with md.id.

export env saves the current environment in a *.dko file.

import env lc md the module md in the current environment.

declare_constant env l id st ty declares the symbol id of type ty and staticity st.

define env l id scope body ty defines the symbol id of type ty to be an alias of body.

add_rules env rule_lst adds a list of rule to a symbol. All rules must be on the same symbol.

infer env ctx term infers the type of term given the typed context ctx

infer env ctx te ty checks that te is of type ty given the typed context ctx

reduction env ctx red te checks first that te is well-typed then reduces it according to the reduction configuration red

are_convertible env ctx tl tr checks first that tl tr have the same type, and then that they are convertible

unsafe_reduction env red te reduces te according to the reduction configuration red. It is unsafe in the sense that te is not type checked first.