From ee95f84c1430844e9a3669864f42486ffcb1c59d Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 30 May 2024 09:49:20 -0400 Subject: [PATCH 1/7] Sketch, abstraction of extractor --- SampCert/Extractor/Abstract.lean | 10 ++++++++++ SampCert/Extractor/Translate.lean | 6 +++--- 2 files changed, 13 insertions(+), 3 deletions(-) create mode 100644 SampCert/Extractor/Abstract.lean diff --git a/SampCert/Extractor/Abstract.lean b/SampCert/Extractor/Abstract.lean new file mode 100644 index 00000000..4509df23 --- /dev/null +++ b/SampCert/Extractor/Abstract.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jean-Baptiste Tristan +-/ + +class MyAbstractLanguage (T : Type) where + FOO : Type → Type + plop : Monad FOO + while_ : (T → Bool) → (T → FOO T) → (init : T) → FOO T diff --git a/SampCert/Extractor/Translate.lean b/SampCert/Extractor/Translate.lean index 75d70735..3d8f1e4c 100644 --- a/SampCert/Extractor/Translate.lean +++ b/SampCert/Extractor/Translate.lean @@ -7,13 +7,13 @@ Authors: Jean-Baptiste Tristan import Lean import SampCert.Extractor.IR import SampCert.Extractor.Extension -import SampCert.SLang +import SampCert.Extractor.Abstract namespace Lean.ToDafny def IsWFMonadic (e: Expr) : MetaM Bool := match e with - | .app (.const ``SLang ..) _ => return true + | .app (.const ``MyAbstractLanguage.FOO ..) _ => return true | .app .. => return true -- Need to work out details of this one, related to translation of dependent types | .forallE _ _ range _ => IsWFMonadic range | _ => return false -- throwError "IsWFMonadic {e}" @@ -70,7 +70,7 @@ partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM | ``ite => return .ite (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[3]!) (← toDafnyExpr dname env args[4]!) | ``dite => return .ite (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname ("dummy" :: env) (chopLambda args[3]!)) (← toDafnyExpr dname ("dummy" :: env) (chopLambda args[4]!)) | ``throwThe => return .throw (← toDafnyExpr dname env args[4]!) - | ``SLang.probWhile => return .prob_while (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) + | ``MyAbstractLanguage.while_ => return .prob_while (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) | ``SLang.probUntil => return .prob_until (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) | ``OfNat.ofNat => toDafnyExpr dname env args[1]! | ``HAdd.hAdd => return .binop .addition (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) From b9bd3a4f406e03111d79bd8f7f2e73378f49a10d Mon Sep 17 00:00:00 2001 From: de Medeiros Date: Thu, 30 May 2024 10:21:26 -0400 Subject: [PATCH 2/7] semibundled capsid --- SampCert/Extractor/Abstract.lean | 37 ++++++++++++++++++++++++++++---- 1 file changed, 33 insertions(+), 4 deletions(-) diff --git a/SampCert/Extractor/Abstract.lean b/SampCert/Extractor/Abstract.lean index 4509df23..2bd93911 100644 --- a/SampCert/Extractor/Abstract.lean +++ b/SampCert/Extractor/Abstract.lean @@ -4,7 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -class MyAbstractLanguage (T : Type) where - FOO : Type → Type - plop : Monad FOO - while_ : (T → Bool) → (T → FOO T) → (init : T) → FOO T +-- Is this correctly bundled? Using this structure seems challenging. Feels like the monad should be in place of T. +class Capsid (T : Type) where + CapsM : Type → Type + CapsM_inst : Monad CapsM + + capsWhile : (T → Bool) → (T → CapsM T) → (init : T) → CapsM T + +def ret_false_test [C : Capsid T] : C.CapsM Bool := C.CapsM_inst.pure False + +class Capsid_semibundled (CapsM : Type u -> Type v) extends Monad CapsM where + capsWhile : (T → Bool) → (T → CapsM T) → (init : T) → CapsM T + +def ret_false_test' [Capsid_semibundled CapsM] : CapsM Bool := return false + + + + + + +/- +Finite unrolling of a loop with a signal for max depth reached +-/ + + + + +-- def iter [Monad m] (body : T -> m T) (cond : T -> Bool) (fuel : Nat) (t : T) : (OptionT m) T +-- := match fuel with +-- | Nat.zero => failure +-- | Nat.succ fuel' => +-- if cond t +-- then (body t) >>= (iter body cond fuel') +-- else pure t From 012a6e474bf64d463ee8848cae3ec81319df0bbd Mon Sep 17 00:00:00 2001 From: de Medeiros Date: Thu, 30 May 2024 11:12:45 -0400 Subject: [PATCH 3/7] wip loop spec --- SampCert/Extractor/Abstract.lean | 78 ++++++++++++++++++-------------- 1 file changed, 45 insertions(+), 33 deletions(-) diff --git a/SampCert/Extractor/Abstract.lean b/SampCert/Extractor/Abstract.lean index 2bd93911..1209afdb 100644 --- a/SampCert/Extractor/Abstract.lean +++ b/SampCert/Extractor/Abstract.lean @@ -4,36 +4,48 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ --- Is this correctly bundled? Using this structure seems challenging. Feels like the monad should be in place of T. -class Capsid (T : Type) where - CapsM : Type → Type - CapsM_inst : Monad CapsM - - capsWhile : (T → Bool) → (T → CapsM T) → (init : T) → CapsM T - -def ret_false_test [C : Capsid T] : C.CapsM Bool := C.CapsM_inst.pure False - -class Capsid_semibundled (CapsM : Type u -> Type v) extends Monad CapsM where - capsWhile : (T → Bool) → (T → CapsM T) → (init : T) → CapsM T - -def ret_false_test' [Capsid_semibundled CapsM] : CapsM Bool := return false - - - - - - -/- -Finite unrolling of a loop with a signal for max depth reached --/ - - - - --- def iter [Monad m] (body : T -> m T) (cond : T -> Bool) (fuel : Nat) (t : T) : (OptionT m) T --- := match fuel with --- | Nat.zero => failure --- | Nat.succ fuel' => --- if cond t --- then (body t) >>= (iter body cond fuel') --- else pure t +import Mathlib.Order.SetNotation + +class Capsid (CapsM : Type u -> Type v) extends Monad CapsM where + capsWhile : (cond : T → Bool) → (body : T → CapsM T) → T → CapsM T + +section capsid_wf + variable {CapsM : Type u -> Type v} [C : Capsid CapsM] + variable {T : Type u} + variable (cond : T -> Bool) (body : T -> CapsM T) + + open Capsid + + def capsIter (fuel : Nat) : T -> (OptionT CapsM) T + := fun t => + match fuel with + | Nat.zero => failure + | Nat.succ fuel' => + if cond t + then (body t) >>= (capsIter fuel') + else pure t + + def capsIterPartial (fuel : Nat) : T -> CapsM T + := fun t => + match fuel with + | Nat.zero => return t + | Nat.succ fuel' => + if cond t + then (body t) >>= (capsIterPartial fuel') + else pure t + + -- Partial correctness specification for While + -- Since we're going to translate it into a while loop, we want specify that the shallow embedding to behave like a + -- the limit of loop iterations. + def CapsWhileSpec : Prop + := ∀ t0, capsWhile cond body t0 = sorry +-- ∀ t0 : T, ∃ i : Nat, ((∀ j : Nat, j < i -> iter body cond j t0 = failure) ∧ ¬ (iter body cond i t0 = failure)) +-- -> iter body cond i t0 = loop T body cond t0 +-- Err... This is not right. Maybe we require that the well-formed Capsid instances are topological types? +-- Do we want to say that "terminating executions of loops equal a finite unrolling" or "loops are the +-- limit of finite unrollings"? + +end capsid_wf + +class CapsidWF (CapsM : Type u -> Type v) extends Capsid CapsM where + capsWhileWF : ∀ (cond : T -> Bool), ∀ (body : T -> CapsM T), CapsWhileSpec cond body From c6b569382bc34ca931e5b96910fc2342092c173a Mon Sep 17 00:00:00 2001 From: de Medeiros Date: Thu, 30 May 2024 11:26:55 -0400 Subject: [PATCH 4/7] instance Capsid SLang (builds, doesn't extract) --- SampCert/Extraction.lean | 43 +++++++++++++++++++------------ SampCert/Extractor/Abstract.lean | 3 +-- SampCert/Extractor/Translate.lean | 21 +++++++-------- 3 files changed, 37 insertions(+), 30 deletions(-) diff --git a/SampCert/Extraction.lean b/SampCert/Extraction.lean index 529fb06b..01b7f1ef 100644 --- a/SampCert/Extraction.lean +++ b/SampCert/Extraction.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ +import SampCert.Extractor.Abstract import SampCert.Extractor.Export import SampCert.Extractor.Align import SampCert.Samplers.Uniform.Code @@ -12,11 +13,14 @@ import SampCert.Samplers.BernoulliNegativeExponential.Code import SampCert.Samplers.Laplace.Code import SampCert.Samplers.Gaussian.Code +noncomputable section + open SLang -/-! Extractor -Attributes which trigger extraction. +/-! Extraction using Capsid + +This file instantiates a Capsid instance for SLang, and marks a list of SLang files for extraction. The names in this file are protected: the extractor will not work if these names are changed.a @@ -24,18 +28,23 @@ Additionally, the following names are protected: - ``UniformPowerOfTwoSample`` -/ -attribute [export_dafny] UniformSample -attribute [export_dafny] BernoulliSample -attribute [export_dafny] BernoulliExpNegSampleUnitLoop -attribute [export_dafny] BernoulliExpNegSampleUnitAux -attribute [export_dafny] BernoulliExpNegSampleUnit -attribute [export_dafny] BernoulliExpNegSampleGenLoop -attribute [export_dafny] BernoulliExpNegSample -attribute [export_dafny] DiscreteLaplaceSampleLoopIn1Aux -attribute [export_dafny] DiscreteLaplaceSampleLoopIn1 -attribute [export_dafny] DiscreteLaplaceSampleLoopIn2Aux -attribute [export_dafny] DiscreteLaplaceSampleLoopIn2 -attribute [export_dafny] DiscreteLaplaceSampleLoop -attribute [export_dafny] DiscreteLaplaceSample -attribute [export_dafny] DiscreteGaussianSampleLoop -attribute [export_dafny] DiscreteGaussianSample +instance : Capsid SLang where + capsWhile := probWhile + + + +-- attribute [export_dafny] UniformSample +-- attribute [export_dafny] BernoulliSample +-- attribute [export_dafny] BernoulliExpNegSampleUnitLoop +-- attribute [export_dafny] BernoulliExpNegSampleUnitAux +-- attribute [export_dafny] BernoulliExpNegSampleUnit +-- attribute [export_dafny] BernoulliExpNegSampleGenLoop +-- attribute [export_dafny] BernoulliExpNegSample +-- attribute [export_dafny] DiscreteLaplaceSampleLoopIn1Aux +-- attribute [export_dafny] DiscreteLaplaceSampleLoopIn1 +-- attribute [export_dafny] DiscreteLaplaceSampleLoopIn2Aux +-- attribute [export_dafny] DiscreteLaplaceSampleLoopIn2 +-- attribute [export_dafny] DiscreteLaplaceSampleLoop +-- attribute [export_dafny] DiscreteLaplaceSample +-- attribute [export_dafny] DiscreteGaussianSampleLoop +-- attribute [export_dafny] DiscreteGaussianSample diff --git a/SampCert/Extractor/Abstract.lean b/SampCert/Extractor/Abstract.lean index 1209afdb..f3b13841 100644 --- a/SampCert/Extractor/Abstract.lean +++ b/SampCert/Extractor/Abstract.lean @@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import Mathlib.Order.SetNotation - class Capsid (CapsM : Type u -> Type v) extends Monad CapsM where capsWhile : (cond : T → Bool) → (body : T → CapsM T) → T → CapsM T + section capsid_wf variable {CapsM : Type u -> Type v} [C : Capsid CapsM] variable {T : Type u} diff --git a/SampCert/Extractor/Translate.lean b/SampCert/Extractor/Translate.lean index 3d8f1e4c..f1c584ae 100644 --- a/SampCert/Extractor/Translate.lean +++ b/SampCert/Extractor/Translate.lean @@ -13,7 +13,7 @@ namespace Lean.ToDafny def IsWFMonadic (e: Expr) : MetaM Bool := match e with - | .app (.const ``MyAbstractLanguage.FOO ..) _ => return true + | .app (.const ``Capsid ..) _ => return true | .app .. => return true -- Need to work out details of this one, related to translation of dependent types | .forallE _ _ range _ => IsWFMonadic range | _ => return false -- throwError "IsWFMonadic {e}" @@ -32,7 +32,7 @@ partial def toDafnyTyp (env : List String) (e : Expr) : MetaM Typ := do | .mvar .. => throwError "toDafnyTyp: not supported -- meta variable {e}" | .sort .. => throwError "toDafnyTyp: not supported -- sort {e}" | .const ``Nat .. => return .nat - | .const ``PNat .. => return .pos + -- | .const ``PNat .. => return .pos | .const ``Bool .. => return .bool | .const ``Int .. => return .int | .const .. => throwError "toDafnyTyp: not supported -- constant {e}" @@ -40,7 +40,7 @@ partial def toDafnyTyp (env : List String) (e : Expr) : MetaM Typ := do if let .const name .. := fn then match name with | ``Prod => return .prod (← toDafnyTyp env args[0]!) (← toDafnyTyp env args[1]!) - | ``SLang => return (← toDafnyTyp env args[0]!) + | ``Capsid => return (← toDafnyTyp env args[0]!) | _ => return .dependent (← toDafnyExpr "dummycalledfromtoDafnyTyp" env e) else throwError "toDafnyExpr: OOL {fn} {args}" ) @@ -70,8 +70,7 @@ partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM | ``ite => return .ite (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[3]!) (← toDafnyExpr dname env args[4]!) | ``dite => return .ite (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname ("dummy" :: env) (chopLambda args[3]!)) (← toDafnyExpr dname ("dummy" :: env) (chopLambda args[4]!)) | ``throwThe => return .throw (← toDafnyExpr dname env args[4]!) - | ``MyAbstractLanguage.while_ => return .prob_while (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``SLang.probUntil => return .prob_until (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) + | ``Capsid.capsWhile => return .prob_while (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) | ``OfNat.ofNat => toDafnyExpr dname env args[1]! | ``HAdd.hAdd => return .binop .addition (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) | ``HSub.hSub => return .binop .substraction (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) @@ -88,20 +87,20 @@ partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM | ``LE.le => return .binop .leastequal (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) | ``GT.gt => return .binop .greater (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) | ``GE.ge => return .binop .greaterequal (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``Nat.log => return .binop .log (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) + -- | ``Nat.log => return .binop .log (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) | ``decide => toDafnyExpr dname env args[0]! - | ``_root_.Rat.den => return .unop .denominator (← toDafnyExpr dname env args[0]!) - | ``_root_.Rat.num => return .unop .numerator (← toDafnyExpr dname env args[0]!) + -- | ``_root_.Rat.den => return .unop .denominator (← toDafnyExpr dname env args[0]!) + -- | ``_root_.Rat.num => return .unop .numerator (← toDafnyExpr dname env args[0]!) | ``Nat.cast => toDafnyExpr dname env args[2]! | ``Int.cast => toDafnyExpr dname env args[2]! | ``Prod.fst => return .proj (← toDafnyExpr dname env args[2]!) 1 | ``Prod.snd => return .proj (← toDafnyExpr dname env args[2]!) 2 | ``Prod.mk => return .pair (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) | ``Neg.neg => return .unop .minus (← toDafnyExpr dname env args[2]!) - | ``abs => return .unop .abs (← toDafnyExpr dname env args[2]!) + -- | ``abs => return .unop .abs (← toDafnyExpr dname env args[2]!) | ``Int.natAbs => return .unop .abs (← toDafnyExpr dname env args[0]!) | ``OfScientific.ofScientific => toDafnyExpr dname env args[4]! - | ``PNat.val => toDafnyExpr dname env args[0]! + -- | ``PNat.val => toDafnyExpr dname env args[0]! | ``Subtype.mk => toDafnyExpr dname env args[2]! | ``Int.sub => return .binop .substraction (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) | _ => @@ -138,7 +137,7 @@ end def toDafnyTypTop (env : List String) (e: Expr) : MetaM ((List Typ) × Typ) := do match e with | .forallE _ (.sort _) _ _ => throwError "toDafnyTypTop: Polymorphism not supported yet" - | (.app (.const ``SLang ..) arg) => return ([],← toDafnyTyp [] arg) + | (.app (.const ``Capsid ..) arg) => return ([],← toDafnyTyp [] arg) | .forallE binder domain range _ => let nenv := binder.toString :: env let r ← toDafnyTypTop nenv range From 1f61a387c57ab372f34d88c8aedca96a03dd260e Mon Sep 17 00:00:00 2001 From: de Medeiros Date: Thu, 30 May 2024 15:55:07 -0400 Subject: [PATCH 5/7] workaround to read a capsid --- SampCert/Extraction.lean | 17 ++- SampCert/Extractor/Abstract.lean | 5 + SampCert/Extractor/Translate.lean | 166 ++++++++++++++++++------------ 3 files changed, 118 insertions(+), 70 deletions(-) diff --git a/SampCert/Extraction.lean b/SampCert/Extraction.lean index 01b7f1ef..5a333a4e 100644 --- a/SampCert/Extraction.lean +++ b/SampCert/Extraction.lean @@ -28,12 +28,25 @@ Additionally, the following names are protected: - ``UniformPowerOfTwoSample`` -/ -instance : Capsid SLang where +-- instance : Capsid SLang where +-- capsWhile := probWhile + +instance SLang_Capsid : Capsid SLang where capsWhile := probWhile +-- MARKUSDE: Can't figure out how to get it to synthesize a typeclass instance +-- at export time, so I'll pass them in instead. Maybe a macro + + + +def UniformCapsid := (SLang_Capsid, UniformSample) + +attribute [export_dafny] UniformCapsid + + + --- attribute [export_dafny] UniformSample -- attribute [export_dafny] BernoulliSample -- attribute [export_dafny] BernoulliExpNegSampleUnitLoop -- attribute [export_dafny] BernoulliExpNegSampleUnitAux diff --git a/SampCert/Extractor/Abstract.lean b/SampCert/Extractor/Abstract.lean index f3b13841..147b70c9 100644 --- a/SampCert/Extractor/Abstract.lean +++ b/SampCert/Extractor/Abstract.lean @@ -4,6 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ +-- class Capsid (T : Type) (M : Type -> Type) where +-- CapsidM_inst : Monad M +-- capsWhile : (T → Bool) → (T → M T) → (init : T) → M T + + class Capsid (CapsM : Type u -> Type v) extends Monad CapsM where capsWhile : (cond : T → Bool) → (body : T → CapsM T) → T → CapsM T diff --git a/SampCert/Extractor/Translate.lean b/SampCert/Extractor/Translate.lean index f1c584ae..af3a9261 100644 --- a/SampCert/Extractor/Translate.lean +++ b/SampCert/Extractor/Translate.lean @@ -11,11 +11,22 @@ import SampCert.Extractor.Abstract namespace Lean.ToDafny -def IsWFMonadic (e: Expr) : MetaM Bool := +/-- +Check if the program is a tuple, whose first element is of type Capsid. +-/ +def readCapsid (e : Expr) : MetaM (Option (Name × Expr)) := + IO.println s!" - Reading Capsid {e}" >>= fun _ => + match e with + | .app (.app (.const ``Prod [1, 0]) (.app (.const ``Capsid _) (.const t _))) f => do + return (some (t, f)) + | _ => return none + +def IsWFMonadic (capsidM : Name) (e: Expr) : MetaM Bool := + IO.println s!" - Checking if {e} is WF monadic" >>= fun _ => match e with - | .app (.const ``Capsid ..) _ => return true + | .app (.const n ..) _ => return (n = capsidM) | .app .. => return true -- Need to work out details of this one, related to translation of dependent types - | .forallE _ _ range _ => IsWFMonadic range + | .forallE _ _ range _ => IsWFMonadic capsidM range | _ => return false -- throwError "IsWFMonadic {e}" def chopLambda (e : Expr) : Expr := @@ -25,23 +36,23 @@ def chopLambda (e : Expr) : Expr := mutual -partial def toDafnyTyp (env : List String) (e : Expr) : MetaM Typ := do +partial def toDafnyTyp (capsidM : Name) (env : List String) (e : Expr) : MetaM Typ := do match e with | .bvar .. => throwError "toDafnyTyp: not supported -- bound variable {e}" | .fvar .. => throwError "toDafnyTyp: not supported -- free variable {e}" | .mvar .. => throwError "toDafnyTyp: not supported -- meta variable {e}" | .sort .. => throwError "toDafnyTyp: not supported -- sort {e}" | .const ``Nat .. => return .nat - -- | .const ``PNat .. => return .pos + | .const ``PNat .. => return .pos | .const ``Bool .. => return .bool | .const ``Int .. => return .int | .const .. => throwError "toDafnyTyp: not supported -- constant {e}" | .app .. => (e.withApp fun fn args => do if let .const name .. := fn then match name with - | ``Prod => return .prod (← toDafnyTyp env args[0]!) (← toDafnyTyp env args[1]!) - | ``Capsid => return (← toDafnyTyp env args[0]!) - | _ => return .dependent (← toDafnyExpr "dummycalledfromtoDafnyTyp" env e) + | ``Prod => return .prod (← toDafnyTyp capsidM env args[0]!) (← toDafnyTyp capsidM env args[1]!) + | ``Capsid => return (← toDafnyTyp capsidM env args[0]!) + | _ => return .dependent (← toDafnyExpr capsidM "dummycalledfromtoDafnyTyp" env e) else throwError "toDafnyExpr: OOL {fn} {args}" ) | .lam .. => throwError "toDafnyTyp: not supported -- lambda abstraction {e}" @@ -51,7 +62,7 @@ partial def toDafnyTyp (env : List String) (e : Expr) : MetaM Typ := do | .mdata .. => throwError "toDafnyTyp: not supported -- metadata {e}" | .proj .. => throwError "toDafnyTyp: not supported -- projection {e}" -partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM Expression := do +partial def toDafnyExpr (capsidM : Name) (dname : String) (env : List String) (e : Expr) : MetaM Expression := do match e with | .bvar i => return .name (env[i]!) | .fvar .. => throwError "toDafnyExpr: not supported -- free variable {e}" @@ -65,46 +76,46 @@ partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM if let .const name .. := fn then let info ← getConstInfo name match name with - | ``pure => return .pure (← toDafnyExpr dname env args[3]!) - | ``bind => return .bind (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``ite => return .ite (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[3]!) (← toDafnyExpr dname env args[4]!) - | ``dite => return .ite (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname ("dummy" :: env) (chopLambda args[3]!)) (← toDafnyExpr dname ("dummy" :: env) (chopLambda args[4]!)) - | ``throwThe => return .throw (← toDafnyExpr dname env args[4]!) - | ``Capsid.capsWhile => return .prob_while (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``OfNat.ofNat => toDafnyExpr dname env args[1]! - | ``HAdd.hAdd => return .binop .addition (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``HSub.hSub => return .binop .substraction (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``HMul.hMul => return .binop .multiplication (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``HDiv.hDiv => return .binop .division (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``HPow.hPow => return .binop .pow (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``HMod.hMod => return .binop .mod (← toDafnyExpr dname env args[4]!) (← toDafnyExpr dname env args[5]!) - | ``Eq => return .binop .equality (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) - | ``Ne => return .binop .inequality (← toDafnyExpr dname env args[1]!) (← toDafnyExpr dname env args[2]!) - | ``And => return .binop .conjunction (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) - | ``Or => return .binop .disjunction (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) - | ``Not => return .unop .negation (← toDafnyExpr dname env args[0]!) - | ``LT.lt => return .binop .least (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``LE.le => return .binop .leastequal (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``GT.gt => return .binop .greater (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``GE.ge => return .binop .greaterequal (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - -- | ``Nat.log => return .binop .log (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) - | ``decide => toDafnyExpr dname env args[0]! - -- | ``_root_.Rat.den => return .unop .denominator (← toDafnyExpr dname env args[0]!) - -- | ``_root_.Rat.num => return .unop .numerator (← toDafnyExpr dname env args[0]!) - | ``Nat.cast => toDafnyExpr dname env args[2]! - | ``Int.cast => toDafnyExpr dname env args[2]! - | ``Prod.fst => return .proj (← toDafnyExpr dname env args[2]!) 1 - | ``Prod.snd => return .proj (← toDafnyExpr dname env args[2]!) 2 - | ``Prod.mk => return .pair (← toDafnyExpr dname env args[2]!) (← toDafnyExpr dname env args[3]!) - | ``Neg.neg => return .unop .minus (← toDafnyExpr dname env args[2]!) - -- | ``abs => return .unop .abs (← toDafnyExpr dname env args[2]!) - | ``Int.natAbs => return .unop .abs (← toDafnyExpr dname env args[0]!) - | ``OfScientific.ofScientific => toDafnyExpr dname env args[4]! - -- | ``PNat.val => toDafnyExpr dname env args[0]! - | ``Subtype.mk => toDafnyExpr dname env args[2]! - | ``Int.sub => return .binop .substraction (← toDafnyExpr dname env args[0]!) (← toDafnyExpr dname env args[1]!) + | ``pure => return .pure (← toDafnyExpr capsidM dname env args[3]!) + | ``bind => return .bind (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``ite => return .ite (← toDafnyExpr capsidM dname env args[1]!) (← toDafnyExpr capsidM dname env args[3]!) (← toDafnyExpr capsidM dname env args[4]!) + | ``dite => return .ite (← toDafnyExpr capsidM dname env args[1]!) (← toDafnyExpr capsidM dname ("dummy" :: env) (chopLambda args[3]!)) (← toDafnyExpr capsidM dname ("dummy" :: env) (chopLambda args[4]!)) + | ``throwThe => return .throw (← toDafnyExpr capsidM dname env args[4]!) + | ``Capsid.capsWhile => return .prob_while (← toDafnyExpr capsidM dname env args[1]!) (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) + | ``OfNat.ofNat => toDafnyExpr capsidM dname env args[1]! + | ``HAdd.hAdd => return .binop .addition (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``HSub.hSub => return .binop .substraction (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``HMul.hMul => return .binop .multiplication (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``HDiv.hDiv => return .binop .division (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``HPow.hPow => return .binop .pow (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``HMod.hMod => return .binop .mod (← toDafnyExpr capsidM dname env args[4]!) (← toDafnyExpr capsidM dname env args[5]!) + | ``Eq => return .binop .equality (← toDafnyExpr capsidM dname env args[1]!) (← toDafnyExpr capsidM dname env args[2]!) + | ``Ne => return .binop .inequality (← toDafnyExpr capsidM dname env args[1]!) (← toDafnyExpr capsidM dname env args[2]!) + | ``And => return .binop .conjunction (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) + | ``Or => return .binop .disjunction (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) + | ``Not => return .unop .negation (← toDafnyExpr capsidM dname env args[0]!) + | ``LT.lt => return .binop .least (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) + | ``LE.le => return .binop .leastequal (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) + | ``GT.gt => return .binop .greater (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) + | ``GE.ge => return .binop .greaterequal (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) + -- | ``Nat.log => return .binop .log (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) + | ``decide => toDafnyExpr capsidM dname env args[0]! + -- | ``_root_.Rat.den => return .unop .denominator (← toDafnyExpr capsidM dname env args[0]!) + -- | ``_root_.Rat.num => return .unop .numerator (← toDafnyExpr capsidM dname env args[0]!) + | ``Nat.cast => toDafnyExpr capsidM dname env args[2]! + | ``Int.cast => toDafnyExpr capsidM dname env args[2]! + | ``Prod.fst => return .proj (← toDafnyExpr capsidM dname env args[2]!) 1 + | ``Prod.snd => return .proj (← toDafnyExpr capsidM dname env args[2]!) 2 + | ``Prod.mk => return .pair (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) + | ``Neg.neg => return .unop .minus (← toDafnyExpr capsidM dname env args[2]!) + -- | ``abs => return .unop .abs (← toDafnyExpr capsidM dname env args[2]!) + | ``Int.natAbs => return .unop .abs (← toDafnyExpr capsidM dname env args[0]!) + | ``OfScientific.ofScientific => toDafnyExpr capsidM dname env args[4]! + -- | ``PNat.val => toDafnyExpr capsidM dname env args[0]! + | ``Subtype.mk => toDafnyExpr capsidM dname env args[2]! + | ``Int.sub => return .binop .substraction (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) | _ => - if ← IsWFMonadic info.type + if ← IsWFMonadic capsidM info.type then let st : State := extension.getState (← getEnv) if let some defn := st.glob.find? name.toString @@ -113,20 +124,20 @@ partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM let args1 := defn.inParamType.zip args.toList let args2 := args1.filter (λ (x,_) => match x with | .dependent _ => false | _ => true) let args3 := args2.map (λ (_,y) => y) - let args' ← args3.mapM (toDafnyExpr dname env) + let args' ← args3.mapM (toDafnyExpr capsidM dname env) return .monadic name.toString args' else - let args' ← args.mapM (toDafnyExpr dname env) + let args' ← args.mapM (toDafnyExpr capsidM dname env) return .monadic name.toString args'.toList else throwError "toDafnyExpr: not supported -- application of {fn} to {args}, info.type {info.type}" else if let .bvar _ := fn -- Coin... - then return .monadic dname [(← toDafnyExpr dname env args[0]!)] + then return .monadic dname [(← toDafnyExpr capsidM dname env args[0]!)] else throwError "toDafnyExpr: OOL {fn} {args}" ) - | .lam binderName _ body _ => return (.lam binderName.toString (← toDafnyExpr dname (binderName.toString :: env) body)) + | .lam binderName _ body _ => return (.lam binderName.toString (← toDafnyExpr capsidM dname (binderName.toString :: env) body)) | .forallE .. => throwError "toDafnyExpr: not supported -- pi {e}" - | .letE lhs _ rhs body _ => return (.letb lhs.toString (← toDafnyExpr dname env rhs) (← toDafnyExpr dname (lhs.toString :: env) body)) + | .letE lhs _ rhs body _ => return (.letb lhs.toString (← toDafnyExpr capsidM dname env rhs) (← toDafnyExpr capsidM dname (lhs.toString :: env) body)) | .lit (.natVal n) => return .num n | .lit (.strVal s) => return .str s | .mdata .. => throwError "toDafnyExpr: not supported -- meta {e}" @@ -134,17 +145,20 @@ partial def toDafnyExpr (dname : String) (env : List String) (e : Expr) : MetaM end -def toDafnyTypTop (env : List String) (e: Expr) : MetaM ((List Typ) × Typ) := do +def toDafnyTypTop (capsidM : Name) (env : List String) (e: Expr) : MetaM ((List Typ) × Typ) := do match e with | .forallE _ (.sort _) _ _ => throwError "toDafnyTypTop: Polymorphism not supported yet" - | (.app (.const ``Capsid ..) arg) => return ([],← toDafnyTyp [] arg) + | (.app (.const t ..) arg) => + if t = capsidM + then return ([],← toDafnyTyp capsidM [] arg) + else throwError "toDafnyTypTop: error on {e} (1)" | .forallE binder domain range _ => let nenv := binder.toString :: env - let r ← toDafnyTypTop nenv range - return ((← toDafnyTyp env domain) :: r.1 , r.2) - | _ => throwError "toDafnyTypTop: error" + let r ← toDafnyTypTop capsidM nenv range + return ((← toDafnyTyp capsidM env domain) :: r.1 , r.2) + | _ => throwError "toDafnyTypTop: error on {e} (2)" -partial def toDafnyExprTop (dname : String) (num_args : Nat) (names : List String) (e : Expr) : MetaM (List String × Expression) := do +partial def toDafnyExprTop (capsidM : Name) (dname : String) (num_args : Nat) (names : List String) (e : Expr) : MetaM (List String × Expression) := do match e with | .bvar .. => throwError "toDafnyExprTop: not supported -- bound variable {e}" | .fvar .. => throwError "toDafnyExprTop: not supported -- free variable {e}" @@ -154,16 +168,16 @@ partial def toDafnyExprTop (dname : String) (num_args : Nat) (names : List Strin | .app .. => e.withApp fun fn args => if let .const ``WellFounded.fix .. := fn - then toDafnyExprTop dname num_args names (args[4]!) + then toDafnyExprTop capsidM dname num_args names (args[4]!) else throwError "toDafnyExprTop: not supported -- application {e}" | .lam binderName _ body _ => let sig_names := names ++ [binderName.toString] if num_args = List.length names + 1 then match body with - | (.lam _ _ body _) => return (sig_names, ← toDafnyExpr dname ("dummy" :: sig_names.reverse) (chopLambda body)) - | _ => return (sig_names, ← toDafnyExpr dname sig_names.reverse body) - else toDafnyExprTop dname num_args sig_names body + | (.lam _ _ body _) => return (sig_names, ← toDafnyExpr capsidM dname ("dummy" :: sig_names.reverse) (chopLambda body)) + | _ => return (sig_names, ← toDafnyExpr capsidM dname sig_names.reverse body) + else toDafnyExprTop capsidM dname num_args sig_names body | .forallE .. => throwError "toDafnyExprTop: not supported -- pi {e}" | .letE .. => throwError "toDafnyExprTop: not supported -- let expression {e}" | .lit .. => throwError "toDafnyExprTop: not supported -- literals {e}" @@ -175,16 +189,32 @@ def printParamTypes (params : List Typ) : String := | [] => "" | param :: params => s!"{param.print}, {printParamTypes params}" + +/-- +Entry point for converting a declaration (by name) into the IR + +Expects a pair of a Capsid instance, and a program. +-/ def toDafnySLangDefIn (declName: Name) : MetaM MDef := do let info ← getConstInfo declName + IO.println s!" - Working on {declName}" match info with | ConstantInfo.defnInfo _ => - if ← IsWFMonadic info.type then - let (inParamTyp, outParamTyp) ← toDafnyTypTop [] info.type - let (inParam, body) ← toDafnyExprTop declName.toString (List.length inParamTyp) [] info.value! + IO.println s!" - Type: {info.type}" + + -- Try to read Capsid information + let capsidV <- readCapsid (info.type) + match capsidV with + | some (capsidM, progT) => do + IO.println s!" - Capsid monad: {capsidM}" + let isMonadic <- (IsWFMonadic capsidM progT) + if !isMonadic then throwError "Program type {progT} is not monadic" + + let (inParamTyp, outParamTyp) ← toDafnyTypTop capsidM [] progT + let (inParam, body) ← toDafnyExprTop capsidM declName.toString (List.length inParamTyp) [] info.value! let defn := MDef.mk (declName.toString) inParamTyp outParamTyp inParam body return defn - else throwError "This extractor works for SLang monadic computations only (1)" - | _ => throwError "This extractor works for SLang monadic computations only (2)" + | _ => throwError "Failed to read Capsid information (1)" + | _ => throwError "Failed to read Capsid information (2)" end Lean.ToDafny From 59c4c9c8caaa81e35a1ef6d2ea18be44e4dee42b Mon Sep 17 00:00:00 2001 From: de Medeiros Date: Thu, 30 May 2024 16:50:05 -0400 Subject: [PATCH 6/7] (heavy WIP) push information through extractor --- SampCert/Extraction.lean | 13 +++----- SampCert/Extractor/Translate.lean | 52 ++++++++++++++++++++++++------- 2 files changed, 46 insertions(+), 19 deletions(-) diff --git a/SampCert/Extraction.lean b/SampCert/Extraction.lean index 5a333a4e..4806156b 100644 --- a/SampCert/Extraction.lean +++ b/SampCert/Extraction.lean @@ -35,18 +35,15 @@ instance SLang_Capsid : Capsid SLang where capsWhile := probWhile +def testSLang : SLang Nat := (return 5) >>= (fun x => x) + -- MARKUSDE: Can't figure out how to get it to synthesize a typeclass instance -- at export time, so I'll pass them in instead. Maybe a macro +def testCapsid := (SLang_Capsid, UniformSample) +attribute [export_dafny] testCapsid - -def UniformCapsid := (SLang_Capsid, UniformSample) - -attribute [export_dafny] UniformCapsid - - - - +-- attribute [export_dafny] UniformSample -- attribute [export_dafny] BernoulliSample -- attribute [export_dafny] BernoulliExpNegSampleUnitLoop -- attribute [export_dafny] BernoulliExpNegSampleUnitAux diff --git a/SampCert/Extractor/Translate.lean b/SampCert/Extractor/Translate.lean index af3a9261..fd551769 100644 --- a/SampCert/Extractor/Translate.lean +++ b/SampCert/Extractor/Translate.lean @@ -9,6 +9,9 @@ import SampCert.Extractor.IR import SampCert.Extractor.Extension import SampCert.Extractor.Abstract +import Mathlib.Data.Nat.Log +import Mathlib.Data.PNat.Defs + namespace Lean.ToDafny /-- @@ -21,6 +24,14 @@ def readCapsid (e : Expr) : MetaM (Option (Name × Expr)) := return (some (t, f)) | _ => return none +def readCapsidProg (e : Expr) : MetaM (Option (Name × Name)) := + IO.println s!" - Reading Capsid Program {e}" >>= fun _ => + match e with + | .app (.app _ (.const e1 _)) (.const e2 _) => return some (e1, e2) + | _ => do + IO.println s!"Capsid program read failure" + return none + def IsWFMonadic (capsidM : Name) (e: Expr) : MetaM Bool := IO.println s!" - Checking if {e} is WF monadic" >>= fun _ => match e with @@ -63,6 +74,7 @@ partial def toDafnyTyp (capsidM : Name) (env : List String) (e : Expr) : MetaM T | .proj .. => throwError "toDafnyTyp: not supported -- projection {e}" partial def toDafnyExpr (capsidM : Name) (dname : String) (env : List String) (e : Expr) : MetaM Expression := do + IO.println s!" + translate {e}" match e with | .bvar i => return .name (env[i]!) | .fvar .. => throwError "toDafnyExpr: not supported -- free variable {e}" @@ -98,10 +110,10 @@ partial def toDafnyExpr (capsidM : Name) (dname : String) (env : List String) (e | ``LE.le => return .binop .leastequal (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) | ``GT.gt => return .binop .greater (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) | ``GE.ge => return .binop .greaterequal (← toDafnyExpr capsidM dname env args[2]!) (← toDafnyExpr capsidM dname env args[3]!) - -- | ``Nat.log => return .binop .log (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) + | ``Nat.log => return .binop .log (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) | ``decide => toDafnyExpr capsidM dname env args[0]! - -- | ``_root_.Rat.den => return .unop .denominator (← toDafnyExpr capsidM dname env args[0]!) - -- | ``_root_.Rat.num => return .unop .numerator (← toDafnyExpr capsidM dname env args[0]!) + | ``_root_.Rat.den => return .unop .denominator (← toDafnyExpr capsidM dname env args[0]!) + | ``_root_.Rat.num => return .unop .numerator (← toDafnyExpr capsidM dname env args[0]!) | ``Nat.cast => toDafnyExpr capsidM dname env args[2]! | ``Int.cast => toDafnyExpr capsidM dname env args[2]! | ``Prod.fst => return .proj (← toDafnyExpr capsidM dname env args[2]!) 1 @@ -111,7 +123,7 @@ partial def toDafnyExpr (capsidM : Name) (dname : String) (env : List String) (e -- | ``abs => return .unop .abs (← toDafnyExpr capsidM dname env args[2]!) | ``Int.natAbs => return .unop .abs (← toDafnyExpr capsidM dname env args[0]!) | ``OfScientific.ofScientific => toDafnyExpr capsidM dname env args[4]! - -- | ``PNat.val => toDafnyExpr capsidM dname env args[0]! + | ``PNat.val => toDafnyExpr capsidM dname env args[0]! | ``Subtype.mk => toDafnyExpr capsidM dname env args[2]! | ``Int.sub => return .binop .substraction (← toDafnyExpr capsidM dname env args[0]!) (← toDafnyExpr capsidM dname env args[1]!) | _ => @@ -167,9 +179,15 @@ partial def toDafnyExprTop (capsidM : Name) (dname : String) (num_args : Nat) (n | .const .. => throwError "toDafnyExprTop: not supported -- constant {e}" | .app .. => e.withApp fun fn args => - if let .const ``WellFounded.fix .. := fn - then toDafnyExprTop capsidM dname num_args names (args[4]!) - else throwError "toDafnyExprTop: not supported -- application {e}" + match fn with + | (.const ``WellFounded.fix ..) => toDafnyExprTop capsidM dname num_args names (args[4]!) + -- Very wrong + -- | (.const ``pure ..) => do + -- let to_translate := args[3]! + -- let de <- toDafnyExpr capsidM dname names to_translate + -- IO.println s!" - PURE: translated value {to_translate}" + -- return (names, de) + | _ => throwError "toDafnyExprTop: not supported -- application {e}" | .lam binderName _ body _ => let sig_names := names ++ [binderName.toString] if num_args = List.length names + 1 @@ -209,11 +227,23 @@ def toDafnySLangDefIn (declName: Name) : MetaM MDef := do IO.println s!" - Capsid monad: {capsidM}" let isMonadic <- (IsWFMonadic capsidM progT) if !isMonadic then throwError "Program type {progT} is not monadic" - let (inParamTyp, outParamTyp) ← toDafnyTypTop capsidM [] progT - let (inParam, body) ← toDafnyExprTop capsidM declName.toString (List.length inParamTyp) [] info.value! - let defn := MDef.mk (declName.toString) inParamTyp outParamTyp inParam body - return defn + let p <- readCapsidProg info.value! + match p with + | none => throwError "program is malformed (should be impossible if normalized)" + | some (capsid_instance_name, program_name) => do + IO.println s!" - Read Capsid instance name {capsid_instance_name}" + IO.println s!" - Read program value name {program_name}" + + -- Now I need to get the program body from the program mane + let progInfo <- getConstInfoDefn program_name + IO.println s!" - Got program value {progInfo.value}" + let capsidInfo <- getConstInfoDefn capsid_instance_name + IO.println s!" - Got capsid value {capsidInfo.value}" + + let (inParam, body) ← toDafnyExprTop capsidM declName.toString (List.length inParamTyp) [] (progInfo.value) + let defn := MDef.mk (declName.toString) inParamTyp outParamTyp inParam body + return defn | _ => throwError "Failed to read Capsid information (1)" | _ => throwError "Failed to read Capsid information (2)" From 8a98b43349e1443a5e1e6cdf95a2b39ddf0d1dd3 Mon Sep 17 00:00:00 2001 From: de Medeiros Date: Thu, 30 May 2024 17:15:11 -0400 Subject: [PATCH 7/7] encapsulate --- SampCert/Extraction.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/SampCert/Extraction.lean b/SampCert/Extraction.lean index 4806156b..578fff38 100644 --- a/SampCert/Extraction.lean +++ b/SampCert/Extraction.lean @@ -37,9 +37,11 @@ instance SLang_Capsid : Capsid SLang where def testSLang : SLang Nat := (return 5) >>= (fun x => x) --- MARKUSDE: Can't figure out how to get it to synthesize a typeclass instance --- at export time, so I'll pass them in instead. Maybe a macro -def testCapsid := (SLang_Capsid, UniformSample) +-- Get a Capsid instance from typeclass inference +def encapsulate {T U : Type*} [HC : Capsid M] (f : T -> M U) : (Capsid M × (T -> M U)) := (HC, f) + +-- MARKUSDE: Push encapsulate into the attribute? +def testCapsid := encapsulate UniformSample attribute [export_dafny] testCapsid