{- |

Module : $Header$

Description : translating a HasCASL subset to Isabelle

Copyright : (c) C. Maeder, DFKI 2008

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

utility function for translation from HasCASL to Isabelle leaving open how

partial values are interpreted

-}

module Comorphisms.PPolyTyConsHOL2IsaUtils

( mapTheory

, simpForPairs

, simpForOption

, typeToks

, transSentence

, SimpKind (..)

, OldSimpKind (..)

) where

import HasCASL.As as As

import HasCASL.AsUtils

import HasCASL.Builtin

import HasCASL.DataAna

import HasCASL.Le as Le

import HasCASL.Unify (substGen)

import Isabelle.IsaSign as Isa

import Isabelle.IsaConsts

import Isabelle.IsaPrint

import Isabelle.Translate

import Common.DocUtils

import Common.Id

import Common.Result

import Common.Utils (isSingleton, number)

import Common.Lib.State

import Common.AS_Annotation

import Common.GlobalAnnotations

import qualified Data.Map as Map

import qualified Data.Set as Set

import Data.List

import Data.Maybe

import Control.Monad (foldM)

mapTheory :: SimpKind -> Simplifier -> (Env, [Named Le.Sentence])

-> Result (Isa.Sign, [Named Isa.Sentence])

mapTheory simK simpF (env, sens) = do

let tyToks = typeToks env

sign <- transSignature env tyToks

isens <- mapM (mapNamedM $ transSentence env tyToks simK simpF) sens

(dt, _, _) <- foldM (transDataEntries env tyToks)

([], Set.empty, Set.empty) $ filter (not . null) $ map

(\ ns -> case sentence ns of

DatatypeSen ds -> ds

_ -> []) sens

return ( sign { domainTab = reverse dt }

, filter ((/= mkSen true) . sentence) isens)

-- * Signature

baseSign :: BaseSig

baseSign = MainHC_thy

transAssumps :: GlobalAnnos -> Set.Set String -> Assumps -> Result ConstTab

transAssumps ga toks = foldM insertOps Map.empty . Map.toList where

insertOps m (name, ops) =

let chk = isPlainFunType

in case map opType $ Set.toList ops of

[TypeScheme _ op _ ] -> do

ty <- funType op

return $ Map.insert

(mkIsaConstT (isPredType op) ga (chk ty)

name baseSign toks) (transPlainFunType ty) m

infos -> foldM ( \ m' (TypeScheme _ op _, i) -> do

ty <- funType op

return $ Map.insert

(mkIsaConstIT (isPredType op) ga (chk ty)

name i baseSign toks) (transPlainFunType ty) m'

) m $ number infos

-- all possible tokens of mixfix identifiers that must not be used as variables

getAssumpsToks :: Assumps -> Set.Set String

getAssumpsToks = Map.foldWithKey (\ i ops s ->

Set.union s $ Set.unions

$ map (\ (_, o) -> getConstIsaToks i o baseSign)

$ number $ Set.toList ops) Set.empty

typeToks :: Env -> Set.Set String

typeToks =

Set.map (`showIsaTypeT` baseSign) . Map.keysSet . typeMap

transSignature :: Env -> Set.Set String -> Result Isa.Sign

transSignature env toks = do

let extractTypeName tyId typeInfo m =

let getTypeArgs n k = case k of

ClassKind _ -> []

FunKind _ _ r _ ->

(TFree ("'a" ++ show n) [], holType)

: getTypeArgs (n + 1) r

in Map.insert (showIsaTypeT tyId baseSign)

[(isaTerm, getTypeArgs (1 :: Int) $ typeKind typeInfo)] m

ct <- transAssumps (globAnnos env) toks $ assumps env

return $ Isa.emptySign

{ baseSig = baseSign

-- translation of typeconstructors

, tsig = emptyTypeSig

{ arities = Map.foldWithKey extractTypeName Map.empty

$ typeMap env }

, constTab = ct }

-- * translation of a type in an operation declaration

unitTyp :: Typ

unitTyp = Type "unit" holType []

mkPartialType :: Typ -> Typ

mkPartialType arg = Type "partial" [] [arg]

transFunType :: FunType -> Typ

transFunType fty = case fty of

UnitType -> unitTyp

BoolType -> boolType

FunType f a -> mkFunType (transFunType f) $ transFunType a

PartialVal a -> mkPartialType $ transFunType a

PairType a b -> prodType (transFunType a) $ transFunType b

TupleType l -> case l of

[] -> error "transFunType"

_ -> transFunType $ foldl1 PairType l

ApplType tid args -> Type (showIsaTypeT tid baseSign) []

$ map transFunType args

TypeVar tid -> TFree (showIsaTypeT tid baseSign) []

-- compute number of arguments for plain CASL functions

isPlainFunType :: FunType -> Int

isPlainFunType fty = case fty of

FunType f a -> case a of

FunType _ _ -> -1

_ -> case f of

TupleType l -> length l

_ -> 1

_ -> 0

transPlainFunType :: FunType -> Typ

transPlainFunType fty =

case fty of

FunType (TupleType l) a -> case a of

FunType _ _ -> transFunType fty

_ -> foldr (mkFunType . transFunType) (transFunType a) l

_ -> transFunType fty

data FunType = UnitType | BoolType

| FunType FunType FunType

| PartialVal FunType

| PairType FunType FunType -- only used to represent tuples as nested pairs

| TupleType [FunType]

| ApplType Id [FunType]

| TypeVar Id

deriving (Eq, Show)

isPartialVal :: FunType -> Bool

isPartialVal t = case t of

PartialVal _ -> True

BoolType -> True

_ -> False

makePartialVal :: FunType -> FunType

makePartialVal t = if isPartialVal t then t else case t of

