fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz{- |

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzModule : $Header$

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzDescription : translating a HasCASL subset to Isabelle

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzCopyright : (c) C. Maeder, DFKI 2008

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzMaintainer : Christian.Maeder@dfki.de

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzStability : provisional

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzPortability : portable

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzutility function for translation from HasCASL to Isabelle leaving open how

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzpartial values are interpreted

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-}

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzmodule Comorphisms.PPolyTyConsHOL2IsaUtils where

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.As as As

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.AsUtils

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Builtin

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.DataAna

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Le as Le

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Unify (substGen)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Isabelle.IsaSign as Isa

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Isabelle.IsaConsts

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Isabelle.Translate

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.DocUtils

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Id

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Result

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport qualified Data.Map as Map

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport qualified Data.Set as Set

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Lib.State

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.AS_Annotation

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.GlobalAnnotations

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savuimport Data.List (elemIndex)

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savuimport Data.Maybe (catMaybes, isNothing)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport Control.Monad (foldM)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumapTheory :: Simplifier -> (Env, [Named Le.Sentence])

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

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumapTheory simpF (env, sens) = do

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu let tyToks = typeToks env

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu sign <- transSignature env tyToks

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

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

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

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (\ ns -> case sentence ns of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu DatatypeSen ds -> ds

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> []) sens

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu return ( sign { domainTab = reverse dt }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , filter (\ ns -> sentence ns /= mkSen true) isens)

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu-- * Signature

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavubaseSign :: BaseSig

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavubaseSign = MainHC_thy

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutransAssumps :: GlobalAnnos -> Set.Set String -> Assumps -> Result ConstTab

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutransAssumps ga toks = foldM insertOps Map.empty . Map.toList where

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu insertOps m (name, ops) =

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu let chk = isPlainFunType

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in case map opType $ Set.toList ops of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu [TypeScheme _ op _ ] -> do

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu ty <- funType op

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu return $ Map.insert

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (mkIsaConstT (isPredType op) ga (chk ty)

3051a3502f027f3d7bb750a1d7a6b1b43cdd2a86Robert Savu name baseSign toks) (transPlainFunType ty) m

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

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ty <- funType op

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu return $ Map.insert

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (mkIsaConstIT (isPredType op) ga (chk ty)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu name i baseSign toks) (transPlainFunType ty) m'

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ) m $ zip [1..] infos

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

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

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavugetAssumpsToks :: Assumps -> Set.Set String

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavugetAssumpsToks = Map.foldWithKey (\ i ops s ->

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Set.union s $ Set.unions

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu $ zipWith (\ o _ -> getConstIsaToks i o baseSign) [1..]

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu $ Set.toList ops) Set.empty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutypeToks :: Env -> Set.Set String

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutypeToks =

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Set.map (\ tyId -> showIsaTypeT tyId baseSign) . Map.keysSet . typeMap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutransSignature :: Env -> Set.Set String -> Result Isa.Sign

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutransSignature env toks = do

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu let extractTypeName tyId typeInfo m =

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu let getTypeArgs n k = case k of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ClassKind _ -> []

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu FunKind _ _ r _ ->

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (TFree ("'a" ++ show n) [], [isaTerm])

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu : getTypeArgs (n + 1) r

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in Map.insert (showIsaTypeT tyId baseSign)

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

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

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu return $ Isa.emptySign

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu { baseSig = baseSign

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu -- translation of typeconstructors

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , tsig = emptyTypeSig

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu { arities = Map.foldWithKey extractTypeName Map.empty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (typeMap env) }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , constTab = ct }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- * translation of a type in an operation declaration

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuunitTyp :: Typ

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuunitTyp = Type "unit" holType []

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumkPartialType :: Typ -> Typ

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumkPartialType arg = Type "partial" [] [arg]

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavutransFunType :: 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 a)

$ map transFunType 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

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) ->

if n == 0 then 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

else if null tys then return $ TypeVar tid

else fatal_error "funType: no higher kinds" $ posOfId tid

_ -> fatal_error "funType: no 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) 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, 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

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

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

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

-> Result Isa.Sentence

transSentence sign tyToks simpF s = case s of

Le.Formula trm -> do

(ty, t) <-

transTerm sign tyToks (getAssumpsToks $ assumps sign) Set.empty trm

case ty of

BoolType -> return $ mkSimplifiedSen simpF t

PartialVal _ ->

return $ mkSimplifiedSen simpF $ mkTermAppl partial2bool t

FunType _ _ -> error "transSentence: FunType"

PairType _ _ -> error "transSentence: PairType"

TupleType _ -> error "transSentence: TupleType"

ApplType _ _ -> error "transSentence: ApplType"

_ -> return $ mkSen true

DatatypeSen _ -> 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 case (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) of

Just str -> str

Nothing -> error $ "transOpId " ++ show op

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

-> ProgEq -> Result ((As.Term, Isa.Term), (FunType, Isa.Term))

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

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

