diff options
Diffstat (limited to 'src/Data/Term/Unify.idr')
| -rw-r--r-- | src/Data/Term/Unify.idr | 105 |
1 files changed, 103 insertions, 2 deletions
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr index 7cb01d6..35cc048 100644 --- a/src/Data/Term/Unify.idr +++ b/src/Data/Term/Unify.idr @@ -5,6 +5,7 @@ import Data.Fin.Occurs import Data.Fin.Strong import Data.Maybe.Properties import Data.Term +import Data.Term.Property import Data.Term.Zipper import Decidable.Equality @@ -143,6 +144,13 @@ for : Term sig (pred k) -> SFin k -> SFin k -> Term sig (pred k) (t `for` x) y = maybe t Var' (thick x y) export +forRefl : + (0 u : Term sig (pred k)) -> + (x : SFin k) -> + (u `for` x) x = u +forRefl u x = cong (maybe u Var') $ extractIsNothing $ thickRefl x + +export forThin : (0 t : Term sig (pred k)) -> (x : SFin k) -> @@ -161,7 +169,7 @@ forUnifies x t prf = Calc $ ~~ (u `for` x) . thin x <$> u ...(sym $ subAssoc (u `for` x) (pure (thin x)) u) ~~ Var' <$> u ...(subCong (forThin u x) u) ~~ u ...(subUnit u) - ~~ (u `for` x) <$> Var' x ...(sym $ cong (maybe u Var') $ extractIsNothing $ thickRefl x) + ~~ (u `for` x) <$> Var' x ...(sym $ forRefl u x) -- Substitution List ----------------------------------------------------------- @@ -202,7 +210,7 @@ evalHomo sub2 (sub1 :< (t, x)) i = Calc $ -- Unification ----------------------------------------------------------------- -flexFlex : (x : SFin (S n)) -> (y : SFin (S n)) -> Exists (AList sig (S n)) +flexFlex : SFin (S n) -> SFin (S n) -> Exists (AList sig (S n)) flexFlex x y = case thick x y of Just z => Evidence _ [<(Var' z, x)] Nothing => Evidence _ [<] @@ -246,3 +254,96 @@ amguAll (t :: ts) (u :: us) acc = do export mgu : DecEq (Exists sig.Operator) => (t, u : Term sig n) -> Maybe (Exists (AList sig n)) mgu t u = amgu t u (Evidence _ [<]) + +-- Properties + +export +trivialUnify : + (0 f : SFin n -> Term sig k) -> + (t : Term sig n) -> + (Max (Extension (Unifies t t) f)).Prop Var' +trivialUnify f t = (Refl , \g, prf => varMax g) + +export +varElim : + (x : SFin (S n)) -> + (t : Term sig (S n)) -> + (0 _ : check x t = Just u) -> + (Max (Unifies (Var x) t)).Prop (u `for` x) +varElim x t prf = + ( sym $ forUnifies x t prf + , \g, prf' => MkLte (g . thin x) (\i => + case decEq x i of + Yes Refl => + Calc $ + |~ g x + ~~ g <$> t ...(prf') + ~~ g <$> pure (thin x) <$> u ...(cong (g <$>) $ checkJust i t prf) + ~~ (g . thin x) <$> u ...(sym $ subAssoc g (pure (thin x)) u) + ~~ (g . thin x) <$> (u `for` x) x ..<(cong ((g . thin x) <$>) $ forRefl u x) + No neq => + let isJust = thickNeq x i neq in + let (y ** thickIsJustY) = extractIsJust isJust in + let thinXYIsI = thickJust x i thickIsJustY in + Calc $ + |~ g i + ~~ g (thin x y) ..<(cong g thinXYIsI) + ~~ (g . thin x) <$> Var' y ...(Refl) + ~~ (g . thin x) <$> (u `for` x) (thin x y) ..<(cong ((g . thin x) <$>) $ forThin u x y) + ~~ (g . thin x) <$> (u `for` x) i ...(cong (((g . thin x) <$>) . (u `for` x)) $ thinXYIsI)) + ) + +flexFlexUnifies : + (x, y : SFin (S n)) -> + (Max {sig} (Unifies (Var x) (Var y))).Prop (eval (flexFlex x y).snd) +flexFlexUnifies x y with (thick x y) proof prf + _ | Just z = + (Max (Unifies (Var x) (Var y))).cong + (\i => sym $ subUnit ((Var' z `for` x) i)) + (varElim x (Var y) (cong (map Var') prf)) + _ | Nothing = + rewrite thickNothing x y (rewrite prf in ItIsNothing) in + trivialUnify Var' (Var y) + +flexRigidUnifies : + (x : SFin (S n)) -> + (t : Term sig (S n)) -> + (0 _ : flexRigid x t = Just sub) -> + (Max (Unifies (Var x) t)).Prop (eval sub.snd) +flexRigidUnifies x t ok with (check x t) proof prf + flexRigidUnifies x t Refl | Just u = + (Max (Unifies (Var x) t)).cong + (\i => sym $ subUnit ((u `for` x) i)) + (varElim x t prf) + +flexRigidFails : + (x : SFin (S k)) -> + (op : sig.Operator j) -> + (ts : Vect j (Term sig (S k))) -> + (0 _ : IsNothing (flexRigid x (Op op ts))) -> + Nothing (Unifies (Var x) (Op op ts)) +flexRigidFails x op ts isNothing f prf' with (check x (Op op ts)) proof prf + _ | Nothing = + let + (zip ** occurs) = checkNothing x (Op op ts) (rewrite prf in ItIsNothing) + cycle : (f x = (f <$> zip) + f x) + cycle = Calc $ + |~ f x + ~~ f <$> Op op ts ...(prf') + ~~ f <$> zip + Var x ...(cong (f <$>) occurs) + ~~ (f <$> zip) + f x ...(actionHomo f zip (Var x)) + zipIsTop : (zip = Top) + zipIsTop = invertActionTop zip $ noCycles (f <$> zip) (f x) (sym cycle) + opIsVar : (Op op ts = Var x) + opIsVar = trans occurs (cong (+ Var x) zipIsTop) + in + absurd opIsVar + +stepEquiv : + (t, u : Term sig (S k)) -> + (sub : AList sig k j) -> + (v : Term sig k) -> + (x : SFin (S k)) -> + Extension (Unifies t u) (eval (sub :< (v, x))) <=> + Extension (Unifies ((v `for` x) <$> t) ((v `for` x) <$> u)) (eval sub) +stepEquiv t u sub v x = extendUnify t u (v `for` x) (eval sub) |