From b437cfd9a381d5d9af5779136f0ef50efeb8ae68 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Nov 2020 15:57:40 -0800
Subject: [PATCH] feat: add `[defaultInstance]` priorities

---
 src/Lean/Elab/SyntheticMVars.lean |  2 +-
 src/Lean/Meta/Instances.lean      | 20 ++++++++++++++------
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index f98826320a..645f012f07 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -155,7 +155,7 @@ def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) : MetaM (Option (List
        match (← getDefaultInstances className) with
        | [] => return none
        | defaultInstances =>
-         for defaultInstance in defaultInstances do
+         for (defaultInstance, prio) in defaultInstances do
             match (← tryToSynthesizeUsingDefaultInstance mvarId defaultInstance) with
             | some newMVarDecls => return some newMVarDecls
             | none => continue
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 8cef2d283a..ead51f892d 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -76,17 +76,22 @@ def getGlobalInstancesIndex : MetaM (DiscrTree Expr) :=
 structure DefaultInstanceEntry where
   className    : Name
   instanceName : Name
+  priority     : Nat
+
+abbrev PrioritySet := Std.RBTree Nat (.<.)
 
 structure DefaultInstances where
-  defaultInstances : NameMap (List Name) := {}
+  defaultInstances : NameMap (List (Name × Nat)) := {}
+  priorities       : PrioritySet := {}
 
 instance : Inhabited DefaultInstances where
   default := {}
 
 def addDefaultInstanceEntry (d : DefaultInstances) (e : DefaultInstanceEntry) : DefaultInstances :=
+  let d := { d with priorities := d.priorities.insert e.priority }
   match d.defaultInstances.find? e.className with
-  | some insts => { defaultInstances := d.defaultInstances.insert e.className <| e.instanceName :: insts }
-  | none       => { defaultInstances := d.defaultInstances.insert e.className [e.instanceName] }
+  | some insts => { d with defaultInstances := d.defaultInstances.insert e.className <| (e.instanceName, e.priority) :: insts }
+  | none       => { d with defaultInstances := d.defaultInstances.insert e.className [(e.instanceName, e.priority)] }
 
 builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances ←
   registerSimplePersistentEnvExtension {
@@ -95,7 +100,7 @@ builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension Defau
     addImportedFn := fun es => (mkStateFromImportedEntries addDefaultInstanceEntry {} es)
   }
 
-def addDefaultInstance (declName : Name) : MetaM Unit := do
+def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do
   match (← getEnv).find? declName with
   | none => throwError! "unknown constant '{declName}'"
   | some info =>
@@ -104,7 +109,7 @@ def addDefaultInstance (declName : Name) : MetaM Unit := do
       | Expr.const className _ _ =>
         unless isClass (← getEnv) className do
           throwError! "invalid default instance '{declName}', it has type '({className} ...)', but {className}' is not a type class"
-        setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName }
+        setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName, priority := prio }
       | _ => throwError! "invalid default instance '{declName}', type must be of the form '(C ...)' where 'C' is a type class"
 
 builtin_initialize
@@ -118,7 +123,10 @@ builtin_initialize
       pure ()
   }
 
-def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List Name) :=
+def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
+  return defaultInstanceExtension.getState (← getEnv) |>.priorities
+
+def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) :=
   return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD []
 
 end Lean.Meta