p@(ty, _) <- transTerm sign tyToks 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 -> Set.Set String -> Set.Set VarDecl

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

transLetEqs sign tyToks toks pVars es = case es of

[] -> return (pVars, [])

e : r -> do

((pat, op), (ty, ot)) <- transLetEq sign tyToks toks pVars e

(newPVars, newEs) <- transLetEqs sign tyToks toks (if isPartialVal ty

then Set.insert (getQualVar pat) pVars

else pVars) r

return (newPVars, (op, ot) : 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 "noneOp"

whenElseOp :: Isa.Term

whenElseOp = conDouble "whenElseOp"

resOp :: Isa.Term

resOp = conDouble "resOp"

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

{- 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 -> Set.Set String -> Set.Set VarDecl

-> As.Term -> Result (FunType, Isa.Term)

transTerm sign tyToks toks pVars trm = case trm of

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

fTy <- funType t

return ( if Set.member vd pVars then makePartialVal fTy else fTy

, Isa.Free $ transVar toks var)

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

fTy <- funType ty

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

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

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

let cf = mkTermAppl (convFun $ instType fTy instfTy)

unCurry f = (fTy, termAppl uncurryOp $ con f)

return $ case () of

()

| opId == trueId -> (fTy, true)

| opId == falseId -> (fTy, false)

| opId == botId -> (fTy, noneOp)

| opId == andId -> unCurry conjV

| opId == orId -> unCurry disjV

| opId == implId -> unCurry implV

| opId == infixIf -> (fTy, ifImplOp)

| opId == eqvId -> unCurry eqV

| opId == exEq -> (instfTy, cf $ termAppl uncurryOp existEqualOp)

| opId == eqId -> (instfTy, cf $ termAppl uncurryOp strongEqualOp)

| opId == notId -> (fTy, notOp)

| opId == defId -> (instfTy, cf defOp)

| opId == whenElse -> (fTy, whenElseOp)

| opId == resId -> (fTy, resOp)

| otherwise -> (instfTy,

cf $ (for (isPlainFunType fTy - 1)

$ termAppl uncurryOp)

$ con $ transOpId sign tyToks opId ts)

QuantifiedTerm quan varDecls phi _ -> do

let qname = case quan of

Universal -> allS

Existential -> exS

Unique -> ex1S

quantify phi' gvd = case gvd of

GenVarDecl (VarDecl var _ _ _) ->

return $ termAppl (conDouble qname)

$ Abs (Isa.Free $ transVar toks var)

phi' NotCont

GenTypeVarDecl _ -> return phi'

(ty, psi) <- transTerm sign tyToks toks pVars phi

psiR <- foldM quantify psi $ reverse varDecls

return (ty, psiR)

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

LambdaTerm pats q body r -> do

p@(ty, _) <- transTerm sign tyToks toks pVars body

appendDiags $ case q of

Partial -> []

Total -> [Diag Warning

("partial lambda body in total abstraction: "

++ showDoc body "") r | isPartialVal ty]

foldM (abstraction sign tyToks toks) p $ reverse pats

LetTerm As.Let peqs body _ -> do

(nPVars, nEqs) <- transLetEqs sign tyToks toks pVars peqs

(bTy, bTrm) <- transTerm sign tyToks toks nPVars body

return (bTy, mkLetAppl nEqs bTrm)

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

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

return $ foldl1 ( \ (s, p) (t, e) ->

(PairType s t, Tuplex [p, e] NotCont)) nTs

TupleTerm [] _ -> return (UnitType, unitOp)

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

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

$ getRange trm

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

(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

MapFun mv cf -> MapFun mv $ invertConv cf

ResFun cf -> ResFun $ invertConv cf

ArgFun cf -> ArgFun $ invertConv cf

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

_ -> IdOp

data MapFun = MapFst | MapSnd | MapPartial

data LiftFun = LiftFst | LiftSnd

data ConvFun =

IdOp | ConstNil | ConstTrue | MkPartial | Bool2partial | Partial2bool

| CompFun ConvFun ConvFun

| MapFun MapFun ConvFun

| LiftFun LiftFun ConvFun

| LiftUnit FunType

| LiftPartial FunType

| ResFun ConvFun

| ArgFun ConvFun

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 :: ConvFun -> Isa.Term

convFun cvf = case cvf of

IdOp -> idOp

Bool2partial -> bool2partial

Partial2bool -> partial2bool

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 ->

mkTermAppl (mkTermAppl compOp $ convFun f1) $ convFun f2

ConstNil -> constNil

ConstTrue -> constTrue

MkPartial -> mkPartial

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

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

LiftFst -> mkTermAppl (mkTermAppl compOp

$ mkTermAppl (mkTermAppl compOp uncurryOp) flipOp)

$ mkTermAppl (mkTermAppl compOp

$ mkTermAppl (mkTermAppl compOp

$ mkTermAppl compOp ccv) flipOp) curryOp

LiftSnd -> mkTermAppl (mkTermAppl compOp uncurryOp) $

mkTermAppl (mkTermAppl compOp $ mkTermAppl compOp ccv)

curryOp

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

ResFun cv -> mkTermAppl compOp $ convFun cv

mapFst, mapSnd, mapPartial, idOp, bool2partial,

partial2bool, constNil, constTrue,

liftUnit2unit, liftUnit2bool, liftUnit2partial, liftUnit, lift2unit,

lift2bool, lift2partial, mkPartial :: Isa.Term

mapFst = conDouble "mapFst"

mapSnd = conDouble "mapSnd"

mapPartial = conDouble "mapPartial"

idOp = conDouble "id"

bool2partial = conDouble "bool2partial"

partial2bool = conDouble "partial2bool"

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"

existEqualOp :: Isa.Term

existEqualOp =

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

strongEqualOp :: Isa.Term

strongEqualOp =

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

unpackOp :: FunType -> Isa.Term

unpackOp ft = case ft of

UnitType -> conDouble "unpack2bool"

BoolType -> conDouble "unpackBool"

PartialVal _ -> conDouble "unpackPartial"

_ -> conDouble "unpack2partial"

-- 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))

(BoolType, PartialVal _) -> return ((False, IdOp), (aTy, Partial2bool))

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

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

(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 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"

applConv :: ConvFun -> Isa.Term -> Isa.Term

applConv cnv t = case cnv of

IdOp -> t

_ -> mkTermAppl (convFun cnv) t

mkArgFun :: ConvFun -> ConvFun

mkArgFun c = case c of

IdOp -> c

_ -> ArgFun c

mkResFun :: ConvFun -> ConvFun

mkResFun c = case c of

IdOp -> 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", "partial2bool", "bool2partial"]

-> Just (ft, la, ra)

_ -> Nothing

isLifted :: Isa.Term -> Bool

isLifted t = case t of

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

_ -> False

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", "strongEqualOp"] ->

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 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 _ | new ma == "True" -> af

| new ma == "False" -> false

_ -> If arg af false c

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

case arg of

Const ma _ | new ma == "True" -> af

| new ma == "False" -> noneOp

_ -> If arg af noneOp c

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

| new mp == "liftUnit2unit" -> arg

| new mp == "lift2unit" -> mkTermAppl (conDouble "partial2bool") 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 == "defOp" && new sm == "makePartial" -> true

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

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

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

| new d == "curryOp" && new sm == uncurryOpS -> a

(Const i _, _)

| new i == "bool2partial" ->

let tc = mkTermAppl mkPartial unitOp

in case arg of

Const j _ | new j == "True" -> tc

| new j == "False" -> 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 == "partial2bool" -> 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 :: Simplifier -> Isa.Term -> State Int Isa.Term

simplify simpF trm = case trm of

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

| elem (new l) ["lift2bool", "lift2partial", "mapPartial"] -> do

n <- freshIndex

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

nF <- simplify simpF $ mkTermAppl f pvar

nArg <- simplify simpF arg

simpF l pvar nF nArg

App f arg c -> do

nF <- simplify simpF f

nArg <- simplify simpF arg

return $ App nF nArg c

Abs v t c -> do

nT <- simplify simpF t

return $ Abs v nT c

_ -> return trm

mkApp :: Env -> Set.Set String -> Set.Set String -> Set.Set VarDecl -> As.Term

-> As.Term -> Result (FunType, Isa.Term)

mkApp sign tyToks toks pVars f arg = do

(fTy, fTrm) <- transTerm sign tyToks toks pVars f

(aTy, aTrm) <- transTerm sign tyToks toks pVars arg

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

TupleTerm [] _ -> return (fTy, fTrm)

_ -> mkError "wrong function type" f

case fTy of

FunType a r -> do

((rTy, fConv), (_, aConv)) <-

adjustPos (getRange [f, arg]) $ adjustTypes a r aTy

return (if rTy then makePartialVal r else r,

mkTermAppl (applConv fConv fTrm)

$ applConv aConv aTrm)

PartialVal (FunType a r) -> do

((_, fConv), (_, aConv)) <-

adjustPos (getRange [f, arg]) $ adjustTypes a r aTy

let resTy = makePartialVal r

return (resTy, mkTermAppl (mkTermAppl (mkTermAppl

(unpackOp r) $ convFun fConv) fTrm)

$ applConv aConv aTrm)

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

p@(ty, _) <- transTerm sign tyToks toks Set.empty pat

case pat of

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

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

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

$ getRange pat

else return p

-- form Abs(pattern term)

abstraction :: Env -> Set.Set String -> Set.Set String -> (FunType, Isa.Term)

-> As.Term -> Result (FunType, Isa.Term)

abstraction sign tyToks toks (ty, body) pat = do

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

return (FunType pTy ty, Abs nPat body NotCont)