From 1d1fa60175785d313f56ef0d2b4f945caa055518 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 22 Aug 2023 09:54:37 -0700 Subject: [PATCH 1/2] Move all json-string functions to Main.lean --- Main.lean | 15 +++++++++++++++ Pantograph.lean | 15 --------------- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/Main.lean b/Main.lean index 10fc6b0..ff57890 100644 --- a/Main.lean +++ b/Main.lean @@ -7,6 +7,21 @@ import Pantograph -- Main IO functions open Pantograph +/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ +def parse_command (s: String): Except String Commands.Command := do + let s := s.trim + match s.get? 0 with + | .some '{' => -- Parse in Json mode + Lean.fromJson? (← Lean.Json.parse s) + | .some _ => -- Parse in line mode + let offset := s.posOf ' ' |> s.offsetOfPos + if offset = s.length then + return { cmd := s.take offset, payload := Lean.Json.null } + else + let payload ← s.drop offset |> Lean.Json.parse + return { cmd := s.take offset, payload := payload } + | .none => throw "Command is empty" + unsafe def loop : MainM Unit := do let state ← get let command ← (← IO.getStdin).getLine diff --git a/Pantograph.lean b/Pantograph.lean index e3501aa..3c5de42 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -20,21 +20,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) -- monadic features in `MainM` abbrev CR α := Except Commands.InteractionError α -/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ -def parse_command (s: String): Except String Commands.Command := do - let s := s.trim - match s.get? 0 with - | .some '{' => -- Parse in Json mode - Lean.fromJson? (← Lean.Json.parse s) - | .some _ => -- Parse in line mode - let offset := s.posOf ' ' |> s.offsetOfPos - if offset = s.length then - return { cmd := s.take offset, payload := Lean.Json.null } - else - let payload ← s.drop offset |> Lean.Json.parse - return { cmd := s.take offset, payload := payload } - | .none => throw "Command is empty" - def execute (command: Commands.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with From e63f7c9afaaa127273210a61be016dfd4e90ed31 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 23 Aug 2023 12:51:06 -0700 Subject: [PATCH 2/2] Add proper printing of sorts --- Pantograph/Serial.lean | 78 +++++++++++++++++++++++++++++++++-------- Pantograph/Version.lean | 2 +- Test/Serial.lean | 5 ++- 3 files changed, 68 insertions(+), 17 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 67a6963..6dd9a9f 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -53,21 +53,73 @@ def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType))) return { binders, target := toString (← Meta.ppExpr body) } +private def name_to_ast: Lean.Name → String + | .anonymous + | .num _ _ => ":anon" + | n@(.str _ _) => toString n + +private def level_depth: Level → Nat + | .zero => 0 + | .succ l => 1 + (level_depth l) + | .max u v | .imax u v => 1 + max (level_depth u) (level_depth v) + | .param _ | .mvar _ => 0 + +theorem level_depth_max_imax (u v: Level): (level_depth (Level.max u v) = level_depth (Level.imax u v)) := by + constructor +theorem level_max_depth_decrease (u v: Level): (level_depth u < level_depth (Level.max u v)) := by + have h1: level_depth (Level.max u v) = 1 + Nat.max (level_depth u) (level_depth v) := by constructor + rewrite [h1] + simp_arith + conv => + rhs + apply Nat.max_def + sorry +theorem level_offset_decrease (u v: Level): (level_depth u ≤ level_depth (Level.max u v).getLevelOffset) := sorry + +/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/ +def serialize_sort_level_ast (level: Level): String := + let k := level.getOffset + let u := level.getLevelOffset + let u_str := match u with + | .zero => "0" + | .succ _ => panic! "getLevelOffset should not return .succ" + | .max v w | .imax v w => + let v := serialize_sort_level_ast v + let w := serialize_sort_level_ast w + s!"(max {v} {w})" + | .param name => + let name := name_to_ast name + s!"{name}" + | .mvar id => + let name := name_to_ast id.name + s!"(:mvar {name})" + match k, u with + | 0, _ => u_str + | _, .zero => s!"{k}" + | _, _ => s!"(+ {u_str} {k})" + termination_by serialize_sort_level_ast level => level_depth level + decreasing_by + . sorry + /-- - Completely serialises an expression tree. Json not used due to compactness + Completely serializes an expression tree. Json not used due to compactness -/ def serialize_expression_ast (expr: Expr): MetaM String := do match expr with | .bvar deBruijnIndex => -- This is very common so the index alone is shown. Literals are handled below. + -- The raw de Bruijn index should never appear in an unbound setting. In + -- Lean these are handled using a `#` prefix. return s!"{deBruijnIndex}" | .fvar fvarId => let name := (← fvarId.getDecl).userName return s!"(:fv {name})" - | .mvar _ => - -- mvarId is ignored. - return s!":mv" - | .sort u => return s!"(:sort {u.depth})" + | .mvar mvarId => + let name := name_to_ast mvarId.name + return s!"(:mv {name})" + | .sort level => + let level := serialize_sort_level_ast level + return s!"(:sort {level})" | .const declName _ => -- The universe level of the const expression is elided since it should be -- inferrable from surrounding expression @@ -77,20 +129,20 @@ def serialize_expression_ast (expr: Expr): MetaM String := do let arg' ← serialize_expression_ast arg return s!"({fn'} {arg'})" | .lam binderName binderType body binderInfo => - let binderName' := nameToAst binderName + let binderName' := name_to_ast binderName let binderType' ← serialize_expression_ast binderType let body' ← serialize_expression_ast body - let binderInfo' := binderInfoToAst binderInfo + let binderInfo' := binder_info_to_ast binderInfo return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" | .forallE binderName binderType body binderInfo => - let binderName' := nameToAst binderName + let binderName' := name_to_ast binderName let binderType' ← serialize_expression_ast binderType let body' ← serialize_expression_ast body - let binderInfo' := binderInfoToAst binderInfo + let binderInfo' := binder_info_to_ast binderInfo return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" | .letE name type value body _ => -- Dependent boolean flag diacarded - let name' := nameToAst name + let name' := name_to_ast name let type' ← serialize_expression_ast type let value' ← serialize_expression_ast value let body' ← serialize_expression_ast body @@ -112,11 +164,7 @@ def serialize_expression_ast (expr: Expr): MetaM String := do where -- Elides all unhygenic names - nameToAst: Lean.Name → String - | .anonymous - | .num _ _ => ":anon" - | n@(.str _ _) => toString n - binderInfoToAst : Lean.BinderInfo → String + binder_info_to_ast : Lean.BinderInfo → String | .default => "" | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 9cf39ff..e4ebd2c 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,5 @@ namespace Pantograph -def version := "0.2.2" +def version := "0.2.3" end Pantograph diff --git a/Test/Serial.lean b/Test/Serial.lean index f84e3e4..e300492 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -39,7 +39,10 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do ("Nat.add", "(:forall :anon (:c Nat) (:forall :anon (:c Nat) (:c Nat)))"), -- These ones are normal and easy ("Nat.add_one", "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"), - ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)") + ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)"), + -- Handling of higher order types + ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"), + ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))") ] let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv