A couple non-breaking changes here and ther. Trying to estabilish alp…

…ha conversion for a simple imperative language
VictorCMiraldo · Feb 17, 2018 · d4eb743 · VictorCMiraldo · Feb 21, 2018 · serras
1 parent 6b98a41
commit d4eb743
Show file tree

Hide file tree

Showing 4 changed files with 148 additions and 54 deletions.
diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs
@@ -44,17 +44,19 @@ data NA  :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where
 -- ** Map, Elim and Zip
 
 -- |Maps a natural transformation over an atom interpretation
-mapNA :: (forall ix . IsNat ix => f ix -> g ix)
-      -> NA ki f a -> NA ki g a
-mapNA nat (NA_I f) = NA_I (nat f)
-mapNA nat (NA_K i) = NA_K i
+mapNA :: (forall k  .             ki k  -> kj k)
+      -> (forall ix . IsNat ix => f  ix -> g  ix)
+      -> NA ki f a -> NA kj g a
+mapNA fk fi (NA_I f) = NA_I (fi f)
+mapNA fk fi (NA_K k) = NA_K (fk k)
 
 -- |Maps a monadic natural transformation over an atom interpretation
 mapMNA :: (Monad m)
-       => (forall ix . IsNat ix => f ix -> m (g ix))
-       -> NA ki f a -> m (NA ki g a)
-mapMNA nat (NA_K i) = return (NA_K i)
-mapMNA nat (NA_I f) = NA_I <$> nat f
+       => (forall k  .             ki k  -> m (kj k))
+       -> (forall ix . IsNat ix => f  ix -> m (g  ix))
+       -> NA ki f a -> m (NA kj g a)
+mapMNA fk fi (NA_K k) = NA_K <$> fk k
+mapMNA fk fi (NA_I f) = NA_I <$> fi f
 
 -- |Eliminates an atom interpretation
 elimNA :: (forall k . ki  k -> b)
@@ -94,14 +96,25 @@ type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
 -- a 'Rep'. These are just the cannonical combination
 -- of their homonym versions in 'NS', 'NP' or 'NA'.
 
-mapRep :: (forall ix . IsNat ix => f ix -> g ix)
+mapRep :: (forall ix . IsNat ix => f  ix -> g ix)
        -> Rep ki f c -> Rep ki g c
-mapRep f = Rep . mapNS (mapNP (mapNA f)) . unRep
+mapRep = hmapRep id
 
 mapMRep :: (Monad m)
-        => (forall ix . IsNat ix => f ix -> m (g ix))
+        => (forall ix . IsNat ix => f  ix -> m (g  ix))
         -> Rep ki f c -> m (Rep ki g c)
-mapMRep f = (Rep <$>) . mapMNS (mapMNP (mapMNA f)) . unRep
+mapMRep = hmapMRep return
+
+hmapRep :: (forall k  .             ki k  -> kj k)
+        -> (forall ix . IsNat ix => f  ix -> g ix)
+        -> Rep ki f c -> Rep kj g c
+hmapRep fk fi = Rep . mapNS (mapNP (mapNA fk fi)) . unRep
+
+hmapMRep :: (Monad m)
+         => (forall k  .             ki k  -> m (kj k))
+         -> (forall ix . IsNat ix => f  ix -> m (g  ix))
+         -> Rep ki f c -> m (Rep kj g c)
+hmapMRep fk fi = (Rep <$>) . mapMNS (mapMNP (mapMNA fk fi)) . unRep
 
 zipRep :: (MonadPlus m)
        => Rep ki f c -> Rep kj g c
@@ -174,6 +187,11 @@ newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)
 proxyFixIdx :: Fix ki fam ix -> Proxy ix
 proxyFixIdx _ = Proxy
 
+mapMFix :: (Monad m)
+        => (forall k . ki k -> m (kj k))
+        -> Fix ki fam ix -> m (Fix kj fam ix)
+mapMFix fk = (Fix <$>) . hmapMRep fk (mapMFix fk) . unFix
+
 -- |Compare two values of a same fixpoint for equality.
 eqFix :: (forall k. ki k -> ki k -> Bool)
       -> Fix ki fam ix -> Fix ki fam ix -> Bool
