module UVMHS.Lib.Parser.Loc where

import UVMHS.Core

import UVMHS.Lib.Pretty

data Loc = Loc
  { Loc -> ℕ64 ∧ ℕ64
locPos ∷ ℕ64 ∧ ℕ64
  , Loc -> ℕ64
locRow ∷ ℕ64
  , Loc -> ℕ64
locCol ∷ ℕ64
  } deriving (Int -> Loc -> ShowS
[Loc] -> ShowS
Loc -> String
(Int -> Loc -> ShowS)
-> (Loc -> String) -> ([Loc] -> ShowS) -> Show Loc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Loc -> ShowS
showsPrec :: Int -> Loc -> ShowS
$cshow :: Loc -> String
show :: Loc -> String
$cshowList :: [Loc] -> ShowS
showList :: [Loc] -> ShowS
Show)
makeLenses ''Loc
makePrettyRecord ''Loc

instance Eq Loc where == :: Loc -> Loc -> Bool
(==) = (ℕ64 ∧ ℕ64) -> (ℕ64 ∧ ℕ64) -> Bool
forall a. Eq a => a -> a -> Bool
(==) ((ℕ64 ∧ ℕ64) -> (ℕ64 ∧ ℕ64) -> Bool)
-> (Loc -> ℕ64 ∧ ℕ64) -> Loc -> Loc -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Loc -> ℕ64 ∧ ℕ64
locPos
instance Ord Loc where compare :: Loc -> Loc -> Ordering
compare = (ℕ64 ∧ ℕ64) -> (ℕ64 ∧ ℕ64) -> Ordering
forall a. Ord a => a -> a -> Ordering
(⋚) ((ℕ64 ∧ ℕ64) -> (ℕ64 ∧ ℕ64) -> Ordering)
-> (Loc -> ℕ64 ∧ ℕ64) -> Loc -> Loc -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Loc -> ℕ64 ∧ ℕ64
locPos

instance Bot Loc where bot :: Loc
bot = (ℕ64 ∧ ℕ64) -> ℕ64 -> ℕ64 -> Loc
Loc ℕ64 ∧ ℕ64
forall a. Bot a => a
bot ℕ64
forall a. Bot a => a
bot ℕ64
forall a. Bot a => a
bot
instance Join Loc where Loc
l₁ ⊔ :: Loc -> Loc -> Loc
⊔ Loc
l₂ = if Loc -> ℕ64 ∧ ℕ64
locPos Loc
l₁ (ℕ64 ∧ ℕ64) -> (ℕ64 ∧ ℕ64) -> Bool
forall a. Ord a => a -> a -> Bool
≥ Loc -> ℕ64 ∧ ℕ64
locPos Loc
l₂ then Loc
l₁ else Loc
l₂
instance JoinLattice Loc
instance Meet Loc where Loc
l₁ ⊓ :: Loc -> Loc -> Loc
⊓ Loc
l₂ = if Loc -> ℕ64 ∧ ℕ64
locPos Loc
l₁ (ℕ64 ∧ ℕ64) -> (ℕ64 ∧ ℕ64) -> Bool
forall a. Ord a => a -> a -> Bool
≤ Loc -> ℕ64 ∧ ℕ64
locPos Loc
l₂ then Loc
l₁ else Loc
l₂

bumpRow₁ ∷ Loc → Loc
bumpRow₁ :: Loc -> Loc
bumpRow₁ (Loc (ℕ64
pos₁ :* ℕ64
pos₂) ℕ64
row ℕ64
_) = (ℕ64 ∧ ℕ64) -> ℕ64 -> ℕ64 -> Loc
Loc ((ℕ64
pos₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one) ℕ64 -> ℕ64 -> ℕ64 ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
pos₂) (ℕ64
row ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one) ℕ64
forall a. Zero a => a
zero

bumpCol₁ ∷ Loc → Loc
bumpCol₁ :: Loc -> Loc
bumpCol₁ (Loc (ℕ64
pos₁ :* ℕ64
pos₂) ℕ64
row ℕ64
col) = (ℕ64 ∧ ℕ64) -> ℕ64 -> ℕ64 -> Loc
Loc ((ℕ64
pos₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one) ℕ64 -> ℕ64 -> ℕ64 ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
pos₂) ℕ64
row (ℕ64
col ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one)

bumpCol₂ ∷ Loc → Loc
bumpCol₂ :: Loc -> Loc
bumpCol₂ (Loc (ℕ64
pos₁ :* ℕ64
pos₂) ℕ64
row ℕ64
col) = (ℕ64 ∧ ℕ64) -> ℕ64 -> ℕ64 -> Loc
Loc (ℕ64
pos₁ ℕ64 -> ℕ64 -> ℕ64 ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* (ℕ64
pos₂ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one)) ℕ64
row (ℕ64
col ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one)

-- # LocRange

