From 8cd8ed2b3340ec6fe9ac4880a03cfa1439ba0110 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Mon, 27 Mar 2023 00:04:47 -0300 Subject: [PATCH 1/5] Removed domain field from lambdas --- Yatima/Common/LightData.lean | 12 ++++----- Yatima/Common/ToLDON.lean | 2 +- Yatima/ContAddr/ContAddr.lean | 4 +-- Yatima/Datatypes/Expr.lean | 2 +- Yatima/Typechecker/Infer.lean | 44 ++++++++++++++++++++------------ Yatima/Typechecker/Printing.lean | 4 +-- 6 files changed, 40 insertions(+), 28 deletions(-) diff --git a/Yatima/Common/LightData.lean b/Yatima/Common/LightData.lean index 1f28fdac..6e34e9c7 100644 --- a/Yatima/Common/LightData.lean +++ b/Yatima/Common/LightData.lean @@ -74,23 +74,23 @@ instance : Encodable Lurk.F LightData where decode x := return (.ofNat $ ← dec x) def exprToLightData : Expr → LightData - | .sort x => .cell #[false, x] - | .lit x => .cell #[true, x] + | .sort x => .cell #[0, x] + | .lit x => .cell #[1, x] + | .lam x => .cell #[2, exprToLightData x] | .var x y => .cell #[0, x, y] | .const x y => .cell #[1, x, y] | .app x y => .cell #[2, exprToLightData x, exprToLightData y] - | .lam x y => .cell #[3, exprToLightData x, exprToLightData y] | .pi x y => .cell #[4, exprToLightData x, exprToLightData y] | .proj x y => .cell #[5, x, exprToLightData y] | .letE x y z => .cell #[false, exprToLightData x, exprToLightData y, exprToLightData z] partial def lightDataToExpr : LightData → Except String Expr - | .cell #[false, x] => return .sort (← lightDataToUniv x) - | .cell #[true, x] => return .lit (← dec x) + | .cell #[0, x] => return .sort (← lightDataToUniv x) + | .cell #[1, x] => return .lit (← dec x) + | .cell #[2, x] => return .lam (← lightDataToExpr x) | .cell #[0, x, y] => return .var (← dec x) (← dec y) | .cell #[1, x, y] => return .const (← dec x) (← dec y) | .cell #[2, x, y] => return .app (← lightDataToExpr x) (← lightDataToExpr y) - | .cell #[3, x, y] => return .lam (← lightDataToExpr x) (← lightDataToExpr y) | .cell #[4, x, y] => return .pi (← lightDataToExpr x) (← lightDataToExpr y) | .cell #[5, x, y] => return .proj (← dec x) (← lightDataToExpr y) | .cell #[false, x, y, z] => diff --git a/Yatima/Common/ToLDON.lean b/Yatima/Common/ToLDON.lean index 8fc73454..d7fd6533 100644 --- a/Yatima/Common/ToLDON.lean +++ b/Yatima/Common/ToLDON.lean @@ -43,7 +43,7 @@ def Expr.toLDON : Expr → LDON | .sort u => ([1, u] : List LDON) | .const ptr lvls => ([2, ptr, lvls.map IR.Univ.toLDON] : List LDON) | .app fn arg => ([3, fn.toLDON, arg.toLDON] : List LDON) - | .lam name body => ([4, name.toLDON, body.toLDON] : List LDON) + | .lam body => ([4, body.toLDON] : List LDON) | .pi x y => ([5, x.toLDON, y.toLDON] : List LDON) | .letE x y z => ([6, x.toLDON, y.toLDON, z.toLDON] : List LDON) | .lit l => ([7, l] : List LDON) diff --git a/Yatima/ContAddr/ContAddr.lean b/Yatima/ContAddr/ContAddr.lean index 0b4e5b1d..c0981aa0 100644 --- a/Yatima/ContAddr/ContAddr.lean +++ b/Yatima/ContAddr/ContAddr.lean @@ -305,8 +305,8 @@ partial def contAddrExpr : Lean.Expr → ContAddrM Expr return .var idx univs | none => return .const (← contAddrConst $ ← getLeanConstant name) univs | .app fnc arg => return .app (← contAddrExpr fnc) (← contAddrExpr arg) - | .lam name typ bod _ => - return .lam (← contAddrExpr typ) (← withBinder name $ contAddrExpr bod) + | .lam name _ bod _ => + return .lam (← withBinder name $ contAddrExpr bod) | .forallE name dom img _ => return .pi (← contAddrExpr dom) (← withBinder name $ contAddrExpr img) | .letE name typ exp bod _ => diff --git a/Yatima/Datatypes/Expr.lean b/Yatima/Datatypes/Expr.lean index 971e3863..e69ee7e4 100644 --- a/Yatima/Datatypes/Expr.lean +++ b/Yatima/Datatypes/Expr.lean @@ -15,7 +15,7 @@ inductive Expr | sort : Univ → Expr | const : Lurk.F → List Univ → Expr | app : Expr → Expr → Expr - | lam : Expr → Expr → Expr + | lam : Expr → Expr | pi : Expr → Expr → Expr | letE : Expr → Expr → Expr → Expr | lit : Literal → Expr diff --git a/Yatima/Typechecker/Infer.lean b/Yatima/Typechecker/Infer.lean index dd7eb50c..4b51ae58 100644 --- a/Yatima/Typechecker/Infer.lean +++ b/Yatima/Typechecker/Infer.lean @@ -82,12 +82,33 @@ mutual Checks if `term : IR.Expr` has type `type : SusValue`. Returns the typed IR for `term` -/ partial def check (term : IR.Expr) (type : SusValue) : TypecheckM TypedExpr := do - let (term, inferType) ← infer term - if !(← eqSortInfo inferType type) then - throw s!"Term: {← ppTypedExpr term}\nInfo mismatch:\n{repr inferType.info}\n\nnot equal to\n{repr type.info}\n\nExpected type: {← ppValue type.get}\nInferred type: {← ppValue inferType.get}" - if !(← equal (← read).lvl type inferType) then - throw s!"Expected type {← ppValue type.get}, found type {← ppValue inferType.get}" - pure term + match term with + | .lam bod => + match type.get with + | .pi dom img env => + let lvl := (← read).lvl + let var := mkSusVar (← infoFromType dom) lvl + let imgVal := suspend img { (← read) with env := env.extendWith var } (← get) + let bod ← withExtendedCtx var dom $ check bod imgVal + let term := ⟨lamInfo bod.info, .lam (← quoteTyped lvl ⟨[], []⟩ dom.getTyped) bod⟩ + pure term + | _ => throw "Term should not be a lambda" + | .letE expType exp bod => + let (expType, _) ← isSort expType + let ctx ← read + let expTypeVal := suspend expType ctx (← get) + let exp ← check exp expTypeVal + let expVal := suspend exp ctx (← get) + let bod ← withExtendedCtx expVal expTypeVal $ check bod type + let term := ⟨bod.info, .letE expType exp bod⟩ + return term + | _ => + let (term, inferType) ← infer term + if !(← eqSortInfo inferType type) then + throw s!"Term: {← ppTypedExpr term}\nInfo mismatch:\n{repr inferType.info}\n\nnot equal to\n{repr type.info}\n\nExpected type: {← ppValue type.get}\nInferred type: {← ppValue inferType.get}" + if !(← equal (← read).lvl type inferType) then + throw s!"Expected type {← ppValue type.get}, found type {← ppValue inferType.get}" + pure term /-- Infers the type of `term : IR.Expr`. Returns the typed IR for `term` along with its inferred type -/ partial def infer (term : IR.Expr) : TypecheckM (TypedExpr × SusValue) := do @@ -136,16 +157,7 @@ mutual let term := ⟨← infoFromType typ, .app fnc arg⟩ pure (term, typ) | val => throw s!"Expected a pi type, found {← ppValue val}" - | .lam dom bod => do - let (dom, _) ← isSort dom - let ctx ← read - let domVal := suspend dom ctx (← get) - let var := mkSusVar (← infoFromType domVal) ctx.lvl - let (bod, imgVal) ← withExtendedCtx var domVal $ infer bod - let term := ⟨lamInfo bod.info, .lam dom bod⟩ - let typ := .mk (← piInfo domVal.info imgVal.info) $ - Value.pi domVal (← quoteTyped (ctx.lvl+1) ctx.env imgVal.getTyped) ctx.env - pure (term, typ) + | .lam .. => throw "Cannot infer lambda" | .pi dom img => let (dom, domLvl) ← isSort dom let ctx ← read diff --git a/Yatima/Typechecker/Printing.lean b/Yatima/Typechecker/Printing.lean index 914e87fd..eb7efdbb 100644 --- a/Yatima/Typechecker/Printing.lean +++ b/Yatima/Typechecker/Printing.lean @@ -100,8 +100,8 @@ mutual | .app func body => match func with | .app .. => return f!"{← ppExpr func} {← paren body}" | _ => return f!"{← paren func} {← paren body}" - | .lam type body => - return f!"fun (_ : {← ppExpr type}) =>{indentD (← ppExpr body)}" + | .lam body => + return f!"fun _ =>{indentD (← ppExpr body)}" | .pi dom img => return f!"(_ : {← ppExpr dom}) → {← ppExpr img}" | .letE type value body => From 30c59334070e21d9affa433bcdb05bd92cbb4298 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Wed, 29 Mar 2023 14:23:53 -0300 Subject: [PATCH 2/5] Added a `type` field to recursor rule --- Yatima/Common/LightData.lean | 4 ++-- Yatima/Common/ToLDON.lean | 2 +- Yatima/ContAddr/ContAddr.lean | 8 ++++++-- Yatima/Datatypes/Const.lean | 1 + Yatima/Typechecker/Infer.lean | 6 ++++-- 5 files changed, 14 insertions(+), 7 deletions(-) diff --git a/Yatima/Common/LightData.lean b/Yatima/Common/LightData.lean index 6e34e9c7..4e78ee8b 100644 --- a/Yatima/Common/LightData.lean +++ b/Yatima/Common/LightData.lean @@ -108,9 +108,9 @@ instance : Encodable Constructor LightData where | x => throw s!"Invalid encoding for IR.Constructor: {x}" instance : Encodable RecursorRule LightData where - encode | ⟨a, b⟩ => .cell #[a, b] + encode | ⟨a, b, c⟩ => .cell #[a, b, c] decode - | .cell #[a, b] => return ⟨← dec a, ← dec b⟩ + | .cell #[a, b, c] => return ⟨← dec a, ← dec b, ← dec c⟩ | x => throw s!"Invalid encoding for IR.RecursorRule: {x}" instance : Encodable Definition LightData where diff --git a/Yatima/Common/ToLDON.lean b/Yatima/Common/ToLDON.lean index d7fd6533..342a18c5 100644 --- a/Yatima/Common/ToLDON.lean +++ b/Yatima/Common/ToLDON.lean @@ -101,7 +101,7 @@ instance : Coe Constructor LDON where coe := Constructor.toLDON def RecursorRule.toLDON : RecursorRule → LDON - | ⟨fields, rhs⟩ => ([0, fields, rhs] : List LDON) + | ⟨fields, rhs, type⟩ => ([0, fields, rhs, type] : List LDON) instance : Coe RecursorRule LDON where coe := RecursorRule.toLDON diff --git a/Yatima/ContAddr/ContAddr.lean b/Yatima/ContAddr/ContAddr.lean index c0981aa0..ecd54346 100644 --- a/Yatima/ContAddr/ContAddr.lean +++ b/Yatima/ContAddr/ContAddr.lean @@ -261,12 +261,14 @@ partial def internalRecToIR (ctors : List Lean.Name) : | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName partial def recRuleToIR (rule : Lean.RecursorRule) : ContAddrM $ Constructor × RecursorRule := do + -- TODO somehow infer the type of `rule.rhs` in the Lean side + let rhsType := sorry let rhs ← contAddrExpr rule.rhs match ← getLeanConstant rule.ctor with | .ctorInfo ctor => withLevels ctor.levelParams do let typ ← contAddrExpr ctor.type let ctor := ⟨ctor.levelParams.length, typ, ctor.cidx, ctor.numParams, ctor.numFields⟩ - pure (ctor, ⟨rule.nfields, rhs⟩) + pure (ctor, ⟨rule.nfields, rhs, rhsType⟩) | const => throw $ .invalidConstantKind const.name "constructor" const.ctorName partial def externalRecToIR : Lean.ConstantInfo → ContAddrM Recursor @@ -278,7 +280,9 @@ partial def externalRecToIR : Lean.ConstantInfo → ContAddrM Recursor | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName partial def externalRecRuleToIR (rule : Lean.RecursorRule) : ContAddrM RecursorRule := - return ⟨rule.nfields, ← contAddrExpr rule.rhs⟩ + -- TODO somehow infer the type of `rule.rhs` in the Lean side + let rhsType := sorry + return ⟨rule.nfields, ← contAddrExpr rule.rhs, rhsType⟩ /-- Content-addresses a Lean expression and adds it to the store. diff --git a/Yatima/Datatypes/Const.lean b/Yatima/Datatypes/Const.lean index f9f12299..90c689de 100644 --- a/Yatima/Datatypes/Const.lean +++ b/Yatima/Datatypes/Const.lean @@ -45,6 +45,7 @@ structure Constructor where structure RecursorRule where fields : Nat rhs : Expr + type : Expr deriving Ord, BEq, Hashable, Repr structure Recursor where diff --git a/Yatima/Typechecker/Infer.lean b/Yatima/Typechecker/Infer.lean index 4b51ae58..ec806df8 100644 --- a/Yatima/Typechecker/Infer.lean +++ b/Yatima/Typechecker/Infer.lean @@ -281,8 +281,10 @@ mutual let univs := List.range recr.lvls |>.map .var let (type, _) ← withEnv ⟨ [], univs ⟩ $ withMutTypes mutTypes $ isSort recr.type let indProj := ⟨indBlockF, indIdx⟩ - let rules ← recr.rules.mapM fun rule => do - let (rhs, _) ← withEnv ⟨ [], univs ⟩ $ withMutTypes mutTypes $ infer rule.rhs + let rules ← recr.rules.mapM fun rule => withEnv ⟨ [], univs ⟩ $ withMutTypes mutTypes $ do + let (type, _) ← isSort rule.type + let typeVal := suspend type (← read) (← get) + let rhs ← check rule.rhs typeVal pure (rule.fields, rhs) let recrConst := .recursor type recr.params recr.motives recr.minors recr.indices recr.isK indProj ⟨rules⟩ modify fun stt => { stt with typedConsts := stt.typedConsts.insert f recrConst } From fa7b583f01f0518024e5c0912453f9d86e15b5a3 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 31 Mar 2023 00:08:50 -0300 Subject: [PATCH 3/5] `ContAddr` now annotates all valid lambdas that could be reached by a call to `infer` --- Yatima/ContAddr/ContAddr.lean | 67 ++++++++++++++++++++++++----------- 1 file changed, 46 insertions(+), 21 deletions(-) diff --git a/Yatima/ContAddr/ContAddr.lean b/Yatima/ContAddr/ContAddr.lean index ecd54346..c1243c55 100644 --- a/Yatima/ContAddr/ContAddr.lean +++ b/Yatima/ContAddr/ContAddr.lean @@ -205,7 +205,7 @@ partial def contAddrInductive (initInd : Lean.InductiveVal) : ContAddrM Lurk.F : addConstToEnv name hash if name == initInd.name then ret? := some hash - let some (ctors, recrs) := nameData.find? indName + let some (ctors, recrs) := nameData.find? indName | throw $ .cantFindMutDefIndex indName for (ctorIdx, ctorName) in ctors.enum do @@ -292,35 +292,60 @@ Constants are the tricky case, for which there are two possibilities: encoded as variables with indexes that go beyond the bind indexes * The constant doesn't belong to `recrCtx`, meaning that it's not a recursion and thus we can contAddr the actual constant right away + +We also must be careful not to create a redex with lambda expressions. That's +because we do not want to reach a lambda from an `infer` call. Instead, every +`(fun x => b) a` will become `(let f : A := fun x => b; f) b`, so that the lambda +is reached by a `check` call, and `infer` will be called on the variable `f`. -/ -partial def contAddrExpr : Lean.Expr → ContAddrM Expr - | .mdata _ e => contAddrExpr e - | expr => match expr with +partial def contAddrExpr (e : Lean.Expr) : ContAddrM Expr := + -- This auxiliary function will return a boolean which indicates whether the expression + -- is a lambda (with a possible let chain surrounding it) + let rec go (e : Lean.Expr) : ContAddrM (Expr × Bool) := match e with + | .mdata _ e => go e | .bvar idx => do match (← read).bindCtx.get? idx with -- Bound variables must be in the bind context - | some _ => return .var idx [] + | some _ => return (.var idx [], false) | none => throw $ .invalidBVarIndex idx - | .sort lvl => return .sort $ ← contAddrUniv lvl + | .sort lvl => return (.sort $ ← contAddrUniv lvl, false) | .const name lvls => do let univs ← lvls.mapM contAddrUniv match (← read).recrCtx.find? name with | some i => -- recursing! let idx := (← read).bindCtx.length + i - return .var idx univs - | none => return .const (← contAddrConst $ ← getLeanConstant name) univs - | .app fnc arg => return .app (← contAddrExpr fnc) (← contAddrExpr arg) - | .lam name _ bod _ => - return .lam (← withBinder name $ contAddrExpr bod) - | .forallE name dom img _ => - return .pi (← contAddrExpr dom) (← withBinder name $ contAddrExpr img) - | .letE name typ exp bod _ => - return .letE (← contAddrExpr typ) (← contAddrExpr exp) - (← withBinder name $ contAddrExpr bod) - | .lit lit => return .lit lit - | .proj _ idx exp => return .proj idx (← contAddrExpr exp) - | .fvar .. => throw $ .freeVariableExpr expr - | .mvar .. => throw $ .metaVariableExpr expr - | .mdata .. => throw $ .metaDataExpr expr + return (.var idx univs, false) + | none => return (.const (← contAddrConst $ ← getLeanConstant name) univs, false) + | .app fnc arg => do + let (fnc', lam?) ← go fnc + let head := if lam? + then + -- TODO somehow infer the type of `fnc` in the Lean side + let fncType := sorry + .letE fncType fnc' (.var 0 []) + else fnc' + let arg := (← go arg).fst + return (.app head arg, false) + | .lam name _ bod _ => do + let bod := (← withBinder name $ go bod).fst + return (.lam bod, true) + | .forallE name dom img _ => do + -- neither `dom` nor `img` can be lambdas + let dom := (← go dom).fst + let img := (← withBinder name $ go img).fst + return (.pi dom img, false) + | .letE name typ exp bod _ => do + let typ := (← go typ).fst + let exp := (← go exp).fst + let (bod, lam?) ← withBinder name $ go bod + return (.letE typ exp bod, lam?) + | .lit lit => return (.lit lit, false) + | .proj _ idx exp => do + -- `exp` cannot be a lambda + let exp := (← go exp).fst + return (.proj idx exp, false) + | expr@(.fvar ..) => throw $ .freeVariableExpr expr + | expr@(.mvar ..) => throw $ .metaVariableExpr expr + return (← go e).fst /-- A name-irrelevant ordering of Lean expressions. From bad7b6dcc3716fa0f3b9ba4f7c09410468cf1aa1 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 31 Mar 2023 18:17:40 -0300 Subject: [PATCH 4/5] `ContAddrM` now extends `MetaM` --- Yatima/ContAddr/ContAddr.lean | 100 +++++++++++++++++---------------- Yatima/ContAddr/ContAddrM.lean | 8 ++- 2 files changed, 56 insertions(+), 52 deletions(-) diff --git a/Yatima/ContAddr/ContAddr.lean b/Yatima/ContAddr/ContAddr.lean index c1243c55..7314f20f 100644 --- a/Yatima/ContAddr/ContAddr.lean +++ b/Yatima/ContAddr/ContAddr.lean @@ -19,8 +19,8 @@ open Std (RBMap) /-- Defines an ordering for Lean universes -/ def cmpLevel (x : Lean.Level) (y : Lean.Level) : ContAddrM Ordering := match x, y with - | .mvar .., _ => throw $ .unfilledLevelMetavariable x - | _, .mvar .. => throw $ .unfilledLevelMetavariable y + | .mvar .., _ => ContAddrExcept.throw $ .unfilledLevelMetavariable x + | _, .mvar .. => ContAddrExcept.throw $ .unfilledLevelMetavariable y | .zero, .zero => return .eq | .zero, _ => return .lt | _, .zero => return .gt @@ -37,8 +37,8 @@ def cmpLevel (x : Lean.Level) (y : Lean.Level) : ContAddrM Ordering := let lvls := (← read).univCtx match (lvls.indexOf? x), (lvls.indexOf? y) with | some xi, some yi => return (compare xi yi) - | none, _ => throw $ .levelNotFound x lvls - | _, none => throw $ .levelNotFound y lvls + | none, _ => ContAddrExcept.throw $ .levelNotFound x lvls + | _, none => ContAddrExcept.throw $ .levelNotFound y lvls /-- Content-addresses a Lean universe level and adds it to the store -/ def contAddrUniv : Lean.Level → ContAddrM Univ @@ -50,14 +50,14 @@ def contAddrUniv : Lean.Level → ContAddrM Univ let lvls := (← read).univCtx match lvls.indexOf? name with | some n => pure $ .var n - | none => throw $ .levelNotFound name lvls - | l@(.mvar ..) => throw $ .unfilledLevelMetavariable l + | none => ContAddrExcept.throw $ .levelNotFound name lvls + | l@(.mvar ..) => ContAddrExcept.throw $ .unfilledLevelMetavariable l /-- Retrieves a Lean constant from the environment by its name -/ def getLeanConstant (name : Lean.Name) : ContAddrM Lean.ConstantInfo := do match (← read).constMap.find? name with | some const => pure const - | none => throw $ .unknownConstant name + | none => ContAddrExcept.throw $ .unknownConstant name def isInternalRec (expr : Lean.Expr) (name : Lean.Name) : Bool := match expr with @@ -79,12 +79,12 @@ partial def contAddrConst (const : Lean.ConstantInfo) : ContAddrM Lurk.F := do | .ctorInfo val => do match ← getLeanConstant val.induct with | .inductInfo ind => discard $ contAddrConst (.inductInfo ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "inductive" const.ctorName contAddrConst const | .recInfo val => do match ← getLeanConstant val.getInduct with | .inductInfo ind => discard $ contAddrConst (.inductInfo ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "inductive" const.ctorName contAddrConst const -- The rest adds the constants to the cache one by one | const => withLevelsAndReset const.levelParams do @@ -118,7 +118,7 @@ partial def contAddrDefinition (struct : Lean.DefinitionVal) : ContAddrM Lurk.F let mutualDefs ← struct.all.mapM fun name => do match ← getLeanConstant name with | .defnInfo defn => pure defn - | const => throw $ .invalidConstantKind const.name "definition" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "definition" const.ctorName let mutualDefs ← sortDefs [mutualDefs] -- Building the `recrCtx` @@ -142,14 +142,14 @@ partial def contAddrDefinition (struct : Lean.DefinitionVal) : ContAddrM Lurk.F for name in struct.all do -- Storing and caching the definition projection -- Also adds the constant to the array of constants - let some idx := recrCtx.find? name | throw $ .cantFindMutDefIndex name + let some idx := recrCtx.find? name | ContAddrExcept.throw $ .cantFindMutDefIndex name let hash ← commit $ .definitionProj ⟨blockHash, idx⟩ addConstToEnv name hash if struct.name == name then ret? := some hash match ret? with | some ret => return ret - | none => throw $ .constantNotContentAddressed struct.name + | none => ContAddrExcept.throw $ .constantNotContentAddressed struct.name partial def definitionToIR (defn : Lean.DefinitionVal) : ContAddrM Definition := return ⟨defn.levelParams.length, ← contAddrExpr defn.type, @@ -178,7 +178,7 @@ partial def contAddrInductive (initInd : Lean.InductiveVal) : ContAddrM Lurk.F : indCtors := indCtors ++ ind.ctors indRecs := indRecs ++ indRecrs nameData := nameData.insert indName (ind.ctors, indRecrs) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "inductive" const.ctorName -- `mutualConsts` is the list of the names of all constants associated with an -- inductive block: the inductives themselves, the constructors and the recursors @@ -191,7 +191,7 @@ partial def contAddrInductive (initInd : Lean.InductiveVal) : ContAddrM Lurk.F : -- constructors and recursors to `consts` let irInds ← initInd.all.mapM fun name => do match ← getLeanConstant name with | .inductInfo ind => withRecrs recrCtx do pure $ (← inductiveToIR ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "inductive" const.ctorName let blockHash ← commit $ .mutIndBlock irInds addBlockToEnv blockHash @@ -206,7 +206,7 @@ partial def contAddrInductive (initInd : Lean.InductiveVal) : ContAddrM Lurk.F : if name == initInd.name then ret? := some hash let some (ctors, recrs) := nameData.find? indName - | throw $ .cantFindMutDefIndex indName + | ContAddrExcept.throw $ .cantFindMutDefIndex indName for (ctorIdx, ctorName) in ctors.enum do -- Store and cache constructor projections @@ -220,7 +220,7 @@ partial def contAddrInductive (initInd : Lean.InductiveVal) : ContAddrM Lurk.F : match ret? with | some ret => return ret - | none => throw $ .constantNotContentAddressed initInd.name + | none => ContAddrExcept.throw $ .constantNotContentAddressed initInd.name partial def inductiveToIR (ind : Lean.InductiveVal) : ContAddrM Inductive := do let leanRecs := (← read).constMap.childrenOfWith ind.name @@ -234,7 +234,7 @@ partial def inductiveToIR (ind : Lean.InductiveVal) : ContAddrM Inductive := do else do let thisRec ← externalRecToIR r pure (thisRec :: recs, ctors) - | _ => throw $ .nonRecursorExtractedFromChildren r.name + | _ => ContAddrExcept.throw $ .nonRecursorExtractedFromChildren r.name let (struct, unit) ← if ind.isRec || ind.numIndices != 0 then pure (false, false) else match ctors with -- Structures can only have one constructor @@ -258,18 +258,17 @@ partial def internalRecToIR (ctors : List Lean.Name) : let recr := ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, rec.numMotives, rec.numMinors, retRules, rec.k, true⟩ return (recr, retCtors) - | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "recursor" const.ctorName partial def recRuleToIR (rule : Lean.RecursorRule) : ContAddrM $ Constructor × RecursorRule := do - -- TODO somehow infer the type of `rule.rhs` in the Lean side - let rhsType := sorry + let rhsType ← contAddrExpr (← Lean.Meta.inferType rule.rhs) let rhs ← contAddrExpr rule.rhs match ← getLeanConstant rule.ctor with | .ctorInfo ctor => withLevels ctor.levelParams do let typ ← contAddrExpr ctor.type let ctor := ⟨ctor.levelParams.length, typ, ctor.cidx, ctor.numParams, ctor.numFields⟩ pure (ctor, ⟨rule.nfields, rhs, rhsType⟩) - | const => throw $ .invalidConstantKind const.name "constructor" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "constructor" const.ctorName partial def externalRecToIR : Lean.ConstantInfo → ContAddrM Recursor | .recInfo rec => withLevels rec.levelParams do @@ -277,11 +276,10 @@ partial def externalRecToIR : Lean.ConstantInfo → ContAddrM Recursor let rules ← rec.rules.mapM externalRecRuleToIR return ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, rec.numMotives, rec.numMinors, rules, rec.k, false⟩ - | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName + | const => ContAddrExcept.throw $ .invalidConstantKind const.name "recursor" const.ctorName -partial def externalRecRuleToIR (rule : Lean.RecursorRule) : ContAddrM RecursorRule := - -- TODO somehow infer the type of `rule.rhs` in the Lean side - let rhsType := sorry +partial def externalRecRuleToIR (rule : Lean.RecursorRule) : ContAddrM RecursorRule := do + let rhsType ← contAddrExpr (← Lean.Meta.inferType rule.rhs) return ⟨rule.nfields, ← contAddrExpr rule.rhs, rhsType⟩ /-- @@ -306,7 +304,7 @@ partial def contAddrExpr (e : Lean.Expr) : ContAddrM Expr := | .bvar idx => do match (← read).bindCtx.get? idx with -- Bound variables must be in the bind context | some _ => return (.var idx [], false) - | none => throw $ .invalidBVarIndex idx + | none => ContAddrExcept.throw $ .invalidBVarIndex idx | .sort lvl => return (.sort $ ← contAddrUniv lvl, false) | .const name lvls => do let univs ← lvls.mapM contAddrUniv @@ -317,12 +315,13 @@ partial def contAddrExpr (e : Lean.Expr) : ContAddrM Expr := | none => return (.const (← contAddrConst $ ← getLeanConstant name) univs, false) | .app fnc arg => do let (fnc', lam?) ← go fnc - let head := if lam? - then - -- TODO somehow infer the type of `fnc` in the Lean side - let fncType := sorry - .letE fncType fnc' (.var 0 []) - else fnc' + let head ← if lam? + then do + let fncType ← Lean.Meta.inferType fnc + -- `fncType` cannot be a lambda + let fncType' := (← go fncType).fst + pure $ .letE fncType' fnc' (.var 0 []) + else pure fnc' let arg := (← go arg).fst return (.app head arg, false) | .lam name _ bod _ => do @@ -334,6 +333,7 @@ partial def contAddrExpr (e : Lean.Expr) : ContAddrM Expr := let img := (← withBinder name $ go img).fst return (.pi dom img, false) | .letE name typ exp bod _ => do + -- `typ` cannot be a lambda let typ := (← go typ).fst let exp := (← go exp).fst let (bod, lam?) ← withBinder name $ go bod @@ -343,8 +343,8 @@ partial def contAddrExpr (e : Lean.Expr) : ContAddrM Expr := -- `exp` cannot be a lambda let exp := (← go exp).fst return (.proj idx exp, false) - | expr@(.fvar ..) => throw $ .freeVariableExpr expr - | expr@(.mvar ..) => throw $ .metaVariableExpr expr + | expr@(.fvar ..) => ContAddrExcept.throw $ .freeVariableExpr expr + | expr@(.mvar ..) => ContAddrExcept.throw $ .metaVariableExpr expr return (← go e).fst /-- @@ -353,10 +353,10 @@ A name-irrelevant ordering of Lean expressions. -/ partial def cmpExpr (weakOrd : Std.RBMap Name Nat compare) : Lean.Expr → Lean.Expr → ContAddrM Ordering - | e@(.mvar ..), _ => throw $ .unfilledExprMetavariable e - | _, e@(.mvar ..) => throw $ .unfilledExprMetavariable e - | e@(.fvar ..), _ => throw $ .freeVariableExpr e - | _, e@(.fvar ..) => throw $ .freeVariableExpr e + | e@(.mvar ..), _ => ContAddrExcept.throw $ .unfilledExprMetavariable e + | _, e@(.mvar ..) => ContAddrExcept.throw $ .unfilledExprMetavariable e + | e@(.fvar ..), _ => ContAddrExcept.throw $ .freeVariableExpr e + | _, e@(.fvar ..) => ContAddrExcept.throw $ .freeVariableExpr e | .mdata _ x, .mdata _ y => cmpExpr weakOrd x y | .mdata _ x, y => cmpExpr weakOrd x y | x, .mdata _ y => cmpExpr weakOrd x y @@ -476,8 +476,9 @@ end /-- Iterates over a list of `Lean.ConstantInfo`, triggering their content-addressing -/ def contAddrM (delta : List Lean.ConstantInfo) : ContAddrM Unit := do - delta.forM fun c => if !c.isUnsafe then discard $ contAddrConst c else pure () - if (← read).persist then dumpData (← get).ldonHashState LDONHASHCACHE + sorry + -- delta.forM fun c => if !c.isUnsafe then discard $ contAddrConst c else pure () + -- if (← read).persist then dumpData (← get).ldonHashState LDONHASHCACHE /-- Content-addresses the "delta" of an environment, that is, the content that is @@ -489,14 +490,15 @@ Open references are variables that point to names which aren't present in the -/ def contAddr (constMap : Lean.ConstMap) (delta : List Lean.ConstantInfo) (quick persist : Bool) : IO $ Except ContAddrError ContAddrState := do - let persist := if quick then false else persist - let ldonHashState ← - if quick then pure default - else pure $ (← loadData LDONHASHCACHE).getD default - if persist then IO.FS.createDirAll STOREDIR - match ← StateT.run (ReaderT.run (contAddrM delta) - (.init constMap quick persist)) (.init ldonHashState) with - | (.ok _, stt) => return .ok stt - | (.error e, _) => return .error e + sorry + -- let persist := if quick then false else persist + -- let ldonHashState ← + -- if quick then pure default + -- else pure $ (← loadData LDONHASHCACHE).getD default + -- if persist then IO.FS.createDirAll STOREDIR + -- match ← StateT.run (ReaderT.run (contAddrM delta) + -- (.init constMap quick persist)) (.init ldonHashState) with + -- | (.ok _, stt) => return .ok stt + -- | (.error e, _) => return .error e end Yatima.ContAddr diff --git a/Yatima/ContAddr/ContAddrM.lean b/Yatima/ContAddr/ContAddrM.lean index 39f1b6a1..17ee39b1 100644 --- a/Yatima/ContAddr/ContAddrM.lean +++ b/Yatima/ContAddr/ContAddrM.lean @@ -1,7 +1,6 @@ import Yatima.ContAddr.ContAddrError import Yatima.Common.ToLDON import Yatima.Common.LightData -import Yatima.Common.IO import Lurk.Scalar namespace Yatima.ContAddr @@ -35,8 +34,11 @@ structure ContAddrCtx where def ContAddrCtx.init (map : Lean.ConstMap) (quick persist : Bool) : ContAddrCtx := ⟨map, [], [], .empty, quick, persist⟩ -abbrev ContAddrM := ReaderT ContAddrCtx $ ExceptT ContAddrError $ - StateT ContAddrState IO +abbrev ContAddrM := ExceptT ContAddrError $ ReaderT ContAddrCtx $ StateT ContAddrState $ Lean.MetaM + +instance ContAddrExcept : MonadExceptOf ContAddrError ContAddrM where + throw e := ExceptT.mk <| pure (Except.error e) + tryCatch := ExceptT.tryCatch def withBinder (name : Name) : ContAddrM α → ContAddrM α := withReader $ fun c => { c with bindCtx := name :: c.bindCtx } From e07c94c4700428c72ae74457f7034d81f05fdaac Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 31 Mar 2023 18:40:29 -0300 Subject: [PATCH 5/5] `ContAddr` done Still need to fix `Cli` --- Yatima/ContAddr/ContAddr.lean | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/Yatima/ContAddr/ContAddr.lean b/Yatima/ContAddr/ContAddr.lean index 7314f20f..1c9ba460 100644 --- a/Yatima/ContAddr/ContAddr.lean +++ b/Yatima/ContAddr/ContAddr.lean @@ -1,4 +1,5 @@ import Yatima.Lean.Utils +import Yatima.Common.IO import Yatima.ContAddr.ContAddrM import YatimaStdLib.RBMap import Lurk.LightData @@ -476,9 +477,8 @@ end /-- Iterates over a list of `Lean.ConstantInfo`, triggering their content-addressing -/ def contAddrM (delta : List Lean.ConstantInfo) : ContAddrM Unit := do - sorry - -- delta.forM fun c => if !c.isUnsafe then discard $ contAddrConst c else pure () - -- if (← read).persist then dumpData (← get).ldonHashState LDONHASHCACHE + delta.forM fun c => if !c.isUnsafe then discard $ contAddrConst c else pure () + if (← read).persist then dumpData (← get).ldonHashState LDONHASHCACHE /-- Content-addresses the "delta" of an environment, that is, the content that is @@ -489,16 +489,16 @@ Open references are variables that point to names which aren't present in the `Lean.ConstMap`. -/ def contAddr (constMap : Lean.ConstMap) (delta : List Lean.ConstantInfo) - (quick persist : Bool) : IO $ Except ContAddrError ContAddrState := do - sorry - -- let persist := if quick then false else persist - -- let ldonHashState ← - -- if quick then pure default - -- else pure $ (← loadData LDONHASHCACHE).getD default - -- if persist then IO.FS.createDirAll STOREDIR - -- match ← StateT.run (ReaderT.run (contAddrM delta) - -- (.init constMap quick persist)) (.init ldonHashState) with - -- | (.ok _, stt) => return .ok stt - -- | (.error e, _) => return .error e + (quick persist : Bool) : Lean.MetaM $ Except ContAddrError ContAddrState := do + let persist := if quick then false else persist + let ldonHashState ← + if quick then pure default + else pure $ (← loadData LDONHASHCACHE).getD default + if persist then IO.FS.createDirAll STOREDIR + let runReader := ReaderT.run (contAddrM delta) (.init constMap quick persist) + let runState := StateT.run runReader (.init ldonHashState) + match ← runState with + | (.ok _, stt) => return .ok stt + | (.error e, _) => return .error e end Yatima.ContAddr