lex-lex
commented
8 years ago Resolved by new unification implementation
Closed lex-lex closed 8 years ago
lex-lex
commented
8 years ago Resolved by new unification implementation
HuetsPreUnification seems to lack a proper distinction between free and bound variables, especially in imitate rule the flex-head is not correctly decreasing depending on how deep it is buried under lambdas. Or is this all fixed if funcext is exhaustively applied before? This seems to slow down the unification process by magnitudes. I need to check that.
`% [FINE] Clause 25 needs unification. Working on it ... % [FINE] Unification on:
% sk1 ⋅ (sk2 ⋅ (λ[$i]. ($false ⋅ (⊥));⊥);3:$i ⋅ (⊥);⊥) = sk1 ⋅ (sk2 ⋅ (1:$i -> $o ⋅ (⊥);⊥);2:$i ⋅ (⊥);⊥) % [FINER] Unsolved (term eqs): sk1 ⋅ (sk2 ⋅ (λ[$i]. ($false ⋅ (⊥));⊥);3:$i ⋅ (⊥);⊥) = sk1 ⋅ (sk2 ⋅ (λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥));⊥);2:$i ⋅ (⊥);⊥) % [FINER] Unsolved (type eqs):
% [FINEST] Apply Decomp % [FINER] Unsolved (term eqs): sk2 ⋅ (λ[$i]. ($false ⋅ (⊥));⊥) = sk2 ⋅ (λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥));⊥) % 3:$i ⋅ (⊥) = 2:$i ⋅ (⊥) % [FINER] Unsolved (type eqs):
% [FINEST] Apply Decomp % [FINER] Unsolved (term eqs): λ[$i]. ($false ⋅ (⊥)) = λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥)) % 3:$i ⋅ (⊥) = 2:$i ⋅ (⊥) % [FINER] Unsolved (type eqs):
% [FINEST] Apply Bind % [FINEST] Bind on % Left: 3:$i ⋅ (⊥) % Right: 2:$i ⋅ (⊥) % [FINEST] Resulting equation: 3:$i ⋅ (⊥) = 2:$i ⋅ (⊥) % [FINER] Unsolved (term eqs): λ[$i]. ($false ⋅ (⊥)) = λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥)) % [FINER] Unsolved (type eqs):
% [FINER] Finished detExhaust % [FINEST] selected: λ[$i]. ($false ⋅ (⊥)) = λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥)) % [FINEST] flex-rigid at depth 0 % [FINER] Apply Imitate % [FINER] Result of Imitate: 2:$i -> $o ⋅ (⊥) = λ[$i]. ($false ⋅ (⊥)) % [FINER] Apply Project % [FINEST] BVars in Projectrule: 1:$i ⋅ (⊥) % [FINEST] compatible type BVars in Projectrule:
% [FINER] Result of Project: %
% [FINER] Unsolved (term eqs): 2:$i -> $o ⋅ (⊥) = λ[$i]. ($false ⋅ (⊥)) % λ[$i]. ($false ⋅ (⊥)) = λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥)) % [FINER] Unsolved (type eqs):
% [FINEST] Apply Bind % [FINEST] Bind on % Left: 2:$i -> $o ⋅ (⊥) % Right: λ[$i]. ($false ⋅ (⊥)) % [FINEST] Resulting equation: 2:$i -> $o ⋅ (⊥) = λ[$i]. ($false ⋅ (⊥)) % [FINER] Unsolved (term eqs): λ[$i]. ($false ⋅ (⊥)) = λ[$i]. (2:$i -> $o ⋅ (1:$i ⋅ (⊥);⊥)) % [FINER] Unsolved (type eqs):
% [FINER] Finished detExhaust `