4358N/ADescription : translating a HasCASL subset to Isabelle
4358N/ACopyright : (c) C. Maeder, DFKI 2008
0N/AMaintainer : Christian.Maeder@dfki.de
0N/AStability : provisional
0N/Autility function for translation from HasCASL to Isabelle leaving open how
0N/Apartial values are interpreted
0N/AmapTheory simK simpF (env, sens) = do
0N/A let tyToks = typeToks env
0N/A sign <- transSignature env tyToks
0N/A isens <- mapM (mapNamedM $ transSentence env tyToks simK simpF) sens
0N/A (dt, _, _) <- foldM (transDataEntries env tyToks)
0N/A (\ ns -> case sentence ns of
0N/A DatatypeSen ds -> ds
0N/A return ( sign { domainTab = reverse dt }
0N/A , filter ((/= mkSen true) . sentence) isens)
0N/AbaseSign = MainHC_thy
0N/AtransAssumps :: GlobalAnnos ->
Set.Set String -> Assumps -> Result ConstTab
0N/A insertOps m (name, ops) =
0N/A [TypeScheme _ op _ ] -> do
0N/A (mkIsaConstT (isPredType op) ga (chk ty)
0N/A name baseSign toks) (transPlainFunType ty) m
0N/A infos -> foldM ( \ m' (TypeScheme _ op _, i) -> do
0N/A (mkIsaConstIT (isPredType op) ga (chk ty)
0N/A name i baseSign toks) (transPlainFunType ty) m'
0N/A-- all possible tokens of mixfix identifiers that must not be used as variables
0N/A $ map (\ (_, o) -> getConstIsaToks i o baseSign)
0N/AtransSignature env toks = do
0N/A let extractTypeName tyId typeInfo m =
0N/A let getTypeArgs n k = case k of
0N/A (TFree ("'a" ++ show n) [], holType)
0N/A : getTypeArgs (n + 1) r
0N/A [(isaTerm, getTypeArgs (1 :: Int) $ typeKind typeInfo)] m
0N/A ct <- transAssumps (globAnnos env) toks $ assumps env
0N/A { baseSig = baseSign
0N/A -- translation of typeconstructors
0N/A , tsig = emptyTypeSig
0N/A-- * translation of a type in an operation declaration
0N/AunitTyp = Type "unit" holType []
0N/AmkPartialType :: Typ -> Typ
0N/AmkPartialType arg = Type "partial" [] [arg]
0N/AtransFunType :: FunType -> Typ
0N/AtransFunType fty = case fty of
0N/A BoolType -> boolType
0N/A FunType f a -> mkFunType (transFunType f) $ transFunType a
0N/A PartialVal a -> mkPartialType $ transFunType a
0N/A PairType a b -> prodType (transFunType a) $ transFunType b
0N/A TupleType l -> case l of
0N/A [] -> error "transFunType"
0N/A _ -> transFunType $ foldl1 PairType l
0N/A ApplType tid args -> Type (showIsaTypeT tid baseSign) []
0N/A $ map transFunType args
0N/A TypeVar tid -> TFree (showIsaTypeT tid baseSign) []
0N/A-- compute number of arguments for plain CASL functions
0N/AisPlainFunType :: FunType -> Int
0N/AisPlainFunType fty = case fty of
0N/A FunType f a -> case a of
0N/A TupleType l -> length l
0N/AtransPlainFunType :: FunType -> Typ
0N/AtransPlainFunType fty =
0N/A FunType (TupleType l) a -> case a of
0N/A FunType _ _ -> transFunType fty
0N/A _ -> foldr (mkFunType . transFunType) (transFunType a) l
0N/Adata FunType = UnitType | BoolType
0N/A | FunType FunType FunType
0N/A | PartialVal FunType
0N/A | PairType FunType FunType -- only used to represent tuples as nested pairs
0N/A | TupleType [FunType]
0N/A | ApplType Id [FunType]
0N/AisPartialVal :: FunType -> Bool
0N/AisPartialVal t = case t of
0N/A PartialVal _ -> True
0N/AmakePartialVal :: FunType -> FunType
0N/AmakePartialVal t = if isPartialVal t then t else case t of
0N/A UnitType -> BoolType
0N/AfunType :: Type -> Result FunType
0N/AfunType t = case getTypeAppl t of
0N/A (TypeName tid _ n, tys)
0N/A ftys <- mapM funType tys
0N/A return $ case ftys of
0N/A [] | tid == unitTypeId -> UnitType
0N/A [ty] | tid == lazyTypeId -> makePartialVal ty
0N/A [t1, t2] | isArrow tid -> FunType t1 $
0N/A if isPartialArrow tid then makePartialVal t2 else t2
0N/A (_ : _ : _) | isProductId tid -> TupleType ftys
0N/A _ -> ApplType tid ftys
0N/A | null tys -> return $ TypeVar tid
0N/A _ -> fatal_error "funType: no flat type appl" $ getRange t
0N/A-- * translation of a datatype declaration
0N/AtransDataEntries env tyToks t@(dt, tys, cs) l = do
0N/A let rs = map (transDataEntry env tyToks) l
0N/A ms = map maybeResult rs
0N/A toWarning = map ( \ d -> d { diagKind = Warning })
0N/A appendDiags $ toWarning $ concatMap diags rs
0N/A if any isNothing ms then return t
0N/A let des = catMaybes ms
0N/A ncs = concatMap (map fst . snd) des
0N/A foldF str cnv = foldM ( \ s i ->
0N/A fail $ "duplicate " ++ str ++ cnv i
0N/A Result d1 mrtys = foldF "datatype " id tys ntys
0N/A Result d2 mrcs = foldF "constructor " new cs ncs
0N/A appendDiags $ toWarning $ d1 ++ d2
0N/A case (mrtys, mrcs) of
0N/A (Just rtys, Just rcs) -> return (des : dt, rtys, rcs)
0N/A-- datatype with name (tyId) + args (tyArgs) and alternatives
0N/AtransDataEntry :: Env ->
Set.Set String -> DataEntry -> Result DomainEntry
0N/AtransDataEntry env tyToks de@(DataEntry _ _ gk _ _ alts) =
0N/A let dp@(DataPat _ i tyArgs _ _) = toDataPat de
0N/A let transDName ti = Type (showIsaTypeT ti baseSign) []
0N/A return (transDName i tyArgs, nalts)
0N/A _ -> fatal_error ("not a free type: " ++ show i)
0N/A-- arguments of a datatype's typeconstructor
0N/AtransTypeArg :: TypeArg -> Typ
0N/AtransTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []
0N/A -> Result (VName, [Typ])
0N/AtransAltDefn env tyToks dp alt = case alt of
0N/A Construct mi ts p _ -> case mi of
0N/A Just opId -> case p of
0N/A let sc = getConstrScheme dp p ts
0N/A nts <- mapM funType ts
0N/A -- extract overloaded opId number
0N/A return (transOpId env tyToks opId sc, case nts of
0N/A [TupleType l] -> map transFunType l
0N/A _ -> map transFunType nts)
0N/A Partial -> mkError "not a total constructor" opId
0N/A Nothing -> mkError "no support for data subtypes" ts
0N/AtransVar toks v = let
4358N/A s = showIsaConstT v baseSign
0N/A in mkVName $ renVar s
0N/AmkTypedConst v fTy =
Isa.Const v $ Disp (transFunType fTy) NA Nothing
0N/AtransTypedVar toks (VarDecl var ty _ _) = do
0N/A return $ mkTypedConst (transVar toks var) fTy
0N/AmkSimplifiedSen simK simpF t = mkSen $ evalState (simplify simK simpF t) 0
0N/A Const n _ -> new n == cTrue
0N/AmkBinConj t1 t2 = case isTrue of
0N/Adata OldSimpKind = NoSimpLift | Lift2Restrict | Lift2Case deriving Eq
data SimpKind = New | Old OldSimpKind deriving Eq
transSentence sign tyToks simK simpF s = case s of
ITC ty t cs <- transTerm sign tyToks (simK == New)
(getAssumpsToks $ assumps sign)
Set.empty trm
PartialVal UnitType -> mkTermAppl defOp t
bt = if isTrue et then cond2bool cs else
mkTermAppl (integrateCondInBool cs) et
st = mkSimplifiedSen (case simK of
New -> NoSimpLift) simpF bt
PartialVal _ -> return st
FunType _ _ -> error "transSentence: FunType"
PairType _ _ -> error "transSentence: PairType"
TupleType _ -> error "transSentence: TupleType"
ApplType _ _ -> error "transSentence: ApplType"
DatatypeSen ls -> if all (\ (DataEntry _ _ gk _ _ _) -> gk == Generated) ls
then transSentence sign tyToks simK simpF .
Le.Formula 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 _) =
Result _ mty = funType ty
Nothing -> error "transOpId"
let args = isPlainFunType fty
in fromMaybe (error $ "transOpId " ++ show op) $ do
if isSingleton ops then return $
mkIsaConstT (isPredType ty) ga args op baseSign tyToks
return $ mkIsaConstIT (isPredType ty)
ga args op (i + 1) baseSign tyToks
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: "
else return ((pat, op), p)
transLetEqs sign tyToks collectConds toks pVars es = case es of
((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 trm = case trm of
QualVar (VarDecl _ _ _ _) -> True
TypedTerm t _ _ _ -> isQualVar t
getQualVar trm = case trm of
TypedTerm t _ _ _ -> getQualVar t
ifImplOp = conDouble "ifImplOp"
unitOp = Tuplex [] NotCont
noneOp = conDouble "undefinedOp"
whenElseOp = conDouble "whenElseOp"
resOp = conDouble "resOp"
makeTotal = conDouble "makeTotal"
uncurryOp = conDouble uncurryOpS
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
Cond t -> show $ printTerm t
CondList l -> intercalate " & " $ map show l
PairCond p1 p2 -> '(' : shows p1 ", " ++ shows p2 ")"
joinCond :: Cond -> Cond -> Cond
in case toCs c1 ++ toCs c2 of
pairCond :: Cond -> Cond -> Cond
pairCond c1 c2 = case (c1, c2) of
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
transTerm sign tyToks collectConds toks pVars trm = case trm of
QualVar vd@(VarDecl v t _ _) -> do
let vt = con $ transVar toks v
return $ if
Set.member vd pVars then ITC (makePartialVal fTy) vt None
QualOp _ (PolyId opId _ _) ts@(TypeScheme targs ty _) insts _ _ -> do
instfTy <- funType $ substGen (if null insts then
Map.empty else
-> (i, t)) targs insts) ty
let cf = mkTermAppl (convFun None $ instType fTy instfTy)
unCurry f = let rf = termAppl uncurryOp $ con f in
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
ef = cf $ termAppl uncurryOp existEqualOp
ef = cf $ termAppl uncurryOp $ con eqV
| 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
isaId = transOpId sign tyToks opId ts
ef = cf $ for (isPlainFunType fTy - 1) (termAppl uncurryOp)
$ if elem opId [injName, projName] then
mkTypedConst isaId instfTy
QuantifiedTerm quan varDecls phi _ -> do
quantify phi' gvd = case gvd of
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
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
("partial lambda body in total abstraction: "
| isPartialVal ty || not (isTrue $ cond2bool ncs) ]
foldM (abstraction sign tyToks toks) (integrateCond p)
LetTerm
As.Let peqs body _ -> do
transLetEqs sign tyToks collectConds toks pVars peqs
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 "")
integrateCond :: IsaTermCond -> IsaTermCond
integrateCond (ITC ty trm cs) = if isTrue $ cond2bool cs then
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) ->
in mkCompFun (mkMapFun MapSnd c2) $ mkMapFun MapFst c1
(FunType a c, FunType b d) ->
in mkCompFun (mkResFun c2) $ mkArgFun $ invertConv c1
invertConv :: ConvFun -> ConvFun
Partial2bool _ -> Bool2partial False
Bool2partial _ -> Partial2bool False
Bool2unit -> Unit2bool False
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)
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 -}
| CompFun ConvFun ConvFun
| LiftFun LiftFun ConvFun
isNotIdOp :: ConvFun -> Bool
mkCompFun :: ConvFun -> ConvFun -> ConvFun
mkCompFun f1 f2 = case f1 of
mkMapFun :: MapFun -> ConvFun -> ConvFun
mkLiftFun :: LiftFun -> ConvFun -> ConvFun
mkLiftFun lv c = case c of
convFun cnd cvf = case cvf of
then metaComp bool2partial $ integrateCondInBool cnd
then metaComp (integrateCondInBool cnd) defOp
Bool2bool -> integrateCondInBool cnd
then metaComp (integrateCondInBool cnd) constTrue else constTrue
Partial2partial -> integrateCondInPartial cnd
then integrateCondInTotal cnd
LiftUnit rTy -> case rTy of
UnitType -> liftUnit2unit
BoolType -> liftUnit2bool
PartialVal _ -> liftUnit2partial
PartialVal _ -> lift2partial
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)
LiftSnd -> metaComp uncurryOp $ metaComp (mkTermAppl compOp ccv)
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.TermmapFst = conDouble "mapFst"
mapSnd = conDouble "mapSnd"
mapPartial = conDouble "mapPartial"
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"
con $ VName "existEqualOp" $ Just $ AltSyntax "(_ =e=/ _)" [50, 51] 50
integrateCondInBool c = let b = cond2bool c in
if isTrue b then idOp else mkTermAppl (con conjV) b
integrateCondInPartial :: Cond ->
Isa.TermintegrateCondInPartial c = let b = cond2bool c in
if isTrue b then idOp else
mkTermAppl (mkTermAppl flipOp restrict) b
metaComp = mkTermAppl . mkTermAppl compOp
integrateCondInTotal :: Cond ->
Isa.TermintegrateCondInTotal c = metaComp (integrateCondInPartial c) mkPartial
addCond = joinCond . Cond
cond2bool c = case nub $ condToList c of
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
return $ mkCompFun Partial2partial c
return $ mkCompFun MkTotal c
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"
_ -> fail $ "cannot adjust argument type\n" ++ show (aTy, ty)
unpackOp fTrm isPf pfTy ft fConv = let isaF = convFun None fConv in
(mkTermAppl (conDouble $ case if pfTy then makePartialVal ft else ft of
UnitType -> "unpack2bool"
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
_ -> (fp, (PartialVal argTy, mkMapFun MapPartial aTrm))
q@(_, ap@(argTy, _)) <- adjustTypes a rTy b
_ -> ((True, LiftPartial rTy), ap)
q@(fp, (argTy, aTrm)) <- adjustTypes a rTy b
_ -> (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),
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
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)
then (mkTermAppl makeTotal fTrm, addCond (mkTermAppl defOp fTrm) fCs)
return $ ITC rTy (mkTermAppl nftrm natrm) $ joinCond nfcs nacs
applConv cnv (t, c) = let
rt = mkTermAppl (convFun c cnv) t
Bool2partial b -> if b then rb else r
Partial2bool b -> if b then rb else r
Unit2bool b -> if b then rb else r
Bool2unit -> (rt, addCond t c)
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
PairCond p1 p2 -> (p1, p2)
(nt1, nc1) = applConv cv (t1, c1)
in (Tuplex [nt1, t2] NotCont, PairCond nc1 c2)
(nt2, nc2) = applConv cv (t2, c2)
in (Tuplex [t1, nt2] NotCont, PairCond c1 nc2)
mkArgFun :: ConvFun -> ConvFun
mkResFun :: ConvFun -> ConvFun
isEquallyLifted l r = case (l, r) of
(App ft@(Const f _) la _,
| f == g && elem (new f) ["makePartial", "bool2partial"]
App (Const f _) _ _ | new f == "makePartial" -> True
splitArg arg = case arg of
App (App (Const n _) p _) b _ | new n == "restrictOp" ->
App (Const pp _) t _ | new pp == "makePartial"
_ -> (mkBinConj b $ mkTermAppl defOp p, mkTermAppl makeTotal p)
_ -> (mkTermAppl defOp arg, mkTermAppl makeTotal arg)
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
in if new bin == "existEqualOp" then
mkBinConj lb $ mkBinConj rb
$ mkTermAppl (mkTermAppl (con eqV) lt) rt
(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
(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
Const ma _ | isTrue arg -> af
| new ma == cFalse -> false
| new mp == "liftUnit2partial" -> let af = mkTermAppl f unitOp in
Const ma _ | isTrue arg -> af
| new ma == cFalse -> noneOp
(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
| new i == "bool2partial" ->
let tc = mkTermAppl mkPartial unitOp
Const j _ | isTrue arg -> tc
| new j == cFalse -> noneOp
_ -> termAppl fun arg -- If arg tc noneOp NotCont
| new i == "constTrue" -> true
| new i == "constNil" -> unitOp
| new i == defOpS -> false
freshIndex :: State Int Int
->
Isa.Term -- simplified application to variable
simpForOption :: Simplifier
simpForOption l v nF nArg =
[ (conDouble "None", if new l == "lift2bool" then false else noneOp)
if new l == "mapPartial" then mkTermAppl mkPartial nF else nF)]
mkLetAppl eqs inTrm = case inTrm of
App (Const mp _) arg _ | new mp == "makePartial" ->
mkTermAppl mkPartial $
Isa.Let eqs arg
simpForPairs :: Simplifier
simpForPairs l v2 nF nArg = do
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 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
res = simK == Lift2Restrict
if res && lf == "lift2partial" then return . mkTermAppl
(mkTermAppl restrict . mkTermAppl f $ mkTermAppl makeTotal nArg)
else if res && lf == "mapPartial" then return . mkTermAppl
(mkTermAppl restrict . mkTermAppl mkPartial
. mkTermAppl f $ mkTermAppl makeTotal nArg)
let pvar = mkFree $ "Xc" ++ show n
nF <- simplify simK simpF $ mkTermAppl f pvar
nF <- simplify simK simpF f
nArg <- simplify simK simpF arg
nT <- simplify simK simpF t
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
_ -> mkError "not a function type" f
-- * translation of lambda abstractions
isPatternType trm = case trm of
QualVar (VarDecl _ _ _ _) -> True
TypedTerm t _ _ _ -> isPatternType t
TupleTerm ts _ -> all isPatternType ts
transPattern sign tyToks toks pat = do
ITC ty trm cs <- transTerm sign tyToks False toks
Set.empty pat
TupleTerm [] _ -> return (ty, mkFree "_")
_ -> if not (isPatternType pat) || isPartialVal ty
fatal_error ("illegal pattern for Isabelle: " ++ showDoc pat "")
-- form Abs(pattern term)
-> 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