fact: Fixpoint repr {A : choiceType} (p : raw_code A) : rFreeF (@ops_StP heap_choiceType) (@ar_StP heap_choiceType) A := match p with | ret x => retrFree x | opr o x k => repr (k (chCanonical (chtgt o))) | getr l k => bindrFree (ropr gett (λ s, retrFree (get_heap s l))) (λ v, repr (k v)) | putr l v k => bindrFree (ropr gett (λ s, ropr (putt (set_heap s l v)) (λ s, retrFree tt))) (λ _, repr k) | sampler op k => bindrFree (ropr (op_iota op) (λ v, retrFree v)) (λ s, repr (k s)) end.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)