NOTE:AUTO-INDPRED (teststodoIndPred1.hs) -- DO NOT DELETE -- RJ: too hard, too brittle, I _thought_ we could just -- generate the F.DataDecl, but really, you need the GHC -- names for the Prop-Ctor if you want to be able to `import` -- a predicate across modules. Seems a LOT easier to just have -- the program explicitly create the the proposition type -- e.g. as shownn in (testsposIndPred0.hs) --------------------------------------------------------------------------------

type SpecTypeRep = RTypeRep RTyCon RTyVar RReft

• - | makePropDecl creates the DataDecl for the *proposition* described
• - by the corresponding TyCon DataDecl, e.g. testspos/IndPred0.hs makePropDecl :: F.TCEmb TyCon -> TyCon -> DataPropDecl -> Maybe F.DataDecl makePropDecl tce tc (dd, pd) = makePropTyDecl tce tc dd $ pd

makePropTyDecl :: F.TCEmb TyCon -> TyCon -> DataDecl -> SpecType -> F.DataDecl makePropTyDecl tce tc dd t = F.DDecl { F.ddTyCon = ftc , F.ddVars = length (ty_vars tRep) , F.ddCtors = [ makePropTyCtor tce ftc tRep ] } where ftc = propFTycon tc dd tRep = toRTypeRep t

propFTycon :: TyCon -> DataDecl -> F.FTycon propFTycon tc = F.symbolFTycon . fmap (suffixSymbol F.propConName) . tyConLocSymbol tc

makePropTyCtor :: F.TCEmb TyCon -> F.FTycon -> SpecTypeRep -> F.DataCtor makePropTyCtor tce ftc t = F.DCtor { F.dcName = F.fTyconSymbol ftc , F.dcFields = makePropTyFields tce ftc t }

makePropTyFields :: F.TCEmb TyCon -> F.FTycon -> SpecTypeRep -> [F.DataField] makePropTyFields tce ftc t = makeDataFields tce ftc as xts where as = [ a | RTVar a _ <- ty_vars t ] xts = zipWith (i t -> (fld i, t)) [0..] (ty_args t) tcSym = F.fTyconSymbol ftc fld = F.atLoc tcSym . GM.symbolMeasure "propField" (val tcSym) . Just

isPropDecl :: F.DataDecl -> Bool isPropDecl d = (F.isSuffixOfSym F.propConName . F.symbol . F.ddTyCon $ d) && (length (F.ddCtors d) == 1)

qualifyDataDecl :: ModName -> DataDecl -> DataDecl qualifyDataDecl name d = d { tycName = qualifyName name (tycName d)}

qualifyName :: ModName -> LocSymbol -> LocSymbol qualifyName n x = F.atLoc x $ GM.qualifySymbol nSym (val x) where nSym = GM.takeModuleNames (F.symbol n)

Bare Predicate: DataCon Definitions ---------------------------------------

DataConMap stores the names of those ctor-fields that have been declared as SMT ADTs so we don't make up new names for them.