Documentation

makeHaskellDataDecls :: Config -> BareSpec -> [TyCon] -> [DataDecl] Source #

makeHaskellMeasures :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [Measure (Located BareType) LocSymbol] Source #

makeHaskellInlines :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [(LocSymbol, LMap)] Source #

makeHaskellBounds :: TCEmb TyCon -> CoreProgram -> HashSet (Var, LocSymbol) -> BareM RBEnv Source #

makeMeasureSpec :: (ModName, BareSpec) -> BareM (MSpec SpecType DataCon) Source #

makeMeasureSpec' :: MSpec SpecType DataCon -> ([(Var, SpecType)], [(LocSymbol, RRType Reft)]) Source #

makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))] Source #

makeMeasureSelectors :: Config -> DataConMap -> (DataCon, Located DataConP) -> [Measure SpecType DataCon] Source #

strengthenHaskellMeasures :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)] Source #

strengthenHaskellInlines :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)] Source #

varMeasures :: Monoid r => [Var] -> [(Symbol, Located (RRType r))] Source #