fact: Fixpoint LiftMethod' (av : Type) (env : Env av) {Rep} {Cod} {Dom} (P : Rep -> Prop) (DecomposeRep : Rep -> Telescope av) (DecomposeRepPre : list {T : _ & prod (NameTag av T) (Comp T)}) {struct Dom} := match Dom return CodWrapperT av Cod -> DomWrapperT av Dom -> Stmt -> list {T : _ & prod (NameTag av T) (Comp T)} -> methodType' Rep Dom Cod -> Prop with | nil => match Cod return CodWrapperT av Cod -> DomWrapperT av nil -> Stmt -> list {T : _ & prod (NameTag av T) (Comp T)} -> methodType' Rep nil Cod -> Prop with | None => fun cWrap dWrap prog pre meth => {{ list2Telescope (pre ++ DecomposeRepPre) }} prog {{ [[meth as database]] :: [[`"ret" ->> Word.natToWord 32 0 as _]] :: (DecomposeRep database) }} ∪ {{ StringMap.empty _ }} // env /\ forall r', computes_to meth r' -> P r' | Some CodT => fun cWrap dWrap prog pre meth => let v : FacadeWrapper (Value av) CodT := (gWrap cWrap) in {{ list2Telescope (pre ++ DecomposeRepPre) }} prog {{[[meth as mPair]] :: [[`"ret" ->> snd mPair as _]] :: (DecomposeRep (fst mPair))}} ∪ {{ StringMap.empty _ }} // env /\ forall r' v', computes_to meth (r', v') -> P r' end | cons DomT Dom' => fun cWrap dWrap prog tele meth => forall d, let _ := gWrap (fst dWrap) in LiftMethod' env Dom' P DecomposeRep DecomposeRepPre cWrap (snd dWrap) prog ((existT _ _ (NTSome (nthArgName (List.length tele)), ret d)) :: tele) (meth d) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction