Language.Haskell.Liquid.Prover.Types

Synopsis

• type LVar = Var ()
• type LVarCtor = VarCtor ()
• type LAxiom = Axiom ()
• type LQuery = Query ()
• data Axiom a = Axiom {
  • axiom_name :: Var a
  • axiom_vars :: [LVar]
  • axiom_body :: Predicate
  }
• data Var a = Var {
  • var_name :: Symbol
  • var_sort :: Sort
  • var_info :: a
  }
• data Ctor a = Ctor {
  • ctor_expr :: Expr a
  • ctor_sort :: Sort
  • ctor_vars :: [LVar]
  • ctor_prop :: Predicate
  }
• data VarCtor a = VarCtor {
  • vctor_var :: Var a
  • vctor_vars :: [LVar]
  • vctor_prop :: Predicate
  }
• data Expr a
  • = EVar (Var a)
  • | EApp (Ctor a) [Expr a]
• newtype Predicate = Pred {
  • p_pred :: Expr
  }
• data Proof a
  • = Invalid
  • | Proof {
    • p_evidence :: [Instance a]
    }
• data Instance a = Inst {
  • inst_axiom :: Axiom a
  • inst_args :: [Expr a]
  • inst_pred :: Predicate
  }
• data Query a = Query {
  • q_axioms :: ![Axiom a]
  • q_ctors :: ![VarCtor a]
  • q_vars :: ![Var a]
  • q_env :: ![LVar]
  • q_goal :: !Predicate
  • q_fname :: !FilePath
  • q_depth :: !Int
  • q_decls :: [Predicate]
  • q_isHO :: Bool
  }
• data ArgExpr a = ArgExpr {
  • arg_sort :: Sort
  • arg_exprs :: [Expr a]
  • arg_ctors :: [Ctor a]
  }
• varCtorToCtor :: VarCtor a -> Ctor a
• isEVar :: Expr t -> Bool
• mkExpr :: Expr a -> Expr

Documentation