PCoClTyConsHOL2IsabelleHOL.hs revision 81eaac399d69af15425d06b054e5d0331dbc132b
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederCopyright : (c) C. Maeder, DFKI 2006
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : maeder@tzi.de
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : non-portable (imports Logic.Logic)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederThe embedding comorphism from HasCASL to Isabelle-HOL.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedermodule Comorphisms.PCoClTyConsHOL2IsabelleHOL
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (PCoClTyConsHOL2IsabelleHOL(..)) where
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Common.Lib.Map as Map
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Common.Lib.Set as Set
989ba1f28e0846635a9f098bebbfbdfa9b1c5ed0Jonathan von Schroederimport Data.List (elemIndex)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Data.Maybe (catMaybes, isNothing)
90d97972167d142dde6ee8b18d9625332040261fJonathan von Schroeder-- | The identity of the comorphism
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederdata PCoClTyConsHOL2IsabelleHOL = PCoClTyConsHOL2IsabelleHOL deriving Show
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederinstance Language PCoClTyConsHOL2IsabelleHOL -- default definition is okay
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederinstance Comorphism PCoClTyConsHOL2IsabelleHOL
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder HasCASL Sublogic
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder BasicSpec Le.Sentence SymbItems SymbMapItems
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Symbol RawSymbol ()
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Isabelle () () Isa.Sentence () ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsabelleMorphism () () () where
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sourceLogic PCoClTyConsHOL2IsabelleHOL = HasCASL
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sourceSublogic PCoClTyConsHOL2IsabelleHOL = noSubtypes
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini targetLogic PCoClTyConsHOL2IsabelleHOL = Isabelle
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mapSublogic PCoClTyConsHOL2IsabelleHOL _ = ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini map_theory PCoClTyConsHOL2IsabelleHOL (env, sens) = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sign <- transSignature env
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder isens <- mapM (mapNamedM $ transSentence env) sens
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (dt, _, _) <- foldM (transDataEntries env) ([], Set.empty, Set.empty)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ filter (not . null) $ map
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ( \ ns -> case sentence ns of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini DatatypeSen ds -> ds
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> []) sens
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (sign { domainTab = reverse dt }, isens)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini map_morphism = mapDefaultMorphism
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini map_sentence PCoClTyConsHOL2IsabelleHOL sign phi =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini transSentence sign phi
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini map_symbol = errMapSymbol
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * Signature
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibaseSign :: BaseSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibaseSign = MainHC_thy
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransAssumps :: GlobalAnnos -> Assumps -> Result ConstTab
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransAssumps ga = foldM insertOps Map.empty . Map.toList where
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini insertOps m (name, ops) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let chk t = isPlainFunType t
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder in case opInfos ops of
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder ty <- transOpInfo info
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (mkIsaConstT False ga (chk ty)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini name baseSign) (transPlainFunType ty) m
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini infos -> foldM ( \ m' (i, info) -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ty <- transOpInfo info
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (mkIsaConstIT False ga (chk ty)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini name i baseSign) (transPlainFunType ty) m'
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ) m $ zip [1..] infos
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransSignature :: Env -> Result Isa.Sign
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransSignature env = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ct <- transAssumps (globAnnos env) $ assumps env
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let extractTypeName tyId typeInfo m =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let getTypeArgs n k = case k of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ClassKind _ -> []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini FunKind _ _ r _ ->
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (TFree ("'a" ++ show n) [], [isaTerm])
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder : getTypeArgs (n + 1) r
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini in Map.insert (showIsaTypeT tyId baseSign)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [(isaTerm, getTypeArgs (1 :: Int) $ typeKind typeInfo)] m
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. Schulze { baseSig = baseSign
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. Schulze -- translation of typeconstructors
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , tsig = emptyTypeSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini { arities = Map.foldWithKey extractTypeName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (typeMap env) }
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , constTab = ct }
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * translation of a type in an operation declaration
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly-- extract type from OpInfo
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillytransOpInfo :: OpInfo -> Result FunType
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillytransOpInfo oi = case opType oi of
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly TypeScheme _ op _ -> funType op
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyunitTyp :: Typ
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyunitTyp = Type "unit" holType []
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillytransType :: Type -> Result Typ
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillytransType = fmap transPlainFunType . funType
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillytransFunType :: FunType -> Typ
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillytransFunType fty = case fty of
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly UnitType -> unitTyp
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly BoolType -> boolType
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly FunType f a -> mkFunType (transFunType f) $ transFunType a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PartialVal a -> mkOptionType $ transFunType a
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder PairType a b -> prodType (transFunType a) $ transFunType b
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder TupleType l -> transFunType $ foldl1 PairType l
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ApplType tid args -> Type (showIsaTypeT tid baseSign) []
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $ map transFunType args
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TypeVar tid -> TFree (showIsaTypeT tid baseSign) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- compute number of arguments for plain CASL functions
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisPlainFunType :: FunType -> Int
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisPlainFunType fty = case fty of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FunType f a -> case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FunType _ _ -> -1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> case f of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TupleType l -> length l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransPlainFunType :: FunType -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransPlainFunType fty =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FunType (TupleType l) a -> case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FunType _ _ -> transFunType fty
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> foldr mkFunType (transFunType a)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ map transFunType l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> transFunType fty
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata FunType = UnitType | BoolType | FunType FunType FunType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | PartialVal FunType | PairType FunType FunType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | TupleType [FunType]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | ApplType Id [FunType] | TypeVar Id
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisPartialVal :: FunType -> Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisPartialVal t = case t of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PartialVal _ -> True
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini BoolType -> True
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimakePartialVal :: FunType -> FunType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimakePartialVal t = if isPartialVal t then t else case t of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini UnitType -> BoolType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> PartialVal t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifunType :: Type -> Result FunType
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederfunType t = case getTypeAppl t of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (TypeName tid _ n, tys) ->
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder if n == 0 then do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ftys <- mapM funType tys
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return $ case ftys of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [] | tid == unitTypeId -> UnitType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [ty] | tid == lazyTypeId -> makePartialVal ty
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [t1, t2] | isArrow tid -> FunType t1 $
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini if isPartialArrow tid then makePartialVal t2 else t2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (_ : _ : _) | isProductId tid -> TupleType ftys
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini _ -> ApplType tid ftys
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini else if null tys then return $ TypeVar tid
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini else fatal_error "funType: no higher kinds" $ posOfId tid
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> fatal_error "funType: no type appl" $ getRange t
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * translation of a datatype declaration
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaedertransDataEntries :: Env -> (DomainTab, Set.Set TName, Set.Set VName)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> [DataEntry] -> Result (DomainTab, Set.Set TName, Set.Set VName)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransDataEntries env t@(dt, tys, cs) l = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let rs = map (transDataEntry env) l
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder ms = map maybeResult rs
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder toWarning = map ( \ d -> d { diagKind = Warning })
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder appendDiags $ toWarning $ concatMap diags rs
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder if any isNothing ms then return t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let des = catMaybes ms
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder ntys = map (Isa.typeId . fst) des
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder ncs = concatMap (map fst . snd) des
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder foldF str cnv = foldM ( \ s i ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini fail $ "duplicate " ++ str ++ cnv i
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder else return $ Set.insert i s)
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder Result d1 mrtys = foldF "datatype " id tys ntys
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder Result d2 mrcs = foldF "constructor " new cs ncs
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini appendDiags $ toWarning $ d1 ++ d2
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini case (mrtys, mrcs) of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder (Just rtys, Just rcs) -> return (des : dt, rtys, rcs)
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder _ -> return t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- datatype with name (tyId) + args (tyArgs) and alternatives
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitransDataEntry :: Env -> DataEntry -> Result DomainEntry
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedertransDataEntry env (DataEntry tm tyId gk tyArgs rk alts) =
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let i = Map.findWithDefault tyId tyId tm
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini dt = patToType i tyArgs rk
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder in case gk of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder nalts <- mapM (transAltDefn env tm tyArgs dt i) alts
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let transDName ti ta = Type (showIsaTypeT ti baseSign) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ map transTypeArg ta
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder return (transDName i tyArgs, nalts)
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder _ -> fatal_error ("not a free type: " ++ show i)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- arguments of a datatype's typeconstructor
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedertransTypeArg :: TypeArg -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedertransTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransAltDefn :: Env -> IdMap -> [TypeArg] -> Type -> Id -> AltDefn
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -> Result (VName, [Typ])
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedertransAltDefn env tm args dt tyId alt = case alt of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder Construct (Just opId) ts Total _ -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let mTs = map (mapType tm) ts
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sc = TypeScheme args (getFunType dt Total mTs) nullRange
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder nts <- mapM funType mTs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- extract overloaded opId number
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder return (transOpId env opId sc, case nts of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [TupleType l] -> map transFunType l
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini _ -> map transFunType nts)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini _ -> fatal_error ("not a total constructor: " ++ show tyId)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini $ posOfId tyId
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- simple variables
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitransVar :: Var -> VName
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedertransVar v = mkVName $ showIsaConstT v baseSign
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedertransSentence :: Env -> Le.Sentence -> Result Isa.Sentence
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitransSentence sign s = case s of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder (ty, t) <- transTerm sign trm
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini BoolType -> return $ mkSen t
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder PartialVal _ -> return $ mkSen $ mkTermAppl option2bool t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FunType _ _ -> error "transSentence: FunType"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PairType _ _ -> error "transSentence: PairType"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TupleType _ -> error "transSentence: TupleType"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ApplType _ _ -> error "transSentence: ApplType"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> return $ mkSen true
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini DatatypeSen _ -> return $ mkSen true
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ProgEqSen _ _ (ProgEq _ _ r) -> warning (mkSen true)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini "translation of sentence not implemented"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- disambiguate operation names
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaedertransOpId :: Env -> UninstOpId -> TypeScheme -> VName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedertransOpId sign op ts@(TypeScheme _ ty _) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let ga = globAnnos sign
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder Result _ mty = funType ty
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in case mty of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> error "transOpId"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let args = isPlainFunType fty
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ops <- Map.lookup op (assumps sign)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder if isSingle (opInfos ops) then return $
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mkIsaConstT False ga args op baseSign
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder else do i <- elemIndex ts (map opType (opInfos ops))
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder return $ mkIsaConstIT False ga args op (i+1) baseSign) of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Just str -> str
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Nothing -> error $ "transOpId " ++ showIsaConstT op baseSign
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedertransProgEq :: Env -> ProgEq -> Result (Isa.Term, Isa.Term)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedertransProgEq sign (ProgEq pat trm r) = do
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder op <- transPattern sign pat
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (ty, ot) <- transTerm sign trm
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder if isPartialVal ty then fatal_error
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder ("rhs must not be partial currently: " ++ showDoc trm "") r
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder else return (op, ot)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederifImplOp = conDouble "ifImplOp"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederunitOp = Tuplex [] NotCont
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedernoneOp = conDouble "None"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederexEqualOp = conDouble "exEqualOp"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederwhenElseOp = conDouble "whenElseOp"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniuncurryOpS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniuncurryOpS = "uncurryOp"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederuncurryOp = conDouble uncurryOpS
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maederfor :: Int -> (a -> a) -> a -> a
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederfor n f a = if n <= 0 then a else for (n - 1) f $ f a
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedertransTerm :: Env -> As.Term -> Result (FunType, Isa.Term)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedertransTerm sign trm = case trm of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder QualVar (VarDecl var t _ _) -> do
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder fTy <- funType t
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder return (fTy, Isa.Free (transVar var) $ transFunType fTy)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder QualOp _ (InstOpId opId is _) ts@(TypeScheme targs ty _) _ -> do
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder fTy <- funType ty
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder instfTy <- funType $ subst (if null is then Map.empty else
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Map.fromList $ zipWith (\ (TypeArg _ _ _ _ i _ _) t
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder -> (i, t)) targs is) ty
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let cf = mkTermAppl (convFun $ instType fTy instfTy)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder unCurry f = (fTy, termAppl uncurryOp $ con f)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder return $ case () of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | opId == trueId -> (fTy, true)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == falseId -> (fTy, false)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == botId -> (fTy, noneOp)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == andId -> unCurry conjV
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | opId == orId -> unCurry disjV
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == implId -> unCurry implV
a2e8cca8a8217b158b0b7a760e8234c03186456dChristian Maeder | opId == infixIf -> (fTy, ifImplOp)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == eqvId -> unCurry eqV
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | opId == exEq -> (fTy, exEqualOp)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == eqId -> (instfTy, cf $ termAppl uncurryOp $ con eqV)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == notId -> (fTy, notOp)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder | opId == defId -> (instfTy, cf $ defOp)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | opId == whenElse -> (fTy, whenElseOp)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | otherwise -> (instfTy,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini cf $ (for (isPlainFunType fTy - 1)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ termAppl uncurryOp)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ con $ transOpId sign opId ts)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder QuantifiedTerm quan varDecls phi _ -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let qname = case quan of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Universal -> allS
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder Existential -> exS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Unique -> ex1S
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini quantify phi' gvd = case gvd of
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder GenVarDecl (VarDecl var typ _ _) -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ty <- transType typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return $ termAppl (conDouble $ qname)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder $ Abs (con $ transVar var)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ty phi' NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder GenTypeVarDecl _ -> return phi'
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder (ty, psi) <- transTerm sign phi
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini psiR <- foldM quantify psi $ reverse varDecls
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (ty, psiR)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TypedTerm t _q _ty _ -> transTerm sign t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini LambdaTerm pats q body r -> do
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder p@(ty, _) <- transTerm sign body
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder pt <- case q of
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder Partial -> return p
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian Maeder Total -> if isPartialVal ty
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then fatal_error
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ("partial lambda body in total abstraction: "
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ++ showDoc body "") r
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else return p
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini foldM (abstraction sign) pt $ reverse pats
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder LetTerm As.Let peqs body _ -> do
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (bTy, bTrm) <- transTerm sign body
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder nEqs <- mapM (transProgEq sign) peqs
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly return (bTy, Isa.Let nEqs bTrm)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly TupleTerm ts@(_ : _) _ -> do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly nTs <- mapM (transTerm sign) ts
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return $ foldl1 ( \ (s, p) (t, e) ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (PairType s t, Tuplex [p, e] NotCont)) nTs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TupleTerm [] _ -> return (UnitType, unitOp)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ApplTerm t1 t2 _ -> mkApp sign t1 t2 -- transAppl sign Nothing t1 t2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> fatal_error ("cannot translate term: " ++ showDoc trm "")
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly $ getRange trm
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyinstType :: FunType -> FunType -> ConvFun
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyinstType f1 f2 = case (f1, f2) of
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (TupleType l1, _) -> instType (foldl1 PairType l1) f2
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (_, TupleType l2) -> instType f1 $ foldl1 PairType l2
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder (PartialVal (TypeVar _), BoolType) -> Option2bool
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (PairType a c, PairType b d) ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let c2 = instType c d
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini c1 = instType a b
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in mkCompFun (mkMapFun MapSnd c2) $ mkMapFun MapFst c1
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder (FunType a c, FunType b d) ->
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder let c2 = instType c d
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder c1 = instType a b
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in mkCompFun (mkResFun c2) $ mkArgFun $ invertConv c1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniinvertConv :: ConvFun -> ConvFun
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederinvertConv c = case c of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Option2bool -> Bool2option
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder MapFun mv cf -> MapFun mv $ invertConv cf
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ResFun cf -> ResFun $ invertConv cf
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ArgFun cf -> ArgFun $ invertConv cf
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder CompFun c1 c2 -> CompFun (invertConv c2) (invertConv c1)
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederdata MapFun = MapFst | MapSnd | MapSome
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata LiftFun = LiftFst | LiftSnd
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederdata ConvFun = IdOp | CompFun ConvFun ConvFun | ConstNil | ConstTrue | SomeOp
ec59d0f6f0e61272419be22982155bde741bf5b3Jonathan von Schroeder | MapFun MapFun ConvFun | LiftFun LiftFun ConvFun
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | LiftUnit FunType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | LiftSome FunType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | ResFun ConvFun | ArgFun ConvFun | Bool2option | Option2bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisNotIdOp :: ConvFun -> Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisNotIdOp f = case f of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IdOp -> False
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedermkCompFun :: ConvFun -> ConvFun -> ConvFun
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkCompFun f1 f2 = case f1 of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> case f2 of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini _ -> CompFun f1 f2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkMapFun :: MapFun -> ConvFun -> ConvFun
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkMapFun m f = case f of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini _ -> MapFun m f
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkLiftFun :: LiftFun -> ConvFun -> ConvFun
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkLiftFun lv c = case c of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini _ -> LiftFun lv c
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftFun :: LiftFun -> Isa.Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftFun lf = case lf of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini LiftFst -> liftFst
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini LiftSnd -> liftSnd
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimapFun :: MapFun -> Isa.Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimapFun mf = case mf of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini MapFst -> mapFst
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini MapSnd -> mapSnd
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini MapSome -> mapSome
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompOp = con compV
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconvFun :: ConvFun -> Isa.Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconvFun cvf = case cvf of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Bool2option -> bool2option
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Option2bool -> option2bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini LiftUnit rTy -> case rTy of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini UnitType -> liftUnit2unit
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini BoolType -> liftUnit2bool
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder PartialVal _ -> liftUnit2option
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> liftUnit
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini LiftSome rTy ->
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder UnitType -> lift2unit
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder BoolType -> lift2bool
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder PartialVal _ -> lift2option
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini CompFun f1 f2 ->
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder mkTermAppl (mkTermAppl compOp $ convFun f1) $ convFun f2
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini ConstNil -> constNil
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ConstTrue -> constTrue
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder SomeOp -> conSome
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini MapFun mf cv -> mkTermAppl (mapFun mf) $ convFun cv
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini LiftFun lf cv -> mkTermAppl (liftFun lf) $ convFun cv
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ArgFun cv -> mkTermAppl (termAppl flipOp compOp) $ convFun cv
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ResFun cv -> mkTermAppl compOp $ convFun cv
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederliftFst, liftSnd, mapFst, mapSnd, mapSome, idOp, bool2option,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini option2bool, constNil, constTrue,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini liftUnit2unit, liftUnit2bool, liftUnit2option, liftUnit, lift2unit,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini lift2bool, lift2option, lift :: Isa.Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftFst = conDouble "liftFst"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederliftSnd = conDouble "liftSnd"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimapFst = conDouble "mapFst"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimapSnd = conDouble "mapSnd"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimapSome = conDouble "mapSome"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniidOp = conDouble "id"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinibool2option = conDouble "bool2option"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinioption2bool = conDouble "option2bool"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconstNil = conDouble "constNil"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconstTrue = conDouble "constTrue"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftUnit2unit = conDouble "liftUnit2unit"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftUnit2bool = conDouble "liftUnit2bool"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftUnit2option = conDouble "liftUnit2option"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftUnit = conDouble "liftUnit"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinilift2unit = conDouble "lift2unit"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinilift2bool = conDouble "lift2bool"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinilift2option = conDouble "lift2option"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederlift = conDouble "mapSome"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniunpackOp :: FunType -> Isa.Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederunpackOp ft = case ft of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini UnitType -> conDouble "unpack2bool"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini BoolType -> conDouble "unpackBool"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PartialVal _ -> conDouble "unpackOption"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> conDouble "unpack2option"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- True means require result type to be partial
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniadjustTypes :: FunType -> FunType -> FunType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> Result ((Bool, ConvFun), (FunType, ConvFun))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniadjustTypes aTy rTy ty = case (aTy, ty) of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (TupleType l, _) -> adjustTypes (foldl1 PairType l) rTy ty
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini (_, TupleType l) -> adjustTypes aTy rTy $ foldl1 PairType l
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (BoolType, BoolType) -> return ((False, IdOp), (ty, IdOp))
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (UnitType, UnitType) -> return ((False, IdOp), (ty, IdOp))
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder (PartialVal _, BoolType) -> return ((False, IdOp), (aTy, Bool2option))
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (BoolType, PartialVal _) -> return ((False, IdOp), (aTy, Option2bool))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (_, BoolType) -> return ((True, LiftUnit rTy), (ty, IdOp))
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (BoolType, _) -> return ((False, IdOp), (aTy, ConstTrue))
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder (PartialVal a, PartialVal b) -> do
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder q@(fp, (argTy, aTrm)) <- adjustTypes a rTy b
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return $ case argTy of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PartialVal _ -> q
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> (fp, (PartialVal argTy, mkMapFun MapSome aTrm))
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (a, PartialVal b) -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini q@(_, ap@(argTy, _)) <- adjustTypes a rTy b
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder return $ case argTy of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PartialVal _ -> q
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> ((True, LiftSome rTy), ap)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (PartialVal a, b) -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini q@(fp, (argTy, aTrm)) <- adjustTypes a rTy b
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return $ case argTy of
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder PartialVal _ -> q
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder _ -> (fp, (PartialVal argTy, mkCompFun SomeOp aTrm))
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (PairType a c, PairType b d) -> do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ((res2Ty, f2), (arg2Ty, a2)) <- adjustTypes c rTy d
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ((res1Ty, f1), (arg1Ty, a1)) <- adjustTypes a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (if res2Ty then makePartialVal rTy else rTy) b
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder return $ ((res1Ty || res2Ty,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mkCompFun (mkLiftFun LiftFst f1) $ mkLiftFun LiftSnd f2),
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (PairType arg1Ty arg2Ty,
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder mkCompFun (mkMapFun MapSnd a2) $ mkMapFun MapFst a1))
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian Maeder (FunType a c, FunType b d) -> do
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder ((_, aF), (aT, aC)) <- adjustTypes b c a
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder ((cB, cF), (dT, dC)) <- adjustTypes c rTy d
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian Maeder if cB || isNotIdOp cF
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder then fail "cannot adjust result types of function type"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder else return ((False, IdOp),
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (FunType aT dT,
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder mkCompFun aF $ mkCompFun (mkResFun dC) $ mkArgFun aC))
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (TypeVar _, _) -> return ((False, IdOp), (ty, IdOp))
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian Maeder (_, TypeVar _) -> return ((False, IdOp), (aTy, IdOp))
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (ApplType i1 l1, ApplType i2 l2) | i1 == i2 && length l1 == length l2
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder -> do l <- mapM (\ (a, b) -> adjustTypes a rTy b) $ zip l1 l2
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder if or (map (fst . fst) l) || or
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (map (isNotIdOp . snd . snd) l)
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder then fail "cannot adjust type application"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder else return ((False, IdOp),
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (ApplType i1 $ map (fst . snd) l, IdOp))
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder _ -> fail "cannot adjust types"
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorriniapplConv cnv t = case cnv of
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini _ -> mkTermAppl (convFun cnv) t
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinimkArgFun :: ConvFun -> ConvFun
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinimkArgFun c = case c of
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder _ -> ArgFun c
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedermkResFun :: ConvFun -> ConvFun
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedermkResFun c = case c of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> ResFun c
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisEquallyLifted :: Isa.Term -> Isa.Term -> Maybe (Isa.Term, Isa.Term, Isa.Term)
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. SchulzeisEquallyLifted l r = case (l, r) of
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. Schulze (App ft@(Const f _) la _,
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. Schulze App (Const g _) ra _)
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder | f == g && elem (new f) [someS, "option2bool", "bool2option"]
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder -> Just (ft, la, ra)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederisLifted :: Isa.Term -> Bool
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisLifted t = case t of
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly App (Const f _) _ _ | new f == someS -> True
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederflipOp = conDouble "flip"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkTermAppl fun arg = case (fun, arg) of
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (App (Const uc _) b _, Tuplex [l, r] _)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly | new uc == uncurryOpS
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -> case (isEquallyLifted l r, b) of
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (Just (_, la, ra), Const bin _) | new bin == eq ->
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder mkTermAppl (mkTermAppl b la) ra
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder _ -> mkTermAppl (mkTermAppl b l) r
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (App (Const mp _) f _, Tuplex [a, b] c)
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder | new mp == "mapFst" -> Tuplex [mkTermAppl f a, b] c
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder | new mp == "mapSnd" -> Tuplex [a, mkTermAppl f b] c
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (App (Const mp1 _) f _, App u@(Const mp2 _) g _)
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder | new mp1 == "liftSnd" && new mp2 == uncurryOpS ->
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder mkTermAppl (mkTermAppl (conDouble "liftCurSnd") f) g
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder | new mp1 == "liftFst" && new mp2 == uncurryOpS ->
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder mkTermAppl (mkTermAppl (conDouble "liftCurFst") f) g
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (Const mp _, Tuplex [a, b] _)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder | new mp == "ifImplOp" -> binImpl b a
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new mp == "exEqualOp" && (isLifted a || isLifted b) ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder mkTermAppl (mkTermAppl uncurryOp (con eqV)) arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Const mp _, Tuplex [Tuplex [a, b] _, c] d)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new mp == "whenElseOp" -> case isEquallyLifted a c of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Just (f, na, nc) -> mkTermAppl f $ If b na nc d
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Nothing -> If b a c d
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (App (Const mp _) f c, _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new mp == "liftUnit2bool" -> let af = mkTermAppl f unitOp in
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Const ma _ | new ma == "True" -> af
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new ma == "False" -> false
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> If arg af false c
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new mp == "liftUnit2option" -> let af = mkTermAppl f unitOp in
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Const ma _ | new ma == "True" -> af
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new ma == "False" -> noneOp
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> If arg af noneOp c
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (App (Const mp _) _ _, _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new mp == "liftUnit2unit" -> arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new mp == "lift2unit" -> mkTermAppl (conDouble "option2bool") arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (App (App (Const cmp _) f _) g c, _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new cmp == compS -> mkTermAppl f $ mkTermAppl g arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new cmp == "curryOp" -> mkTermAppl f $ Tuplex [g, arg] c
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new cmp == "flip" -> mkTermAppl (mkTermAppl f arg) g
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (App (App (Const cmp _) f _) g _, _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new cmp == "liftCurFst" ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder termAppl (termAppl compOp $ termAppl (termAppl flipOp f) arg)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $ termAppl flipOp g
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new cmp == "liftCurSnd" ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder mkTermAppl f $ mkTermAppl g arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Const d _, App (Const sm _) a _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new d == "defOp" && new sm == someS -> true
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new d == "option2bool" && new sm == someS -> true
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new d == "option2bool" && new sm == "bool2option"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder || new d == "bool2option" && new sm == "option2bool" -> a
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new d == "curryOp" && new sm == uncurryOpS -> a
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Const i _, _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new i == "bool2option" ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let tc = mkTermAppl conSome $ unitOp
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder in case arg of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Const j _ | new j == "True" -> tc
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new j == "False" -> noneOp
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> termAppl fun arg -- If arg tc noneOp NotCont
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new i == "id" -> arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new i == "constTrue" -> true
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new i == "constNil" -> unitOp
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Const i _, Tuplex [] _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | new i == "option2bool" -> false
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> termAppl fun arg
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedermkApp :: Env -> As.Term -> As.Term -> Result (FunType, Isa.Term)
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedermkApp sg f arg = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (fTy, fTrm) <- transTerm sg f
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (aTy, aTrm) <- transTerm sg arg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder FunType a r -> do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ((rTy, fConv), (_, aConv)) <- adjustTypes a r aTy
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return $ (if rTy then makePartialVal r else r,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder mkTermAppl (applConv fConv fTrm)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $ applConv aConv aTrm)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder PartialVal (FunType a r) -> do
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'Reilly ((_, fConv), (_, aConv)) <- adjustTypes a r aTy
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'Reilly let resTy = makePartialVal r
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'Reilly return (resTy, mkTermAppl (mkTermAppl (mkTermAppl
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (unpackOp r) $ convFun fConv) fTrm)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $ applConv aConv aTrm)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> fail "not a function type"
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'Reilly-- * translation of lambda abstractions
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedergetPatternType :: As.Term -> Result FunType
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedergetPatternType t =
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder QualVar (VarDecl _ typ _ _) -> funType typ
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder TypedTerm _ _ typ _ -> funType typ
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder TupleTerm ts _ -> do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ptys <- mapM getPatternType ts
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return $ foldl1 PairType ptys
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder _ -> fatal_error ("not a pattern for Isabelle: " ++ showDoc t "")
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedertransPattern :: Env -> As.Term -> Result Isa.Term
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedertransPattern sign pat = do
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder (ty, trm) <- transTerm sign pat
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder if isPartialVal ty then
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder fatal_error ("pattern must not be partial: " ++ showDoc pat "")
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $ getRange pat
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder else return trm
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- form Abs(pattern term)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederabstraction :: Env -> (FunType, Isa.Term) -> As.Term
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -> Result (FunType, Isa.Term)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederabstraction sign (ty, body) pat = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder pTy <- getPatternType pat
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder nPat <- transPattern sign pat
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (FunType pTy ty, Abs nPat (transFunType pTy) body NotCont)