Extending the type preservation check #189
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
| @@ -60,7 +60,8 @@ let _ = | |||
| c : (confluence) notifies about information provided to the confluence | |||
| checker (when option --confluence used) | |||
| 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?
| @@ -92,6 +93,11 @@ let _ = | |||
| ; ( "--type-lhs" | |||
| , Arg.Set Typing.fail_on_unsatisfiable_constraints | |||
| , " 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?
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.