Ticket #2296: Proof_default.hs

{-# LANGUAGE NoMonomorphismRestriction, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, UndecidableInstances, Rank2Types, EmptyDataDecls, FunctionalDependencies #-}
{-# OPTIONS_GHC -fno-warn-missing-methods -fno-warn-overlapping-patterns #-}

module Proof_default where
import Prelude hiding (($),(/))
import Data.List
{- # LINE 212 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["eval"]
-- !typesigFunction []
-- !implementsFunction ["eval","|"]

eval (Call f xs)  | f == "error" = Bottom
                   | otherwise = eval $ body f / (args f, xs)


{- # LINE 188 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["eval"]
 -- !typesigFunction []
 -- !implementsFunction ["eval"]

e''1 (Make c xs) = Val c (map e''1 xs)


{- # LINE 112 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["isBottom","valCtor","propTaut","satE'","satE","satV'","satV","sat"]
-- !typesigFunction ["isBottom","valCtor","propTaut","satE'","satE","satV'","satV","sat"]
-- !implementsFunction ["isBottom","valCtor","propTaut","satE'","satE","satV'","satV"]

isBottom :: Val -> Bool
isBottom Bottom = True
isBottom (Val c xs) = any isBottom xs

valCtor :: Val -> Maybe CtorName
valCtor (Val c xs) = Just c
valCtor Bottom = Nothing

propTaut :: (alpha -> Bool) -> Prop alpha -> Bool
propTaut f x = (propTrue :: Prop ()) == propMap (propBool . f) x

satE' :: Prop (Sat Expr) -> Bool
satE' = propTaut satE

satE :: Sat Expr -> Bool
satE (Sat x k) = sat (eval x) k

satV' :: Prop (Sat Val) -> Bool
satV' = propTaut satV

satV :: Sat Val -> Bool
satV (Sat v k) = sat v k

sat :: Val -> Constraint -> Bool

sat = undefined -- stub

{- # LINE 84 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["eval","uneval"]
 -- !typesigFunction ["eval","uneval"]
 -- !implementsFunction ["data","|","eval","Val","->","uneval"]

data Val  =  Val CtorName [Val]
          |  Bottom

data Expr  =  Make CtorName [Expr]
           |  Call FuncName [Expr]
           |  Var  VarName
           |  Case Expr [Alt]

data Alt = Alt CtorName [VarName] Expr

e''3 :: Expr -> Val
e''3 (Make c xs   ) = Val c (map e''3 xs)
e''3 (Call f xs)  | f == "error" = Bottom
                  | otherwise = e''3 $ body f / (args f, xs)
e''3 (Case x as   ) = case e''3 x of
    Val c xs -> e''3 $ head [y / (vs, map uneval xs) | Alt c' vs y <- as, c == c']
    Bottom -> Bottom

uneval :: Val -> Expr
uneval (Val c xs)  = Make c (map uneval xs)
uneval Bottom      = Call "error" []


{- # LINE 9 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["infixr","freeVars","body","args","var","ctors","precond","prePost","pre","reduce","red","substP","-<","|>","<|","propAnd","propAnds","propMap","propTrue","propBool","propLit","propOr","propOrs","propFalse"]
-- !typesigFunction ["$","freeVars","body","args","var","ctors","precond","prePost","pre","reduce","red","substP","-<","|>","<|","propOr","propAnd","propOrs","propAnds","propMap","propFalse","propTrue","propBool","propLit"]
-- !implementsFunction ["import","infixr","class","instance","type","data"]

-- HIDE import Prelude hiding (($),(/))
-- HIDE import Data.List

infixr 1  $
infixr 0  ==>
class Implies a where (==>) :: a -> a -> Bool
($) :: (a -> b) -> a -> b

instance Implies Bool
instance Implies (Prop a)

type FuncName = String
type CtorName = String
type VarName = String

freeVars :: Expr -> [String]
body   :: FuncName  -> Expr
args   :: FuncName  -> [VarName]
var    :: VarName   -> Maybe (Expr, Selector)
ctors  :: CtorName  -> [CtorName]
type Selector  =  (CtorName, Int)

precond   :: FuncName -> Prop (Sat VarName)
prePost   :: FuncName -> Constraint -> Prop (Sat VarName)
pre ::  Expr -> Prop (Sat Expr)
reduce    :: Prop (Sat Expr) -> Prop (Sat VarName)
red :: Expr -> Constraint -> Prop (Sat VarName)
substP :: Eq alpha => [(alpha,beta)] -> Prop (Sat alpha) -> Prop (Sat beta)

data Sat alpha = Sat alpha Constraint
instance Eq a => Eq (Sat a)

(-<)  :: alpha -> [CtorName] -> Prop (Sat alpha)
(|>)  :: Selector -> Constraint -> Constraint
(<|)  :: CtorName -> Constraint -> Prop (Sat Int)

data Prop alpha
instance Eq a => Eq (Prop a)

propAnd, propOr           :: Prop alpha -> Prop alpha -> Prop alpha
propAnds, propOrs         :: [Prop alpha] -> Prop alpha
propMap                   :: (alpha -> Prop beta) -> Prop alpha -> Prop beta
propTrue, propFalse       :: Prop alpha
propBool                  :: Bool -> Prop alpha
propLit                   :: alpha -> Prop alpha

data Constraint = Constraint

class Subst a b c | c -> b, c -> a, a -> b where (/) :: a -> b -> c
instance Subst Expr ([VarName], [Expr]) Expr
instance Subst a b c => Subst (Prop a) b (Prop c)
instance (Eq a, Eq b) => Subst (Sat a) ([a], [b]) (Sat b)

instance Eq Val
instance Eq Expr

($) = undefined -- stub
freeVars = undefined -- stub
body = undefined -- stub
args = undefined -- stub
var = undefined -- stub
ctors = undefined -- stub
precond = undefined -- stub
prePost = undefined -- stub
pre = undefined -- stub
reduce = undefined -- stub
red = undefined -- stub
substP = undefined -- stub
(-<) = undefined -- stub
(|>) = undefined -- stub
(<|) = undefined -- stub
propOr = undefined -- stub
propAnd = undefined -- stub
propOrs = undefined -- stub
propAnds = undefined -- stub
propMap = undefined -- stub
propFalse = undefined -- stub
propTrue = undefined -- stub
propBool = undefined -- stub
propLit = undefined -- stub

{- # LINE 76 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_1"]
auto_1 = error
 where

{- # LINE 108 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_7"]
auto_7 = x / (vs,ys)
 where
 x = undefined
 vs = undefined
 ys = undefined

{- # LINE 146 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_16"]
auto_16 = satE' $ pre x ==> not $ isBottom $ eval x
 where
 x = undefined

{- # LINE 151 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_17"]
auto_17 = satV' $ x -< cs ==> maybe True (`elem` cs) (valCtor x)
 where
 x = undefined
 cs = undefined

{- # LINE 154 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_19"]
auto_19 = sat (Val c xs) ((c,i) |> k) ==> sat (xs !! i) k
 where
 k = undefined
 c = undefined
 i = undefined
 xs = undefined

{- # LINE 157 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_21"]
auto_21 = satV' $ (c <| k) / ([1..],xs) ==> sat (Val c xs) k
 where
 k = undefined
 c = undefined
 xs = undefined

{- # LINE 162 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_22"]
auto_22 = precond "error" == propFalse
 where

{- # LINE 165 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_23"]
auto_23 = precond f ==> reduce $ pre $ body f
 where
 f = undefined

{- # LINE 168 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_24"]
auto_24 = satE' $ reduce x / (vs,xs) ==> satE' $ x / (vs, xs)
 where
 x = undefined
 vs = undefined
 xs = undefined

{- # LINE 174 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_25"]
auto_25 = not $ isBottom x ==> satE' $ pre $ uneval x
 where
 x = undefined

{- # LINE 194 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_29"]
auto_29 = satE' $ pre $ Make c xs  ==> all (satE' . pre) xs
    -- inline |pre|
 where
 c = undefined
 xs = undefined

{- # LINE 194 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_30"]
auto_30 = satE' $ propAnds $ map pre xs ==> all (satE' . pre) xs
    -- inline |satE'|
 where
 xs = undefined

{- # LINE 194 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_31"]
auto_31 = and $ map satE' $ map pre xs  ==> all (satE' . pre) xs
    -- |map f . map g == map (f . g)|
 where
 xs = undefined

{- # LINE 194 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_32"]
auto_32 = and $ map (satE' . pre) xs ==> all (satE' . pre) xs
    -- |and . map f == all f|
 where
 xs = undefined

{- # LINE 194 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_33"]
auto_33 = all (satE' . pre) xs ==> all (satE' . pre) xs
    -- equal
 where
 xs = undefined

{- # LINE 219 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_36"]
auto_36 = satE' $ pre $ Call f xs ==> f /= "error"
    -- inline |pre|
 where
 f = undefined
 xs = undefined

{- # LINE 219 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_37"]
auto_37 = satE' $ (precond f / (args f, xs)) `propAnd` propAnds (map pre xs) ==> f /= "error"
    -- inline |satE'|
 where
 f = undefined
 xs = undefined

{- # LINE 219 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_38"]
auto_38 = satE' (precond f / (args f, xs)) && all (satE' . pre) xs ==> f /= "error"
    -- weaken implication
 where
 f = undefined
 xs = undefined

{- # LINE 219 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_39"]
auto_39 = satE' (precond f / (args f, xs)) ==> f /= "error"
 where
 f = undefined
 xs = undefined

{- # LINE 231 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_42"]
auto_42 = satE' (precond f / (args f, xs)) ==> f /= "error"
    -- assume |f /= "error"|
 where
 f = undefined
 xs = undefined

{- # LINE 231 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_43"]
auto_43 = satE' (precond f / (args f, xs)) ==> True
    -- implication
 where
 f = undefined
 xs = undefined

{- # LINE 239 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_44"]
auto_44 = satE' (precond f / (args f, xs)) ==> f /= "error"
    -- assume |f == "error"|
 where
 f = undefined
 xs = undefined

{- # LINE 239 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_45"]
auto_45 = satE' (precond f / (args f, xs)) ==> False
    -- implication
 where
 f = undefined
 xs = undefined

{- # LINE 239 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_46"]
auto_46 = not $ satE' (precond "error" / (args f, xs))
    -- \lemma{precond/error}
 where
 f = undefined
 xs = undefined

{- # LINE 239 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_47"]
auto_47 = not $ satE' $ (propFalse / (args f, xs))
    -- inline |(/)|
 where
 f = undefined
 xs = undefined

{- # LINE 239 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_48"]
auto_48 = not $ satE' propFalse
    -- inline |satE'|
 where

{- # LINE 239 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_49"]
auto_49 = not $ False
    -- inline |not|
 where

{- # LINE 257 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_50"]
auto_50 = satE' $ pre $ Call f xs ==> satE' $ pre $ body f / (args f, xs)
    -- inline pre on LHS
 where
 f = undefined
 xs = undefined

{- # LINE 257 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_51"]
auto_51 = satE' $ (precond f / (args f, xs)) `propAnd` propAnds (map pre xs) ==> satE' $ pre $ body f / (args f, xs)
    -- inline |satE'|
 where
 f = undefined
 xs = undefined

{- # LINE 257 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_52"]
auto_52 = satE' (precond f / (args f, xs)) && all (satE' . pre) xs ==> satE' $ pre $ body f / (args f, xs)
    -- \lemma{precond}
 where
 f = undefined
 xs = undefined

{- # LINE 257 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_53"]
auto_53 = satE' ((reduce $ pre $ body f) / (args f, xs)) && all (satE' . pre) xs ==> satE' $ pre $ body f / (args f, xs)
    -- \lemma{reduce}
 where
 f = undefined
 xs = undefined

{- # LINE 257 "E:\\Neil\\thesis\\proof.tex" # -}
-- !defines ["auto_54"]
auto_54 = satE' (pre (body f) / (args f / xs)) && all (satE' . pre) xs ==> satE' $ pre $ body f / (args f, xs)
    -- \lemma{pre/subst}
 where
 f = undefined
 xs = undefined