
   0 | ||| Courtesy of @z-snails
   1 | module Core.Ord
   2 | 
   3 | import Core.CompileExpr
   4 | import Core.TT
   5 | import Data.Vect
   6 | 
   7 | import Libraries.Data.Ordering.Extra
   8 | 
   9 | lrTag : LazyReason -> Int
  10 | lrTag LInf = 0
  11 | lrTag LLazy = 1
  12 | lrTag LUnknown = 2
  13 | 
  14 | export
  15 | Ord LazyReason where
  16 |     compare l1 l2 = compare (lrTag l1) (lrTag l2)
  17 | 
  18 | mutual
  19 |     export
  20 |     covering
  21 |     Eq (CExp vars) where
  22 |         CLocal {idx=x1} _ _ == CLocal {idx=x2} _ _ = x1 == x2
  23 |         CRef _ n1 == CRef _ n2 = n1 == n2
  24 |         CLam _ n1 e1 == CLam _ n2 e2 = case nameEq n1 n2 of
  25 |             Just Refl => e1 == e2
  26 |             Nothing => False
  27 |         CLet _ n1 _ val1 sc1 == CLet _ n2 _ val2 sc2 = case nameEq n1 n2 of
  28 |             Just Refl => val1 == val2 && sc1 == sc2
  29 |             Nothing => False
  30 |         CApp _ f1 a1 == CApp _ f2 a2 = f1 == f2 && a1 == a2
  31 |         CCon _ n1 _ t1 a1 == CCon _ n2 _ t2 a2 = t1 == t2 && n1 == n2 && a1 == a2
  32 |         COp _ f1 a1 == COp _ f2 a2 = case primFnEq f1 f2 of
  33 |             Just Refl => a1 == a2
  34 |             Nothing => False
  35 |         CExtPrim _ f1 a1 == CExtPrim _ f2 a2 = f1 == f2 && a1 == a2
  36 |         CForce _ l1 e1 == CForce _ l2 e2 = l1 == l2 && e1 == e2
  37 |         CDelay _ l1 e1 == CDelay _ l2 e2 = l1 == l2 && e1 == e2
  38 |         CConCase _ s1 a1 d1 == CConCase _ s2 a2 d2 = s1 == s2 && a1 == a2 && d1 == d2
  39 |         CConstCase _ s1 a1 d1 == CConstCase _ s2 a2 d2 = s1 == s2 && a1 == a2 && d1 == d2
  40 |         CPrimVal _ c1 == CPrimVal _ c2 = c1 == c2
  41 |         CErased _ == CErased _ = True
  42 |         CCrash _ m1 == CCrash _ m2 = m1 == m2
  43 |         _ == _ = False
  44 | 
  45 |     export
  46 |     covering
  47 |     Eq (CConAlt vars) where
  48 |         MkConAlt n1 _ t1 a1 e1 == MkConAlt n2 _ t2 a2 e2 = t1 == t2 && n1 == n2 && case namesEq a1 a2 of
  49 |             Just Refl => e1 == e2
  50 |             Nothing => False
  51 | 
  52 |     export
  53 |     covering
  54 |     Eq (CConstAlt vars) where
  55 |         MkConstAlt c1 e1 == MkConstAlt c2 e2 = c1 == c2 && e1 == e2
  56 | 
  57 | mutual
  58 |     export
  59 |     covering
  60 |     Ord (CExp vars) where
  61 |         CLocal {idx=x1} _ _ `compare` CLocal {idx=x2} _ _ = x1 `compare` x2
  62 |         CRef _ n1 `compare` CRef _ n2 = n1 `compare` n2
  63 |         CLam _ n1 e1 `compare` CLam _ n2 e2 = case nameEq n1 n2 of
  64 |             Just Refl => compare e1 e2
  65 |             Nothing => compare n1 n2
  66 |         CLet _ n1 _ val1 sc1 `compare` CLet _ n2 _ val2 sc2 = case nameEq n1 n2 of
  67 |             Just Refl => compare val1 val2 `thenCmp` compare sc1 sc2
  68 |             Nothing => compare n1 n2
  69 |         CApp _ f1 a1 `compare` CApp _ f2 a2 = compare f1 f2 `thenCmp` compare a1 a2
  70 |         CCon _ n1 _ t1 a1 `compare` CCon _ n2 _ t2 a2 = compare t1 t2 `thenCmp` compare n1 n2 `thenCmp` compare a1 a2
  71 |         COp _ f1 a1 `compare` COp _ f2 a2 = case primFnEq f1 f2 of
  72 |             Just Refl => compare a1 a2
  73 |             Nothing => primFnCmp f1 f2
  74 |         CExtPrim _ f1 a1 `compare` CExtPrim _ f2 a2 = compare f1 f2 `thenCmp` compare a1 a2
  75 |         CForce _ l1 e1 `compare` CForce _ l2 e2 = compare l1 l2 `thenCmp` compare e1 e2
  76 |         CDelay _ l1 e1 `compare` CDelay _ l2 e2 = compare l1 l2 `thenCmp` compare e1 e2
  77 |         CConCase _ s1 a1 d1 `compare` CConCase _ s2 a2 d2 = compare s1 s2 `thenCmp` compare a1 a2 `thenCmp` compare d1 d2
  78 |         CConstCase _ s1 a1 d1 `compare` CConstCase _ s2 a2 d2 = compare s1 s2 `thenCmp` compare a1 a2 `thenCmp` compare d1 d2
  79 |         CPrimVal _ c1 `compare` CPrimVal _ c2 = compare c1 c2
  80 |         CErased _ `compare` CErased _ = EQ
  81 |         CCrash _ m1 `compare` CCrash _ m2 = compare m1 m2
  82 |         e1 `compare` e2 = compare (tag e1) (tag e2)
  83 |           where
  84 |             tag : forall vars . CExp vars -> Int
  85 |             tag (CLocal {}) = 0
  86 |             tag (CRef {}) = 1
  87 |             tag (CLam {}) = 2
  88 |             tag (CLet {}) = 3
  89 |             tag (CApp {}) = 4
  90 |             tag (CCon {}) = 5
  91 |             tag (COp {}) = 6
  92 |             tag (CExtPrim {}) = 7
  93 |             tag (CForce {}) = 8
  94 |             tag (CDelay {}) = 9
  95 |             tag (CConCase {}) = 10
  96 |             tag (CConstCase {}) = 11
  97 |             tag (CPrimVal {}) = 12
  98 |             tag (CErased {}) = 13
  99 |             tag (CCrash {}) = 14
 100 | 
 101 |     export
 102 |     covering
 103 |     Ord (CConAlt vars) where
 104 |         MkConAlt n1 _ t1 a1 e1 `compare` MkConAlt n2 _ t2 a2 e2 =
 105 |             compare t1 t2 `thenCmp` compare n1 n2 `thenCmp` case namesEq a1 a2 of
 106 |                 Just Refl => compare e1 e2
 107 |                 Nothing => compare a1 a2
 108 | 
 109 |     export
 110 |     covering
 111 |     Ord (CConstAlt vars) where
 112 |         MkConstAlt c1 e1 `compare` MkConstAlt c2 e2 = compare c1 c2 `thenCmp` compare e1 e2
 113 |