UnitType -> BoolType

_ -> PartialVal t

funType :: Type -> Result FunType

funType t = case getTypeAppl t of

(TypeName tid _ n, tys)

| n == 0 -> do

ftys <- mapM funType tys

return $ case ftys of

[] | tid == unitTypeId -> UnitType

[ty] | tid == lazyTypeId -> makePartialVal ty

[t1, t2] | isArrow tid -> FunType t1 $

if isPartialArrow tid then makePartialVal t2 else t2

(_ : _ : _) | isProductId tid -> TupleType ftys

_ -> ApplType tid ftys

| null tys -> return $ TypeVar tid

_ -> fatal_error "funType: no flat type appl" $ getRange t

-- * translation of a datatype declaration

transDataEntries :: Env -> Set.Set String

-> (DomainTab, Set.Set TName, Set.Set VName) -> [DataEntry]

-> Result (DomainTab, Set.Set TName, Set.Set VName)

transDataEntries env tyToks t@(dt, tys, cs) l = do

let rs = map (transDataEntry env tyToks) l

ms = map maybeResult rs

toWarning = map ( \ d -> d { diagKind = Warning })

appendDiags $ toWarning $ concatMap diags rs

if any isNothing ms then return t

else do

let des = catMaybes ms

ntys = map (Isa.typeId . fst . fst) des

ncs = concatMap (map fst . snd) des

foldF str cnv = foldM ( \ s i ->

if Set.member i s then

fail $ "duplicate " ++ str ++ cnv i

else return $ Set.insert i s)

Result d1 mrtys = foldF "datatype " id tys ntys

Result d2 mrcs = foldF "constructor " new cs ncs

appendDiags $ toWarning $ d1 ++ d2

case (mrtys, mrcs) of

(Just rtys, Just rcs) -> return (des : dt, rtys, rcs)

_ -> return t

-- datatype with name (tyId) + args (tyArgs) and alternatives

transDataEntry :: Env -> Set.Set String -> DataEntry -> Result DomainEntry

transDataEntry env tyToks de@(DataEntry _ _ gk _ _ alts) =

let dp@(DataPat _ i tyArgs _ _) = toDataPat de

in case gk of

Le.Free -> do

nalts <- mapM (transAltDefn env tyToks dp) $ Set.toList alts

let transDName ti = Type (showIsaTypeT ti baseSign) []

. map transTypeArg

return ((transDName i tyArgs, Nothing), nalts)

_ -> fatal_error ("not a free type: " ++ show i)

$ posOfId i

-- arguments of a datatype's typeconstructor

transTypeArg :: TypeArg -> Typ

transTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []

-- datatype alternatives/constructors

transAltDefn :: Env -> Set.Set String -> DataPat -> AltDefn

-> Result (VName, [Typ])

transAltDefn env tyToks dp alt = case alt of

Construct mi ts p _ -> case mi of

Just opId -> case p of

Total -> do

let sc = getConstrScheme dp p ts

nts <- mapM funType ts

-- extract overloaded opId number

return (transOpId env tyToks opId sc, case nts of

[TupleType l] -> map transFunType l

_ -> map transFunType nts)

Partial -> mkError "not a total constructor" opId

Nothing -> mkError "no support for data subtypes" ts

-- * Formulas

-- variables

transVar :: Set.Set String -> Id -> VName

transVar toks v = let

s = showIsaConstT v baseSign

renVar t = if Set.member t toks then renVar $ "X_" ++ t else t

in mkVName $ renVar s

mkTypedConst :: VName -> FunType -> Isa.Term

mkTypedConst v fTy = Isa.Const v $ Disp (transFunType fTy) NA Nothing

transTypedVar :: Set.Set String -> VarDecl -> Result Isa.Term

transTypedVar toks (VarDecl var ty _ _) = do

fTy <- funType ty

return $ mkTypedConst (transVar toks var) fTy

mkSimplifiedSen :: OldSimpKind -> Simplifier -> Isa.Term -> Isa.Sentence

mkSimplifiedSen simK simpF t = mkSen $ evalState (simplify simK simpF t) 0

isTrue :: Isa.Term -> Bool

isTrue t = case t of

Const n _ -> new n == cTrue

_ -> False

mkBinConj :: Isa.Term -> Isa.Term -> Isa.Term

mkBinConj t1 t2 = case isTrue of

isT | isT t1 -> t2

| isT t2 -> t1

_ -> binConj t1 t2

data OldSimpKind = NoSimpLift | Lift2Restrict | Lift2Case deriving Eq

data SimpKind = New | Old OldSimpKind deriving Eq

transSentence :: Env -> Set.Set String -> SimpKind -> Simplifier -> Le.Sentence

-> Result Isa.Sentence

transSentence sign tyToks simK simpF s = case s of

Le.Formula trm -> do

ITC ty t cs <- transTerm sign tyToks (simK == New)

(getAssumpsToks $ assumps sign) Set.empty trm

let et = case ty of

PartialVal UnitType -> mkTermAppl defOp t

_ -> t

bt = if isTrue et then cond2bool cs else

mkTermAppl (integrateCondInBool cs) et

st = mkSimplifiedSen (case simK of

Old osim -> osim

New -> NoSimpLift) simpF bt

case ty of

BoolType -> return st

PartialVal _ -> return st

FunType _ _ -> error "transSentence: FunType"

PairType _ _ -> error "transSentence: PairType"

TupleType _ -> error "transSentence: TupleType"

ApplType _ _ -> error "transSentence: ApplType"

_ -> return $ mkSen true

DatatypeSen ls -> if all (\ (DataEntry _ _ gk _ _ _) -> gk == Generated) ls

then transSentence sign tyToks simK simpF . Le.Formula

