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

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

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"

Pantograph/Version.lean

@@ -1,5 +1,5 @@
 namespace Pantograph
 
-def version := "0.2.2"
+def version := "0.2.3"
 
 end Pantograph

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