mostly complete locally nameless support

Lott/DSL/Elab/JudgementComprehension.lean

@@ -7,7 +7,7 @@ open Lean.Elab
 
 @[lott_term_elab Lott.DSL.judgementComprehension]
 private
-def judgementComprehensionTermElab : TermElab := fun stx => do
+def judgementComprehensionTermElab : TermElab := fun _ stx => do
  let `(Lott.Judgement| </ $«judgement»:Lott.Judgement // $i ∈ $c />) := stx
  | throwUnsupportedSyntax
  Lean.Elab.Term.elabTerm (← ``(∀ $i:ident ∈ $c, [[$«judgement»:Lott.Judgement]])) none

Lott/DSL/Elab/Nat.lean

@@ -22,11 +22,11 @@ def nat.term_parser : Parser :=
 
 @[lott_term_elab Lott.Symbol.Nat]
 def natTermElab : TermElab
- | .node _ `Lott.Symbol.Nat #[n@(.ident ..)]
- | .node _ `Lott.Symbol.Nat #[n@(.node _ `num _)]
- | .node _ `Lott.Symbol.Nat #[.atom _ "(", n, .atom _ ")"] =>
+ | _, .node _ `Lott.Symbol.Nat #[n@(.ident ..)]
+ | _, .node _ `Lott.Symbol.Nat #[n@(.node _ `num _)]
+ | _, .node _ `Lott.Symbol.Nat #[.atom _ "(", n, .atom _ ")"] =>
  Term.elabTerm n <| .some (.const `Nat [])
- | _ => throwUnsupportedSyntax
+ | _, _ => throwUnsupportedSyntax
 
 @[lott_tex_elab Lott.Symbol.Nat]
 def natTexElab : TexElab

Lott/DSL/Elab/UniversalJudgement.lean

