module Main where
main :: IO ()
main = print (idList [1, 2])
sameLength xs ys = case xs of
[] -> case ys of [] -> True
(_:_) -> False
(_:as) -> case ys of [] -> False
(_:bs) -> sameLength as bs
-- idList : xs -> {rs | sameLength xs rs}
idList_rec idList xs = case xs of
[] -> []
y:ys -> y:idList ys
-- Programatically generated version:
-- idList_check idList xs
-- = let rs = idList_rec idList_ok xs
-- in case sameLength xs rs of True -> rs
-- where idList_ok xs = if sameLength xs rs then rs else error "UNR"
-- where rs = idList xs
-- An example with less work sharing but exactly the same issues:
{-# SUPERCOMPILE idList_check #-}
idList_check idList xs
= case sameLength xs (idList_rec idList_ok xs) of True -> idList_rec idList_ok xs
where idList_ok xs = if sameLength xs (idList xs) then idList xs else error "UNR"
{-# SUPERCOMPILE idList #-}
idList = root idList
{-
-- Here is why this doesn't work. First, the above program in g-function form:
sameLength xs ys = case xs of
[] -> case ys of [] -> True
(_:_) -> False
(_:as) -> case ys of [] -> False
(_:bs) -> sameLength as bs
sameLength [] ys = sameLengthNil ys
sameLength (_:as) ys = sameLengthCons as ys
sameLengthNil [] = True
sameLengthNil (_:_) = False
sameLengthCons as [] = False
sameLengthCons as (_:bs) = sameLength as bs
idList_rec idList [] = []
idList_rec idList (y:ys) = y:idList ys
idList_ok idList xs = let rs_ok = idList xs in if sameLength xs rs_ok then rs_ok else error "UNR"
idList_check idList xs
= let rs_rec = idList_rec (idList_ok idList) xs
in case sameLength xs rs_rec of True -> rs_rec
-- Now the drive sequence:
h0 idList xs = let rs_rec = idList_rec (idList_ok idList) xs
in case sameLength xs rs_rec of True -> rs_rec
=> case xs of
[] -> h1 idList = let rs_rec = idList_rec (idList_ok idList) []
in case sameLength [] rs_rec of True -> rs_rec
=> []
(a:as) -> h2 idList a as = let rs_rec = idList_rec (idList_ok idList) (a:as)
in case sameLength (a:as) rs_rec of True -> rs_rec
=> let rs_rec = a : idList_ok idList as
in case sameLengthCons as rs_rec of True -> rs_rec
=> let rs_rec1 = idList_ok idList as
in case sameLength as rs_rec1 of True -> a:rs_rec1
=> case as of
[] -> h3 idList a = let rs_rec1 = idList_ok idList []
in case sameLength [] rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok = idList [] in if sameLength [] rs_ok then rs_ok else error "UNR"
in case sameLengthNil rs_rec1 of True -> a:rs_rec1
=> a:[]
(a1:as1) -> h4 idList a a1 as1 = let rs_rec1 = idList_ok idList (a1:as1)
in case sameLength (a1:as1) rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then rs_ok else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok2 = idList as1 in if sameLength as1 rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
=> case as1 of
[] -> h5 idList a a1 = let rs_rec1 = let rs_ok2 = idList [] in if sameLength [] rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons [] rs_rec1 of True -> a:rs_rec1
=> a:a1:[]
(a2:as2) -> h6 idList a a1 a2 as2 = let rs_rec1 = let rs_ok2 = idList (a2:as2) in if sameLength (a2:as2) rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons (a2:as2) rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok3 = idList as2 in if sameLength as2 rs_ok3 then (a1:a2:rs_ok3) else error "UNR"
in case sameLengthCons (a2:as2) rs_rec1 of True -> a:rs_rec1
=> case as2 of
[] -> h7 idList a a1 a2 = ...
(a3:as3) -> h8 idList a a1 a2 a3 as3 = let rs_rec1 = let rs_ok3 = idList (a3:as3) in if sameLength (a3:as3) rs_ok3 then (a1:a2:rs_ok3) else error "UNR"
in case sameLengthCons (a2:a3:as3) rs_rec1 of True -> a:rs_rec1
-- Interesting stuff. You can see that we don't get tieback due to growing things:
-- Zeroeth time around (ish, this is a bit of a lie as the zeroeth time we haven't unfolded idList_ok yet):
let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then rs_ok else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
-- First time around:
let rs_rec1 = let rs_ok2 = idList (a2:as2) in if sameLength (a2:as2) rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons (a2:as2) rs_rec1 of True -> a:rs_rec1
-- Second time around:
let rs_rec1 = let rs_ok3 = idList (a3:as3) in if sameLength (a3:as3) rs_ok3 then (a1:a2:rs_ok3) else error "UNR"
in case sameLengthCons (a2:a3:as3) rs_rec1 of True -> a:rs_rec1
-- The same thing, without let:
-- Zeroeth time around (ish, this is a bit of a lie as the zeroeth time we haven't unfolded idList_ok yet):
case sameLengthCons as1 (if sameLength (a1:as1) (idList (a1:as1)) then idList (a1:as1) else error "UNR") of
True -> a:if sameLength (a1:as1) (idList (a1:as1)) then idList (a1:as1) else error "UNR"
-- First time around:
case sameLengthCons (a2:as2) (if sameLength (a2:as2) (idList (a2:as2)) then (a1:idList (a2:as2)) else error "UNR") of
True -> a:if sameLength (a2:as2) (idList (a2:as2)) then (a1:idList (a2:as2)) else error "UNR"
-- Second time around:
case sameLengthCons (a2:a3:as3) (if sameLength (a3:as3) (idList (a3:as3)) then (a1:a2:idList (a3:as3)) else error "UNR") of
True -> a:if sameLength (a3:as3) (idList (a3:as3)) then (a1:a2:idList (a3:as3)) else error "UNR"
-- Voightlander story:
let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then rs_ok else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
-- 1) Generalise:
gen1 = rs_ok
gen2 = as1
let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then gen1 else error "UNR"
in case sameLengthCons gen2 rs_rec1 of True -> a:rs_rec1
-- 2) Evaluate:
let rs_rec1 = let rs_ok1 = idList as1 in if sameLength as1 rs_ok1 then a1:gen1 else error "UNR"
in case sameLengthCons gen2 rs_rec1 of True -> a:rs_rec1
-- 3) We are stuck, so case split on as1:
-- 3a) Evaluate nil case normally
=> case sameLengthCons gen2 (a1:gen1) of True -> a:a1:gen1
=> case sameLength gen2 gen1 of True -> a:a1:gen1
-- 3ai) Generate gen2 based float
case sameLength <_> gen1 of True -> a:a1:gen1
-- 3b) Generalise the cons case
gen1' = a1:gen1
let rs_rec1 = let rs_ok1 = idList (a2:as2) in if sameLength (a2:as2) rs_ok1 then gen1' else error "UNR"
in case sameLengthCons gen2 rs_rec1 of True -> a:rs_rec1
-- 3bi) Tie back to the generalised verson, with:
gen2 = gen2
gen1 = gen1'
a1 = a2
as1 = as2
-- 3bii) Expand float:
case sameLength gen2 (a1:gen1) of True -> a:a2:gen1'
??? seems wrong
-}