[clean up and commend id system more, close last holes in the ADT, create a more efficient binary representation for Ids
John Meacham <john@repetae.net>**20090222011836
 Ignore-this: b747fcaf62ca752779e2496b2b932c9e
] hunk ./DataConstructors.hs 97
-        v <- newName (map anonymous [70,72..]) () tv
+        v <- newName (map anonymous [35 .. ]) () tv
hunk ./DataConstructors.hs 237
-        typeVars = take n [ tvr { tvrType = eStar, tvrIdent = v } | v <- map anonymous [ 2,4 ..]]
-        vars =  [ tvr { tvrType = EVar t, tvrIdent = v } | v <- map anonymous [ 2*n + 16, 2*n + 18 ..] | t <- typeVars ]
+        typeVars = take n [ tvr { tvrType = eStar, tvrIdent = v } | v <- anonymousIds ]
+        vars =  [ tvr { tvrType = EVar t, tvrIdent = v } | v <- map anonymous [ n + 8, n + 9 ..] | t <- typeVars ]
hunk ./DataConstructors.hs 267
-            conExpr = ELam (tVr id2 eStar) (ELam (tVr id4 eStar) (EPi (tVr emptyId (EVar $ tVr id2 eStar)) (EVar $ tVr id4 eStar))),
+            conExpr = ELam (tVr va1 eStar) (ELam (tVr va2 eStar) (EPi (tVr emptyId (EVar $ tVr va1 eStar)) (EVar $ tVr va2 eStar))),
hunk ./DataConstructors.hs 270
-        } where id2 = anonymous 2 ; id4 = anonymous 4
+        }
hunk ./DataConstructors.hs 287
-            conExpr = ELam (tVr (anonymous 2) rt) (ELit (litCons { litName = dc, litArgs = [EVar (tVr (anonymous 2) rt)], litType = tipe })),
+            conExpr = ELam (tVr va1 rt) (ELit (litCons { litName = dc, litArgs = [EVar (tVr va1 rt)], litType = tipe })),
hunk ./DataConstructors.hs 475
-        v1 = tvr { tvrIdent = anonymous 2,  tvrType = typ }
-        v2 = tvr { tvrIdent = anonymous 4,  tvrType = typ }
-        i1 = tvr { tvrIdent = anonymous 6,  tvrType = it }
-        i2 = tvr { tvrIdent = anonymous 8,  tvrType = it }
-        b3 = tvr { tvrIdent = anonymous 10, tvrType = tBoolzh }
-        val1 = tvr { tvrIdent = anonymous 14, tvrType = typ }
+        v1 = tvr { tvrIdent = anonymous 1,  tvrType = typ }
+        v2 = tvr { tvrIdent = anonymous 2,  tvrType = typ }
+        i1 = tvr { tvrIdent = anonymous 3,  tvrType = it }
+        i2 = tvr { tvrIdent = anonymous 4,  tvrType = it }
+        b3 = tvr { tvrIdent = anonymous 5, tvrType = tBoolzh }
+        val1 = tvr { tvrIdent = anonymous 7, tvrType = typ }
hunk ./DataConstructors.hs 535
-        return (foldr ELam sl [ tVr (anonymous i) s | s <- getSlots cs | i <- [2,4..]])
+        return (foldr ELam sl [ tVr i s | s <- getSlots cs | i <- anonymousIds])
hunk ./DataConstructors.hs 574
-            dataCons = fc { conName = consName, conType = getType (conExpr dataCons), conOrigSlots = [SlotNormal rtype], conExpr = ELam (tVr (anonymous 12) rtype) (ELit (litCons { litName = consName, litArgs = [EVar (tVr (anonymous 12) rtype)], litType =  conExpr theType })) }
+            dataCons = fc { conName = consName, conType = getType (conExpr dataCons), conOrigSlots = [SlotNormal rtype], conExpr = ELam (tVr (anonymous 3) rtype) (ELit (litCons { litName = consName, litArgs = [EVar (tVr (anonymous 6) rtype)], litType =  conExpr theType })) }
hunk ./DataConstructors.hs 607
-        strictize tslots con = E.Subst.subst tvr { tvrIdent = anonymous $ -1 } Unknown $ f tslots con where
+        strictize tslots con = E.Subst.subst tvr { tvrIdent = sillyId } Unknown $ f tslots con where
hunk ./DataConstructors.hs 617
-            mapM_ (newName (map anonymous [2,4..]) ()) vs
+            mapM_ (newName anonymousIds ()) vs
hunk ./DataConstructors.hs 619
-        subst = substMap $ fromList [ (tvrIdent tv ,EVar $ tv { tvrIdent = p }) | EVar tv <- thisTypeArgs | p <- map anonymous [2,4..] ]
+        subst = substMap $ fromList [ (tvrIdent tv ,EVar $ tv { tvrIdent = p }) | EVar tv <- thisTypeArgs | p <- anonymousIds ]
hunk ./DataConstructors.hs 640
-            fvset = freeVars (thisTypeArgs,origArgs) `mappend` fromList (map anonymous [2,4 .. 2 * (length theTypeArgs + 2)])
+            fvset = freeVars (thisTypeArgs,origArgs) `mappend` fromList (take (length theTypeArgs + 2) anonymousIds)
hunk ./DataConstructors.hs 654
-        theTypeArgs = [ tvr { tvrIdent = x } | tvr  <- theTypeKArgs' | x <- map anonymous [2,4..] ]
+        theTypeArgs = [ tvr { tvrIdent = x } | tvr  <- theTypeKArgs' | x <- anonymousIds ]
hunk ./DataConstructors.hs 689
-    sub = substMap $ fromDistinctAscList [ (anonymous i,sl) | sl <- xs | i <- [2,4..] ]
+    sub = substMap $ fromDistinctAscList [ (i,sl) | sl <- xs | i <- anonymousIds ]
hunk ./DataConstructors.hs 712
-                            return $ tVr (anonymous $ 2*s) t
+                            return $ tVr (anonymous s) t
hunk ./DataConstructors.hs 731
-    sub = substMap $ fromDistinctAscList [ (anonymous i,sl) | sl <- xs | i <- [2,4..] ]
+    sub = substMap $ fromDistinctAscList [ (i,sl) | sl <- xs | i <- anonymousIds ]
hunk ./DataConstructors.hs 748
-    sub = substMap $ fromDistinctAscList [ (anonymous i,sl) | sl <- xs | i <- [2,4..] ]
+    sub = substMap $ fromDistinctAscList [ (i,sl) | sl <- xs | i <- anonymousIds ]
hunk ./E/Arbitrary.hs 42
-    return $ TVr (anonymous $ 2*x) t mempty
+    return $ TVr (anonymous x) t mempty
hunk ./E/Binary.hs 13
--- Binary instance
-data TvrBinary = TvrBinaryNone | TvrBinaryAtom Atom | TvrBinaryInt Word32
hunk ./E/Binary.hs 15
-    put (TVr { tvrIdent = eid, tvrType =  e, tvrInfo = nf} ) | eid == emptyId = do
-        put (TvrBinaryNone)
-        put e
-        putInfo nf
-    put (TVr { tvrIdent = i, tvrType =  e, tvrInfo = nf}) | Just x <- intToAtom (idToInt i) = do
-        put (TvrBinaryAtom x)
-        put e
-        putInfo nf
-    put (TVr { tvrIdent = i, tvrType =  e, tvrInfo = nf}) = do
-        put (TvrBinaryInt $ fromIntegral (idToInt i))
+    put TVr { tvrIdent = eid, tvrType =  e, tvrInfo = nf} = do
+        put eid
hunk ./E/Binary.hs 20
-        (x ) <- get
+        x <- get
hunk ./E/Binary.hs 23
-        case x of
-            TvrBinaryNone -> return $ TVr emptyId e nf
-            TvrBinaryAtom a -> return $ TVr (fromAtom a) e nf
-            TvrBinaryInt i -> return $ TVr (anonymous $ fromIntegral i) e nf
+        return $ TVr x e nf
hunk ./E/Binary.hs 25
-instance Binary TvrBinary where
-    put TvrBinaryNone = do putWord8  0
-    put (TvrBinaryAtom aa) = do
-        putWord8 1
-        put aa
-    put (TvrBinaryInt ab) = do
-	    putWord8 2
-	    put ab
-    get = do
-	    h <- getWord8
-	    case h of
-	      0 -> do return TvrBinaryNone
-	      1 -> do
-		    aa <- get
-		    return (TvrBinaryAtom aa)
-	      2 -> do
-		    ab <- get
-		    return (TvrBinaryInt ab)
-	      _ -> fail "invalid binary data found"
hunk ./E/E.hs 74
-tvrSilly = tVr (anonymous (-1)) Unknown
+tvrSilly = tVr sillyId Unknown
hunk ./E/FromHs.hs 184
-            worldVar = tvr { tvrIdent = anonymous 2, tvrType = tWorld__ }
+            worldVar = tvr { tvrIdent = va1, tvrType = tWorld__ }
hunk ./E/SSimplify.hs 1067
-        (used,bound) <- getIds
-        let genNames i = [st, st + 2 ..]  where
-                st = abs i + 2 + abs i `mod` 2
---        trace ("newName: "++ show (size used, size bound)) $ return ()
-        --newNameFrom  (genNames (size used + size bound))
-        sm <- get
-        let (g1,g2) = split (smStdGen sm)
-        put sm{smStdGen = g1}
-        newNameFrom (map anonymous $ filter (>0) $ filter even $ randoms g2)
+        (used,_bound) <- getIds
+        newNameFrom (newIds used)
hunk ./FrontEnd/Class.hs 309
-vtrace s v | verbose = trace s v
+vtrace s v | False && verbose = trace s v
hunk ./Name/Id.hs 7
+    va1,va2,va3,va4,va5,
hunk ./Name/Id.hs 14
+    anonymousIds,
+    sillyId,
hunk ./Name/Id.hs 34
+    candidateIds,
hunk ./Name/Id.hs 39
-import Control.Monad.State
hunk ./Name/Id.hs 40
-import Data.Binary(Binary())
-import Data.Traversable
+import Control.Monad.State
+import Data.Bits
hunk ./Name/Id.hs 43
+import Data.Int
hunk ./Name/Id.hs 45
+import Data.Traversable
hunk ./Name/Id.hs 48
-import Data.Bits
+import qualified Data.Binary as B
hunk ./Name/Id.hs 52
+import Doc.DocLike
+import Doc.PPrint
+import Name.Name
hunk ./Name/Id.hs 60
-import Name.Name
-import Doc.PPrint
-import Doc.DocLike
+
+
+{-
+ - An Id is an opaque type with equality and ordering, Its range is split into the following categories
+ - all the following categories are disjoint.
+ -
+ - the unique empty id, called 'emptyId'
+ -
+ - for every Atom there is a unique cooresponding Id.
+ -
+ - a set of anonymous ids, indexed by positive numbers.
+ -
+ - a set of epheremal Ids presented as the list 'epheremalIds'. these are
+ - generally used as placeholders for unification algorithms.
+ -
+ - In general, only atomic and anonymous ids are used as values, and the empty id is used to indicate
+ - an usused binding site. epheremal and silly ids are used internally in certain algorithms and have no
+ - meaning outside of said context. They never escape the code that uses them.
+ -
+ -}
+
+
hunk ./Name/Id.hs 83
--- TODO - make this a newtype
hunk ./Name/Id.hs 84
-    deriving(Eq,Ord,Enum,Binary)
+    deriving(Eq,Ord)
hunk ./Name/Id.hs 87
-anonymous x = Id x
+anonymous x | x <= 0 = error "invalid anonymous id"
+            | otherwise = Id (2*x)
+
+-- | some convinience anonymous ids
+va1,va2,va3,va4,va5 :: Id
+va1  = anonymous 1
+va2  = anonymous 2
+va3  = anonymous 3
+va4  = anonymous 4
+va5  = anonymous 5
hunk ./Name/Id.hs 213
-        let genNames i = map Id [st, st + 2 ..]  where
-                st = abs i + 2 + abs i `mod` 2
-        fromIdNameT $ newNameFrom  (genNames (size used + size bound))
+        fromIdNameT $ newNameFrom (candidateIds (size used `xor` size bound))
hunk ./Name/Id.hs 239
-        showsPrec _ n =  maybe (showString ('x':show (idToInt n))) shows (fromId n)
-    
+        showsPrec _ (Id 0) =  showChar '_'
+        showsPrec _ (Id x) =  maybe (showString ('x':show (x `div` 2))) shows (fromId $ Id x)
hunk ./Name/Id.hs 243
-    showsPrec n is = showsPrec n $ map f (idSetToList is) where
-        f n =  maybe (toAtom ('x':show (idToInt n))) (toAtom . show) (fromId n)
+    showsPrec n is = showsPrec n (idSetToList is)
hunk ./Name/Id.hs 246
-    showsPrec n is = showsPrec n $ map f (idMapToList is) where
-        f (n,v) =  (maybe (toAtom ('x':show (idToInt n))) (toAtom . show) (fromId n),v)
+    showsPrec n is = showsPrec n (idMapToList is)
+
+anonymousIds :: [Id]
+anonymousIds = map anonymous [1 .. ]
+
hunk ./Name/Id.hs 252
--- Id types
--- odd - an atom
--- 0 - special, indicating lack of binding
--- negative - etherial id, used as placeholder within algorithms
--- positive and even - arbitrary numbers.
hunk ./Name/Id.hs 254
-etherealIds = map Id [-2, -4 ..  ]
+etherealIds = map Id [-4, -6 ..  ]
hunk ./Name/Id.hs 256
+isEmptyId x = x == emptyId
hunk ./Name/Id.hs 259
+-- | id isn't anonymous or atom-mapped
hunk ./Name/Id.hs 262
+-- | A occasionally useful random ethereal id
+sillyId :: Id
+sillyId = Id $ -2
+
hunk ./Name/Id.hs 274
-newIds ids = [ Id i | i <- [s, s + 2 ..] , Id i `notMember` ids ] where
-    s = 2 + (2 * size ids)
+newIds (IdSet ids) = [ i | i <- candidateIds (size ids' `xor` IS.findMin ids' `xor` IS.findMax ids') , i `notMember` IdSet ids ] where
+    ids' = IS.insert 0 ids
hunk ./Name/Id.hs 281
-newId seed check = head $ filter check ls where
-    ls = map mask $ randoms (mkStdGen seed)
-    mask x = Id $ x .&. 0x0FFFFFFE
+newId seed check = head $ filter check (candidateIds seed)
hunk ./Name/Id.hs 283
+-- generate a list of candidate anonymous ids based on a seed value
+candidateIds :: Int -> [Id]
+candidateIds seed = map mask $ randoms (mkStdGen seed) where
+    mask x = Id $ x .&. 0x0FFFFFFE
hunk ./Name/Id.hs 296
---fromId i | even i || i < 0 = fail $ "Name.fromId: not a name " ++ show i
---fromId i | not $ isValidAtom i = fail $ "Name.fromId: not a name " ++ show i
hunk ./Name/Id.hs 298
-    Nothing -> fail $ "Name.fromId: not a name " ++ show i
+    Nothing -> fail $ "Name.fromId: not a name " ++ show (Id i)
hunk ./Name/Id.hs 300
-isEmptyId x = x == emptyId
hunk ./Name/Id.hs 305
-    genNames i = map Id [st, st + 2 ..]  where
-        st = abs i + 2 + abs i `mod` 2
+    genNames = candidateIds
hunk ./Name/Id.hs 307
+instance B.Binary Id where
+    put (Id x) = case intToAtom x of
+        Just a -> do B.putWord8 128 >> B.put a
+        Nothing | x >= 0 && x < 128 -> B.putWord8 (fromIntegral x)
+                | otherwise -> do
+                    B.putWord8 129
+                    B.put (fromIntegral x :: Int32)
+    get = do
+        x <- B.getWord8
+        case x of
+            128 -> do
+                a <- B.get
+                return (toId $ fromAtom a)
+            129 -> do
+                v <- B.get
+                return (Id $ fromIntegral (v :: Int32))
+            _ -> return (Id $ fromIntegral x)
hunk ./data/PrimitiveOperators-in.hs 32
-                       , litAliasFor = Just (ELam tvr { tvrIdent = anonymous 2
+                       , litAliasFor = Just (ELam tvr { tvrIdent = va1
hunk ./data/PrimitiveOperators-in.hs 42
-    tvra =  tVr (anonymous 4) t1
-    tvrb =  tVr (anonymous 6) t2
+    tvra =  tVr va2 t1
+    tvrb =  tVr va3 t2
hunk ./data/PrimitiveOperators-in.hs 84
-    tvra' = tVr (anonymous 2) t
-    tvrb' = tVr (anonymous 4) tInt
-    tvra = tVr (anonymous 6) st
-    tvrb = tVr (anonymous 8) intt
-    tvrc = tVr (anonymous 10) st
+    tvra' = tVr va1 t
+    tvrb' = tVr va2 tInt
+    tvra = tVr va3 st
+    tvrb = tVr va4 intt
+    tvrc = tVr va5 st
hunk ./data/PrimitiveOperators-in.hs 94
-    tvra' = tVr (anonymous 2) t
-    tvrb' = tVr (anonymous 4) t
-    tvra = tVr (anonymous 6) st
-    tvrb = tVr (anonymous 8) st
-    tvrc = tVr (anonymous 10) st
+    tvra' = tVr va1 t
+    tvrb' = tVr va2 t
+    tvra = tVr va3 st
+    tvrb = tVr va4 st
+    tvrc = tVr va5 st
hunk ./data/PrimitiveOperators-in.hs 103
-    tvra' = tVr (anonymous 2) t
-    tvra = tVr (anonymous 6) st
-    tvrc = tVr (anonymous 10) st
+    tvra' = tVr va1 t
+    tvra = tVr va3 st
+    tvrc = tVr va5 st
hunk ./data/PrimitiveOperators-in.hs 120
-    tvra' = tVr (anonymous 2) t
-    tvrb' = tVr (anonymous 4) t
-    tvra = tVr (anonymous 6) st
-    tvrb = tVr (anonymous 8) st
-    tvrc = tVr (anonymous 10) tBoolzh
+    tvra' = tVr va1 t
+    tvrb' = tVr va2 t
+    tvra = tVr va3 st
+    tvrb = tVr va4 st
+    tvrc = tVr va5 tBoolzh
hunk ./data/PrimitiveOperators-in.hs 131
-    tvra = tVr (anonymous 2) st
-    tvrb = tVr (anonymous 4) st
+    tvra = tVr va1 st
+    tvrb = tVr va2 st
hunk ./data/PrimitiveOperators-in.hs 142
-    tvra = tVr (anonymous 2) st
+    tvra = tVr va1 st
hunk ./data/PrimitiveOperators-in.hs 147
-    tvra = tVr (anonymous 2) st
+    tvra = tVr va1 st
hunk ./data/PrimitiveOperators-in.hs 156
-    tvra = tVr (anonymous 2) st
+    tvra = tVr va1 st
hunk ./data/PrimitiveOperators-in.hs 167
-    tvra = tVr (anonymous 2) st
+    tvra = tVr va1 st
hunk ./data/PrimitiveOperators-in.hs 178
-    tvr = (tVr (anonymous 2) (tPtr t))
-    tvr' = tVr (anonymous 4) (rawType "bits<ptr>")
+    tvr = (tVr va1 (tPtr t))
+    tvr' = tVr va2 (rawType "bits<ptr>")
hunk ./data/PrimitiveOperators-in.hs 188
-    ptr_tvr =  (tVr (anonymous 2) (tPtr t))
-    v_tvr = tVr (anonymous 4) t
-    ptr_tvr' =  (tVr (anonymous 6) (rawType "bits<ptr>"))
-    v_tvr' = tVr (anonymous 8) (rawType p)
+    ptr_tvr =  (tVr va1 (tPtr t))
+    v_tvr = tVr va2 t
+    ptr_tvr' =  (tVr va3 (rawType "bits<ptr>"))
+    v_tvr' = tVr va4 (rawType p)
hunk ./data/PrimitiveOperators-in.hs 227
-v2_Int = tVr (anonymous 2) tInt
-v2_Integer = tVr (anonymous 2) tInteger
-v2 t = tVr (anonymous 2) t
+v2_Int = tVr va1 tInt
+v2_Integer = tVr va1 tInteger
+v2 t = tVr va1 t