/
InstantiateLevelParams.lean
60 lines (52 loc) · 2.26 KB
/
InstantiateLevelParams.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.ReplaceExpr
namespace Lean.Expr
/--
Instantiate level parameters
-/
@[specialize] def instantiateLevelParamsCore (s : Name → Option Level) (e : Expr) : Expr :=
e.replace replaceFn
where
@[specialize] replaceFn (e : Expr) : Option Expr :=
if !e.hasLevelParam then e else match e with
| const _ us => e.updateConst! (us.map fun u => u.substParams s)
| sort u => e.updateSort! (u.substParams s)
| _ => none
private def getParamSubst : List Name → List Level → Name → Option Level
| p::ps, u::us, p' => if p == p' then some u else getParamSubst ps us p'
| _, _, _ => none
/--
Instantiate universe level parameters names `paramNames` with `lvls` in `e`.
If the two lists have different length, the smallest one is used.
-/
def instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr :=
if paramNames.isEmpty || lvls.isEmpty then e else
instantiateLevelParamsCore (getParamSubst paramNames lvls) e
/--
Instantiate universe level parameters names `paramNames` with `lvls` in `e`.
If the two lists have different length, the smallest one is used.
(Does not preserve expression sharing.)
-/
def instantiateLevelParamsNoCache (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr :=
if paramNames.isEmpty || lvls.isEmpty then e else
e.replaceNoCache (instantiateLevelParamsCore.replaceFn (getParamSubst paramNames lvls))
private partial def getParamSubstArray (ps : Array Name) (us : Array Level) (p' : Name) (i : Nat) : Option Level :=
if h : i < ps.size then
let p := ps.get ⟨i, h⟩
if h : i < us.size then
let u := us.get ⟨i, h⟩
if p == p' then some u else getParamSubstArray ps us p' (i+1)
else none
else none
/--
Instantiate universe level parameters names `paramNames` with `lvls` in `e`.
If the two arrays have different length, the smallest one is used.
-/
def instantiateLevelParamsArray (e : Expr) (paramNames : Array Name) (lvls : Array Level) : Expr :=
if paramNames.isEmpty || lvls.isEmpty then e else
e.instantiateLevelParamsCore fun p =>
getParamSubstArray paramNames lvls p 0