$ inductionScheme ls

else return $ mkSen true

ProgEqSen _ _ (ProgEq _ _ r) -> warning (mkSen true)

"translation of sentence not implemented" r

-- disambiguate operation names

transOpId :: Env -> Set.Set String -> Id -> TypeScheme -> VName

transOpId sign tyToks op ts@(TypeScheme _ ty _) =

let ga = globAnnos sign

Result _ mty = funType ty

in case mty of

Nothing -> error "transOpId"

Just fty ->

let args = isPlainFunType fty

in fromMaybe (error $ "transOpId " ++ show op) $ do

ops <- Map.lookup op (assumps sign)

if isSingleton ops then return $

mkIsaConstT (isPredType ty) ga args op baseSign tyToks

else do

i <- elemIndex ts $ map opType $ Set.toList ops

return $ mkIsaConstIT (isPredType ty)

ga args op (i + 1) baseSign tyToks

transLetEq :: Env -> Set.Set String -> Bool -> Set.Set String

-> Set.Set VarDecl -> ProgEq -> Result ((As.Term, Isa.Term), IsaTermCond)

transLetEq sign tyToks collectConds toks pVars (ProgEq pat trm r) = do

(_, op) <- transPattern sign tyToks toks pat

p@(ITC ty _ _) <- transTerm sign tyToks collectConds toks pVars trm

if isPartialVal ty && not (isQualVar pat) then fatal_error

("rhs must not be partial for a tuple currently: "

++ showDoc trm "") r

else return ((pat, op), p)

transLetEqs :: Env -> Set.Set String -> Bool -> Set.Set String

-> Set.Set VarDecl -> [ProgEq]

-> Result (Set.Set VarDecl, [(Isa.Term, IsaTermCond)])

transLetEqs sign tyToks collectConds toks pVars es = case es of

[] -> return (pVars, [])

e : r -> do

((pat, op), pt@(ITC ty _ _)) <-

transLetEq sign tyToks collectConds toks pVars e

(newPVars, newEs) <- transLetEqs sign tyToks collectConds toks

(if isPartialVal ty then Set.insert (getQualVar pat) pVars else pVars) r

return (newPVars, (op, pt) : newEs)

isQualVar :: As.Term -> Bool

isQualVar trm = case trm of

QualVar (VarDecl _ _ _ _) -> True

TypedTerm t _ _ _ -> isQualVar t

_ -> False

getQualVar :: As.Term -> VarDecl

getQualVar trm = case trm of

QualVar vd -> vd

TypedTerm t _ _ _ -> getQualVar t

_ -> error "getQualVar"

ifImplOp :: Isa.Term

ifImplOp = conDouble "ifImplOp"

unitOp :: Isa.Term

unitOp = Tuplex [] NotCont

noneOp :: Isa.Term

noneOp = conDouble "undefinedOp"

whenElseOp :: Isa.Term

whenElseOp = conDouble "whenElseOp"

resOp :: Isa.Term

resOp = conDouble "resOp"

makeTotal :: Isa.Term

makeTotal = conDouble "makeTotal"

uncurryOpS :: String

uncurryOpS = "uncurryOp"

curryOpS :: String

curryOpS = "curryOp"

uncurryOp :: Isa.Term

uncurryOp = conDouble uncurryOpS

curryOp :: Isa.Term

curryOp = conDouble curryOpS

for :: Int -> (a -> a) -> a -> a

for n f a = if n <= 0 then a else for (n - 1) f $ f a

data IsaTermCond = ITC FunType Isa.Term Cond

data Cond = None

| Cond Isa.Term

| CondList [Cond]

| PairCond Cond Cond

instance Show Cond where

show c = case c of

None -> "none"

Cond t -> show $ printTerm t

CondList l -> intercalate " & " $ map show l

PairCond p1 p2 -> '(' : shows p1 ", " ++ shows p2 ")"

joinCond :: Cond -> Cond -> Cond

joinCond c1 c2 = let

toCs c = case c of

CondList cs -> cs

None -> []

_ -> [c]

in case toCs c1 ++ toCs c2 of

[] -> None

[s] -> s

cs -> CondList cs

pairCond :: Cond -> Cond -> Cond

pairCond c1 c2 = case (c1, c2) of

(None, None) -> None

_ -> PairCond c1 c2

condToList :: Cond -> [Isa.Term]

condToList c = case c of

None -> []

Cond t -> [t]

CondList cs -> concatMap condToList cs

PairCond c1 c2 -> condToList c1 ++ condToList c2

{- pass tokens that must not be used as variable names and pass those

variables that are partial because they have been computed in a

let-term. -}

transTerm :: Env -> Set.Set String -> Bool -> Set.Set String

-> Set.Set VarDecl -> As.Term -> Result IsaTermCond

transTerm sign tyToks collectConds toks pVars trm = case trm of

QualVar vd@(VarDecl v t _ _) -> do

fTy <- funType t

let vt = con $ transVar toks v

return $ if Set.member vd pVars then ITC (makePartialVal fTy) vt None

else ITC fTy vt None

QualOp _ (PolyId opId _ _) ts@(TypeScheme targs ty _) insts _ _ -> do

fTy <- funType ty

instfTy <- funType $ substGen (if null insts then Map.empty else

Map.fromList $ zipWith (\ (TypeArg _ _ _ _ i _ _) t

-> (i, t)) targs insts) ty

let cf = mkTermAppl (convFun None $ instType fTy instfTy)

unCurry f = let rf = termAppl uncurryOp $ con f in

ITC fTy rf None

return $ case (opId ==) of

is | is trueId -> ITC fTy true None

| is falseId -> ITC fTy false None

| is botId -> case instfTy of

