From f16f215c2a88674f3e161ac3d83186ff3d4d2c7d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Nov 2014 08:53:14 -0800 Subject: [PATCH] refactor(data/num/string): break into pieces to reduce dependencies --- library/data/num/decl.lean | 2 +- library/data/string/decl.lean | 11 +++++++++++ library/data/string/default.lean | 4 ++++ library/data/{string.lean => string/thms.lean} | 11 +---------- library/tools/helper_tactics.lean | 2 +- library/tools/tactic.lean | 3 +-- tests/lean/beginend_bug.lean | 2 +- tests/lean/goals1.lean | 2 +- tests/lean/run/beginend.lean | 2 +- tests/lean/run/beginend3.lean | 2 +- tests/lean/run/decidable.lean | 2 +- tests/lean/run/rename_tac.lean | 2 +- tests/lean/run/set2.lean | 2 +- tests/lean/run/tac1.lean | 2 +- 14 files changed, 27 insertions(+), 22 deletions(-) create mode 100644 library/data/string/decl.lean create mode 100644 library/data/string/default.lean rename library/data/{string.lean => string/thms.lean} (67%) diff --git a/library/data/num/decl.lean b/library/data/num/decl.lean index e1f821d5b..f27e0e13a 100644 --- a/library/data/num/decl.lean +++ b/library/data/num/decl.lean @@ -3,7 +3,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura ---------------------------------------------------------------------------------------------------- - +import data.unit.decl -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))). -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). diff --git a/library/data/string/decl.lean b/library/data/string/decl.lean new file mode 100644 index 000000000..361fd6a5d --- /dev/null +++ b/library/data/string/decl.lean @@ -0,0 +1,11 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura +import data.bool.decl + +inductive char : Type := + mk : bool → bool → bool → bool → bool → bool → bool → bool → char + +inductive string : Type := + empty : string, + str : char → string → string diff --git a/library/data/string/default.lean b/library/data/string/default.lean new file mode 100644 index 000000000..1a20b29a4 --- /dev/null +++ b/library/data/string/default.lean @@ -0,0 +1,4 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura +import data.string.decl data.string.thms diff --git a/library/data/string.lean b/library/data/string/thms.lean similarity index 67% rename from library/data/string.lean rename to library/data/string/thms.lean index b82f768e7..30e045b35 100644 --- a/library/data/string.lean +++ b/library/data/string/thms.lean @@ -1,23 +1,14 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura - -import data.bool - +import data.string.decl data.bool open bool inhabited -inductive char : Type := - mk : bool → bool → bool → bool → bool → bool → bool → bool → char - namespace char protected definition is_inhabited [instance] : inhabited char := inhabited.mk (mk ff ff ff ff ff ff ff ff) end char -inductive string : Type := - empty : string, - str : char → string → string - namespace string protected definition is_inhabited [instance] : inhabited string := inhabited.mk empty diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean index 335069a7b..cba7c953d 100644 --- a/library/tools/helper_tactics.lean +++ b/library/tools/helper_tactics.lean @@ -7,7 +7,7 @@ -- Useful tactics. -import .tactic +import tools.tactic logic.eq open tactic diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 4641999db..9c088ff1c 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -3,8 +3,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura ---------------------------------------------------------------------------------------------------- - -import data.string data.num.decl +import data.string.decl data.num.decl -- This is just a trick to embed the 'tactic language' as a -- Lean expression. We should view 'tactic' as automation -- that when execute produces a term. diff --git a/tests/lean/beginend_bug.lean b/tests/lean/beginend_bug.lean index 12b1a11ec..9c153e076 100644 --- a/tests/lean/beginend_bug.lean +++ b/tests/lean/beginend_bug.lean @@ -1,4 +1,4 @@ -import tools.tactic +import tools.tactic logic open tactic theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c := diff --git a/tests/lean/goals1.lean b/tests/lean/goals1.lean index d2cc0b67d..da193bbf1 100644 --- a/tests/lean/goals1.lean +++ b/tests/lean/goals1.lean @@ -1,4 +1,4 @@ -import tools.tactic +import tools.tactic logic.eq open tactic set_option pp.notation false diff --git a/tests/lean/run/beginend.lean b/tests/lean/run/beginend.lean index 01782efe3..e9ec1c932 100644 --- a/tests/lean/run/beginend.lean +++ b/tests/lean/run/beginend.lean @@ -1,4 +1,4 @@ -import tools.tactic +import tools.tactic logic.eq open tactic theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c := diff --git a/tests/lean/run/beginend3.lean b/tests/lean/run/beginend3.lean index eefff0212..01335cd5c 100644 --- a/tests/lean/run/beginend3.lean +++ b/tests/lean/run/beginend3.lean @@ -1,4 +1,4 @@ -import tools.tactic +import tools.tactic logic open tactic theorem foo (A : Type) (a b c : A) : a = b → b = c → a = c ∧ c = a := diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean index bf04e8e55..7d712e29c 100644 --- a/tests/lean/run/decidable.lean +++ b/tests/lean/run/decidable.lean @@ -1,4 +1,4 @@ -import logic data.unit +import logic data.unit data.bool open bool unit decidable constants a b c : bool diff --git a/tests/lean/run/rename_tac.lean b/tests/lean/run/rename_tac.lean index 81bdea97e..9db0f1857 100644 --- a/tests/lean/run/rename_tac.lean +++ b/tests/lean/run/rename_tac.lean @@ -1,4 +1,4 @@ -import tools.tactic +import tools.tactic logic open tactic theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c := diff --git a/tests/lean/run/set2.lean b/tests/lean/run/set2.lean index d4eac8c54..2f3f7cba1 100644 --- a/tests/lean/run/set2.lean +++ b/tests/lean/run/set2.lean @@ -1,4 +1,4 @@ -import logic +import logic data.bool open bool namespace set diff --git a/tests/lean/run/tac1.lean b/tests/lean/run/tac1.lean index 82bb786e3..58e5d0a0a 100644 --- a/tests/lean/run/tac1.lean +++ b/tests/lean/run/tac1.lean @@ -1,4 +1,4 @@ -import tools.tactic +import tools.tactic logic open tactic definition mytac := apply @and.intro; apply @eq.refl