From 60091a49cdf46a890726790c8e2cf8798eb9f478 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2020 08:38:17 -0700 Subject: [PATCH] chore: move to new frontend --- src/Lean/Meta/Offset.lean | 74 ++++++++++++++--------------- src/Lean/Meta/Tactic.lean | 1 + src/Lean/Meta/TransparencyMode.lean | 7 ++- 3 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index 8b05936107..a2a4de414b 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -1,3 +1,4 @@ +#lang lean4 /- Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -6,43 +7,43 @@ Authors: Leonardo de Moura import Lean.Data.LBool import Lean.Meta.InferType -namespace Lean -namespace Meta +namespace Lean.Meta partial def evalNat : Expr → Option Nat | Expr.lit (Literal.natVal n) _ => pure n | Expr.mdata _ e _ => evalNat e | Expr.const `Nat.zero _ _ => pure 0 -| e@(Expr.app _ a _) => - let fn := e.getAppFn; +| e@(Expr.app _ a _) => do + let fn := e.getAppFn match fn with | Expr.const c _ _ => - let nargs := e.getAppNumArgs; - if c == `Nat.succ && nargs == 1 then do - v ← evalNat a; pure $ v+1 - else if c == `Nat.add && nargs == 2 then do - v₁ ← evalNat (e.getArg! 0); - v₂ ← evalNat (e.getArg! 1); + let nargs := e.getAppNumArgs + if c == `Nat.succ && nargs == 1 then + let v ← evalNat a + pure $ v+1 + else if c == `Nat.add && nargs == 2 then + let v₁ ← evalNat (e.getArg! 0) + let v₂ ← evalNat (e.getArg! 1) pure $ v₁ + v₂ - else if c == `Nat.sub && nargs == 2 then do - v₁ ← evalNat (e.getArg! 0); - v₂ ← evalNat (e.getArg! 1); + else if c == `Nat.sub && nargs == 2 then + let v₁ ← evalNat (e.getArg! 0) + let v₂ ← evalNat (e.getArg! 1) pure $ v₁ - v₂ - else if c == `Nat.mul && nargs == 2 then do - v₁ ← evalNat (e.getArg! 0); - v₂ ← evalNat (e.getArg! 1); + else if c == `Nat.mul && nargs == 2 then + let v₁ ← evalNat (e.getArg! 0) + let v₂ ← evalNat (e.getArg! 1) pure $ v₁ * v₂ - else if c == `HasAdd.add && nargs == 4 then do - v₁ ← evalNat (e.getArg! 2); - v₂ ← evalNat (e.getArg! 3); + else if c == `HasAdd.add && nargs == 4 then + let v₁ ← evalNat (e.getArg! 2) + let v₂ ← evalNat (e.getArg! 3) pure $ v₁ + v₂ - else if c == `HasAdd.sub && nargs == 4 then do - v₁ ← evalNat (e.getArg! 2); - v₂ ← evalNat (e.getArg! 3); + else if c == `HasAdd.sub && nargs == 4 then + let v₁ ← evalNat (e.getArg! 2) + let v₂ ← evalNat (e.getArg! 3) pure $ v₁ - v₂ - else if c == `HasAdd.mul && nargs == 4 then do - v₁ ← evalNat (e.getArg! 2); - v₂ ← evalNat (e.getArg! 3); + else if c == `HasAdd.mul && nargs == 4 then + let v₁ ← evalNat (e.getArg! 2) + let v₂ ← evalNat (e.getArg! 3) pure $ v₁ * v₂ else if c == `HasOfNat.ofNat && nargs == 3 then evalNat (e.getArg! 2) @@ -54,20 +55,20 @@ partial def evalNat : Expr → Option Nat /- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/ private partial def getOffsetAux : Expr → Bool → Option (Expr × Nat) | e@(Expr.app _ a _), top => - let fn := e.getAppFn; + let fn := e.getAppFn match fn with | Expr.const c _ _ => - let nargs := e.getAppNumArgs; + let nargs := e.getAppNumArgs if c == `Nat.succ && nargs == 1 then do - (s, k) ← getOffsetAux a false; + let (s, k) ← getOffsetAux a false pure (s, k+1) else if c == `Nat.add && nargs == 2 then do - v ← evalNat (e.getArg! 1); - (s, k) ← getOffsetAux (e.getArg! 0) false; + let v ← evalNat (e.getArg! 1) + let (s, k) ← getOffsetAux (e.getArg! 0) false pure (s, k+v) else if c == `HasAdd.add && nargs == 4 then do - v ← evalNat (e.getArg! 3); - (s, k) ← getOffsetAux (e.getArg! 2) false; + let v ← evalNat (e.getArg! 3) + let (s, k) ← getOffsetAux (e.getArg! 2) false pure (s, k+v) else if top then none else pure (e, 0) | _ => if top then none else pure (e, 0) @@ -78,10 +79,10 @@ getOffsetAux e true private partial def isOffset : Expr → Option (Expr × Nat) | e@(Expr.app _ a _) => - let fn := e.getAppFn; + let fn := e.getAppFn match fn with | Expr.const c _ _ => - let nargs := e.getAppNumArgs; + let nargs := e.getAppNumArgs if (c == `Nat.succ && nargs == 1) || (c == `Nat.add && nargs == 2) || (c == `HasAdd.add && nargs == 4) then getOffset e else none @@ -99,7 +100,7 @@ else if isNatZero e then mkNatLit offset else mkAppB (mkConst `Nat.add) e (mkNatLit offset) def isDefEqOffset (s t : Expr) : DefEqM LBool := -let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t; +let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t match isOffset s with | some (s, k₁) => match isOffset t with | some (t, k₂) => -- s+k₁ =?= t+k₂ @@ -119,5 +120,4 @@ match isOffset s with | none => pure LBool.undef | none => pure LBool.undef -end Meta -end Lean +end Lean.Meta diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index c06dab4c1b..a262b596a7 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -1,3 +1,4 @@ +#lang lean4 /- Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. diff --git a/src/Lean/Meta/TransparencyMode.lean b/src/Lean/Meta/TransparencyMode.lean index 4cc204299c..5986f051bf 100644 --- a/src/Lean/Meta/TransparencyMode.lean +++ b/src/Lean/Meta/TransparencyMode.lean @@ -1,10 +1,10 @@ +#lang lean4 /- Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -namespace Lean -namespace Meta +namespace Lean.Meta inductive TransparencyMode | all | default | reducible @@ -35,5 +35,4 @@ def lt : TransparencyMode → TransparencyMode → Bool end TransparencyMode -end Meta -end Lean +end Lean.Meta