@@ -183,33 +201,3 @@ eqFix p = eqRep p (eqFix p) `on` unFix
 heqFixIx :: (IsNat ix , IsNat ix')
          => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix')
 heqFixIx fa fb = testEquality (getSNat Proxy) (getSNat Proxy)
-
-{-
-
--- |Crush the first layer of a value by traversing it and applying the
---  provided morphism.
---  ATTENTION: Not recursive!
-crush1M :: (Monad m)
-        => (forall iy . NA ki (Fix ki fam) iy -> m a)
-        -> ([a] -> m a)
-        -> Fix ki fam ix -> m a
-crush1M alg cat (Fix (Rep ns))
-  = elimNS ((>>= cat) . sequence . elimNP alg) ns
-
--- |Crushes the whole value by recursing on type-variables.
-crushM :: forall m a ki fam ix . (Monad m)
-       => (forall k . ki k -> m a)
-       -> ([a] -> m a)
-       -> Fix ki fam ix -> m a
-crushM f cat = crush1M go cat
-  where
-    go :: (Monad m) => NA ki (Fix ki fam) iy -> m a
-    go (NA_I i) = crushM f cat i
-    go (NA_K x) = f x
-
--- |Pure variant of 'crush'
-crush :: (forall k . ki k -> a)
-      -> ([a] -> a)
-      -> Fix ki fam ix -> a
-crush f cat = runIdentity . crushM (return . f) (return . cat)
--}
diff --git a/src/Generics/MRSOP/Examples/Lambda/Let.hs b/src/Generics/MRSOP/Examples/Lambda/Let.hs
@@ -14,11 +14,8 @@ module Generics.MRSOP.Examples.Lambda.Let where
 
 import Data.Function (on)
 
-import Generics.MRSOP.Base.Internal.NS
-import Generics.MRSOP.Base.Internal.NP
-import Generics.MRSOP.Base.Universe
-import Generics.MRSOP.Base.Class
-import Generics.MRSOP.Konstants
+import Generics.MRSOP.Base
+import Generics.MRSOP.Opaque
 import Generics.MRSOP.Util
 
 import Generics.MRSOP.TH
@@ -41,8 +38,17 @@ data Binding var
 deriveFamily [t| Term String |]
 
 alphaEq :: Term String -> Term String -> Bool
-alphaEq t1 t2 = galphaEq (from' @Singl t1) (from t2)
+alphaEq = (galphaEq SZ) `on` (deep @FamTermString)
   where
-    galphaEq :: FAM ix -> FAM ix -> Bool
-    galphaEq (Fix (Rep t)) (Fix (Rep u))
-      = undefined
+    galphaEq :: forall iy . (IsNat iy)
+             => SNat iy
+             -> Fix Singl CodesTermString iy
+             -> Fix Singl CodesTermString iy
+             -> Bool
+    galphaEq iy (Fix x) (Fix y)
+      = case zipRep x y of
+          Nothing -> False
+          Just xy -> case iy of
+                       SZ      -> case sop xy of
+                         Tag cx px -> _
+                       (SS SZ) -> _
diff --git a/src/Generics/MRSOP/Examples/RoseTree.hs b/src/Generics/MRSOP/Examples/RoseTree.hs
@@ -9,12 +9,13 @@
 {-# LANGUAGE PolyKinds               #-}
 {-# LANGUAGE ScopedTypeVariables     #-}
 {-# LANGUAGE FunctionalDependencies  #-}
+{-# LANGUAGE PatternSynonyms         #-}
 module Generics.MRSOP.Examples.RoseTree where
 
 import Data.Function (on)
 
 import Generics.MRSOP.Base
-import Generics.MRSOP.Konstants
+import Generics.MRSOP.Opaque
 import Generics.MRSOP.Util
 
 -- * Standard Rose-Tree datatype
@@ -64,12 +65,14 @@ testEq = value1 == value1
 
 -- * Compos test
 
+pattern RInt_ = SS SZ
+
 normalize :: R Int -> R Int
 normalize = unEl . go (SS SZ) . into
   where
     go :: forall iy. (IsNat iy) => SNat iy -> El FamRose iy -> El FamRose iy
-    go (SS SZ) (El (Leaf a)) = El (a :>: [])
-    go _       x             = compos go x
+    go RInt_ (El (Leaf a)) = El (a :>: [])
+    go _       x           = compos go x
 
 -- * Crush test
 

diff --git a/src/Generics/MRSOP/Examples/SimpTH.hs b/src/Generics/MRSOP/Examples/SimpTH.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE TypeApplications        #-}
+{-# LANGUAGE RankNTypes              #-}
+{-# LANGUAGE FlexibleContexts        #-}
+{-# LANGUAGE FlexibleInstances       #-}
+{-# LANGUAGE GADTs                   #-}
+{-# LANGUAGE TypeOperators           #-}
+{-# LANGUAGE DataKinds               #-}
+{-# LANGUAGE PolyKinds               #-}
+{-# LANGUAGE ScopedTypeVariables     #-}
+{-# LANGUAGE FunctionalDependencies  #-}
+{-# LANGUAGE TemplateHaskell         #-}
+{-# LANGUAGE LambdaCase              #-}
+{-# LANGUAGE PatternSynonyms         #-}
+module Generics.MRSOP.Examples.SimpTH where
+
+import Data.Function (on)
+
+import Generics.MRSOP.Base
+import Generics.MRSOP.Opaque
+import Generics.MRSOP.Util
+
+import Generics.MRSOP.TH
+
+import Control.Monad
+
+-- * Simple IMPerative Language:
+
+data Stmt var
+  = SAssign var (Exp var)
+  | SIf     (Exp var) (Stmt var) (Stmt var)
+  | SSeq    (Stmt var) (Stmt var)
+  | SReturn (Exp var)
+  | SDecl (Decl var)
+  | SSkip
+
+data Decl var
+  = DVar var
+  | DFun String [var] (Stmt var)
+
+data Exp var
+  = EVar  var
+  | ECall String [Exp var]
+
+{- EXAMPLE
+
+decl fib(n):
+  aux = fib(n-1) + fib(n-2);
+  return aux;
+
+is alpha eq to
+
+decl fib(x):
+  r = fib(x-1) + fib(x-2);
+  return r;
+-}
+
+deriveFamily [t| Stmt String |]
+
+pattern Decl_ = SS (SS SZ)
+pattern Exp_  = SS SZ
+pattern Stmt_ = SZ
+
+pattern SAssign_ v e = Tag CZ (NA_K v :* NA_I e :* NP0)
+pattern EVar_    = CS CZ
+
+type FIX = Fix Singl CodesStmtString
+
+alphaEq :: Decl String -> Decl String -> Bool
+alphaEq = (galphaEq [] Decl_) `on` (deep @FamStmtString)
+  where
+    galphaEq :: forall iy . (IsNat iy)
+             => [[(String,String)]]
+             -> SNat iy -> FIX iy -> FIX iy -> Bool
+    galphaEq eqs iy (Fix x)
+      = maybe False (go eqs iy) . zipRep x . unFix
+
+    addvar :: String -> String
+            -> [[ (String , String) ]]
+            -> [[ (String , String) ]]
+    addvar v1 v2 (x:xs) = ((v1 , v2):x):xs
+
+    isvalid :: [[ (String , String) ]]
+            -> Singl k -> Singl k -> Bool
+    isvalid eqs (SString v) (SString k) = _
+
+    go :: forall iy
+        . [[ (String , String) ]]
+       -> SNat iy
+       -> Rep (Singl :*: Singl) (FIX :*: FIX)
+              (Lkup iy CodesStmtString)
+       -> Bool
+    go eqs Stmt_ x
+      = case sop x of
+          SAssign_ (SString v1 :*: SString v2) e1e2
+            -> uncurry' (galphaEq (addvar v1 v2 eqs) Exp_) e1e2 
+          otherwise
+            -> _