PartialVal t -> ITC t (termAppl makeTotal noneOp) $ Cond false

_ -> ITC instfTy (cf noneOp) None

| is andId -> unCurry conjV

| is orId -> unCurry disjV

| is implId -> unCurry implV

| is infixIf -> ITC fTy ifImplOp None

| is eqvId -> unCurry eqV

| is exEq -> let

ef = cf $ termAppl uncurryOp existEqualOp

in ITC instfTy ef None

| is eqId -> let

ef = cf $ termAppl uncurryOp $ con eqV

in ITC instfTy ef None

| is notId -> ITC fTy notOp None

| is defId -> ITC instfTy (cf defOp) None

| is whenElse -> ITC instfTy (cf whenElseOp) None

| is resId -> ITC instfTy (cf resOp) None

_ -> let

isaId = transOpId sign tyToks opId ts

ef = cf $ for (isPlainFunType fTy - 1) (termAppl uncurryOp)

$ if elem opId [injName, projName] then

mkTypedConst isaId instfTy

else con isaId

in ITC instfTy ef None

QuantifiedTerm quan varDecls phi _ -> do

let qname = case quan of

Universal -> allS

Existential -> exS

Unique -> ex1S

quantify phi' gvd = case gvd of

GenVarDecl vd -> do

vt <- transTypedVar toks vd

return $ termAppl (conDouble qname) $ Abs vt phi' NotCont

GenTypeVarDecl _ -> return phi'

ITC ty psi cs <- fmap integrateCond

$ transTerm sign tyToks collectConds toks pVars phi

psiR <- foldM quantify psi $ reverse varDecls

return $ ITC ty psiR cs

TypedTerm t _q _ty _ -> transTerm sign tyToks collectConds toks pVars t

LambdaTerm pats q body r -> do

p@(ITC ty _ ncs) <- transTerm sign tyToks collectConds toks pVars body

appendDiags $ case q of

Partial -> []

Total -> [Diag Warning

("partial lambda body in total abstraction: "

++ showDoc body "") r

| isPartialVal ty || not (isTrue $ cond2bool ncs) ]

foldM (abstraction sign tyToks toks) (integrateCond p)

$ reverse pats

LetTerm As.Let peqs body _ -> do

(nPVars, nEqs) <-

transLetEqs sign tyToks collectConds toks pVars peqs

ITC bTy bTrm defCs <-

transTerm sign tyToks collectConds toks nPVars body

let pEs = map (\ (p, ITC _ t _) -> (p, t)) nEqs

cs = foldl joinCond None $ map (\ (_, ITC _ _ c) -> c) nEqs

return $ ITC bTy (mkLetAppl pEs bTrm) $ joinCond cs defCs

TupleTerm ts@(_ : _) _ -> do

nTs <- mapM (transTerm sign tyToks collectConds toks pVars) ts

return $ foldl1 ( \ (ITC s p cs) (ITC t e cr) ->

ITC (PairType s t) (Tuplex [p, e] NotCont) $ pairCond cs cr) nTs

TupleTerm [] _ -> return $ ITC UnitType unitOp None

ApplTerm t1 t2 _ -> mkApp sign tyToks collectConds toks pVars t1 t2

_ -> fatal_error ("cannot translate term: " ++ showDoc trm "")

$ getRange trm

integrateCond :: IsaTermCond -> IsaTermCond

integrateCond (ITC ty trm cs) = if isTrue $ cond2bool cs then

ITC ty trm None

else case ty of

PartialVal _ -> ITC ty (mkTermAppl (integrateCondInPartial cs) trm) None

BoolType -> ITC ty (mkTermAppl (integrateCondInBool cs) trm) None

UnitType -> ITC BoolType (cond2bool cs) None

_ -> ITC (makePartialVal ty)

(mkTermAppl (integrateCondInTotal cs) trm) None

-- return partial result type

instType :: FunType -> FunType -> ConvFun

instType f1 f2 = case (f1, f2) of

(TupleType l1, _) -> instType (foldl1 PairType l1) f2

(_, TupleType l2) -> instType f1 $ foldl1 PairType l2

(PartialVal (TypeVar _), BoolType) -> Partial2bool True

(PairType a c, PairType b d) ->

let c2 = instType c d

c1 = instType a b

in mkCompFun (mkMapFun MapSnd c2) $ mkMapFun MapFst c1

(FunType a c, FunType b d) ->

let c2 = instType c d

c1 = instType a b

in mkCompFun (mkResFun c2) $ mkArgFun $ invertConv c1

_ -> IdOp

invertConv :: ConvFun -> ConvFun

invertConv c = case c of

Partial2bool _ -> Bool2partial False

Bool2partial _ -> Partial2bool False

Unit2bool _ -> Bool2unit

Bool2unit -> Unit2bool False

MkPartial _ -> MkTotal

MkTotal -> MkPartial False

MapFun mv cf -> mkMapFun mv $ invertConv cf

ResFun cf -> mkResFun $ invertConv cf

ArgFun cf -> mkArgFun $ invertConv cf

CompFun c1 c2 -> mkCompFun (invertConv c2) (invertConv c1)

_ -> IdOp

data MapFun = MapFst | MapSnd | MapPartial deriving Show

data LiftFun = LiftFst | LiftSnd deriving Show

{- the additional Bool indicates condition integration

Bool2bool and Partial2partial must be mapped to IdOp

if the conditions should be ignored.

Bool2Unit and MkTotal can propagate out conditions -}

data ConvFun =

IdOp

| Bool2partial Bool

| Partial2bool Bool

| Bool2bool

| Unit2bool Bool

| Bool2unit

| Partial2partial

| MkPartial Bool

| MkTotal

| CompFun ConvFun ConvFun

