0N/ACopyright : (c) Sonja Groening, C. Maeder, Uni Bremen 2003-2005
0N/AMaintainer : maeder@tzi.de
0N/AStability : provisional
0N/AThe embedding comorphism from HasCASL to Isabelle-HOL.
-- | The identity of the comorphism
data HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving Show
instance Language HasCASL2IsabelleHOL -- default definition is okay
instance Comorphism HasCASL2IsabelleHOL
HasCASL HasCASL_Sublogics
IsabelleMorphism () () () where
sourceLogic HasCASL2IsabelleHOL = HasCASL
sourceSublogic HasCASL2IsabelleHOL = HasCASL_SL
{ has_sub = False, -- subsorting
has_part = True, -- partiality
has_eq = True, -- equality
has_pred = True, -- predicates
has_ho = True, -- higher order
has_type_classes = False,
has_type_constructors = True,
targetLogic HasCASL2IsabelleHOL = Isabelle
targetSublogic HasCASL2IsabelleHOL = ()
map_theory HasCASL2IsabelleHOL = mkTheoryMapping transSignature
(map_sentence HasCASL2IsabelleHOL)
map_morphism HasCASL2IsabelleHOL mor = do
(sig1,_) <- map_sign HasCASL2IsabelleHOL (
Logic.dom HasCASL mor)
(sig2,_) <- map_sign HasCASL2IsabelleHOL (cod HasCASL mor)
inclusion Isabelle sig1 sig2
map_sentence HasCASL2IsabelleHOL sign phi =
case transSentence sign phi of
Nothing -> warning (Sentence {senTerm = true})
"translation of sentence not implemented" nullRange
Just (ts) -> return $ Sentence {senTerm = ts}
-- ============================ Signature ================================== --
-- translation of typeconstructors
-- translation of operation declarations
-- translation of datatype declarations
dataTypeTab = transDatatype (typeMap sign),
extractTypeName tyId typeInfo m =
if isDatatypeDefn typeInfo then m
else
Map.insert (showIsaTypeT tyId baseSign) [(isaTerm, [])] m
-- translate the kind here!
isDatatypeDefn t = case typeDefn t of
in if isSingle infos then
let transOp = transOpInfo (head infos)
Map.insert (VName {new=showIsaConstT name baseSign,orig=show name}) op m
let transOps = map transOpInfo infos
in foldl (\ m' (transOp,i) ->
Just typ ->
Map.insert (VName {new=showIsaConstIT name i baseSign,
orig=show name ++ show i})
m (zip transOps [1::Int ..])
---------- translation of a type in an operation declaration ----------
-- extract type from OpInfo
-- omit datatype constructors
transOpInfo :: OpInfo -> Maybe Typ
transOpInfo (OpInfo t _ opDef) =
ConstructData _ -> Nothing
_ -> Just (transOpType t)
transOpType :: TypeScheme -> Typ
transOpType (TypeScheme _ op _) = transType op
transType t = case getTypeAppl t of
(TypeName tid _ n, tyArgs) -> let num = length tyArgs in
if tid == unitTypeId && null tyArgs then boolType
else if tid == lazyTypeId && num == 1 then
else if isArrow tid && num == 2 then
in mkFunType (transType t1) $
if isPartialArrow tid && not (isPredType t)
then mkOptionType tr else tr
else if isProductId tid && num > 1 then
foldl1 prodType $ map transType tyArgs
else foldl binTypeAppl (Type (showIsaTypeT tid baseSign) [] [])
else foldl binTypeAppl (TFree (showIsaTypeT tid baseSign) [])
_ -> error $ "transType " ++ showPretty t "\n" ++ show t
---------- translation of a datatype declaration ----------
transDatatype :: TypeMap -> DataTypeTab
transDatatype tm = map transDataEntry (
Map.fold extractDataypes [] tm)
where extractDataypes ti des = case typeDefn ti of
DatatypeDefn de -> des++[de]
-- datatype with name (tyId) + args (tyArgs) and alternatives
transDataEntry :: DataEntry -> DataTypeTabEntry
transDataEntry (DataEntry _ tyId
Le.Free tyArgs _ alts) =
[((transDName tyId tyArgs), (map transAltDefn alts))]
where transDName ti ta = Type (showIsaTypeT ti baseSign) [] (map transTypeArg ta)
-- arguments of datatype's typeconstructor
transTypeArg :: TypeArg -> Typ
transTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []
transAltDefn :: AltDefn -> DataTypeAlt
transAltDefn (Construct opId ts Total _) =
let ts' = map transType ts
Just opId' -> ((VName {new=showIsaConstT opId' baseSign,
Nothing -> ((VName {new="",orig=""}), ts')
------------------------------ Formulas ------------------------------
transVar v = mkVName $ showIsaConstT v baseSign
transSentence sign s = case s of
ProgEqSen _ _ _pe -> Nothing
-- disambiguate operation names
transOpId :: Env -> UninstOpId -> TypeScheme -> String
if isSingle (opInfos ops) then return $ showIsaConstT op baseSign
else do i <- elemIndex ts (map opType (opInfos ops))
return $ showIsaConstIT op (i+1) baseSign) of
Nothing -> showIsaConstT op baseSign
transProgEq sign (ProgEq pat t _) =
(transPattern sign pat, transPattern sign t)
transTerm sign trm = case trm of
QualVar (VarDecl var t _ _) ->
ot = mkFunType t' $ mkOptionType t'
QualOp _ (InstOpId opId _ _) ts _ ->
if opId == trueId then conDouble "True"
else if opId == falseId then conDouble "False"
else termAppl conSome (conDouble (transOpId sign opId ts))
QuantifiedTerm quan varDecls phi _ ->
let quantify q gvd phi' = case gvd of
GenVarDecl (VarDecl var typ _ _) ->
termAppl (conDouble $ qname q)
$ Abs (con $ transVar var) (transType typ) phi' NotCont
in foldr (quantify quan) (transTerm sign phi) varDecls
TypedTerm t _ _ _ -> transTerm sign t
LambdaTerm pats p body _ ->
let lambdaAbs f = if null pats then termAppl conSome
noType (f sign body) NotCont)
else termAppl conSome (foldr (abstraction sign)
-- distinguishes between partial and total lambda abstraction
-- total lambda bodies are of type 'a' instead of type 'a option'
Partial -> lambdaAbs transTerm
Total -> lambdaAbs transTotalLambda
IsaSign.Let (map (transProgEq sign) peqs) $ transTerm sign body
TupleTerm ts@(_ : _) _ ->
foldl1 (binConst pairC) (map (transTerm sign) ts)
ApplTerm t1 t2 _ -> transAppl sign Nothing t1 t2
-- flatten case alternatives
let alts = arangeCaseAlts sign peqs
-- introduces new case statement if case variable is
-- a term application that may evaluate to 'Some x' or 'None'
QualVar (VarDecl decl _ _ _) ->
_ -> Case (transTerm sign t)
[(conDouble "None", conDouble "None"),
(App conSome (
IsaSign.Free (mkVName "caseVar") noType) NotCont,
transAppl s typ t' t'' = case t'' of
TupleTerm [] _ -> transTerm s t'
QualVar (VarDecl _ ty _ _) -> if isPredType ty
then mkApp "pApp" s t' t''
else transApplOp s ty t' t''
QualOp _ (InstOpId opId _ _) (TypeScheme _ ty _) _ ->
if elem opId $ map fst bList then
-- logical formulas are translated seperatly (transLog)
if opId == whenElse then transWhenElse s t''
else transLog s opId t' t''
else if isPredType ty then mkApp "pApp" s t' t''
else transApplOp s ty t' t''
-- distinguishes between partial and total term application
TypedTerm tt' _ typ' _ -> transAppl s (Just typ') tt' t''
_ -> maybe (mkApp "app" s t' t'')
( \ ty -> transApplOp s ty t' t'') typ
mkApp s sg tt tt' = termAppl (termAppl (conDouble s) (transTerm sg tt))
transApplOp s typ tt tt' = case getTypeAppl typ of
(TypeName tid _ 0, [_, _]) | isArrow tid ->
if isPartialArrow tid then mkApp "app" s tt tt'
else mkApp "apt" s tt tt'
_ -> mkApp "app" s tt tt'
-- translation formulas with logical connectives
transLog sign opId opTerm t = case t of
| opId == andId -> binConst conj l r
| opId == orId -> binConst disj l r
| opId == implId -> binConst impl l r
| opId == infixIf -> binConst impl r l
| opId == eqvId -> binConst eqv l r
| opId == exEq -> binConst conj (binConst eq l r) $
binConst conj (termAppl defOp l) $
| opId == eqId -> binConst eq l r
where l = transTerm sign l'
_ | opId == notId -> termAppl notOp (transTerm sign t)
| opId == defId -> termAppl defOp (transTerm sign t)
| otherwise -> termAppl (transTerm sign opTerm) (transTerm sign t)
let ts = (map (transTerm sign) terms)
[i, c, e] -> If c i e NotCont
--translation of lambda abstractions
-- form Abs(pattern term)
abstraction sign pat body =
Abs (transPattern sign pat) (getType pat) body NotCont where
-- Abs (transPattern sign pat) body NotCont where
QualVar (VarDecl _ typ _ _) -> transType typ
TypedTerm _ _ typ _ -> transType typ
TupleTerm terms _ -> evalTupleType terms
evalTupleType t = foldr1 prodType (map getType t)
-- translation of lambda patterns
-- a pattern keeps his type 't', isn't translated to 't option'
transPattern _ (QualVar (VarDecl var typ _ _)) =
transPattern sign (TupleTerm terms@(_ : _) _) =
foldl1 (binConst isaPair) $ map (transPattern sign) terms
transPattern _ (QualOp _ (InstOpId opId _ _) _ _) =
conDouble $ showIsaConstT opId baseSign
transPattern sign (TypedTerm t _ _ _) = transPattern sign t
transPattern sign (ApplTerm t1 t2 _) =
App (transPattern sign t1) (transPattern sign t2) NotCont
transPattern sign t = transTerm sign t
-- translation of total lambda abstraction bodies
transTotalLambda _ (QualVar (VarDecl var typ _ _)) =
transTotalLambda sign t@(QualOp _ (InstOpId opId _ _) _ _) =
if opId == trueId || opId == falseId then transTerm sign t
else conDouble $ showIsaConstT opId baseSign
transTotalLambda sign (ApplTerm term1 term2 _) =
termAppl (transTotalLambda sign term1) $ transTotalLambda sign term2
transTotalLambda sign (TypedTerm t _ _ _) = transTotalLambda sign t
transTotalLambda sign (LambdaTerm pats part body _) =
Partial -> lambdaAbs transTerm
Total -> lambdaAbs transTotalLambda
if (null pats) then Abs (
IsaSign.Free (VName {new="dummyVar",orig="dummyVar"}) noType)
noType (f sign body) NotCont
-- if (null pats) then Abs [("dummyVar", noType)]
else foldr (abstraction sign) (f sign body) pats
transTotalLambda sign (TupleTerm terms@(_ : _) _) =
foldl1 (binConst isaPair) $ map (transTotalLambda sign) terms
transTotalLambda sign (CaseTerm t pEqs _) =
Case (transTotalLambda sign t) $ map transCaseAltTotal pEqs
where transCaseAltTotal (ProgEq pat trm _) =
(transPat sign pat, transTotalLambda sign trm)
transTotalLambda sign t = transTerm sign t
----------------- translation of case alternatives ------------------
{- Annotation concerning Patterns:
Following the HasCASL-Summary and the limits of the encoding
QualVar, QualOp, ApplTerm, TupleTerm and TypedTerm
-- Input: List of case alternative (one pattern per term)
-- Functionality: Tests wheter pattern is a variable -> case alternative is
| and (map patIsVar peqs) = map (transCaseAlt sign) peqs
| otherwise = sortCaseAlts sign peqs
{- Input: List of case alternatives, that patterns does consist of
datatype constructors (with arguments) or tupels
Functionality: Groups case alternatives by leading
pattern-constructor each pattern group is flattened
| null peqs = error "No case alternatives."
| otherwise = getCons sign (getName (head peqs))
in map (flattenPattern sign) groupedByCons
-- Returns a list of the constructors of the used datatype
getCons :: Env -> TypeId -> [UninstOpId]
extractIds (typeDefn (findInMap tyId (typeMap sign)))
where extractIds (DatatypeDefn (DataEntry _ _ _ _ _ altDefns)) =
catMaybes (map stripConstruct altDefns)
stripConstruct (Construct i _ _ _) = i
findInMap :: Ord k => k ->
Map.Map k a -> a
-- Extracts the type of the used datatype in case patterns
getName :: ProgEq -> TypeId
getName (ProgEq pat _ _) = (getTypeName pat)
getTypeName :: Pattern -> TypeId
QualVar (VarDecl _ typ _ _) -> name typ
QualOp _ _ (TypeScheme _ typ _) _ -> name typ
TypedTerm _ _ typ _ -> name typ
ApplTerm t _ _ -> getTypeName t
TupleTerm ts _ -> getTypeName (head ts)
where name tp = case getTypeAppl tp of
(TypeName tyId _ 0, tyArgs) -> let num = length tyArgs in
if isArrow tyId && num == 2 then
name $ head $ tail tyArgs
else if isProductId tyId && num > 1 then
-- Input: Case alternatives and name of one constructor
-- Functionality: Filters case alternatives by constructor's name
groupCons :: [ProgEq] -> UninstOpId -> [ProgEq]
groupCons peqs name = filter hasSameName peqs
where hasSameName (ProgEq pat _ _) =
QualOp _ (InstOpId n _ _) _ _ -> n == name
ApplTerm t1 _ _ -> hsn t1
TypedTerm t _ _ _ -> hsn t
-- Input: List of case alternatives with same leading constructor
-- Functionality: Tests whether the constructor has no arguments, if so
-- translates case alternatives
flattenPattern sign peqs = case peqs of
[] -> error "Missing constructor alternative in case pattern."
[h] -> transCaseAlt sign h
-- at this stage there are patterns left which use 'ApplTerm' or 'TupleTerm'
-- or the 'TypedTerm' variant of one of them
_ -> let m = concentrate (matricize peqs) sign in
transCaseAlt sign (ProgEq (shrinkPat m) (term m) nullRange)
data CaseMatrix = CaseMatrix { patBrand :: PatBrand,
data PatBrand = Appl | Tuple | QuOp | QuVar deriving (Eq, Show)
instance Eq CaseMatrix where
(==) cmx cmx' = (patBrand cmx == patBrand cmx')
&& (args cmx == args cmx')
&& (term cmx == term cmx')
&& (cons cmx == cons cmx')
&& (newArgs cmx == newArgs cmx')
{- First of all a matrix is allocated (matriArg) with the arguments of a
constructor resp. of a tuple. They're binded with the term, that would
be executed if the pattern matched. Then the resulting list of
matrices is grouped by the leading argument. (groupArgs) Afterwards -
if a list of grouped arguments has more than one element - the last
pattern argument (in the list 'patterns') is replaced by a new variable.
n patterns are reduced to one pattern.
This procedure is repeated until there's only one case alternative
-- Functionality: turns ProgEq into CaseMatrix
matricize :: [ProgEq] -> [CaseMatrix]
matriPEq :: ProgEq -> CaseMatrix
matriPEq (ProgEq pat altTerm _) = matriArg pat altTerm
matriArg :: Pattern ->
As.Term -> CaseMatrix
ApplTerm t1 t2 _ -> let (c, p) = stripAppl t1 (Nothing, [])
CaseMatrix { patBrand = Appl,
TupleTerm ts _ -> CaseMatrix { patBrand = Tuple,
TypedTerm t _ _ _ -> matriArg t cTerm
qv@(QualVar _) -> CaseMatrix { patBrand = QuVar,
qo@(QualOp _ _ _ _) -> CaseMatrix { patBrand = QuOp,
-- Assumption: The innermost term of a case-pattern consisting of a ApplTerm
-- is a QualOp, that is a datatype constructor
where stripAppl ct tp = case ct of
TypedTerm (ApplTerm q@(QualOp _ _ _ _) t' _) _ _ _ ->
TypedTerm (ApplTerm (TypedTerm
q@(QualOp _ _ _ _) _ _ _) t' _) _ _ _ -> (Just q, [t'] ++ snd tp)
TypedTerm (ApplTerm t' t'' _) _ _ _ ->
stripAppl t' (fst tp, [t''] ++ snd tp)
ApplTerm q@(QualOp _ _ _ _) t' _ -> (Just q, [t'] ++ snd tp)
q@(QualOp _ _ _ _) _ _ _) t' _ -> (Just q, [t'])
stripAppl t' (fst tp, [t''] ++ snd tp)
-- TypedTerm t' _ _ _ -> stripAppl t' tp
q@(QualOp _ _ _ _) -> (Just q, snd tp)
_ -> (Nothing, [ct] ++ snd tp)
-- Input: List with CaseMatrix of same leading constructor pattern
-- Functionality: First: Groups CMs so that these CMs are in one list
-- that only differ in their last argument
-- then: reduces list of every CMslist to one CM
concentrate :: [CaseMatrix] -> Env -> CaseMatrix
concentrate cmxs sign = case map (redArgs sign) $
nub $ map (groupByArgs cmxs) [0..(length cmxs-1)] of
groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]
| and (map null (map args cmxs)) = cmxs
| otherwise = (filter equalPat cmxs)
where patE = init (args (cmxs !! i))
equalPat cmx = isSingle (args cmx) || init (args cmx) == patE
redArgs :: Env -> [CaseMatrix] -> CaseMatrix
| and (map (testPatBrand Appl) cmxs) = redAppl cmxs sign
| and (map (testPatBrand Tuple) cmxs) = redAppl cmxs sign
| isSingle cmxs = head cmxs
where testPatBrand pb cmx = pb == patBrand cmx
{- Input: List of CMs thats leading constructor and arguments except
Functionality: Reduces n CMs to one with same last argument in
pattern (perhaps a new variable
redAppl :: [CaseMatrix] -> Env -> CaseMatrix
| and (map null (map args cmxs)) = head cmxs
(head cmxs) { args = init $ args $ head cmxs,
newArgs = last (args $ head cmxs) : newArgs (head cmxs) }
| and (map termIsVar lastArgs) = substVar (head cmxs)
| otherwise = substTerm (head cmxs)
where terms = map term cmxs
lastArgs = map last (map args cmxs)
varName = "caseVar" ++ show (length (args (head cmxs)))
varId = (mkId [(mkSimpleId varName)])
newVar = QualVar (VarDecl varId (TypeName varId rStar 1)
newPeqs = (map newProgEq (zip lastArgs terms))
newPeqs' = recArgs sign newPeqs
newArgs = last(args cmx) : (newArgs cmx) }
cmx { args = init (args cmx),
newArgs = last(args cmx) : (newArgs cmx) }
newArgs = newVar : (newArgs cmx),
term = CaseTerm newVar newPeqs' nullRange }
cmx { args = init(args cmx),
newArgs = newVar : (newArgs cmx),
term = CaseTerm newVar newPeqs' nullRange }
newProgEq (p, t) = ProgEq p t nullRange
-- Input: ProgEqs that were build to replace an argument
recArgs :: Env -> [ProgEq] -> [ProgEq]
|| null groupedByCons = []
| otherwise = doPEQ groupedByCons []
| null peqs = error "No case alternatives."
| otherwise = getCons sign (getName (head peqs))
groupedByCons = map (groupCons peqs) consList
| isSingle g = doPEQ gByCs (res ++ g)
| otherwise = doPEQ gByCs (res ++ [(toPEQ (testPEQs sign g))])
toPEQ cmx = ProgEq (shrinkPat cmx) (term cmx) nullRange
| otherwise = concentrate (matricize ps) sig
-- accumulates arguments of caseMatrix to one pattern
Just c -> foldl mkApplT c ((args cmx) ++ (newArgs cmx))
Tuple -> TupleTerm ((args cmx) ++ (newArgs cmx)) nullRange
where mkApplT t1 t2 = ApplTerm t1 t2 nullRange
patIsVar :: ProgEq -> Bool
patIsVar (ProgEq pat _ _) = termIsVar pat
TypedTerm tr _ _ _ -> termIsVar tr
TupleTerm ts _ -> and (map termIsVar ts)
patHasNoArg :: ProgEq -> Bool
patHasNoArg (ProgEq pat _ _) = termHasNoArg pat
termHasNoArg t = case t of
TypedTerm tr _ _ _ -> termHasNoArg tr
transCaseAlt sign (ProgEq pat trm _) =
(transPat sign pat, (transTerm sign trm))
transPat _ (QualVar (VarDecl var _ _ _)) =
transPat sign (ApplTerm term1 term2 _) =
termAppl (transPat sign term1) (transPat sign term2)
transPat sign (TypedTerm trm _ _ _) = transPat sign trm
transPat sign (TupleTerm terms@(_ : _) _) =
foldl1 (binConst isaPair) (map (transPat sign) terms)
transPat _ (QualOp _ (InstOpId i _ _) _ _) =
conDouble (showIsaConstT i baseSign)