diff options
Diffstat (limited to 'backends')
-rw-r--r-- | backends/lean/Base/Arith/Int.lean | 2 | ||||
-rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 2 | ||||
-rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 41 | ||||
-rw-r--r-- | backends/lean/Base/Utils.lean | 12 |
4 files changed, 32 insertions, 25 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 48a30a49..7a5bbe98 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -147,7 +147,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) let hs ← collectInstancesFromMainCtx lookup hs.toArray.mapM fun e => do let type ← inferType e - let name ← mkFreshUserName `h + let name ← mkFreshAnonPropUserName -- Add a declaration let nval ← Utils.addDeclTac name e type (asLet := false) -- Simplify to unfold the declaration to unfold (i.e., the projector) diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 6f4a8eba..b792ff21 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -12,7 +12,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do -- Inroduce the bounds for the isize/usize types let add (e : Expr) : Tactic.TacticM Unit := do let ty ← inferType e - let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false) + let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false) add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 4a406bdf..9300edff 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -79,7 +79,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) match th with | .Theorem thName => mkAppOptM thName (mvars.map some) | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some) - let asmName ← do match keep with | none => mkFreshUserName `h | some n => do pure n + let asmName ← do match keep with | none => mkFreshAnonPropUserName | some n => do pure n let thTy ← inferType th let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false) withMainContext do -- The context changed - TODO: remove once addDeclTac is updated @@ -101,8 +101,8 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) let hName := (← h.fvarId!.getDecl).userName let (optIds, ids) ← do match ids with - | [] => do pure (some (hName, ← mkFreshUserName `h), []) - | none :: ids => do pure (some (hName, ← mkFreshUserName `h), ids) + | [] => do pure (some (hName, ← mkFreshAnonPropUserName), []) + | none :: ids => do pure (some (hName, ← mkFreshAnonPropUserName), ids) | some id :: ids => do pure (some (hName, id), ids) splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids) else k h none ids @@ -142,7 +142,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) -- Split let nid ← do match nid with - | none => mkFreshUserName `h + | none => mkFreshAnonPropUserName | some nid => pure nid trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}" if ← isConj (← inferType hPost) then @@ -270,23 +270,26 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL -- Nothing worked: failed throwError "Progress failed" -syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")? +syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")? def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do let args := args.raw -- Process the arguments to retrieve the identifiers to use trace[Progress] "Progress arguments: {args}" - let args := args.getArgs + let (keepArg, withArg, asArgs) ← + match args.getArgs.toList with + | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs) + | _ => throwError "Unexpected: invalid arguments" let keep : Option Name ← do - let args := (args.get! 0).getArgs - if args.size > 0 then do - let args := (args.get! 1).getArgs - if args.size > 0 then pure (some (args.get! 1).getId) - else do pure (some (← mkFreshUserName `h)) - else pure none + let args := keepArg.getArgs + trace[Progress] "Keep args: {args}" + let arg := args.get! 1 + trace[Progress] "Keep arg: {arg}" + if arg.isIdent then pure (some arg.getId) + else do pure (some (← mkFreshAnonPropUserName)) trace[Progress] "Keep: {keep}" let withArg ← do - let withArg := (args.get! 1).getArgs + let withArg := withArg.getArgs if withArg.size > 0 then let id := withArg.get! 1 trace[Progress] "With arg: {id}" @@ -306,12 +309,12 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do pure (some (.Theorem id)) else pure none let ids := - let args := (args.get! 2).getArgs + let args := asArgs.getArgs let args := (args.get! 2).getSepArgs args.map (λ s => if s.isIdent then some s.getId else none) trace[Progress] "User-provided ids: {ids}" let splitPost : Bool := - let args := (args.get! 2).getArgs + let args := asArgs.getArgs (args.get! 3).getArgs.size > 0 trace[Progress] "Split post: {splitPost}" /- For scalarTac we have a fast track: if the goal is not a linear @@ -343,15 +346,15 @@ namespace Test (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by - progress keep as h as ⟨ x, h1 .. ⟩ - simp [*] + progress keep _ as ⟨ z, h1 .. ⟩ + simp [*, h1] example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by - progress keep as h with Scalar.add_spec as ⟨ z ⟩ - simp [*] + progress keep h with Scalar.add_spec as ⟨ z ⟩ + simp [*, h] /- Checking that universe instantiation works: the original spec uses `α : Type u` where u is quantified, while here we use `α : Type 0` -/ diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index f6dc45c7..1f8f1455 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -201,6 +201,10 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr : | .proj _ _ b => return e.updateProj! (← visit (i + 1) b) visit 0 e +-- Generate a fresh user name for an anonymous proposition to introduce in the +-- assumptions +def mkFreshAnonPropUserName := mkFreshUserName `_ + section Methods variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m] variable {a : Type} @@ -411,7 +415,7 @@ def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do trace[Arith] "left: {inl}: {mleft}" trace[Arith] "right: {inr}: {mright}" -- Create the match expression - withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do + withLocalDeclD (← mkFreshAnonPropUserName) hTy fun hVar => do let motive ← mkLambdaFVars #[hVar] goalType let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr] let mgoal ← getMainGoal @@ -505,8 +509,8 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr let altVarNames ← match optIds with | none => do - let id0 ← mkFreshUserName `h - let id1 ← mkFreshUserName `h + let id0 ← mkFreshAnonPropUserName + let id1 ← mkFreshAnonPropUserName pure #[{ varNames := [id0, id1] }] | some (id0, id1) => do pure #[{ varNames := [id0, id1] }] @@ -532,7 +536,7 @@ partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName : let ids ← do if keepCurrentName then do let cur := (← h.fvarId!.getDecl).userName - let nid ← mkFreshUserName `h + let nid ← mkFreshAnonPropUserName pure (some (cur, nid)) else pure none |