fact: Fixpoint AxiomatizeMethodPostSpec' {Dom} {Cod} {RepSpec RepImpl} (av : Type) {numRepArgs : nat} (AbsR : RepSpec -> RepImpl -> Prop) {struct Dom} : CodWrapperT av Cod -> DomWrapperT av Dom -> list ((Value av) * option av) -> (RepImpl -> Vector.t ((Value av) * option av) numRepArgs) -> methodType' RepSpec Dom Cod -> list ((Value av) * option av) -> Value av -> Prop := match Dom return CodWrapperT av Cod -> DomWrapperT av Dom -> list ((Value av) * option av) -> (RepImpl -> Vector.t ((Value av) * option av) numRepArgs) -> methodType' RepSpec Dom Cod -> list ((Value av) * option av) -> Value av -> Prop with | nil => match Cod return CodWrapperT av Cod -> DomWrapperT av nil -> list ((Value av) * option av) -> (RepImpl -> Vector.t ((Value av) * option av) numRepArgs) -> methodType' RepSpec nil Cod -> list ((Value av) * option av) -> Value av -> Prop with | None => fun cWrap dWrap domArgs repArgs meth args ret => exists (r' : RepSpec) (r'' : RepImpl), computes_to meth r' /\ AbsR r' r'' /\ args = List.app (domArgs) (Vector.to_list (repArgs r'')) /\ ret = wrap (Word.natToWord 32 0) | Some CodT => fun cWrap dWrap domArgs repArgs meth args ret => exists r' r'' v', computes_to meth (r', v') /\ AbsR r' r'' /\ args = List.app (domArgs) (Vector.to_list (repArgs r'')) /\ ret = wrap (FacadeWrapper := gWrap cWrap) v' end | cons DomT Dom' => fun cWrap dWrap domArgs repArgs meth args ret => let wrap' := gWrap (fst dWrap) in exists x : DomT, AxiomatizeMethodPostSpec' AbsR cWrap (snd dWrap) ((wrap x, None) :: domArgs) repArgs (meth x) args ret 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