| MapFun MapFun ConvFun

| LiftFun LiftFun ConvFun

| LiftUnit FunType

| LiftPartial FunType

| ResFun ConvFun

| ArgFun ConvFun

deriving Show

isNotIdOp :: ConvFun -> Bool

isNotIdOp f = case f of

IdOp -> False

_ -> True

mkCompFun :: ConvFun -> ConvFun -> ConvFun

mkCompFun f1 f2 = case f1 of

IdOp -> f2

_ -> case f2 of

IdOp -> f1

_ -> CompFun f1 f2

mkMapFun :: MapFun -> ConvFun -> ConvFun

mkMapFun m f = case f of

IdOp -> IdOp

_ -> MapFun m f

mkLiftFun :: LiftFun -> ConvFun -> ConvFun

mkLiftFun lv c = case c of

IdOp -> IdOp

_ -> LiftFun lv c

mapFun :: MapFun -> Isa.Term

mapFun mf = case mf of

MapFst -> mapFst

MapSnd -> mapSnd

MapPartial -> mapPartial

compOp :: Isa.Term

compOp = con compV

convFun :: Cond -> ConvFun -> Isa.Term

convFun cnd cvf = case cvf of

IdOp -> idOp

Bool2partial b -> if b

then metaComp bool2partial $ integrateCondInBool cnd

else bool2partial

Partial2bool b -> if b

then metaComp (integrateCondInBool cnd) defOp

else defOp

Bool2bool -> integrateCondInBool cnd

Unit2bool b -> if b

then metaComp (integrateCondInBool cnd) constTrue else constTrue

Bool2unit -> constNil

Partial2partial -> integrateCondInPartial cnd

MkPartial b -> if b

then integrateCondInTotal cnd

else mkPartial

MkTotal -> makeTotal

LiftUnit rTy -> case rTy of

UnitType -> liftUnit2unit

BoolType -> liftUnit2bool

PartialVal _ -> liftUnit2partial

_ -> liftUnit

LiftPartial rTy ->

case rTy of

UnitType -> lift2unit

BoolType -> lift2bool

PartialVal _ -> lift2partial

_ -> mapPartial

CompFun f1 f2 -> metaComp (convFun cnd f1) $ convFun cnd f2

MapFun mf cv -> mkTermAppl (mapFun mf) $ convFun cnd cv

LiftFun lf cv -> let ccv = convFun cnd cv in case lf of

LiftFst -> metaComp (metaComp uncurryOp flipOp)

$ metaComp (metaComp (mkTermAppl compOp ccv) flipOp)

curryOp

LiftSnd -> metaComp uncurryOp $ metaComp (mkTermAppl compOp ccv)

curryOp

ArgFun cv -> mkTermAppl (termAppl flipOp compOp) $ convFun cnd cv

ResFun cv -> mkTermAppl compOp $ convFun cnd cv

mapFst, mapSnd, mapPartial, idOp, bool2partial, constNil, constTrue,

liftUnit2unit, liftUnit2bool, liftUnit2partial, liftUnit, lift2unit,

lift2bool, lift2partial, mkPartial, restrict :: Isa.Term

mapFst = conDouble "mapFst"

mapSnd = conDouble "mapSnd"

mapPartial = conDouble "mapPartial"

idOp = conDouble "id"

bool2partial = conDouble "bool2partial"

constNil = conDouble "constNil"

constTrue = conDouble "constTrue"

liftUnit2unit = conDouble "liftUnit2unit"

liftUnit2bool = conDouble "liftUnit2bool"

liftUnit2partial = conDouble "liftUnit2partial"

liftUnit = conDouble "liftUnit"

lift2unit = conDouble "lift2unit"

lift2bool = conDouble "lift2bool"

lift2partial = conDouble "lift2partial"

mkPartial = conDouble "makePartial"

restrict = conDouble "restrictOp"

existEqualOp :: Isa.Term

existEqualOp =

con $ VName "existEqualOp" $ Just $ AltSyntax "(_ =e=/ _)" [50, 51] 50

integrateCondInBool :: Cond -> Isa.Term

integrateCondInBool c = let b = cond2bool c in

if isTrue b then idOp else mkTermAppl (con conjV) b

integrateCondInPartial :: Cond -> Isa.Term

integrateCondInPartial c = let b = cond2bool c in

if isTrue b then idOp else

mkTermAppl (mkTermAppl flipOp restrict) b

metaComp :: Isa.Term -> Isa.Term -> Isa.Term

metaComp = mkTermAppl . mkTermAppl compOp

integrateCondInTotal :: Cond -> Isa.Term

integrateCondInTotal c = metaComp (integrateCondInPartial c) mkPartial

addCond :: Isa.Term -> Cond -> Cond

addCond = joinCond . Cond

cond2bool :: Cond -> Isa.Term

cond2bool c = case nub $ condToList c of

[] -> true

ncs -> foldr1 mkBinConj ncs

{- adjust actual argument to expected argument type of function

considering a definedness conditions -}

adjustArgType :: FunType -> FunType -> Result ConvFun

adjustArgType aTy ty = case (aTy, ty) of

(TupleType l, _) -> adjustArgType (foldl1 PairType l) ty

(_, TupleType l) -> adjustArgType aTy $ foldl1 PairType l

(BoolType, BoolType) -> return Bool2bool

(UnitType, UnitType) -> return IdOp

(PartialVal UnitType, BoolType) -> return $ Bool2partial True

(BoolType, PartialVal UnitType) -> return $ Partial2bool True

(UnitType, BoolType) -> return Bool2unit

(BoolType, UnitType) -> return $ Unit2bool True

(PartialVal a, PartialVal b) -> do

c <- adjustArgType a b

return $ mkCompFun Partial2partial c

