Main.hs 9.04 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
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
-}