<commit_before>module LinSpace where

{-@ measure orthDim :: PVector -> Int 
    orthDim (PVector v o z) = dim o
  @-}

{-@ measure tail :: [a] -> [a]
    tail (x:xs)  = xs
  @-}

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

{-@ measure orthSp :: PVector -> Space
    orthSp (PVector v m o) = o
  @-}

{-@ measure pvlen :: PVector -> Int
    pvlen (PVector v m o) = len v
  @-}

{-@ predicate SameLen  X Y = ((pvlen X)  = (pvlen Y))  @-}
{-@ predicate SameOrth X Y = ((orthSp X) = (orthSp Y)) @-}
{-@ type SameSpace X       = {v:PVector | ((SameLen X v) && (SameOrth X v))} @-}

{-@ measure isReal :: Space -> Prop
    isReal (Null)       = false
    isReal (Rreal pv n) = true
  @-}

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

-- ASSERT: length muCoeff == dim orthSpace
-- ASSERT: maybe True (\(v,_) -> length vec == length (vec v)) orthSpace 

{-@ predicate OrthMu  Orth Mu  = (dim Orth) = (len Mu) @-}

{-@ predicate OrthVec Orth Vec = (isReal Orth) => (len Vec) = (pvlen (spaceVec Orth)) @-}

{-@ data PVector = PVector { 
      vec  :: [Integer]   
    , mu   :: [Integer] 
    , orth :: {v: Space | ((OrthMu v mu) && (OrthVec v vec))}
    } 
  @-}

--------------------
-- "dim" and "sameSpace" are only used in the ASSERTs
dim             :: Space -> Int 
dim Null        = 0
dim (Real pv _) = 1 + dim (orthSpace pv)

sameSpace :: PVector -> PVector -> Bool
sameSpace pv1 pv2 = 
  (length (vec pv1) == length (vec pv2)) && (orthSpace pv1 == orthSpace pv2)
--------------------

data PVector = PVector { 
    vec       :: [Integer]    -- vector coordinates
  , muCoeff   :: [Integer]    -- <vec,bn*>det^2(b[1..n-1]) : ... 
  , orthSpace :: Space        -- lattice basis
  } deriving (Show, Eq)

-- Orthogonalized vector bn* and squared lattice determinant 
-- type Space = Maybe (PVector, Integer) 

data Space 
  = Null 
  | Real PVector Integer
  deriving (Show, Eq)

-- squared determinant of orthSpace
detPV :: PVector -> Integer 
-- detPV = maybe 1 snd . orthSpace
detPV (PVector _ _ Null)       = 1
detPV (PVector _ _ (Real _ n)) = n

-- peel off last layer of projection from PVector
-- ASSERT: dim (orthSpace (liftPV v)) == dim (orthSpace v) - 1
{-@ liftPV :: pv:PVector -> {v:PVector | ((orthSp v) = (tail (orthSp pv)) && ((orthDim v) = (orthDim pv) - 1))} @-}
liftPV (PVector v (m:mu) (Real pv _)) = PVector v mu (orthSpace pv)

-- dot product of two vectors
-- ASSERT: length xs == length ys
{-@ dot :: (Num a) => xs:[a] -> {v:[a] | (len v) = (len xs)} -> a @-}
dot xs ys = sum (zipWith (*) xs ys)<commit_msg>Asdasd<commit_after>module LinSpace where

{-@ measure orthDim :: PVector -> Int 
    orthDim (PVector v o z) = (dim o)
  @-}

{-@ measure tail :: [a] -> [a]
    tail (x:xs)  = xs
  @-}

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

{-@ measure orthSp :: PVector -> Space
    orthSp (PVector v m o) = o
  @-}

{-@ measure pvlen :: PVector -> Int
    pvlen (PVector v m o) = (len v)
  @-}

{-@ predicate SameLen  X Y = ((pvlen X)  = (pvlen Y))  @-}
{-@ predicate SameOrth X Y = ((orthSp X) = (orthSp Y)) @-}
{-@ type SameSpace X       = {v:PVector | ((SameLen X v) && (SameOrth X v))} @-}

{-@ measure isReal :: Space -> Prop
    isReal (Null)       = false
    isReal (Rreal pv n) = true
  @-}

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

-- ASSERT: length muCoeff == dim orthSpace
-- ASSERT: maybe True (\(v,_) -> length vec == length (vec v)) orthSpace 

{-@ predicate OrthMu  Orth Mu  = (dim Orth) = (len Mu) @-}

{-@ predicate OrthVec Orth Vec = ((isReal Orth) => (len Vec) = (pvlen (spaceVec Orth))) @-}

{-@ data PVector = PVector { 
      vec  :: [Integer]   
    , mu   :: [Integer] 
    , orth :: {v: Space | ((OrthMu v mu) && (OrthVec v vec))}
    } 
  @-}

--------------------
-- "dim" and "sameSpace" are only used in the ASSERTs
dim             :: Space -> Int 
dim Null        = 0
dim (Real pv _) = 1 + dim (orthSpace pv)

sameSpace :: PVector -> PVector -> Bool
sameSpace pv1 pv2 = 
  (length (vec pv1) == length (vec pv2)) && (orthSpace pv1 == orthSpace pv2)
--------------------

data PVector = PVector { 
    vec       :: [Integer]    -- vector coordinates
  , muCoeff   :: [Integer]    -- <vec,bn*>det^2(b[1..n-1]) : ... 
  , orthSpace :: Space        -- lattice basis
  } deriving (Show, Eq)

-- Orthogonalized vector bn* and squared lattice determinant 
-- type Space = Maybe (PVector, Integer) 

data Space = Null | Real PVector Integer
  deriving (Show, Eq)

-- squared determinant of orthSpace
detPV :: PVector -> Integer 
-- detPV = maybe 1 snd . orthSpace
detPV (PVector _ _ Null)       = 1
detPV (PVector _ _ (Real _ n)) = n

-- peel off last layer of projection from PVector
-- ASSERT: dim (orthSpace (liftPV v)) == dim (orthSpace v) - 1
{-@ liftPV :: pv:PVector -> {v:PVector | ((orthSp v) = (tail (orthSp pv)) && ((orthDim v) = (orthDim pv) - 1))} @-}
liftPV (PVector v (m:mu) (Real pv _)) = PVector v mu (orthSpace pv)

-- dot product of two vectors
-- ASSERT: length xs == length ys
{-@ dot :: (Num a) => xs:[a] -> {v:[a] | (len v) = (len xs)} -> a @-}
dot xs ys = sum (zipWith (*) xs ys)
{'fraction_non_alphanumeric': 0.18856377892522472, 'fraction_numerical': 0.00650219927328361, 'mean_word_length': 2.3333333333333335, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6850786', 'n_tokens_mistral': 2018, 'n_tokens_neox': 1920, 'n_words': 639}