diff --git a/Apps/ZKVoting/Prover.lean b/Apps/ZKVoting/Prover.lean index c09760dc..8a8e3ecf 100644 --- a/Apps/ZKVoting/Prover.lean +++ b/Apps/ZKVoting/Prover.lean @@ -29,35 +29,33 @@ def runElection (votes: List Candidate) : Result := open Ix.Compile def main : IO UInt32 := do - let mut stt : CompileState := .init (<- get_env!) + let mut env : Lean.Environment := <- get_env! -- simulate getting the votes from somewhere let votes : List Candidate <- pure privateVotes let mut as : List Lean.Name := [] - -- default maxHeartBeats - let ticks : USize := 200000 -- the type of each vote to commit let voteType := Lean.toTypeExpr Candidate -- loop over the votes for v in votes do -- add each vote to our environment as a commitment - let (lvls, typ, val) <- runMeta (metaMakeDef v) stt.env - let ((addr, _), stt') <- (commitDef lvls typ val).runIO' ticks stt - stt := stt' + let (lvls, typ, val) <- runMeta (metaMakeDef v) env + let ((addr, _), stt) <- (commitDef lvls typ val).runIO env + env := stt.env as := (Address.toUniqueName addr)::as IO.println s!"vote: {repr v}, commitment: {addr}" -- build a Lean list of our commitments as the argument to runElection - let arg : Lean.Expr <- runMeta (metaMakeList voteType as) stt.env + let arg : Lean.Expr <- runMeta (metaMakeList voteType as) env let (lvls, input, output, type, sort) <- - runMeta (metaMakeEvalClaim ``runElection [arg]) stt.env - let inputPretty <- runMeta (Lean.Meta.ppExpr input) stt.env - let outputPretty <- runMeta (Lean.Meta.ppExpr output) stt.env - let typePretty <- runMeta (Lean.Meta.ppExpr type) stt.env + runMeta (metaMakeEvalClaim ``runElection [arg]) env + let inputPretty <- runMeta (Lean.Meta.ppExpr input) env + let outputPretty <- runMeta (Lean.Meta.ppExpr output) env + let typePretty <- runMeta (Lean.Meta.ppExpr type) env IO.println s!"claim: {inputPretty}" IO.println s!" ~> {outputPretty}" IO.println s!" : {typePretty}" IO.println s!" @ {repr lvls}" - let ((claim,_,_,_), _stt') <- - (evalClaim lvls input output type sort true).runIO' ticks stt + let ((claim,_,_,_), _stt') <- + (evalClaim lvls input output type sort true).runIO env IO.println s!"{claim}" -- Ix.prove claim stt return 0 diff --git a/Ix.lean b/Ix.lean index 3da4f8da..e2d4bc7e 100644 --- a/Ix.lean +++ b/Ix.lean @@ -5,5 +5,6 @@ import Ix.TransportM import Ix.IR import Ix.Meta import Ix.CompileM +import Ix.DecompileM import Ix.Claim import Ix.Prove diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index 20a9e7c4..0e2a6052 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -7,6 +7,8 @@ import Ix.Address import Ix.Meta import Lean +open Ix.Compile + --❯ ix prove IxTest.lean "id'" --typechecking: --id' (A : Type) (x : A) : A @@ -22,8 +24,7 @@ def runProveCheck IO.println "typechecking:" IO.println signature.fmt.pretty let ((claim, _, _), _stt) <- - (Ix.Compile.checkClaim constInfo.name constInfo.type constSort - constInfo.levelParams commit).runIO' 200000 (.init env) + (checkClaim constInfo.name constInfo.type constSort constInfo.levelParams commit).runIO env IO.println $ s!"claim: {claim}" -- TODO: prove return 0 @@ -62,8 +63,7 @@ def runProveEval IO.println s!" ~> {outputPretty}" IO.println s!" : {typePretty}" IO.println s!" @ {repr lvls}" - let ((claim, _, _), _stt) <- - (Ix.Compile.evalClaim lvls input output type sort commit).runIO' 200000 (.init env) + let ((claim, _, _), _stt) <- (evalClaim lvls input output type sort commit).runIO env IO.println $ s!"claim: {claim}" -- TODO: prove return 0 diff --git a/Ix/Cli/StoreCmd.lean b/Ix/Cli/StoreCmd.lean index 40ef5196..797d8514 100644 --- a/Ix/Cli/StoreCmd.lean +++ b/Ix/Cli/StoreCmd.lean @@ -2,12 +2,14 @@ import Cli import Ix.Cronos import Ix.Common import Ix.CompileM +import Ix.TransportM import Ix.Store import Ix.Address import Lean -- ix store -- ix store get
+-- ix store remat
def runStore (p : Cli.Parsed) : IO UInt32 := do let source : String := p.positionalArg! "source" |>.as! String let mut cronos ← Cronos.new.clock "Lean-frontend" @@ -15,11 +17,10 @@ def runStore (p : Cli.Parsed) : IO UInt32 := do --StoreIO.toIO ensureStoreDir let path := ⟨source⟩ let leanEnv ← Lean.runFrontend (← IO.FS.readFile path) path - let delta := leanEnv.getDelta cronos ← cronos.clock "Lean-frontend" -- Start content-addressing cronos ← cronos.clock "content-address" - let stt ← Ix.Compile.compileDeltaIO leanEnv delta + let stt ← Ix.Compile.compileEnvIO leanEnv stt.names.forM fun name (const, meta) => do IO.println <| s!"{name}:" IO.println <| s!" #{const}" @@ -49,6 +50,20 @@ def runGet (p : Cli.Parsed) : IO UInt32 := do IO.println <| s!"{repr const}" return 0 +def runRemat (p : Cli.Parsed) : IO UInt32 := do + let cont : String := p.positionalArg! "constantAddress" |>.as! String + let meta : String := p.positionalArg! "metadataAddress" |>.as! String + let (c, m) <- IO.ofExcept $ + match Address.fromString cont, Address.fromString meta with + | .some c, .some m => .ok (c, m) + | .none, _ => .error "bad address {cont}" + | _, .none => .error "bad address {meta}" + let cont <- StoreIO.toIO (Store.readConst c) + let meta <- StoreIO.toIO (Store.readConst m) + let ix := Ix.TransportM.rematerialize cont meta + IO.println <| s!"{repr ix}" + return 0 + def storeGetCmd : Cli.Cmd := `[Cli| get VIA runGet; "print a store entry" @@ -56,6 +71,14 @@ def storeGetCmd : Cli.Cmd := `[Cli| address : String; "Ix address" ] +def storeRematCmd : Cli.Cmd := `[Cli| + remat VIA runRemat; + "print a store entry" + ARGS: + constantAddress : String; "Ix constant address" + metadataAddress : String; "Ix metadata address" +] + def storeCmd : Cli.Cmd := `[Cli| store VIA runStore; "Interact with the Ix store" @@ -67,6 +90,7 @@ def storeCmd : Cli.Cmd := `[Cli| source : String; "Source file input" SUBCOMMANDS: - storeGetCmd + storeGetCmd; + storeRematCmd ] diff --git a/Ix/Common.lean b/Ix/Common.lean index 266fe2f7..5b741e50 100644 --- a/Ix/Common.lean +++ b/Ix/Common.lean @@ -10,6 +10,16 @@ def compareList [Ord α] : List α -> List α -> Ordering | [], _::_ => .lt | [], [] => .eq +def compareListM + [Monad μ] (cmp: α -> α -> μ Ordering) : List α -> List α -> μ Ordering +| a::as, b::bs => do + match (<- cmp a b) with + | .eq => compareListM cmp as bs + | x => pure x +| _::_, [] => pure .gt +| [], _::_ => pure .lt +| [], [] => pure .eq + instance [Ord α] : Ord (List α) where compare := compareList @@ -22,14 +32,36 @@ instance : Ord Lean.Name where compare := Lean.Name.quickCmp deriving instance Ord for Lean.Literal +--deriving instance Ord for Lean.Expr deriving instance Ord for Lean.BinderInfo -deriving instance Ord for Lean.QuotKind +deriving instance BEq, Repr, Hashable, Ord for Lean.QuotKind +deriving instance Hashable, Repr for Lean.ReducibilityHints +deriving instance BEq, Ord, Hashable, Repr for Lean.DefinitionSafety +deriving instance BEq, Repr for Lean.ConstantVal +deriving instance BEq, Repr for Lean.QuotVal +deriving instance BEq, Repr for Lean.AxiomVal +deriving instance BEq, Repr for Lean.TheoremVal +deriving instance BEq, Repr for Lean.DefinitionVal +deriving instance BEq, Repr for Lean.OpaqueVal +deriving instance BEq, Repr for Lean.RecursorRule +deriving instance BEq, Repr for Lean.RecursorVal +deriving instance BEq, Repr for Lean.ConstructorVal +deriving instance BEq, Repr for Lean.InductiveVal +deriving instance BEq, Repr for Lean.ConstantInfo +deriving instance BEq, Repr for Ordering def UInt8.MAX : UInt64 := 0xFF def UInt16.MAX : UInt64 := 0xFFFF def UInt32.MAX : UInt64 := 0xFFFFFFFF def UInt64.MAX : UInt64 := 0xFFFFFFFFFFFFFFFF +/-- Distinguish different kinds of Ix definitions --/ +inductive Ix.DefMode where +| «definition» +| «opaque» +| «theorem» +deriving BEq, Ord, Hashable, Repr, Nonempty, Inhabited + namespace List partial def mergeM [Monad μ] (cmp : α → α → μ Ordering) : List α → List α → μ (List α) @@ -72,26 +104,16 @@ mutual end -def sortByM [Monad μ] (xs: List α) (cmp: α -> α -> μ Ordering) (rev := false) : - μ (List α) := do - if rev then - let revCmp : _ → _ → μ Ordering := fun x y => do - match (← cmp x y) with - | .gt => return Ordering.lt - | .eq => return Ordering.eq - | .lt => return Ordering.gt - sequencesM revCmp xs >>= mergeAllM revCmp - else - sequencesM cmp xs >>= mergeAllM cmp +def sortByM [Monad μ] (xs: List α) (cmp: α -> α -> μ Ordering) : μ (List α) := + sequencesM cmp xs >>= mergeAllM cmp /-- -Mergesort from least to greatest. To sort from greatest to +Mergesort from least to greatest. To sort from greatest to least set `rev` -/ -def sortBy (cmp : α -> α -> Ordering) (xs: List α) (rev := false) : List α := - Id.run do xs.sortByM (cmp <$> · <*> ·) rev +def sortBy (cmp : α -> α -> Ordering) (xs: List α) : List α := + Id.run <| xs.sortByM (fun x y => pure <| cmp x y) -def sort [Ord α] (xs: List α) (rev := false) : List α := - sortBy compare xs rev +def sort [Ord α] (xs: List α) : List α := sortBy compare xs def groupByMAux [Monad μ] (eq : α → α → μ Bool) : List α → List (List α) → μ (List (List α)) | a::as, (ag::g)::gs => do match (← eq a ag) with @@ -216,4 +238,26 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do (← msgs.toList.mapM (·.toString)).map String.trim else return s.commandState.env +def Expr.stripMData : Expr -> Expr +| .mdata _ x => x.stripMData +| .app f a => .app f.stripMData a.stripMData +| .lam bn bt b bi => .lam bn bt.stripMData b.stripMData bi +| .forallE bn bt b bi => .forallE bn bt.stripMData b.stripMData bi +| .letE ln t v b nd => .letE ln t.stripMData v.stripMData b.stripMData nd +| .proj tn i s => .proj tn i s.stripMData +| x => x + +def RecursorRule.stripMData : RecursorRule -> RecursorRule +| ⟨c, nf, rhs⟩ => ⟨c, nf, rhs.stripMData⟩ + +def ConstantInfo.stripMData : Lean.ConstantInfo -> Lean.ConstantInfo +| .axiomInfo x => .axiomInfo { x with type := x.type.stripMData } +| .defnInfo x => .defnInfo { x with type := x.type.stripMData, value := x.value.stripMData } +| .thmInfo x => .thmInfo { x with type := x.type.stripMData, value := x.value.stripMData } +| .quotInfo x => .quotInfo { x with type := x.type.stripMData } +| .opaqueInfo x => .opaqueInfo { x with type := x.type.stripMData, value := x.value.stripMData } +| .inductInfo x => .inductInfo { x with type := x.type.stripMData } +| .ctorInfo x => .ctorInfo { x with type := x.type.stripMData } +| .recInfo x => .recInfo { x with type := x.type.stripMData, rules := x.rules.map (·.stripMData) } end Lean + diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean index 761a3a18..8f0d8f17 100644 --- a/Ix/CompileM.lean +++ b/Ix/CompileM.lean @@ -20,47 +20,57 @@ inductive CompileError | freeVariableExpr : Lean.Expr → CompileError | metaVariableExpr : Lean.Expr → CompileError | metaDataExpr : Lean.Expr → CompileError -| levelNotFound : Lean.Name → List Lean.Name → CompileError +| levelNotFound : Lean.Name → List Lean.Name -> String → CompileError | invalidConstantKind : Lean.Name → String → String → CompileError | constantNotContentAddressed : Lean.Name → CompileError | nonRecursorExtractedFromChildren : Lean.Name → CompileError | cantFindMutDefIndex : Lean.Name → CompileError | transportError : TransportError → CompileError -| kernelException : String → CompileError -| storeError : StoreError → CompileError -| todo - -instance : ToString CompileError where toString -| .unknownConstant n => s!"Unknown constant '{n}'" -| .unfilledLevelMetavariable l => s!"Unfilled level metavariable on universe '{l}'" -| .unfilledExprMetavariable e => s!"Unfilled level metavariable on expression '{e}'" -| .invalidBVarIndex idx => s!"Invalid index {idx} for bound variable context" -| .freeVariableExpr e => s!"Free variable in expression '{e}'" -| .metaVariableExpr e => s!"Metavariable in expression '{e}'" -| .metaDataExpr e => s!"Meta data in expression '{e}'" -| .levelNotFound n ns => s!"'Level {n}' not found in '{ns}'" -| .invalidConstantKind n ex gt => - s!"Invalid constant kind for '{n}'. Expected '{ex}' but got '{gt}'" -| .constantNotContentAddressed n => s!"Constant '{n}' wasn't content-addressed" -| .nonRecursorExtractedFromChildren n => +| kernelException : Lean.Kernel.Exception → CompileError +| cantPackLevel : Nat → CompileError +| nonCongruentInductives : PreInductive -> PreInductive -> CompileError +| alphaInvarianceFailure : Ix.Const -> Address -> Ix.Const -> Address -> CompileError +| emptyDefsEquivalenceClass: List (List PreDefinition) -> CompileError +| emptyIndsEquivalenceClass: List (List PreInductive) -> CompileError + +def CompileError.pretty : CompileError -> IO String +| .unknownConstant n => pure s!"Unknown constant '{n}'" +| .unfilledLevelMetavariable l => pure s!"Unfilled level metavariable on universe '{l}'" +| .unfilledExprMetavariable e => pure s!"Unfilled level metavariable on expression '{e}'" +| .invalidBVarIndex idx => pure s!"Invalid index {idx} for bound variable context" +| .freeVariableExpr e => pure s!"Free variable in expression '{e}'" +| .metaVariableExpr e => pure s!"Metavariable in expression '{e}'" +| .metaDataExpr e => pure s!"Meta data in expression '{e}'" +| .levelNotFound n ns msg => pure s!"'Level {n}' not found in '{ns}', {msg}" +| .invalidConstantKind n ex gt => pure s!"Invalid constant kind for '{n}'. Expected '{ex}' but got '{gt}'" +| .constantNotContentAddressed n => pure s!"Constant '{n}' wasn't content-addressed" +| .nonRecursorExtractedFromChildren n => pure s!"Non-recursor '{n}' extracted from children" -| .cantFindMutDefIndex n => s!"Can't find index for mutual definition '{n}'" -| .transportError n => s!"Transport error '{repr n}'" -| .kernelException e => e -| _ => s!"todo" +| .cantFindMutDefIndex n => pure s!"Can't find index for mutual definition '{n}'" +| .transportError n => pure s!"compiler transport error '{repr n}'" +| .kernelException e => (·.pretty 80) <$> (e.toMessageData .empty).format +| .cantPackLevel n => pure s!"Can't pack level {n} greater than 2^256'" +| .nonCongruentInductives a b => pure s!"noncongruent inductives {a.name} {b.name}'" +| .alphaInvarianceFailure x xa y ya => + pure s!"alpha invariance failure {repr x} hashes to {xa}, but {repr y} hashes to {ya}" +| .emptyDefsEquivalenceClass dss => + pure s!"empty equivalence class while sorting definitions {dss.map fun ds => ds.map (·.name)}" +| .emptyIndsEquivalenceClass dss => + pure s!"empty equivalence class while sorting inductives {dss.map fun ds => ds.map (·.name)}" structure CompileEnv where univCtx : List Lean.Name bindCtx : List Lean.Name mutCtx : RBMap Lean.Name Nat compare maxHeartBeats: USize - persist : Bool + current : Lean.Name def CompileEnv.init (maxHeartBeats: USize): CompileEnv := - ⟨default, default, default, maxHeartBeats, true⟩ + ⟨default, default, default, maxHeartBeats, default⟩ structure CompileState where env: Lean.Environment + prng: StdGen names: RBMap Lean.Name (Address × Address) compare store: RBMap Address Ixon.Const compare cache: RBMap Ix.Const (Address × Address) compare @@ -68,48 +78,36 @@ structure CompileState where axioms: RBMap Lean.Name (Address × Address) compare blocks: RBSet (Address × Address) compare -def CompileState.init (env: Lean.Environment): CompileState := - ⟨env, default, default, default, default, default, default⟩ +def CompileState.init (env: Lean.Environment) (seed: Nat): CompileState := + ⟨env, mkStdGen seed, default, default, default, default, default, default⟩ -abbrev CompileM := - ReaderT CompileEnv <| ExceptT CompileError <| StateT CompileState IO +abbrev CompileM := ReaderT CompileEnv <| EStateM CompileError CompileState -def CompileM.runIO (maxHeartBeats: USize) (stt: CompileState) (c : CompileM α) - : IO (Except CompileError α × CompileState) := do - StateT.run (ReaderT.run c (.init maxHeartBeats)) stt +def CompileM.run (env: CompileEnv) (stt: CompileState) (c : CompileM α) + : EStateM.Result CompileError CompileState α + := EStateM.run (ReaderT.run c env) stt -def CompileM.runIO' (maxHeartBeats: USize) (stt: CompileState) (c : CompileM α) - : IO (α × CompileState) := do - let (res, stt) <- c.runIO maxHeartBeats stt - let res <- IO.ofExcept res - return (res, stt) - -def CompileM.liftIO (io: IO α): CompileM α := - monadLift io - -def liftStoreIO (io: StoreIO α): CompileM α := do - match <- CompileM.liftIO (EIO.toIO' io) with - | .ok a => return a - | .error e => throw (.storeError e) - -def writeToStore (const: Ixon.Const): CompileM Address := do - let addr <- if (<- read).persist - then liftStoreIO (Store.writeConst const) - else pure (Address.blake3 (Ixon.Serialize.put const)) +def storeConst (const: Ixon.Const): CompileM Address := do + let addr := Address.blake3 (Ixon.Serialize.put const) modifyGet fun stt => (addr, { stt with store := stt.store.insert addr const }) -def IO.freshSecret : IO Address := do - IO.setRandSeed (← IO.monoNanosNow) - let mut secret : ByteArray := default +def randByte (lo hi: Nat): CompileM Nat := do + modifyGet fun s => + let (res, g') := randNat s.prng lo hi + (res, {s with prng := g'}) + +def freshSecret : CompileM Address := do + let mut secret: ByteArray := default for _ in [:32] do - let rand ← IO.rand 0 (UInt8.size - 1) + let rand <- randByte 0 255 secret := secret.push rand.toUInt8 return ⟨secret⟩ -def freshSecret : CompileM Address := do - CompileM.liftIO IO.freshSecret +-- add binding name to local context +def withCurrent (name: Lean.Name) : CompileM α -> CompileM α := + withReader $ fun c => { c with current := name } -- add binding name to local context def withBinder (name: Lean.Name) : CompileM α -> CompileM α := @@ -120,7 +118,8 @@ def withLevels (lvls : List Lean.Name) : CompileM α -> CompileM α := withReader $ fun c => { c with univCtx := lvls } -- add mutual recursion info to local context -def withMutCtx (mutCtx : RBMap Lean.Name Nat compare) : CompileM α -> CompileM α := +def withMutCtx (mutCtx : RBMap Lean.Name Nat compare) + : CompileM α -> CompileM α := withReader $ fun c => { c with mutCtx := mutCtx } -- reset local context @@ -138,8 +137,8 @@ def hashConst (const: Ix.Const) : CompileM (Address × Address) := do let (anonIxon, metaIxon) <- match constToIxon const with | .ok (a, m) => pure (a, m) | .error e => throw (.transportError e) - let anonAddr <- writeToStore anonIxon - let metaAddr <- writeToStore metaIxon + let anonAddr <- storeConst anonIxon + let metaAddr <- storeConst metaIxon modifyGet fun stt => ((anonAddr, metaAddr), { stt with cache := stt.cache.insert const (anonAddr, metaAddr) }) @@ -153,33 +152,38 @@ def concatOrds : List Ordering → Ordering := List.foldl (· * ·) .eq /-- Defines an ordering for Lean universes -/ -def compareLevel (x : Lean.Level) (y : Lean.Level) : CompileM Ordering := - match x, y with - | .mvar .., _ => throw $ .unfilledLevelMetavariable x - | _, .mvar .. => throw $ .unfilledLevelMetavariable y +def compareLevel (xctx yctx: List Lean.Name) + : Lean.Level -> Lean.Level -> CompileM Ordering + | x@(.mvar ..), _ => throw $ .unfilledLevelMetavariable x + | _, y@(.mvar ..) => throw $ .unfilledLevelMetavariable y | .zero, .zero => return .eq | .zero, _ => return .lt | _, .zero => return .gt - | .succ x, .succ y => compareLevel x y + | .succ x, .succ y => compareLevel xctx yctx x y | .succ .., _ => return .lt | _, .succ .. => return .gt - | .max lx ly, .max rx ry => - (· * ·) <$> compareLevel lx rx <*> compareLevel ly ry + | .max xl xr, .max yl yr => do + let l' <- compareLevel xctx yctx xl yl + let r' <- compareLevel xctx yctx xr yr + return l' * r' | .max .., _ => return .lt | _, .max .. => return .gt - | .imax lx ly, .imax rx ry => - (· * ·) <$> compareLevel lx rx <*> compareLevel ly ry + | .imax xl xr, .imax yl yr => do + let l' <- compareLevel xctx yctx xl yl + let r' <- compareLevel xctx yctx xr yr + return l' * r' | .imax .., _ => return .lt | _, .imax .. => return .gt | .param x, .param y => do - let lvls := (← read).univCtx - match (lvls.idxOf? x), (lvls.idxOf? y) with + match (xctx.idxOf? x), (yctx.idxOf? y) with | some xi, some yi => return (compare xi yi) - | none, _ => throw $ .levelNotFound x lvls - | _, none => throw $ .levelNotFound y lvls + | none, _ => + throw $ .levelNotFound x xctx s!"compareLevel @ {(<- read).current}" + | _, none => + throw $ .levelNotFound y yctx s!"compareLevel @ {(<- read).current}" /-- Canonicalizes a Lean universe level and adds it to the store -/ -def compileLevel : Lean.Level → CompileM Ix.Univ +def compileLevel : Lean.Level → CompileM Ix.Level | .zero => pure .zero | .succ u => return .succ (← compileLevel u) | .max a b => return .max (← compileLevel a) (← compileLevel b) @@ -187,8 +191,8 @@ def compileLevel : Lean.Level → CompileM Ix.Univ | .param name => do let lvls := (← read).univCtx match lvls.idxOf? name with - | some n => pure $ .var name n - | none => throw $ .levelNotFound name lvls + | some n => pure $ .param name n + | none => throw $ .levelNotFound name lvls s!"compileLevel @ {(<- read).current}" | l@(.mvar ..) => throw $ .unfilledLevelMetavariable l /-- Retrieves a Lean constant from the environment by its name -/ @@ -212,94 +216,91 @@ mutual /-- compile Lean Constant --/ partial def compileConst (const : Lean.ConstantInfo) : CompileM (Address × Address) := do + -- first check if we've already compiled this const match (← get).names.find? const.name with - | some (anonAddr, metaAddr) => pure (anonAddr, metaAddr) - | none => match const with - | .defnInfo val => - resetCtxWithLevels val.levelParams $ compileDefinition val - | .inductInfo val => - resetCtxWithLevels val.levelParams $ compileInductive val + -- if we have, returned the cached address + | some (anonAddr, metaAddr) => do + pure (anonAddr, metaAddr) + -- if not, pattern match on the const + | none => resetCtx $ withCurrent const.name $ match const with + -- convert possible mutual block elements to PreDefinitions + | .defnInfo val => do + compileDefinition (mkPreDefinition val) + | .thmInfo val => do + compileDefinition (mkPreTheorem val) + | .opaqueInfo val => do + compileDefinition (mkPreOpaque val) + -- compile possible mutual inductive block elements + | .inductInfo val => do + compileInductive val + -- compile constructors through their parent inductive | .ctorInfo val => do match ← findLeanConst val.induct with - | .inductInfo ind => discard $ compileConst (.inductInfo ind) + | .inductInfo ind => do + let _ <- compileInductive ind + compileConst (.ctorInfo val) | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - -- this should return by finding the ctor in names via the above some case - compileConst const + -- compile recursors through their parent inductive | .recInfo val => do match ← findLeanConst val.getMajorInduct with - | .inductInfo ind => discard $ compileConst (.inductInfo ind) + | .inductInfo ind => do + let _ <- compileInductive ind + compileConst (.recInfo val) | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - -- this should return by finding the recr in names via the above some case - compileConst const -- The rest adds the constants to the cache one by one | .axiomInfo val => resetCtxWithLevels const.levelParams do - let c := .axiom ⟨val.levelParams.length, ← compileExpr val.type⟩ + let c := .axiom ⟨val.name, val.levelParams, ← compileExpr val.type, val.isUnsafe⟩ let (anonAddr, metaAddr) ← hashConst c modify fun stt => { stt with axioms := stt.axioms.insert const.name (anonAddr, metaAddr) names := stt.names.insert const.name (anonAddr, metaAddr) } - return (metaAddr, metaAddr) - | .thmInfo val => resetCtxWithLevels const.levelParams do - let type <- compileExpr val.type - let value <- compileExpr val.value - let c := .theorem ⟨val.levelParams.length, type, value⟩ - let (anonAddr, metaAddr) ← hashConst c - modify fun stt => { stt with - names := stt.names.insert const.name (anonAddr, metaAddr) - } - return (metaAddr, metaAddr) - | .opaqueInfo val => resetCtxWithLevels const.levelParams do - let mutCtx := .single val.name 0 - let type <- compileExpr val.type - let value <- withMutCtx mutCtx $ compileExpr val.value - let c := .opaque ⟨val.levelParams.length, type, value⟩ - let (anonAddr, metaAddr) ← hashConst c - modify fun stt => { stt with - names := stt.names.insert const.name (anonAddr, metaAddr) - } - return (metaAddr, metaAddr) + return (anonAddr, metaAddr) | .quotInfo val => resetCtxWithLevels const.levelParams do let type <- compileExpr val.type - let c := .quotient ⟨val.levelParams.length, type, val.kind⟩ + let c := .quotient ⟨val.name, val.levelParams, type, val.kind⟩ let (anonAddr, metaAddr) ← hashConst c modify fun stt => { stt with axioms := (stt.axioms.insert const.name (anonAddr, metaAddr)) names := stt.names.insert const.name (anonAddr, metaAddr) } - return (metaAddr, metaAddr) + return (anonAddr, metaAddr) /-- compile possibly mutual Lean definition --/ -partial def compileDefinition (struct: Lean.DefinitionVal) +partial def compileDefinition (struct: PreDefinition) : CompileM (Address × Address) := do -- If the mutual size is one, simply content address the single definition if struct.all matches [_] then - let defn <- withMutCtx (.single struct.name 0) $ definitionToIR struct + let defn <- withMutCtx (.single struct.name 0) $ preDefinitionToIR struct let (anonAddr, metaAddr) <- hashConst $ .definition defn modify fun stt => { stt with names := stt.names.insert struct.name (anonAddr, metaAddr) } return (anonAddr, metaAddr) -- Collecting and sorting all definitions in the mutual block - let mutualDefs <- struct.all.mapM fun name => do - match <- findLeanConst name with - | .defnInfo defn => pure defn - | const => - throw $ .invalidConstantKind const.name "definition" const.ctorName - let mutualDefs <- sortDefs [mutualDefs] + let mut mutDefs : Array PreDefinition := #[] + for n in struct.all do + match <- findLeanConst n with + | .defnInfo x => mutDefs := mutDefs.push (mkPreDefinition x) + | .opaqueInfo x => mutDefs := mutDefs.push (mkPreOpaque x) + | .thmInfo x => mutDefs := mutDefs.push (mkPreTheorem x) + | x => throw $ .invalidConstantKind x.name "mutdef" x.ctorName + let mutualDefs <- sortDefs mutDefs.toList -- Building the `mutCtx` let mut mutCtx := default - for (ds, i) in List.zipIdx mutualDefs do + let mut i := 0 + for ds in mutualDefs do + let mut x := #[] for d in ds do + x := x.push d.name mutCtx := mutCtx.insert d.name i - let definitions ← withMutCtx mutCtx $ mutualDefs.mapM (·.mapM definitionToIR) + i := i + 1 + let definitions ← withMutCtx mutCtx $ mutualDefs.mapM (·.mapM preDefinitionToIR) -- Building and storing the block - -- TODO: check if this flatten call actually makes sense - let definitionsIR := (definitions.map (match ·.head? with - | some d => [d] | none => [])).flatten - let (blockAnonAddr, blockMetaAddr) ← hashConst $ .mutDefBlock definitionsIR + let (blockAnonAddr, blockMetaAddr) ← + hashConst $ .mutual ⟨definitions⟩ modify fun stt => { stt with blocks := stt.blocks.insert (blockAnonAddr, blockMetaAddr) } -- While iterating on the definitions from the mutual block, we need to track @@ -310,7 +311,7 @@ partial def compileDefinition (struct: Lean.DefinitionVal) -- Also adds the constant to the array of constants let some idx := mutCtx.find? name | throw $ .cantFindMutDefIndex name let (anonAddr, metaAddr) ← - hashConst $ .definitionProj ⟨blockAnonAddr, blockMetaAddr, idx⟩ + hashConst $ .definitionProj ⟨name, blockAnonAddr, blockMetaAddr, idx⟩ modify fun stt => { stt with names := stt.names.insert name (anonAddr, metaAddr) } @@ -319,12 +320,48 @@ partial def compileDefinition (struct: Lean.DefinitionVal) | some ret => return ret | none => throw $ .constantNotContentAddressed struct.name - -partial def definitionToIR (defn: Lean.DefinitionVal) - : CompileM Ix.Definition := do - let type <- compileExpr defn.type - let value <- compileExpr defn.value - return ⟨defn.levelParams.length, type, value, defn.safety == .partial⟩ +partial def preDefinitionToIR (d: PreDefinition) + : CompileM Ix.Definition := withCurrent d.name $ withLevels d.levelParams do + let typ <- compileExpr d.type + let val <- compileExpr d.value + return ⟨d.name, d.levelParams, typ, d.mode, val, d.hints, d.safety, d.all⟩ + +partial def getRecursors (ind : Lean.InductiveVal) + : CompileM (List Lean.RecursorVal) := do + return (<- get).env.constants.fold accRecr [] + where + accRecr (acc: List Lean.RecursorVal) (n: Lean.Name) (c: Lean.ConstantInfo) + : List Lean.RecursorVal := + match n with + | .str n .. + | .num n .. => + if n == ind.name then match c with + | .recInfo r => r :: acc + | _ => acc + else acc + | _ => acc + +partial def makePreInductive (ind: Lean.InductiveVal) + : CompileM Ix.PreInductive := do + let ctors <- ind.ctors.mapM getCtor + let recrs <- getRecursors ind + return ⟨ind.name, ind.levelParams, ind.type, ind.numParams, ind.numIndices, + ind.all, ctors, recrs, ind.numNested, ind.isRec, ind.isReflexive, ind.isUnsafe⟩ + where + getCtor (name: Lean.Name) : CompileM (Lean.ConstructorVal) := do + match (<- findLeanConst name) with + | .ctorInfo c => pure c + | _ => throw <| .invalidConstantKind name "constructor" "" + +partial def checkCtorRecrLengths : List PreInductive -> CompileM (Nat × Nat) +| [] => return (0, 0) +| x::xs => go x xs + where + go : PreInductive -> List PreInductive -> CompileM (Nat × Nat) + | x, [] => return (x.ctors.length, x.recrs.length) + | x, a::as => + if x.ctors.length == a.ctors.length && x.recrs.length == a.recrs.length + then go x as else throw <| .nonCongruentInductives x a /-- Content-addresses an inductive and all inductives in the mutual block as a @@ -335,32 +372,38 @@ constructors and recursors, hence the complexity of this function. -/ partial def compileInductive (initInd: Lean.InductiveVal) : CompileM (Address × Address) := do - let mut inds := [] - let mut indCtors := [] - let mut indRecs := [] + let mut preInds := #[] let mut nameData : RBMap Lean.Name (List Lean.Name × List Lean.Name) compare := .empty + -- collect all mutual inductives as Ix.PreInductives for indName in initInd.all do match ← findLeanConst indName with | .inductInfo ind => - let indRecrs := ((← get).env.constants.childrenOfWith ind.name - fun c => match c with | .recInfo _ => true | _ => false).map (·.name) - inds := inds ++ [indName] - indCtors := indCtors ++ ind.ctors - indRecs := indRecs ++ indRecrs - nameData := nameData.insert indName (ind.ctors, indRecrs) + let preInd <- makePreInductive ind + preInds := preInds.push preInd + nameData := nameData.insert indName (ind.ctors, preInd.recrs.map (·.name)) | const => 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 - let mutualConsts := inds ++ indCtors ++ indRecs - let mutCtx := mutualConsts.zipIdx.foldl (init := default) - fun acc (n, i) => acc.insert n i - -- This part builds the inductive block - -- and adds all inductives, constructors and recursors to `consts` - let irInds ← initInd.all.mapM fun name => do match ← findLeanConst name with - | .inductInfo ind => withMutCtx mutCtx do pure $ (← inductiveToIR ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - let (blockAnonAddr, blockMetaAddr) ← hashConst $ .mutIndBlock irInds + -- sort PreInductives into equivalence classes + let mutualInds <- sortInds preInds.toList + let mut mutCtx : RBMap Lean.Name Nat compare := default + let mut i := 0 + -- build the mutual context + for inds in mutualInds do + let mut x := #[] + -- double-check that all inductives in the class have the same number + -- of constructors and recursors + let (numCtors, numRecrs) <- checkCtorRecrLengths inds + for ind in inds do + x := x.push ind.name + mutCtx := mutCtx.insert ind.name i + for (c, cidx) in List.zipIdx ind.ctors do + mutCtx := mutCtx.insert c.name (i + cidx) + for (r, ridx) in List.zipIdx ind.recrs do + mutCtx := mutCtx.insert r.name (i + numCtors + ridx) + i := i + 1 + numCtors + numRecrs + -- compile each preinductive with the mutCtx + let irInds ← withMutCtx mutCtx $ mutualInds.mapM (·.mapM preInductiveToIR) + let (blockAnonAddr, blockMetaAddr) ← hashConst $ .inductive ⟨irInds⟩ modify fun stt => { stt with blocks := stt.blocks.insert (blockAnonAddr, blockMetaAddr) } -- While iterating on the inductives from the mutual block, we need to track @@ -370,7 +413,7 @@ partial def compileInductive (initInd: Lean.InductiveVal) -- Store and cache inductive projections let name := indName let (anonAddr, metaAddr) ← - hashConst $ .inductiveProj ⟨blockAnonAddr, blockMetaAddr, indIdx⟩ + hashConst $ .inductiveProj ⟨name, blockAnonAddr, blockMetaAddr, indIdx⟩ modify fun stt => { stt with names := stt.names.insert name (anonAddr, metaAddr) } @@ -381,7 +424,7 @@ partial def compileInductive (initInd: Lean.InductiveVal) -- Store and cache constructor projections let (anonAddr, metaAddr) ← hashConst $ .constructorProj - ⟨blockAnonAddr, blockMetaAddr, indIdx, ctorIdx⟩ + ⟨ctorName, blockAnonAddr, blockMetaAddr, indIdx, indName, ctorIdx⟩ modify fun stt => { stt with names := stt.names.insert ctorName (anonAddr, metaAddr) } @@ -389,7 +432,7 @@ partial def compileInductive (initInd: Lean.InductiveVal) -- Store and cache recursor projections let (anonAddr, metaAddr) ← hashConst $ .recursorProj - ⟨blockAnonAddr, blockMetaAddr, indIdx, recrIdx⟩ + ⟨recrName, blockAnonAddr, blockMetaAddr, indIdx, indName, recrIdx⟩ modify fun stt => { stt with names := stt.names.insert recrName (anonAddr, metaAddr) } @@ -397,69 +440,63 @@ partial def compileInductive (initInd: Lean.InductiveVal) | some ret => return ret | none => throw $ .constantNotContentAddressed initInd.name -partial def inductiveToIR (ind : Lean.InductiveVal) : CompileM Ix.Inductive := do - let leanRecs := (← get).env.constants.childrenOfWith ind.name - fun c => match c with | .recInfo _ => true | _ => false - let (recs, ctors) ← leanRecs.foldrM (init := ([], [])) - fun r (recs, ctors) => match r with - | .recInfo rv => - if isInternalRec rv.type ind.name then do - let (thisRec, thisCtors) := ← internalRecToIR ind.ctors r +partial def preInductiveToIR (ind : Ix.PreInductive) : CompileM Ix.Inductive + := withCurrent ind.name $ withLevels ind.levelParams $ do + let (recs, ctors) := <- ind.recrs.foldrM (init := ([], [])) collectRecsCtors + let type <- compileExpr ind.type + -- NOTE: for the purpose of extraction, the order of `ctors` and `recs` MUST + -- match the order used in `mutCtx` + return ⟨ind.name, ind.levelParams, type, ind.numParams, ind.numIndices, + ind.all, ctors, recs, ind.numNested, ind.isRec, ind.isReflexive, ind.isUnsafe⟩ + where + collectRecsCtors + : Lean.RecursorVal + -> List Recursor × List Constructor + -> CompileM (List Recursor × List Constructor) + | r, (recs, ctors) => + if isInternalRec r.type ind.name then do + let (thisRec, thisCtors) <- internalRecToIR (ind.ctors.map (·.name)) r pure (thisRec :: recs, thisCtors) else do let thisRec ← externalRecToIR r pure (thisRec :: recs, ctors) - | _ => 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 - | [ctor] => pure (true, ctor.fields == 0) - | _ => pure (false, false) - return ⟨ind.levelParams.length, ← compileExpr ind.type, ind.numParams, ind.numIndices, - -- NOTE: for the purpose of extraction, the order of `ctors` and `recs` MUST - -- match the order used in `recrCtx` - ctors, recs, ind.isRec, ind.isReflexive, struct, unit⟩ - -partial def internalRecToIR (ctors : List Lean.Name) - : Lean.ConstantInfo → CompileM (Ix.Recursor × List Ix.Constructor) - | .recInfo rec => withLevels rec.levelParams do - let typ ← compileExpr rec.type - let (retCtors, retRules) ← rec.rules.foldrM (init := ([], [])) + +partial def internalRecToIR (ctors : List Lean.Name) (recr: Lean.RecursorVal) + : CompileM (Ix.Recursor × List Ix.Constructor) := + withCurrent recr.name $ withLevels recr.levelParams do + let typ ← compileExpr recr.type + let (retCtors, retRules) ← recr.rules.foldrM (init := ([], [])) fun r (retCtors, retRules) => do if ctors.contains r.ctor then let (ctor, rule) ← recRuleToIR r pure $ (ctor :: retCtors, rule :: retRules) else pure (retCtors, retRules) -- this is an external recursor rule - let recr := ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, - rec.numMotives, rec.numMinors, retRules, rec.k, true⟩ + let recr := ⟨recr.name, recr.levelParams, typ, recr.numParams, recr.numIndices, + recr.numMotives, recr.numMinors, retRules, recr.k, recr.isUnsafe⟩ return (recr, retCtors) - | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName + +partial def externalRecToIR (recr: Lean.RecursorVal): CompileM Recursor := + withCurrent recr.name $ withLevels recr.levelParams do + let typ ← compileExpr recr.type + let rules ← recr.rules.mapM externalRecRuleToIR + return ⟨recr.name, recr.levelParams, typ, recr.numParams, recr.numIndices, + recr.numMotives, recr.numMinors, rules, recr.k, recr.isUnsafe⟩ partial def recRuleToIR (rule : Lean.RecursorRule) : CompileM (Ix.Constructor × Ix.RecursorRule) := do let rhs ← compileExpr rule.rhs match ← findLeanConst rule.ctor with - | .ctorInfo ctor => withLevels ctor.levelParams do + | .ctorInfo ctor => withCurrent ctor.name $ withLevels ctor.levelParams do let typ ← compileExpr ctor.type let ctor := - ⟨ctor.levelParams.length, typ, ctor.cidx, ctor.numParams, ctor.numFields⟩ - pure (ctor, ⟨rule.nfields, rhs⟩) + ⟨ctor.name, ctor.levelParams, typ, ctor.cidx, ctor.numParams, ctor.numFields, ctor.isUnsafe⟩ + pure (ctor, ⟨rule.ctor, rule.nfields, rhs⟩) | const => throw $ .invalidConstantKind const.name "constructor" const.ctorName -partial def externalRecToIR : Lean.ConstantInfo → CompileM Recursor - | .recInfo rec => withLevels rec.levelParams do - let typ ← compileExpr rec.type - 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 - partial def externalRecRuleToIR (rule : Lean.RecursorRule) : CompileM RecursorRule := - return ⟨rule.nfields, ← compileExpr rule.rhs⟩ + return ⟨rule.ctor, rule.nfields, ← compileExpr rule.rhs⟩ /-- Content-addresses a Lean expression and adds it to the store. @@ -482,7 +519,7 @@ partial def compileExpr : Lean.Expr → CompileM Expr let univs ← lvls.mapM compileLevel match (← read).mutCtx.find? name with -- recursing! - | some i => return .rec_ i univs + | some i => return .rec_ name i univs | none => match (<- get).comms.find? name with | some (commAddr, metaAddr) => do return .const name commAddr metaAddr univs @@ -505,100 +542,70 @@ partial def compileExpr : Lean.Expr → CompileM Expr | .mvar .. => throw $ .metaVariableExpr expr | .mdata .. => throw $ .metaDataExpr expr -partial def makeLeanDef - (name: Lean.Name) (levelParams: List Lean.Name) (type value: Lean.Expr) - : Lean.DefinitionVal := - { name, levelParams, type, value, hints := .opaque, safety := .safe } - -partial def tryAddLeanDecl (defn: Lean.DefinitionVal) : CompileM Unit := do - match (<- get).env.constants.find? defn.name with - | some _ => pure () - | none => do - let env <- (·.env) <$> get - let maxHeartBeats <- (·.maxHeartBeats) <$> read - let decl := Lean.Declaration.defnDecl defn - match Lean.Environment.addDeclCore env maxHeartBeats decl .none with - | .ok e => do - modify fun stt => { stt with env := e } - return () - | .error e => do - let x <- (e.toMessageData .empty).format - throw $ .kernelException (x.pretty 80) - -partial def addDef (lvls: List Lean.Name) (typ val: Lean.Expr) - : CompileM (Address × Address) := do - let typ' <- compileExpr typ - let val' <- compileExpr val - let (a, m) <- hashConst $ Ix.Const.definition ⟨lvls.length, typ', val', true⟩ - tryAddLeanDecl (makeLeanDef a.toUniqueName lvls typ val) - return (a, m) - -partial def commitConst (anon meta: Address) - : CompileM (Address × Address) := do - let secret <- freshSecret - let comm := .comm ⟨secret, anon⟩ - let commAddr <- writeToStore comm - let commMeta := .comm ⟨secret, meta⟩ - let commMetaAddr <- writeToStore commMeta - modify fun stt => { stt with - comms := stt.comms.insert commAddr.toUniqueName (commAddr, commMetaAddr) - } - return (commAddr, commMetaAddr) - -partial def commitDef (lvls: List Lean.Name) (typ val: Lean.Expr) - : CompileM (Address × Address) := do - let (a, m) <- addDef lvls typ val - let (ca, cm) <- commitConst a m - tryAddLeanDecl (makeLeanDef ca.toUniqueName lvls typ val) - --tryAddLeanDecl (makeLeanDef ca.toUniqueName lvls typ (mkConst a.toUniqueName [])) - return (ca, cm) - /-- A name-irrelevant ordering of Lean expressions. `weakOrd` contains the best known current mutual ordering -/ -partial def compareExpr (weakOrd : RBMap Lean.Name Nat compare) +partial def compareExpr + (weakOrd : RBMap Lean.Name Nat compare) + (xlvls ylvls: List Lean.Name) : Lean.Expr → Lean.Expr → CompileM Ordering | e@(.mvar ..), _ => throw $ .unfilledExprMetavariable e | _, e@(.mvar ..) => throw $ .unfilledExprMetavariable e | e@(.fvar ..), _ => throw $ .freeVariableExpr e | _, e@(.fvar ..) => throw $ .freeVariableExpr e - | .mdata _ x, .mdata _ y => compareExpr weakOrd x y - | .mdata _ x, y => compareExpr weakOrd x y - | x, .mdata _ y => compareExpr weakOrd x y + | .mdata _ x, .mdata _ y => compareExpr weakOrd xlvls ylvls x y + | .mdata _ x, y => compareExpr weakOrd xlvls ylvls x y + | x, .mdata _ y => compareExpr weakOrd xlvls ylvls x y | .bvar x, .bvar y => return (compare x y) | .bvar .., _ => return .lt | _, .bvar .. => return .gt - | .sort x, .sort y => compareLevel x y + | .sort x, .sort y => compareLevel xlvls ylvls x y | .sort .., _ => return .lt | _, .sort .. => return .gt | .const x xls, .const y yls => do - let univs ← concatOrds <$> (xls.zip yls).mapM fun (x,y) => compareLevel x y - if univs != .eq then return univs + let univs ← concatOrds <$> (xls.zip yls).mapM + fun (x,y) => compareLevel xlvls ylvls x y + if univs != .eq then + return univs match weakOrd.find? x, weakOrd.find? y with | some nx, some ny => return compare nx ny - | none, some _ => return .gt - | some _, none => return .lt + | none, some _ => do + return .gt + | some _, none => + return .lt | none, none => - return compare - (← compileConst $ ← findLeanConst x) - (← compileConst $ ← findLeanConst y) + if x == y then + return .eq + else do + let x' <- compileConst $ ← findLeanConst x + let y' <- compileConst $ ← findLeanConst y + return compare x' y' | .const .., _ => return .lt | _, .const .. => return .gt - | .app xf xa, .app yf ya => - (· * ·) <$> compareExpr weakOrd xf yf <*> compareExpr weakOrd xa ya + | .app xf xa, .app yf ya => do + let f' <- compareExpr weakOrd xlvls ylvls xf yf + let a' <- compareExpr weakOrd xlvls ylvls xa ya + return f' * a' | .app .., _ => return .lt | _, .app .. => return .gt - | .lam _ xt xb _, .lam _ yt yb _ => - (· * ·) <$> compareExpr weakOrd xt yt <*> compareExpr weakOrd xb yb + | .lam _ xt xb _, .lam _ yt yb _ => do + let t' <- compareExpr weakOrd xlvls ylvls xt yt + let b' <- compareExpr weakOrd xlvls ylvls xb yb + return t' * b' | .lam .., _ => return .lt | _, .lam .. => return .gt - | .forallE _ xt xb _, .forallE _ yt yb _ => - (· * ·) <$> compareExpr weakOrd xt yt <*> compareExpr weakOrd xb yb + | .forallE _ xt xb _, .forallE _ yt yb _ => do + let t' <- compareExpr weakOrd xlvls ylvls xt yt + let b' <- compareExpr weakOrd xlvls ylvls xb yb + return t' * b' | .forallE .., _ => return .lt | _, .forallE .. => return .gt - | .letE _ xt xv xb _, .letE _ yt yv yb _ => - (· * · * ·) <$> compareExpr weakOrd xt yt <*> compareExpr weakOrd xv yv <*> compareExpr weakOrd xb yb + | .letE _ xt xv xb _, .letE _ yt yv yb _ => do + let t' <- compareExpr weakOrd xlvls ylvls xt yt + let v' <- compareExpr weakOrd xlvls ylvls xv yv + let b' <- compareExpr weakOrd xlvls ylvls xb yb + return t' * v' * b' | .letE .., _ => return .lt | _, .letE .. => return .gt | .lit x, .lit y => @@ -606,26 +613,26 @@ partial def compareExpr (weakOrd : RBMap Lean.Name Nat compare) | .lit .., _ => return .lt | _, .lit .. => return .gt | .proj _ nx tx, .proj _ ny ty => do - let ts ← compareExpr weakOrd tx ty + let ts ← compareExpr weakOrd xlvls ylvls tx ty return concatOrds [compare nx ny, ts] /-- AST comparison of two Lean definitions. `weakOrd` contains the best known current mutual ordering -/ partial def compareDef (weakOrd : RBMap Lean.Name Nat compare) - (x : Lean.DefinitionVal) - (y : Lean.DefinitionVal) + (x y: PreDefinition) : CompileM Ordering := do + let mode := compare x.mode y.mode let ls := compare x.levelParams.length y.levelParams.length - let ts ← compareExpr weakOrd x.type y.type - let vs ← compareExpr weakOrd x.value y.value - return concatOrds [ls, ts, vs] + let ts ← compareExpr weakOrd x.levelParams y.levelParams x.type y.type + let vs ← compareExpr weakOrd x.levelParams y.levelParams x.value y.value + return concatOrds [mode, ls, ts, vs] /-- AST equality between two Lean definitions. `weakOrd` contains the best known current mutual ordering -/ @[inline] partial def eqDef (weakOrd : RBMap Lean.Name Nat compare) - (x y : Lean.DefinitionVal) + (x y : PreDefinition) : CompileM Bool := return (← compareDef weakOrd x y) == .eq @@ -665,9 +672,9 @@ Two optimizations: them as lists. To fix this, we sort the list by name before comparing. Note we could maybe also use `List (RBTree ..)` everywhere, but it seemed like a hassle. -/ -partial def sortDefs (dss : List (List Lean.DefinitionVal)) : - CompileM (List (List Lean.DefinitionVal)) := do - let enum (ll : List (List Lean.DefinitionVal)) := +partial def sortPreDefs (dss : List (List PreDefinition)) : + CompileM (List (List PreDefinition)) := do + let enum (ll : List (List PreDefinition)) := RBMap.ofList (ll.zipIdx.map fun (xs, n) => xs.map (·.name, n)).flatten let weakOrd := enum dss _ let newDss ← (← dss.mapM fun ds => @@ -676,28 +683,218 @@ partial def sortDefs (dss : List (List Lean.DefinitionVal)) : | [d] => pure [[d]] | ds => do pure $ (← List.groupByM (eqDef weakOrd) $ ← ds.sortByM (compareDef weakOrd))).joinM - -- must normalize, see comments let normDss := dss.map fun ds => ds.map (·.name) |>.sort let normNewDss := newDss.map fun ds => ds.map (·.name) |>.sort if normDss == normNewDss then return newDss - else sortDefs newDss + else sortPreDefs newDss + +partial def sortDefs: List PreDefinition -> CompileM (List (List PreDefinition)) +| [] => return [] +| xs => sortDefs' [xs.sortBy (fun x y => compare x.name y.name)] + +partial def weakOrdDefs (dss: List (List PreDefinition)) + : CompileM (RBMap Lean.Name Nat compare) := do + let mut weakOrd := default + for (ds, n) in dss.zipIdx do + for d in ds do + weakOrd := weakOrd.insert d.name n + return weakOrd + +partial def sortDefs' (dss: List (List PreDefinition)) + : CompileM (List (List PreDefinition)) := do + let weakOrd <- weakOrdDefs dss + let mut dss' : Array (List PreDefinition) := default + for ds in dss do + match ds with + | [] => throw <| .emptyDefsEquivalenceClass dss + | [d] => dss' := dss'.push [d] + | ds => do + let ds' <- ds.sortByM (compareDef weakOrd) + let ds' <- List.groupByM (eqDef weakOrd) ds' + for d in ds' do + let d' <- d.sortByM (fun x y => pure $ compare x.name y.name) + dss' := dss'.push d' + if dss == dss'.toList + then return dss + else sortDefs' dss'.toList + + +/-- AST comparison of two Lean opaque definitions. + `weakOrd` contains the best known current mutual ordering -/ +partial def compareInd + (weakOrd : RBMap Lean.Name Nat compare) + (x y: PreInductive) + : CompileM Ordering := do + let ls := compare x.levelParams.length y.levelParams.length + let ts ← compareExpr weakOrd x.levelParams y.levelParams x.type y.type + let nps := compare x.numParams y.numParams + let nis := compare x.numIndices y.numIndices + let ctors <- compareListM compareCtors x.ctors y.ctors + let recrs <- compareListM compareRecrs x.recrs y.recrs + return concatOrds [ls, ts,nps, nis, ctors, recrs] + where + compareCtors (x y: Lean.ConstructorVal) : CompileM Ordering := do + let ls := compare x.levelParams.length y.levelParams.length + let ts <- compareExpr weakOrd x.levelParams y.levelParams x.type y.type + let cis := compare x.cidx y.cidx + let nps := compare x.numParams y.numParams + let nfs := compare x.numFields y.numFields + return concatOrds [ls, ts, cis, nps, nfs] + compareRecrs (x y: Lean.RecursorVal) : CompileM Ordering := do + let ls := compare x.levelParams.length y.levelParams.length + let ts <- compareExpr weakOrd x.levelParams y.levelParams x.type y.type + let nps := compare x.numParams y.numParams + let nis := compare x.numIndices y.numIndices + let nmos := compare x.numMotives y.numMotives + let nmis := compare x.numMinors y.numMinors + let rrs <- compareListM (compareRules x.levelParams y.levelParams) x.rules y.rules + let ks := compare x.k y.k + return concatOrds [ls, ts, nps, nis, nmos, nmis, rrs, ks] + compareRules (xlvls ylvls: List Lean.Name) (x y: Lean.RecursorRule) + : CompileM Ordering := do + let nfs := compare x.nfields y.nfields + let rs <- compareExpr weakOrd xlvls ylvls x.rhs y.rhs + return concatOrds [nfs, rs] + +/-- AST equality between two Lean opaque definitions. + `weakOrd` contains the best known current mutual ordering -/ +@[inline] partial def eqInd + (weakOrd : RBMap Lean.Name Nat compare) + (x y : PreInductive) + : CompileM Bool := + return (← compareInd weakOrd x y) == .eq + +partial def sortInds: List PreInductive -> CompileM (List (List PreInductive)) +| [] => return [] +| xs => sortInds' [xs.sortBy (fun x y => compare x.name y.name)] + +-- e_1 e_2 e_k +-- [ [i_1_1, i_1_2, ..., i_1_E1], [i_2_1, i_2_2, ..., i_1_E2], ... [i_k_1, i_k_2, ..., i_k_EK]] +-- let x be the class index, and y be the inductive index within the class +-- i_x_y contains c constructors and r recursors, each with a `cidx` +-- constructor index and a `ridx` recursor index +-- to construct a weak ordering, we need to create a natural number index `n` for each +-- inductive, constructor and recursors in the list of equivalence classes, such +-- that inductives in the same class, constructors with the same cidx, and +-- recursors with the same ridx all have the same weak index + +partial def weakOrdInds (iss: List (List PreInductive)) + : CompileM (RBMap Lean.Name Nat compare) := do + let mut weakOrd := default + let mut idx := 0 + for is in iss do + let mut maxCtors := 0 + let mut maxRecrs := 0 + for i in is do + weakOrd := weakOrd.insert i.name idx + let numCtors := i.ctors.length + let numRecrs := i.recrs.length + if numCtors > maxCtors then maxCtors := numCtors + if numRecrs > maxRecrs then maxRecrs := numRecrs + for (ctor, cidx) in i.ctors.zipIdx do + weakOrd := weakOrd.insert ctor.name (idx + 1 + cidx ) + for (recr, ridx) in i.recrs.zipIdx do + weakOrd := weakOrd.insert recr.name (idx + 1 + numCtors + ridx) + idx := idx + 1 + maxCtors + maxRecrs + return weakOrd + +partial def sortInds' (iss: List (List PreInductive)) + : CompileM (List (List PreInductive)) := do + let weakOrd <- weakOrdInds iss + let mut iss' : Array (List PreInductive) := default + for is in iss do + match is with + | [] => throw <| .emptyIndsEquivalenceClass iss + | [i] => iss' := iss'.push [i] + | is => do + let is' <- is.sortByM (compareInd weakOrd) + let is' <- List.groupByM (eqInd weakOrd) is' + for i in is' do + let i' <- i.sortByM (fun x y => pure $ compare x.name y.name) + iss' := iss'.push i' + if iss == iss'.toList + then return iss + else sortInds' iss'.toList end +partial def makeLeanDef + (name: Lean.Name) (levelParams: List Lean.Name) (type value: Lean.Expr) + : Lean.DefinitionVal := + { name, levelParams, type, value, hints := .opaque, safety := .safe } + +partial def tryAddLeanDef (defn: Lean.DefinitionVal) : CompileM Unit := do + match (<- get).env.constants.find? defn.name with + | some _ => pure () + | none => do + let env <- (·.env) <$> get + let maxHeartBeats <- (·.maxHeartBeats) <$> read + let decl := Lean.Declaration.defnDecl defn + match Lean.Environment.addDeclCore env maxHeartBeats decl .none with + | .ok e => do + modify fun stt => { stt with env := e } + return () + | .error e => throw $ .kernelException e + +partial def addDef + (lvls: List Lean.Name) + (typ val: Lean.Expr) + : CompileM (Address × Address) := do + let typ' <- compileExpr typ + let val' <- compileExpr val + let anonConst := Ix.Const.definition + ⟨.anonymous, lvls, typ', .definition, val', .opaque, .safe, []⟩ + let anonIxon <- match constToIxon anonConst with + | .ok (a, _) => pure a + | .error e => throw (.transportError e) + let anonAddr <- storeConst anonIxon + let name := anonAddr.toUniqueName + let const := + Ix.Const.definition ⟨name, lvls, typ', .definition, val', .opaque, .safe, []⟩ + let (a, m) <- hashConst const + if a != anonAddr then + throw <| .alphaInvarianceFailure anonConst anonAddr const a + else + tryAddLeanDef (makeLeanDef a.toUniqueName lvls typ val) + return (a, m) + +partial def commitConst (anon meta: Address) + : CompileM (Address × Address) := do + let secret <- freshSecret + let comm := .comm ⟨secret, anon⟩ + let commAddr <- storeConst comm + let commMeta := .comm ⟨secret, meta⟩ + let commMetaAddr <- storeConst commMeta + modify fun stt => { stt with + comms := stt.comms.insert commAddr.toUniqueName (commAddr, commMetaAddr) + } + return (commAddr, commMetaAddr) + +partial def commitDef + (lvls: List Lean.Name) + (typ val: Lean.Expr) + : CompileM (Address × Address) := do + let (a, m) <- addDef lvls typ val + let (ca, cm) <- commitConst a m + tryAddLeanDef (makeLeanDef ca.toUniqueName lvls typ val) + --tryAddLeanDecl (makeLeanDef ca.toUniqueName lvls typ (mkConst a.toUniqueName [])) + return (ca, cm) + + partial def packLevel (lvls: Nat) (commit: Bool): CompileM Address := match Ixon.natPackAsAddress lvls with | some lvlsAddr => do if commit then let secret <- freshSecret let comm := .comm (Ixon.Comm.mk secret lvlsAddr) - let commAddr <- writeToStore comm + let commAddr <- storeConst comm modify fun stt => { stt with comms := stt.comms.insert commAddr.toUniqueName (commAddr, commAddr) } return commAddr else return lvlsAddr - | .none => throw .todo + | .none => throw $ .cantPackLevel lvls partial def checkClaim (const: Lean.Name) @@ -730,16 +927,6 @@ partial def evalClaim where comm a := if commit then commitConst (Prod.fst a) (Prod.snd a) else pure a -def compileConstIO (env : Lean.Environment ) (const: Lean.ConstantInfo) - : IO $ (Address × Address) × CompileState := do - let (a, s) <- (compileConst const).runIO 200000 (.init env) - let a <- IO.ofExcept a - return (a, s) - -def compileDelta (delta : Lean.PersistentHashMap Lean.Name Lean.ConstantInfo) - : CompileM Unit := do - delta.forM fun _ c => if !c.isUnsafe then discard $ compileConst c else pure () - /-- Content-addresses the "delta" of an environment, that is, the content that is added on top of the imports. @@ -748,14 +935,37 @@ Important: constants with open references in their expressions are filtered out. Open references are variables that point to names which aren't present in the `Lean.ConstMap`. -/ -def compileDeltaIO +def compileDelta (delta : Lean.PersistentHashMap Lean.Name Lean.ConstantInfo) + : CompileM Unit := delta.forM fun _ c => discard $ compileConst c + +def compileEnv (env: Lean.Environment) + : CompileM Unit := do + compileDelta env.getDelta + env.getConstMap.forM fun _ c => if !c.isUnsafe then discard $ compileConst c else pure () + +def CompileM.runIO (c : CompileM α) (env: Lean.Environment) - (delta : Lean.PersistentHashMap Lean.Name Lean.ConstantInfo) - : IO CompileState := do - let (res, stt) <- (compileDelta delta).runIO 200000 (.init env) - IO.ofExcept res - return stt + (maxHeartBeats: USize := 200000) + (seed : Option Nat := .none) + : IO (α × CompileState) := do + let seed <- match seed with + | .none => IO.monoNanosNow + | .some s => pure s + match c.run (.init maxHeartBeats) (.init env seed) with + | .ok a stt => do + stt.store.forM fun a c => discard $ (Store.forceWriteConst a c).toIO + return (a, stt) + | .error e _ => throw (IO.userError (<- e.pretty)) + +def CompileM.runIO' (c : CompileM α) + (stt: CompileState) + (maxHeartBeats: USize := 200000) + : IO (α × CompileState) := do + match c.run (.init maxHeartBeats) stt with + | .ok a stt => do + stt.store.forM fun a c => discard $ (Store.forceWriteConst a c).toIO + return (a, stt) + | .error e _ => throw (IO.userError (<- e.pretty)) def compileEnvIO (env: Lean.Environment) : IO CompileState := do - compileDeltaIO env env.getDelta - + Prod.snd <$> (compileDelta env.getDelta).runIO env diff --git a/Ix/DecompileM.lean b/Ix/DecompileM.lean new file mode 100644 index 00000000..38cf8c59 --- /dev/null +++ b/Ix/DecompileM.lean @@ -0,0 +1,417 @@ +import Batteries.Data.RBMap +import Ix.TransportM +import Ix.Ixon.Metadata +import Ix.Ixon.Const +import Ix.Ixon.Serialize +import Ix.Common +import Ix.Store +import Ix.CompileM + +open Batteries (RBMap) +open Batteries (RBSet) +open Ix.TransportM +open Ix.Compile + +namespace Ix.Decompile + +/- the current Ix constant being decompiled -/ +structure Named where + name: Lean.Name + cont: Address + meta: Address +deriving Inhabited, Repr + +instance : ToString Named where + toString n := s!"{n.cont}:{n.meta}-{n.name}" + +/- The local environment for the Ix -> Lean4 decompiler -/ +structure DecompileEnv where + names : RBMap Lean.Name (Address × Address) compare + store : RBMap Address Ixon.Const compare + univCtx : List Lean.Name + bindCtx : List Lean.Name + mutCtx : RBMap Lean.Name Nat compare + current: Named + deriving Repr, Inhabited + +/- initialize from an Ixon store and a name-index to the store -/ +def DecompileEnv.init + (names : RBMap Lean.Name (Address × Address) compare) + (store : RBMap Address Ixon.Const compare) + : DecompileEnv + := ⟨names, store, default, default, default, default⟩ + +/- a collection of an inductive datatype with its constructors and recursors -/ +structure InductiveBlock where + val: Lean.ConstantInfo + ctors: List Lean.ConstantInfo + recrs: List Lean.ConstantInfo +deriving Repr + +def InductiveBlock.contains (i: InductiveBlock) (name: Lean.Name) : Bool := + i.val.name == name || + i.ctors.any (fun c => c.name == name) || + i.recrs.any (fun r => r.name == name) + +/- A Block is one of the possible sets of Lean constants we could generate + from a pair of content and metadata Ix addresses -/ +inductive Block where +| single : Lean.ConstantInfo -> Block +| mutual : List Lean.ConstantInfo -> Block +| inductive: List InductiveBlock -> Block +deriving Repr + +def Block.contains (name: Lean.Name) : Block -> Bool +| .single const => const.name == name +| .mutual consts => consts.any (fun c => c.name == name) +| .inductive is => is.any (fun i => i.contains name) + +/- The name of an inductive datatype with the names of its constructors and +recursors. Used to create a BlockNames struct. +-/ +structure InductiveBlockNames where + val: Lean.Name + ctors: List Lean.Name + recrs: List Lean.Name +deriving Repr + +def InductiveBlockNames.contains (i: InductiveBlockNames) (name: Lean.Name) : Bool := + i.val == name || + i.ctors.any (fun c => c == name) || + i.recrs.any (fun r => r == name) + +/- A BlockNames struct is the names of a Block. Naively, the decompiler +operates by mapping content-address pairs to blocks, but since each block might +be mapped onto by many address pairs, we only record address pair to BlockNames +mapping, and separately keep a single level map of Lean.Name to +Lean.ConstantInfo +-/ +inductive BlockNames where +| single : Lean.Name -> BlockNames +| mutual : List Lean.Name -> BlockNames +| inductive : List InductiveBlockNames -> BlockNames +deriving Repr, Inhabited, Nonempty + +def BlockNames.contains (name: Lean.Name) : BlockNames -> Bool +| .single const => const == name +| .mutual consts => consts.any (fun c => c == name) +| .inductive is => is.any (fun i => i.contains name) + +structure DecompileState where + constants: RBMap Lean.Name Lean.ConstantInfo compare + blocks : RBMap (Address × Address) BlockNames compare + deriving Inhabited + +inductive DecompileError +| freeLevel (curr: Named) (ctx: List Lean.Name) (lvl: Lean.Name) (idx: Nat) +| mismatchedLevelName + (curr: Named) (ctx: List Lean.Name) (got: Lean.Name) + (exp: Lean.Name) (idx: Nat) +| invalidBVarIndex (curr: Named) (ctx: List Lean.Name) (idx: Nat) +| mismatchedMutIdx + (curr: Named) (ctx: RBMap Lean.Name Nat compare) (exp: Lean.Name) + (idx: Nat) (got: Nat) +| unknownMutual + (curr: Named) (ctx: RBMap Lean.Name Nat compare) (exp: Lean.Name) (idx: Nat) +| transport (curr: Named) (err: TransportError) (cont meta: Address) +| unknownName (curr: Named) (name: Lean.Name) +| unknownStoreAddress (curr: Named) (exp: Address) +| expectedIxonMetadata (curr: Named) (exp: Address) (got: Ixon.Const) +| badProjection + (curr: Named) (name: Lean.Name) (cont meta: Address) (msg: String) +| nonCongruentInductives (curr: Named) (x y: Ix.Inductive) +| nameNotInBlockNames + (curr: Named) (block: BlockNames) (name: Lean.Name) (cont meta: Address) +| nameNotInBlock + (curr: Named) (block: Block) (name: Lean.Name) (cont meta: Address) +| mismatchedName + (curr: Named) (exp: Lean.Name) (got: Lean.Name) (cont meta: Address) +| expectedNameInBlock + (curr: Named) (exp: Lean.Name) (got: BlockNames) (cont meta: Address) +| expectedDefnBlock (curr: Named) (exp: Lean.Name) (got: Block) (cont meta: Address) +| expectedMutDefBlock (curr: Named) (got: BlockNames) (cont meta: Address) +| expectedMutIndBlock (curr: Named) (got: BlockNames) (cont meta: Address) +| expectedMutIndConst (curr: Named) (got: Ix.Const) (cont meta: Address) +| expectedMutDefConst (curr: Named) (got: Ix.Const) (cont meta: Address) +| overloadedConstants (curr: Named) (x y: Lean.ConstantInfo) +| todo +deriving Repr + + +def DecompileError.pretty : DecompileError -> String +| .freeLevel c lvls n i => s!"Free level {n} at {i} with ctx {repr lvls} @ {c}" +| .mismatchedLevelName c ctx n' n i => + s!"Expected level name {n} at index {i} but got {n'} with context {repr ctx} @ {c}" +| .invalidBVarIndex c ctx i => + s!"Bound variable {i} escapes context {ctx} @ {c}" +| .mismatchedMutIdx c ctx n i i' => + s!"expected mutual recusion index {i} at name {n} but got {i'} with context {repr ctx} @ {c}" +| .unknownMutual c ctx n i => + s!"unknown mutual name {n} with expected index {i} with context {repr ctx} @ {c}" +| .transport curr e c m => s!"decompiler transport error {e} at {c} {m} @ {curr}" +| .unknownName c n => s!"unknown name {n} @ {c}" +| .unknownStoreAddress c x => s!"unknown store address {x} @ {c}" +| .expectedIxonMetadata c x ixon => s!"expected metadata at address {x}, got {repr ixon} @ {c}" +| .badProjection curr n c m s => s!"bad projection {n} at address {c}:{m}, {s} @ {curr}" +| .nonCongruentInductives c x y => s!"noncongruent inductives {repr x} {repr y} @ {c}" +| .nameNotInBlockNames curr b n c m => s!"expected block names {repr b} at {c}:{m} to contain {n} @ {curr}" +| .nameNotInBlock curr b n c m => s!"expected block {repr b} at {c}:{m} to contain {n} @ {curr}" +| .mismatchedName curr e g c m => + s!"expected name {e}, got {g} at address {c} {m} @ {curr}" +| .expectedNameInBlock curr e b c m => + s!"expected name {e} in block {repr b} at address {c} {m} @ {curr}" +| .expectedDefnBlock curr e g c m => + s!"expected definition named {e}, got {repr g} at address {c} {m} @ {curr}" +| .expectedMutDefBlock curr g c m => + s!"expected mutual definition block, got {repr g} at address {c} {m} @ {curr}" +| .expectedMutIndBlock curr g c m => + s!"expected mutual inductive block, got {repr g} at address {c} {m} @ {curr}" +| .expectedMutIndConst curr g c m => + s!"expected mutual inductive constant, got {repr g} at address {c} {m} @ {curr}" +| .expectedMutDefConst curr g c m => + s!"expected mutual definition constant, got {repr g} at address {c} {m} @ {curr}" +| .overloadedConstants curr x y => + s!"overloaded constants, tried to overwrite {repr y} with {repr x} @ {curr}" +| .todo => s!"todo" + +abbrev DecompileM := ReaderT DecompileEnv <| EStateM DecompileError DecompileState + +def DecompileM.run (env: DecompileEnv) (stt: DecompileState) (c : DecompileM α) + : EStateM.Result DecompileError DecompileState α + := EStateM.run (ReaderT.run c env) stt + +-- add binding name to local context +def withBinder (name: Lean.Name) : DecompileM α -> DecompileM α := + withReader $ fun c => { c with bindCtx := name :: c.bindCtx } + +-- add levels to local context +def withLevels (lvls : List Lean.Name) : DecompileM α -> DecompileM α := + withReader $ fun c => { c with univCtx := lvls } + +-- add mutual recursion info to local context +def withMutCtx (mutCtx : RBMap Lean.Name Nat compare) + : DecompileM α -> DecompileM α := + withReader $ fun c => { c with mutCtx := mutCtx } + +def withNamed (name: Lean.Name) (cont meta: Address) + : DecompileM α -> DecompileM α := + withReader $ fun c => { c with current := ⟨name, cont, meta⟩ } + +-- reset local context +def resetCtx : DecompileM α -> DecompileM α := + withReader $ fun c => { c with univCtx := [], bindCtx := [], mutCtx := .empty } + +def resetCtxWithLevels (lvls: List Lean.Name) : DecompileM α -> DecompileM α := + withReader $ fun c => { c with univCtx := lvls, bindCtx := [], mutCtx := .empty } + +def decompileLevel: Ix.Level → DecompileM Lean.Level +| .zero => pure .zero +| .succ u => .succ <$> decompileLevel u +| .max a b => Lean.Level.max <$> decompileLevel a <*> decompileLevel b +| .imax a b => Lean.Level.imax <$> decompileLevel a <*> decompileLevel b +| .param n i => do + let env <- read + match env.univCtx[i]? with + | some n' => + if n == n' then pure (Lean.Level.param n) + else throw (.mismatchedLevelName env.current env.univCtx n' n i) + | none => throw <| .freeLevel env.current env.univCtx n i + +partial def insertConst + (const: Lean.ConstantInfo) + : DecompileM Lean.Name := do + match (<- get).constants.find? const.name with + | .some const' => + if const == const' then return const.name + else throw <| .overloadedConstants (<- read).current const const' + | .none => modify fun stt => + { stt with constants := stt.constants.insert const.name const } + return const.name + +partial def insertBlock (c m: Address) (b: Block) : DecompileM BlockNames := do + let bn <- match b with + | .single const => .single <$> insertConst const + | .mutual cs => .mutual <$> cs.mapM insertConst + | .inductive is => .inductive <$> is.mapM insertInductive + modifyGet fun stt => + (bn, { stt with blocks := stt.blocks.insert (c, m) bn }) + where + insertInductive (i: InductiveBlock) : DecompileM InductiveBlockNames := do + let val <- insertConst i.val + let ctors <- i.ctors.mapM insertConst + let recrs <- i.recrs.mapM insertConst + return ⟨val, ctors, recrs⟩ + +partial def decompileMutualCtx (ctx: List (List Lean.Name)) + : DecompileM (RBMap Lean.Name Nat compare) := do + let mut mutCtx : RBMap Lean.Name Nat compare := RBMap.empty + for (ns, i) in List.zipIdx ctx do + for n in ns do + mutCtx := mutCtx.insert n i + return mutCtx + +partial def checkCtorRecrLengths : List Ix.Inductive -> DecompileM (Nat × Nat) +| [] => return (0, 0) +| x::xs => go x xs + where + go : Ix.Inductive -> List Ix.Inductive -> DecompileM (Nat × Nat) + | x, [] => return (x.ctors.length, x.recrs.length) + | x, a::as => do + if x.ctors.length == a.ctors.length && x.recrs.length == a.recrs.length + then go x as else throw <| .nonCongruentInductives (<- read).current x a + +partial def decompileMutIndCtx (block: Ix.InductiveBlock) + : DecompileM (RBMap Lean.Name Nat compare) := do + let mut mutCtx : RBMap Lean.Name Nat compare := RBMap.empty + let mut i := 0 + for inds in block.inds do + let (numCtors, numRecrs) <- checkCtorRecrLengths inds + for ind in inds do + mutCtx := mutCtx.insert ind.name i + for (c, cidx) in List.zipIdx ind.ctors do + mutCtx := mutCtx.insert c.name (i + cidx) + for (r, ridx) in List.zipIdx ind.recrs do + mutCtx := mutCtx.insert r.name (i + numCtors + ridx) + i := i + 1 + numCtors + numRecrs + return mutCtx + +mutual + +partial def decompileExpr: Ix.Expr → DecompileM Lean.Expr +| .var i => do match (← read).bindCtx[i]? with + | some _ => return .bvar i + | none => throw <| .invalidBVarIndex (<-read).current (<-read).bindCtx i +| .sort u => Lean.Expr.sort <$> decompileLevel u +| .lit l => pure (.lit l) +| .app f a => Lean.mkApp <$> decompileExpr f <*> decompileExpr a +| .lam n bi t b => + Lean.mkLambda n bi <$> decompileExpr t <*> withBinder n (decompileExpr b) +| .pi n bi t b => + Lean.mkForall n bi <$> decompileExpr t <*> withBinder n (decompileExpr b) +| .letE n t v b nd => + (@Lean.mkLet n) + <$> decompileExpr t + <*> decompileExpr v + <*> withBinder n (decompileExpr b) + <*> pure nd +| .proj n cont meta i e => do + let _ <- ensureBlock n cont meta + Lean.mkProj n i <$> decompileExpr e +| .const n cont meta us => do + let _ <- ensureBlock n cont meta + return Lean.mkConst n (<- us.mapM decompileLevel) +| .rec_ n i us => do match (<- read).mutCtx.find? n with + | some i' => + if i == i' then return Lean.mkConst n (<- us.mapM decompileLevel) + else throw <| .mismatchedMutIdx (<- read).current (<- read).mutCtx n i i' + | none => throw <| .unknownMutual (<- read).current (<- read).mutCtx n i + +partial def ensureBlock (name: Lean.Name) (c m: Address) : DecompileM BlockNames := do + match (<- get).blocks.find? (c, m) with + | .some b => + if b.contains name then pure b + else throw <| .nameNotInBlockNames (<- read).current b name c m + | .none => + let cont : Ixon.Const <- match (<- read).store.find? c with + | .some ixon => pure ixon + | .none => throw <| .unknownStoreAddress (<- read).current c + let meta : Ixon.Const <- match (<- read).store.find? m with + | .some ixon => pure ixon + | .none => throw <| .unknownStoreAddress (<- read).current m + match rematerialize cont meta with + | .ok const => do + let blockNames <- withNamed name c m <| decompileConst const + if !blockNames.contains name then + throw <| .nameNotInBlockNames (<- read).current blockNames name c m + return blockNames + | .error e => throw (.transport (<- read).current e c m) + +partial def decompileDefn (x: Ix.Definition) + : DecompileM Lean.ConstantInfo := withLevels x.levelParams do + let type <- decompileExpr x.type + let val <- decompileExpr x.value + match x.mode with + | .definition => return .defnInfo <| + Lean.mkDefinitionValEx x.name x.levelParams type val x.hints x.safety x.all + | .opaque => return .opaqueInfo <| + Lean.mkOpaqueValEx x.name x.levelParams type val (x.safety == .unsafe) x.all + | .theorem => return .thmInfo <| + Lean.mkTheoremValEx x.name x.levelParams type val x.all + +partial def decompileIndc (x: Ix.Inductive) + : DecompileM + (Lean.ConstantInfo × List Lean.ConstantInfo × List Lean.ConstantInfo) + := withLevels x.levelParams do + let type <- decompileExpr x.type + let indc := + Lean.mkInductiveValEx x.name x.levelParams type x.numParams x.numIndices + x.all (x.ctors.map (·.name)) x.numNested x.isRec x.isUnsafe x.isReflexive + let ctors <- x.ctors.mapM (decompileCtor x.name) + let recrs <- x.recrs.mapM (decompileRecr x.all) + return (.inductInfo indc, ctors, recrs) + where + decompileCtor (indcName: Lean.Name) (x: Ix.Constructor) + : DecompileM Lean.ConstantInfo := withLevels x.levelParams do + let type <- decompileExpr x.type + return .ctorInfo <| + Lean.mkConstructorValEx x.name x.levelParams type indcName + x.cidx x.numParams x.numFields x.isUnsafe + decompileRecrRule (x: Ix.RecursorRule) : DecompileM Lean.RecursorRule := do + let rhs <- decompileExpr x.rhs + return ⟨x.ctor, x.nfields, rhs⟩ + decompileRecr (indcAll: List Lean.Name) (x: Ix.Recursor) + : DecompileM Lean.ConstantInfo := withLevels x.levelParams do + let type <- decompileExpr x.type + let rules <- x.rules.mapM decompileRecrRule + return .recInfo <| + Lean.mkRecursorValEx x.name x.levelParams type indcAll + x.numParams x.numIndices x.numMotives x.numMinors rules x.k x.isUnsafe + +-- TODO: name integrity +partial def decompileConst : Ix.Const -> DecompileM BlockNames +| .axiom x => withLevels x.levelParams do + let ⟨_, c, m⟩ := (<- read).current + let type <- decompileExpr x.type + let const := (.axiomInfo <| Lean.mkAxiomValEx x.name x.levelParams type x.isUnsafe) + insertBlock c m (.single const) +| .definition x => do + let ⟨_, c, m⟩ := (<- read).current + let const <- decompileDefn x + insertBlock c m (.single const) +| .quotient x => withLevels x.levelParams do + let ⟨_, c, m⟩ := (<- read).current + let type <- decompileExpr x.type + let const := (.quotInfo <| Lean.mkQuotValEx x.name x.levelParams type x.kind) + insertBlock c m (.single const) +| .inductiveProj x => ensureBlock x.name x.blockCont x.blockMeta +| .constructorProj x => ensureBlock x.induct x.blockCont x.blockMeta +| .recursorProj x => ensureBlock x.induct x.blockCont x.blockMeta +| .definitionProj x => ensureBlock x.name x.blockCont x.blockMeta +| .mutual x => do + let ⟨_, c, m⟩ := (<- read).current + let mutCtx <- decompileMutualCtx x.ctx + withMutCtx mutCtx do + let mut block := #[] + for defns in x.defs do + for defn in defns do + let const <- decompileDefn defn + block := block.push const + insertBlock c m (.mutual block.toList) +| .inductive x => do + let ⟨_, c, m⟩ := (<- read).current + let mutCtx <- decompileMutIndCtx x + withMutCtx mutCtx do + let mut block := #[] + for inds in x.inds do + for ind in inds do + let (i, cs, rs) <- decompileIndc ind + block := block.push ⟨i, cs, rs⟩ + insertBlock c m (Block.inductive block.toList) + +end + +def decompileEnv : DecompileM Unit := do + for (n, (anon, meta)) in (<- read).names do + let _ <- ensureBlock n anon meta + +end Decompile diff --git a/Ix/IR.lean b/Ix/IR.lean index 9e6010f9..3e7d93fb 100644 --- a/Ix/IR.lean +++ b/Ix/IR.lean @@ -1,4 +1,531 @@ -import Ix.IR.Univ -import Ix.IR.Expr -import Ix.IR.Const -import Ix.IR.Env +import Ix.Common +import Ix.Address + +namespace Ix + +/- +Ix.IR is an internal representation of the Lean kernel values defined in +[Lean.Declaration](https://leanprover-community.github.io/mathlib4_docs/Lean/Declaration.html) +The purpose of Ix.IR is to separate-in-place alpha-invariant or nameless +computational information from non-computational symbolic or ergonomic metadata. + +Ix.IR is generated as an intermediate output from the Ix compiler in Ix.CompileM, +in the course of generating the anonymously content-addressed Ixon bytecode. +Ix.IR is consumed by the Ix transporter in Ix.TransportM, which completes +separation or "dematerialization" of the Lean kernel into Ixon bytecode and Ixon +metadata. The transporter can also reconstitute, or "rematerialize" Ix IR from +the Ixon wire-format. + +Finally, Ix.IR can be converted back into Lean kernel values via Ix.DecompileM + +The Ix IR differs from the Lean kernel in the following ways: + +1. It excludes all `unsafe` constants, as these are not guaranteed to be + well-defined in the pure setting of a zero-knowledge prover +2. It excludes free variables and metavariables in expressions, all Ix IR terms +are closed. +3. It guarantees disambiguation of all names with de-bruijn index (int the case + of universe variables) and hash Addresses in the case of global constant + references. These Addresses are generated by hashing the anonymous Ixon + bytecode of the referenced constant, following dematerialization. The + separated metadata is also hashed and stored in-place in the Expr.const + reference. +4. Since inductive datatypes are content-addressed namelessly, only the type of + an inductive and the type and order of its constructors are relevant for + defining an Ix inductive. Consequently, the datatypes + + ```lean + inductive Boolean where + | false : Bool + | true : Bool + + inductive Loobean where + | true : Bool + | false : Bool + ``` + + compile to identical Ixon inductives, with the same Ix address (differing + only in their metadata) + + As a consequence, Ix will accept as valid the following Lean code: + + ```lean + def Boolean.and (x y: Boolean) : Boolean + | .true, .true => true + | _, _ => false + + def coerceLoobeanAsBoolean : Bool := Boolean.and Loobean.false Loobean.false + ``` + + We conjecture that this does not cause soundness issues in the Ix + typechecker, as one can treat this case as the Ix compiler inferring an + implicit coercion between isomorphic datatypes like so: + + ``` + def Loobean.toBoolean : Loobean -> Boolean + | .true => Boolean.false + | .false => Boolean.true + + def coerceLoobeanAsBoolean : Bool := + Boolean.and Loobean.false.toBoolean Loobean.false.toBoolean + ``` + + However, we have not rigorously demonstrated this yet, and therefore best + practice is to only pass environments to Ix which have passed Lean + typechecking to sanitize this case. +-/ + +/-- +Ix.Level universe levels are almost identical to Lean.Level, except that they +exclude metavariables and de-bruijn index variable parameters. +--/ +inductive Level + | zero + | succ : Level → Level + | max : Level → Level → Level + | imax : Level → Level → Level + | param: Lean.Name → Nat → Level + deriving Inhabited, Ord, BEq, Hashable, Repr + +/-- +Ix.Expr expressions are similar to Lean.Expr, except they exclude free variables +and metavariables, and annotate global constant references with Ix.Address +content-addresses +--/ +inductive Expr + | var (idx: Nat) + | sort (univ: Level) + | const (name: Lean.Name) (ref: Address) (meta: Address) (univs: List Level) + | rec_ (name: Lean.Name) (idx: Nat) (univs: List Level) + | app (func: Expr) (argm: Expr) + | lam (name: Lean.Name) (info: Lean.BinderInfo) (type: Expr) (body: Expr) + | pi (name: Lean.Name) (info: Lean.BinderInfo) (type: Expr) (body: Expr) + | letE (name: Lean.Name) (type: Expr) (value: Expr) (body: Expr) (nonDep: Bool) + | lit (lit: Lean.Literal) + | proj (typeName: Lean.Name) (typeCont: Address) (typeMeta: Address) (idx: Nat) (struct: Expr) + deriving Inhabited, Ord, BEq, Repr, Hashable + + +/-- +Ix.Quotient quotients are analogous to Lean.QuotVal +--/ +structure Quotient where + name: Lean.Name + levelParams : List Lean.Name + type : Expr + kind : Lean.QuotKind + deriving Ord, BEq, Hashable, Repr, Nonempty + +/-- +Ix.Axiom axioms are analogous to Lean.AxiomVal, differing only in not including +the `isUnsafe` parameter, as Ix constants are never unsafe +--/ +structure Axiom where + name: Lean.Name + levelParams : List Lean.Name + type : Expr + isUnsafe: Bool + deriving Ord, BEq, Hashable, Repr, Nonempty + +structure PreDefinition where + name: Lean.Name + levelParams : List Lean.Name + type : Lean.Expr + mode : DefMode + value : Lean.Expr + hints : Lean.ReducibilityHints + safety : Lean.DefinitionSafety + all : List Lean.Name + deriving BEq, Repr, Nonempty + +def mkPreDefinition (x: Lean.DefinitionVal) : PreDefinition := + ⟨x.name, x.levelParams, x.type, .definition, x.value, x.hints, x.safety, x.all⟩ + +def mkPreTheorem (x: Lean.TheoremVal) : PreDefinition := + ⟨x.name, x.levelParams, x.type, .theorem, x.value, .opaque, .safe, x.all⟩ + +def mkPreOpaque (x: Lean.OpaqueVal) : PreDefinition := + ⟨x.name, x.levelParams, x.type, .opaque, x.value, .opaque, + if x.isUnsafe then .unsafe else .safe, x.all⟩ + + +/-- +Ix.Definition definitions combine Lean.DefinitionVal, Lean.OpaqueVal and +Lean.TheoremVal into a single structure in order to enable content-addressing of +mutually recursive blocks. These cases are disambiguated via the Ix.DefMode +inductive. ReducibilityHints are preserved only as metadata, and are set to +`ReducibilityHints.opaque` and ignored if the DefMode is either .opaque or +.theorem. The `safety : Lean.DefinitionSafety` parameter from DefinitionVal is +replaced with a boolean for partial definitions, as Ix definitions are +restricted to exclude unsafe constants. +--/ +structure Definition where + name: Lean.Name + levelParams : List Lean.Name + type : Expr + mode: DefMode + value : Expr + hints : Lean.ReducibilityHints + safety: Lean.DefinitionSafety + all : List Lean.Name + deriving BEq, Ord, Hashable, Repr, Nonempty + +def mkTheorem + (name: Lean.Name) + (levelParams: List Lean.Name) + (type: Expr) + (value: Expr) + (all: List Lean.Name) + : Definition + := ⟨name, levelParams, type, .theorem, value, .opaque, .safe, all⟩ + +def mkOpaque + (name: Lean.Name) + (levelParams: List Lean.Name) + (type: Expr) + (value: Expr) + (all: List Lean.Name) + (isUnsafe: Bool) + : Definition + := ⟨name, levelParams, type, .opaque, value, .opaque, if isUnsafe then .unsafe else .safe, all⟩ + +/-- +Ix.Constructor inductive datatype constructors are analogous to +Lean.ConstructorVal. The primary difference is that Ix.Constructor only appears +within an Ix.Inductive, and is not directly present in the top level +environment. This is done to enable content-addressing of inductive datatypes. +Instead, Ix.ConstructorProj is used to project or access an inductive +constructor at the top level. Unlike other Ix constants, the `name` parameter is +represented here, but only as metadata to aid in decompilation. +--/ +structure Constructor where + name : Lean.Name + levelParams : List Lean.Name + type : Expr + cidx : Nat + numParams : Nat + numFields : Nat + isUnsafe: Bool + deriving BEq, Ord, Hashable, Repr, Nonempty + +/-- +Ix.RecursorRule is analogous to Lean.RecursorRule +--/ +structure RecursorRule where + ctor : Lean.Name + nfields : Nat + rhs : Expr + deriving BEq, Ord, Hashable, Repr, Nonempty + +/-- +Ix.Recursor represents inductive recursors and is analogous to Lean.RecursorVal. +However, like Ix.Constructor, recursors do not appear directly in the top-level +environment but are instead held directly within their corresponding Inductive. +Recursors are accessed in an environment using the `Ix.RecursorProj` projection +constant +--/ +structure Recursor where + name: Lean.Name + levelParams : List Lean.Name + type : Expr + numParams : Nat + numIndices : Nat + numMotives : Nat + numMinors : Nat + rules : List RecursorRule + k : Bool + isUnsafe: Bool + deriving BEq, Ord, Hashable, Repr, Nonempty + +/-- +Ix.PreInductive is used to capture a Lean.InductiveVal along with their +constructors and recursors, in order to perform structural sorting +--/ +structure PreInductive where + name: Lean.Name + levelParams : List Lean.Name + type : Lean.Expr + numParams : Nat + numIndices : Nat + all : List Lean.Name + ctors : List Lean.ConstructorVal + recrs : List Lean.RecursorVal + numNested: Nat + isRec : Bool + isReflexive : Bool + isUnsafe: Bool + deriving BEq, Repr, Nonempty + +/-- +Ix.Inductive represents inductive datatypes and is analogous to +Lean.InductiveVal. However, unlike in Lean, Ix.Inductive directly contains its +corresponding Constructors and Recursors in order to enable content-addressing. +--/ +structure Inductive where + name: Lean.Name + levelParams : List Lean.Name + type : Expr + numParams : Nat + numIndices : Nat + all : List Lean.Name + ctors : List Constructor + recrs : List Recursor + numNested: Nat + isRec : Bool + isReflexive : Bool + isUnsafe: Bool + deriving BEq, Ord, Hashable, Repr, Nonempty + + +structure InductiveProj where + /-- name of an inductive within a mutual inductive block --/ + name: Lean.Name + /-- content-address of a mutual inductive block --/ + blockCont : Address + /-- metadata content-address a mutual inductive block --/ + blockMeta : Address + /-- index of the specific inductive datatype within the block --/ + idx : Nat + deriving BEq, Ord, Hashable, Repr, Nonempty + +structure ConstructorProj where + /-- name of a specific constructor within an inductive --/ + name: Lean.Name + /-- content-address of a mutual inductive block --/ + blockCont : Address + /-- metadata content-address a mutual inductive block --/ + blockMeta : Address + /-- index of a specific inductive datatype within the block --/ + idx : Nat + /-- name of a specific inductive datatype within the block --/ + induct: Lean.Name + /-- index of a specific constructor within the inductive --/ + cidx : Nat + deriving BEq, Ord, Hashable, Repr, Nonempty + +structure RecursorProj where + /-- name of a specific recursor within the inductive --/ + name: Lean.Name + /-- content-address of a mutual inductive block --/ + blockCont : Address + /-- metadata content-address of a mutual inductive block --/ + blockMeta : Address + /-- index of a specific inductive datatype within the block --/ + idx : Nat + /-- name of a specific inductive datatype within the block --/ + induct: Lean.Name + /-- index of a specific recursor within the inductive --/ + ridx : Nat + deriving BEq, Ord, Hashable, Repr, Nonempty + +structure DefinitionProj where + name: Lean.Name + /-- content-address of a mutual definition block --/ + blockCont : Address + /-- metadata content-address of a mutual definition block --/ + blockMeta : Address + /-- index of a specific definition within the block --/ + idx : Nat + deriving BEq, Ord, Hashable, Repr, Nonempty + +structure MutualBlock where + defs : List (List Definition) + --all: List Lean.Name + deriving BEq, Ord, Hashable, Repr, Nonempty + +def MutualBlock.ctx (x: MutualBlock) : List (List Lean.Name) := + x.defs.map fun xs => xs.map fun x => x.name + +structure InductiveBlock where + inds : List (List Inductive) + --all: List Lean.Name + deriving BEq, Ord, Hashable, Repr, Nonempty, Inhabited + +def InductiveBlock.ctx (x: InductiveBlock) : List (List Lean.Name) := + x.inds.map fun xs => xs.map fun x => x.name + +inductive Const where + | «axiom» : Axiom → Const + | quotient : Quotient → Const + | «definition»: Definition → Const + -- projections of mutual blocks + | inductiveProj : InductiveProj → Const + | constructorProj : ConstructorProj → Const + | recursorProj : RecursorProj → Const + | definitionProj : DefinitionProj → Const + -- constants to represent mutual blocks + | «mutual» : MutualBlock → Const + | «inductive» : InductiveBlock → Const + deriving Ord, BEq, Inhabited, Repr, Nonempty + +def Const.isMutBlock : Const → Bool + | .mutual _ | .inductive _ => true + | _ => false + +namespace Level + +/-- +Reduces as a `max` applied to two values: `max a 0 = max 0 a = a` and +`max (succ a) (succ b) = succ (max a b)`. +It is assumed that `a` and `b` are already reduced +-/ +def reduceMax (a b : Level) : Level := + match a, b with + | .zero, _ => b + | _, .zero => a + | .succ a, .succ b => .succ (reduceMax a b) + | .param _ idx, .param _ idx' => if idx == idx' then a else .max a b + | _, _ => .max a b + +/-- +Reduces as an `imax` applied to two values. +It is assumed that `a` and `b` are already reduced +-/ +def reduceIMax (a b : Level) : Level := + match b with + -- IMax(a, b) will reduce to 0 if b == 0 + | .zero => .zero + -- IMax(a, b) will reduce as Max(a, b) if b == Succ(..) (impossible case) + | .succ _ => reduceMax a b + | .param _ idx => match a with + | .param _ idx' => if idx == idx' then a else .imax a b + | _ => .imax a b + -- Otherwise, IMax(a, b) is stuck, with a and b reduced + | _ => .imax a b + +/-- +Reduce, or simplify, the universe levels to a normal form. Notice that universe +levels with no free paramiables always reduce to a number, i.e., a sequence of +`succ`s followed by a `zero` +-/ +def reduce : Level → Level + | .succ u' => .succ (reduce u') + | .max a b => reduceMax (reduce a) (reduce b) + | .imax a b => + let b' := reduce b + match b' with + | .zero => .zero + | .succ _ => reduceMax (reduce a) b' + | _ => .imax (reduce a) b' + | u => u + +/-- +Instantiate a paramiable and reduce at the same time. Assumes an already reduced +`subst`. This function is only used in the comparison algorithm, and it doesn't +shift paramiables, because we want to instantiate a paramiable `param idx` with +`succ (param idx)`, so by shifting the paramiables we would transform `param (idx+1)` +into `param idx` which is not what we want +-/ +def instReduce (u : Level) (idx : Nat) (subst : Level) : Level := + match u with + | .succ u => .succ (instReduce u idx subst) + | .max a b => reduceMax (instReduce a idx subst) (instReduce b idx subst) + | .imax a b => + let a' := instReduce a idx subst + let b' := instReduce b idx subst + match b' with + | .zero => .zero + | .succ _ => reduceMax a' b' + | _ => .imax a' b' + | .param _ idx' => if idx' == idx then subst else u + | .zero => u + +/-- +Instantiate multiple paramiables at the same time and reduce. Assumes already +reduced `substs` +-/ +def instBulkReduce (substs : List Level) : Level → Level + | z@(.zero ..) => z + | .succ u => .succ (instBulkReduce substs u) + | .max a b => reduceMax (instBulkReduce substs a) (instBulkReduce substs b) + | .imax a b => + let b' := instBulkReduce substs b + match b' with + | .zero => .zero + | .succ _ => reduceMax (instBulkReduce substs a) b' + | _ => .imax (instBulkReduce substs a) b' + | .param n idx => match substs[idx]? with + | some u => u + -- This case should never happen if we're correctly enclosing every + -- expression with a big enough universe environment + | none => .param n (idx - substs.length) + +/-- +We say that two universe levels `a` and `b` are (semantically) equal, if they +are equal as numbers for all possible substitution of free paramiables to numbers. +Although writing an algorithm that follows this exact scheme is impossible, it +is possible to write one that is equivalent to such semantical equality. +Comparison algorithm `a <= b + diff`. Assumes `a` and `b` are already reduced +-/ +partial def leq (a b : Level) (diff : Int) : Bool := + if diff >= 0 && a == .zero then true + else match a, b with + | .zero, .zero => diff >= 0 + --! Succ cases + | .succ a, _ => leq a b (diff - 1) + | _, .succ b => leq a b (diff + 1) + | .param .., .zero => false + | .zero, .param .. => diff >= 0 + | .param _ x, .param _ y => x == y && diff >= 0 + --! IMax cases + -- The case `a = imax c d` has only three possibilities: + -- 1) d = param .. + -- 2) d = max .. + -- 3) d = imax .. + -- It can't be any otherway since we are assuming `a` is reduced, and thus `d` is reduced as well + | .imax _ (.param n idx), _ => + -- In the case for `param idx`, we need to compare two substitutions: + -- 1) idx <- zero + -- 2) idx <- succ (param idx) + -- In the first substitution, we know `a` becomes `zero` + leq .zero (instReduce b idx .zero) diff && + let succ := .succ (.param n idx) + leq (instReduce a idx succ) (instReduce b idx succ) diff + + | .imax c (.max e f), _ => + -- Here we use the relationship + -- imax c (max e f) = max (imax c e) (imax c f) + let new_max := reduceMax (reduceIMax c e) (reduceIMax c f) + leq new_max b diff + | .imax c (.imax e f), _ => + -- Here we use the relationship + -- imax c (imax e f) = max (imax c e) (imax e f) + let new_max := reduceMax (reduceIMax c e) (.imax e f) + leq new_max b diff + -- Analogous to previous case + | _, .imax _ (.param n idx) => + leq (instReduce a idx .zero) .zero diff && + let succ := .succ (.param n idx) + leq (instReduce a idx succ) (instReduce b idx succ) diff + | _, .imax c (.max e f) => + let new_max := reduceMax (reduceIMax c e) (reduceIMax c f) + leq a new_max diff + | _, .imax c (.imax e f) => + let new_max := reduceMax (reduceIMax c e) (.imax e f) + leq a new_max diff + --! Max cases + | .max c d, _ => leq c b diff && leq d b diff + | _, .max c d => leq a c diff || leq a d diff + | _, _ => false -- Impossible cases + +/-- The equality algorithm. Assumes `a` and `b` are already reduced -/ +def equalLevel (a b : Level) : Bool := + leq a b 0 && leq b a 0 + +/-- +Two lists of universes are considered equal iff they have the same length and +`Ix.equalLevel` returns `true` for all of their zip pairs +-/ +def equalLevels : List Level → List Level → Bool + | [], [] => true + | u::us, u'::us' => equalLevel u u' && equalLevels us us' + | _, _ => false + +/-- Faster equality for zero, assumes that the input is already reduced -/ +def isZero : Level → Bool + | .zero => true + -- all other cases are false since they are either `succ` or a reduced + -- expression with free paramiables, which are never semantically equal to zero + | _ => false + +end Ix.Level diff --git a/Ix/IR/Const.lean b/Ix/IR/Const.lean deleted file mode 100644 index ec31fa20..00000000 --- a/Ix/IR/Const.lean +++ /dev/null @@ -1,123 +0,0 @@ -import Ix.IR.Univ -import Ix.IR.Expr -import Ix.Address - -deriving instance BEq, Repr, Hashable, Ord for Lean.QuotKind - -namespace Ix - -structure Quotient where - lvls : Nat - type : Expr - kind : Lean.QuotKind - deriving Ord, BEq, Hashable, Repr - -structure Axiom where - lvls : Nat - type : Expr - deriving Ord, BEq, Hashable, Repr - -structure Theorem where - lvls : Nat - type : Expr - value : Expr - deriving Ord, BEq, Hashable, Repr - -structure Opaque where - lvls : Nat - type : Expr - value : Expr - deriving BEq, Ord, Hashable, Repr - -structure Definition where - lvls : Nat - type : Expr - value : Expr - part : Bool - deriving BEq, Ord, Hashable, Repr - -structure Constructor where - lvls : Nat - type : Expr - idx : Nat - params : Nat - fields : Nat - deriving BEq, Ord, Hashable, Repr - -structure RecursorRule where - fields : Nat - rhs : Expr - deriving BEq, Ord, Hashable, Repr - -structure Recursor where - lvls : Nat - type : Expr - params : Nat - indices : Nat - motives : Nat - minors : Nat - rules : List RecursorRule - isK : Bool - internal : Bool - deriving BEq, Ord, Hashable, Repr - -structure Inductive where - lvls : Nat - type : Expr - params : Nat - indices : Nat - ctors : List Constructor - recrs : List Recursor - recr : Bool - refl : Bool - struct : Bool - unit : Bool - deriving BEq, Ord, Hashable, Repr - -structure InductiveProj where - blockCont : Address - blockMeta : Address - idx : Nat - deriving BEq, Ord, Hashable, Repr - -structure ConstructorProj where - blockCont : Address - blockMeta : Address - idx : Nat - cidx : Nat - deriving BEq, Ord, Hashable, Repr - -structure RecursorProj where - blockCont : Address - blockMeta : Address - idx : Nat - ridx : Nat - deriving BEq, Ord, Hashable, Repr - -structure DefinitionProj where - blockCont : Address - blockMeta : Address - idx : Nat - deriving BEq, Ord, Hashable, Repr - -inductive Const where - | «axiom» : Axiom → Const - | «theorem» : Theorem → Const - | «opaque» : Opaque → Const - | «definition»: Definition → Const - | quotient : Quotient → Const - -- projections of mutual blocks - | inductiveProj : InductiveProj → Const - | constructorProj : ConstructorProj → Const - | recursorProj : RecursorProj → Const - | definitionProj : DefinitionProj → Const - -- constants to represent mutual blocks - | mutDefBlock : List Definition → Const - | mutIndBlock : List Inductive → Const - deriving Ord, BEq, Inhabited, Repr - -def Const.isMutType : Const → Bool - | .mutDefBlock _ | .mutIndBlock _ => true - | _ => false - -end Ix diff --git a/Ix/IR/Env.lean b/Ix/IR/Env.lean deleted file mode 100644 index 254bb317..00000000 --- a/Ix/IR/Env.lean +++ /dev/null @@ -1,19 +0,0 @@ -import Batteries.Data.RBMap -import Ix.IR.Univ -import Ix.IR.Expr -import Ix.IR.Const -import Ix.Ixon.Const -import Ix.Ixon.Metadata -import Ix.Common - -namespace Ix - -open Batteries (RBMap) -open Batteries (RBSet) - ---structure Env where --- names : RBMap Lean.Name Address compare --- store : RBMap Address Ixon.Const compare --- consts : RBMap Address (Batteries.RBMap Address Ix.Const compare) compare --- blocks : RBSet Address compare - diff --git a/Ix/IR/Expr.lean b/Ix/IR/Expr.lean deleted file mode 100644 index 8eb82ff6..00000000 --- a/Ix/IR/Expr.lean +++ /dev/null @@ -1,21 +0,0 @@ -import Ix.IR.Univ -import Ix.Address -import Ix.Common -import Lean.Expr - -namespace Ix - -inductive Expr - | var (idx: Nat) - | sort (univ: Univ) - | const (name: Lean.Name) (ref: Address) (meta: Address) (univs: List Univ) - | rec_ (idx: Nat) (univs: List Univ) - | app (func: Expr) (argm: Expr) - | lam (name: Lean.Name) (info: Lean.BinderInfo) (type: Expr) (body: Expr) - | pi (name: Lean.Name) (info: Lean.BinderInfo) (type: Expr) (body: Expr) - | letE (name: Lean.Name) (type: Expr) (value: Expr) (body: Expr) (nonDep: Bool) - | lit (lit: Lean.Literal) - | proj (typeName: Lean.Name) (typeCont: Address) (typeMeta: Address) (idx: Nat) (struct: Expr) - deriving Inhabited, Ord, BEq, Repr, Hashable - -end Ix diff --git a/Ix/IR/Univ.lean b/Ix/IR/Univ.lean deleted file mode 100644 index d92bb2d2..00000000 --- a/Ix/IR/Univ.lean +++ /dev/null @@ -1,179 +0,0 @@ -import Ix.Common - -namespace Ix - -inductive Univ - | zero - | succ : Univ → Univ - | max : Univ → Univ → Univ - | imax : Univ → Univ → Univ - | var : Lean.Name → Nat → Univ - deriving Inhabited, Ord, BEq, Hashable, Repr - -namespace Univ - -/-- -Reduces as a `max` applied to two values: `max a 0 = max 0 a = a` and -`max (succ a) (succ b) = succ (max a b)`. -It is assumed that `a` and `b` are already reduced --/ -def reduceMax (a b : Univ) : Univ := - match a, b with - | .zero, _ => b - | _, .zero => a - | .succ a, .succ b => .succ (reduceMax a b) - | .var _ idx, .var _ idx' => if idx == idx' then a else .max a b - | _, _ => .max a b - -/-- -Reduces as an `imax` applied to two values. -It is assumed that `a` and `b` are already reduced --/ -def reduceIMax (a b : Univ) : Univ := - match b with - -- IMax(a, b) will reduce to 0 if b == 0 - | .zero => .zero - -- IMax(a, b) will reduce as Max(a, b) if b == Succ(..) (impossible case) - | .succ _ => reduceMax a b - | .var _ idx => match a with - | .var _ idx' => if idx == idx' then a else .imax a b - | _ => .imax a b - -- Otherwise, IMax(a, b) is stuck, with a and b reduced - | _ => .imax a b - -/-- -Reduce, or simplify, the universe levels to a normal form. Notice that universe -levels with no free variables always reduce to a number, i.e., a sequence of -`succ`s followed by a `zero` --/ -def reduce : Univ → Univ - | .succ u' => .succ (reduce u') - | .max a b => reduceMax (reduce a) (reduce b) - | .imax a b => - let b' := reduce b - match b' with - | .zero => .zero - | .succ _ => reduceMax (reduce a) b' - | _ => .imax (reduce a) b' - | u => u - -/-- -Instantiate a variable and reduce at the same time. Assumes an already reduced -`subst`. This function is only used in the comparison algorithm, and it doesn't -shift variables, because we want to instantiate a variable `var idx` with -`succ (var idx)`, so by shifting the variables we would transform `var (idx+1)` -into `var idx` which is not what we want --/ -def instReduce (u : Univ) (idx : Nat) (subst : Univ) : Univ := - match u with - | .succ u => .succ (instReduce u idx subst) - | .max a b => reduceMax (instReduce a idx subst) (instReduce b idx subst) - | .imax a b => - let a' := instReduce a idx subst - let b' := instReduce b idx subst - match b' with - | .zero => .zero - | .succ _ => reduceMax a' b' - | _ => .imax a' b' - | .var _ idx' => if idx' == idx then subst else u - | .zero => u - -/-- -Instantiate multiple variables at the same time and reduce. Assumes already -reduced `substs` --/ -def instBulkReduce (substs : List Univ) : Univ → Univ - | z@(.zero ..) => z - | .succ u => .succ (instBulkReduce substs u) - | .max a b => reduceMax (instBulkReduce substs a) (instBulkReduce substs b) - | .imax a b => - let b' := instBulkReduce substs b - match b' with - | .zero => .zero - | .succ _ => reduceMax (instBulkReduce substs a) b' - | _ => .imax (instBulkReduce substs a) b' - | .var n idx => match substs[idx]? with - | some u => u - -- This case should never happen if we're correctly enclosing every - -- expression with a big enough universe environment - | none => .var n (idx - substs.length) - -/-- -We say that two universe levels `a` and `b` are (semantically) equal, if they -are equal as numbers for all possible substitution of free variables to numbers. -Although writing an algorithm that follows this exact scheme is impossible, it -is possible to write one that is equivalent to such semantical equality. -Comparison algorithm `a <= b + diff`. Assumes `a` and `b` are already reduced --/ -partial def leq (a b : Univ) (diff : Int) : Bool := - if diff >= 0 && a == .zero then true - else match a, b with - | .zero, .zero => diff >= 0 - --! Succ cases - | .succ a, _ => leq a b (diff - 1) - | _, .succ b => leq a b (diff + 1) - | .var .., .zero => false - | .zero, .var .. => diff >= 0 - | .var _ x, .var _ y => x == y && diff >= 0 - --! IMax cases - -- The case `a = imax c d` has only three possibilities: - -- 1) d = var .. - -- 2) d = max .. - -- 3) d = imax .. - -- It can't be any otherway since we are assuming `a` is reduced, and thus `d` is reduced as well - | .imax _ (.var n idx), _ => - -- In the case for `var idx`, we need to compare two substitutions: - -- 1) idx <- zero - -- 2) idx <- succ (var idx) - -- In the first substitution, we know `a` becomes `zero` - leq .zero (instReduce b idx .zero) diff && - let succ := .succ (.var n idx) - leq (instReduce a idx succ) (instReduce b idx succ) diff - - | .imax c (.max e f), _ => - -- Here we use the relationship - -- imax c (max e f) = max (imax c e) (imax c f) - let new_max := reduceMax (reduceIMax c e) (reduceIMax c f) - leq new_max b diff - | .imax c (.imax e f), _ => - -- Here we use the relationship - -- imax c (imax e f) = max (imax c e) (imax e f) - let new_max := reduceMax (reduceIMax c e) (.imax e f) - leq new_max b diff - -- Analogous to previous case - | _, .imax _ (.var n idx) => - leq (instReduce a idx .zero) .zero diff && - let succ := .succ (.var n idx) - leq (instReduce a idx succ) (instReduce b idx succ) diff - | _, .imax c (.max e f) => - let new_max := reduceMax (reduceIMax c e) (reduceIMax c f) - leq a new_max diff - | _, .imax c (.imax e f) => - let new_max := reduceMax (reduceIMax c e) (.imax e f) - leq a new_max diff - --! Max cases - | .max c d, _ => leq c b diff && leq d b diff - | _, .max c d => leq a c diff || leq a d diff - | _, _ => false -- Impossible cases - -/-- The equality algorithm. Assumes `a` and `b` are already reduced -/ -def equalUniv (a b : Univ) : Bool := - leq a b 0 && leq b a 0 - -/-- -Two lists of universes are considered equal iff they have the same length and -`Yatima.Univ.equalUniv` returns `true` for all of their zip pairs --/ -def equalUnivs : List Univ → List Univ → Bool - | [], [] => true - | u::us, u'::us' => equalUniv u u' && equalUnivs us us' - | _, _ => false - -/-- Faster equality for zero, assumes that the input is already reduced -/ -def isZero : Univ → Bool - | .zero => true - -- all other cases are false since they are either `succ` or a reduced - -- expression with free variables, which are never semantically equal to zero - | _ => false - -end Ix.Univ diff --git a/Ix/Ixon/Const.lean b/Ix/Ixon/Const.lean index 962f7ef3..9fb24f48 100644 --- a/Ix/Ixon/Const.lean +++ b/Ix/Ixon/Const.lean @@ -1,3 +1,4 @@ +import Ix.Common import Ix.Address import Ix.Prove import Lean.Declaration @@ -7,10 +8,6 @@ import Ix.Ixon.Expr namespace Ixon -deriving instance BEq for Lean.QuotKind - -deriving instance Repr for Lean.QuotKind - structure Quotient where lvls : Nat type : Expr @@ -18,217 +15,244 @@ structure Quotient where deriving BEq, Repr structure Axiom where - lvls : Nat - type : Expr - deriving BEq, Repr - -structure Theorem where - lvls : Nat - type : Expr - value : Expr - deriving BEq, Repr - -structure Opaque where - lvls : Nat - type : Expr - value : Expr + lvls : Nat + type : Expr + isUnsafe: Bool deriving BEq, Repr structure Definition where - lvls : Nat - type : Expr + lvls : Nat + type : Expr + mode : Ix.DefMode value : Expr - part : Bool + safety : Lean.DefinitionSafety deriving BEq, Repr structure Constructor where - lvls : Nat - type : Expr - idx : Nat + lvls : Nat + type : Expr + cidx : Nat params : Nat fields : Nat + isUnsafe: Bool deriving BEq, Repr structure RecursorRule where fields : Nat - rhs : Expr + rhs : Expr deriving BEq, Repr structure Recursor where - lvls : Nat - type : Expr - params : Nat - indices : Nat - motives : Nat - minors : Nat - rules : List RecursorRule - isK : Bool - internal : Bool + lvls : Nat + type : Expr + params : Nat + indices : Nat + motives : Nat + minors : Nat + rules : List RecursorRule + k : Bool + isUnsafe: Bool deriving BEq, Repr structure Inductive where - lvls : Nat - type : Expr - params : Nat + lvls : Nat + type : Expr + params : Nat indices : Nat - ctors : List Constructor - recrs : List Recursor - recr : Bool - refl : Bool - struct : Bool - unit : Bool + ctors : List Constructor + recrs : List Recursor + nested : Nat + recr : Bool + refl : Bool + isUnsafe: Bool deriving BEq, Repr structure InductiveProj where block : Address - idx : Nat + idx : Nat deriving BEq, Repr structure ConstructorProj where block : Address - idx : Nat - cidx : Nat + idx : Nat + cidx : Nat deriving BEq, Repr structure RecursorProj where block : Address - idx : Nat - ridx : Nat + idx : Nat + ridx : Nat deriving BEq, Repr structure DefinitionProj where block : Address - idx : Nat + idx : Nat deriving BEq, Repr structure Comm where - secret: Address - payload: Address + secret : Address + payload : Address deriving BEq, Repr inductive Const where -- 0xC0 - | axio : Axiom -> Const + | defn : Definition -> Const -- 0xC1 - | theo : Theorem -> Const + | axio : Axiom -> Const -- 0xC2 - | opaq : Opaque -> Const - -- 0xC3 - | defn : Definition -> Const - -- 0xC4 | quot : Quotient -> Const - -- 0xC5 + -- 0xC3 | ctorProj : ConstructorProj -> Const - -- 0xC6 + -- 0xC4 | recrProj : RecursorProj -> Const - -- 0xC7 + -- 0xC5 | indcProj : InductiveProj -> Const - -- 0xC8 + -- 0xC6 | defnProj : DefinitionProj -> Const - -- 0xC9 + -- 0xC7 | mutDef : List Definition -> Const - -- 0xCA + -- 0xC8 | mutInd : List Inductive -> Const - -- 0xCB + -- 0xC9 | meta : Metadata -> Const - -- 0xCC + -- 0xCA | proof : Proof -> Const - -- 0xCD + -- 0xCC | comm: Comm -> Const deriving BEq, Repr, Inhabited def putConst : Const → PutM -| .axio x => putUInt8 0xC0 *> putNatl x.lvls *> putExpr x.type -| .theo x => putUInt8 0xC1 *> putNatl x.lvls *> putExpr x.type *> putExpr x.value -| .opaq x => putUInt8 0xC2 *> putNatl x.lvls *> putExpr x.type *> putExpr x.value -| .defn x => putUInt8 0xC3 *> putDefn x -| .quot x => putUInt8 0xC4 *> putNatl x.lvls *> putExpr x.type *> putQuotKind x.kind -| .ctorProj x => putUInt8 0xC5 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.cidx -| .recrProj x => putUInt8 0xC6 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.ridx -| .indcProj x => putUInt8 0xC7 *> putBytes x.block.hash *> putNatl x.idx -| .defnProj x => putUInt8 0xC8 *> putBytes x.block.hash *> putNatl x.idx -| .mutDef xs => putUInt8 0xC9 *> putArray (putDefn <$> xs) -| .mutInd xs => putUInt8 0xCA *> putArray (putIndc <$> xs) -| .meta m => putUInt8 0xCB *> putMetadata m -| .proof p => putUInt8 0xCC *> putProof p -| .comm c => putUInt8 0xCD *> putComm c +| .defn x => putUInt8 0xC0 *> putDefn x +| .axio x => putUInt8 0xC1 *> putNatl x.lvls *> putExpr x.type *> putBool x.isUnsafe +| .quot x => putUInt8 0xC2 *> putNatl x.lvls *> putExpr x.type *> putQuotKind x.kind +| .ctorProj x => putUInt8 0xC3 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.cidx +| .recrProj x => putUInt8 0xC4 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.ridx +| .indcProj x => putUInt8 0xC5 *> putBytes x.block.hash *> putNatl x.idx +| .defnProj x => putUInt8 0xC6 *> putBytes x.block.hash *> putNatl x.idx +| .mutDef xs => putUInt8 0xC7 *> putArray putDefn xs +| .mutInd xs => putUInt8 0xC8 *> putArray putIndc xs +| .meta m => putUInt8 0xC9 *> putMetadata m +| .proof p => putUInt8 0xCA *> putProof p +| .comm c => putUInt8 0xCC *> putComm c where - putDefn (x: Definition) := - putNatl x.lvls *> putExpr x.type *> putExpr x.value *> putBool x.part + putDefn (x: Definition) := do + putNatl x.lvls + putExpr x.type + putDefMode x.mode + putExpr x.value + putDefinitionSafety x.safety putRecrRule (x: RecursorRule) : PutM := putNatl x.fields *> putExpr x.rhs - putCtor (x: Constructor) : PutM := - putNatl x.lvls *> putExpr x.type - *> putNatl x.idx *> putNatl x.params *> putNatl x.fields - putRecr (x: Recursor) : PutM := - putNatl x.lvls *> putExpr x.type - *> putNatl x.params *> putNatl x.indices *> putNatl x.motives - *> putNatl x.minors *> putArray (putRecrRule <$> x.rules) - *> putBools [x.isK, x.internal] - putIndc (x: Inductive) : PutM := - putNatl x.lvls *> putExpr x.type - *> putNatl x.params *> putNatl x.indices - *> putArray (putCtor <$> x.ctors) *> putArray (putRecr <$> x.recrs) - *> putBools [x.recr, x.refl, x.struct, x.unit] + putCtor (x: Constructor) : PutM := do + putNatl x.lvls + putExpr x.type + putNatl x.cidx + putNatl x.params + putNatl x.fields + putBool x.isUnsafe + putRecr (x: Recursor) : PutM := do + putNatl x.lvls + putExpr x.type + putNatl x.params + putNatl x.indices + putNatl x.motives + putNatl x.minors + putArray putRecrRule x.rules + putBool x.k + putBool x.isUnsafe + putIndc (x: Inductive) : PutM := do + putNatl x.lvls + putExpr x.type + putNatl x.params + putNatl x.indices + putArray putCtor x.ctors + putArray putRecr x.recrs + putNatl x.nested + putBools [x.recr, x.refl, x.isUnsafe] putProof (p: Proof) : PutM := match p.claim with - | .checks lvls type value => - putUInt8 0 - *> putBytes lvls.hash - *> putBytes type.hash - *> putBytes value.hash - *> putByteArray p.bin - | .evals lvls inp out type => - putUInt8 1 - *> putBytes lvls.hash - *> putBytes inp.hash - *> putBytes out.hash - *> putBytes type.hash - *> putByteArray p.bin + | .checks lvls type value => do + putUInt8 0 + putBytes lvls.hash + putBytes type.hash + putBytes value.hash + putByteArray p.bin + | .evals lvls inp out type => do + putUInt8 1 + putBytes lvls.hash + putBytes inp.hash + putBytes out.hash + putBytes type.hash + putByteArray p.bin putComm (c: Comm) : PutM := putBytes c.secret.hash *> putBytes c.payload.hash def getConst : GetM Const := do let tag ← getUInt8 match tag with - | 0xC0 => .axio <$> (.mk <$> getNatl <*> getExpr) - | 0xC1 => .theo <$> (.mk <$> getNatl <*> getExpr <*> getExpr) - | 0xC2 => .opaq <$> (.mk <$> getNatl <*> getExpr <*> getExpr) - | 0xC3 => .defn <$> getDefn - | 0xC4 => .quot <$> (.mk <$> getNatl <*> getExpr <*> getQuotKind) - | 0xC5 => .ctorProj <$> (.mk <$> getAddr <*> getNatl <*> getNatl) - | 0xC6 => .recrProj <$> (.mk <$> getAddr <*> getNatl <*> getNatl) - | 0xC7 => .indcProj <$> (.mk <$> getAddr <*> getNatl) - | 0xC8 => .defnProj <$> (.mk <$> getAddr <*> getNatl) - | 0xC9 => .mutDef <$> getArray getDefn - | 0xCA => .mutInd <$> getArray getIndc - | 0xCB => .meta <$> getMetadata - | 0xCC => .proof <$> getProof - | 0xCD => .comm <$> getComm + | 0xC0 => .defn <$> getDefn + | 0xC1 => .axio <$> (.mk <$> getNatl <*> getExpr <*> getBool) + | 0xC2 => .quot <$> (.mk <$> getNatl <*> getExpr <*> getQuotKind) + | 0xC3 => .ctorProj <$> (.mk <$> getAddr <*> getNatl <*> getNatl) + | 0xC4 => .recrProj <$> (.mk <$> getAddr <*> getNatl <*> getNatl) + | 0xC5 => .indcProj <$> (.mk <$> getAddr <*> getNatl) + | 0xC6 => .defnProj <$> (.mk <$> getAddr <*> getNatl) + | 0xC7 => .mutDef <$> getArray getDefn + | 0xC8 => .mutInd <$> getArray getIndc + | 0xC9 => .meta <$> getMetadata + | 0xCA => .proof <$> getProof + | 0xCC => .comm <$> getComm | e => throw s!"expected Const tag, got {e}" where - getDefn : GetM Definition := - .mk <$> getNatl <*> getExpr <*> getExpr <*> getBool - getCtor : GetM Constructor := - .mk <$> getNatl <*> getExpr <*> getNatl <*> getNatl <*> getNatl - getRecrRule : GetM RecursorRule := - RecursorRule.mk <$> getNatl <*> getExpr + getDefn : GetM Definition := do + let lvls <- getNatl + let type <- getExpr + let mode <- getDefMode + let value <- getExpr + let safety <- getDefinitionSafety + return ⟨lvls, type, mode, value, safety⟩ + getCtor : GetM Constructor := do + let lvls <- getNatl + let type <- getExpr + let cidx <- getNatl + let params <- getNatl + let fields <- getNatl + let safety <- getBool + return ⟨lvls, type, cidx, params, fields, safety⟩ + getRecrRule : GetM RecursorRule := RecursorRule.mk <$> getNatl <*> getExpr getRecr : GetM Recursor := do - let f ← Recursor.mk <$> getNatl <*> getExpr <*> getNatl - <*> getNatl <*> getNatl <*> getNatl <*> getArray getRecrRule - match ← getBools 2 with - | [x, y] => return f x y - | _ => throw s!"unreachable" + let lvls <- getNatl + let type <- getExpr + let params <- getNatl + let indices <- getNatl + let motives <- getNatl + let minors <- getNatl + let rules <- getArray getRecrRule + let k <- getBool + let safety <- getBool + return ⟨lvls, type, params, indices, motives, minors, rules, k, safety⟩ getIndc : GetM Inductive := do - let f ← Inductive.mk <$> getNatl <*> getExpr <*> getNatl <*> getNatl - <*> getArray getCtor <*> getArray getRecr - match ← getBools 4 with - | [w, x, y, z] => return f w x y z - | _ => throw s!"unreachable" + let lvls <- getNatl + let type <- getExpr + let params <- getNatl + let indices <- getNatl + let ctors <- getArray getCtor + let recrs <- getArray getRecr + let nested <- getNatl + let (recr, refl, safety) <- match ← getBools 3 with + | [x, y, z] => pure (x, y, z) + | _ => throw s!"unreachable" + return ⟨lvls, type, params, indices, ctors, recrs, nested, recr, refl, safety⟩ getAddr : GetM Address := .mk <$> getBytes 32 getProof : GetM Proof := do match (<- getUInt8) with - | 0 => .mk <$> (.checks <$> getAddr <*> getAddr <*> getAddr) <*> getByteArray - | 1 => .mk <$> (.evals <$> getAddr <*> getAddr <*> getAddr <*> getAddr) <*> getByteArray + | 0 => do + let claim <- .checks <$> getAddr <*> getAddr <*> getAddr + let proof <- getByteArray + return ⟨claim, proof⟩ + | 1 => do + let claim <- .evals <$> getAddr <*> getAddr <*> getAddr <*> getAddr + let proof <- getByteArray + return ⟨claim, proof⟩ | e => throw s!"expect proof variant tag, got {e}" getComm : GetM Comm := .mk <$> getAddr <*> getAddr diff --git a/Ix/Ixon/Expr.lean b/Ix/Ixon/Expr.lean index 8db1c7e8..9843f19d 100644 --- a/Ix/Ixon/Expr.lean +++ b/Ix/Ixon/Expr.lean @@ -133,11 +133,18 @@ instance : Serialize Expr where put := runPut ∘ putExpr get := runGet getExpr -def putArray (xs : List PutM) := do + +def putArray {A: Type} (putM : A -> PutM) (xs : List A) : PutM := do + putExprTag 0xB (UInt64.ofNat xs.length) + List.forM xs putM + +-- useful for arrays of non-uniform type, such as encoding tuples, although that +-- requires a custom getArray equivalent +def putArray' (xs : List PutM) : PutM := do putExprTag 0xB (UInt64.ofNat xs.length) List.forM xs id -def putByteArray (x: ByteArray) := do +def putByteArray (x: ByteArray) : PutM := do putExprTag 0xB (UInt64.ofNat x.size) x.toList.forM putUInt8 @@ -158,8 +165,8 @@ def getByteArray : GetM ByteArray := do def putOption (putM: A -> PutM): Option A → PutM -| .none => putArray [] -| .some x => putArray [putM x] +| .none => putArray putM [] +| .some x => putArray putM [x] def getOption [Repr A] (getM: GetM A): GetM (Option A) := do match ← getArray getM with diff --git a/Ix/Ixon/Metadata.lean b/Ix/Ixon/Metadata.lean index 822b98cb..b917cb1e 100644 --- a/Ix/Ixon/Metadata.lean +++ b/Ix/Ixon/Metadata.lean @@ -6,14 +6,17 @@ import Batteries.Data.RBMap namespace Ixon -structure MetaNode where - name : Option Lean.Name - info : Option Lean.BinderInfo - link : Option Address - deriving BEq, Repr, Ord +inductive Metadatum where +| name : Lean.Name -> Metadatum +| info : Lean.BinderInfo -> Metadatum +| link : Address -> Metadatum +| hints : Lean.ReducibilityHints -> Metadatum +| all : List Lean.Name -> Metadatum +| mutCtx : List (List Lean.Name) -> Metadatum +deriving BEq, Repr, Ord, Inhabited structure Metadata where - map: Batteries.RBMap Nat MetaNode compare + map: Batteries.RBMap Nat (List Metadatum) compare deriving BEq, Repr inductive NamePart where @@ -41,36 +44,37 @@ def getNamePart : GetM NamePart := do | .natl s => return (.num s) | e => throw s!"expected NamePart from .strl or .natl, got {repr e}" -def putName (n: Lean.Name): PutM := putArray (putNamePart <$> (nameToParts n)) +def putName (n: Lean.Name): PutM := putArray putNamePart (nameToParts n) def getName: GetM Lean.Name := nameFromParts <$> getArray getNamePart -def putMetaNode: MetaNode → PutM -| ⟨n, b, l⟩ => putArray - [ putOption putName n, - putOption putBinderInfo b, - putOption (putBytes ·.hash) l - ] +def putMetadatum : Metadatum → PutM +| .name n => putUInt8 0 *> putName n +| .info i => putUInt8 1 *> putBinderInfo i +| .link l => putUInt8 2 *> putBytes l.hash +| .hints h => putUInt8 3 *> putReducibilityHints h +| .all ns => putUInt8 4 *> putArray putName ns +| .mutCtx ctx => putUInt8 5 *> (putArray (putArray putName) ctx) -def getMetaNode: GetM MetaNode := do - let tagByte ← getUInt8 - let tag := UInt8.shiftRight tagByte 4 - let small := UInt8.land tagByte 0b111 - let isLarge := (UInt8.land tagByte 0b1000 != 0) - match tag with - | 0xB => do - let _ ← UInt64.toNat <$> getExprTag isLarge small - let n ← getOption getName - let b ← getOption getBinderInfo - let l ← getOption (Address.mk <$> getBytes 32) - return MetaNode.mk n b l - | e => throw s!"expected metanode Array with tag 0xB, got {e}" +def getMetadatum : GetM Metadatum := do + match (<- getUInt8) with + | 0 => .name <$> getName + | 1 => .info <$> getBinderInfo + | 2 => .link <$> (.mk <$> getBytes 32) + | 3 => .hints <$> getReducibilityHints + | 4 => .all <$> getArray getName + | 5 => .mutCtx <$> getArray (getArray getName) + | e => throw s!"expected Metadatum encoding between 0 and 4, got {e}" -def putMetadata (m: Metadata) : PutM := putArray (putEntry <$> m.map.toList) +def putMetadata (m: Metadata) : PutM := putArray putEntry m.map.toList where - putEntry e := putNatl e.fst *> putMetaNode e.snd + putEntry e := putNatl e.fst *> putArray putMetadatum e.snd def getMetadata : GetM Metadata := do - let xs <- getArray (Prod.mk <$> getNatl <*> getMetaNode) + let xs <- getArray (Prod.mk <$> getNatl <*> getArray getMetadatum) return Metadata.mk (Batteries.RBMap.ofList xs compare) +instance : Serialize Metadatum where + put := runPut ∘ putMetadatum + get := runGet getMetadatum + end Ixon diff --git a/Ix/Ixon/Serialize.lean b/Ix/Ixon/Serialize.lean index 13acf07e..598fb83f 100644 --- a/Ix/Ixon/Serialize.lean +++ b/Ix/Ixon/Serialize.lean @@ -1,3 +1,4 @@ +import Ix.Common import Lean.Declaration import Ix.Address @@ -26,6 +27,12 @@ def runPut (putm: PutM) : ByteArray := def putUInt8 (x: UInt8) : PutM := StateT.modifyGet (fun s => ((), s.push x)) +def putUInt32LE (x: UInt32) : PutM := do + List.forM (List.range 4) fun i => + let b := UInt32.toUInt8 (x >>> (i.toUInt32 * 8)) + putUInt8 b + pure () + def putUInt64LE (x: UInt64) : PutM := do List.forM (List.range 8) fun i => let b := UInt64.toUInt8 (x >>> (i.toUInt64 * 8)) @@ -44,6 +51,13 @@ def getUInt8 : GetM UInt8 := do else throw "EOF" +def getUInt32LE : GetM UInt32 := do + let mut x : UInt32 := 0 + for i in List.range 4 do + let b ← getUInt8 + x := x + (UInt8.toUInt32 b) <<< ((UInt32.ofNat i) * 8) + pure x + def getUInt64LE : GetM UInt64 := do let mut x : UInt64 := 0 for i in List.range 8 do @@ -144,6 +158,18 @@ def getQuotKind : GetM Lean.QuotKind := do | 3 => return .ind | e => throw s!"expected QuotKind encoding between 0 and 3, got {e}" +def putDefMode : Ix.DefMode → PutM +| .«definition» => putUInt8 0 +| .«opaque» => putUInt8 1 +| .«theorem» => putUInt8 2 + +def getDefMode : GetM Ix.DefMode := do + match (← getUInt8) with + | 0 => return .definition + | 1 => return .opaque + | 2 => return .theorem + | e => throw s!"expected DefMode encoding between 0 and 3, got {e}" + def putBinderInfo : Lean.BinderInfo → PutM | .default => putUInt8 0 | .implicit => putUInt8 1 @@ -156,6 +182,30 @@ def getBinderInfo : GetM Lean.BinderInfo := do | 1 => return .implicit | 2 => return .strictImplicit | 3 => return .instImplicit - | e => throw s!"expected QuotKind encoding between 0 and 3, got {e}" + | e => throw s!"expected BinderInfo encoding between 0 and 3, got {e}" + +def putReducibilityHints : Lean.ReducibilityHints → PutM +| .«opaque» => putUInt8 0 +| .«abbrev» => putUInt8 1 +| .regular x => putUInt8 2 *> putUInt32LE x + +def getReducibilityHints : GetM Lean.ReducibilityHints := do + match (← getUInt8) with + | 0 => return .«opaque» + | 1 => return .«abbrev» + | 2 => .regular <$> getUInt32LE + | e => throw s!"expected ReducibilityHints encoding between 0 and 2, got {e}" + +def putDefinitionSafety : Lean.DefinitionSafety → PutM +| .«unsafe» => putUInt8 0 +| .«safe» => putUInt8 1 +| .«partial» => putUInt8 2 + +def getDefinitionSafety : GetM Lean.DefinitionSafety := do + match (← getUInt8) with + | 0 => return .«unsafe» + | 1 => return .«safe» + | 2 => return .«partial» + | e => throw s!"expected DefinitionSafety encoding between 0 and 2, got {e}" end Ixon diff --git a/Ix/Meta.lean b/Ix/Meta.lean index d439e56f..2bfb1a7b 100644 --- a/Ix/Meta.lean +++ b/Ix/Meta.lean @@ -39,7 +39,7 @@ macro "get_env!" : term => `(getFileEnv this_file!) def computeIxAddress (env: Lean.Environment) (const : ConstantInfo) : IO Address := do - let ((a, _), _) <- Ix.Compile.compileConstIO env const + let ((a, _), _) <- (Ix.Compile.compileConst const).runIO env return a def runCore (f : CoreM α) (env : Environment) : IO α := diff --git a/Ix/Store.lean b/Ix/Store.lean index 9f5da80c..75da1dc4 100644 --- a/Ix/Store.lean +++ b/Ix/Store.lean @@ -48,6 +48,14 @@ def writeConst (x: Ixon.Const) : StoreIO Address := do let _ <- IO.toEIO .ioError (IO.FS.writeBinFile path bytes) return addr +-- unsafe, can corrupt store if called with bad address +def forceWriteConst (addr: Address) (x: Ixon.Const) : StoreIO Address := do + let bytes := Ixon.Serialize.put x + let store ← storeDir + let path := store / hexOfBytes addr.hash + let _ <- IO.toEIO .ioError (IO.FS.writeBinFile path bytes) + return addr + def readConst (a: Address) : StoreIO Ixon.Const := do let store ← storeDir let path := store / hexOfBytes a.hash diff --git a/Ix/TransportM.lean b/Ix/TransportM.lean index aebcf6c1..d9f48336 100644 --- a/Ix/TransportM.lean +++ b/Ix/TransportM.lean @@ -1,8 +1,6 @@ -import Ix.IR.Univ +import Ix.IR import Ix.Ixon.Univ -import Ix.IR.Expr import Ix.Ixon.Expr -import Ix.IR.Const import Ix.Ixon.Const import Ix.Common import Ix.Address @@ -22,21 +20,25 @@ def emptyDematState : DematState := { idx := 0, meta := { map := Batteries.RBMap.empty }} inductive TransportError - | natTooBig (idx: Nat) (x: Nat) - | unknownIndex (idx: Nat) (m: Ixon.Metadata) - | unexpectedNode (idx: Nat) (m: Ixon.Metadata) - | rawMetadata (m: Ixon.Metadata) - | rawProof (m: Proof) - | rawComm (m: Ixon.Comm) - deriving BEq, Repr +| natTooBig (idx: Nat) (x: Nat) +| unknownIndex (idx: Nat) (m: Ixon.Metadata) +| unexpectedNode (idx: Nat) (m: Ixon.Metadata) +| rawMetadata (m: Ixon.Metadata) +| expectedMetadata (m: Ixon.Const) +| rawProof (m: Proof) +| rawComm (m: Ixon.Comm) +| emptyEquivalenceClass +deriving BEq, Repr instance : ToString TransportError where toString | .natTooBig idx x => s!"At index {idx}, natural number {x} too big to fit in UInt64" | .unknownIndex idx x => s!"Unknown index {idx} with metadata {repr x}" | .unexpectedNode idx x => s!"Unexpected node at {idx} with metadata {repr x}" | .rawMetadata x => s!"Can't rematerialize raw metadata {repr x}" +| .expectedMetadata x => s!"Expected metadata, got {repr x}" | .rawProof x => s!"Can't rematerialize raw proof {repr x}" | .rawComm x => s!"Can't rematerialize raw commitment {repr x}" +| .emptyEquivalenceClass => s!"empty equivalence class, should be unreachable" abbrev DematM := EStateM TransportError DematState @@ -50,11 +52,12 @@ structure RematCtx where abbrev RematM := ReaderT RematCtx (EStateM TransportError RematState) -def countSucc : Ix.Univ -> Nat -> (Nat × Ix.Univ) + +def countSucc : Ix.Level -> Nat -> (Nat × Ix.Level) | .succ x, i => countSucc x (.succ i) | n, i => (i, n) -def unrollSucc : Nat -> Ix.Univ -> Ix.Univ +def unrollSucc : Nat -> Ix.Level -> Ix.Level | 0, x => x | .succ i, x => unrollSucc i (.succ x) @@ -70,24 +73,34 @@ def dematIncrN (x: Nat) : DematM Nat := do def dematIncr : DematM Nat := dematIncrN 1 -def dematMeta (node: Ixon.MetaNode): DematM Unit := do +def dematMeta (node: List Ixon.Metadatum): DematM Unit := do let n <- (·.idx) <$> get modify fun stt => { stt with meta := { stt.meta with map := stt.meta.map.insert n node } } -partial def dematUniv : Ix.Univ -> DematM Ixon.Univ +partial def dematUniv : Ix.Level -> DematM Ixon.Univ | .zero => dematIncr *> return .const 0 | .succ x => match countSucc x 1 with | (i, .zero) => dematIncrN (i + 1) *> .const <$> dematNat i | (i, x) => dematIncrN (i + 1) *> .add <$> dematNat i <*> dematUniv x | .max x y => dematIncr *> .max <$> dematUniv x <*> dematUniv y | .imax x y => dematIncr *> .imax <$> dematUniv x <*> dematUniv y -| .var n i => do +| .param n i => do let _ <- dematIncr - dematMeta { name := .some n, info := .none, link := .none } + dematMeta [.name n] .var <$> dematNat i +partial def dematLevels (lvls: List Lean.Name): DematM Nat := + go 0 lvls + where + go (acc: Nat) : List Lean.Name -> DematM Nat + | n::ns => do + let _ <- dematIncr + dematMeta [.name n] + go (acc+1) ns + | [] => pure acc + def rematIncrN (x: Nat) : RematM Nat := do let n <- (·.idx) <$> get modify fun stt => { stt with idx := n + x } @@ -95,25 +108,35 @@ def rematIncrN (x: Nat) : RematM Nat := do def rematIncr : RematM Nat := rematIncrN 1 -def rematMeta : RematM Ixon.MetaNode := do +def rematMeta : RematM (List Ixon.Metadatum) := do let n <- (·.idx) <$> get let m <- (·.meta) <$> read match m.map.find? n with | .some n => return n | .none => throw (.unknownIndex n m) -def rematThrowUnexpectedNode : RematM α := do +def rematThrowUnexpected : RematM α := do let n <- (·.idx) <$> get let m <- (·.meta) <$> read throw (.unexpectedNode n m) +partial def rematLevels (lvls: Nat): RematM (List Lean.Name) := do + go [] lvls + where + go (acc: List Lean.Name): Nat -> RematM (List Lean.Name) + | 0 => pure acc.reverse + | i => do + let _ <- rematIncr + match (<- rematMeta) with + | [.name n] => go (n::acc) (i - 1) + | _ => rematThrowUnexpected + def rematBindMeta : RematM (Lean.Name × Lean.BinderInfo) := do - let n <- rematMeta - match n.name, n.info with - | .some n, some i => return (n, i) - | _, _ => rematThrowUnexpectedNode + match (<- rematMeta) with + | [.name n, .info i] => return (n, i) + | _ => rematThrowUnexpected -def rematUniv : Ixon.Univ -> RematM Ix.Univ +def rematUniv : Ixon.Univ -> RematM Ix.Level | .const i => do let i' := UInt64.toNat i rematIncrN (i' + 1) *> return (unrollSucc i') .zero @@ -123,33 +146,35 @@ def rematUniv : Ixon.Univ -> RematM Ix.Univ | .max x y => rematIncr *> .max <$> rematUniv x <*> rematUniv y | .imax x y => rematIncr *> .imax <$> rematUniv x <*> rematUniv y | .var x => do - let k <- rematIncr - let mn <- rematMeta - match mn.name with - | .some name => return .var name (UInt64.toNat x) - | .none => read >>= fun ctx => throw (.unexpectedNode k ctx.meta) + let _ <- rematIncr + match (<- rematMeta) with + | [.name name] => return .param name (UInt64.toNat x) + | _ => rematThrowUnexpected partial def dematExpr : Ix.Expr -> DematM Ixon.Expr | .var i => dematIncr *> .vari <$> dematNat i | .sort u => dematIncr *> .sort <$> dematUniv u | .const n r m us => do let _ <- dematIncr - dematMeta { name := .some n, info := .none, link := .some m } + dematMeta [.name n, .link m ] .cnst r <$> (us.mapM dematUniv) -| .rec_ i us => dematIncr *> .rec_ <$> dematNat i <*> (us.mapM dematUniv) +| .rec_ n i us => do + let _ <- dematIncr + dematMeta [.name n] + .rec_ <$> dematNat i <*> (us.mapM dematUniv) | .app f a => apps f a [] | .lam n i t b => lams (.lam n i t b) [] | .pi n i t b => alls (.pi n i t b) [] | .letE n t v b nD => do let _ <- dematIncr - dematMeta { name := .some n, info := .none, link := none } + dematMeta [.name n] .let_ nD <$> dematExpr t <*> dematExpr v <*> dematExpr b | .lit l => dematIncr *> match l with | .strVal s => return .strl s | .natVal n => return .natl n | .proj n t tM i s => do let _ <- dematIncr - dematMeta { name := .some n, info := .none, link := .some tM } + dematMeta [.name n, .link tM ] .proj t <$> dematNat i <*> dematExpr s where apps : Ix.Expr -> Ix.Expr -> List Ix.Expr -> DematM Ixon.Expr @@ -160,14 +185,14 @@ partial def dematExpr : Ix.Expr -> DematM Ixon.Expr lams : Ix.Expr -> List Ixon.Expr -> DematM Ixon.Expr | .lam n i t b, ts => do let _ <- dematIncr - dematMeta { name := .some n, info := .some i, link := .none} + dematMeta [.name n, .info i] let t' <- dematExpr t lams b (t'::ts) | x, ts => .lams ts.reverse <$> dematExpr x alls : Ix.Expr -> List Ixon.Expr -> DematM Ixon.Expr | .pi n i t b, ts => do let _ <- dematIncr - dematMeta { name := .some n, info := .some i, link := .none} + dematMeta [.name n, .info i] let t' <- dematExpr t alls b (t'::ts) | x, ts => .alls ts.reverse <$> dematExpr x @@ -179,10 +204,16 @@ partial def rematExpr : Ixon.Expr -> RematM Ix.Expr let _ <- rematIncr let node <- rematMeta let us' <- us.mapM rematUniv - match node.name, node.link with - | .some name, .some link => return (.const name adr link us') - | _, _ => rematThrowUnexpectedNode -| .rec_ i us => rematIncr *> .rec_ i.toNat <$> us.mapM rematUniv + match node with + | [.name name, .link link] => return (.const name adr link us') + | _ => rematThrowUnexpected +| .rec_ i us => do + let _ <- rematIncr + let node <- rematMeta + let us' <- us.mapM rematUniv + match node with + | [.name name] => return (.rec_ name i.toNat us') + | _ => rematThrowUnexpected | .apps f a as => do let as' <- as.reverse.mapM (fun e => rematIncr *> rematExpr e) let f' <- rematExpr f @@ -200,61 +231,95 @@ partial def rematExpr : Ixon.Expr -> RematM Ix.Expr return ts'.foldr (fun (m, t) b => Expr.pi m.fst m.snd t b) b' | .let_ nD t d b => do let _ <- rematIncr - let m <- (·.name) <$> rematMeta - let name <- match m with - | .some m => pure m - | _ => rematThrowUnexpectedNode + let node <- rematMeta + let name <- match node with + | [.name n] => pure n + | _ => rematThrowUnexpected .letE name <$> rematExpr t <*> rematExpr d <*> rematExpr b <*> pure nD | .proj t i s => do let _ <- rematIncr - let m <- rematMeta - let (name, link) <- match m.name, m.link with - | .some n, .some l => pure (n, l) - | _, _ => rematThrowUnexpectedNode + let node <- rematMeta + let (name, link) <- match node with + | [.name n, .link l] => pure (n, l) + | _ => rematThrowUnexpected .proj name t link i.toNat <$> rematExpr s | .strl s => rematIncr *> return .lit (.strVal s) | .natl n => rematIncr *> return .lit (.natVal n) partial def dematConst : Ix.Const -> DematM Ixon.Const -| .«axiom» x => .axio <$> (.mk x.lvls <$> dematExpr x.type) -| .«theorem» x => .theo <$> (.mk x.lvls <$> dematExpr x.type <*> dematExpr x.value) -| .«opaque» x => - .opaq <$> (.mk x.lvls <$> dematExpr x.type <*> dematExpr x.value) +| .«axiom» x => do + dematMeta [.name x.name] + let lvls <- dematLevels x.levelParams + let type <- dematExpr x.type + return .axio (.mk lvls type x.isUnsafe) | .«definition» x => .defn <$> dematDefn x -| .quotient x => .quot <$> - (.mk x.lvls <$> dematExpr x.type <*> pure x.kind) +| .quotient x => do + dematMeta [.name x.name] + let lvls <- dematLevels x.levelParams + let type <- dematExpr x.type + return .quot (.mk lvls type x.kind) | .inductiveProj x => do - dematMeta { name := .none, info := .none, link := .some x.blockMeta} + dematMeta [.name x.name, .link x.blockMeta] return .indcProj (.mk x.blockCont x.idx) | .constructorProj x => do - dematMeta { name := .none, info := .none, link := .some x.blockMeta} + dematMeta [.name x.name, .link x.blockMeta, .name x.induct] return .ctorProj (.mk x.blockCont x.idx x.cidx) | .recursorProj x => do - dematMeta { name := .none, info := .none, link := .some x.blockMeta} + dematMeta [.name x.name, .link x.blockMeta, .name x.induct] return .recrProj (.mk x.blockCont x.idx x.ridx) | .definitionProj x => do - dematMeta { name := .none, info := .none, link := .some x.blockMeta} + dematMeta [.name x.name, .link x.blockMeta] return .defnProj (.mk x.blockCont x.idx) -| .mutDefBlock xs => .mutDef <$> (xs.mapM dematDefn) -| .mutIndBlock xs => .mutInd <$> (xs.mapM dematInd) +| .mutual x => do + dematMeta [.mutCtx x.ctx] + let defs <- x.defs.mapM fun ds => ds.mapM dematDefn + let ds <- defs.mapM fun d => match d.head? with + | .some a => pure a + | .none => throw .emptyEquivalenceClass + return .mutDef ds +| .inductive x => do + dematMeta [.mutCtx x.ctx] + let inds <- x.inds.mapM fun is => is.mapM dematIndc + let is <- inds.mapM fun i => match i.head? with + | .some a => pure a + | .none => throw .emptyEquivalenceClass + return .mutInd is where - dematDefn : Ix.Definition -> DematM Ixon.Definition - | x => .mk x.lvls <$> dematExpr x.type <*> dematExpr x.value <*> pure x.part - dematCtor : Ix.Constructor -> DematM Ixon.Constructor - | x => do - let t <- dematExpr x.type - return .mk x.lvls t x.idx x.params x.fields - dematRecr : Ix.Recursor -> DematM Ixon.Recursor - | x => do + dematDefn (x: Ix.Definition): DematM Ixon.Definition := do + let _ <- dematIncr + dematMeta [.name x.name, .hints x.hints, .all x.all] + let lvls <- dematLevels x.levelParams + let type <- dematExpr x.type + let value <- dematExpr x.value + return .mk lvls type x.mode value x.safety + dematCtor (x: Ix.Constructor): DematM Ixon.Constructor := do + let _ <- dematIncr + dematMeta [.name x.name] + let lvls <- dematLevels x.levelParams let t <- dematExpr x.type - let rrs <- x.rules.mapM (fun rr => .mk rr.fields <$> dematExpr rr.rhs) - return .mk x.lvls t x.params x.indices x.motives x.minors rrs x.isK x.internal - dematInd : Ix.Inductive -> DematM Ixon.Inductive - | x => do + return .mk lvls t x.cidx x.numParams x.numFields x.isUnsafe + dematRecrRule (x: Ix.RecursorRule): DematM Ixon.RecursorRule := do + let _ <- dematIncr + dematMeta [.name x.ctor] + let rhs <- dematExpr x.rhs + return ⟨x.nfields, rhs⟩ + dematRecr (x: Ix.Recursor): DematM Ixon.Recursor := do + let _ <- dematIncr + dematMeta [.name x.name] + let lvls <- dematLevels x.levelParams let t <- dematExpr x.type - let cs <- x.ctors.mapM dematCtor - let rs <- x.recrs.mapM dematRecr - return .mk x.lvls t x.params x.indices cs rs x.recr x.refl x.struct x.unit + let rrs <- x.rules.mapM dematRecrRule + return ⟨lvls, t, x.numParams, x.numIndices, x.numMotives, x.numMinors, + rrs, x.k, x.isUnsafe⟩ + dematIndc (x: Ix.Inductive): DematM Ixon.Inductive := do + let _ <- dematIncr + dematMeta [.name x.name, .all x.all] + let lvls <- dematLevels x.levelParams + let type <- dematExpr x.type + let ctors <- x.ctors.mapM dematCtor + let recrs <- x.recrs.mapM dematRecr + return ⟨lvls, type, x.numParams, x.numIndices, ctors, recrs, x.numNested, + x.isRec, x.isReflexive, x.isUnsafe⟩ def constToIxon (x: Ix.Const) : Except TransportError (Ixon.Const × Ixon.Const) := match EStateM.run (dematConst x) emptyDematState with @@ -270,46 +335,121 @@ def constAddress (x: Ix.Const) : Except TransportError Address := do return Address.blake3 bs partial def rematConst : Ixon.Const -> RematM Ix.Const -| .axio x => .«axiom» <$> (.mk x.lvls <$> rematExpr x.type) -| .theo x => .«theorem» <$> (.mk x.lvls <$> rematExpr x.type <*> rematExpr x.value) -| .opaq x => .«opaque» <$> (.mk x.lvls <$> rematExpr x.type <*> rematExpr x.value) | .defn x => .«definition» <$> rematDefn x -| .quot x => .quotient <$> (.mk x.lvls <$> rematExpr x.type <*> pure x.kind) +| .axio x => do + let name <- match (<- rematMeta) with + | [.name x] => pure x + | _ => rematThrowUnexpected + let lvls <- rematLevels x.lvls + let type <- rematExpr x.type + return .«axiom» ⟨name, lvls, type, x.isUnsafe⟩ +| .quot x => do + let name <- match (<- rematMeta) with + | [.name x] => pure x + | _ => rematThrowUnexpected + let lvls <- rematLevels x.lvls + let type <- rematExpr x.type + return .quotient ⟨name, lvls, type, x.kind⟩ | .indcProj x => do - let link <- rematMeta >>= fun m => m.link.elim rematThrowUnexpectedNode pure - return .inductiveProj (.mk x.block link x.idx) + let (name, link) <- match (<- rematMeta) with + | [.name n, .link x] => pure (n, x) + | _ => rematThrowUnexpected + return .inductiveProj ⟨name, x.block, link, x.idx⟩ | .ctorProj x => do - let link <- rematMeta >>= fun m => m.link.elim rematThrowUnexpectedNode pure - return .constructorProj (.mk x.block link x.idx x.cidx) + let (name, link, induct) <- match (<- rematMeta) with + | [.name n, .link x, .name i] => pure (n, x, i) + | _ => rematThrowUnexpected + return .constructorProj ⟨name, x.block, link, x.idx, induct, x.cidx⟩ | .recrProj x => do - let link <- rematMeta >>= fun m => m.link.elim rematThrowUnexpectedNode pure - return .recursorProj (.mk x.block link x.idx x.ridx) + let (name, link, induct) <- match (<- rematMeta) with + | [.name n, .link x, .name i] => pure (n, x, i) + | _ => rematThrowUnexpected + return .recursorProj ⟨name, x.block, link, x.idx, induct, x.ridx⟩ | .defnProj x => do - let link <- rematMeta >>= fun m => m.link.elim rematThrowUnexpectedNode pure - return .definitionProj (.mk x.block link x.idx) -| .mutDef xs => .mutDefBlock <$> (xs.mapM rematDefn) -| .mutInd xs => .mutIndBlock <$> (xs.mapM rematInd) + let (name, link) <- match (<- rematMeta) with + | [.name n, .link x] => pure (n, x) + | _ => rematThrowUnexpected + return .definitionProj ⟨name, x.block, link, x.idx⟩ +| .mutDef xs => do + let ctx <- match (<- rematMeta) with + | [.mutCtx x] => pure x + | _ => rematThrowUnexpected + let mut defs := #[] + for (x, ns) in List.zip xs ctx do + let mut ds := #[] + for _ in ns do + let d <- rematDefn x + ds := ds.push d + defs := defs.push ds.toList + return .mutual ⟨defs.toList⟩ +| .mutInd xs => do + let ctx <- match (<- rematMeta) with + | [.mutCtx x] => pure x + | _ => rematThrowUnexpected + let mut inds := #[] + for (x, ns) in List.zip xs ctx do + let mut is := #[] + for _ in ns do + let i <- rematIndc x + is := is.push i + inds := inds.push is.toList + return .inductive ⟨inds.toList⟩ | .meta m => throw (.rawMetadata m) -- TODO: This could return a Proof inductive, since proofs have no metadata | .proof p => throw (.rawProof p) | .comm p => throw (.rawComm p) where - rematDefn : Ixon.Definition -> RematM Ix.Definition - | x => .mk x.lvls <$> rematExpr x.type <*> rematExpr x.value <*> pure x.part - rematCtor : Ixon.Constructor -> RematM Ix.Constructor - | x => do + rematDefn (x: Ixon.Definition) : RematM Ix.Definition := do + let _ <- rematIncr + let (name, hints, all) <- match (<- rematMeta) with + | [.name n, .hints h, .all as] => pure (n, h, as) + | _ => rematThrowUnexpected + let lvls <- rematLevels x.lvls + let type <- rematExpr x.type + let value <- rematExpr x.value + return .mk name lvls type x.mode value hints x.safety all + rematCtor (x: Ixon.Constructor) : RematM Ix.Constructor := do + let _ <- rematIncr + let name <- match (<- rematMeta) with + | [.name n] => pure n + | _ => rematThrowUnexpected + let lvls <- rematLevels x.lvls let t <- rematExpr x.type - return .mk x.lvls t x.idx x.params x.fields - rematRecr : Ixon.Recursor -> RematM Ix.Recursor - | x => do + return .mk name lvls t x.cidx x.params x.fields x.isUnsafe + rematRecrRule (x: Ixon.RecursorRule) : RematM Ix.RecursorRule := do + let _ <- rematIncr + let ctor <- match (<- rematMeta) with + | [.name n] => pure n + | _ => rematThrowUnexpected + let rhs <- rematExpr x.rhs + return ⟨ctor, x.fields, rhs⟩ + rematRecr (x: Ixon.Recursor) : RematM Ix.Recursor := do + let _ <- rematIncr + let name <- match (<- rematMeta) with + | [.name n] => pure n + | _ => rematThrowUnexpected + let lvls <- rematLevels x.lvls let t <- rematExpr x.type - let rrs <- x.rules.mapM (fun rr => .mk rr.fields <$> rematExpr rr.rhs) - return .mk x.lvls t x.params x.indices x.motives x.minors rrs x.isK x.internal - rematInd : Ixon.Inductive -> RematM Ix.Inductive - | x => do + let rs <- x.rules.mapM rematRecrRule + return ⟨name, lvls, t, x.params, x.indices, x.motives, x.minors, rs, x.k, x.isUnsafe⟩ + rematIndc (x: Ixon.Inductive) : RematM Ix.Inductive := do + let _ <- rematIncr + let (name, all) <- match (<- rematMeta) with + | [.name n, .all as] => pure (n, as) + | _ => rematThrowUnexpected + let lvls <- rematLevels x.lvls let t <- rematExpr x.type let cs <- x.ctors.mapM rematCtor let rs <- x.recrs.mapM rematRecr - return .mk x.lvls t x.params x.indices cs rs x.recr x.refl x.struct x.unit + return ⟨name, lvls, t, x.params, x.indices, all, cs, rs, x.nested, x.recr, + x.refl, x.isUnsafe⟩ + +def rematerialize (c m: Ixon.Const) : Except TransportError Ix.Const := do + let m <- match m with + | .meta m => pure m + | x => throw <| .expectedMetadata x + match ((rematConst c).run { meta := m }).run emptyRematState with + | .ok a _ => return a + | .error e _ => throw e end Ix.TransportM diff --git a/Tests/Ix.lean b/Tests/Ix.lean index dd8f83cd..774abf88 100644 --- a/Tests/Ix.lean +++ b/Tests/Ix.lean @@ -1,5 +1,6 @@ import LSpec import Ix.Ixon +import Ix.Ixon.Metadata import Ix.Address import Ix.Ixon.Serialize import Ix.Ixon.Univ @@ -8,6 +9,8 @@ import LSpec.SlimCheck.Gen import LSpec import Blake3 +import Tests.Common +import Tests.Ix.Common import Tests.Ix.Ixon import Tests.Ix.IR @@ -22,7 +25,7 @@ def serde [Ixon.Serialize A] [BEq A] (x: A) : Bool := open Ix.TransportM -def transportUniv (univ: Ix.Univ): Bool := +def transportUniv (univ: Ix.Level): Bool := match EStateM.run (dematUniv univ) emptyDematState with | .ok ixon stt => let remat := (ReaderT.run (rematUniv ixon) { meta := stt.meta}) @@ -58,27 +61,28 @@ def transportConst (x: Ix.Const): Bool := -- | .error e _ => .error e -- | .error e _ => .error e -- ---def myConfig : SlimCheck.Configuration where --- numInst := 100000 --- maxSize := 100 --- traceDiscarded := true --- traceSuccesses := true --- traceShrink := true --- traceShrinkCandidates := true +def myConfig : SlimCheck.Configuration where + numInst := 10000 + maxSize := 100 + traceDiscarded := true + traceSuccesses := true + traceShrink := true + traceShrinkCandidates := true ---def dbg : IO UInt32 := do --- --SlimCheck.Checkable.check (∀ x: Ix.Univ, transportUniv x) myConfig --- SlimCheck.Checkable.check (∀ x: Ix.Expr, transportExpr x) myConfig --- return 0 +def dbg : IO UInt32 := do + SlimCheck.Checkable.check (∀ x: Ix.Const, transportConst x) myConfig + return 0 --def Test.Ix.unitTransport : TestSeq := -- testExprs.foldl (init := .done) fun tSeq x => -- tSeq ++ (test s!"transport {repr x}" $ Except.isOk (transportExpr' x)) + def Tests.Ix.suite : List LSpec.TestSeq := [ + check "metadatum serde" (∀ x : Ixon.Metadatum, serde x), check "universe serde" (∀ x : Ixon.Univ, serde x), - check "universe transport" (∀ x : Ix.Univ, transportUniv x), + check "universe transport" (∀ x : Ix.Level, transportUniv x), check "expr serde" (∀ x : Ixon.Expr, serde x), check "expr transport" (∀ x : Ix.Expr, transportExpr x), check "const serde" (∀ x : Ixon.Const, serde x), diff --git a/Tests/Ix/Common.lean b/Tests/Ix/Common.lean index 438a725a..1b37f51c 100644 --- a/Tests/Ix/Common.lean +++ b/Tests/Ix/Common.lean @@ -1,4 +1,5 @@ import LSpec +import Ix.Common import Ix.Ixon import Ix.Address import Ix.Ixon.Serialize @@ -37,6 +38,10 @@ def genList' (gen: Gen α) : Gen (List α) := do let n ← genNat' List.mapM (fun _ => gen) (List.range n) +def genListSize (gen: Gen α) (lo hi: Nat): Gen (List α) := do + let n ← choose Nat lo hi + List.mapM (fun _ => gen) (List.range n) + def genOption (gen: Gen α) : Gen (Option α) := oneOf' [ pure .none, .some <$> gen] @@ -65,6 +70,18 @@ def genBinderInfo : Gen Lean.BinderInfo := oneOf' , pure .instImplicit ] +def genDefMode : Gen Ix.DefMode := oneOf' + [ pure .opaque + , pure .theorem + , pure .definition + ] + +def genReducibilityHints : Gen Lean.ReducibilityHints := oneOf' + [ pure .opaque + , pure .abbrev + , (.regular ·.toUInt32) <$> genUSize + ] + def genQuotKind : Gen Lean.QuotKind := oneOf' [ pure .type , pure .ctor diff --git a/Tests/Ix/Compile.lean b/Tests/Ix/Compile.lean index 39f2f995..d84f0398 100644 --- a/Tests/Ix/Compile.lean +++ b/Tests/Ix/Compile.lean @@ -4,43 +4,139 @@ import Ix.Ixon import Ix.Address import Ix.Common import Ix.CompileM +import Ix.DecompileM import Ix.Meta +import Ix.IR import Lean import Tests.Ix.Fixtures import Lean open LSpec open Ix.Compile +open Ix.Decompile ---def testCompileExpr (env: Lean.Environment) --- (msg: String) (commit: Bool) (input: Lean.Expr) (expected: Ix.Expr) --- : IO TestSeq := do --- let (out, _) <- --- CompileM.runIO' env (compileExpr commit input) --- return test msg (out == expected) --- ---def threeIO : IO TestSeq := do --- return test "one isn't two" (1 == 2) --- ---def foo : IO Lean.Expr := do --- runMeta (Lean.Meta.whnf (Lean.toExpr 3)) (<- get_env!) --- ---def bar : IO Ix.Expr := do --- let env <- get_env! --- let .defnInfo defn ← runCore (Lean.getConstInfo ``id) env --- | unreachable! --- let input <- runMeta (Lean.Meta.whnf defn.value) env --- --let (out, _) <- CompileM.runIO' env (compileExpr false input) --- return out - ---#eval bar - -def test1 : IO TestSeq := do + +namespace Test.Ix.Inductives + +mutual + unsafe inductive A | a : B → C → A + unsafe inductive B | b : A → B + unsafe inductive C | c : A → C +end + +end Test.Ix.Inductives + + +namespace Test.Ix.Mutual + + +mutual + unsafe def A : Nat → Nat + | 0 => 0 + | n + 1 => B n + C n + 1 + + unsafe def B : Nat → Nat + | 0 => 0 + | n + 1 => A n + 1 + + unsafe def C : Nat → Nat + | 0 => 0 + | n + 1 => A n + 1 +end + +end Test.Ix.Mutual + + +def testMutual : IO TestSeq := do + let env <- get_env! + let mut cstt : CompileState := .init env 0 + let all := (env.getDelta.find! `Test.Ix.Mutual.A).all + let predefs <- all.mapM fun n => match env.getDelta.find! n with + | .defnInfo d => pure <| Ix.mkPreDefinition d + | .opaqueInfo d => pure <| Ix.mkPreOpaque d + | .thmInfo d => pure <| Ix.mkPreTheorem d + | _ => throw (IO.userError "not a def") + let (dss, _) <- match (sortDefs predefs).run (.init 200000) cstt with + | .ok a stt => do + pure (a, stt) + | .error e _ => do + throw (IO.userError (<- e.pretty)) + let res := [[`Test.Ix.Mutual.C, `Test.Ix.Mutual.B],[`Test.Ix.Mutual.A]] + let nss := dss.map fun ds => ds.map (·.name) + return test "test mutual" (res == nss) + +def testInductives : IO TestSeq := do + let env <- get_env! + let mut cstt : CompileState := .init env 0 + --let delta := env.getDelta.filter fun n _ => namesp.isPrefixOf n + --let consts := env.getConstMap.filter fun n _ => namesp.isPrefixOf n + let all := (env.getDelta.find! `Test.Ix.Inductives.A).all + let preinds <- all.mapM fun n => match env.getDelta.find! n with + | .inductInfo v => match (makePreInductive v).run (.init 200000) cstt with + | .ok a _ => pure a + | .error e _ => do throw (IO.userError (<- e.pretty)) + | _ => throw (IO.userError "not an inductive") + let (dss, _) <- match (sortInds preinds).run (.init 200000) cstt with + | .ok a stt => do + pure (a, stt) + | .error e _ => do + throw (IO.userError (<- e.pretty)) + let res := [[`Test.Ix.Inductives.C], [`Test.Ix.Inductives.B],[`Test.Ix.Inductives.A]] + let nss := dss.map fun ds => ds.map (·.name) + return test "test inductives" (res == nss) + +def testRoundtripGetEnv : IO TestSeq := do let env <- get_env! - let input <- runMeta (Lean.Meta.whnf (Lean.toExpr 3)) env - let expected := Lean.Expr.lit (Lean.Literal.natVal 3) - return test "expected 3" (input == expected) + let mut cstt : CompileState := .init env 0 + --IO.println s!"compiling env" + for (_, c) in env.getDelta do + let (_, stt) <- match (compileConst c).run (.init 200000) cstt with + | .ok a stt => do + --stt.store.forM fun a c => discard $ (Store.forceWriteConst a c).toIO + pure (a, stt) + | .error e _ => do + IO.println s!"failed {c.name}" + throw (IO.userError (<- e.pretty)) + let (anon, meta) <- match stt.names.find? c.name with + | .some (a, m) => pure (a, m) + | .none => throw (IO.userError "name {n} not in env") + IO.println s!"✓ {c.name} -> {anon}:{meta}" + cstt := stt + IO.println s!"compiled env" + IO.println s!"decompiling env" + let denv := DecompileEnv.init cstt.names cstt.store + let dstt <- match decompileEnv.run denv default with + | .ok _ s => pure s + --IO.println s!"✓ {n} @ {anon}:{meta}" + | .error e _ => do + throw (IO.userError e.pretty) + IO.println s!"decompiled env" + let mut res := true + for (n, (anon, meta)) in denv.names do + let c <- match env.constants.find? n with + | .some c => pure c + | .none => throw (IO.userError "name {n} not in env") + match dstt.constants.find? n with + | .some c2 => + if c.stripMData == c2.stripMData + then + IO.println s!"✓ {n} @ {anon}:{meta}" + else + IO.println s!"× {n} @ {anon}:{meta}" + IO.FS.writeFile "c.out" s!"{repr c.stripMData}" + IO.FS.writeFile "c2.out" s!"{repr c2.stripMData}" + res := false + break + | .none => do + let e' := (DecompileError.unknownName default n).pretty + throw (IO.userError e') + IO.println s!"input delta: {env.getDelta.toList.length}" + IO.println s!"input env: {env.constants.toList.length}" + IO.println s!"output env: {dstt.constants.toList.length}" + return test "env compile roundtrip" (res == true) def Tests.Ix.Compile.suiteIO: List (IO TestSeq) := [ - test1 + testMutual, + testInductives, + testRoundtripGetEnv ] diff --git a/Tests/Ix/Fixtures.lean b/Tests/Ix/Fixtures.lean index 721a93ef..1189aba6 100644 --- a/Tests/Ix/Fixtures.lean +++ b/Tests/Ix/Fixtures.lean @@ -1,6 +1,7 @@ import Tests.Ix.Fixtures.Export -set_option linter.all false -- prevent error messages from runFrontend +namespace Test.Ix.Fixtures + namespace WellFounded mutual @@ -165,7 +166,6 @@ end Inductives namespace Import - def Foo := MyNat -- triggering the compilation of `MyNat` def Bar := Nat -- triggering the compilation of `Nat` @@ -174,3 +174,6 @@ inductive MyOtherNat | mais : MyOtherNat → MyOtherNat end Import + +end Test.Ix.Fixtures + diff --git a/Tests/Ix/IR.lean b/Tests/Ix/IR.lean index 66f0e477..60fa726b 100644 --- a/Tests/Ix/IR.lean +++ b/Tests/Ix/IR.lean @@ -1,3 +1,4 @@ +import Ix.Common import Ix.IR import LSpec.SlimCheck.Gen @@ -12,23 +13,23 @@ open SlimCheck.Gen namespace Ix -def genUniv : Gen Ix.Univ := getSize >>= go +def genLevel : Gen Ix.Level := getSize >>= go where - go : Nat -> Gen Ix.Univ + go : Nat -> Gen Ix.Level | 0 => return .zero | Nat.succ f => frequency [ (100, return .zero), - (100, .var <$> genName <*> genNatUSize), + (100, .param <$> genName <*> genNatUSize), (50, .succ <$> go f), (25, .max <$> go f <*> go f), (25, .imax <$> go f <*> go f) ] -instance : Shrinkable Ix.Univ where +instance : Shrinkable Ix.Level where shrink _ := [] -instance : SampleableExt Ix.Univ := SampleableExt.mkSelfContained genUniv +instance : SampleableExt Ix.Level := SampleableExt.mkSelfContained genLevel def genExpr : Gen Ix.Expr := getSize >>= go where @@ -37,9 +38,9 @@ def genExpr : Gen Ix.Expr := getSize >>= go | Nat.succ f => frequency [ (100, .var <$> genNatUSize), - (100, .sort <$> genUniv), - (50, .const <$> genName <*> genAddress <*> genAddress <*> resizeListOf genUniv), - (50, .rec_ <$> genNat' <*> resizeListOf genUniv), + (100, .sort <$> genLevel), + (50, .const <$> genName <*> genAddress <*> genAddress <*> resizeListOf genLevel), + (50, .rec_ <$> genName <*> genNat' <*> resizeListOf genLevel), (50, .app <$> go f <*> go f), (50, .lam <$> genName <*> genBinderInfo <*> go f <*> go f), (50, .pi <$> genName <*> genBinderInfo <*> go f <*> go f), @@ -57,32 +58,60 @@ instance : SampleableExt Ix.Expr := SampleableExt.mkSelfContained genExpr def genConst : Gen Ix.Const := getSize >>= go where - genDef : Gen Ix.Definition := .mk <$> genNat' <*> genExpr <*> genExpr <*> genBool + genNames : Gen (List Lean.Name) := resizeListOf genName + genDef : Gen Ix.Definition := do + let n <- genName + let lvls <- genNames + let type <- genExpr + let mode <- genDefMode + let value <- genExpr + let hints <- genReducibilityHints + let safety <- oneOf #[pure .safe, pure .partial, pure .unsafe] + let all <- genNames + return ⟨n, lvls, type, mode, value, hints, safety, all⟩ genCtor : Gen Ix.Constructor := - .mk <$> genNat' <*> genExpr <*> genNat' <*> genNat' <*> genNat' + .mk <$> genName <*> genNames <*> genExpr <*> genNat' <*> genNat' <*> genNat' <*> genBool genRecr : Gen Ix.Recursor := - .mk <$> genNat' <*> genExpr <*> genNat' <*> genNat' <*> genNat' <*> genNat' - <*> resizeListOf (.mk <$> genNat' <*> genExpr) + .mk <$> genName <*> genNames <*> genExpr <*> genNat' <*> genNat' <*> genNat' <*> genNat' + <*> resizeListOf (.mk <$> genName <*> genNat' <*> genExpr) <*> genBool <*> genBool - genInd : Gen Ix.Inductive := - .mk <$> genNat' <*> genExpr <*> genNat' <*> genNat' - <*> resizeListOf genCtor <*> resizeListOf genRecr - <*> genBool <*> genBool <*> genBool <*> genBool + genInd : Gen Ix.Inductive := do + let n <- genName + let lvls <- genNames + let type <- genExpr + let params <- genNat' + let indices <- genNat' + let all <- genNames + let ctors <- resizeListOf genCtor + let recrs <- resizeListOf genRecr + let nested <- genNat' + let (isRec, isRefl, isUnsafe) <- (·,·,·) <$> genBool <*> genBool <*> genBool + return ⟨n, lvls, type, params, indices, all, ctors, recrs, nested, isRec, isRefl, isUnsafe⟩ + genMutDef : Gen Ix.MutualBlock := do + let nns <- resizeListOf (genListSize genName 1 5) + let ds <- nns.mapM fun ns => do + let x <- genDef + ns.mapM (fun _ => pure x) + return .mk ds + genMutInd : Gen Ix.InductiveBlock := do + let nns <- resizeListOf (genListSize genName 1 5) + let ds <- nns.mapM fun ns => do + let x <- genInd + ns.mapM (fun _ => pure x) + return .mk ds go : Nat -> Gen Ix.Const - | 0 => return .«axiom» (.mk 0 (Ix.Expr.sort (Ix.Univ.zero))) + | 0 => return .«axiom» (.mk .anonymous [] (Ix.Expr.sort (Ix.Level.zero)) false) | Nat.succ _ => frequency [ - (100, .«axiom» <$> (.mk <$> genNat' <*> genExpr)), - (100, .«theorem» <$> (.mk <$> genNat' <*> genExpr <*> genExpr)), - (100, .«opaque» <$> (.mk <$> genNat' <*> genExpr <*> genExpr)), + (100, .«axiom» <$> (.mk <$> genName <*> genNames <*> genExpr <*> genBool)), (100, .«definition» <$> genDef), - (100, .quotient <$> (.mk <$> genNat' <*> genExpr <*> genQuotKind)), - (100, .inductiveProj <$> (.mk <$> genAddress <*> genAddress <*> genNat')), - (100, .constructorProj <$> (.mk <$> genAddress <*> genAddress <*> genNat' <*> genNat')), - (100, .recursorProj <$> (.mk <$> genAddress <*> genAddress <*> genNat' <*> genNat')), - (100, .definitionProj <$> (.mk <$> genAddress <*> genAddress <*> genNat')), - (100, .mutDefBlock <$> resizeListOf genDef), - (100, .mutIndBlock <$> resizeListOf genInd), + (100, .quotient <$> (.mk <$> genName <*> genNames <*> genExpr <*> genQuotKind)), + (100, .inductiveProj <$> (.mk <$> genName <*> genAddress <*> genAddress <*> genNat')), + (100, .constructorProj <$> (.mk <$> genName <*> genAddress <*> genAddress <*> genNat' <*> genName <*> genNat')), + (100, .recursorProj <$> (.mk <$> genName <*> genAddress <*> genAddress <*> genNat' <*> genName <*> genNat')), + (100, .definitionProj <$> (.mk <$> genName <*> genAddress <*> genAddress <*> genNat')), + (100, .mutual <$> genMutDef), + (100, .inductive <$> genMutInd), ] instance : Shrinkable Ix.Const where diff --git a/Tests/Ix/Ixon.lean b/Tests/Ix/Ixon.lean index e64cafb3..ec508370 100644 --- a/Tests/Ix/Ixon.lean +++ b/Tests/Ix/Ixon.lean @@ -16,9 +16,9 @@ open Ixon namespace Ixon -def genUniv : SlimCheck.Gen Ixon.Univ := getSize >>= go +def genUniv : Gen Ixon.Univ := getSize >>= go where - go : Nat -> SlimCheck.Gen Ixon.Univ + go : Nat -> Gen Ixon.Univ | 0 => return .const 0 | Nat.succ f => frequency [ @@ -64,23 +64,44 @@ instance : SampleableExt Expr := SampleableExt.mkSelfContained genExpr -- Metadata -def genMetaNode : Gen MetaNode := - .mk <$> genOption genName <*> genOption genBinderInfo <*> genOption genAddress + +def genMetadatum : Gen Ixon.Metadatum := + frequency [ + (100, .name <$> genName), + (100, .info <$> genBinderInfo), + (100, .link <$> genAddress), + (100, .hints <$> genReducibilityHints), + (25, .all <$> genList' genName), + ] + +instance : Shrinkable Metadatum where + shrink _ := [] + +instance : SampleableExt Metadatum := + SampleableExt.mkSelfContained genMetadatum + +def genMetaNode : Gen (List Metadatum) := + genList' genMetadatum def genMetadata : Gen Metadata := do let xs ← genList' genMetaNode return .mk (Batteries.RBMap.ofList ((List.range xs.length).zip xs) compare) + -- Const -def genAxiom : Gen Axiom := .mk <$> genNat' <*> genExpr -def genTheorem : Gen Theorem := .mk <$> genNat' <*> genExpr <*> genExpr -def genOpaque : Gen Opaque := .mk <$> genNat' <*> genExpr <*> genExpr -def genDefinition : Gen Definition := - .mk <$> genNat' <*> genExpr <*> genExpr <*> genBool +def genAxiom : Gen Axiom := .mk <$> genNat' <*> genExpr <*> genBool + +def genDefinition : Gen Definition := do + let lvls <- genNat' + let type <- genExpr + let mode <- genDefMode + let value <- genExpr + let safety <- oneOf #[pure .safe, pure .unsafe, pure .partial] + return .mk lvls type mode value safety def genConstructor : Gen Constructor := - .mk <$> genNat' <*> genExpr <*> genNat' <*> genNat' <*> genNat' + .mk <$> genNat' <*> genExpr <*> genNat' <*> genNat' <*> genNat' <*> genBool def genRecursorRule : Gen RecursorRule := .mk <$> genNat' <*> genExpr @@ -90,8 +111,8 @@ def genRecursor : Gen Recursor := def genInductive : Gen Inductive := .mk <$> genNat' <*> genExpr <*> genNat' <*> genNat' - <*> genList' genConstructor <*> genList' genRecursor - <*> genBool <*> genBool <*> genBool <*> genBool + <*> genList' genConstructor <*> genList' genRecursor <*> genNat' + <*> genBool <*> genBool <*> genBool def genConstructorProj : Gen ConstructorProj := .mk <$> genAddress <*> genNat' <*> genNat' @@ -109,12 +130,10 @@ def genInductiveProj : Gen InductiveProj := def genConst : Gen Ixon.Const := getSize >>= go where go : Nat -> Gen Ixon.Const - | 0 => return .axio ⟨0, .vari 0⟩ + | 0 => return .axio ⟨0, .vari 0, false⟩ | Nat.succ _ => frequency [ (100, .axio <$> genAxiom), - (100, .theo <$> genTheorem), - (100, .opaq <$> genOpaque), (100, .defn <$> genDefinition), --(100, .ctor <$> genConstructor), --(100, .recr <$> genRecursor), diff --git a/Tests/Ix/Lean.lean b/Tests/Ix/Lean.lean new file mode 100644 index 00000000..e69de29b diff --git a/Tests/Main.lean b/Tests/Main.lean index c1b7651e..ad760ee5 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -9,10 +9,8 @@ import Tests.Keccak import Tests.Cli def main (args: List String) : IO UInt32 := do - if args.contains "compile" then - LSpec.lspecEachIO Tests.Ix.Compile.suiteIO id - else if args.contains "cli" then - Tests.ixCli + if args.contains "compile" + then LSpec.lspecEachIO Tests.Ix.Compile.suiteIO id else LSpec.lspecIO (.ofList [ ("aiur", Tests.Aiur.suite),