Comorphisms.HasCASL2IsabelleHOL

Contents

• Signature
• translation of a type in an operation declaration
• translation of a datatype declaration
• Formulas
• translation of lambda abstractions
• translation of case alternatives

Description

Synopsis

• data HasCASL2IsabelleHOL = HasCASL2IsabelleHOL
• baseSign :: BaseSig
• transSignature :: Env -> Result (Sign, [Named Sentence])
• transOpInfo :: OpInfo -> Maybe Typ
• transOpType :: TypeScheme -> Typ
• transType :: Type -> Typ
• transDatatype :: TypeMap -> DomainTab
• transDataEntry :: DataEntry -> [DomainEntry]
• transTypeArg :: TypeArg -> Typ
• transAltDefn :: AltDefn -> (VName, [Typ])
• transVar :: Id -> VName
• transSentence :: Env -> Sentence -> Maybe Term
• transOpId :: Env -> Id -> TypeScheme -> String
• transProgEq :: Env -> ProgEq -> (Term, Term)
• transTerm :: Env -> Term -> Term
• transAppl :: Env -> Maybe Type -> Term -> Term -> Term
• mkApp :: String -> Env -> Term -> Term -> Term
• transApplOp :: Env -> Type -> Term -> Term -> Term
• transLog :: Env -> Id -> Term -> Term -> Term
• transWhenElse :: Env -> Term -> Term
• abstraction :: Env -> Term -> Term -> Term
• transPattern :: Env -> Term -> Term
• transTotalLambda :: Env -> Term -> Term
• arangeCaseAlts :: Env -> [ProgEq] -> [(Term, Term)]
• sortCaseAlts :: Env -> [ProgEq] -> [(Term, Term)]
• getCons :: Env -> Id -> [Id]
• getName :: ProgEq -> Id
• getTypeName :: Term -> Id
• groupCons :: [ProgEq] -> Id -> [ProgEq]
• flattenPattern :: Env -> [ProgEq] -> (Term, Term)
• data CaseMatrix = CaseMatrix {
  • patBrand :: PatBrand
  • cons :: Maybe Term
  • args :: [Term]
  • newArgs :: [Term]
  • term :: Term
  }
• data PatBrand
  • = Appl
  • | Tuple
  • | QuOp
  • | QuVar
• matricize :: [ProgEq] -> [CaseMatrix]
• matriPEq :: ProgEq -> CaseMatrix
• matriArg :: Term -> Term -> CaseMatrix
• concentrate :: [CaseMatrix] -> Env -> CaseMatrix
• groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]
• redArgs :: Env -> [CaseMatrix] -> CaseMatrix
• redAppl :: [CaseMatrix] -> Env -> CaseMatrix
• recArgs :: Env -> [ProgEq] -> [ProgEq]
• shrinkPat :: CaseMatrix -> Term
• patIsVar :: ProgEq -> Bool
• termIsVar :: Term -> Bool
• patHasNoArg :: ProgEq -> Bool
• termHasNoArg :: Term -> Bool
• transCaseAlt :: Env -> ProgEq -> (Term, Term)
• transPat :: Env -> Term -> Term
• binConst :: String -> Term -> Term -> Term
• isaPair :: String

Documentation

Signature

translation of a type in an operation declaration

translation of a datatype declaration

Formulas

translation of lambda abstractions

translation of case alternatives