Elaborator Reflection - Example 2

As an example of elaborator reflection here we step through this identity implementation: 
mkId : Elab ()
mkId = do
    x <- gensym "x"
    attack
    intro x
    fill (Var x)
    solve
    solve

natId : Nat -> Nat
natId = %runElab mkId

 

  

After each tactic we will look at the state:

We start with the type signature like this: 
mkId : Elab ()
mkId = do
    x <- gensym "x"
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: proof state 1
We can also look at the logic at each stage: example 1 logic 1
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
. 
         attack
  example 2
  logic example 1 2
Term: 
?{hole_0} ≈ ?{hole_2} ≈ ? {hole_6} . {hole_6} . {hole_2} . {hole_0}

getEnv

getGoal

getHoles

 
getEnv=[]

getGoal=({hole_6}, {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_6},
             {hole_2}, {hole_0}]
getGuess

Not a guess

  
 Holes:
             ----------------------------------
             {hole_6} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
             
             ----------------------------------
             {hole_2} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
             
             ----------------------------------
             {hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
  
         intro x
  example 1 3
  logic example 1
Term: 
?{hole_0} ≈ ?{hole_2} ≈ λ {x_105} . ? {hole_6} . {hole_6} . {hole_2} .
               {hole_0}

getEnv

getGoal

getHoles

 
getEnv=[({x_105}, {λ ({`{{Nat}}.["Nat", "Prelude"]}:{type const
             tag=8,0}).{TT:TType

             tt=ext=./Prelude/Nat.idr#20
}
})]

getGoal=({hole_6},
             {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_6},
             {hole_2}, {hole_0}]
getGuess

not a guess
  
 Holes:
             {x_105} : Prelude.Nat.Nat
             ----------------------------------
             {hole_6} : Prelude.Nat.Nat
             
             ----------------------------------
             {hole_2} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
             
             ----------------------------------
             {hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
Substitute a guess into a hole. 
         fill (Var x)
   
  logic example 1 4
Term: 
?{hole_0} ≈ ?{hole_2} ≈ λ {x_105} . ?{hole_6} ≈ {x_105} . {hole_6} .
                           {hole_2} .
               {hole_0}

getEnv

getGoal

getHoles

 
getEnv=[({x_105}, {λ ({`{{Nat}}.["Nat", "Prelude"]}:{type const
             tag=8,0}).{TT:TType

             tt=ext=./Prelude/Nat.idr#20
}
})]

getGoal=({hole_6},
             {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_6},
             {hole_2}, {hole_0}]
getGuess 
{TT:Parameter name ref
 NameType=NameType just bound by intro

             TTName={x_105}
 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_105} : Prelude.Nat.Nat
             ----------------------------------
             {hole_6} : Prelude.Nat.Nat
             
             ----------------------------------
             {hole_2} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
             
             ----------------------------------
             {hole_0} : (__pi_arg : Prelude.Nat.Nat) -> Prelude.Nat.Nat
   
  logic example 1 4
  
x

getEnv

getGoal

getHoles

 
x
getGuess 
x
  
x
   
  logic example 1 4
  
x

getEnv

getGoal

getHoles

 
x
getGuess 
x
  
x

 

 

metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.