diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean index 4a5f1cb036..ad68cdcda8 100644 --- a/library/init/lean/format.lean +++ b/library/init/lean/format.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import init.control.except init.control.reader init.control.state +import init.lean.options universes u v namespace Lean @@ -77,9 +77,6 @@ def be : Nat → Nat → String → List (Nat × Format) → String let r := merge w (spaceUptoLine f₁ w) (spaceUptoLine' z w) in if r.exceeded then be w k out ((i, f₂)::z) else be w k out ((i, f₁)::z) -def pretty (f : Format) (w : Nat := 80) : String := -be w 0 "" [(0, f)] - @[inline] def bracket (l : String) (f : Format) (r : String) : Format := group (nest l.length $ l ++ f ++ r) @@ -89,6 +86,25 @@ bracket "(" f ")" @[inline] def sbracket (f : Format) : Format := bracket "[" f "]" +def defIndent := 4 +def defUnicode := true +def defWidth := 120 + +def getWidth (o : Options) : Nat := o.get `format.width defWidth +def getIndent (o : Options) : Nat := o.get `format.indent defIndent +def getUnicode (o : Options) : Bool := o.get `format.unicode defUnicode + +@[init] def indentOption : IO Unit := +registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" } +@[init] def unicodeOption : IO Unit := +registerOption `format.unicode { defValue := defUnicode, group := "format", descr := "unicode characters" } +@[init] def widthOption : IO Unit := +registerOption `format.width { defValue := defWidth, group := "format", descr := "line width" } + +def pretty (f : Format) (o : Options := {}) : String := +let w := getWidth o in +be w 0 "" [(0, f)] + end Format open Lean.Format @@ -133,13 +149,12 @@ instance listHasToFormat {α : Type u} [HasToFormat α] : HasToFormat (List α) instance prodHasToFormat {α : Type u} {β : Type v} [HasToFormat α] [HasToFormat β] : HasToFormat (Prod α β) := ⟨λ ⟨a, b⟩, paren $ toFormat a ++ "," ++ line ++ toFormat b⟩ -instance natHasToFormat : HasToFormat Nat := ⟨λ n, toString n⟩ +instance natHasToFormat : HasToFormat Nat := ⟨λ n, toString n⟩ instance uint16HasToFormat : HasToFormat UInt16 := ⟨λ n, toString n⟩ instance uint32HasToFormat : HasToFormat UInt32 := ⟨λ n, toString n⟩ instance uint64HasToFormat : HasToFormat UInt64 := ⟨λ n, toString n⟩ -instance usizeHasToFormat : HasToFormat USize := ⟨λ n, toString n⟩ - -instance formatHasToString : HasToString Format := ⟨pretty⟩ +instance usizeHasToFormat : HasToFormat USize := ⟨λ n, toString n⟩ +instance nameHasToFormat : HasToFormat Name := ⟨λ n, n.toString⟩ protected def Format.repr : Format → Format | nil := "Format.nil" @@ -149,6 +164,9 @@ protected def Format.repr : Format → Format | (compose b f₁ f₂) := paren $ "Format.compose " ++ repr b ++ line ++ Format.repr f₁ ++ line ++ Format.repr f₂ | (choice f₁ f₂) := paren $ "Format.choice" ++ line ++ Format.repr f₁ ++ line ++ Format.repr f₂ + +instance formatHasToString : HasToString Format := ⟨Format.pretty⟩ + instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩ end Lean diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean index 72409517c7..9913d9b9e5 100644 --- a/library/init/lean/kvmap.lean +++ b/library/init/lean/kvmap.lean @@ -10,9 +10,9 @@ namespace Lean inductive DataValue | ofString (v : String) -| ofNat (v : Nat) | ofBool (v : Bool) | ofName (v : Name) +| ofNat (v : Nat) | ofInt (v : Int) def DataValue.beq : DataValue → DataValue → Bool @@ -23,6 +23,12 @@ def DataValue.beq : DataValue → DataValue → Bool instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩ +instance string2DataValue : HasCoe String DataValue := ⟨DataValue.ofString⟩ +instance bool2DataValue : HasCoe Bool DataValue := ⟨DataValue.ofBool⟩ +instance name2DataValue : HasCoe Name DataValue := ⟨DataValue.ofName⟩ +instance nat2DataValue : HasCoe Nat DataValue := ⟨DataValue.ofNat⟩ +instance int2DataValue : HasCoe Int DataValue := ⟨DataValue.ofInt⟩ + /- Remark: we do not use RBMap here because we need to manipulate KVMap objects in C++ and RBMap is implemented in Lean. So, we use just a List until we can generate C++ code from Lean code. -/ @@ -47,30 +53,30 @@ def insert : KVMap → Name → DataValue → KVMap def contains (m : KVMap) (n : Name) : Bool := (m.find n).isSome -def getString (m : KVMap) (k : Name) : Option String := +def getString (m : KVMap) (k : Name) (defVal := "") : String := match m.find k with -| some (DataValue.ofString v) := some v -| _ := none +| some (DataValue.ofString v) := v +| _ := defVal -def getNat (m : KVMap) (k : Name) : Option Nat := +def getNat (m : KVMap) (k : Name) (defVal := 0) : Nat := match m.find k with -| some (DataValue.ofNat v) := some v -| _ := none +| some (DataValue.ofNat v) := v +| _ := defVal -def getInt (m : KVMap) (k : Name) : Option Int := +def getInt (m : KVMap) (k : Name) (defVal : Int := 0) : Int := match m.find k with -| some (DataValue.ofInt v) := some v -| _ := none +| some (DataValue.ofInt v) := v +| _ := defVal -def getBool (m : KVMap) (k : Name) : Option Bool := +def getBool (m : KVMap) (k : Name) (defVal := false) : Bool := match m.find k with -| some (DataValue.ofBool v) := some v -| _ := none +| some (DataValue.ofBool v) := v +| _ := defVal -def getName (m : KVMap) (k : Name) : Option Name := +def getName (m : KVMap) (k : Name) (defVal := Name.anonymous) : Name := match m.find k with -| some (DataValue.ofName v) := some v -| _ := none +| some (DataValue.ofName v) := v +| _ := defVal def setString (m : KVMap) (k : Name) (v : String) : KVMap := m.insert k (DataValue.ofString v) @@ -99,5 +105,30 @@ subset m₁ m₂ && subset m₂ m₁ instance : HasBeq KVMap := ⟨eqv⟩ +class isKVMapVal (α : Type) := +(defVal : α) +(set : KVMap → Name → α → KVMap) +(get : KVMap → Name → α → α) + +export isKVMapVal (set) + +@[inline] def get {α : Type} [isKVMapVal α] (m : KVMap) (k : Name) (defVal := isKVMapVal.defVal α) : α := +isKVMapVal.get m k defVal + +instance boolVal : isKVMapVal Bool := +{ defVal := false, set := setBool, get := λ k n v, getBool k n v } + +instance natVal : isKVMapVal Nat := +{ defVal := 0, set := setNat, get := λ k n v, getNat k n v } + +instance intVal : isKVMapVal Int := +{ defVal := 0, set := setInt, get := λ k n v, getInt k n v } + +instance nameVal : isKVMapVal Name := +{ defVal := Name.anonymous, set := setName, get := λ k n v, getName k n v } + +instance stringVal : isKVMapVal String := +{ defVal := "", set := setString, get := λ k n v, getString k n v } + end KVMap end Lean diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index 4610f21bd6..2302037090 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.lean.name init.data.option.basic +import init.data.option.basic init.lean.name init.lean.format namespace Lean @@ -80,8 +80,8 @@ inductive Result | leaf : Format → Result | num : Nat → Result | offset : Result → Nat → Result -| maxNode : List Result → Result -| imaxNode : List Result → Result +| maxNode : List Result → Result +| imaxNode : List Result → Result def Result.succ : Result → Result | (Result.offset f k) := Result.offset f (k+1) diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index e84fa8b7ef..a1e335478e 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -5,7 +5,7 @@ Author: Leonardo de Moura -/ prelude import init.data.string.basic init.coe init.data.uint init.data.tostring -import init.lean.format init.data.hashable init.data.rbmap init.data.rbtree +import init.data.hashable init.data.rbmap init.data.rbtree namespace Lean inductive Name @@ -138,9 +138,6 @@ toStringWithSep "." instance : HasToString Name := ⟨Name.toString⟩ -instance : HasToFormat Name := -⟨λ n, n.toString⟩ - theorem mkStringNeMkStringOfNePrefix {p₁ : Name} (s₁ : String) {p₂ : Name} (s₂ : String) : p₁ ≠ p₂ → mkString p₁ s₁ ≠ mkString p₂ s₂ := λ h₁ h₂, Name.noConfusion h₂ (λ h _, absurd h h₁) diff --git a/library/init/lean/options.lean b/library/init/lean/options.lean index 2ad3ec2b6d..48ec656bcd 100644 --- a/library/init/lean/options.lean +++ b/library/init/lean/options.lean @@ -9,6 +9,7 @@ import init.lean.kvmap init.io init.control.combinators init.data.tostring namespace Lean def Options := KVMap + namespace Options def empty : Options := {KVMap .} instance : HasEmptyc Options := ⟨empty⟩ @@ -16,6 +17,7 @@ end Options structure OptionDecl := (defValue : DataValue) +(group : String := "") (descr : String := "") def OptionDecls := NameMap OptionDecl @@ -39,6 +41,10 @@ do decls ← getOptionDecls, (some decl) ← pure (decls.find name) | throw $ IO.userError ("unknown option '" ++ toString name ++ "'"), pure decl +def getOptionDefaulValue (name : Name) : IO DataValue := +do decl ← getOptionDecl name, + pure decl.defValue + def getOptionDescr (name : Name) : IO String := do decl ← getOptionDecl name, pure decl.descr @@ -46,10 +52,8 @@ do decl ← getOptionDecl name, def setOptionFromString (opts : Options) (entry : String) : IO Options := do let ps := (entry.split "=").map String.trim, [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form ' = '", - let key := key.toName, - decls ← getOptionDecls, - (some decl) ← pure (decls.find key) | throw $ IO.userError ("unknown option '" ++ toString key ++ "'"), - match decl.defValue with + defValue ← getOptionDefaulValue key.toName, + match defValue with | DataValue.ofString v := pure $ opts.setString key val | DataValue.ofBool v := if key == "true" then pure $ opts.setBool key true @@ -62,4 +66,5 @@ do let ps := (entry.split "=").map String.trim, | DataValue.ofInt v := do unless val.isInt $ throw (IO.userError ("invalid Int option value '" ++ val ++ "'")), pure $ opts.setInt key val.toInt + end Lean diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 8b6295a514..c815418a1b 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -10,6 +10,7 @@ https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/Parsec-paper prelude import init.data.tostring init.data.string.basic init.data.list.basic init.control.except import init.data.repr init.lean.name init.data.dlist init.control.monadfail init.control.combinators +import init.lean.format namespace Lean namespace Parser diff --git a/library/init/lean/parser/rec.lean b/library/init/lean/parser/rec.lean index 39fc1dfe5a..69f4e50d98 100644 --- a/library/init/lean/parser/rec.lean +++ b/library/init/lean/parser/rec.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Recursion monad transformer -/ prelude -import init.lean.parser.parsec init.fix +import init.control.reader init.lean.parser.parsec init.fix namespace Lean.Parser diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index f05d431953..67054ec400 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -55,7 +55,7 @@ private def toStringAux {α : Type} : Trie α → List Format toFormat (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) [] instance {α : Type} : HasToString (Trie α) := -⟨λ t, (flip Format.joinSep Format.line $ toStringAux t).pretty 0⟩ +⟨λ t, (flip Format.joinSep Format.line $ toStringAux t).pretty⟩ end Trie end Parser diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 65b5a2b938..3218ef1b4a 100644 --- a/library/init/lean/trace.lean +++ b/library/init/lean/trace.lean @@ -50,7 +50,7 @@ traceCtx cls msg (pure () : m Unit) instance (m) [Monad m] : MonadTracer (TraceT m) := { traceRoot := λ α pos cls msg ctx, do { st ← get, - if st.opts.getBool cls = some true then do { + if st.opts.getBool cls = true then do { modify $ λ st, {curPos := pos, curTraces := [], ..st}, a ← ctx.get, modify $ λ (st : TraceState), {roots := st.roots.insert pos ⟨msg, st.curTraces⟩, ..st}, @@ -62,7 +62,7 @@ instance (m) [Monad m] : MonadTracer (TraceT m) := -- tracing enabled? some _ ← pure st.curPos | ctx.get, -- Trace class enabled? - if st.opts.getBool cls = some true then do { + if st.opts.getBool cls = true then do { set {curTraces := [], ..st}, a ← ctx.get, modify $ λ (st' : TraceState), {curTraces := st.curTraces ++ [⟨msg, st'.curTraces⟩], ..st'},