Tip.Types

Contents

• Other views of theories

Description

Synopsis

• data Head a
  • = Gbl (Global a)
  • | Builtin Builtin
• data Local a = Local {
  • lcl_name :: a
  • lcl_type :: Type a
  }
• data Global a = Global {
  • gbl_name :: a
  • gbl_type :: PolyType a
  • gbl_args :: [Type a]
  }
• data Expr a
  • = (Head a) :@: [Expr a]
  • | Lcl (Local a)
  • | Lam [Local a] (Expr a)
  • | Match (Expr a) [Case a]
  • | Let (Local a) (Expr a) (Expr a)
  • | Quant QuantInfo Quant [Local a] (Expr a)
• data Quant
  • = Forall
  • | Exists
• data QuantInfo
  • = NoInfo
  • | QuantIH Int
• data Case a = Case {
  • case_pat :: Pattern a
  • case_rhs :: Expr a
  }
• data Builtin
  • = At
  • | Lit Lit
  • | And
  • | Or
  • | Not
  • | Implies
  • | Equal
  • | Distinct
  • | IntAdd
  • | IntSub
  • | IntMul
  • | IntDiv
  • | IntMod
  • | IntGt
  • | IntGe
  • | IntLt
  • | IntLe
• intBuiltin :: Builtin -> Bool
• litBuiltin :: Builtin -> Bool
• eqRelatedBuiltin :: Builtin -> Bool
• logicalBuiltin :: Builtin -> Bool
• data Lit
  • = Int Integer
  • | Bool Bool
  • | String String
• data Pattern a
  • = Default
  • | ConPat {
    • pat_con :: Global a
    • pat_args :: [Local a]
    }
  • | LitPat Lit
• data PolyType a = PolyType {
  • polytype_tvs :: [a]
  • polytype_args :: [Type a]
  • polytype_res :: Type a
  }
• data Type a
  • = TyVar a
  • | TyCon a [Type a]
  • | [Type a] :=>: (Type a)
  • | BuiltinType BuiltinType
• data BuiltinType
  • = Integer
  • | Boolean
• data Function a = Function {
  • func_name :: a
  • func_tvs :: [a]
  • func_args :: [Local a]
  • func_res :: Type a
  • func_body :: Expr a
  }
• data Signature a = Signature {
  • sig_name :: a
  • sig_type :: PolyType a
  }
• data Sort a = Sort {
  • sort_name :: a
  • sort_tvs :: [a]
  }
• data Datatype a = Datatype {
  • data_name :: a
  • data_tvs :: [a]
  • data_cons :: [Constructor a]
  }
• data Constructor a = Constructor {
  • con_name :: a
  • con_discrim :: a
  • con_args :: [(a, Type a)]
  }
• data Theory a = Theory {
  • thy_datatypes :: [Datatype a]
  • thy_sorts :: [Sort a]
  • thy_sigs :: [Signature a]
  • thy_funcs :: [Function a]
  • thy_asserts :: [Formula a]
  }
• emptyTheory :: Theory a
• joinTheories :: Theory a -> Theory a -> Theory a
• data Formula a = Formula {
  • fm_role :: Role
  • fm_info :: Info a
  • fm_tvs :: [a]
  • fm_body :: Expr a
  }
• data Info a
  • = Definition a
  • | IH Int
  • | Lemma Int
  • | Projection a
  • | DataDomain a
  • | DataProjection a
  • | DataDistinct a
  • | Defunction a
  • | UserAsserted
  • | Unknown
• data Role
  • = Assert
  • | Prove
• data Decl a
  • = DataDecl (Datatype a)
  • | SortDecl (Sort a)
  • | SigDecl (Signature a)
  • | FuncDecl (Function a)
  • | AssertDecl (Formula a)
• theoryDecls :: Theory a -> [Decl a]
• declsToTheory :: [Decl a] -> Theory a
• declsPass :: ([Decl a] -> [Decl b]) -> Theory a -> Theory b
• transformExpr :: (Expr a -> Expr a) -> Expr a -> Expr a
• transformExprM :: Monad m => (Expr a -> m (Expr a)) -> Expr a -> m (Expr a)
• transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a
• transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a)
• transformType :: (Type a -> Type a) -> Type a -> Type a
• transformTypeInExpr :: (Type a -> Type a) -> Expr a -> Expr a
• transformTypeInDecl :: (Type a -> Type a) -> Decl a -> Decl a

Documentation

Other views of theories