From a8914380dc90100317de8bd70161c91dc0feeb97 Mon Sep 17 00:00:00 2001 From: Daniel Fabian Date: Thu, 1 Apr 2021 18:23:18 +0000 Subject: [PATCH] feat: add `Ord` and deriving instance for it. For many data structures having an ordering is necessary. This one adds the `Ord` type class and a deriving handler for it. The ordering is based on order of constructors followed by lexicographical ordering within a constructor. --- src/Init/Data.lean | 1 + src/Init/Data/Ord.lean | 34 +++++++++++ src/Lean/Elab/Deriving.lean | 1 + src/Lean/Elab/Deriving/Ord.lean | 104 ++++++++++++++++++++++++++++++++ 4 files changed, 140 insertions(+) create mode 100644 src/Init/Data/Ord.lean create mode 100644 src/Lean/Elab/Deriving/Ord.lean diff --git a/src/Init/Data.lean b/src/Init/Data.lean index ecb12e592a..082afdbc40 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -17,6 +17,7 @@ import Init.Data.Fin import Init.Data.UInt import Init.Data.Float import Init.Data.Option +import Init.Data.Ord import Init.Data.Random import Init.Data.ToString import Init.Data.Range diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean new file mode 100644 index 0000000000..5fdcd3007f --- /dev/null +++ b/src/Init/Data/Ord.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Dany Fabian +-/ + +prelude +import Init.Data.Int +import Init.Data.String + +inductive Ordering +| LT | EQ | GT + +class Ord (α : Type u) where + compare : α → α → Ordering + +def cmp [inst : Ord α] := inst.compare + +def compareOfLessAndEq {α} (x y : α) [HasLess α] [Decidable (x < y)] [DecidableEq α] := + if x < y then Ordering.LT + else if x = y then Ordering.EQ + else Ordering.GT + +instance : Ord Nat where + compare x y := compareOfLessAndEq x y + +instance : Ord Int where + compare x y := compareOfLessAndEq x y + +instance : Ord Int where + compare x y := compareOfLessAndEq x y + +instance : Ord String where + compare x y := compareOfLessAndEq x y diff --git a/src/Lean/Elab/Deriving.lean b/src/Lean/Elab/Deriving.lean index e6cb0076f1..c483d9c8f8 100644 --- a/src/Lean/Elab/Deriving.lean +++ b/src/Lean/Elab/Deriving.lean @@ -12,3 +12,4 @@ import Lean.Elab.Deriving.Repr import Lean.Elab.Deriving.FromToJson import Lean.Elab.Deriving.SizeOf import Lean.Elab.Deriving.Hashable +import Lean.Elab.Deriving.Ord diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean new file mode 100644 index 0000000000..dde40be924 --- /dev/null +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dany Fabian +-/ +import Lean.Meta.Transform +import Lean.Elab.Deriving.Basic +import Lean.Elab.Deriving.Util + +namespace Lean.Elab.Deriving.Ord +open Lean.Parser.Term +open Meta + +def mkOrdHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do + mkHeader ctx `Ord 2 indVal + +def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do + let discrs ← mkDiscrs header indVal + let alts ← mkAlts + `(match $[$discrs],* with $alts:matchAlt*) +where + mkAlts : TermElabM (Array Syntax) := do + let mut alts := #[] + for ctorName in indVal.ctors do + let ctorInfo ← getConstInfoCtor ctorName + let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do + let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies + let mut patterns := #[] + -- add `_` pattern for indices + for i in [:indVal.numIndices] do + patterns := patterns.push (← `(_)) + let mut ctorArgs1 := #[] + let mut ctorArgs2 := #[] + let mut rhs ← `(Ordering.EQ) + -- add `_` for inductive parameters, they are inaccessible + for i in [:indVal.numParams] do + ctorArgs1 := ctorArgs1.push (← `(_)) + ctorArgs2 := ctorArgs2.push (← `(_)) + for i in [:ctorInfo.numFields] do + let x := xs[indVal.numParams + i] + if type.containsFVar x.fvarId! || (←isProp (←inferType x)) then + -- If resulting type depends on this field or is a proof, we don't need to compare + ctorArgs1 := ctorArgs1.push (← `(_)) + ctorArgs2 := ctorArgs2.push (← `(_)) + else + let a := mkIdent (← mkFreshUserName `a) + let b := mkIdent (← mkFreshUserName `b) + ctorArgs1 := ctorArgs1.push a + ctorArgs2 := ctorArgs2.push b + rhs ← `(match cmp $a:ident $b:ident with + | Ordering.LT => Ordering.LT + | Ordering.GT => Ordering.GT + | Ordering.EQ => $rhs) + patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1.reverse:term*)) + patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2.reverse:term*)) + #[←`(matchAltExpr| | $[$patterns:term],* => $rhs:term), + ←`(matchAltExpr| | @$(mkIdent ctorName):ident $ctorArgs1.reverse:term*, _ => Ordering.LT), + ←`(matchAltExpr| | _, @$(mkIdent ctorName):ident $ctorArgs2.reverse:term* => Ordering.GT)] + alts := alts ++ alt + return alts.pop.pop + +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do + let auxFunName ← ctx.auxFunNames[i] + let indVal ← ctx.typeInfos[i] + let header ← mkOrdHeader ctx indVal + let mut body ← mkMatch ctx header indVal auxFunName + if ctx.usePartial || indVal.isRec then + let letDecls ← mkLocalInstanceLetDecls ctx `Ord header.argNames + body ← mkLet letDecls body + let binders := header.binders + if ctx.usePartial || indVal.isRec then + `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : Ordering := $body:term) + else + `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : Ordering := $body:term) + +def mkMutualBlock (ctx : Context) : TermElabM Syntax := do + let mut auxDefs := #[] + for i in [:ctx.typeInfos.size] do + auxDefs := auxDefs.push (← mkAuxFunction ctx i) + `(mutual + $auxDefs:command* + end) + +private def mkOrdInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do + let ctx ← mkContext "ord" declNames[0] + let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord declNames) + trace[Elab.Deriving.ord] "\n{cmds}" + return cmds + +open Command + +def mkOrdInstanceHandler (declNames : Array Name) : CommandElabM Bool := do + if (← declNames.allM isInductive) && declNames.size > 0 then + let cmds ← liftTermElabM none <| mkOrdInstanceCmds declNames + cmds.forM elabCommand + return true + else + return false + +builtin_initialize + registerBuiltinDerivingHandler `Ord mkOrdInstanceHandler + registerTraceClass `Elab.Deriving.ord + +end Lean.Elab.Deriving.Ord