{-# LANGUAGE ScopedTypeVariables #-}

{-@ LIQUID "--no-termination" @-}

module LinSpace () where


data PVector = PVector [Integer] [Integer] (Space PVector) -- { 

-- | Orthogonalized vector bn* and squared lattice determinant 
data Space a = Null | Real a Integer

{-@ data PVector = PVector { 
      pec_  :: [Integer]   
    , mu_   :: [Integer] 
    , orth_ :: {v: (Space (PVectorN (len pec_))) | (dim v) = (len mu_)}
    } 
  @-}

{-@ data Space [dim] @-}

{-@ measure dim     :: (Space PVector) -> Int 
    dim (Null)      = 0
    dim (Real pv n) = 1 + (dim (orthSpace pv))
  @-}

{-@ measure spaceVec     :: (Space PVector) -> PVector
    spaceVec (Real pv n) = pv
  @-}

{-@ measure vec :: PVector -> [Integer]
    vec (PVector p m o) = p
  @-}
{-@ measure orthSpace :: PVector -> (Space PVector)
    orthSpace (PVector v m o) = o
  @-}

{-@ measure muCoeff :: PVector -> [Integer]
    muCoeff (PVector v m o) = m 
  @-}

--  If the above v is renames to anything else the test is SAFE
-- this v creates a type for PVector
-- PVector :: v{} -> m {} -> o{}
-- and the argument bind v clashs with the special value v....

{-@ invariant {v: PVector | (Inv v) }    @-}
{-@ invariant {v: Space | (dim v) >= 0 } @-}

-- RJ: Helpers for defining properties

{-@ predicate Inv V        = (dim (orthSpace V)) = (len (muCoeff V)) @-}
{-@ predicate SameLen  X Y = ((len (vec X))  = (len (vec Y)))  @-}
{-@ predicate SameOrth X Y = ((orthSpace X) = (orthSpace Y)) @-}

-- RJ: Useful type aliases for specs

{-@ type SameSpace X       = {v:PVector | ((Inv v) && (SameLen X v) && (SameOrth X v))} @-}
{-@ type PVectorN N        = {v: PVector | (len (vec v)) = N}   @-} 
{-@ type PVectorP P        = {v: PVector | (SameLen v P)}       @-} 

--------------------


{-@ orthSpace_ :: p:PVector -> (Space (PVectorP p))  @-} 
orthSpace_ (PVector v m o) = o