@@ -0,0 +1,20 @@
+import Lott.DSL.Elab.Basic
+import Lott.DSL.Parser.UniversalJudgement
+
+namespace Lott.DSL.Elab
+
+open Lean.Elab
+
+@[lott_term_elab Lott.DSL.universalJudgement]
+private
+def universalJudgementTermElab : TermElab := fun _ stx => do
+ let `(Lott.Judgement| ∀ $i $[$binderPred?]?, $«judgement»:Lott.Judgement) := stx
+ | throwUnsupportedSyntax
+ let stx' ← if let some bp := binderPred? then
+ ``(∀ $i:ident, satisfies_binder_pred% $i $bp → [[$«judgement»:Lott.Judgement]])
+ else
+ ``(∀ $i:ident, [[$«judgement»:Lott.Judgement]])
+ Lean.Elab.Term.elabTerm stx' none
+
+end Lott.DSL.Elab
+

Lott/DSL/Environment.lean

@@ -1,89 +1 @@
-import Lean.Data.Trie
-import Lean.Environment
-import Lott.DSL.IR
-
-namespace Lott.DSL
-
-open Lean
-open Lean.Data
-
-structure Alias where
- canon : Name
- alias : Name
-
-instance : Inhabited Alias where default := { canon := default, alias := default }
-
-structure AliasState where
- byAlias : Trie Alias
- allCanon : NameSet
-
-instance : Inhabited AliasState where default := { byAlias := default, allCanon := default }
-
-initialize aliasExt : PersistentEnvExtension Alias Alias AliasState ←
- registerPersistentEnvExtension {
- mkInitial := return default
- addImportedFn := fun aliasss => return {
- byAlias :=
- aliasss.flatten.foldl (init := .empty) fun acc a => acc.upsert a.alias.toString fun _ => a
- allCanon := aliasss.flatten.map (·.canon) |> RBTree.fromArray (cmp := Name.quickCmp)
- }
- addEntryFn := fun { byAlias, allCanon } a => {
- byAlias := byAlias.insert a.alias.toString a
- allCanon := allCanon.insert a.canon
- }
- exportEntriesFn := fun { byAlias, .. } => byAlias.values
-}
-
-initialize metaVarExt : PersistentEnvExtension Name Name NameSet ←
- registerPersistentEnvExtension {
- mkInitial := return default
- addImportedFn := fun metaVarss => return metaVarss.flatten.foldl NameSet.insert .empty
- addEntryFn := NameSet.insert
- exportEntriesFn :=
- RBTree.fold (cmp := Name.quickCmp) (init := #[]) fun acc metaVar => acc.push metaVar
-}
-
-structure Symbol where
- qualified : Name
- normalProds : NameMap (Array IR)
- substitutions : Array (Name × Name)
-
-instance : Inhabited Symbol where
- default := { qualified := default, normalProds := default, substitutions := default }
-
-abbrev SymbolState := NameMap Symbol
-
-initialize symbolExt : PersistentEnvExtension Symbol Symbol SymbolState ←
- registerPersistentEnvExtension {
- mkInitial := return default
- addImportedFn := fun symss =>
- return symss.flatten.foldl (init := mkNameMap _) fun acc sym => acc.insert sym.qualified sym
- addEntryFn := fun st sym => st.insert sym.qualified sym
- exportEntriesFn := RBMap.fold (cmp := Name.quickCmp) (init := #[]) fun acc _ sym => acc.push sym
-}
-
-structure Judgement where
- name : Name
- ir : Array IR
-
-structure JudgementState where
- byName : NameMap Judgement
- all : NameSet
-
-instance : Inhabited JudgementState where default := { byName := default, all := default }
-
-initialize judgementExt : PersistentEnvExtension Judgement Judgement JudgementState ← registerPersistentEnvExtension {
- mkInitial := return default
- addImportedFn := fun jds => return {
- byName := jds.flatten.foldl (init := mkNameMap _) fun acc jd => acc.insert jd.name jd
- all := jds.flatten.map (·.name) |> RBTree.fromArray (cmp := Name.quickCmp)
- }
- addEntryFn := fun { byName, all } jd => {
- byName := byName.insert jd.name jd
- all := all.insert jd.name
- }
- exportEntriesFn := fun { byName, .. } =>
- byName.fold (cmp := Name.quickCmp) (init := #[]) fun acc _ jd => acc.push jd
-}
-
-end Lott.DSL
+import Lott.DSL.Environment.Basic

Lott/DSL/Environment/Basic.lean

@@ -0,0 +1,81 @@
+import Lean.Data.Trie
+import Lean.Environment
+import Lott.DSL.IR
+
+namespace Lott.DSL
+
+open Lean
+open Lean.Data
+
+structure Alias where
+ canon : Name
+ alias : Name
+
+instance : Inhabited Alias where default := { canon := default, alias := default }
+
+structure AliasState where
+ byAlias : Trie Alias
+ allCanon : NameSet
+
+instance : Inhabited AliasState where default := { byAlias := default, allCanon := default }
+
+initialize aliasExt : PersistentEnvExtension Alias Alias AliasState ←
+ registerPersistentEnvExtension {
+ mkInitial := return default
+ addImportedFn := fun aliasss => return {
+ byAlias :=
+ aliasss.flatten.foldl (init := .empty) fun acc a => acc.upsert a.alias.toString fun _ => a
+ allCanon := aliasss.flatten.map (·.canon) |> RBTree.fromArray (cmp := Name.quickCmp)
+ }
+ addEntryFn := fun { byAlias, allCanon } a => {
+ byAlias := byAlias.insert a.alias.toString a
+ allCanon := allCanon.insert a.canon
+ }
+ exportEntriesFn := fun { byAlias, .. } => byAlias.values
+}
+
+structure Symbol where
+ qualified : Name
+ normalProds : NameMap (Array IR)
+ substitutions : Array (Name × Name)
+
+instance : Inhabited Symbol where
+ default := { qualified := default, normalProds := default, substitutions := default }
+
+abbrev SymbolState := NameMap Symbol
+
+initialize symbolExt : PersistentEnvExtension Symbol Symbol SymbolState ←
+ registerPersistentEnvExtension {
+ mkInitial := return default
+ addImportedFn := fun symss =>
+ return symss.flatten.foldl (init := mkNameMap _) fun acc sym => acc.insert sym.qualified sym
+ addEntryFn := fun st sym => st.insert sym.qualified sym
+ exportEntriesFn := RBMap.fold (cmp := Name.quickCmp) (init := #[]) fun acc _ sym => acc.push sym
+}
+
+structure Judgement where
+ name : Name
+ ir : Array IR
+ ids : Array Name
+
+structure JudgementState where
+ byName : NameMap Judgement
+ all : NameSet
+
+instance : Inhabited JudgementState where default := { byName := default, all := default }
+
+initialize judgementExt : PersistentEnvExtension Judgement Judgement JudgementState ← registerPersistentEnvExtension {
+ mkInitial := return default
+ addImportedFn := fun jds => return {
+ byName := jds.flatten.foldl (init := mkNameMap _) fun acc jd => acc.insert jd.name jd
+ all := jds.flatten.map (·.name) |> RBTree.fromArray (cmp := Name.quickCmp)
+ }
+ addEntryFn := fun { byName, all } jd => {
+ byName := byName.insert jd.name jd
+ all := all.insert jd.name
+ }
+ exportEntriesFn := fun { byName, .. } =>
+ byName.fold (cmp := Name.quickCmp) (init := #[]) fun acc _ jd => acc.push jd
+}
+
+end Lott.DSL

Lott/DSL/Environment/MetaVar.lean

@@ -0,0 +1,16 @@
+import Lean
+
+namespace Lott.DSL
+
+open Lean
+
+initialize metaVarExt : PersistentEnvExtension (Name × Bool) (Name × Bool) (NameMap Bool) ←
+ registerPersistentEnvExtension {
+ mkInitial := return default
+ addImportedFn := fun metaVarss =>
+ return metaVarss.flatten.foldl (init := mkNameMap _) (fun acc (n, ln) => acc.insert n ln)
+ addEntryFn := fun st (n, ln) => st.insert n ln
+ exportEntriesFn := RBMap.fold (cmp := Name.quickCmp) (init := #[]) fun acc n ln => acc.push (n, ln)
+}
+
+end Lott.DSL

Lott/DSL/IR.lean

@@ -1,4 +1,5 @@
 import Lean
+import Lott.DSL.Environment.MetaVar
 
 namespace Lott.DSL
 
@@ -37,6 +38,14 @@ end
 
 namespace IR
 
+partial
+def containsName (ir : Array IR) (name : Name) : Bool :=
+ ir.any fun (mk l ir) =>
+ l.getId == name ||
+ match ir with
+ | .sepBy ir _ | .optional ir => containsName ir name
+ | _ => false
+
 mutual
 private partial
 def toParser' (canon : Name) : IR → CommandElabM Term
@@ -100,19 +109,26 @@ end
 
 mutual
 partial
-def toType : IR → CommandElabM (Option Term)
- | IR.mk _ (.category n) => return some <| mkIdent n
+def toType (ids binders : Array Name) : IR → CommandElabM (Option Term)
+ | IR.mk l (.category n) => do
+ for binder in binders do
+ if l.getId == binder && (metaVarExt.getState (← getEnv)).find! n then
+ return none
+ for id in ids do
+ if l.getId == id && (metaVarExt.getState (← getEnv)).find! n then
+ return some <| mkIdent <| n.appendAfter "Id"
+ return some <| mkIdent n
  | IR.mk _ (.atom _) => return none
  | IR.mk _ (.sepBy ir _) => do
- let some type' ← toTypeProdSeq ir | return none
+ let some type' ← toTypeProdSeq ids binders ir | return none
  ``(List $type')
  | IR.mk _ (.optional ir) => do
- let some type' ← toTypeProdSeq ir | return none
+ let some type' ← toTypeProdSeq ids binders ir | return none
  return some <| ← ``(Option $type')
 
 partial
-def toTypeProdSeq (ir : Array IR) : CommandElabM (Option Term) := do
- let types ← ir.filterMapM IR.toType
+def toTypeProdSeq (ids binders : Array Name) (ir : Array IR) : CommandElabM (Option Term) := do
+ let types ← ir.filterMapM <| IR.toType ids binders
  let some (type' : Term) := types[0]? | return none
  return some <| ← types.foldlM (start := 1) (init := type') fun acc t => ``($acc × $t)
 end
@@ -137,8 +153,11 @@ def toMkTypeProdSeqExpr (ir : Array IR) : CommandElabM (Option Term) := do
  ``(mkApp2 (Expr.const `Prod [levelOne, levelOne]) $t $acc)
 end
 
