| As an example of elaborator reflection here we step through this identity implementation: | %language ElabReflection
idNat : Nat -> Nat
idNat = %runElab (do
intro `{{x}}
fill (Var `{{x}})
solve
) |
We start off with a hole for the whole term (of type Nat->Nat ) We fill that with 'intro' which creates a lambda term with a hole for the expression. |
 |
After each tactic we will look at the state:
| We start with the type signature like this: | %language ElabReflection idNat : Nat -> Nat idNat = %runElab (do |
| In order to investigate how the program works we can look at the proofState at each stage as the tactics are applied. So here is the proofState at the start: |  |
| We can also look at the logic at each stage: |  |
| The term is: | ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} |
getEnv getGoal getHoles |
getEnv=[]
getGoal=({hole_2}, {TT:Bind
name=`{{__pi_arg}}
binder={
Π ({`{{Nat}}.["Nat", "Prelude"]}:{type const tag=8,0}).{
TT:TType tt=ext=./Prelude/Nat.idr#20
}
}
tt={
TT:Parameter name ref
NameType={type const tag=8,0}
TTName={`{{Nat}}.["Nat","Prelude"]}
TT={TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
})
getHoles=[{hole_2},{hole_0}] |
| getGuess | error no guess |
Here is the state (given by 'debug') at the start. 'pi_arg' represents the first argument of the function. If there had been other arguments they would be 'pi_arg1'.'pi_arg2'... |
Holes:
----------------------------------
{hole_2} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
----------------------------------
{hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
Term:
?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
|
| Introduce a lambda binding around the current hole and focus on the body. | intro `{{x}} |
 |
|
 |
|
?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} |
|
getEnv getGoal getHoles |
getEnv=[(
`{{x}}, {
λ ({`{{Nat}}.["Nat", "Prelude"]}:{type const tag=8,0}).
{TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
)]
getGoal=({hole_2},{
TT:Parameter name ref
NameType={type const tag=8,0}
TTName={`{{Nat}}.["Nat", "Prelude"]}
TT={TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
)
getHoles=[{hole_2},{hole_0}] |
| getGuess | error no guess |
Holes:
x : Prelude.Nat.Nat
----------------------------------
{hole_2} : Prelude.Nat.Nat
----------------------------------
{hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
Term:
?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} |
|
| Place a term into a hole, unifying its type | fill (Var `{{x}}) |
 |
|
 |
|
?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0} |
|
getEnv getGoal getHoles |
getEnv=[(`{{x}}, {λ ({`{{Nat}}.["Nat", "Prelude"]}:
{type const tag=8,0}).
{TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
)]
getGoal=({hole_2},
{TT:Parameter name ref
NameType={type const tag=8,0}
TTName={`{{Nat}}.["Nat", "Prelude"]}
TT={TT:TType
tt=ext=./Prelude/Nat.idr#20
}
})
getHoles=[{hole_2}, {hole_0}] |
| getGuess | {TT:Parameter name ref
NameType=NameType just bound by intro
TTName=`{{x}}
TT={TT:Parameter name ref
NameType={type const tag=8,0}
TTName={`{{Nat}}.["Nat", "Prelude"]}
TT={TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
} |
Holes:
x : Prelude.Nat.Nat
----------------------------------
{hole_2} : Prelude.Nat.Nat
----------------------------------
{hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
Term:
?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
|
|
| Substitute a guess into a hole. | solve |
 |
|
?{hole_0} ≈ λ x . x . {hole_0} |
|
getEnv getGoal getHoles |
getEnv=[]
getGoal=({hole_0}, {TT:Bind
name=`{{__pi_arg}}
binder={
Π ({`{{Nat}}.["Nat", "Prelude"]}:
{type const tag=8,0}).{TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
tt={TT:Parameter name ref
NameType={type const tag=8,0}
TTName={`{{Nat}}.["Nat","Prelude"]}
TT={TT:TType tt=ext=./Prelude/Nat.idr#20}
}
})
getHoles=[{hole_0}] |
| getGuess | {TT:Bind
name=`{{x}}
binder={λ ({`{{Nat}}.["Nat","Prelude"]}:{type const tag=8,0}).{
TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
tt={TT:Parameter name ref
NameType=NameType just bound by intro
TTName=`{{x}}
TT={TT:Parameter name ref
NameType={type const tag=8,0}
TTName={`{{Nat}}.["Nat", "Prelude"]}
TT={TT:TType
tt=ext=./Prelude/Nat.idr#20
}
}
} |
Holes:
----------------------------------
{hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
Term:
?{hole_0} ≈ λ x . x . {hole_0} |
