From c842ff34ebed50639f367769c4191143d09fff3d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Jan 2025 14:25:40 +0000 Subject: [PATCH 1/5] Start updating to Lean v4.15.0 --- backends/lean/Base/Arith/Int.lean | 7 +- backends/lean/Base/Arith/ScalarNF.lean | 6 +- backends/lean/Base/Diverge/Base.lean | 11 ++- backends/lean/Base/Diverge/Elab.lean | 87 ++++++++++++---------- backends/lean/Base/Diverge/ElabBase.lean | 8 +- backends/lean/Base/Extensions.lean | 13 +--- backends/lean/Base/List/List.lean | 4 +- backends/lean/Base/Progress/Base.lean | 12 +-- backends/lean/Base/Progress/Progress.lean | 4 +- backends/lean/Base/Saturate/Attribute.lean | 11 +-- backends/lean/Base/Saturate/Tactic.lean | 29 ++++---- backends/lean/Base/Termination.lean | 2 +- backends/lean/Base/Utils.lean | 50 ++++++++----- backends/lean/lake-manifest.json | 84 +++++++++++++-------- backends/lean/lakefile.lean | 11 --- backends/lean/lakefile.toml | 10 +++ backends/lean/lean-toolchain | 2 +- 17 files changed, 189 insertions(+), 162 deletions(-) delete mode 100644 backends/lean/lakefile.lean create mode 100644 backends/lean/lakefile.toml diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index b215654d1..cdb17fa09 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -198,10 +198,13 @@ def intTac (tacName : String) (splitAllDisjs splitGoalConjs : Bool) [``and_self, ``false_implies, ``true_implies, ``Prod.mk.injEq, ``not_false_eq_true, ``not_true_eq_false, ``true_and, ``and_true, ``false_and, ``and_false, - ``true_or, ``or_true,``false_or, ``or_false] []) + ``true_or, ``or_true,``false_or, ``or_false, + ``Bool.true_eq_false, ``Bool.false_eq_true] []) allGoalsNoRecover (do trace[Arith] "Goal after simplification: {← getMainGoal}" - Tactic.Omega.omegaTactic {}) + trace[Arith] "Calling omega" + Tactic.Omega.omegaTactic {} + trace[Arith] "Omega solved the goal") if splitAllDisjs then do /- In order to improve performance, we first try to prove the goal without splitting. If it fails, we split. -/ diff --git a/backends/lean/Base/Arith/ScalarNF.lean b/backends/lean/Base/Arith/ScalarNF.lean index 59f264958..ccb8b0004 100644 --- a/backends/lean/Base/Arith/ScalarNF.lean +++ b/backends/lean/Base/Arith/ScalarNF.lean @@ -21,7 +21,9 @@ macro_rules open Lean.Parser.Tactic in open Mathlib.Tactic.Ring in -macro "scalar_nf" cfg:(config)? loc:(location)? : tactic => - `(tactic| ring_nf $(cfg)? $(loc)?) +macro "scalar_nf" cfg:optConfig loc:(location)? : tactic => + `(tactic| ring_nf $cfg:optConfig $(loc)?) + +example : True := by ring_nf end Arith diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean index 8803f3d8e..0b972830a 100644 --- a/backends/lean/Base/Diverge/Base.lean +++ b/backends/lean/Base/Diverge/Base.lean @@ -581,7 +581,7 @@ namespace FixI -- However, by parameterizing Funs with those parameters, we can state -- and prove lemmas like Funs.is_valid_p_is_valid_p inductive Funs (id : Type u) (a : id → Type v) (b : (i:id) → (x:a i) → Type w) : - List in_out_ty.{v, w} → Type (max (u + 1) (max (v + 1) (w + 1))) := + List in_out_ty.{v, w} → Type (max (u + 1) (max (v + 1) (w + 1))) where | Nil : Funs id a b [] | Cons {ity : Type v} {oty : ity → Type w} {tys : List in_out_ty} (f : kk_ty id a b → (x:ity) → Result (oty x)) (tl : Funs id a b tys) : @@ -794,7 +794,7 @@ namespace FixII -- and prove lemmas like Funs.is_valid_p_is_valid_p inductive Funs (id : Type u) (ty : id → Type v) (a : (i:id) → ty i → Type w) (b : (i:id) → ty i → Type x) : - List in_out_ty.{v, w, x} → Type (max (u + 1) (max (v + 1) (max (w + 1) (x + 1)))) := + List in_out_ty.{v, w, x} → Type (max (u + 1) (max (v + 1) (max (w + 1) (x + 1)))) where | Nil : Funs id ty a b [] | Cons {it: Type v} {ity : it → Type w} {oty : it → Type x} {tys : List in_out_ty} (f : kk_ty id ty a b → (i:it) → (x:ity i) → Result (oty i)) (tl : Funs id ty a b tys) : @@ -1223,7 +1223,7 @@ namespace Ex5 apply is_valid_p_bind <;> try simp_all /- An example which uses map -/ - inductive Tree (a : Type) := + inductive Tree (a : Type) where | leaf (x : a) | node (tl : List (Tree a)) @@ -1262,7 +1262,7 @@ namespace Ex5 := by have Heq := is_valid_fix_fixed_eq (@id_body_is_valid a) simp [id] - conv => lhs; rw [Heq]; simp; rw [id_body] + conv => lhs; rw [Heq]; simp; unfold id_body rfl end Ex5 @@ -1304,7 +1304,6 @@ namespace Ex6 intro x; try simp at x simp only [list_nth_body] -- Prove the validity of the individual bodies - intro k x split <;> try simp split <;> simp @@ -1507,7 +1506,7 @@ namespace Ex9 /- An example which uses map -/ open Primitives FixII Ex8 - inductive Tree (a : Type u) := + inductive Tree (a : Type u) where | leaf (x : a) | node (tl : List (Tree a)) diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index efd6c8e11..11ce74cd1 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -127,7 +127,7 @@ def mkProdsType (xl : List Expr) : MetaM Expr := -/ def splitInputArgs (in_tys : Array Expr) (out_ty : Expr) : MetaM (Array Expr × Array Expr) := do -- Look for the first parameter which appears in the subsequent parameters - let rec splitAux (in_tys : List Expr) : MetaM (HashSet FVarId × List Expr × List Expr) := + let rec splitAux (in_tys : List Expr) : MetaM (Std.HashSet FVarId × List Expr × List Expr) := match in_tys with | [] => do let fvars ← getFVarIds (← inferType out_ty) @@ -150,18 +150,18 @@ def splitInputArgs (in_tys : Array Expr) (out_ty : Expr) : MetaM (Array Expr × -- We must split later: update the fvars set let fvars := fvars.insertMany (← getFVarIds (← inferType ty)) pure (fvars, [], ty :: in_args) - let (_, in_tys, in_args) ← splitAux in_tys.data + let (_, in_tys, in_args) ← splitAux in_tys.toList pure (Array.mk in_tys, Array.mk in_args) /- Apply a lambda expression to some arguments, simplifying the lambdas -/ def applyLambdaToArgs (e : Expr) (xs : Array Expr) : MetaM Expr := do lambdaTelescopeN e xs.size fun vars body => -- Create the substitution - let s : HashMap FVarId Expr := HashMap.ofList (List.zip (vars.toList.map Expr.fvarId!) xs.toList) + let s : Std.HashMap FVarId Expr := Std.HashMap.ofList (List.zip (vars.toList.map Expr.fvarId!) xs.toList) -- Substitute in the body pure (body.replace fun e => match e with - | Expr.fvar fvarId => match s.find? fvarId with + | Expr.fvar fvarId => match s.get? fvarId with | none => e | some v => v | _ => none) @@ -447,10 +447,10 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr) Remark: the continuation has an indexed type; we use the index (a finite number of type `Fin`) to control which function we call at the recursive call site. -/ - let nameToInfo : HashMap Name (Nat × TypeInfo) := + let nameToInfo : Std.HashMap Name (Nat × TypeInfo) := let bl := preDefs.mapIdx fun i d => - (d.declName, (i.val, paramInOutTys.get! i.val)) - HashMap.ofList bl.toList + (d.declName, (i, paramInOutTys.get! i)) + Std.HashMap.ofList bl.toList trace[Diverge.def.genBody] "nameToId: {nameToInfo.toList}" @@ -466,7 +466,7 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr) -- Check if this is a recursive call if f.isConst then let name := f.constName! - match nameToInfo.find? name with + match nameToInfo.get? name with | none => pure e | some (id, type_info) => trace[Diverge.def.genBody.visit] "this is a recursive call" @@ -499,9 +499,9 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr) it without arguments (if we give it to a higher-order function for instance) and there are actually no type parameters. -/ - if (nameToInfo.find? name).isSome then do + if (nameToInfo.get? name).isSome then do -- Checking the type information - match nameToInfo.find? name with + match nameToInfo.get? name with | none => pure e | some (id, type_info) => trace[Diverge.def.genBody.visit] "this is a recursive call" @@ -539,7 +539,7 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr) -- (over which we match to retrieve the individual arguments). lambdaTelescope body fun args body => do -- Split the arguments between the type parameters and the "regular" inputs - let (_, type_info) := nameToInfo.find! preDef.declName + let (_, type_info) := nameToInfo.get! preDef.declName let (param_args, args) := args.toList.splitAt type_info.num_params let body ← mkProdsMatchOrUnit args body trace[Diverge.def.genBody] "Body after mkProdsMatchOrUnit: {body}" @@ -853,7 +853,7 @@ partial def proveAppIsValid (k_var kk_var : Expr) (e : Expr) (f : Expr) (args : - if yes: we have to lookup theorems in div spec database and continue -/ trace[Diverge.def.valid] "regular app: {e}, f: {f}, args: {args}" let argsFVars ← args.mapM getFVarIds - let allArgsFVars := argsFVars.foldl (fun hs fvars => hs.insertMany fvars) HashSet.empty + let allArgsFVars := argsFVars.foldl (fun hs fvars => hs.insertMany fvars) Std.HashSet.empty trace[Diverge.def.valid] "allArgsFVars: {allArgsFVars.toList.map mkFVar}" if ¬ allArgsFVars.contains kk_var.fvarId! then do -- Simple case @@ -878,8 +878,8 @@ partial def proveAppIsValidApplyThms (k_var kk_var : Expr) (e : Expr) -- Introduce fresh meta-variables for the universes let ul : List (Name × Level) ← thDecl.levelParams.mapM (λ x => do pure (x, ← mkFreshLevelMVar)) - let ulMap : HashMap Name Level := HashMap.ofList ul - let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x) + let ulMap : Std.HashMap Name Level := Std.HashMap.ofList ul + let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.get! x) trace[Diverge.def.valid] "Trying with theorem {thName}: {thTy}" -- Introduce meta variables for the universally quantified variables let (mvars, _binders, thTyBody) ← forallMetaTelescope thTy @@ -1133,9 +1133,9 @@ def mkDeclareFixDefs (mutRecBody : Expr) (paramInOutTys : Array TypeInfo) (preDe let defs ← preDefs.mapIdxM fun idx preDef => do lambdaTelescope preDef.value fun xs _ => do -- Retrieve the parameters info - let type_info := paramInOutTys.get! idx.val + let type_info := paramInOutTys.get! idx -- Create the index - let idx ← mkFinVal grSize idx.val + let idx ← mkFinVal grSize idx -- Group the inputs into two tuples let (params_args, input_args) := xs.toList.splitAt type_info.num_params let params ← mkSigmasVal type_info.params_ty params_args @@ -1256,11 +1256,11 @@ def divRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do let (params, in_tys) ← splitInputArgs in_tys out_ty trace[Diverge.def] "Decomposed arguments: {preDef.declName}: {params}, {in_tys}, {out_ty}" let num_params := params.size - let params_ty ← mkSigmasType params.data - let in_ty ← mkSigmasMatchOrUnit params.data (← mkProdsType in_tys.data) + let params_ty ← mkSigmasType params.toList + let in_ty ← mkSigmasMatchOrUnit params.toList (← mkProdsType in_tys.toList) -- Retrieve the type in the "Result" let out_ty ← getResultTy out_ty - let out_ty ← mkSigmasMatchOrUnit params.data out_ty + let out_ty ← mkSigmasMatchOrUnit params.toList out_ty trace[Diverge.def] "inOutTy: {preDef.declName}: {params_ty}, {in_tys}, {out_ty}" pure ⟨ total_num_args, num_params, params_ty, in_ty, out_ty ⟩)) trace[Diverge.def] "paramInOutTys: {paramInOutTys}" @@ -1386,31 +1386,43 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC else return () catch _ => s.restore +namespace Term + -- The following three functions are copy-pasted from Lean.Elab.MutualDef.lean open private elabHeaders levelMVarToParamHeaders getAllUserLevelNames withFunLocalDecls elabFunValues instantiateMVarsAtHeader instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes withUsed from Lean.Elab.MutualDef -- Copy/pasted from Lean.Elab.Term.withHeaderSecVars (because the definition is private) -private def Term.withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader) +private def withHeaderSecVars {α} (vars : Array Expr) (sc : Command.Scope) (headers : Array DefViewElabHeader) (k : Array Expr → TermElabM α) : TermElabM α := do - let (_, used) ← collectUsed.run {} + let mut revSectionFVars : Std.HashMap FVarId Name := {} + for (uid, var) in (← read).sectionFVars do + revSectionFVars := revSectionFVars.insert var.fvarId! uid + let (_, used) ← collectUsed revSectionFVars |>.run {} let (lctx, localInsts, vars) ← removeUnused vars used withLCtx lctx localInsts <| k vars where - collectUsed : StateRefT CollectFVars.State MetaM Unit := do + collectUsed revSectionFVars : StateRefT CollectFVars.State MetaM Unit := do -- directly referenced in headers headers.forM (·.type.collectFVars) -- included by `include` - vars.forM fun var => do - let ldecl ← getFVarLocalDecl var - if includedVars.contains ldecl.userName then - modify (·.add ldecl.fvarId) + for var in vars do + if let some uid := revSectionFVars[var.fvarId!]? then + if sc.includedVars.contains uid then + modify (·.add var.fvarId!) -- transitively referenced get >>= (·.addDependencies) >>= set + for var in (← get).fvarIds do + if let some uid := revSectionFVars[var]? then + if sc.omittedVars.contains uid then + throwError "cannot omit referenced section variable '{Expr.fvar var}'" -- instances (`addDependencies` unnecessary as by definition they may only reference variables -- already included) - vars.forM fun var => do + for var in vars do let ldecl ← getFVarLocalDecl var + if let some uid := revSectionFVars[var.fvarId!]? then + if sc.omittedVars.contains uid then + continue let st ← get if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then modify (·.add ldecl.fvarId) @@ -1422,7 +1434,7 @@ def isExample (views : Array DefView) : Bool := views.any (·.kind.isExample) open Language in -def Term.elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit := +def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit := if isExample views then withoutModifyingEnv do -- save correct environment in info tree @@ -1451,9 +1463,9 @@ where addTermInfo' view.declId funFVar let values ← try - let values ← elabFunValues headers vars includedVars + let values ← elabFunValues headers vars sc Term.synthesizeSyntheticMVarsNoPostponing - values.mapM (instantiateMVars ·) + values.mapM (instantiateMVarsProfiling ·) catch ex => logException ex headers.mapM fun header => mkSorry header.type (synthetic := true) @@ -1461,23 +1473,22 @@ where let letRecsToLift ← getLetRecsToLift let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes funFVars letRecsToLift - (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars headers else withUsed vars headers values letRecsToLift) fun vars => do + (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift for preDef in preDefs do trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}" - let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs + let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs let preDefs ← instantiateMVarsAtPreDecls preDefs let preDefs ← shareCommonPreDefs preDefs let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames for preDef in preDefs do trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}" - checkForHiddenUnivLevels allUserLevelNames preDefs addPreDefinitions preDefs -- MODIFICATION 2: we use our custom function here processDeriving headers for view in views, header in headers do -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting -- that depends only on a part of the ref - addDeclarationRanges header.declName view.ref + addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref processDeriving (headers : Array DefViewElabHeader) := do for header in headers, view in views do @@ -1488,7 +1499,7 @@ where unless (← processDefDeriving className header.declName) do throwError "failed to synthesize instance '{className}' for '{header.declName}'" -#check Command.elabMutualDef +end Term -- Copy/pasted from Lean.Elab.MutualDef open Command in @@ -1502,7 +1513,7 @@ def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do let mut reusedAllHeaders := true for h : i in [0:ds.size], headerPromise in headerPromises do let d := ds[i] - let modifiers ← elabModifiers d[0] + let modifiers ← elabModifiers ⟨d[0]⟩ if ds.size > 1 && modifiers.isNonrec then throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block" let mut view ← mkDefView modifiers d[2] -- MODIFICATION: changed the index to 2 @@ -1533,8 +1544,8 @@ def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do if let some snap := snap? then -- no non-fatal diagnostics at this point snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot } - let includedVars := (← getScope).includedVars - runTermElabM fun vars => Term.elabMutualDef vars includedVars views + let sc ← getScope + runTermElabM fun vars => Term.elabMutualDef vars sc views syntax (name := divergentDef) declModifiers "divergent" Lean.Parser.Command.definition : command diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean index 414340fe6..7e2123346 100644 --- a/backends/lean/Base/Diverge/ElabBase.lean +++ b/backends/lean/Base/Diverge/ElabBase.lean @@ -59,9 +59,7 @@ initialize divspecAttr : DivSpecAttr ← do let (_, _, fExpr) ← lambdaMetaTelescope fExpr.consumeMData trace[Diverge] "Registering divspec theorem for {fExpr}" -- Convert the function expression to a discrimination tree key - -- We use the default configuration - let config : WhnfCoreConfig := {} - DiscrTree.mkPath fExpr config) + DiscrTree.mkPath fExpr) let env := ext.addEntry env (fKey, thName) setEnv env trace[Diverge] "Saved the environment" @@ -71,9 +69,7 @@ initialize divspecAttr : DivSpecAttr ← do pure { attr := attrImpl, ext := ext } def DivSpecAttr.find? (s : DivSpecAttr) (e : Expr) : MetaM (Array Name) := do - -- We use the default configuration - let config : WhnfCoreConfig := {} - (s.ext.getState (← getEnv)).getMatch e config + (s.ext.getState (← getEnv)).getMatch e def DivSpecAttr.getState (s : DivSpecAttr) : MetaM (DiscrTree Name) := do pure (s.ext.getState (← getEnv)) diff --git a/backends/lean/Base/Extensions.lean b/backends/lean/Base/Extensions.lean index 8093ff183..3fa903662 100644 --- a/backends/lean/Base/Extensions.lean +++ b/backends/lean/Base/Extensions.lean @@ -20,22 +20,11 @@ def mkListDeclarationExtension [Inhabited α] (name : Name := by exact decl_name IO (ListDeclarationExtension α) := registerSimplePersistentEnvExtension { name := name, - addImportedFn := fun entries => entries.foldl (fun s l => l.data ++ s) [], + addImportedFn := fun entries => entries.foldl (fun s l => l.toList ++ s) [], addEntryFn := fun l x => x :: l, toArrayFn := fun l => l.toArray } --- This is not used anymore but we keep it here. --- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR? -def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : - IO (MapDeclarationExtension α) := - registerSimplePersistentEnvExtension { - name := name, - addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBMap.empty, - addEntryFn := fun s n => s.insert n.1 n.2, - toArrayFn := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1) - } - def SetDeclarationExtension := SimplePersistentEnvExtension Name NameSet def mkSetDeclarationExtension (name : Name := by exact decl_name%) : diff --git a/backends/lean/Base/List/List.lean b/backends/lean/Base/List/List.lean index 2d46c88ec..e536ccbe1 100644 --- a/backends/lean/Base/List/List.lean +++ b/backends/lean/Base/List/List.lean @@ -300,8 +300,8 @@ theorem length_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Nat) ( theorem length_flatten_update_eq_disj {α : Type u} (ls : List (List α)) (i : Nat) (x : List α) : i < 0 ∨ ls.length ≤ i ∨ (ls.update i x).flatten.length + (ls.index i).length = ls.flatten.length + x.length := by - cases h: (i < 0 : Bool) <;> simp_all - cases h: (ls.length ≤ i : Bool) <;> simp_all + cases h: (i < 0 : Bool) <;> simp_all only [not_lt_zero', decide_false, Bool.false_eq_true, not_false_eq_true, neq_imp] + cases h: (ls.length ≤ i : Bool) <;> simp_all only [decide_eq_false_iff_not, not_le, false_or, decide_eq_true_eq, true_or] rw [length_flatten_update_eq] <;> simp [*] theorem length_flatten_update_as_int_eq {α : Type u} (ls : List (List α)) (i : Nat) (x : List α) diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 816ff3483..7a597dac3 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -108,9 +108,9 @@ section Methods -- Check if some existentially quantified variables let _ := do -- Collect all the free variables in the arguments - let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty + let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) Std.HashSet.empty -- Check if they intersect the fvars we introduced for the existentially quantified variables - let evarsSet : HashSet FVarId := HashSet.empty.insertMany (evars.map (fun (x : Expr) => x.fvarId!)) + let evarsSet : Std.HashSet FVarId := Std.HashSet.empty.insertMany (evars.map (fun (x : Expr) => x.fvarId!)) let filtArgsFVars := allArgsFVars.toArray.filter (fun var => evarsSet.contains var) if filtArgsFVars.isEmpty then pure () else @@ -166,9 +166,7 @@ initialize pspecAttr : PSpecAttr ← do let fExpr ← getPSpecFunArgsExpr false ty trace[Progress] "Registering spec theorem for expr: {fExpr}" -- Convert the function expression to a discrimination tree key - -- We use the default configuration - let config : WhnfCoreConfig := {} - DiscrTree.mkPath fExpr config) + DiscrTree.mkPath fExpr) let env := ext.addEntry env (fKey, thName) setEnv env trace[Progress] "Saved the environment" @@ -178,9 +176,7 @@ initialize pspecAttr : PSpecAttr ← do pure { attr := attrImpl, ext := ext } def PSpecAttr.find? (s : PSpecAttr) (e : Expr) : MetaM (Array Name) := do - -- We use the default configuration - let config : WhnfCoreConfig := {} - (s.ext.getState (← getEnv)).getMatch e config + (s.ext.getState (← getEnv)).getMatch e def PSpecAttr.getState (s : PSpecAttr) : MetaM (DiscrTree Name) := do pure (s.ext.getState (← getEnv)) diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 1157a7f1c..7926fb7e9 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -213,7 +213,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) trace[Progress] "new goals: {newGoals}" -- Split between the goals which are propositions and the others let (newPropGoals, newNonPropGoals) ← - newGoals.data.partitionM fun mvar => do isProp (← mvar.getType) + newGoals.toList.partitionM fun mvar => do isProp (← mvar.getType) trace[Progress] "Prop goals: {newPropGoals}" trace[Progress] "Non prop goals: {← newNonPropGoals.mapM fun mvarId => do pure ((← mvarId.getDecl).userName, mvarId)}" -- Try to solve the goals which are propositions @@ -259,7 +259,7 @@ def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : try let res ← progressWith fExpr th keep ids splitPost asmTac pure (some res) - catch _ => none + catch _ => pure none match res with | some .Ok => pure true | some (.Error msg) => throwError msg diff --git a/backends/lean/Base/Saturate/Attribute.lean b/backends/lean/Base/Saturate/Attribute.lean index 3fb14eb35..c444abb0f 100644 --- a/backends/lean/Base/Saturate/Attribute.lean +++ b/backends/lean/Base/Saturate/Attribute.lean @@ -162,7 +162,7 @@ initialize saturateAttr : SaturateAttribute ← do let pat ← instantiateMVars (← Elab.Term.elabTerm pat none |>.run') trace[Saturate.attribute] "Pattern: {pat}" -- Check that the pattern contains all the quantified variables - let allFVars ← fvars.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty + let allFVars ← fvars.foldlM (fun hs arg => getFVarIds arg hs) Std.HashSet.empty let patFVars ← getFVarIds pat (← getFVarIds (← inferType pat)) trace[Saturate.attribute] "allFVars: {← allFVars.toList.mapM FVarId.getUserName}" trace[Saturate.attribute] "patFVars: {← patFVars.toList.mapM FVarId.getUserName}" @@ -178,11 +178,10 @@ initialize saturateAttr : SaturateAttribute ← do -- Create the pattern let patExpr ← mkLambdaFVars fvars pat trace[Saturate.attribute] "Pattern expression: {patExpr}" - -- Create the discrimination tree key - we use the default configuration + -- Create the discrimination tree key let (_, _, patWithMetas) ← lambdaMetaTelescope patExpr trace[Saturate.attribute] "patWithMetas: {patWithMetas}" - let config : WhnfCoreConfig := {} - let key ← DiscrTree.mkPath patWithMetas config + let key ← DiscrTree.mkPath patWithMetas trace[Saturate.attribute] "key: {key}" -- let key : Key := ⟨ setName, key ⟩ @@ -204,9 +203,7 @@ def SaturateAttribute.find? (s : SaturateAttribute) (setName : Name) (e : Expr) match s.rules.find? setName with | none => pure #[] | some dTree => - -- We use the default configuration - let config : WhnfCoreConfig := {} - let rules ← dTree.getMatch e config + let rules ← dTree.getMatch e -- Filter the rules which have been deactivated pure (rules.filter fun r => s.nameToRule.contains r.thName) diff --git a/backends/lean/Base/Saturate/Tactic.lean b/backends/lean/Base/Saturate/Tactic.lean index ff222a7fe..38ba7133b 100644 --- a/backends/lean/Base/Saturate/Tactic.lean +++ b/backends/lean/Base/Saturate/Tactic.lean @@ -17,13 +17,12 @@ open Attribute We return the set of: (theroem name, list of arguments) -/ def matchExpr (nameToRule : NameMap Rule) (dtrees : Array (DiscrTree Rule)) - (boundVars : HashSet FVarId) - (matched : HashSet (Name × List Expr)) (e : Expr) : - MetaM (HashSet (Name × List Expr)) := do + (boundVars : Std.HashSet FVarId) + (matched : Std.HashSet (Name × List Expr)) (e : Expr) : + MetaM (Std.HashSet (Name × List Expr)) := do trace[Saturate] "Matching: {e}" dtrees.foldlM (fun matched dtree => do - let config : WhnfCoreConfig := {} - let exprs ← dtree.getMatch e config + let exprs ← dtree.getMatch e trace[Saturate] "Potential matches: {exprs}" -- Check each expression (exprs.foldlM fun matched rule => do @@ -43,7 +42,7 @@ def matchExpr (nameToRule : NameMap Rule) (dtrees : Array (DiscrTree Rule)) let arg ← instantiateMVars arg let hs ← getFVarIds arg hs pure (arg :: args, hs) - ) ([], HashSet.empty) + ) ([], Std.HashSet.empty) if boundVars.all (fun fvar => ¬ allFVars.contains fvar) then -- Ok: save the theorem trace[Saturate] "Matched with: {rule.thName} {args}" @@ -69,17 +68,17 @@ def matchExpr (nameToRule : NameMap Rule) (dtrees : Array (DiscrTree Rule)) /- Recursively explore a term -/ private partial def visit (depth : Nat) (nameToRule : NameMap Rule) (dtrees : Array (DiscrTree Rule)) - (boundVars : HashSet FVarId) - (matched : HashSet (Name × List Expr)) - (e : Expr) : MetaM (HashSet (Name × List Expr)) := do + (boundVars : Std.HashSet FVarId) + (matched : Std.HashSet (Name × List Expr)) + (e : Expr) : MetaM (Std.HashSet (Name × List Expr)) := do trace[Saturate] "Visiting {e}" -- Match let matched ← matchExpr nameToRule dtrees boundVars matched e -- Recurse let visitBinders (depth : Nat) - (boundVars : HashSet FVarId) (matched : HashSet (Name × List Expr)) (xs: Array Expr) : - MetaM (HashSet FVarId × (HashSet (Name × List Expr))) := do + (boundVars : Std.HashSet FVarId) (matched : Std.HashSet (Name × List Expr)) (xs: Array Expr) : + MetaM (Std.HashSet FVarId × (Std.HashSet (Name × List Expr))) := do -- Visit the type of the binders, as well as the bodies xs.foldlM (fun (boundVars, matched) x => do let fvarId := x.fvarId! @@ -144,14 +143,14 @@ def evalSaturate (sets : List Name) : TacticM Unit := do let matched ← decls.foldlM (fun matched (decl : LocalDecl) => do trace[Saturate] "Exploring local decl: {decl.userName}" /- We explore both the type, the expresion and the body (if there is) -/ - let matched ← visit 0 s.nameToRule dtrees HashSet.empty matched decl.type - let matched ← visit 0 s.nameToRule dtrees HashSet.empty matched decl.toExpr + let matched ← visit 0 s.nameToRule dtrees Std.HashSet.empty matched decl.type + let matched ← visit 0 s.nameToRule dtrees Std.HashSet.empty matched decl.toExpr match decl.value? with | none => pure matched - | some value => visit 0 s.nameToRule dtrees HashSet.empty matched value) HashSet.empty + | some value => visit 0 s.nameToRule dtrees Std.HashSet.empty matched value) Std.HashSet.empty -- Explore the goal trace[Saturate] "Exploring the goal" - let matched ← visit 0 s.nameToRule dtrees HashSet.empty matched (← Tactic.getMainTarget) + let matched ← visit 0 s.nameToRule dtrees Std.HashSet.empty matched (← Tactic.getMainTarget) -- Introduce the theorems in the context for (thName, args) in matched do let th ← mkAppOptM thName (args.map some).toArray diff --git a/backends/lean/Base/Termination.lean b/backends/lean/Base/Termination.lean index 1190af220..6609a3e9b 100644 --- a/backends/lean/Base/Termination.lean +++ b/backends/lean/Base/Termination.lean @@ -48,7 +48,7 @@ def removeInvImageAssumptions : TacticM Unit := do match d.value? with | none => pure hs | some e => getFVarIds e hs - ) HashSet.empty + ) Std.HashSet.empty let fvarIds := filtDecls.map fun d => d.fvarId let fvarIds := fvarIds.filter (fun id => ¬ allFVarsInTypes.contains id) -- Clear them diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index ab46e2c86..0a3e7c7bb 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -3,15 +3,6 @@ import Mathlib.Tactic.Core import Base.UtilsBase import Aesop -namespace List - - -- TODO: I could not find this function?? - @[simp] def flatten {a : Type u} : List (List a) → List a - | [] => [] - | x :: ls => x ++ flatten ls - -end List - namespace Lean namespace LocalContext @@ -396,14 +387,14 @@ def destEq (e : Expr) : MetaM (Expr × Expr) := do -- Return the set of FVarIds in the expression -- TODO: this collects fvars introduced in the inner bindings -partial def getFVarIds (e : Expr) (hs : HashSet FVarId := HashSet.empty) : MetaM (HashSet FVarId) := do - reduceVisit (fun _ (hs : HashSet FVarId) e => +partial def getFVarIds (e : Expr) (hs : Std.HashSet FVarId := Std.HashSet.empty) : MetaM (Std.HashSet FVarId) := do + reduceVisit (fun _ (hs : Std.HashSet FVarId) e => if e.isFVar then pure (hs.insert e.fvarId!) else pure hs) hs e -- Return the set of MVarIds in the expression -partial def getMVarIds (e : Expr) (hs : HashSet MVarId := HashSet.empty) : MetaM (HashSet MVarId) := do - reduceVisit (fun _ (hs : HashSet MVarId) e => +partial def getMVarIds (e : Expr) (hs : Std.HashSet MVarId := Std.HashSet.empty) : MetaM (Std.HashSet MVarId) := do + reduceVisit (fun _ (hs : Std.HashSet MVarId) e => if e.isMVar then pure (hs.insert e.mvarId!) else pure hs) hs e @@ -676,7 +667,6 @@ elab "split_existsl" " at " n:ident : tactic => do splitAllExistsTac fvar [] (fun _ _ => pure ()) example (h : a ∧ b) : a := by - split_existsl at h split_conj at h assumption @@ -727,7 +717,7 @@ def mkSimpCtx (simpOnly : Bool) (config : Simp.Config) (kind : SimpKind) let congrTheorems ← getSimpCongrTheorems let defaultSimprocs ← if simpOnly then pure {} else Simp.getSimprocs let simprocs ← simprocs.foldlM (fun simprocs name => simprocs.add name true) defaultSimprocs - let ctx := { config, simpTheorems := #[simpThms], congrTheorems } + let ctx ← Simp.mkContext config (simpTheorems := #[simpThms]) congrTheorems pure (ctx, #[simprocs]) inductive Location where @@ -836,9 +826,9 @@ def rewriteAt (cfg : Rewrite.Config) (rpt : Bool) -- Lookup the theorem and introduce fresh meta-variables for the universes let th ← mkConstWithFreshMVarLevels thName pure (x.fst, th) - match ← getEqnsFor? thName (nonRec := true) with + match ← getEqnsFor? thName with | some eqThms => do - eqThms.data.mapM lookupOne + eqThms.toList.mapM lookupOne | none => do pure [← lookupOne thName] let thms ← List.mapM lookupThm thms @@ -992,4 +982,30 @@ example (x y : Int) : True := by example (x y : Int) : True := by dcases h: x = y <;> simp +def extractGoal : TacticM Unit := do + withMainContext do + let ctx ← Lean.MonadLCtx.getLCtx + let decls ← ctx.getDecls + let assumptions : List Format ← decls.mapM fun decl => do + let ty ← Meta.ppExprWithInfos decl.type + let name := + match decl.userName with + | .num _ _ => "_" + | _ => decl.userName.toString + pure ("\n (" ++ name ++ " : " ++ ty.fmt ++ ")") + let assumptions := Format.joinSep assumptions "" + let mgoal ← Tactic.getMainGoal + let goal ← Meta.ppExprWithInfos (← mgoal.getType) + let msg := "example " ++ assumptions ++ " :\n " ++ goal.fmt ++ "\n := sorry" + println! msg + +elab "extract_goal" : tactic => do + withMainContext do + extractGoal + +example (x : Nat) (y : Nat) (_ : Nat) (h : x ≤ y) : y ≥ x := by + set_option linter.unusedTactic false in + extract_goal + omega + end Utils diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json index 859348233..187f608a2 100644 --- a/backends/lean/lake-manifest.json +++ b/backends/lean/lake-manifest.json @@ -1,75 +1,95 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53", - "name": "batteries", + "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", - "name": "Qq", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", - "name": "aesop", + "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a96aee5245720f588876021b6a0aa73efee49c76", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.41", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", - "name": "Cli", + "scope": "leanprover-community", + "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", - "name": "importGraph", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71", - "name": "mathlib", + "scope": "leanprover-community", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}], + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "base", "lakeDir": ".lake"} diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean deleted file mode 100644 index 21a4a3325..000000000 --- a/backends/lean/lakefile.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Lake -open Lake DSL - --- Important: mathlib imports std4 and quote4: we mustn't add a `require std4` line -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" - -package «base» {} - -@[default_target] -lean_lib «Base» {} diff --git a/backends/lean/lakefile.toml b/backends/lean/lakefile.toml new file mode 100644 index 000000000..0794cba13 --- /dev/null +++ b/backends/lean/lakefile.toml @@ -0,0 +1,10 @@ +name = "base" +defaultTargets = ["Base"] + +[[lean_lib]] +name = "Base" + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "v4.15.0" \ No newline at end of file diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain index e7a4f40b8..f8e93dad4 100644 --- a/backends/lean/lean-toolchain +++ b/backends/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0-rc2 +leanprover/lean4:v4.15.0 \ No newline at end of file From eb115a81e8441f5674c8756a8d5577869b6c62b4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Jan 2025 15:06:29 +0000 Subject: [PATCH 2/5] Start updating the Lean tests --- backends/lean/lakefile.lean | 11 +++ backends/lean/lakefile.toml | 10 -- backends/lean/lean-toolchain | 2 +- .../{misc => }/MutuallyRecursiveTraits.lean | 0 tests/lean/lake-manifest.json | 96 +++++++++++-------- tests/lean/lakefile.lean | 14 ++- tests/lean/lean-toolchain | 2 +- tests/src/mutually-recursive-traits.rs | 1 - 8 files changed, 84 insertions(+), 52 deletions(-) create mode 100644 backends/lean/lakefile.lean delete mode 100644 backends/lean/lakefile.toml rename tests/lean/{misc => }/MutuallyRecursiveTraits.lean (100%) diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean new file mode 100644 index 000000000..a1dbfd713 --- /dev/null +++ b/backends/lean/lakefile.lean @@ -0,0 +1,11 @@ +import Lake +open Lake DSL + +-- Important: mathlib imports std4 and quote4: we mustn't add a `require std4` line +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0" + +package «base» {} + +@[default_target] +lean_lib «Base» {} diff --git a/backends/lean/lakefile.toml b/backends/lean/lakefile.toml deleted file mode 100644 index 0794cba13..000000000 --- a/backends/lean/lakefile.toml +++ /dev/null @@ -1,10 +0,0 @@ -name = "base" -defaultTargets = ["Base"] - -[[lean_lib]] -name = "Base" - -[[require]] -name = "mathlib" -git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.15.0" \ No newline at end of file diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain index f8e93dad4..d0eb99ff6 100644 --- a/backends/lean/lean-toolchain +++ b/backends/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 \ No newline at end of file +leanprover/lean4:v4.15.0 diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/MutuallyRecursiveTraits.lean similarity index 100% rename from tests/lean/misc/MutuallyRecursiveTraits.lean rename to tests/lean/MutuallyRecursiveTraits.lean diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json index d6c3c7a09..0ef9a9bc3 100644 --- a/tests/lean/lake-manifest.json +++ b/tests/lean/lake-manifest.json @@ -1,82 +1,102 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"type": "path", + "scope": "", + "name": "base", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./../../backends/lean", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53", - "name": "batteries", + "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", - "name": "Qq", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", - "name": "aesop", + "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a96aee5245720f588876021b6a0aa73efee49c76", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.41", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", - "name": "Cli", + "scope": "leanprover-community", + "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", - "name": "importGraph", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71", - "name": "mathlib", + "scope": "leanprover-community", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, - {"type": "path", - "scope": "", - "name": "base", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "./../../backends/lean", - "configFile": "lakefile.lean"}], + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "tests", "lakeDir": ".lake"} diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index 7197dd2e3..64aba9dbd 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -2,23 +2,35 @@ import Lake open Lake DSL require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0" require base from "../../backends/lean" package «tests» {} @[default_target] lean_lib Arrays +@[default_target] lean_lib AdtBorrows @[default_target] lean_lib Avl @[default_target] lean_lib BaseTutorial @[default_target] lean_lib Betree +@[default_target] lean_lib Bitwise +@[default_target] lean_lib Builtin @[default_target] lean_lib Constants @[default_target] lean_lib Demo @[default_target] lean_lib External @[default_target] lean_lib Hashmap +@[default_target] lean_lib InfiniteLoop +@[default_target] lean_lib Issue194RecursiveStructProjector +@[default_target] lean_lib Issue270LoopList @[default_target] lean_lib Loops +@[default_target] lean_lib Matches +@[default_target] lean_lib MiniTree +@[default_target] lean_lib MutuallyRecursiveTraits @[default_target] lean_lib NoNestedBorrows @[default_target] lean_lib Paper @[default_target] lean_lib PoloniusList +@[default_target] lean_lib RenameAttribute +@[default_target] lean_lib Scalars @[default_target] lean_lib Traits @[default_target] lean_lib Tutorial +@[default_target] lean_lib Vec diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain index e7a4f40b8..d0eb99ff6 100644 --- a/tests/lean/lean-toolchain +++ b/tests/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0-rc2 +leanprover/lean4:v4.15.0 diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs index 9bc4ca63f..476760f18 100644 --- a/tests/src/mutually-recursive-traits.rs +++ b/tests/src/mutually-recursive-traits.rs @@ -1,6 +1,5 @@ //@ [lean] known-failure //@ [!lean] skip -//@ [lean] subdir=misc pub trait Trait1 { type T: Trait2; } From 5ed12f8e15cfbf6540264f05edc0395d3de6a7c1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 17 Jan 2025 10:50:01 +0000 Subject: [PATCH 3/5] Make progress updating the Lean tests --- backends/lean/Base/Arith/Int.lean | 2 +- backends/lean/Base/Diverge/Elab.lean | 7 ++- src/extract/ExtractTypes.ml | 7 +-- tests/lean/Avl/Properties.lean | 47 ++++++++++---------- tests/lean/Avl/Types.lean | 4 -- tests/lean/Hashmap/Properties.lean | 30 ++++++------- tests/lean/{Matches.lean => SwitchTest.lean} | 0 tests/src/{matches.rs => switch_test.rs} | 0 8 files changed, 47 insertions(+), 50 deletions(-) rename tests/lean/{Matches.lean => SwitchTest.lean} (100%) rename tests/src/{matches.rs => switch_test.rs} (100%) diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index cdb17fa09..b7a59f570 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -194,7 +194,7 @@ def intTac (tacName : String) (splitAllDisjs splitGoalConjs : Bool) -/ Utils.tryTac ( -- TODO: is there a simproc to simplify propositional logic? - Utils.simpAll {failIfUnchanged := false, maxSteps := 75} true [``reduceIte] [] + Utils.simpAll {failIfUnchanged := false, maxSteps := 1000} true [``reduceIte] [] [``and_self, ``false_implies, ``true_implies, ``Prod.mk.injEq, ``not_false_eq_true, ``not_true_eq_false, ``true_and, ``and_true, ``false_and, ``and_false, diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index 11ce74cd1..bac3bef00 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -666,7 +666,7 @@ partial def proveExprIsValid (k_var kk_var : Expr) (e : Expr) : MetaM Expr := do pure e else pure e match e with - | .const _ _ => throwError "Unimplemented" -- Shouldn't get there? + | .const _ _ => proveNoKExprIsValid k_var e | .bvar _ | .fvar _ | .lit _ @@ -1699,8 +1699,11 @@ namespace Tests #check infinite_loop.unfold - -- Testing a degenerate case + -- Another degenerate case + def infinite_loop1_call : Result Unit := Result.ok () divergent def infinite_loop1 : Result Unit := + do + infinite_loop1_call infinite_loop1 #check infinite_loop1.unfold diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index 3a73c55c6..a8f1b662f 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -1829,9 +1829,10 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) if backend () = Lean then ( (* Box for the attributes *) F.pp_open_vbox fmt 0; - (* Annotate the projectors with both simp and reducible. - The first one allows to automatically unfold when calling simp in proofs. - The second ensures that projectors will interact well with the unifier *) + (* We used to annotate the projectors as reducible but it would + cause issues. Today we only mark the simp lemmas as reducible. + The consequence is that projectors won't interact well with the unifier. + *) F.pp_print_string fmt "@[reducible]"; F.pp_print_break fmt 0 0; (* Close box for the attributes *) diff --git a/tests/lean/Avl/Properties.lean b/tests/lean/Avl/Properties.lean index 3ee18f16d..e933a2a41 100644 --- a/tests/lean/Avl/Properties.lean +++ b/tests/lean/Avl/Properties.lean @@ -6,6 +6,9 @@ namespace avl open Primitives Result +-- This rewriting lemma is problematic below +attribute [-simp] Bool.exists_bool + -- TODO: move @[simp] def Option.allP {α : Type u} (p : α → Prop) (x : Option α) : Prop := @@ -18,7 +21,7 @@ abbrev Subtree (T : Type) := Option (Node T) mutual @[simp] def Node.height: Node T -> Nat -| Node.mk y left right _ => 1 + max (Subtree.height left) (Subtree.height right) +| Node.mk _ left right _ => 1 + max (Subtree.height left) (Subtree.height right) @[simp] def Subtree.height: Subtree T -> Nat @@ -29,7 +32,7 @@ end mutual @[simp] def Node.size: Node T -> Nat -| Node.mk y left right _ => 1 + Subtree.size left + Subtree.size right +| Node.mk _ left right _ => 1 + Subtree.size left + Subtree.size right @[simp] def Subtree.size: Subtree T -> Nat @@ -300,7 +303,7 @@ theorem Node.rotate_left_spec cases hIn . rename _ => hIn cases hIn - . simp [*] + . simp_all (config := {maxDischargeDepth := 1}) . -- Proving: y ∈ a → y < z -- Using: y < x ∧ x < z rename _ => hIn @@ -579,9 +582,9 @@ theorem Node.rotate_left_right_spec . -- invAux for y split_conjs <;> (try omega) <;> (try tauto) . -- invAux for z - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- invAux for x - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- The sets are the same apply Set.ext; simp [tree, z_tree, y_tree]; tauto . -- Height @@ -594,9 +597,9 @@ theorem Node.rotate_left_right_spec . -- invAux for y split_conjs <;> (try omega) <;> (try tauto) . -- invAux for z - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- invAux for x - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- The sets are the same apply Set.ext; simp [tree, z_tree, y_tree]; tauto . -- Height @@ -607,9 +610,9 @@ theorem Node.rotate_left_right_spec . -- invAux for y split_conjs <;> (try omega) <;> (try tauto) . -- invAux for z - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- invAux for x - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- The sets are the same apply Set.ext; simp [tree, z_tree, y_tree]; tauto . -- Height @@ -704,9 +707,9 @@ theorem Node.rotate_right_left_spec . -- invAux for y split_conjs <;> (try omega) <;> (try tauto) . -- invAux for z - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- invAux for x - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- The sets are the same apply Set.ext; simp [tree, z_tree, y_tree]; tauto . -- Height @@ -719,9 +722,9 @@ theorem Node.rotate_right_left_spec . -- invAux for y split_conjs <;> (try omega) <;> (try tauto) . -- invAux for z - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- invAux for x - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- The sets are the same apply Set.ext; simp [tree, z_tree, y_tree]; tauto . -- Height @@ -732,17 +735,14 @@ theorem Node.rotate_right_left_spec . -- invAux for y split_conjs <;> (try omega) <;> (try tauto) . -- invAux for z - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- invAux for x - split_conjs <;> (try scalar_tac) <;> tauto + split_conjs <;> (try scalar_tac) . -- The sets are the same apply Set.ext; simp [tree, z_tree, y_tree]; tauto . -- Height scalar_tac --- This rewriting lemma is problematic below -attribute [-simp] Bool.exists_bool - -- For the proofs of termination @[simp] theorem Node.left_height_lt_height (n : Node T) : @@ -796,9 +796,7 @@ theorem Tree.insert_in_opt_node_spec rw [Tree.insert_in_opt_node] cases hNode : tree <;> simp [hNode] . -- tree = none - split_conjs - . simp [Node.invAux, Node.balanceFactor] - . simp [Subtree.inv] + simp [Node.invAux, Node.balanceFactor] . -- tree = some rename Node T => node have hNodeInv : Node.inv node := by simp_all (config := {maxDischargeDepth := 1}) @@ -847,6 +845,7 @@ theorem Node.insert_in_left_spec . simp_all (config := {maxDischargeDepth := 1}) . simp_all (config := {maxDischargeDepth := 1}) [Node.inv, Node.invAux, Node.invAuxNotBalanced, Node.balanceFactor] scalar_tac + . simp_all (config := {maxDischargeDepth := 1}) [Node.invAux, Node.balanceFactor] . -- End of the proof simp [*] split_conjs @@ -946,6 +945,7 @@ theorem Node.insert_in_right_spec . simp_all (config := {maxDischargeDepth := 1}) . simp_all (config := {maxDischargeDepth := 1}) . simp_all (config := {maxDischargeDepth := 1}) [Node.inv, Node.invAux, Node.invAuxNotBalanced, Node.balanceFactor]; scalar_tac + . simp_all (config := {maxDischargeDepth := 1}) [Node.invAux, Node.balanceFactor] . -- End of the proof simp [*] split_conjs @@ -953,9 +953,8 @@ theorem Node.insert_in_right_spec simp_all (config := {maxDischargeDepth := 1}) . -- height simp_all (config := {maxDischargeDepth := 1}) [Node.invAux, Node.balanceFactor] - -- This assertion is not necessary for the proof, but it is important that it holds. - -- We can prove it because of the post-conditions `b → node'.balanceFactor ≠ 0` (see above) - have : bf_z.val = 1 := by scalar_tac + -- Remark: here we have: + -- bf_z.val = -1 scalar_tac . -- rotate_right_left cases node with | mk x t1 right balance_factor => diff --git a/tests/lean/Avl/Types.lean b/tests/lean/Avl/Types.lean index aa65c9bdb..0e78741ee 100644 --- a/tests/lean/Avl/Types.lean +++ b/tests/lean/Avl/Types.lean @@ -25,19 +25,15 @@ structure Ord (Self : Type) where inductive Node (T : Type) := | mk : T → Option (Node T) → Option (Node T) → I8 → Node T -@[reducible] def Node.value {T : Type} (x : Node T) := match x with | Node.mk x1 _ _ _ => x1 -@[reducible] def Node.left {T : Type} (x : Node T) := match x with | Node.mk _ x1 _ _ => x1 -@[reducible] def Node.right {T : Type} (x : Node T) := match x with | Node.mk _ _ x1 _ => x1 -@[reducible] def Node.balance_factor {T : Type} (x : Node T) := match x with | Node.mk _ _ _ x1 => x1 diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index cfdc1b5a1..9edccf31c 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -104,7 +104,7 @@ def lookup (hm : HashMap α) (k : Usize) : Option α := abbrev len_s (hm : HashMap α) : Nat := hm.al_v.length instance : Membership Usize (HashMap α) where - mem k hm := hm.lookup k ≠ none + mem (hm : HashMap α) k := hm.lookup k ≠ none /- Activate the ↑ notation -/ attribute [coe] HashMap.v @@ -141,6 +141,9 @@ def frame_load (hm nhm : HashMap α) : Prop := -- This rewriting lemma is problematic below attribute [-simp] Bool.exists_bool +-- These simp lemmas were introduced by upstream changes and are problematic +attribute [-simp] List.length_flatten List.flatten_eq_nil_iff List.lookup_eq_none_iff + attribute [local simp] List.lookup /- Adding some theorems for `scalar_tac` -/ @@ -398,7 +401,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value simp [*] have hbounds : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by simp [lookup] at hnsat - simp_all (config := {maxDischargeDepth := 1}) + simp_all (config := {maxDischargeDepth := 1}) [] scalar_tac progress as ⟨ z, hp ⟩ simp [hp] @@ -499,8 +502,6 @@ theorem move_elements_from_list_spec have hLookupKey : ntable.lookup key = none := by by_contra cases h: ntable.lookup key <;> simp_all (config := {maxDischargeDepth := 1}) - have h := hDisjoint1 _ _ h - simp_all (config := {maxDischargeDepth := 1}) have : ntable.lookup key = none → ntable.len_s < Usize.max := by simp_all (config := {maxDischargeDepth := 1}); scalar_tac progress as ⟨ ntable1, _, _, hLookup11, hLookup12, hLength1 ⟩ simp [hLookupKey] at hLength1 @@ -733,8 +734,8 @@ theorem move_elements_loop_spec := by rw [move_elements_loop] simp - if hi: i.val < slots.val.length then - -- Continue the proof + dcases hi: i.val < slots.val.length + . -- Continue the proof have hIneq : 0 ≤ i.val ∧ i.val < slots.val.length := by scalar_tac simp [hi] progress as ⟨ slot, hSlotEq ⟩ @@ -752,8 +753,6 @@ theorem move_elements_loop_spec have := slots_inv_lookup_imp_eq slots hSlotsInv i.toNat (by scalar_tac) key simp_all (config := {maxDischargeDepth := 1}) cases h: slot.lookup key <;> simp_all (config := {maxDischargeDepth := 1}) - have := hDisjoint2 _ _ h - simp_all (config := {maxDischargeDepth := 1}) have : ntable.al_v.length + slot.v.length ≤ Usize.max := by have := slots_index_len_le_flatten_len slots.val i.toNat (by scalar_tac) @@ -762,8 +761,6 @@ theorem move_elements_loop_spec . intro key v hLookup by_contra cases h : ntable.lookup key <;> simp_all (config := {maxDischargeDepth := 1}) - have := ntableLookupImpSlot _ _ h - simp_all (config := {maxDischargeDepth := 1}) progress as ⟨ i' ⟩ have : i' ≤ alloc.vec.Vec.len (alloc.vec.Vec.update slots i Nil) := by @@ -800,8 +797,6 @@ theorem move_elements_loop_spec . intro key v hLookup by_contra h cases h : ntable1.lookup key <;> simp_all (config := {maxDischargeDepth := 1}) - have := ntable1LookupImpSlots1 _ _ h - simp_all (config := {maxDischargeDepth := 1}) . have : i.val < (List.map AList.v slots.val).length := by simp; scalar_tac simp_all (config := {maxDischargeDepth := 2}) [Slots.al_v, List.length_flatten_update_eq, List.map_update_eq, List.length_flatten_update_as_int_eq] scalar_tac @@ -831,8 +826,7 @@ theorem move_elements_loop_spec . apply hLookupPreserve.right . intro j h0 apply hIndexNil j h0 - else - simp [hi, *] + . simp [hi, *] -- TODO: simp_all (config := {maxDischargeDepth := 1}) removes hEmpty!! have hi : i = alloc.vec.Vec.len slots := by scalar_tac have hEmpty : ∀ (j : Nat), j < slots.val.length → slots.val.index j = AList.Nil := by @@ -842,7 +836,12 @@ theorem move_elements_loop_spec have hLenNonZero : slots.val.length ≠ 0 := by simp [*] have hLookupEmpty := slots_forall_nil_imp_lookup_none slots hLenNonZero hEmpty simp [hNil, hLookupEmpty, frame_slots_params] - apply hEmpty + split_conjs + . intros + simp [*] + . intros + simp_all + . apply hEmpty termination_by (slots.val.length - i.val).toNat decreasing_by scalar_decr_tac -- TODO: this is expensive @@ -1082,7 +1081,6 @@ theorem get_mut_spec {α} (hm : HashMap α) (key : Usize) (hInv : hm.inv) : replace hBackSome := hBackSome v v' (by simp) have ⟨ _, _, _, _ ⟩ := hBackSome clear hBackSome - simp [*] intro key' hNotEq -- TODO: simplify have : 0 ≤ key'.val % hm.slots.val.length ∧ key'.val % hm.slots.val.length < hm.slots.val.length := by scalar_tac diff --git a/tests/lean/Matches.lean b/tests/lean/SwitchTest.lean similarity index 100% rename from tests/lean/Matches.lean rename to tests/lean/SwitchTest.lean diff --git a/tests/src/matches.rs b/tests/src/switch_test.rs similarity index 100% rename from tests/src/matches.rs rename to tests/src/switch_test.rs From 25e2d429b2932defeaabc64b26d32b25bc42d3ce Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 17 Jan 2025 11:18:48 +0000 Subject: [PATCH 4/5] Finish fixing the Lean tests --- backends/lean/Base/Primitives/Scalar.lean | 4 +- src/extract/ExtractBuiltin.ml | 51 +++++++++---------- src/extract/ExtractTypes.ml | 20 ++------ tests/lean/AdtBorrows.lean | 6 +-- tests/lean/Arrays.lean | 2 +- tests/lean/Avl/Types.lean | 13 ++--- tests/lean/Betree/Types.lean | 14 ++--- tests/lean/Bst/Types.lean | 16 ++---- tests/lean/Demo/Demo.lean | 2 +- tests/lean/Hashmap/Types.lean | 2 +- .../Issue194RecursiveStructProjector.lean | 5 +- tests/lean/Issue270LoopList.lean | 2 +- tests/lean/Loops.lean | 2 +- tests/lean/MiniTree.lean | 3 +- tests/lean/NoNestedBorrows.lean | 14 ++--- tests/lean/Paper.lean | 2 +- tests/lean/PoloniusList.lean | 2 +- tests/lean/RenameAttribute.lean | 2 +- tests/lean/Scalars.lean | 8 +-- tests/lean/SwitchTest.lean | 10 ++-- tests/lean/Tutorial/Tutorial.lean | 2 +- tests/lean/lakefile.lean | 2 +- tests/src/scalars.rs | 16 +++--- 23 files changed, 84 insertions(+), 116 deletions(-) diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index de8176b73..60f1caa42 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1356,7 +1356,7 @@ theorem core.num.Usize.saturating_sub_spec (x y : Usize) : split <;> split <;> split <;> scalar_tac -- Wrapping add -def Scalar.wrapping_add {ty} (x y : Scalar ty) : Result (Scalar ty) := sorry +def Scalar.wrapping_add {ty} (x y : Scalar ty) : Scalar ty := sorry /- [core::num::{u8}::wrapping_add] -/ def core.num.U8.wrapping_add := @Scalar.wrapping_add ScalarTy.U8 @@ -1396,7 +1396,7 @@ def core.num.Isize.wrapping_add := @Scalar.wrapping_add ScalarTy.Isize -- TODO: reasoning lemmas for wrapping add -- Wrapping sub -def Scalar.wrapping_sub {ty} (x y : Scalar ty) : Result (Scalar ty) := sorry +def Scalar.wrapping_sub {ty} (x y : Scalar ty) : Scalar ty := sorry /- [core::num::{u8}::wrapping_sub] -/ def core.num.U8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U8 diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index 1c12cfd11..5fd6ee644 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -446,23 +446,6 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = mk_fun "core::option::{core::option::Option<@T>}::unwrap" ~extract_name:(Some "core.option.Option.unwrap") (); ] - @ List.flatten - (List.map - (fun int_name -> - List.map - (fun op -> - mk_fun - ("core::num::" ^ "{" ^ int_name ^ "}::" ^ op) - ~can_fail:false ()) - [ - "saturating_add"; - "saturating_sub"; - "wrapping_add"; - "wrapping_sub"; - "rotate_left"; - "rotate_right"; - ]) - all_int_names) @ List.flatten (List.map (fun op -> @@ -569,17 +552,29 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = ~filter:(Some [ true; false ]) (); ] - @ List.map - (fun ty -> - mk_fun - ("core::num::{" ^ ty ^ "}::overflowing_add") - ~extract_name: - (Some - ("core.num." - ^ StringUtils.capitalize_first_letter ty - ^ ".overflowing_add")) - ()) - all_int_names) + @ List.flatten + (List.map + (fun int_name -> + List.map + (fun (can_fail, op) -> + mk_fun + ("core::num::" ^ "{" ^ int_name ^ "}::" ^ op) + ~extract_name: + (Some + ("core.num." + ^ StringUtils.capitalize_first_letter int_name + ^ "." ^ op)) + ~can_fail ()) + [ + (false, "saturating_add"); + (false, "saturating_sub"); + (false, "wrapping_add"); + (false, "wrapping_sub"); + (true, "overflowing_add"); + (false, "rotate_left"); + (false, "rotate_right"); + ]) + all_int_names)) let builtin_funs : unit -> (pattern * bool list option * builtin_fun_info) list = diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index a8f1b662f..8b6a73691 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -1571,9 +1571,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) type (and not a product between, say, integers) we need to help Coq a bit *) if is_tuple_struct then ": Type :=" else ":=" - | Lean -> - if type_kind = Some Struct && kind = SingleNonRec then "where" - else ":=" + | Lean -> if is_tuple_struct then ":=" else "where" | HOL4 -> "=" in F.pp_print_string fmt eq) @@ -1825,18 +1823,10 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (* Inner box for the projector definition *) F.pp_open_hvbox fmt ctx.indent_incr; - (* For Lean: add some attributes *) - if backend () = Lean then ( - (* Box for the attributes *) - F.pp_open_vbox fmt 0; - (* We used to annotate the projectors as reducible but it would - cause issues. Today we only mark the simp lemmas as reducible. - The consequence is that projectors won't interact well with the unifier. - *) - F.pp_print_string fmt "@[reducible]"; - F.pp_print_break fmt 0 0; - (* Close box for the attributes *) - F.pp_close_box fmt ()); + (* For Lean: we used to mark the projectors as reducible but it would + cause issues with the simplifier, probably because of the simp + lemmas. The consequence is that projectors won't interact well with + the unifier, but it shouldn't be an issue in practice. *) (* Box for the [def ADT.proj ... :=] *) F.pp_open_hovbox fmt ctx.indent_incr; diff --git a/tests/lean/AdtBorrows.lean b/tests/lean/AdtBorrows.lean index 3d84aaeb5..964bcb865 100644 --- a/tests/lean/AdtBorrows.lean +++ b/tests/lean/AdtBorrows.lean @@ -304,7 +304,7 @@ def use_boxed_slice_mut_borrow2 /- [adt_borrows::SharedList] Source: 'tests/src/adt-borrows.rs', lines 207:0-210:1 -/ -inductive SharedList (T : Type) := +inductive SharedList (T : Type) where | Nil : SharedList T | Cons : T → SharedList T → SharedList T @@ -324,7 +324,7 @@ def SharedList.pop /- [adt_borrows::MutList] Source: 'tests/src/adt-borrows.rs', lines 227:0-230:1 -/ -inductive MutList (T : Type) := +inductive MutList (T : Type) where | Nil : MutList T | Cons : T → MutList T → MutList T @@ -372,7 +372,7 @@ def wrap_mut_in_option /- [adt_borrows::List] Source: 'tests/src/adt-borrows.rs', lines 255:0-258:1 -/ -inductive List (T : Type) := +inductive List (T : Type) where | Cons : T → List T → List T | Nil : List T diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index f326efa6e..954e751e8 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -10,7 +10,7 @@ namespace arrays /- [arrays::AB] Source: 'tests/src/arrays.rs', lines 6:0-9:1 -/ -inductive AB := +inductive AB where | A : AB | B : AB diff --git a/tests/lean/Avl/Types.lean b/tests/lean/Avl/Types.lean index 0e78741ee..469a424e2 100644 --- a/tests/lean/Avl/Types.lean +++ b/tests/lean/Avl/Types.lean @@ -10,7 +10,7 @@ namespace avl /- [avl::Ordering] Source: 'src/avl.rs', lines 19:0-23:1 -/ -inductive Ordering := +inductive Ordering where | Less : Ordering | Equal : Ordering | Greater : Ordering @@ -22,17 +22,14 @@ structure Ord (Self : Type) where /- [avl::Node] Source: 'src/avl.rs', lines 29:0-34:1 -/ -inductive Node (T : Type) := +inductive Node (T : Type) where | mk : T → Option (Node T) → Option (Node T) → I8 → Node T -def Node.value {T : Type} (x : Node T) := - match x with | Node.mk x1 _ _ _ => x1 +def Node.value {T : Type} (x : Node T) := match x with | Node.mk x1 _ _ _ => x1 -def Node.left {T : Type} (x : Node T) := - match x with | Node.mk _ x1 _ _ => x1 +def Node.left {T : Type} (x : Node T) := match x with | Node.mk _ x1 _ _ => x1 -def Node.right {T : Type} (x : Node T) := - match x with | Node.mk _ _ x1 _ => x1 +def Node.right {T : Type} (x : Node T) := match x with | Node.mk _ _ x1 _ => x1 def Node.balance_factor {T : Type} (x : Node T) := match x with | Node.mk _ _ _ x1 => x1 diff --git a/tests/lean/Betree/Types.lean b/tests/lean/Betree/Types.lean index 1075d1401..6606d38d2 100644 --- a/tests/lean/Betree/Types.lean +++ b/tests/lean/Betree/Types.lean @@ -11,19 +11,19 @@ namespace betree /- [betree::betree::List] Source: 'src/betree.rs', lines 17:0-20:1 -/ -inductive betree.List (T : Type) := +inductive betree.List (T : Type) where | Cons : T → betree.List T → betree.List T | Nil : betree.List T /- [betree::betree::UpsertFunState] Source: 'src/betree.rs', lines 63:0-66:1 -/ -inductive betree.UpsertFunState := +inductive betree.UpsertFunState where | Add : U64 → betree.UpsertFunState | Sub : U64 → betree.UpsertFunState /- [betree::betree::Message] Source: 'src/betree.rs', lines 69:0-117:1 -/ -inductive betree.Message := +inductive betree.Message where | Insert : U64 → betree.Message | Delete : betree.Message | Upsert : betree.UpsertFunState → betree.Message @@ -38,30 +38,26 @@ mutual /- [betree::betree::Internal] Source: 'src/betree.rs', lines 156:0-161:1 -/ -inductive betree.Internal := +inductive betree.Internal where | mk : U64 → U64 → betree.Node → betree.Node → betree.Internal /- [betree::betree::Node] Source: 'src/betree.rs', lines 179:0-184:1 -/ -inductive betree.Node := +inductive betree.Node where | Internal : betree.Internal → betree.Node | Leaf : betree.Leaf → betree.Node end -@[reducible] def betree.Internal.id (x : betree.Internal) := match x with | betree.Internal.mk x1 _ _ _ => x1 -@[reducible] def betree.Internal.pivot (x : betree.Internal) := match x with | betree.Internal.mk _ x1 _ _ => x1 -@[reducible] def betree.Internal.left (x : betree.Internal) := match x with | betree.Internal.mk _ _ x1 _ => x1 -@[reducible] def betree.Internal.right (x : betree.Internal) := match x with | betree.Internal.mk _ _ _ x1 => x1 diff --git a/tests/lean/Bst/Types.lean b/tests/lean/Bst/Types.lean index 9e0b8f710..65f7a6b49 100644 --- a/tests/lean/Bst/Types.lean +++ b/tests/lean/Bst/Types.lean @@ -10,7 +10,7 @@ namespace bst /- [bst::Ordering] Source: 'src/bst.rs', lines 5:0-9:1 -/ -inductive Ordering := +inductive Ordering where | Less : Ordering | Equal : Ordering | Greater : Ordering @@ -22,20 +22,14 @@ structure Ord (Self : Type) where /- [bst::Node] Source: 'src/bst.rs', lines 15:0-19:1 -/ -inductive Node (T : Type) := +inductive Node (T : Type) where | mk : T → Option (Node T) → Option (Node T) → Node T -@[reducible] -def Node.value {T : Type} (x : Node T) := - match x with | Node.mk x1 _ _ => x1 +def Node.value {T : Type} (x : Node T) := match x with | Node.mk x1 _ _ => x1 -@[reducible] -def Node.left {T : Type} (x : Node T) := - match x with | Node.mk _ x1 _ => x1 +def Node.left {T : Type} (x : Node T) := match x with | Node.mk _ x1 _ => x1 -@[reducible] -def Node.right {T : Type} (x : Node T) := - match x with | Node.mk _ _ x1 => x1 +def Node.right {T : Type} (x : Node T) := match x with | Node.mk _ _ x1 => x1 @[simp] theorem Node.value._simpLemma_ {T : Type} (value : T) (left : Option (Node T)) diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index d4cf6a820..8dadd2890 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -48,7 +48,7 @@ def use_incr : Result Unit := /- [demo::CList] Source: 'tests/src/demo.rs', lines 36:0-39:1 -/ -inductive CList (T : Type) := +inductive CList (T : Type) where | CCons : T → CList T → CList T | CNil : CList T diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 026bf798b..1ca632d2c 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -11,7 +11,7 @@ namespace hashmap /- [hashmap::AList] Source: 'tests/src/hashmap.rs', lines 30:0-33:1 -/ -inductive AList (T : Type) := +inductive AList (T : Type) where | Cons : Usize → T → AList T → AList T | Nil : AList T diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean index 06694b446..c858a5397 100644 --- a/tests/lean/Issue194RecursiveStructProjector.lean +++ b/tests/lean/Issue194RecursiveStructProjector.lean @@ -10,18 +10,15 @@ namespace issue_194_recursive_struct_projector /- [issue_194_recursive_struct_projector::AVLNode] Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-6:1 -/ -inductive AVLNode (T : Type) := +inductive AVLNode (T : Type) where | mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T -@[reducible] def AVLNode.value {T : Type} (x : AVLNode T) := match x with | AVLNode.mk x1 _ _ => x1 -@[reducible] def AVLNode.left {T : Type} (x : AVLNode T) := match x with | AVLNode.mk _ x1 _ => x1 -@[reducible] def AVLNode.right {T : Type} (x : AVLNode T) := match x with | AVLNode.mk _ _ x1 => x1 diff --git a/tests/lean/Issue270LoopList.lean b/tests/lean/Issue270LoopList.lean index 5c3d5419d..1d1170cd2 100644 --- a/tests/lean/Issue270LoopList.lean +++ b/tests/lean/Issue270LoopList.lean @@ -10,7 +10,7 @@ namespace issue_270_loop_list /- [issue_270_loop_list::List] Source: 'tests/src/issue-270-loop-list.rs', lines 2:0-5:1 -/ -inductive List (T : Type) := +inductive List (T : Type) where | Cons : T → List T → List T | Nil : List T diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index dd0380702..3ca247634 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -98,7 +98,7 @@ def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := /- [loops::List] Source: 'tests/src/loops.rs', lines 74:0-77:1 -/ -inductive List (T : Type) := +inductive List (T : Type) where | Cons : T → List T → List T | Nil : List T diff --git a/tests/lean/MiniTree.lean b/tests/lean/MiniTree.lean index bba4af74b..803497c50 100644 --- a/tests/lean/MiniTree.lean +++ b/tests/lean/MiniTree.lean @@ -10,10 +10,9 @@ namespace mini_tree /- [mini_tree::Node] Source: 'tests/src/mini_tree.rs', lines 3:0-5:1 -/ -inductive Node := +inductive Node where | mk : Option Node → Node -@[reducible] def Node.child (x : Node) := match x with | Node.mk x1 => x1 @[simp] diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 2319c3ad8..0eccbcb42 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -16,23 +16,23 @@ structure Pair (T1 : Type) (T2 : Type) where /- [no_nested_borrows::List] Source: 'tests/src/no_nested_borrows.rs', lines 12:0-15:1 -/ -inductive List (T : Type) := +inductive List (T : Type) where | Cons : T → List T → List T | Nil : List T /- [no_nested_borrows::One] Source: 'tests/src/no_nested_borrows.rs', lines 23:0-25:1 -/ -inductive One (T1 : Type) := +inductive One (T1 : Type) where | One : T1 → One T1 /- [no_nested_borrows::EmptyEnum] Source: 'tests/src/no_nested_borrows.rs', lines 29:0-31:1 -/ -inductive EmptyEnum := +inductive EmptyEnum where | Empty : EmptyEnum /- [no_nested_borrows::Enum] Source: 'tests/src/no_nested_borrows.rs', lines 35:0-38:1 -/ -inductive Enum := +inductive Enum where | Variant1 : Enum | Variant2 : Enum @@ -42,7 +42,7 @@ inductive Enum := /- [no_nested_borrows::Sum] Source: 'tests/src/no_nested_borrows.rs', lines 44:0-47:1 -/ -inductive Sum (T1 : Type) (T2 : Type) := +inductive Sum (T1 : Type) (T2 : Type) where | Left : T1 → Sum T1 T2 | Right : T2 → Sum T1 T2 @@ -243,13 +243,13 @@ mutual /- [no_nested_borrows::Tree] Source: 'tests/src/no_nested_borrows.rs', lines 232:0-235:1 -/ -inductive Tree (T : Type) := +inductive Tree (T : Type) where | Leaf : T → Tree T | Node : T → NodeElem T → Tree T → Tree T /- [no_nested_borrows::NodeElem] Source: 'tests/src/no_nested_borrows.rs', lines 237:0-240:1 -/ -inductive NodeElem (T : Type) := +inductive NodeElem (T : Type) where | Cons : Tree T → NodeElem T → NodeElem T | Nil : NodeElem T diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 112c2acaf..f5808aa91 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -49,7 +49,7 @@ def test_choose : Result Unit := /- [paper::List] Source: 'tests/src/paper.rs', lines 38:0-41:1 -/ -inductive List (T : Type) := +inductive List (T : Type) where | Cons : T → List T → List T | Nil : List T diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index 4c9c06b28..eb7789e80 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -10,7 +10,7 @@ namespace polonius_list /- [polonius_list::List] Source: 'tests/src/polonius_list.rs', lines 6:0-9:1 -/ -inductive List (T : Type) := +inductive List (T : Type) where | Cons : T → List T → List T | Nil : List T diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean index ff7b746ab..e336523da 100644 --- a/tests/lean/RenameAttribute.lean +++ b/tests/lean/RenameAttribute.lean @@ -42,7 +42,7 @@ def BoolFn (T : Type) (x : Bool) : Result Bool := /- [rename_attribute::SimpleEnum] Source: 'tests/src/rename_attribute.rs', lines 36:0-41:1 -/ -inductive VariantsTest := +inductive VariantsTest where | Variant1 : VariantsTest | SecondVariant : VariantsTest | ThirdVariant : VariantsTest diff --git a/tests/lean/Scalars.lean b/tests/lean/Scalars.lean index b3da5351e..4f714c931 100644 --- a/tests/lean/Scalars.lean +++ b/tests/lean/Scalars.lean @@ -11,22 +11,22 @@ namespace scalars /- [scalars::u32_use_wrapping_add]: Source: 'tests/src/scalars.rs', lines 3:0-5:1 -/ def u32_use_wrapping_add (x : U32) (y : U32) : Result U32 := - Result.ok (core.num.u32.wrapping_add x y) + Result.ok (core.num.U32.wrapping_add x y) /- [scalars::i32_use_wrapping_add]: Source: 'tests/src/scalars.rs', lines 7:0-9:1 -/ def i32_use_wrapping_add (x : I32) (y : I32) : Result I32 := - Result.ok (core.num.i32.wrapping_add x y) + Result.ok (core.num.I32.wrapping_add x y) /- [scalars::u32_use_wrapping_sub]: Source: 'tests/src/scalars.rs', lines 11:0-13:1 -/ def u32_use_wrapping_sub (x : U32) (y : U32) : Result U32 := - Result.ok (core.num.u32.wrapping_sub x y) + Result.ok (core.num.U32.wrapping_sub x y) /- [scalars::i32_use_wrapping_sub]: Source: 'tests/src/scalars.rs', lines 15:0-17:1 -/ def i32_use_wrapping_sub (x : I32) (y : I32) : Result I32 := - Result.ok (core.num.i32.wrapping_sub x y) + Result.ok (core.num.I32.wrapping_sub x y) /- [scalars::u32_use_shift_right]: Source: 'tests/src/scalars.rs', lines 19:0-21:1 -/ diff --git a/tests/lean/SwitchTest.lean b/tests/lean/SwitchTest.lean index 093abf746..b859b9908 100644 --- a/tests/lean/SwitchTest.lean +++ b/tests/lean/SwitchTest.lean @@ -1,19 +1,19 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [matches] +-- [switch_test] import Base open Primitives set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false -namespace matches +namespace switch_test -/- [matches::match_u32]: - Source: 'tests/src/matches.rs', lines 4:0-10:1 -/ +/- [switch_test::match_u32]: + Source: 'tests/src/switch_test.rs', lines 4:0-10:1 -/ def match_u32 (x : U32) : Result U32 := match x with | 0#scalar => Result.ok 0#u32 | 1#scalar => Result.ok 1#u32 | _ => Result.ok 2#u32 -end matches +end switch_test diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean index 663d8e928..bf55bd2b7 100644 --- a/tests/lean/Tutorial/Tutorial.lean +++ b/tests/lean/Tutorial/Tutorial.lean @@ -48,7 +48,7 @@ def use_incr : Result Unit := /- [tutorial::CList] Source: 'src/lib.rs', lines 30:0-33:1 -/ -inductive CList (T : Type) := +inductive CList (T : Type) where | CCons : T → CList T → CList T | CNil : CList T diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index 64aba9dbd..a78c9eaf8 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -23,7 +23,6 @@ package «tests» {} @[default_target] lean_lib Issue194RecursiveStructProjector @[default_target] lean_lib Issue270LoopList @[default_target] lean_lib Loops -@[default_target] lean_lib Matches @[default_target] lean_lib MiniTree @[default_target] lean_lib MutuallyRecursiveTraits @[default_target] lean_lib NoNestedBorrows @@ -31,6 +30,7 @@ package «tests» {} @[default_target] lean_lib PoloniusList @[default_target] lean_lib RenameAttribute @[default_target] lean_lib Scalars +@[default_target] lean_lib SwitchTest @[default_target] lean_lib Traits @[default_target] lean_lib Tutorial @[default_target] lean_lib Vec diff --git a/tests/src/scalars.rs b/tests/src/scalars.rs index 88eb4de28..80d264c3d 100644 --- a/tests/src/scalars.rs +++ b/tests/src/scalars.rs @@ -1,33 +1,33 @@ //@ [coq,fstar,borrow-check] skip -fn u32_use_wrapping_add(x : u32, y : u32) -> u32 { +fn u32_use_wrapping_add(x: u32, y: u32) -> u32 { x.wrapping_add(y) } -fn i32_use_wrapping_add(x : i32, y : i32) -> i32 { +fn i32_use_wrapping_add(x: i32, y: i32) -> i32 { x.wrapping_add(y) } -fn u32_use_wrapping_sub(x : u32, y : u32) -> u32 { +fn u32_use_wrapping_sub(x: u32, y: u32) -> u32 { x.wrapping_sub(y) } -fn i32_use_wrapping_sub(x : i32, y : i32) -> i32 { +fn i32_use_wrapping_sub(x: i32, y: i32) -> i32 { x.wrapping_sub(y) } -fn u32_use_shift_right(x : u32) -> u32 { +fn u32_use_shift_right(x: u32) -> u32 { x >> 2 } -fn i32_use_shift_right(x : i32) -> i32 { +fn i32_use_shift_right(x: i32) -> i32 { x >> 2 } -fn u32_use_shift_left(x : u32) -> u32 { +fn u32_use_shift_left(x: u32) -> u32 { x << 2 } -fn i32_use_shift_left(x : i32) -> i32 { +fn i32_use_shift_left(x: i32) -> i32 { x << 2 } From ee78db1653fdea67e9ba272cd350ba576fead28d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 17 Jan 2025 13:02:53 +0000 Subject: [PATCH 5/5] Commit a forgotten file --- tests/fstar/misc/{Matches.fst => SwitchTest.fst} | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) rename tests/fstar/misc/{Matches.fst => SwitchTest.fst} (63%) diff --git a/tests/fstar/misc/Matches.fst b/tests/fstar/misc/SwitchTest.fst similarity index 63% rename from tests/fstar/misc/Matches.fst rename to tests/fstar/misc/SwitchTest.fst index 1c82f5baa..6a177444e 100644 --- a/tests/fstar/misc/Matches.fst +++ b/tests/fstar/misc/SwitchTest.fst @@ -1,12 +1,12 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [matches] *) -module Matches +(** [switch_test] *) +module SwitchTest open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [matches::match_u32]: - Source: 'tests/src/matches.rs', lines 4:0-10:1 *) +(** [switch_test::match_u32]: + Source: 'tests/src/switch_test.rs', lines 4:0-10:1 *) let match_u32 (x : u32) : result u32 = begin match x with | 0 -> Ok 0 | 1 -> Ok 1 | _ -> Ok 2 end