liquidhaskell-0.8.0.2: tests/strings/pos/StringIndexingStep3.hs
{-
NV TODO
1. refine data type
2. connect it with Steps 1 & 2
3. connect it with dyn programming
-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--totality" @-}
{-@ LIQUID "--exactdc" @-}
module Main where
import Language.Haskell.Liquid.String
import GHC.TypeLits
import Data.String hiding (fromString)
import Data.Proxy
import Prelude hiding (mempty, mappend, id, mconcat, map)
import Language.Haskell.Liquid.ProofCombinators
import Data.Maybe
-- | Interface
main :: IO ()
main =
do input <- fromString <$> readFile "input.txt"
let mi1 = toMI input :: MI "abcab" SMTString
let is1 = getIndex mi1
putStrLn ("Serial Indices: " ++ show is1)
let mi2 = toMIPar input :: MI "abcab" SMTString
let is2 = getIndex mi2
putStrLn ("Parallel Indices: " ++ show is2)
putStrLn ("Are equal? " ++ show (is1 == is2))
{-
main :: IO ()
main =
do input <- fromString <$> readFile "input.txt"
case someSymbolVal "x" of
SomeSymbol (_ :: Proxy y) ->
let mi1 = toMI input :: MI y SMTString
let is1 = getIndex mi1
putStrLn ("Serial Indices: " ++ show is1)
let mi2 = toMIPar input :: MI "abcab" SMTString
let is2 = getIndex mi2
putStrLn ("Parallel Indices: " ++ show is2)
putStrLn ("Are equal? " ++ show (is1 == is2))
-}
test1 = indices input1
input1 = fromString $ clone 100 "ababcabcab"
indices :: SMTString -> List Int
indices input
= case toMI input :: MI "abcab" SMTString of
MI _ i -> i
{-
|
-}
mconcatPar :: forall (target :: Symbol). (KnownSymbol target) => Int -> [MI target SMTString] -> MI target SMTString
mconcatPar n xs = mconcat (mconcatPar' n xs)
{-@ Lazy mconcatPar' @-}
-- Termination proof is terribly slow and will change...
{-@ mconcatPar' :: forall (target :: Symbol). (KnownSymbol target) => Int -> xs:[MI target SMTString] -> [MI target SMTString] @-}
mconcatPar' :: forall (target :: Symbol). (KnownSymbol target) => Int -> [MI target SMTString] -> [MI target SMTString]
mconcatPar' n xs | length xs <= n = [mconcat xs]
mconcatPar' n xs = let (x, r) = splitAt n xs
in mconcatPar' n (mconcat x:mconcatPar' n r)
toMIPar :: forall (target :: Symbol). (KnownSymbol target) => SMTString -> MI target SMTString
toMIPar input = undefined
toMI :: forall (target :: Symbol). (KnownSymbol target) => SMTString -> MI target SMTString
toMI input = if isNullString input then mempty else MI input (makeIndices input (fromString (symbolVal (Proxy :: Proxy target))) 0 (stringLen input - 1))
getIndex :: forall (target :: Symbol). MI target SMTString -> List Int
getIndex (MI _ i) = i
clone :: Int -> [a] -> [a]
clone i xs | i <= 0 = []
clone 1 xs = xs
clone n xs = xs ++ clone (n-1) xs
mconcat :: forall (target :: Symbol). (KnownSymbol target) => [MI target SMTString] -> MI target SMTString
mconcat [] = mempty
mconcat [x] = x
mconcat [x1, x2] = mappend x1 x2
mconcat (x:xs) = mappend x (mconcat xs)
-- | Indexing Structure Definition
-- Structure that defines valid indeces of a type level target
-- symbol in a value level string
data MI (target :: Symbol) s where
MI :: SMTString -- input string
-> (List Int) -- valid indeces of target in input
-> MI target s
deriving (Show)
{-@ data MI target s
= MI { input :: SMTString
, idxes :: List Int
} @-}
{- data MI target s
= MI { input :: SMTString
, List :: List (GoodIndex input target)
} @-}
{-@ measure indixesMI @-}
indixesMI (MI _ is) = is
{-@ measure inputMI @-}
inputMI (MI i _) = i
{-@ type GoodIndex Input Target
= {i:Int | IsGoodIndex Input Target i}
@-}
{-@ type GoodIndexTwo Input Input2 Target
= {i:Int | IsGoodIndex Input Target i && IsGoodIndex (concatString Input Input2) Target i }
@-}
{-@ predicate IsGoodIndex Input Target I
= (subString Input I (stringLen Target) == Target)
&& (I + stringLen Target <= stringLen Input)
&& (0 <= I)
@-}
-- | Monoid methods
{-@ reflect mempty @-}
mempty :: forall (target :: Symbol). MI target SMTString
mempty = MI stringEmp N
{-@ reflect mappend @-}
mappend :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> MI target SMTString -> MI target SMTString
mappend (MI i1 is1) (MI i2 is2)
= MI (concatString i1 i2) -- (mappendMakeIndixes i1 i2 (fromString (symbolVal (Proxy :: Proxy target))) is1 is2)
((is1
`append`
makeNewIndices i1 i2 (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen i1)) is2)
-------------------------------------------------------------------------------
--------------- PROOFS -------------------------------------------------------
-------------------------------------------------------------------------------
mempty_left :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> Proof
{-@ mempty_left :: xs:MI target SMTString -> {mappend xs mempty == xs } @-}
mempty_left (MI i1 is1)
= mappend (MI i1 is1) (mempty :: MI target SMTString)
==. mappend (MI i1 is1) (MI stringEmp N)
==. MI (concatString i1 stringEmp)
(is1 `append` map (shift (stringLen i1)) N
`append` makeNewIndices i1 stringEmp (fromString (symbolVal (Proxy :: Proxy target))))
==. MI (concatString i1 stringEmp)
((is1 `append` N)
`append` makeNewIndices i1 stringEmp (fromString (symbolVal (Proxy :: Proxy target))))
==. MI (concatString i1 stringEmp)
(is1 `append` makeNewIndices i1 stringEmp (fromString (symbolVal (Proxy :: Proxy target))))
? appendEmp is1
==. MI (concatString i1 stringEmp)
(is1 `append` N)
? makeNewIndicesNullLeft i1 (fromString (symbolVal (Proxy :: Proxy target)))
==. MI (concatString i1 stringEmp) is1
? appendEmp is1
==. MI i1 is1
? concatStringNeutral i1
*** QED
mempty_right :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> Proof
{-@ mempty_right :: xs:MI target SMTString -> {mappend mempty xs == xs } @-}
mempty_right (MI i is)
= mappend (mempty :: MI target SMTString) (MI i is)
==. mappend (MI stringEmp N) (MI i is)
==. MI (concatString stringEmp i)
(N `append` makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
`append` map (shift (stringLen stringEmp)) is)
==. MI (concatString stringEmp i)
( makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
`append`
map (shift (stringLen stringEmp)) is)
==. MI (concatString stringEmp i)
( makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
`append`
map (shift 0) is)
==. MI (concatString stringEmp i)
(makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
`append`
is)
? mapShiftZero is
==. MI (concatString stringEmp i)
(N `append` is)
? makeNewIndicesNullRight i (fromString (symbolVal (Proxy :: Proxy target)))
==. MI (concatString stringEmp i) is
==. MI i is
? concatStringNeutralRight i
*** QED
{-@ mappend_assoc
:: x:MI target SMTString -> y:MI target SMTString -> z:MI target SMTString
-> {v:Proof | mappend x (mappend y z) = mappend (mappend x y) z}
@-}
mappend_assoc
:: forall (target :: Symbol). (KnownSymbol target)
=> MI target SMTString -> MI target SMTString -> MI target SMTString -> Proof
mappend_assoc x@(MI xi xis) y@(MI yi yis) z@(MI zi zis)
| stringLen (fromString (symbolVal (Proxy :: Proxy target))) <= stringLen yi
= mappend x (mappend y z)
==. mappend (MI xi xis) (mappend (MI yi yis) (MI zi zis))
==. mappend (MI xi xis)
(MI (concatString yi zi)
((yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis))
==. MI (concatString xi (concatString yi zi))
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi))
((yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis)
)
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi))
((yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis)
)
? concatStringAssoc xi yi zi
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
(
(map (shift (stringLen xi)) (yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
`append`
map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
)
? map_append (shift (stringLen xi))
(yis `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
(map (shift (stringLen yi)) zis)
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
(
(map (shift (stringLen xi)) yis
`append` (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))))
`append`
map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
)
? map_append (shift (stringLen xi)) yis (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
(
(map (shift (stringLen xi)) yis
`append` (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))))
`append`
map (shift (stringLen (concatString xi yi))) zis)
)
? map_len_fusion xi yi zis
-- ((x1~x2) ~ ((x3~x4) ~ x5))
-- ==
-- ((((x1~x2) ~x3) ~x4) ~x5
==. MI (concatString (concatString xi yi) zi)
(((( xis
`append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target)))) `append` map (shift (stringLen xi)) yis)
`append`
map (shift (stringLen xi)) yis)
`append`
map (shift (stringLen (concatString xi yi))) zis)
? appendReorder xis
(makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
(map (shift (stringLen xi)) yis)
(map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
(map (shift (stringLen (concatString xi yi))) zis)
-- ((((x1 ~ x2) ~ x3) ~ x4) ~ x5)
--
-- ((((x1 ~ x2) ~ x3) ~ x4) ~ x5)
==. MI (concatString (concatString xi yi) zi)
(((( xis
`append`
makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi)) yis)
`append`
makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen (concatString xi yi))) zis
)
? shiftIndexes xi yi zi (fromString (symbolVal (Proxy :: Proxy target)))
==. mappend (MI (concatString xi yi)
( (xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) yis
)
) (MI zi zis)
==. mappend (mappend (MI xi xis) (MI yi yis)) (MI zi zis)
*** QED
mappend_assoc x@(MI xi xis) y@(MI yi yis) z@(MI zi zis)
| stringLen yi < stringLen (fromString (symbolVal (Proxy :: Proxy target)))
= mappend x (mappend y z)
==. mappend (MI xi xis) (mappend (MI yi yis) (MI zi zis))
==. mappend (MI xi xis)
(MI (concatString yi zi)
((yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis))
==. MI (concatString xi (concatString yi zi))
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi))
((yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis)
)
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi))
((yis
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis)
)
? concatStringAssoc xi yi zi
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi))
((N
`append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen yi)) zis)
)
? emptyIndexes y (assumeGoodIndex yi (fromString (symbolVal (Proxy :: Proxy target))) yis)
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
map (shift (stringLen xi))
(makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))
`append` map (shift (stringLen yi)) zis)
)
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
(map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
)
? map_append (shift (stringLen xi))
(makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
(map (shift (stringLen yi)) zis)
==. MI (concatString (concatString xi yi) zi)
((xis `append`
makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
`append`
(map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
)
? map_len_fusion xi yi zis
-- ((x1~x2) ~ (x3~x4))
-- ==
-- (x1 ~ (x2~x3)) ~ x4
==. MI (concatString (concatString xi yi) zi)
((xis `append`
(makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target)))
`append`
map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
`append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
)
? appendGroupNew xis
(makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
(map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
(map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
==. MI (concatString (concatString xi yi) zi)
((xis `append`
(makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target)))
`append`
makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
)
? shiftNewIndexes xi yi zi (fromString (symbolVal (Proxy :: Proxy target)))
==. MI (concatString (concatString xi yi) zi)
((xis `append`
(makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target)))
`append`
makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen (concatString xi yi))) zis)
)
? map_len_fusion xi yi zis
-- (x1 ~ (x2 ~ x3)) ~ x4 == ((x1 ~ x2) ~ x3) ~ x4
==. MI (concatString (concatString xi yi) zi)
(((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append`
(makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
`append`
map (shift (stringLen (concatString xi yi))) zis )
? appendUnGroupNew xis
(makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
(makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
(map (shift (stringLen (concatString xi yi))) zis)
==. MI (concatString (concatString xi yi) zi)
((((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append` N
)
`append`
(makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
`append`
map (shift (stringLen (concatString xi yi))) zis )
? appendEmp (xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
==. MI (concatString (concatString xi yi) zi)
((((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) N
)
`append`
(makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
`append`
map (shift (stringLen (concatString xi yi))) zis )
==. MI (concatString (concatString xi yi) zi)
((((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) yis
)
`append`
(makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
`append`
map (shift (stringLen (concatString xi yi))) zis )
?emptyIndexes y (assumeGoodIndex yi (fromString (symbolVal (Proxy :: Proxy target))) yis)
==. mappend (MI (concatString xi yi)
( (xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
`append` map (shift (stringLen xi)) yis
)
) (MI zi zis)
==. mappend (mappend (MI xi xis) (MI yi yis)) (MI zi zis)
*** QED
-------------------------------------------------------------------------------
------------------ Helper Proofs ----------------------------------------------
-------------------------------------------------------------------------------
{-@ assumeGoodIndex :: input:SMTString -> target:SMTString -> is:List Int
-> {v:List (GoodIndex input target) | v == is} @-}
assumeGoodIndex :: SMTString -> SMTString -> List Int -> List Int
assumeGoodIndex input target is
= if isJust (areGoodIndexes input target is) then fromJust (areGoodIndexes input target is) else error ""
{-@ areGoodIndexes :: input:SMTString -> target:SMTString -> is:List Int
-> Maybe ({v:List (GoodIndex input target) | v == is}) @-}
areGoodIndexes :: SMTString -> SMTString -> List Int -> Maybe (List Int)
areGoodIndexes input target N
= Just N
areGoodIndexes input target (C x xs)
| isGoodIndex input target x
= case areGoodIndexes input target xs of
Nothing -> Nothing
Just is -> Just (C x is)
| otherwise
= Nothing
emptyIndexes :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> List Int -> Proof
{-@ emptyIndexes :: mi:MI target SMTString
-> is:{List (GoodIndex (inputMI mi) target) | is == indixesMI mi && stringLen (inputMI mi) < stringLen target}
-> { is == N } @-}
emptyIndexes (MI _ _) N
= trivial
emptyIndexes (MI _ _) (C _ _)
= trivial
{-@ shiftIndexes
:: xi:SMTString
-> yi:SMTString
-> zi:SMTString
-> tg:{SMTString | stringLen tg <= stringLen yi }
-> { (makeNewIndices xi (concatString yi zi) tg == makeNewIndices xi yi tg)
&&
(map (shift (stringLen xi)) (makeNewIndices yi zi tg) == makeNewIndices (concatString xi yi) zi tg)
}
@-}
shiftIndexes :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
shiftIndexes xi yi zi tg = shiftIndexesLeft xi yi zi tg &&& shiftIndexesRight xi yi zi tg
{-@ reflect chunkString @-}
{-@ chunkString :: Int -> xs:SMTString -> List (SMTString) / [stringLen xs] @-}
chunkString :: Int -> SMTString -> List (SMTString)
chunkString i xs
| i <= 0
= C xs N
| stringLen xs <= i
= C xs N
| otherwise
= C (takeString i xs) (chunkString i (dropString i xs))
{-@ shiftIndexesLeft
:: xi:SMTString
-> yi:SMTString
-> zi:SMTString
-> tg:{SMTString | stringLen tg <= stringLen yi }
-> { makeNewIndices xi (concatString yi zi) tg == makeNewIndices xi yi tg}
@-}
shiftIndexesLeft :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
shiftIndexesLeft xi yi zi tg
| stringLen tg < 2
= makeNewIndices xi (concatString yi zi) tg
==. N
==. makeNewIndices xi yi tg
*** QED
| otherwise
= makeNewIndices xi (concatString yi zi) tg
==. makeIndices (concatString xi (concatString yi zi)) tg
(maxInt (stringLen xi - (stringLen tg-1)) 0)
(stringLen xi - 1)
==. makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen xi - (stringLen tg-1)) 0)
(stringLen xi - 1)
?concatStringAssoc xi yi zi
==. makeIndices (concatString xi yi) tg
(maxInt (stringLen xi - (stringLen tg-1)) 0)
(stringLen xi - 1)
? concatmakeNewIndices (maxInt (stringLen xi - (stringLen tg-1)) 0) (stringLen xi - 1) tg (concatString xi yi) zi
==. makeNewIndices xi yi tg
*** QED
{-@ concatmakeNewIndices
:: lo:Nat -> hi:Int
-> target: SMTString
-> input : {SMTString | hi + stringLen target <= stringLen input }
-> input': SMTString
-> { makeIndices (concatString input input') target lo hi == makeIndices input target lo hi }
/ [hi - lo] @-}
concatmakeNewIndices :: Int -> Int -> SMTString -> SMTString -> SMTString -> Proof
concatmakeNewIndices lo hi target input input'
| hi < lo
= makeIndices input target lo hi
==. N
==. makeIndices (concatString input input') target lo hi
*** QED
| lo == hi, isGoodIndex input target lo
= makeIndices input target lo hi
==. lo `C` N
==. makeIndices (concatString input input') target lo hi
? isGoodIndexConcatString input input' target lo
*** QED
| lo == hi
= makeIndices input target lo hi
==. N
==. makeIndices (concatString input input') target lo hi
? isGoodIndexConcatString input input' target lo
*** QED
concatmakeNewIndices lo hi target input input'
| isGoodIndex input target lo
= makeIndices input target lo hi
==. lo `C` (makeIndices input target (lo + 1) hi)
==. lo `C` (makeIndices (concatString input input') target (lo + 1) hi)
? concatmakeNewIndices (lo+1) hi target input input'
==. makeIndices (concatString input input') target lo hi
? isGoodIndexConcatString input input' target lo
*** QED
| otherwise
= makeIndices input target lo hi
==. makeIndices input target (lo + 1) hi
==. makeIndices (concatString input input') target (lo + 1) hi
? concatmakeNewIndices (lo+1) hi target input input'
==. makeIndices (concatString input input') target lo hi
? isGoodIndexConcatString input input' target lo
*** QED
{-@ isGoodIndexConcatFront
:: input:SMTString -> input':SMTString -> tg:SMTString -> i:Nat
-> {((isGoodIndex input tg i) <=> isGoodIndex (concatString input' input) tg (stringLen input' + i) )
} @-}
isGoodIndexConcatFront :: SMTString -> SMTString -> SMTString -> Int -> Proof
isGoodIndexConcatFront input input' tg i
= isGoodIndex input tg i
==. (subString input i (stringLen tg) == tg
&& i + stringLen tg <= stringLen input
&& 0 <= i)
==. (subString input i (stringLen tg) == tg
&& (stringLen input' + i) + stringLen tg <= stringLen (concatString input' input)
&& 0 <= i)
==. (subString (concatString input' input) (stringLen input' + i) (stringLen tg) == tg
&& (stringLen input' + i) + stringLen tg <= stringLen (concatString input' input)
&& 0 <= (stringLen input' + i))
? (subStringConcatFront input input' (stringLen tg) i *** QED)
==. isGoodIndex (concatString input' input) tg (stringLen input' + i)
*** QED
{-@ isGoodIndexConcatString
:: input:SMTString -> input':SMTString -> tg:SMTString -> i:{Int | i + stringLen tg <= stringLen input }
-> {((isGoodIndex input tg i) <=> isGoodIndex (concatString input input') tg i)
} @-}
isGoodIndexConcatString :: SMTString -> SMTString -> SMTString -> Int -> Proof
isGoodIndexConcatString input input' tg i
= isGoodIndex input tg i
==. (subString input i (stringLen tg) == tg
&& i + stringLen tg <= stringLen input
&& 0 <= i)
==. (subString (concatString input input') i (stringLen tg) == tg
&& i + stringLen tg <= stringLen input
&& 0 <= i)
? (subStringConcat input input' (stringLen tg) i *** QED )
==. (subString (concatString input input') i (stringLen tg) == tg
&& i + stringLen tg <= stringLen (concatString input input')
&& 0 <= i)
? (((stringLen input <= stringLen (concatString input input') *** QED ) &&& (lenConcat input input') *** QED))
==. isGoodIndex (concatString input input') tg i
*** QED
{-@ shiftIndexesRight
:: xi:SMTString
-> yi:SMTString
-> zi:SMTString
-> tg:{SMTString | stringLen tg <= stringLen yi }
-> { map (shift (stringLen xi)) (makeNewIndices yi zi tg) == makeNewIndices (concatString xi yi) zi tg }
@-}
shiftIndexesRight :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
shiftIndexesRight xi yi zi tg
| stringLen tg < 2
= makeNewIndices (concatString xi yi) zi tg
==. N
==. map (shift (stringLen xi)) N
==. map (shift (stringLen xi)) (makeNewIndices yi zi tg)
*** QED
shiftIndexesRight xi yi zi tg
-- NV NV NV
-- This is suspicious!!! it should require exactly the precondition
-- || tg || <= || yi ||
-- | stringLen tg <= stringLen yi + 1
= makeNewIndices (concatString xi yi) zi tg
==. makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen (concatString xi yi) - (stringLen tg -1)) 0)
(stringLen (concatString xi yi) - 1 )
==. makeIndices (concatString (concatString xi yi) zi) tg
(stringLen (concatString xi yi) - (stringLen tg -1))
(stringLen (concatString xi yi) - 1 )
==. makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi + stringLen yi - stringLen tg + 1)
(stringLen xi + stringLen yi - 1 )
==. makeIndices (concatString xi (concatString yi zi)) tg
(stringLen xi + stringLen yi - stringLen tg + 1)
(stringLen xi + stringLen yi - 1 )
?concatStringAssoc xi yi zi
==. map (shift (stringLen xi)) (makeIndices (concatString yi zi) tg (stringLen yi - stringLen tg + 1) (stringLen yi - 1))
? shiftIndexesRight' (stringLen yi - stringLen tg + 1)
(stringLen yi - 1)
xi
(concatString yi zi)
tg
==. map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
(maxInt (stringLen yi - (stringLen tg -1)) 0)
(stringLen yi -1))
==. map (shift (stringLen xi))
(makeNewIndices yi zi tg)
*** QED
{-@ shiftIndexesRight'
:: lo:Nat
-> hi:Int
-> x:SMTString
-> input:SMTString
-> tg:SMTString
-> { map (shift (stringLen x)) (makeIndices input tg lo hi) == makeIndices (concatString x input) tg (stringLen x + lo) (stringLen x + hi) }
/ [if hi < lo then 0 else hi-lo]
@-}
shiftIndexesRight' :: Int -> Int -> SMTString -> SMTString -> SMTString -> Proof
shiftIndexesRight' lo hi x input target
| hi < lo
= map (shift (stringLen x)) (makeIndices input target lo hi)
==. map (shift (stringLen x)) N
==. N
==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
*** QED
| lo == hi, isGoodIndex input target lo
= map (shift (stringLen x)) (makeIndices input target lo hi)
==. map (shift (stringLen x)) (lo `C` N)
==. ((shift (stringLen x)) lo) `C` (map (shift (stringLen x)) N)
==. (stringLen x + lo) `C` N
==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
? isGoodIndexConcatFront input x target lo -- ( => IsGoodIndex (concatString x input) target (stringLen x + lo))
*** QED
| lo == hi
= map (shift (stringLen x)) (makeIndices input target lo hi)
==. map (shift (stringLen x)) N
==. N
==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
? (isGoodIndexConcatFront input x target lo *** QED)
*** QED
shiftIndexesRight' lo hi x input target
| isGoodIndex input target lo
= map (shift (stringLen x)) (makeIndices input target lo hi)
==. map (shift (stringLen x)) (lo `C`(makeIndices input target (lo+1) hi))
==. (shift (stringLen x) lo) `C` (map (shift (stringLen x)) (makeIndices input target (lo+1) hi))
==. (shift (stringLen x) lo) `C` (makeIndices (concatString x input) target (stringLen x + (lo+1)) (stringLen x + hi))
? shiftIndexesRight' (lo+1) hi x input target
==. (stringLen x + lo) `C` (makeIndices (concatString x input) target (stringLen x + (lo+1)) (stringLen x + hi))
==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
? (isGoodIndexConcatFront input x target lo *** QED)
*** QED
| otherwise
= map (shift (stringLen x)) (makeIndices input target lo hi)
==. map (shift (stringLen x)) (makeIndices input target (lo + 1) hi)
==. makeIndices (concatString x input) target (stringLen x + (lo+1)) (stringLen x + hi)
? shiftIndexesRight' (lo+1) hi x input target
==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
? (isGoodIndexConcatFront input x target lo *** QED)
*** QED
{-@ shiftNewIndexes
:: xi:SMTString
-> yi:SMTString
-> zi:SMTString
-> tg:{SMTString | stringLen yi < stringLen tg }
-> { append (makeNewIndices xi (concatString yi zi) tg) (map (shift (stringLen xi)) (makeNewIndices yi zi tg)) == append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
}
@-}
shiftNewIndexes :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
shiftNewIndexes xi yi zi tg
| stringLen tg < 2
= append (makeNewIndices xi (concatString yi zi) tg) (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. append N (map (shift (stringLen xi)) N)
==. map (shift (stringLen xi)) N
==. N
==. append N N
==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
*** QED
shiftNewIndexes xi yi zi tg
| stringLen xi == 0
= append (makeNewIndices xi (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. append (makeNewIndices stringEmp (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
? stringEmpProp xi
==. append (makeNewIndices stringEmp (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
? makeNewIndicesNullRight (concatString yi zi) tg
==. append N
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. map (shift (stringLen xi)) (makeNewIndices yi zi tg)
==. map (shift 0) (makeNewIndices yi zi tg)
? mapShiftZero (makeNewIndices yi zi tg)
==. makeNewIndices yi zi tg
==. makeNewIndices (concatString xi yi) zi tg
? concatEmpLeft xi yi
==. append N (makeNewIndices (concatString xi yi) zi tg)
==. append (makeNewIndices stringEmp yi tg) (makeNewIndices (concatString xi yi) zi tg)
? makeNewIndicesNullRight yi tg
==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
? stringEmpProp xi
*** QED
| stringLen yi == 0
= append (makeNewIndices xi (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. append (makeNewIndices xi zi tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
? concatEmpLeft yi zi
==. append (makeNewIndices xi zi tg)
(map (shift (stringLen xi)) (makeNewIndices stringEmp zi tg))
? stringEmpProp yi
==. append (makeNewIndices xi zi tg)
(map (shift (stringLen xi)) N)
? makeNewIndicesNullRight zi tg
==. append (makeNewIndices xi zi tg)
N
==. makeNewIndices xi zi tg
?appendEmp (makeNewIndices xi zi tg)
==. makeNewIndices (concatString xi yi) zi tg
? concatEmpRight xi yi
==. append N (makeNewIndices (concatString xi yi) zi tg)
==. append (makeNewIndices xi stringEmp tg) (makeNewIndices (concatString xi yi) zi tg)
? makeNewIndicesNullLeft xi tg
==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
? stringEmpProp yi
*** QED
| stringLen yi - stringLen tg == -1
= let minidx = maxInt (stringLen xi - stringLen tg + 1) 0 in
append (makeNewIndices xi (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
(maxInt (stringLen xi - stringLen tg + 1) 0)
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
(maxInt (stringLen yi - stringLen tg +1) 0)
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
(maxInt (stringLen xi - stringLen tg + 1) 0)
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
(maxInt 0 0)
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
(maxInt (stringLen xi - stringLen tg + 1) 0)
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
0
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
minidx
(stringLen xi -1))
(makeIndices (concatString xi (concatString yi zi)) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? shiftIndexesRight' 0 (stringLen yi -1) xi (concatString yi zi) tg
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi -1))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? concatStringAssoc xi yi zi
==. append (append
(makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi -1))
)
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? mergeIndixes (concatString (concatString xi yi) zi) tg
minidx -- maxInt (stringLen xi - stringLen tg + 1) 0
(stringLen xi -1)
(stringLen xi -1)
==. append (append
(makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
N
)
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
?appendEmp (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi -1))
(makeIndices (concatString (concatString xi yi) zi) tg
((stringLen xi))
(stringLen xi + stringLen yi -1))
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen (concatString xi yi) - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi - 1)
)
? catIndixes (concatString xi yi) zi tg minidx (stringLen xi-1)
==. append (makeIndices (concatString xi yi) tg
minidx
-- maxInt (stringLen xi - stringLen tg + 1) 0 && 2 <= stringLen tg
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi - 1)
)
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen xi) 0)
(stringLen xi + stringLen yi - 1)
)
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen xi + stringLen yi - stringLen tg + 1) 0)
(stringLen xi + stringLen yi - 1)
)
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
(stringLen (concatString xi yi) - 1)
)
==. append (makeIndices (concatString xi yi) tg
(maxInt (stringLen xi - stringLen tg +1) 0)
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
(stringLen (concatString xi yi) - 1)
)
==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
*** QED
shiftNewIndexes xi yi zi tg
-- THIS ALWAYS HOLDS
-- | stringLen yi + 1 <= stringLen tg
| 0 <= stringLen xi + stringLen yi - stringLen tg
-- , 0 < stringLen xi
= let minidx = maxInt (stringLen xi - stringLen tg + 1) 0 in
append (makeNewIndices xi (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
(maxInt (stringLen xi - stringLen tg + 1) 0)
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
(maxInt (stringLen yi - stringLen tg +1) 0)
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
minidx
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
0
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
minidx
(stringLen xi -1))
(makeIndices (concatString xi (concatString yi zi)) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? shiftIndexesRight' 0 (stringLen yi -1) xi (concatString yi zi) tg
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi -1))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? concatStringAssoc xi yi zi
==. append (append
(makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi + stringLen yi - stringLen tg + 1)
(stringLen xi -1))
)
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? mergeIndixes (concatString (concatString xi yi) zi) tg
minidx -- maxInt (stringLen xi - stringLen tg + 1) 0
(stringLen xi + stringLen yi - stringLen tg)
(stringLen xi -1)
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
(append
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi + stringLen yi - stringLen tg +1)
(stringLen xi -1))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1)) )
? appendAssoc
(makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi + stringLen yi - stringLen tg+1)
(stringLen xi -1))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen xi + stringLen yi - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
((stringLen xi + stringLen yi - stringLen tg+1))
(stringLen xi + stringLen yi -1))
? mergeIndixes (concatString (concatString xi yi) zi) tg
((stringLen xi + stringLen yi - stringLen tg+1))
(stringLen xi-1)
(stringLen xi + stringLen yi -1)
==. append (makeIndices (concatString (concatString xi yi) zi) tg
minidx
(stringLen (concatString xi yi) - stringLen tg))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi + stringLen yi - stringLen tg + 1)
(stringLen xi + stringLen yi -1))
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi + stringLen yi - stringLen tg + 1)
(stringLen xi + stringLen yi - 1)
)
? catIndixes (concatString xi yi) zi tg minidx (stringLen xi-1)
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen xi + stringLen yi - stringLen tg + 1) 0)
(stringLen xi + stringLen yi - 1)
)
==. append (makeIndices (concatString xi yi) tg
minidx
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
(stringLen (concatString xi yi) - 1)
)
==. append (makeIndices (concatString xi yi) tg
(maxInt (stringLen xi - stringLen tg +1) 0)
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
(stringLen (concatString xi yi) - 1)
)
==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
*** QED
-- | stringLen yi + 1 <= stringLen tg
| stringLen xi + stringLen yi < stringLen tg
= append (makeNewIndices xi (concatString yi zi) tg)
(map (shift (stringLen xi)) (makeNewIndices yi zi tg))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
(maxInt (stringLen xi - stringLen tg + 1) 0)
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
(maxInt (stringLen yi - stringLen tg +1) 0)
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
0
(stringLen xi -1))
(map (shift (stringLen xi))
(makeIndices (concatString yi zi) tg
0
(stringLen yi -1)
))
==. append (makeIndices (concatString xi (concatString yi zi)) tg
0
(stringLen xi -1))
(makeIndices (concatString xi (concatString yi zi)) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? shiftIndexesRight' 0 (stringLen yi -1) xi (concatString yi zi) tg
==. append (makeIndices (concatString (concatString xi yi) zi) tg
0
(stringLen xi -1))
(makeIndices (concatString (concatString xi yi) zi) tg
(stringLen xi)
(stringLen xi + stringLen yi -1))
? concatStringAssoc xi yi zi
==. makeIndices (concatString (concatString xi yi) zi) tg
0
(stringLen (concatString xi yi) - 1)
?mergeIndixes (concatString (concatString xi yi) zi) tg
0
(stringLen xi-1)
(stringLen (concatString xi yi) -1)
==. append N
(makeIndices (concatString (concatString xi yi) zi) tg
0
(stringLen (concatString xi yi) - 1)
)
==. append (makeIndices (concatString xi yi) tg
0
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
0
(stringLen (concatString xi yi) - 1)
)
? smallInput (concatString xi yi) tg 0 (stringLen xi -1)
==. append (makeIndices (concatString xi yi) tg
(maxInt (stringLen xi - stringLen tg +1) 0)
(stringLen xi-1)
)
(makeIndices (concatString (concatString xi yi) zi) tg
(maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
(stringLen (concatString xi yi) - 1)
)
==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
*** QED
-- NIKI CHECK: Feels have done this proof before
maxIndixes
:: SMTString -> SMTString -> Int -> Int -> Proof
{-@ maxIndixes
:: input:SMTString -> target:SMTString -> lo:{Nat | stringLen input < lo + stringLen target} -> hi:Int
-> {makeIndices input target lo hi = N}
/ [hi - lo ] @-}
maxIndixes input target lo hi
| hi < lo
= makeIndices input target lo hi
==. N
*** QED
| lo == hi, not (isGoodIndex input target lo)
= makeIndices input target lo hi
==. N
*** QED
| not (isGoodIndex input target lo)
= makeIndices input target lo hi
==. N
==. makeIndices input target (lo+1) hi
? maxIndixes input target (lo+1) hi
*** QED
mergeIndixes :: SMTString -> SMTString -> Int -> Int -> Int -> Proof
{-@ mergeIndixes
:: input:SMTString -> target:SMTString -> lo:Nat -> mid:{Int | lo <= mid} -> hi:{Int | mid <= hi}
-> {makeIndices input target lo hi == append (makeIndices input target lo mid) (makeIndices input target (mid+1) hi)}
/ [mid] @-}
mergeIndixes input target lo mid hi
| lo == mid, isGoodIndex input target lo
= append (makeIndices input target lo mid) (makeIndices input target (mid+1) hi)
==. append (makeIndices input target lo lo) (makeIndices input target (mid+1) hi)
==. append (lo `C` N) (makeIndices input target (mid+1) hi)
==. lo `C` (append N (makeIndices input target (lo+1) hi))
==. lo `C` (makeIndices input target (lo+1) hi)
==. makeIndices input target lo hi
*** QED
| lo == mid, not (isGoodIndex input target lo)
= append (makeIndices input target lo mid) (makeIndices input target (mid+1) hi)
==. append (makeIndices input target lo lo) (makeIndices input target (mid+1) hi)
==. append (lo `C` N) (makeIndices input target (mid+1) hi)
==. (append N (makeIndices input target (lo+1) hi))
==. makeIndices input target lo hi
*** QED
| lo < mid, not (isGoodIndex input target mid)
= makeIndices input target lo hi
==. append (makeIndices input target lo (mid-1))
(makeIndices input target mid hi)
? mergeIndixes input target lo (mid-1) hi
==. append (makeIndices input target lo (mid-1))
(makeIndices input target (mid+1) hi)
==. append (makeIndices input target lo mid)
(makeIndices input target (mid+1) hi)
?makeNewIndicesBadLast input target lo mid
*** QED
| lo < mid, isGoodIndex input target mid
= makeIndices input target lo hi
==. append (makeIndices input target lo (mid-1))
(makeIndices input target mid hi)
? mergeIndixes input target lo (mid-1) hi
==. append (makeIndices input target lo (mid-1))
(mid `C` makeIndices input target (mid+1) hi)
==. append (makeIndices input target lo (mid-1))
(mid `C` (append N (makeIndices input target (mid+1) hi)))
==. append (makeIndices input target lo (mid-1))
(append (C mid N) (makeIndices input target (mid+1) hi))
==. append (append (makeIndices input target lo (mid-1)) (C mid N))
(makeIndices input target (mid+1) hi)
? appendAssoc (makeIndices input target lo (mid-1)) (C mid N) (makeIndices input target (mid+1) hi)
==. append (makeIndices input target lo mid)
(makeIndices input target (mid+1) hi)
?makeNewIndicesGoodLast input target lo mid
*** QED
makeNewIndicesGoodLast, makeNewIndicesBadLast
:: SMTString -> SMTString -> Int -> Int -> Proof
{-@ makeNewIndicesGoodLast
:: input:SMTString -> target:SMTString -> lo:Nat -> hi:{Int | lo <= hi && (isGoodIndex input target hi)}
-> {makeIndices input target lo hi == append (makeIndices input target lo (hi-1)) (C hi N)}
/ [hi - lo] @-}
makeNewIndicesGoodLast input target lo hi
| lo == hi, (isGoodIndex input target lo)
= makeIndices input target lo hi
==. hi `C` N
==. append (N) (C hi N)
==. append (makeIndices input target lo (hi-1)) (C hi N)
*** QED
| not (isGoodIndex input target lo), isGoodIndex input target hi
= makeIndices input target lo hi
==. makeIndices input target (lo+1) hi
==. append (makeIndices input target (lo+1) (hi-1)) (C hi N)
? makeNewIndicesGoodLast input target (lo+1) hi
==. append (makeIndices input target lo (hi-1)) (C hi N)
*** QED
| isGoodIndex input target lo, isGoodIndex input target hi
= makeIndices input target lo hi
==. lo `C` makeIndices input target (lo+1) hi
==. lo `C` (append (makeIndices input target (lo+1) (hi-1)) (C hi N))
? makeNewIndicesGoodLast input target (lo+1) hi
==. (append (lo `C` makeIndices input target (lo+1) (hi-1)) (C hi N))
==. append (makeIndices input target lo (hi-1)) (C hi N)
*** QED
{-@ makeNewIndicesBadLast
:: input:SMTString -> target:SMTString -> lo:Nat -> hi:{Int | lo <= hi && (not (isGoodIndex input target hi))}
-> {makeIndices input target lo hi == makeIndices input target lo (hi-1)}
/ [hi - lo]
@-}
-- NV sweet proof
makeNewIndicesBadLast input target lo hi
| lo == hi, not (isGoodIndex input target lo)
= makeIndices input target lo (hi-1)
==. N
==. makeIndices input target lo hi
*** QED
| not (isGoodIndex input target lo), not (isGoodIndex input target hi)
= makeIndices input target lo hi
==. makeIndices input target (lo+1) hi
==. makeIndices input target (lo+1) (hi-1)
? makeNewIndicesBadLast input target (lo+1) hi
==. makeIndices input target lo (hi-1)
*** QED
| isGoodIndex input target lo , not (isGoodIndex input target hi)
= makeIndices input target lo hi
==. lo `C` makeIndices input target (lo+1) hi
==. lo `C` makeIndices input target (lo+1) (hi-1)
? makeNewIndicesBadLast input target (lo+1) hi
==. makeIndices input target lo (hi-1)
*** QED
catIndixes :: SMTString -> SMTString -> SMTString -> Int -> Int -> Proof
{-@ catIndixes
:: input:SMTString -> x:SMTString
-> target:{SMTString | 0 <= stringLen input - stringLen target + 1}
-> lo:{Nat | lo <= stringLen input - stringLen target }
-> hi:{Int | stringLen input - stringLen target <= hi}
-> { makeIndices input target lo hi == makeIndices (concatString input x) target lo (stringLen input - stringLen target) }
@-}
catIndixes input x target lo hi
= makeIndices input target lo hi
==. append (makeIndices input target lo (stringLen input - stringLen target))
(makeIndices input target (stringLen input - stringLen target + 1) hi)
? mergeIndixes input target lo (stringLen input - stringLen target) hi
==. append (makeIndices input target lo (stringLen input - stringLen target))
N
? maxIndixes input target (stringLen input - stringLen target + 1) hi
==. makeIndices input target lo (stringLen input - stringLen target)
? appendEmp (makeIndices input target lo (stringLen input - stringLen target))
==. makeIndices (concatString input x) target lo (stringLen input - stringLen target)
? concatmakeNewIndices lo (stringLen input - stringLen target) target input x
*** QED
map_len_fusion :: SMTString -> SMTString -> List Int -> Proof
{-@ map_len_fusion
:: xi:SMTString
-> yi:SMTString
-> zis:List Int
-> { map (shift (stringLen (concatString xi yi))) zis == map (shift (stringLen xi)) (map (shift (stringLen yi)) zis)
}
@-}
map_len_fusion xi yi N
= map (shift (stringLen (concatString xi yi))) N
==. N
==. map (shift (stringLen xi)) N
==. map (shift (stringLen xi)) (map (shift (stringLen yi)) N)
*** QED
map_len_fusion xi yi (C i is)
= map (shift (stringLen (concatString xi yi))) (C i is)
==. shift (stringLen (concatString xi yi)) i `C` map (shift (stringLen (concatString xi yi))) is
==. shift (stringLen xi + stringLen yi) i `C` map (shift (stringLen (concatString xi yi))) is
? concatLen xi yi
==. shift (stringLen xi) (shift (stringLen yi) i) `C` map (shift (stringLen (concatString xi yi))) is
? concatLen xi yi
==. shift (stringLen xi) (shift (stringLen yi) i) `C` map (shift (stringLen xi)) (map (shift (stringLen yi)) is)
? map_len_fusion xi yi is
==. map (shift (stringLen xi)) (shift (stringLen yi) i `C` map (shift (stringLen yi)) is)
==. map (shift (stringLen xi)) (map (shift (stringLen yi)) (i `C` is))
*** QED
smallInput :: SMTString -> SMTString -> Int -> Int -> Proof
{-@ smallInput :: input:SMTString -> target:{SMTString | stringLen input < stringLen target } -> lo:Nat -> hi:Int
-> {makeIndices input target lo hi == N }
/ [hi -lo]
@-}
smallInput input target lo hi
| hi < lo
= makeIndices input target lo hi
==. N
*** QED
| lo == hi, not (isGoodIndex input target lo)
= makeIndices input target lo hi
==. N
*** QED
| not (isGoodIndex input target lo)
= makeIndices input target lo hi
==. makeIndices input target (lo+1) hi
==. N ? smallInput input target (lo+1) hi
*** QED
-------------------------------------------------------------------------------
---------- Indexing ----------------------------------------------------------
-------------------------------------------------------------------------------
data List a = N | C a (List a) deriving (Show, Eq)
{-@ data List [idxlen] a = N | C {idxhd :: a , idxtl :: List a} @-}
{-@ measure idxlen @-}
{-@ idxlen :: List a -> Nat @-}
idxlen :: List a -> Int
idxlen N = 0
idxlen (C _ xs) = 1 + idxlen xs
{-@ reflect map @-}
map :: (a -> b) -> List a -> List b
map _ N = N
map f (C x xs) = C (f x) (map f xs)
{-@ reflect append @-}
append :: List a -> List a -> List a
append N xs = xs
append (C x xs) ys = C x (append xs ys)
{-@ reflect shift @-}
shift :: Int -> Int -> Int
shift x y = x + y
{-@ symbolVal :: forall n proxy. KnownSymbol n => x:proxy n
-> {v:String | v == n && v == symbolVal x } @-}
{-@ measure symbolVal :: p n -> String @-}
{-@ reflect makeNewIndices @-}
{-@ makeNewIndices :: s1:SMTString -> s2:SMTString -> target:SMTString -> List (GoodIndex {concatString s1 s2} target) @-}
makeNewIndices :: SMTString -> SMTString -> SMTString -> List Int
makeNewIndices s1 s2 target
| stringLen target < 2
= N
| otherwise
= makeIndices (concatString s1 s2) target
(maxInt (stringLen s1 - (stringLen target-1)) 0)
(stringLen s1 - 1)
{-@ reflect maxInt @-}
maxInt :: Int -> Int -> Int
maxInt x y = if x <= y then y else x
{-@ reflect makeIndices @-}
makeIndices :: SMTString -> SMTString -> Int -> Int -> List Int
{-@ makeIndices :: input:SMTString -> target:SMTString -> lo:{Int | 0 <= lo} -> hi:Int -> List (GoodIndex input target)
/ [hi - lo] @-}
makeIndices input target lo hi
| hi < lo
= N
| lo == hi, isGoodIndex input target lo
= lo `C` N
| lo == hi
= N
makeIndices input target lo hi
| isGoodIndex input target lo
= lo `C` (makeIndices input target (lo + 1) hi)
| otherwise
= makeIndices input target (lo + 1) hi
{-@ reflect isGoodIndex @-}
isGoodIndex :: SMTString -> SMTString -> Int -> Bool
{-@ isGoodIndex :: input:SMTString -> target:SMTString -> i:Int
-> {b:Bool | Prop b <=> IsGoodIndex input target i} @-}
isGoodIndex input target i
= subString input i (stringLen target) == target
&& i + stringLen target <= stringLen input
&& 0 <= i
-------------------------------------------------------------------------------
---------- Indexing Properties -----------------------------------------------
-------------------------------------------------------------------------------
{-@ appendEmp :: xs:List a -> {append xs N = xs } @-}
appendEmp :: List a -> Proof
appendEmp N
= append N N
==. N
*** QED
appendEmp (C x xs)
= append (C x xs) N
==. C x (append xs N)
==. C x xs ? appendEmp xs
*** QED
{-@ appendAssoc :: x:List a -> y:List a -> z:List a
-> {(append x (append y z)) == (append (append x y) z) } @-}
appendAssoc :: List a -> List a -> List a -> Proof
appendAssoc N y z
= append N (append y z)
==. append y z
==. append (append N y) z
*** QED
appendAssoc (C x xs) y z
= append (C x xs) (append y z)
==. C x (append xs (append y z))
==. C x (append (append xs y) z)
? appendAssoc xs y z
==. append (C x (append xs y)) z
==. append (append (C x xs) y) z
*** QED
makeNewIndicesNullRight :: SMTString -> SMTString -> Proof
{-@ makeNewIndicesNullRight
:: s1:SMTString
-> t:SMTString
-> {makeNewIndices stringEmp s1 t == N } @-}
makeNewIndicesNullRight s t
| stringLen t < 2
= makeNewIndices stringEmp s t ==. N *** QED
makeNewIndicesNullRight s t
= makeNewIndices stringEmp s t
==. makeIndices (concatString stringEmp s) t
(maxInt (1 + stringLen stringEmp - stringLen t) 0)
(stringLen stringEmp - 1)
==. makeIndices s t
(maxInt (1 - stringLen t) 0)
(-1)
? concatStringNeutralRight s
==. makeIndices s t 0 (-1)
==. N ? makeNewIndicesNullRightEmp s t
*** QED
-- (x1 ~ x2) ~ (x3 ~ x4)
-- ==
-- ((x1 ~ (x2 ~ x3)) ~ x4)
appendGroupNew :: List a -> List a -> List a -> List a -> Proof
{-@ appendGroupNew
:: x1:List a
-> x2:List a
-> x3:List a
-> x4:List a
-> { (append (append x1 x2) (append x3 x4))
== (append (append x1 (append x2 x3)) x4)
} @-}
appendGroupNew x1 x2 x3 x4
= (append (append x1 x2) (append x3 x4))
==. (append (append (append x1 x2) x3) x4)
? appendAssoc (append x1 x2) x3 x4
==. (append (append x1 (append x2 x3)) x4)
? appendAssoc x1 x2 x3
*** QED
-- (x1 ~ (x2 ~ x3)) ~ x4 == ((x1 ~ x2) ~ x3) ~ x4
appendUnGroupNew :: List a -> List a -> List a -> List a -> Proof
{-@ appendUnGroupNew
:: x1:List a
-> x2:List a
-> x3:List a
-> x4:List a
-> { ((append (append (append x1 x2) x3) x4))
== (append (append x1 (append x2 x3)) x4)
} @-}
appendUnGroupNew x1 x2 x3 x4
= append (append (append x1 x2) x3) x4
==. append (append x1 (append x2 x3)) x4
? appendAssoc x1 x2 x3
*** QED
appendReorder :: List a -> List a -> List a -> List a -> List a -> Proof
{-@ appendReorder
:: x1:List a
-> x2:List a
-> x3:List a
-> x4:List a
-> x5:List a
-> { (append (append x1 x2) (append (append x3 x4) x5))
== (append (append (append (append x1 x2) x3) x4) x5)
} @-}
appendReorder x1 x2 x3 x4 x5
= append (append x1 x2) (append (append x3 x4) x5)
==. append (append x1 x2) (append x3 (append x4 x5))
? appendAssoc x3 x4 x5
==. append (append (append x1 x2) x3) (append x4 x5)
? appendAssoc (append x1 x2) x3 (append x4 x5)
==. append ((append (append (append x1 x2) x3)) x4) x5
? appendAssoc (append (append x1 x2) x3) x4 x5
*** QED
-- ((x1~x2) ~ ((x3~x4) ~ x5))
-- ==
-- ((((x1~x2) ~x3) ~x4) ~x5
map_append :: (a -> b) -> List a -> List a -> Proof
{-@ map_append
:: f:(a -> b) -> xs:List a -> ys:List a
-> {map f (append xs ys) == append (map f xs) (map f ys)}
@-}
map_append f N ys
= map f (append N ys)
==. map f ys
==. append N (map f ys)
==. append (map f N) (map f ys)
*** QED
map_append f (C x xs) ys
= map f (append (C x xs) ys)
==. map f (x `C` (append xs ys))
==. f x `C` (map f (append xs ys))
==. f x `C` (append (map f xs) (map f ys))
? map_append f xs ys
==. append (f x `C` map f xs) (map f ys)
==. append (map f (x `C` xs)) (map f ys)
*** QED
mapShiftZero :: List Int -> Proof
{-@ mapShiftZero :: is:List Int -> {map (shift 0) is == is } @-}
mapShiftZero N
= map (shift 0) N ==. N *** QED
mapShiftZero (C i is)
= map (shift 0) (C i is)
==. shift 0 i `C` map (shift 0) is
==. i `C` is ? mapShiftZero is
*** QED
{-@ makeNewIndicesNullRightEmp :: s:SMTString -> t:SMTString -> {makeIndices s t 0 (-1) == N } @-}
makeNewIndicesNullRightEmp :: SMTString -> SMTString -> Proof
makeNewIndicesNullRightEmp s t
= makeIndices s t 0 (-1)
==. N
*** QED
makeNewIndicesNullLeft :: SMTString -> SMTString -> Proof
{-@ makeNewIndicesNullLeft
:: s:SMTString
-> t:SMTString
-> {makeNewIndices s stringEmp t == N } @-}
makeNewIndicesNullLeft s t
| stringLen t < 2
= makeNewIndices s stringEmp t ==. N *** QED
makeNewIndicesNullLeft s t
| 1 + stringLen s <= stringLen t
= makeNewIndices s stringEmp t
==. makeIndices (concatString s stringEmp) t
(maxInt (1 + stringLen s - stringLen t) 0)
(stringLen s - 1)
==. makeIndices s t
0
(stringLen s - 1)
? concatStringNeutral s
==. makeIndices s t
0
(stringLen s - 1)
==. N ? makeNewIndicesNull1 s t 0 (stringLen s - 1)
*** QED
makeNewIndicesNullLeft s t
= makeNewIndices s stringEmp t
==. makeIndices (concatString s stringEmp) t
(maxInt (1 + stringLen s - stringLen t) 0)
(stringLen s - 1)
==. makeIndices (concatString s stringEmp) t
(1 + stringLen s - stringLen t)
(stringLen s - 1)
==. makeIndices s t
(1 + stringLen s - stringLen t)
(stringLen s - 1) ? concatStringNeutral s
==. N ? makeNewIndicesNull2 s t (1 + stringLen s - stringLen t) (stringLen s - 1)
*** QED
makeNewIndicesNull1 :: SMTString -> SMTString -> Int -> Int -> Proof
{-@ makeNewIndicesNull1
:: s:SMTString
-> t:{SMTString | 1 + stringLen s <= stringLen t }
-> lo:Nat
-> hi:Int
-> {makeIndices s t lo hi == N } / [hi - lo] @-}
makeNewIndicesNull1 s1 t lo hi
| hi < lo
= makeIndices s1 t lo hi ==. N *** QED
| lo == hi, not (isGoodIndex s1 t lo)
= makeIndices s1 t lo hi ==. N *** QED
| not (isGoodIndex s1 t lo)
= makeIndices s1 t lo hi
==. makeIndices s1 t (lo + 1) hi
==. N ? makeNewIndicesNull1 s1 t (lo+1) hi
*** QED
makeNewIndicesNull2 :: SMTString -> SMTString -> Int -> Int -> Proof
{-@ makeNewIndicesNull2
:: s:SMTString
-> t:{SMTString | stringLen t < 2 + stringLen s }
-> lo:{Int | -1 <= lo && 1 + stringLen s - stringLen t <= lo }
-> hi:{Int | lo <= hi}
-> {makeIndices s t lo hi == N } / [hi - lo] @-}
makeNewIndicesNull2 s1 t lo hi
| lo == hi, not (isGoodIndex s1 t lo)
= makeIndices s1 t lo hi ==. N *** QED
| not (isGoodIndex s1 t lo)
= makeIndices s1 t lo hi
==. makeIndices s1 t (lo + 1) hi
==. N ? makeNewIndicesNull2 s1 t (lo+1) hi
*** QED