Improve sharing.

semantic-core/src/Data/Core.hs

@@ -33,7 +33,7 @@ data Core a
   | Let Name
   -- | Sequencing without binding; analogous to '>>' or '*>'.
   | Core a :>> Core a
-  | Lam (Core (Incr a))
+  | Lam (Core (Incr (Core a)))
   -- | Function application; analogous to '$'.
   | Core a :$ Core a
   | Unit
@@ -64,7 +64,7 @@ instance Applicative Core where
   (<*>) = ap
 
 instance Monad Core where
-  a >>= f = gfold id Let (:>>) Lam (:$) Unit Bool If String Load Edge Frame (:.) (:=) Ann (incr (pure Z) (fmap S)) (f <$> a)
+  a >>= f = gfold id Let (:>>) Lam (:$) Unit Bool If String Load Edge Frame (:.) (:=) Ann pure (f <$> a)
 
 
 lam :: Eq a => a -> Core a -> Core a
@@ -108,7 +108,7 @@ gfold :: forall m n b
       .  (forall a . m a -> n a)
       -> (forall a . Name -> n a)
       -> (forall a . n a -> n a -> n a)
-      -> (forall a . n (Incr a) -> n a)
+      -> (forall a . n (Incr (n a)) -> n a)
       -> (forall a . n a -> n a -> n a)
       -> (forall a . n a)
       -> (forall a . Bool -> n a)
@@ -120,7 +120,7 @@ gfold :: forall m n b
       -> (forall a . n a -> n a -> n a)
       -> (forall a . n a -> n a -> n a)
       -> (forall a . Loc -> n a -> n a)
-      -> (forall a . Incr (m a) -> m (Incr a))
+      -> (forall a . Incr a -> m (Incr a))
       -> Core (m b)
       -> n b
 gfold var let' seq' lam app unit bool if' string load edge frame dot assign ann k = go
@@ -129,7 +129,7 @@ gfold var let' seq' lam app unit bool if' string load edge frame dot assign ann
           Var a -> var a
           Let a -> let' a
           a :>> b -> go a `seq'` go b
-          Lam b -> lam (go (k <$> b))
+          Lam b -> lam (go (k . fmap go <$> b))
           f :$ a -> go f `app` go a
           Unit -> unit
           Bool b -> bool b
@@ -144,9 +144,9 @@ gfold var let' seq' lam app unit bool if' string load edge frame dot assign ann
 
 
 -- | Bind occurrences of a name in a 'Core' term, producing a 'Core' in which the name is bound.
-bind :: Eq a => a -> Core a -> Core (Incr a)
-bind name = fmap (match name)
+bind :: Eq a => a -> Core a -> Core (Incr (Core a))
+bind name = fmap (fmap pure . match name)
 
 -- | Substitute a 'Core' term for the free variable in a given 'Core', producing a closed 'Core' term.
-instantiate :: Core a -> Core (Incr a) -> Core a
-instantiate t b = b >>= subst t . fmap pure
+instantiate :: Core a -> Core (Incr (Core a)) -> Core a
+instantiate t b = b >>= subst t