-def toTypeArrSeq (ir : Array IR) (init : Term) : CommandElabM Term := do
- (← ir.filterMapM IR.toType) |>.foldrM (init := init) fun t acc => ``($t → $acc)
+def foldrArrow (args : Array Term) (init : Term) : CommandElabM Term :=
+ args.foldrM (init := init) fun arg acc => ``($arg → $acc)
+
+def toTypeArrSeq (ir : Array IR) (init : Term) (ids binders : Array Name) : CommandElabM Term := do
+ (← ir.filterMapM <| IR.toType ids binders) |> foldrArrow (init := init)
 
 private
 def toPatternArg : IR → CommandElabM Term
@@ -152,9 +171,19 @@ def toPatternArgs (ir : Array IR) : CommandElabM (TSepArray `term ",") :=
 
 def toJoinArgs (ir : Array IR) : TSepArray `term "," := ir.map (β := Term) fun | mk l _ => l
 
+def foldrProd (as : Array Term) : CommandElabM Term := if let some a := as.back? then
+ as.foldrM (init := a) (start := as.size - 1) fun a acc => `(($acc, $a))
+ else
+ ``(())
+
+def foldlAnd (as : Array Term) : CommandElabM Term := if let some a := as[0]? then
+ as.foldlM (init := a) (start := 1) fun acc a => `($acc ∧ $a)
+ else
+ ``(True)
+
 partial
 def toIsChildCtor (prodIdent isIdent : Ident) (qualified pqualified : Name) (ir pir : Array IR)
- : CommandElabM (TSyntax `Lean.Parser.Command.ctor) := do
+ (binders : Array Name) : CommandElabM (TSyntax `Lean.Parser.Command.ctor) := do
  if ir.size != pir.size then
  throwErrorAt prodIdent "length of child production ({ir.size}) doesn't match length of parent production ({pir.size})"
 
@@ -172,25 +201,15 @@ where
  | `(Lean.binderIdent| $i:ident) => `(term| $i:ident)
  | _ => throwUnsupportedSyntax
 
- foldrArrow (args : Array Term) (init : Term) : CommandElabM Term :=
- args.foldrM (init := init) fun arg acc => ``($arg → $acc)
-
- foldrProd (as : Array Term) : CommandElabM Term := if let some a := as.back? then
- as.foldrM (init := a) (start := as.size - 1) fun a acc => `(($acc, $a))
- else
- ``(())
-
- foldlAnd (as : Array Term) : CommandElabM Term := if let some a := as[0]? then
- as.foldlM (init := a) (start := 1) fun acc a => `($acc ∧ $a)
- else
- ``(True)
-
  go (irs : Array (IR × IR)) (patAcc : TSyntaxArray `Lean.binderIdent := #[])
  (propAcc : Array Term := #[])
  : CommandElabM (TSyntaxArray `Lean.binderIdent × Array Term) := do
  let some (mk l' ir, mk l pir) := irs[0]? | return (patAcc, propAcc)
  let irs' := irs.extract 1 irs.size
 
+ if binders.contains l'.getId then
+ return ← go irs' patAcc propAcc
+
  let lbi ← `(Lean.binderIdent| $l:ident)
  let l'bi ← `(Lean.binderIdent| $l':ident)
  let hole ← `(Lean.binderIdent| _)