Conversation
Gaspi
changed the title
|
Better handling constraints means developing a (better) unification algorithm. Why doing this in Dedukti and not in Lambdapi? |
Fixing comment
Gaspi
added
Dedukti 2.7
WIP
francoisthire
left a comment
francoisthire
left a comment
There was a problem hiding this comment.
This PR adds a lot of complexity in the understanding of the SR algorithm. I am not confident enough to judge this algorithm. However. probably some comments should be MADE in the Readme file.
| u : (rule) provides information about type checking of rules | ||
| t : (typing) provides information about type-checking of terms | ||
| t : (typing) provides information about type checking of terms | ||
| s : (SR) provides information about subject reduction checking of terms |
There was a problem hiding this comment.
The SR criterion here is for the rules, not terms in general, right?
| , " Forbids rules with untypable left-hand side" ) | ||
| ; ( "--sr-check" | ||
| , Arg.Int (fun i -> Srcheck.srfuel := i) | ||
| , "LVL Sets the level of subject reduction checking to LVL. |
There was a problem hiding this comment.
LVL Sets... it should be --sr-check right?
| - Variables with DB index [k] < [n] are considered "locally bound" and are never substituted. | ||
| - Variables with DB index [k] >= [n] may be substituted if [k-n] is mapped in [sigma] | ||
| and if they occur applied to enough arguments (substitution's arity). *) | ||
| let apply_exsubst (subst:ex_substitution) (n:int) (te:term) : term*bool = |
There was a problem hiding this comment.
Why this function cannot be implemented by one of the subst function? Why this function is not in the module Subst?
There was a problem hiding this comment.
Ok, I rephrase, why do we have two modules for substitution now? Why don't we keep only one module for substitutions?
4 participants
From the type checking of a LHS of a rule, several kind of constraints may be inferred
X = tX x1 ... xn = t(underk>=nabstractions)where
x1 ... xnare distinct locally bound variablest = u(possibly undernabstractions)The constraints are then used to check convertibility of inferred type of RHS and LHS.
Expected behavior for these constraints are:
Xwithtin other constraints and in both LHS and RHS expected typesX a1 ... anwitht{x1\a1, ..., xn\an}in other constraints and in both LHS and RHS expected typesNote : what happens when several rules map the same variable ?
-> raise a warning or fail
(1.) and (4.) are already handled in an acceptable way.
This PR should:
tests/OK/first_order_cstr1.dk)typing/pseudo_uto allow several successive passes of inferring from constraints / process constraints.