(a, PartialVal b) -> do

c <- adjustArgType a b

return $ mkCompFun MkTotal c

(PartialVal a, b) -> do

c <- adjustArgType a b

return $ mkCompFun (MkPartial True) c

(PairType e1 e2, PairType a1 a2) -> do

c1 <- adjustArgType e1 a1

c2 <- adjustArgType e2 a2

return . mkCompFun (mkMapFun MapSnd c2) $ mkMapFun MapFst c1

(FunType a b, FunType c d) -> do

aC <- adjustArgType a c -- function a -> c (a fixed)

dC <- adjustArgType b d -- function d -> b (b fixed)

{- (d -> b) o (c -> d) o (a -> c) :: a -> b

do not integrate cond treatment via invertConv . invertConv -}

return . mkCompFun (mkResFun . invertConv $ invertConv dC)

. mkArgFun $ invertConv aC

(TypeVar _, _) -> return IdOp

(_, TypeVar _) -> return IdOp

(ApplType i1 l1, ApplType i2 l2) | i1 == i2 && length l1 == length l2 -> do

l <- mapM (uncurry adjustArgType) $ zip l1 l2

if any (isNotIdOp . invertConv) l

then fail "cannot adjust type application"

else return IdOp

_ -> fail $ "cannot adjust argument type\n" ++ show (aTy, ty)

unpackOp :: Isa.Term -> Bool -> Bool -> FunType -> ConvFun -> Isa.Term

unpackOp fTrm isPf pfTy ft fConv = let isaF = convFun None fConv in

if isPf then mkTermAppl

(mkTermAppl (conDouble $ case if pfTy then makePartialVal ft else ft of

UnitType -> "unpack2bool"

BoolType -> "unpackBool"

PartialVal _ -> "unpackPartial"

_ -> "unpack2partial") isaF) fTrm

else mkTermAppl isaF fTrm

-- True means function type result was partial

adjustMkApplOrig :: Isa.Term -> Cond -> Bool -> FunType -> FunType

-> IsaTermCond -> Result IsaTermCond

adjustMkApplOrig fTrm fCs isPf aTy rTy (ITC ty aTrm aCs) = do

((pfTy, fConv), (_, aConv)) <- adjustTypes aTy rTy ty

return . ITC (if isPf || pfTy then makePartialVal rTy else rTy)

(mkTermAppl (unpackOp fTrm isPf pfTy rTy fConv)

$ mkTermAppl (convFun None aConv) aTrm) $ joinCond fCs aCs

-- True means require result type to be partial

adjustTypes :: FunType -> FunType -> FunType

-> Result ((Bool, ConvFun), (FunType, ConvFun))

adjustTypes aTy rTy ty = case (aTy, ty) of

(TupleType l, _) -> adjustTypes (foldl1 PairType l) rTy ty

(_, TupleType l) -> adjustTypes aTy rTy $ foldl1 PairType l

(BoolType, BoolType) -> return ((False, IdOp), (ty, IdOp))

(UnitType, UnitType) -> return ((False, IdOp), (ty, IdOp))

(PartialVal _, BoolType) ->

return ((False, IdOp), (aTy, Bool2partial False))

(BoolType, PartialVal _) ->

return ((False, IdOp), (aTy, Partial2bool False))

(_, BoolType) -> return ((True, LiftUnit rTy), (ty, IdOp))

(BoolType, _) -> return ((False, IdOp), (aTy, Unit2bool False))

(PartialVal a, PartialVal b) -> do

q@(fp, (argTy, aTrm)) <- adjustTypes a rTy b

return $ case argTy of

PartialVal _ -> q

_ -> (fp, (PartialVal argTy, mkMapFun MapPartial aTrm))

(a, PartialVal b) -> do

q@(_, ap@(argTy, _)) <- adjustTypes a rTy b

return $ case argTy of

PartialVal _ -> q

_ -> ((True, LiftPartial rTy), ap)

(PartialVal a, b) -> do

q@(fp, (argTy, aTrm)) <- adjustTypes a rTy b

return $ case argTy of

PartialVal _ -> q

_ -> (fp, (PartialVal argTy, mkCompFun (MkPartial False) aTrm))

(PairType a c, PairType b d) -> do

((res2Ty, f2), (arg2Ty, a2)) <- adjustTypes c rTy d

((res1Ty, f1), (arg1Ty, a1)) <- adjustTypes a

(if res2Ty then makePartialVal rTy else rTy) b

return ((res1Ty || res2Ty,

mkCompFun (mkLiftFun LiftFst f1) $ mkLiftFun LiftSnd f2),

(PairType arg1Ty arg2Ty,

mkCompFun (mkMapFun MapSnd a2) $ mkMapFun MapFst a1))

(FunType a c, FunType b d) -> do

((_, aF), (aT, aC)) <- adjustTypes b c a

((cB, cF), (dT, dC)) <- adjustTypes c rTy d

if cB || isNotIdOp cF

then fail "cannot adjust result types of function type"

else return ((False, IdOp), (FunType aT dT,

mkCompFun aF $ mkCompFun (mkResFun dC) $ mkArgFun aC))

(TypeVar _, _) -> return ((False, IdOp), (ty, IdOp))

(_, TypeVar _) -> return ((False, IdOp), (aTy, IdOp))

(ApplType i1 l1, ApplType i2 l2) | i1 == i2 && length l1 == length l2 -> do

l <- mapM (\ (a, b) -> adjustTypes a rTy b) $ zip l1 l2

if any (fst . fst) l || any (isNotIdOp . snd . snd) l

then fail "cannot adjust type application"

else return ((False, IdOp), (ApplType i1 $ map (fst . snd) l, IdOp))

