summaryrefslogtreecommitdiff
path: root/src/Data/Term/Unify.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Term/Unify.idr')
-rw-r--r--src/Data/Term/Unify.idr227
1 files changed, 220 insertions, 7 deletions
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 35cc048..f75a61a 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -208,8 +208,25 @@ evalHomo sub2 (sub1 :< (t, x)) i = Calc $
~~ (eval sub2 . eval sub1) <$> (t `for` x) i ...(subCong (evalHomo sub2 sub1) ((t `for` x) i))
~~ eval sub2 <$> eval sub1 <$> (t `for` x) i ...(subAssoc (eval sub2) (eval sub1) ((t `for` x) i))
+export
+appendUnitLeft : (sub : AList sig k n) -> [<] ++ sub = sub
+appendUnitLeft [<] = Refl
+appendUnitLeft (sub :< tx) = cong (:< tx) (appendUnitLeft sub)
+
+export
+appendAssoc :
+ (sub3 : AList sig _ _) ->
+ (sub2 : AList sig _ _) ->
+ (sub1 : AList sig _ _) ->
+ sub3 ++ (sub2 ++ sub1) = (sub3 ++ sub2) ++ sub1
+appendAssoc sub3 sub2 [<] = Refl
+appendAssoc sub3 sub2 (sub1 :< tx) = cong (:< tx) (appendAssoc sub3 sub2 sub1)
+
-- Unification -----------------------------------------------------------------
+coerce : {0 op, op' : sig.Op} -> op = op' -> Vect op'.fst a -> Vect op.fst a
+coerce Refl = id
+
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)]
@@ -222,20 +239,19 @@ flexRigid x t = case check x t of
export
amgu :
- DecEq (Exists sig.Operator) =>
+ DecEq sig.Op =>
(t, u : Term sig n) ->
Exists (AList sig n) ->
Maybe (Exists (AList sig n))
amguAll :
- DecEq (Exists sig.Operator) =>
+ DecEq sig.Op =>
(ts, us : Vect k (Term sig n)) ->
Exists (AList sig n) ->
Maybe (Exists (AList sig n))
-amgu (Op op ts) (Op op' us) acc =
- case decEq {t = Exists sig.Operator} (Evidence _ op) (Evidence _ op') of
- Yes prf => amguAll ts (replace {p = \k => Vect k (Term sig n)} (sym $ cong fst prf) us) acc
- No neq => Nothing
+amgu (Op op ts) (Op op' us) acc with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op'))
+ amgu (Op op ts) (Op op us) acc | Yes Refl = amguAll ts us acc
+ _ | No neq = Nothing
amgu (Var x) (Var y) (Evidence _ [<]) = Just (flexFlex x y)
amgu (Var x) (Op op' us) (Evidence _ [<]) = flexRigid x (Op op' us)
amgu (Op op ts) (Var y) (Evidence _ [<]) = flexRigid y (Op op ts)
@@ -252,7 +268,7 @@ amguAll (t :: ts) (u :: us) acc = do
amguAll ts us acc
export
-mgu : DecEq (Exists sig.Operator) => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecEq sig.Op => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
mgu t u = amgu t u (Evidence _ [<])
-- Properties
@@ -347,3 +363,200 @@ stepEquiv :
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)
+
+parameters {auto _ : DecEq sig.Op}
+ public export
+ data AmguProof : (t, u : Term sig k) -> Exists (AList sig k) -> Type where
+ Success :
+ {0 sub : Exists (AList sig k)} ->
+ (sub' : Exists (AList sig sub.fst)) ->
+ (Max (Extension (Unifies t u) (eval sub.snd))).Prop (eval sub'.snd) ->
+ amgu t u sub = Just (Evidence sub'.fst (sub'.snd ++ sub.snd)) ->
+ AmguProof t u sub
+ Failure :
+ {0 sub : Exists (AList sig k)} ->
+ Nothing (Extension (Unifies t u) (eval sub.snd)) ->
+ IsNothing (amgu t u sub) ->
+ AmguProof t u sub
+
+ public export
+ data AmguAllProof : (ts, us : Vect n (Term sig k)) -> Exists (AList sig k) -> Type where
+ SuccessAll :
+ {0 sub : Exists (AList sig k)} ->
+ (sub' : Exists (AList sig sub.fst)) ->
+ (Max (Extension (UnifiesAll ts us) (eval sub.snd))).Prop (eval sub'.snd) ->
+ amguAll ts us sub = Just (Evidence sub'.fst (sub'.snd ++ sub.snd)) ->
+ AmguAllProof ts us sub
+ FailureAll :
+ {0 sub : Exists (AList sig k)} ->
+ Nothing (Extension (UnifiesAll ts us) (eval sub.snd)) ->
+ IsNothing (amguAll ts us sub) ->
+ AmguAllProof ts us sub
+
+export
+amguProof :
+ DecEq sig.Op =>
+ (t, u : Term sig n) ->
+ (sub : Exists (AList sig n)) ->
+ AmguProof t u sub
+export
+amguAllProof :
+ DecEq sig.Op =>
+ (ts, us : Vect k (Term sig n)) ->
+ (sub : Exists (AList sig n)) ->
+ AmguAllProof ts us sub
+
+amguProof (Op op ts) (Op op' us) sub
+ with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op')) proof prf
+ amguProof (Op op ts) (Op op us) sub | Yes Refl
+ with (amguAllProof ts us sub)
+ _ | SuccessAll sub' val prf' =
+ let
+ cong :
+ Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub.snd)) <=>
+ Max (Extension (UnifiesAll ts us) (eval sub.snd))
+ cong = maxCong $ extendCong (eval sub.snd) $ unifiesOp op ts us
+ in
+ Success sub'
+ (cong.rightToLeft (eval sub'.snd) val)
+ (rewrite prf in prf')
+ _ | FailureAll absurd prf' =
+ Failure
+ (nothingEquiv (symmetric $ extendCong (eval sub.snd) $ unifiesOp op ts us) absurd)
+ (rewrite prf in prf')
+ _ | No neq =
+ Failure
+ (\f, prf => neq $ opInjectiveOp prf)
+ (rewrite prf in ItIsNothing)
+amguProof (Var x) (Var y) (Evidence _ [<]) with (thick x y) proof prf
+ _ | Just z = Success (flexFlex x y) (flexFlexUnifies x y) (rewrite prf in Refl)
+ _ | Nothing = Success (flexFlex x y) (flexFlexUnifies x y) (rewrite prf in Refl)
+amguProof (Var x) (Op op' us) (Evidence _ [<]) with (flexRigid x (Op op' us)) proof prf
+ _ | Just sub@(Evidence _ _) = Success sub (flexRigidUnifies x (Op op' us) prf) prf
+ _ | Nothing =
+ Failure
+ (flexRigidFails x op' us (rewrite prf in ItIsNothing))
+ (rewrite prf in ItIsNothing)
+amguProof (Op op ts) (Var y) (Evidence _ [<]) with (flexRigid y (Op op ts)) proof prf
+ _ | Just sub@(Evidence _ sub') =
+ let
+ cong :
+ Max (Extension (Unifies (Var y) (Op op ts)) Var') <=>
+ Max (Extension (Unifies (Op op ts) (Var y)) Var')
+ cong = maxCong $ extendCong Var' $ unifiesSym (Var y) (Op op ts)
+ in
+ Success sub
+ (cong.leftToRight (eval sub.snd) (flexRigidUnifies y (Op op ts) prf))
+ prf
+ _ | Nothing =
+ let
+ cong :
+ Nothing (Extension (Unifies (Var y) (Op op ts)) Var') ->
+ Nothing (Extension (Unifies (Op op ts) (Var y)) Var')
+ cong = nothingEquiv $ extendCong Var' $ unifiesSym (Var y) (Op op ts)
+ in
+ Failure
+ (cong $ flexRigidFails y op ts (rewrite prf in ItIsNothing))
+ (rewrite prf in ItIsNothing)
+amguProof (Var x) (Var y) (Evidence l (sub :< (v, z)))
+ with (amguProof ((v `for` z) x) ((v `for` z) y) (Evidence _ sub))
+ _ | Success sub' val prf =
+ let
+ cong' :
+ Max (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
+ Max (Extension (Unifies ((v `for` z) x) ((v `for` z) y)) (eval sub))
+ cong' = maxCong $ stepEquiv (Var x) (Var y) sub v z
+ in
+ Success sub'
+ (cong'.rightToLeft (eval sub'.snd) val)
+ (cong (map (:< (v, z))) prf)
+ _ | Failure absurd prf =
+ Failure
+ (nothingEquiv (symmetric $ stepEquiv (Var x) (Var y) sub v z) absurd)
+ (mapNothing (:< (v, z)) prf)
+amguProof (Var x) (Op op' us) (Evidence _ (sub :< (v, z)))
+ with (amguProof ((v `for` z) x) ((v `for` z) <$> Op op' us) (Evidence _ sub))
+ _ | Success sub' val prf =
+ let
+ cong' :
+ Max (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
+ Max (Extension (Unifies ((v `for` z) x) ((v `for` z) <$> Op op' us)) (eval sub))
+ cong' = maxCong $ stepEquiv (Var x) (Op op' us) sub v z
+ in
+ Success sub'
+ (cong'.rightToLeft (eval sub'.snd) val)
+ (cong (map (:< (v, z))) prf)
+ _ | Failure absurd prf =
+ Failure
+ (nothingEquiv (symmetric $ stepEquiv (Var x) (Op op' us) sub v z) absurd)
+ (mapNothing (:< (v, z)) prf)
+amguProof (Op op ts) (Var y) (Evidence _ (sub :< (v, z)))
+ with (amguProof ((v `for` z) <$> Op op ts) ((v `for` z) y) (Evidence _ sub))
+ _ | Success sub' val prf =
+ let
+ cong' :
+ Max (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
+ Max (Extension (Unifies ((v `for` z) <$> Op op ts) ((v `for` z) y)) (eval sub))
+ cong' = maxCong $ stepEquiv (Op op ts) (Var y) sub v z
+ in
+ Success sub'
+ (cong'.rightToLeft (eval sub'.snd) val)
+ (cong (map (:< (v, z))) prf)
+ _ | Failure absurd prf =
+ Failure
+ (nothingEquiv (symmetric $ stepEquiv (Op op ts) (Var y) sub v z) absurd)
+ (mapNothing (:< (v, z)) prf)
+
+amguAllProof [] [] (Evidence _ sub) =
+ SuccessAll (Evidence _ [<])
+ ([], \g, x => varMax g)
+ (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
+amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
+ _ | Success sub' val prf with (amguAllProof ts us (Evidence _ (sub'.snd ++ sub.snd)))
+ _ | SuccessAll sub'' val' prf' =
+ let
+ cong' =
+ maxCong $
+ extendCong2 (evalHomo sub'.snd sub.snd) (reflexive {x = UnifiesAll ts us})
+ opt =
+ optimistLemma (unifiesDClosed t u) val $
+ cong'.leftToRight (eval sub''.snd) val'
+ in
+ SuccessAll (Evidence _ (sub''.snd ++ sub'.snd))
+ ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub.snd))).cong
+ (\i => sym $ evalHomo sub''.snd sub'.snd i)
+ opt)
+ (rewrite prf in rewrite prf' in
+ cong (\sub => Just (Evidence sub''.fst sub)) $
+ appendAssoc sub''.snd sub'.snd sub.snd)
+ _ | FailureAll absurd prf' =
+ let
+ cong' = extendCong2 (evalHomo sub'.snd sub.snd) (reflexive {x = UnifiesAll ts us})
+ in
+ FailureAll
+ (failTail val $ nothingEquiv cong' absurd)
+ (rewrite prf in prf')
+ _ | Failure absurd prf =
+ FailureAll
+ (failHead absurd)
+ (bindNothing prf (amguAll ts us))
+
+parameters {auto _ : DecEq sig.Op}
+ namespace MguProof
+ public export
+ data MguProof : (t, u : Term sig k) -> Type where
+ Success :
+ (sub : Exists (AList sig k)) ->
+ (Max (Unifies t u)).Prop (eval sub.snd) ->
+ mgu t u = Just sub ->
+ MguProof t u
+ Failure :
+ Nothing (Unifies t u) ->
+ IsNothing (mgu t u) ->
+ MguProof t u
+
+export
+mguProof : DecEq sig.Op => (t, u : Term sig k) -> MguProof t u
+mguProof t u with (amguProof t u (Evidence _ [<]))
+ _ | Success (Evidence _ sub) val prf = Success (Evidence _ sub) val prf
+ _ | Failure absurd prf = Failure absurd prf
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 04:03:54 +0000