module Why.Conversion where

import qualified Why.Syntax as W
import qualified Why.SyntaxFlattened as WF
{-
import Data.Generics

class F a where
  flatten :: a -> WF.WhyF

instance F W.Term where
  flatten (W.Const a) = WF.Const (flatten a)
  flatten (W.Sum a b) = WF.Sum (flatten a) (flatten b)

instance F W.Constant where
  flatten = undefined

-- TODO: continue...


class UF a where
  unflatten :: WF.WhyF -> a

instance UF W.Term where
  unflatten (WF.Const a) = W.Const (unflatten a)
  unflatten (WF.Sum a b) = W.Sum (unflatten a) (unflatten b)

instance UF W.Constant where
  unflatten = undefined

-- TODO: continue... or think about using Data.Generics

-}


flatten :: Show a => a -> WF.WhyF
flatten = read . show

unflatten :: WF.Why -> W.Why
unflatten = read . show

unflattenD :: WF.Why -> [(W.Why,String)]
unflattenD = reads . show

{-
data Term =
    Const Constant
  | Sum Term Term
  | Sub Term Term
  | Mult Term Term
  | Div Term Term
  | Rem Term Term
  | TNegation Term
  | TVar LabIdentifier
  | TFunction Identifier Terms -- one or more Term
--  | X LabIdentifier (Maybe Term) -- what is this?
  | TIfThenElse Term Term Term

data Constant =
    IntConst Int
  | RealConst Float
  | BoolConst Bool
  | Void

data Predicate = 
    PredTrue
  | PredFalse
  | PVar Identifier
  | PFunction Identifier Terms -- one or more Term
  | Equal Predicate Predicate
  | Diff Predicate Predicate
  | Lesser Predicate Predicate
  | LessEq Predicate Predicate
  | Greater Predicate Predicate
  | GreatEq Predicate Predicate
  | PNegation Predicate
  | Conj Predicate Predicate
  | Disj Predicate Predicate
  | Imp Predicate Predicate
  | Equiv Predicate Predicate
  | PIfThenElse Term Predicate Predicate
  | Forall Identifiers Type Triggers Predicate -- one or more Identifier, Trigger
  | Exists Identifiers Type Predicate
--  | X Identifier String Predicate -- what is this?

data Type = 
    TInt 
  | TBool 
  | TReal 
  | TUnit 
  | User Identifier
--  | X Identifier -- what is this?
--  | Y Type Identifier -- what is this?
--  | Z Types Identifier -- what is this?

data LDeclaration =
    DType (Maybe TypeParameters) Identifier -- (Maybe External) dropped
  | DLogic Identifiers Type -- (Maybe External) dropped
  | DFunction Identifier LogicBinders Type Term
  | DPredicate Identifier LogicBinders Predicate
  | DAxiom Identifier Predicate
  | DGoal Identifier Predicate

data LogicType =
    Prop LogicArgTypes
  | LTArrow LogicArgTypes Type

data LogicArgType = LATPrim Type | LATArray Type

data SimpleValueType = 
    SVTPrim Type
  | SVTRef Type
  | SVTArray Type

data ValueType = 
    Simple SimpleValueType
  | VTArrow SimpleValueType ComputationType
  | VTLArrow Identifier SimpleValueType ComputationType

data ComputationType =
    CT (Maybe Pre) (Maybe Identifier) ValueType Effects (Maybe Post)
  | CTVT ValueType

data Prog =
    PConst Constant
  | PIdent Identifier
  | ProgNegation Identifier
  | Assign Identifier Prog
  | ArrayAccess Identifier Prog
  | ArrayAssign Identifier Prog Prog
  | Infix Prog InfixOp Prog
  | Symm Prog
  | Not Prog
  | LetIn Identifier Prog Prog
  | LetInRef Identifier Prog Prog
  | ProgIfThenElse Prog Prog (Maybe Prog)
  | While Prog LoopAnnot Prog
  | Seq Prog Prog
--  | X Identifier Prog -- what is this?
  | Assert Assertions Prog
  | PPost1 Prog Post
  | PPost2 Prog Post
  | Fun Binders Prog
  | LetBind Identifier Binders Prog Prog
  | LetRec RecFun (Maybe Prog)
  | App Prog Prog
  | Raise1 Identifier (Maybe ValueType)
  | Raise2 Identifier Prog (Maybe ValueType)
  | TryWith Prog Handlers
  | Absurd (Maybe ValueType)
  | Block Prog -- is it necessary?

data InfixOp = OpPlus | OpMinus | OpMult | OpDiv | OpRem | OpEq | OpNEq | OpL | OpLT | OpG | OpGT | OpOr | OpAnd

data Handler = 
    Hand1 Identifier Prog
  | Hand2 Identifier Identifier Prog

data Declaration = 
    Let Identifier (Maybe Binders) Prog
  | DLetRec RecFun
  | Parameter Identifiers ValueType -- one or more Identifier
  | Exception Identifier (Maybe Type)
  | L LDeclaration
-}
