[ refactor ] move SizeChange to a separate file

idris2api.ipkg

@@ -5,6 +5,7 @@ modules =
     Algebra,
     Algebra.Preorder,
     Algebra.Semiring,
+    Algebra.SizeChange,
     Algebra.ZeroOneOmega,
 
     Compiler.ANF,

src/Algebra/SizeChange.idr

@@ -0,0 +1,43 @@
+module Algebra.SizeChange
+
+import Algebra.Semiring
+
+import Libraries.Text.PrettyPrint.Prettyprinter
+
+public export
+data SizeChange = Smaller | Same | Unknown
+
+export
+Semigroup SizeChange where
+  -- Same is a neutral
+  Unknown <+> _ = Unknown
+  Same <+> c = c
+  _ <+> Unknown = Unknown
+  Smaller <+> _ = Smaller
+
+export
+Monoid SizeChange where
+  neutral = Same
+
+export
+Show SizeChange where
+  show Smaller = "Smaller"
+  show Same = "Same"
+  show Unknown = "Unknown"
+
+export
+Eq SizeChange where
+  Smaller == Smaller = True
+  Same == Same = True
+  Unknown == Unknown = True
+  _ == _ = False
+
+export
+Ord SizeChange where
+  compare Smaller Smaller = EQ
+  compare Smaller _ = LT
+  compare _ Smaller = GT
+  compare Same Same = EQ
+  compare Same _ = LT
+  compare _ Same = GT
+  compare Unknown Unknown = EQ

src/Core/Context/Context.idr

@@ -7,6 +7,8 @@ import public Core.Name
 import public Core.Options.Log
 import public Core.TT
 
+import public Algebra.SizeChange
+
 import Data.IORef
 import Data.String
 
@@ -260,45 +262,6 @@ Show DefFlag where
   show (ConType ci) = "contype " ++ show ci
   show (Identity x) = "identity " ++ show x
 
-public export
-data SizeChange = Smaller | Same | Unknown
-
-export
-Semigroup SizeChange where
-  -- Unknown is a 0
-  -- Same is a neutral
-  _ <+> Unknown = Unknown
-  Unknown <+> _ = Unknown
-  c <+> Same = c
-  _ <+> Smaller = Smaller
-
-export
-Monoid SizeChange where
-  neutral = Same
-
-export
-Show SizeChange where
-  show Smaller = "Smaller"
-  show Same = "Same"
-  show Unknown = "Unknown"
-
-export
-Eq SizeChange where
-  Smaller == Smaller = True
-  Same == Same = True
-  Unknown == Unknown = True
-  _ == _ = False
-
-export
-Ord SizeChange where
-  compare Smaller Smaller = EQ
-  compare Smaller _ = LT
-  compare _ Smaller = GT
-  compare Same Same = EQ
-  compare Same _ = LT
-  compare _ Same = GT
-  compare Unknown Unknown = EQ
-
 public export
 record SCCall where
      constructor MkSCCall