data LocRange = LocRange
  { LocRange -> AddBT Loc
locRangeBegin ∷ AddBT Loc
  , LocRange -> AddBT Loc
locRangeEnd ∷ AddBT Loc
  } deriving (LocRange -> LocRange -> Bool
(LocRange -> LocRange -> Bool)
-> (LocRange -> LocRange -> Bool) -> Eq LocRange
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocRange -> LocRange -> Bool
== :: LocRange -> LocRange -> Bool
$c/= :: LocRange -> LocRange -> Bool
/= :: LocRange -> LocRange -> Bool
Eq,Eq LocRange
Eq LocRange =>
(LocRange -> LocRange -> Ordering)
-> (LocRange -> LocRange -> Bool)
-> (LocRange -> LocRange -> Bool)
-> (LocRange -> LocRange -> Bool)
-> (LocRange -> LocRange -> Bool)
-> (LocRange -> LocRange -> LocRange)
-> (LocRange -> LocRange -> LocRange)
-> Ord LocRange
LocRange -> LocRange -> Bool
LocRange -> LocRange -> Ordering
LocRange -> LocRange -> LocRange
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LocRange -> LocRange -> Ordering
compare :: LocRange -> LocRange -> Ordering
$c< :: LocRange -> LocRange -> Bool
< :: LocRange -> LocRange -> Bool
$c<= :: LocRange -> LocRange -> Bool
<= :: LocRange -> LocRange -> Bool
$c> :: LocRange -> LocRange -> Bool
> :: LocRange -> LocRange -> Bool
$c>= :: LocRange -> LocRange -> Bool
>= :: LocRange -> LocRange -> Bool
$cmax :: LocRange -> LocRange -> LocRange
max :: LocRange -> LocRange -> LocRange
$cmin :: LocRange -> LocRange -> LocRange
min :: LocRange -> LocRange -> LocRange
Ord,Int -> LocRange -> ShowS
[LocRange] -> ShowS
LocRange -> String
(Int -> LocRange -> ShowS)
-> (LocRange -> String) -> ([LocRange] -> ShowS) -> Show LocRange
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LocRange -> ShowS
showsPrec :: Int -> LocRange -> ShowS
$cshow :: LocRange -> String
show :: LocRange -> String
$cshowList :: [LocRange] -> ShowS
showList :: [LocRange] -> ShowS
Show)
makeLenses ''LocRange
makePrettyUnion ''LocRange

bumpColEnd₂ ∷ LocRange → LocRange
bumpColEnd₂ :: LocRange -> LocRange
bumpColEnd₂ (LocRange AddBT Loc
b AddBT Loc
e) = AddBT Loc -> AddBT Loc -> LocRange
LocRange AddBT Loc
b (Loc -> Loc
bumpCol₂ (Loc -> Loc) -> AddBT Loc -> AddBT Loc
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ AddBT Loc
e)

instance Bot LocRange where bot :: LocRange
bot = AddBT Loc -> AddBT Loc -> LocRange
LocRange AddBT Loc
forall a. Top a => a
top AddBT Loc
forall a. Bot a => a
bot
instance Top LocRange where top :: LocRange
top = AddBT Loc -> AddBT Loc -> LocRange
LocRange AddBT Loc
forall a. Bot a => a
bot AddBT Loc
forall a. Top a => a
top

instance Join LocRange where LocRange AddBT Loc
b₁ AddBT Loc
e₁ ⊔ :: LocRange -> LocRange -> LocRange
⊔ LocRange AddBT Loc
b₂ AddBT Loc
e₂ = AddBT Loc -> AddBT Loc -> LocRange
LocRange (AddBT Loc
b₁ AddBT Loc -> AddBT Loc -> AddBT Loc
forall a. Meet a => a -> a -> a
⊓ AddBT Loc
b₂) (AddBT Loc
e₁ AddBT Loc -> AddBT Loc -> AddBT Loc
forall a. Join a => a -> a -> a
⊔ AddBT Loc
e₂)
instance Meet LocRange where LocRange AddBT Loc
b₁ AddBT Loc
e₁ ⊓ :: LocRange -> LocRange -> LocRange
⊓ LocRange AddBT Loc
b₂ AddBT Loc
e₂ = AddBT Loc -> AddBT Loc -> LocRange
LocRange (AddBT Loc
b₁ AddBT Loc -> AddBT Loc -> AddBT Loc
forall a. Join a => a -> a -> a
⊔ AddBT Loc
b₂) (AddBT Loc
e₁ AddBT Loc -> AddBT Loc -> AddBT Loc
forall a. Meet a => a -> a -> a
⊓ AddBT Loc
e₂)

locRange₀ ∷ LocRange
locRange₀ :: LocRange
locRange₀ = AddBT Loc -> AddBT Loc -> LocRange
LocRange AddBT Loc
forall a. Bot a => a
bot AddBT Loc
forall a. Bot a => a
bot