summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Data/Term.idr62
-rw-r--r--src/Data/Term/Property.idr44
-rw-r--r--src/Data/Term/Unify.idr84
3 files changed, 147 insertions, 43 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 973ff3d..bfeb360 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -2,7 +2,10 @@ module Data.Term
import public Data.DPair
import public Data.Vect
+
+import Data.Fin.Extra
import Data.Vect.Properties.Map
+
import Syntax.PreorderReasoning
%prefix_record_projections off
@@ -88,12 +91,20 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
export
subComp :
- (f : Fin k -> Term sig n) ->
- (r : Fin j -> Fin k) ->
+ (0 f : Fin k -> Term sig n) ->
+ (0 r : Fin j -> Fin k) ->
f . pure r .=. f . r
subComp f r i = Refl
export
+subAssoc' :
+ (f : Fin k -> Term sig n) ->
+ (g : Fin j -> Fin k) ->
+ (t : Term sig j) ->
+ (f . g) <$> t = f <$> pure g <$> t
+subAssoc' f g = subAssoc f (Var . g)
+
+export
compCong2 :
{0 f1, f2 : Fin k -> Term sig n} ->
{0 g1, g2 : Fin j -> Term sig k} ->
@@ -119,6 +130,53 @@ compCongR :
f . g1 .=. f . g2
compCongR f prf = compCong2 (\_ => Refl) prf
+-- Substitution is a Semigroupoid ----------------------------------------------
+
+export
+(++) :
+ {j : Nat} ->
+ (Fin j -> Term sig n) ->
+ (Fin k -> Term sig n) ->
+ Fin (j + k) -> Term sig n
+f ++ g = either f g . splitSum
+
+export
+appendWeakenN :
+ {j : Nat} ->
+ (0 f : Fin j -> Term sig n) ->
+ (0 g : Fin k -> Term sig n) ->
+ (f ++ g) . weakenN k .=. f
+appendWeakenN f g i = cong (either f g) $ splitSumOfWeakenN i
+
+export
+appendShift :
+ {j : Nat} ->
+ (0 f : Fin j -> Term sig n) ->
+ (0 g : Fin k -> Term sig n) ->
+ (f ++ g) . shift j .=. g
+appendShift f g i = cong (either f g) $ splitSumOfShift i
+
+export
+appendCong2 :
+ {j : Nat} ->
+ {0 f : Fin j -> Term sig n} ->
+ {0 g : Fin k -> Term sig n} ->
+ {0 h : Fin (j + k) -> Term sig n} ->
+ h . weakenN k .=. f ->
+ h . shift j .=. g ->
+ h .=. f ++ g
+appendCong2 prf1 prf2 x with (splitSum x) proof prf
+ _ | Left i = Calc $
+ |~ h x
+ ~~ h (indexSum (splitSum x)) ..<(cong h (indexOfSplitSumInverse x))
+ ~~ h (weakenN k i) ...(cong (h . indexSum) prf)
+ ~~ f i ...(prf1 i)
+ _ | Right i = Calc $
+ |~ h x
+ ~~ h (indexSum (splitSum x)) ..<(cong h (indexOfSplitSumInverse x))
+ ~~ h (shift j i) ...(cong (h . indexSum) prf)
+ ~~ g i ...(prf2 i)
+
-- Injectivity -----------------------------------------------------------------
export
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 62f4caa..958c1c2 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -232,8 +232,8 @@ transitive prf1 prf2 = MkLte
}
export
-varMax : (f : Fin k -> Term sig m) -> f <= Var
-varMax f = MkLte f (\i => Refl)
+varUniqueMax : (f : Fin k -> Term sig m) -> f <= Var
+varUniqueMax f = MkLte f (\i => Refl)
export
compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
@@ -255,6 +255,34 @@ lteExtend :
(Extension p g).Prop prf.sub
lteExtend prf x = p.cong _ _ prf.prf x
+-- Maximal ---------------------------------------------------------------------
+
+public export
+record Maximal (p : Property sig k) (f : Fin k -> Term sig n) where
+ constructor MkMaximal
+ valid : p.Prop f
+ universal : forall j. (g : Fin k -> Term sig j) -> p.Prop g -> Fin n -> Term sig j
+ factors :
+ forall j.
+ (g : Fin k -> Term sig j) ->
+ (v : p.Prop g) ->
+ g .=. universal g v . f
+
+public export
+Max : Property sig k -> Property sig k
+Max p = MkProp
+ { Prop = Maximal p
+ , cong = \f, g, prf, mg =>
+ MkMaximal
+ { valid = p.cong f g prf mg.valid
+ , universal = mg.universal
+ , factors = \h, v, x => Calc $
+ |~ h x
+ ~~ mg.universal h v <$> f x ...(mg.factors h v x)
+ ~~ mg.universal h v <$> g x ...(compCongR (mg.universal h v) prf x)
+ }
+ }
+
-- Most General ----------------------------------------------------------------
public export
@@ -278,6 +306,10 @@ record MostGeneral (p : Property sig k) (f : Fin k -> Term sig n) where
%name MostGeneral mg
export
+mostGeneralIsMaximal : MostGeneral p f -> Maximal p f
+mostGeneralIsMaximal mg = MkMaximal mg.valid mg.universal mg.factors
+
+export
varMostGeneral : p.Prop Var -> MostGeneral p Var
varMostGeneral v =
MkMostGeneral
@@ -288,8 +320,8 @@ varMostGeneral v =
}
public export
-Max : Property sig k -> Property sig k
-Max p = MkProp
+UniqueMax : Property sig k -> Property sig k
+UniqueMax p = MkProp
{ Prop = MostGeneral p
, cong = \f, g, prf, mg =>
MkMostGeneral
@@ -309,7 +341,7 @@ Max p = MkProp
}
export
-maxCong : p <=> q -> Max p <=> Max q
+maxCong : p <=> q -> UniqueMax p <=> UniqueMax q
maxCong prf = MkEquivalence
{ leftToRight = \f, mg =>
MkMostGeneral
@@ -429,7 +461,7 @@ failTail :
{ps : Vect _ (Property sig j)} ->
{a : Fin j -> Term sig k} ->
{f : Fin k -> Term sig m} ->
- (Max (Extension p a)).Prop f ->
+ (UniqueMax (Extension p a)).Prop f ->
Nothing (Extension (All ps) (f . a)) ->
Nothing (Extension (All (p :: ps)) a)
failTail mg absurd g (v :: vs) =
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 9f806fa..113514a 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -148,8 +148,8 @@ data AList : Signature -> Nat -> Nat -> Type where
namespace Exists
public export
- (:<) : Exists (AList sig n) -> (Term sig n, Fin (S n)) -> Exists (AList sig (S n))
- Evidence _ sub :< tx = Evidence _ (sub :< tx)
+ (:<) : (k ** AList sig n k) -> (Term sig n, Fin (S n)) -> (k ** AList sig (S n) k)
+ (_ ** sub) :< tx = (_ ** sub :< tx)
export
eval : {k : Nat} -> AList sig k n -> Fin k -> Term sig n
@@ -198,29 +198,29 @@ flexFlex {n = S n} x y = case thick x y of
Just z => (_ **[<(Var z, x)])
Nothing => (_ ** [<])
-flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (Exists (AList sig n))
+flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (k ** AList sig n k)
flexRigid {n = S n} x t = case check x t of
- Just u => Just (Evidence _ [<(u, x)])
+ Just u => Just (_ ** [<(u, x)])
Nothing => Nothing
export
amgu :
DecOp sig =>
- {n : Nat} ->
+ {k, n : Nat} ->
(t, u : Term sig n) ->
AList sig n k ->
- Maybe (Exists (AList sig n))
+ Maybe (k ** AList sig n k)
amguAll :
DecOp sig =>
- {n : Nat} ->
+ {k, n : Nat} ->
(ts, us : Vect j (Term sig n)) ->
AList sig n k ->
- Maybe (Exists (AList sig n))
+ Maybe (k ** AList sig n k)
amgu (Op op ts) (Op op' us) acc with (decOp (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) [<] = Just (Evidence _ (flexFlex x y).snd)
+amgu (Var x) (Var y) [<] = Just (flexFlex x y)
amgu (Var x) (Op op' us) [<] = flexRigid x (Op op' us)
amgu (Op op ts) (Var y) [<] = flexRigid y (Op op ts)
amgu t@(Var _) u@(Var _) (sub :< (v, z)) =
@@ -230,13 +230,13 @@ amgu t@(Var _) u@(Op _ _) (sub :< (v, z)) =
amgu t@(Op _ _) u@(Var _) (sub :< (v, z)) =
(:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) sub
-amguAll [] [] acc = Just (Evidence _ acc)
+amguAll [] [] acc = Just (_ ** acc)
amguAll (t :: ts) (u :: us) acc = do
acc <- amgu t u acc
amguAll ts us acc.snd
export
-mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (k ** AList sig n k)
mgu t u = amgu t u [<]
-- Properties
@@ -258,17 +258,17 @@ flexFlexUnifies {n = S n} x y with (thickProof x y)
trivialUnify Var (Var x)
flexFlexUnifies {n = S n} x _ | Thinned y prf =
rewrite prf in
- (Max (Unifies (Var x) (Var _))).cong _ _
+ (UniqueMax (Unifies (Var x) (Var _))).cong _ _
(\i => sym $ subUnit ((Var y `for` x) i))
(varElim x (Var y))
-data FlexRigidProof : Fin n -> Term sig n -> Maybe (Exists (AList sig n)) -> Type where
+data FlexRigidProof : Fin n -> Term sig n -> Maybe (k ** AList sig n k) -> Type where
NoUnifier : Nothing (Unifies (Var x) t) -> res = Nothing -> FlexRigidProof x t res
ElimVar :
{n : Nat} ->
(sub : AList sig k n) ->
(mgu : MostGeneral (Unifies (Var x) t) (eval sub)) ->
- res = Just (Evidence _ sub) ->
+ res = Just (_ ** sub) ->
FlexRigidProof x t res
flexRigidProof :
@@ -301,7 +301,7 @@ flexRigidProof {n = S n} x op ts with (checkProof x (Op op ts))
rewrite prf in
ElimVar
[<(Op op us, x)]
- ((Max (Unifies (Var x) (Op op _))).cong _ _
+ ((UniqueMax (Unifies (Var x) (Op op _))).cong _ _
(\i => sym $ subUnit ((Op op us `for` x) i))
(varElim x (Op op us)))
Refl
@@ -322,7 +322,7 @@ parameters {auto _ : DecOp sig}
Term sig k ->
Term sig k ->
AList sig k n ->
- Maybe (Exists (AList sig k)) ->
+ Maybe (n ** AList sig k n) ->
Type
where
Failure :
@@ -334,7 +334,7 @@ parameters {auto _ : DecOp sig}
{0 sub : AList sig k n} ->
(sub' : AList sig n j) ->
MostGeneral (Extension (Unifies t u) (eval sub)) (eval sub') ->
- res = Just (Evidence _ (sub' ++ sub)) ->
+ res = Just (_ ** sub' ++ sub) ->
AmguProof t u sub res
public export
@@ -342,7 +342,7 @@ parameters {auto _ : DecOp sig}
Vect j (Term sig k) ->
Vect j (Term sig k) ->
AList sig k n ->
- Maybe (Exists (AList sig k)) ->
+ Maybe (n ** AList sig k n) ->
Type
where
FailureAll :
@@ -354,7 +354,7 @@ parameters {auto _ : DecOp sig}
{0 sub : AList sig k n} ->
(sub' : AList sig n j) ->
MostGeneral (Extension (UnifiesAll ts us) (eval sub)) (eval sub') ->
- res = Just (Evidence _ (sub' ++ sub)) ->
+ res = Just (_ ** sub' ++ sub) ->
AmguAllProof ts us sub res
export
@@ -378,8 +378,8 @@ amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op'
_ | SuccessAll sub' val prf' =
let
cong :
- Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
- Max (Extension (UnifiesAll ts us) (eval sub))
+ UniqueMax (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
+ UniqueMax (Extension (UnifiesAll ts us) (eval sub))
cong = maxCong $ extendCong (eval sub) $ unifiesOp op ts us
in
Success sub'
@@ -397,7 +397,10 @@ amguProof (Var x) (Var y) [<] =
Success
(flexFlex x y).snd
(flexFlexUnifies x y)
- Refl
+ (cong Just $ ext _ (flexFlex x y))
+ where
+ ext : (0 b : a -> Type) -> (v : (x : a ** b x)) -> v = (v.fst ** v.snd)
+ ext b (fst ** snd) = Refl
amguProof (Var x) (Op op' us) [<] with (flexRigidProof x op' us)
_ | NoUnifier absurd prf = Failure absurd prf
_ | ElimVar sub val prf = Success sub val prf
@@ -413,8 +416,8 @@ amguProof (Op op ts) (Var y) [<] with (flexRigidProof y op ts)
_ | ElimVar sub val prf =
let
cong :
- Max (Extension (Unifies (Var y) (Op op ts)) Var) <=>
- Max (Extension (Unifies (Op op ts) (Var y)) Var)
+ UniqueMax (Extension (Unifies (Var y) (Op op ts)) Var) <=>
+ UniqueMax (Extension (Unifies (Op op ts) (Var y)) Var)
cong = maxCong $ extendCong Var $ unifiesSym (Var y) (Op op ts)
in
Success sub (cong.leftToRight _ val) prf
@@ -423,8 +426,8 @@ amguProof (Var x) (Var y) (sub :< (v, z))
_ | 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))
+ UniqueMax (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
+ UniqueMax (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'
@@ -439,8 +442,8 @@ amguProof (Var x) (Op op' us) (sub :< (v, z))
_ | 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))
+ UniqueMax (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
+ UniqueMax (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'
@@ -455,8 +458,8 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
_ | 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))
+ UniqueMax (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
+ UniqueMax (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'
@@ -470,7 +473,7 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
amguAllProof [] [] sub =
SuccessAll [<]
(varMostGeneral [])
- (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
+ (sym $ cong (\sub => Just (_ ** sub)) $ appendUnitLeft sub)
amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
_ | Success sub' val prf with (amguAllProof ts us (sub' ++ sub))
_ | SuccessAll sub'' val' prf' =
@@ -483,11 +486,11 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
cong'.leftToRight (eval sub'') val'
in
SuccessAll (sub'' ++ sub')
- ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong _ _
+ ((UniqueMax (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong _ _
(\i => sym $ evalHomo sub'' sub' i)
opt)
(rewrite prf in rewrite prf' in
- cong (\sub => Just (Evidence _ sub)) $
+ cong (\sub => Just (_ ** sub)) $
appendAssoc sub'' sub' sub)
_ | FailureAll absurd prf' =
let
@@ -504,11 +507,12 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
parameters {auto _ : DecOp sig}
namespace MguProof
public export
- data MguProof : (t, u : Term sig k) -> Maybe (Exists (AList sig k)) -> Type where
+ data MguProof : (t, u : Term sig k) -> Maybe (n ** AList sig k n) -> Type where
Success :
+ {n : Nat} ->
(sub : AList sig k n) ->
MostGeneral (Unifies t u) (eval sub) ->
- res = Just (Evidence _ sub) ->
+ res = Just (_ ** sub) ->
MguProof t u res
Failure :
Nothing (Unifies t u) ->
@@ -520,3 +524,13 @@ mguProof : DecOp sig => {k : Nat} -> (t, u : Term sig k) -> MguProof t u (mgu t
mguProof t u with (amguProof t u [<])
_ | Success sub val prf = Success sub val prf
_ | Failure absurd prf = Failure absurd prf
+
+export
+invertMgu :
+ DecOp sig =>
+ {0 t, u : Term sig k} ->
+ MguProof t u res ->
+ res = Just (_ ** sub) ->
+ MostGeneral (Unifies t u) (eval sub)
+invertMgu (Success sub mg Refl) Refl = mg
+invertMgu (Failure _ prf) Refl = absurd prf
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:18:44 +0000