_ -> fail $ "cannot adjust types\n" ++ show (aTy, ty)

adjustMkAppl :: Isa.Term -> Cond -> Bool -> FunType -> FunType

-> IsaTermCond -> Result IsaTermCond

adjustMkAppl fTrm fCs isPf aTy rTy (ITC ty aTrm aCs) = do

aConv <- adjustArgType aTy ty

let (natrm, nacs) = applConv aConv (aTrm, aCs)

(nftrm, nfcs) = if isPf

then (mkTermAppl makeTotal fTrm, addCond (mkTermAppl defOp fTrm) fCs)

else (fTrm, fCs)

return $ ITC rTy (mkTermAppl nftrm natrm) $ joinCond nfcs nacs

applConv :: ConvFun -> (Isa.Term, Cond) -> (Isa.Term, Cond)

applConv cnv (t, c) = let

rt = mkTermAppl (convFun c cnv) t

r = (rt, c)

rb = (rt, None)

in case cnv of

IdOp -> (t, c)

Bool2partial b -> if b then rb else r

Partial2bool b -> if b then rb else r

Bool2bool -> rb

Unit2bool b -> if b then rb else r

Bool2unit -> (rt, addCond t c)

Partial2partial -> rb

MkPartial b -> if b then rb else r

MkTotal -> (rt, addCond (mkTermAppl defOp t) c)

CompFun f1 f2 -> applConv f1 $ applConv f2 (t, c)

MapFun mf cv -> case t of

Tuplex [t1, t2] _ -> let

(c1, c2) = case c of

PairCond p1 p2 -> (p1, p2)

_ -> (c, c)

in case mf of

MapFst -> let

(nt1, nc1) = applConv cv (t1, c1)

in (Tuplex [nt1, t2] NotCont, PairCond nc1 c2)

MapSnd -> let

(nt2, nc2) = applConv cv (t2, c2)

in (Tuplex [t1, nt2] NotCont, PairCond c1 nc2)

MapPartial -> r

_ -> r

_ -> r

mkArgFun :: ConvFun -> ConvFun

mkArgFun c = case c of

IdOp -> c

Bool2bool -> c

Partial2partial -> c

_ -> ArgFun c

mkResFun :: ConvFun -> ConvFun

mkResFun c = case c of

IdOp -> c

Bool2bool -> c

Partial2partial -> c

_ -> ResFun c

isEquallyLifted :: Isa.Term -> Isa.Term -> Maybe (Isa.Term, Isa.Term, Isa.Term)

isEquallyLifted l r = case (l, r) of

(App ft@(Const f _) la _,

App (Const g _) ra _)

| f == g && elem (new f) ["makePartial", "bool2partial"]

-> Just (ft, la, ra)

_ -> Nothing

isLifted :: Isa.Term -> Bool

isLifted t = case t of

App (Const f _) _ _ | new f == "makePartial" -> True

_ -> False

splitArg :: Isa.Term -> (Isa.Term, Isa.Term)

splitArg arg = case arg of

App (App (Const n _) p _) b _ | new n == "restrictOp" ->

case p of

App (Const pp _) t _ | new pp == "makePartial"

-> (b, t)

_ -> (mkBinConj b $ mkTermAppl defOp p, mkTermAppl makeTotal p)

_ -> (mkTermAppl defOp arg, mkTermAppl makeTotal arg)

flipS :: String

flipS = "flip"

flipOp :: Isa.Term

flipOp = conDouble flipS

mkTermAppl :: Isa.Term -> Isa.Term -> Isa.Term

mkTermAppl fun arg = case (fun, arg) of

(App (Const uc _) b _, Tuplex [l, r] _) | new uc == uncurryOpS ->

let res = mkTermAppl (mkTermAppl b l) r in case b of

Const bin _ | elem (new bin) [eq, "existEqualOp"] ->

case isEquallyLifted l r of

Just (_, la, ra) -> mkTermAppl (mkTermAppl (con eqV) la) ra

_ -> if isLifted l || isLifted r

then mkTermAppl (mkTermAppl (con eqV) l) r

else let

(lb, lt) = splitArg l

(rb, rt) = splitArg r

in if new bin == "existEqualOp" then

mkBinConj lb $ mkBinConj rb

$ mkTermAppl (mkTermAppl (con eqV) lt) rt

else res

_ -> res

(App (Const mp _) f _, Tuplex [a, b] c)

| new mp == "mapFst" -> Tuplex [mkTermAppl f a, b] c

| new mp == "mapSnd" -> Tuplex [a, mkTermAppl f b] c

(Const mp _, Tuplex [a, b] _)

| new mp == "ifImplOp" -> binImpl b a

(Const mp _, Tuplex [Tuplex [a, b] _, c] d)

| new mp == "whenElseOp" -> case isEquallyLifted a c of

Just (f, na, nc) -> mkTermAppl f $ If b na nc d

Nothing -> If b a c d

(App (Const mp _) f _, App (Const mp2 _) arg2 _)

| new mp == "mapPartial" && new mp2 == "makePartial" ->

mkTermAppl mkPartial $ mkTermAppl f arg2

(App (Const mp _) f c, _)

| new mp == "liftUnit2bool" -> let af = mkTermAppl f unitOp in

case arg of

Const ma _ | isTrue arg -> af

| new ma == cFalse -> false

_ -> If arg af false c

| new mp == "liftUnit2partial" -> let af = mkTermAppl f unitOp in

case arg of

Const ma _ | isTrue arg -> af

| new ma == cFalse -> noneOp

_ -> If arg af noneOp c

(App (Const mp _) _ _, _)

| new mp == "liftUnit2unit" -> arg

| new mp == "lift2unit" -> mkTermAppl defOp arg

