proposition: Lemma CompileMap_SCA : forall {av A} `{FacadeWrapper av (list A)} `{FacadeWrapper av (list W)} `{FacadeWrapper (Value av) A} (lst: list A) vhead vhead' vtest vlst vret vtmp fpop fempty falloc fdealloc fcons facadeBody facadeCoda env (ext: StringMap.t (Value av)) tenv tenv' (f: A -> W), GLabelMap.MapsTo fpop (Axiomatic (List_pop A)) env -> GLabelMap.MapsTo fempty (Axiomatic (List_empty A)) env -> GLabelMap.MapsTo falloc (Axiomatic (FacadeImplementationOfConstructor (list W) nil)) env -> GLabelMap.MapsTo fdealloc (Axiomatic (FacadeImplementationOfDestructor (list A))) env -> GLabelMap.MapsTo fcons (Axiomatic (FacadeImplementationOfMutation_SCA (list W) cons)) env -> PreconditionSet tenv ext [[[vhead; vhead'; vtest; vlst; vret; vtmp]]] -> {{ [[`vret ->> (revmap f lst) as _]] :: tenv }} facadeCoda {{ [[`vret ->> (revmap f lst) as _]] :: tenv' }} ∪ {{ ext }} // env -> (forall head (s: list A) (s': list W), {{ [[`vhead ->> head as _]] :: tenv }} facadeBody {{ [[`vhead' ->> f head as _]] :: tenv }} ∪ {{ [vret |> wrap s'] :: [vtest |> wrap (bool2w false)] :: [vlst |> wrap s] :: ext }} // env) -> {{ [[`vlst ->> lst as _]] :: tenv }} (Seq (Call vret falloc nil) (Seq (Seq (Fold vhead vtest vlst fpop fempty (Seq facadeBody (Call vtmp fcons (vret :: vhead' :: nil)))) (Call vtest fdealloc (vlst :: nil))) facadeCoda)) {{ [[`vret ->> (revmap f lst) as _]] :: tenv' }} ∪ {{ ext }} // env.
proof: Proof. intros. setoid_rewrite <- revmap_fold_comp. apply CompileLoopAlloc; eauto. PreconditionSet_t; eauto. eapply (CompileCallFacadeImplementationOfConstructor (A := list W)); loop_t. setoid_rewrite revmap_fold_comp; eassumption. intros. rewrite SameValues_Fiat_Bind_TelEq. move_to_front vret. apply miniChomp'; intros. hoare. apply ProgOk_Chomp_Some; loop_t; defunctionalize_evar; eauto. apply CompileCallFacadeImplementationOfMutation_SCA; unfold DummyArgument; compile_do_side_conditions. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs