Elaborator Reflection - Example 1

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.

tree

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: 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
             
     
Term: 
        ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
Introduce a lambda binding around the current hole and focus on the body.
         intro `{{x}}
  example 2
  logic example 1 2
 
?{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}})
  example 1 3
  logic example 1
 
?{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
   
  logic example 1 4
 
?{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}

 

 


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.