(App (App (Const cmp _) f _) g c, _)

| new cmp == compS -> mkTermAppl f $ mkTermAppl g arg

| new cmp == curryOpS -> mkTermAppl f $ Tuplex [g, arg] c

| new cmp == flipS -> mkTermAppl (mkTermAppl f arg) g

(Const d _, App (Const sm _) a _)

| new d == defOpS && new sm == "makePartial" -> true

| new d == defOpS && new sm == "bool2partial"

|| new d == "bool2partial" && new sm == defOpS -> a

| new d == curryOpS && new sm == uncurryOpS -> a

(Const i _, _)

| new i == "bool2partial" ->

let tc = mkTermAppl mkPartial unitOp

in case arg of

Const j _ | isTrue arg -> tc

| new j == cFalse -> noneOp

_ -> termAppl fun arg -- If arg tc noneOp NotCont

| new i == "id" -> arg

| new i == "constTrue" -> true

| new i == "constNil" -> unitOp

(Const i _, Tuplex [] _)

| new i == defOpS -> false

_ -> termAppl fun arg

freshIndex :: State Int Int

freshIndex = do

i <- get

put $ i + 1

return i

type Simplifier = VName

-> Isa.Term -- variable

-> Isa.Term -- simplified application to variable

-> Isa.Term -- simplified argument

-> State Int Isa.Term

simpForOption :: Simplifier

simpForOption l v nF nArg =

return $ Case nArg

[ (conDouble "None", if new l == "lift2bool" then false else noneOp)

, (termAppl conSome v,

if new l == "mapPartial" then mkTermAppl mkPartial nF else nF)]

mkLetAppl :: [(Isa.Term, Isa.Term)] -> Isa.Term -> Isa.Term

mkLetAppl eqs inTrm = case inTrm of

App (Const mp _) arg _ | new mp == "makePartial" ->

mkTermAppl mkPartial $ Isa.Let eqs arg

_ -> Isa.Let eqs inTrm

simpForPairs :: Simplifier

simpForPairs l v2 nF nArg = do

n <- freshIndex

let v1 = mkFree $ "Xb" ++ show n

return $ mkLetAppl [(Tuplex [v1, v2] NotCont, nArg)] $

If v1 (if new l == "mapPartial" then mkTermAppl mkPartial nF else nF)

(if new l == "lift2bool" then false else noneOp) NotCont

simplify :: OldSimpKind -> Simplifier -> Isa.Term -> State Int Isa.Term

simplify simK simpF trm = case trm of

App (App (Const l _) f _) arg _

| simK /= NoSimpLift && elem (new l)

["lift2bool", "lift2partial", "mapPartial"] -> do

nArg <- simplify simK simpF arg

let lf = new l

res = simK == Lift2Restrict

if res && lf == "lift2partial" then return . mkTermAppl

(mkTermAppl restrict . mkTermAppl f $ mkTermAppl makeTotal nArg)

$ mkTermAppl defOp nArg

else if res && lf == "mapPartial" then return . mkTermAppl

(mkTermAppl restrict . mkTermAppl mkPartial

. mkTermAppl f $ mkTermAppl makeTotal nArg)

$ mkTermAppl defOp nArg

else do

n <- freshIndex

let pvar = mkFree $ "Xc" ++ show n

nF <- simplify simK simpF $ mkTermAppl f pvar

simpF l pvar nF nArg

App f arg c -> do

nF <- simplify simK simpF f

nArg <- simplify simK simpF arg

return $ App nF nArg c

Abs v t c -> do

nT <- simplify simK simpF t

return $ Abs v nT c

_ -> return trm

mkApp :: Env -> Set.Set String -> Bool -> Set.Set String

-> Set.Set VarDecl -> As.Term -> As.Term -> Result IsaTermCond

mkApp sign tyToks collectConds toks pVars f arg = do

fTr@(ITC fTy fTrm fCs) <-

transTerm sign tyToks collectConds toks pVars f

aTr <- transTerm sign tyToks collectConds toks pVars arg

let pv = case arg of -- dummy application of a unit argument

TupleTerm [] _ -> return fTr

_ -> mkError "wrong function type" f

adjstAppl = if collectConds then adjustMkAppl else adjustMkApplOrig

adjustPos (getRange [f, arg]) $ case fTy of

FunType a r -> adjstAppl fTrm fCs False a r aTr

PartialVal (FunType a r) -> adjstAppl fTrm fCs True a r aTr

PartialVal _ -> pv

BoolType -> pv

_ -> mkError "not a function type" f

-- * translation of lambda abstractions

isPatternType :: As.Term -> Bool

isPatternType trm = case trm of

QualVar (VarDecl _ _ _ _) -> True

TypedTerm t _ _ _ -> isPatternType t

TupleTerm ts _ -> all isPatternType ts

_ -> False

transPattern :: Env -> Set.Set String -> Set.Set String -> As.Term

-> Result (FunType, Isa.Term)

transPattern sign tyToks toks pat = do

ITC ty trm cs <- transTerm sign tyToks False toks Set.empty pat

case pat of

TupleTerm [] _ -> return (ty, mkFree "_")

_ -> if not (isPatternType pat) || isPartialVal ty

|| case cs of

None -> False

_ -> True then

fatal_error ("illegal pattern for Isabelle: " ++ showDoc pat "")

$ getRange pat

else return (ty, trm)

-- form Abs(pattern term)

abstraction :: Env -> Set.Set String -> Set.Set String

-> IsaTermCond -> As.Term -> Result IsaTermCond

abstraction sign tyToks toks (ITC ty body cs) pat = do

(pTy, nPat) <- transPattern sign tyToks toks pat

return $ ITC (FunType pTy ty) (Abs nPat body NotCont) cs