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} |