F Khattar

F Dornaika

Franck Luthon
email: franck.luthon@univ-pau.fr

Benoît Quadcopter Larroque

Control

Khattar Fawzi
email: fawzi.khattar@univ-pau.fr

Dornaika Fadi
email: fadi.dornaika@ehu.eus

Luthon Franck

Larroque Benoit
email: benoit.larroque@univ-pau.fr

Quadcopter Control Using Onboard Monocular Camera for Enriching Remote Laboratory Facilities

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

I. INTRODUCTION

Remote labs constitute an interesting and novel way of doing labs. Anywhere and at anytime the student can access the lab equipment and do his labwork. This new way of distance learning can be used to increase the motivation of nowadays students, especially if it is coupled with new technologies like quadcopters [START_REF] Luthon | Use of gaming and computer vision to drive student motivation in remote learning lab activities[END_REF].

Quadcopters equipped with a camera can be used in these laboratories in order to mimic the student behavior in traditional lab and increase motivation for learning. It can be an interesting way to make the lab experience immersive and ludic. Specifically, in remote electronics laboratories it can fly and move in 3D space to inspect electrical instruments, consequently sending direct visual feedback of the results of an experiment in a new interesting way to the student. To achieve this, and to make the process autonomous two systems are needed. First, a localization system that can estimate the position and orientation of the quadcopter in 3D space with respect to an object of interest (front panel of an electrical instrument in our case). Second, a control system that sends appropriate commands to the quadcopter in order to reach a desired relative or absolute 3D position.

Many localization systems and sensors can be used in order to estimate quadcopter position and orientation in 3D space. For outdoor environments, GPS sensors constitute the best solution to localize a quadcopter. For indoor environments, artificial markers can be placed in the scene to facilitate the task of localization [START_REF] Eberli | Vision based position control for MAVs using one single circular landmark[END_REF]. These markers can also be reflective and detected by an external localization system that gives accurate position estimate. However, the challenge in these applications is to use only available on-board sensors. Different sensors can be used to gather information about the environment and localize the quadcopter. Stereo rig cameras [START_REF] Schauwecker | On-board dual-stereo-vision for the navigation of an autonomous MAV[END_REF] and RGBD cameras [START_REF] Flores | A vision and GPS-based real-time trajectory planning for a MAV in unknown and low-sunlight environments[END_REF] have been investigated. Using stereo or RGBD cameras allows for absolute pose estimate however this comes with an additional weight and power consumption. In this work we used the Parrot AR Drone 2.0 [5], a low cost quadcopter equipped with two monocular cameras facing forwards and downwards, in addition to pressure, ultrasound and inertial sensors. Using the monocular cameras available on-board constitutes a good trade-off between weight and information recovery from the environment (3D localization, environment recognition, etc.). However, a monocular camera alone cannot give absolute scale pose estimate due to the well known scale ambiguity rising from the perspective projection of 3D world into 2D images. Despite this fact, combining the visual information with some prior knowledge of 3D world or other sensors, that can give partial but absolute pose estimate, can overcome this issue and allow for absolute 3D pose estimate. In [START_REF] Engel | Scale-aware navigation of a low-cost quadrocopter with a monocular camera[END_REF] authors use the well known SLAM algorithm PTAM (Parallel tracking and mapping) [START_REF] Klein | Parallel tracking and mapping for small AR workspaces[END_REF] and combine it with inertial and ultrasound sensors readings in order to get the absolute 3D pose estimate. They fuse all the available information in a Kalman filter allowing for information fusion and delay compensation. In the present implementation, we build on their system and use it for 3D pose estimation when the quadcopter is exploring the 3D world. However, since the visual SLAM relies on corresponding points detected in the flow of images, it will drastically fail to give 3D pose estimate if the quadcopter is asked to inspect an object of interest, since these points will disappear when the object of interest occupies the majority of the image pixels. In this scenario, the quadcopter must move to a position near the object of interest which will cause the visual tracking of points to fail because there are not enough points available in the field of view of the camera. To overcome this limitation, this system is extended by using the object of interest as a landmark. In this way two localization modules are available: a visual SLAM module (needed for localization w.r.t. an arbitrary world coordinate system) and a localization module that relies on detecting and localizing a planar object with respect to the quadcopter and to the arbitrary world coordinate system (needed for controlling the remote lab activities and sending visual feedback to the student). The first module is suitable while exploring the environment whereas the latter is suitable when the quadrocopter is in a short distance range from the object of interest or when it needs to land on a landing zone. The paper is organised as follows: In the second section we present an overview of the remote electronic lab LaboREM. In section 3 we explain how detection and 3D localization can be carried out for a given planar object of interest. Based on the planar assumption the homography transform is estimated in order to estimate the quadcopter-object relative pose. It also presents the 3D pose visual servoing of the quadcopter. In the final section, we present some experiments and results.

II. REVIEW OF THE REMOTE ELECTRONICS LAB

LaboREM is a remote laboratory in electronics developed for first year undergraduate students in engineering. The learning objective of LaboREM is to enable students to wire and test remotely electronic circuits, make measurements and characterize each circuit by its time or frequency response. The electronic circuits consist of operational amplifiers, active filters and oscillators. Its design is based on a classic clientserver architecture [START_REF] Luthon | LaboREM a remote laboratory for game-like training in electronics[END_REF]. The student calls for a lab session by simple URL addressing. A first-in first-out strategy is adopted to give access to the remote lab to one client (student) at a time. A 5 minute connection is allotted to each student for one short manipulation. If he wants to repeat, he has to queue again. The remote lab application is developed using NI-LabVIEW software and the easy-to-use RFP protocol to pilot the remote devices. The hardware setup is shown in Figure 1. It includes: (i) a robotic arm that mimics the student's hand for placing electronic components equipped with magnets on an electronic breadboard, (ii) measurement instruments and data acquisition system (DAQ), (iii) a webcam with zoom control that mimics the student's eye in order that the student doesn't feel so far away from what is actually happening in the lab, (iv) a quadcopter (AR quadcopter 2.0) with the role of flying in the lab for exploring the environment and inspecting electrical instruments in order to increase student immersion and motivation. The pedagogical scenario for the lab activity is based on a game-like approach: it includes a treasure hunt and a Top10 of the best measurements. Technically, the game scenario is built on four basic concepts like in e-games: time spent, score or mark obtained for an activity, level (beginner, medium, advanced) and number of lives or repetitions allowed.

III. PROPOSED IMPLEMENTATION

A. Quadcopter-Object relative 3D pose : A real-time and marker free solution Planar objects are a well defined type of objects that are widely available in human made environments. Incorporating the information that the object of interest is planar is of great benefit for camera object pose estimation. Suppose we want to determine the 3D rigid transformation from the planar object coordinate system to the camera coordinate system by using the projection of that object into the image. Suppose the coordinate system attached to the planar object is chosen in a way that the object lies in its XY plane. Any point (X i , Y i , 0, 1) on the object will thus have zero Z coordinate. Using the pinhole camera model, a point on the object (X i , Y i , 0, 1) will be projected to an image point p i as follows:

p i = s[u i , v i , 1] T = KT ×     X i Y i 0 1     =   α u 0 u c 0 α v v c 0 0 1     r 11 r 12 r 13 t x r 21 r 22 r 23 t y r 31 r 32 r 33 t z       X i Y i 0 1     =   α u 0 u c 0 α v v c 0 0 1     r 11 r 12 t x r 21 r 22 t y r 31 r 32 t z     X i Y i 1   =   h 11 h 12 h 13 h 21 h 22 h 23 h 31 h 32 h 33     X i Y i 1   α u , α v are
the focal length in image pixel coordinate system and u c , v c are the coordinate of the principal point in the same coordinate system. r ij and t i denotes the elements of the rotation transformation and the translation transformation respectively. s denotes the scale parameter. The 3 by 3 matrix H is called homography and it encapsulates the intrinsic and extrinsic parameters. Once this matrix is estimated, the aim is to extract the extrinsic parameters and use them for controlling the quadcopter using the paradigm of 3D pose-based servoing. However, due to scale ambiguity arising from perspective projection, there is not one single H matrix that can map the 3D points to the 2D points but a 1D vectorial space of 3 by 3 matrices H λ = λ K T . The ambiguity can be eliminated by forcing the rotation matrix to be orthonormal and by having prior information about the dimensions of the object. From this homography matrix, one can directly calculate the rotation and translation matrix as follows [START_REF] Medioni | Emerging topics in computer vision[END_REF]:

  r 11 r 21 r 31   = 1 λ K -1   h 11 h 21 h 31     r 12 r 22 r 32   = 1 λ K -1   h 12 h 22 h 32     r 13 r 23 r 33   =   0 -r 31 r 21 r 31 0 -r 11 -r 21 r 11 0     r 12 r 22 r 32     t x t y t z   = 1 λ K -1   h 13 h 23 h 33   λ = K -1   h 11 h 21 h 31  

B. Estimating the homography matrix

In order to estimate the homography matrix that maps any plane into another plane by means of perspective projections several methods can be used. These methods are usually classified into local (feature-based) and global (featureless) methods.

Given a template image of the planar object, local methods extract local keypoints and attribute a descriptor to each of them both in the template image and the current image. After this step, keypoints (at least four keypoints) in both images are matched according to a similarity metric performed on the descriptors. Given the point correspondences, the homography matrix is estimated using robust methods like RANSAC (Random Sample Consensus) in order to deal with the presence of outlier correspondences. Local methods can work well with no prior information on the homography parameters. However, in some cases the robust computation may be computationally expensive and do not work in real time. Different descriptors exist like SIFT [START_REF] David G Lowe | Object recognition from local scale-invariant features[END_REF], SURF [START_REF] Bay | Speeded-up robust features (SURF)[END_REF], ORB [START_REF] Rublee | ORB: An efficient alternative to SIFT or SURF[END_REF], BRIEF [START_REF] Calonder | Brief: Binary robust independent elementary features[END_REF] and many others. A survey about keypoint detectors and descriptors can be found in [START_REF] Krig | Interest point detector and feature descriptor survey[END_REF].

On the other hand, the global methods use all the information in the image and attempt to find the homography matrix that best aligns the template patch to the test image. This process however gives rise to non linear minimization problems that can be solved using iterative algorithms like gradient descent or Levenberg-Marquardt. Thus, a good initialization is necessary to guarantee the convergence of those algorithms. Different similarity functions exist to measure the degree to which two patches are aligned, the most used ones being the sum of squared distance (SSD) and the enhanced correlation coefficient (ECC) [START_REF] Georgios | Parametric image alignment using enhanced correlation coefficient maximization[END_REF]. In practice the first one uses a brightness model in order to cope with variation of additive and multiplicative change of illumination [START_REF] Dornaika | Registering conventional images with low resolution panoramic images[END_REF] whereas the latter is by definition insensitive to those illumination changes. These methods have the advantage that they can run in real time and give good results if a rough estimate of the homography parameters is known. Thus the two families of methods are complementary: The first one is robust with no priors needed but computationally expensive, while the second is fast and works well if a prior is available.

Here, both approaches are used in order to estimate the 3D pose of the quadcopter with respect to the object of interest. The first approach is used for detecting the object of interest as well as for recovering from a tracking loss. The second is used in the tracking process. The approach is divided into two steps: detection and tracking. In the detection step, template matching on a pyramid of the image is used to search for the desired object. Once the detection is done, a homography transformation is computed by using the bounding box of the detected object to determine the quadcopter-object relative pose. A command is then sent to the drone in order to move it closer to the object. Template matching is used to allow successful detection of the object despite its distance from the camera and its size, as keypoints detector (SIFT) fails to detect and put in correspondences keypoints if the object of interest doesn't occupy a certain amount of image pixels. However once the quadcopter's camera is close to the object we use the SIFT descriptor to allow more robustness to orientation changes. Once the object is detected, the tracking stage begins. As a rough estimation of the homography matrix is available from the detection stage, it is used as an initial solution for the next frame and the ECC algorithm is applied to estimate the homography in this frame. The homography estimation is propagated in this way from a frame to the next one, and used as a prior for the ECC algorithm. However, sometimes the ECC algorithm will fail to converge due to several reasons. For example, communication problems between the quadcopter and the computer makes the last estimated homography not close enough to the real solution of the current frame, which prevents algorithm convergence. Besides, the image quality can be degraded by motion blur or decoding/encoding problems. In this work, tracking loss is declared if the ECC algorithm is unable to converge or if it converges to a clearly unrealistic estimation. At each frame, we compute the 3D pose of the quadcopter with respect to the planar object. By monitoring the differences in the position of the quadcopter along time, we can detect a loss of tracking by setting a threshold on the difference of two consecutive pose estimates (position and orientation) which works well in practice. For example if the distance traveled in 3D space during two consecutive frames is larger than 30 cm, it is clear that the tracking is not correct and the pose is erroneous. In the latter case, we resort back to the local method (SIFT) if the quadcopter-object distance is relatively small, or to the template matching method in the other case, to reinitialize the ECC tracker as shown in Figure 2. This pose estimate is fused with inertial measurements sent by the drone in a Kalman filter framework in order to smooth this estimate, and to provide robustness when the visual tracker fails. The Kalman filter is used also to compensate for time delays as done in [START_REF] Engel | Scale-aware navigation of a low-cost quadrocopter with a monocular camera[END_REF]. The homography estimation process is shown in Figure 2.

C. Visual control of the quadcopter

In order to control the 3D position and orientation of the quadcopter, a feedback control loop is used with two complementary sensors. One of the sensors is used for feedback at a time. The approach in [START_REF] Engel | Scale-aware navigation of a low-cost quadrocopter with a monocular camera[END_REF] is used, taking as input video stream, ultrasound and inertial measurements when the quadcopter is exploring the environment far from the object of interest and when the quadcopter needs to return to the base station. The homography algorithm fused with inertial measurements is used when the quadcopter is inspecting the object of interest at a close distance. In this way, lost of localization is avoided when the quadcopter is approaching the instrument which allows for autonomous object inspection and environment exploration. The pose derived from either source is used in a closed servoing loop. The control loop is shown in Figure 3. The controlled degrees of freedom associated with the quadcopter are the 3D translation and the yaw angle. Each degree is controlled by a closed loop control system with a Fig. 2. Diagram showing the homography estimation process for each input video frame. The object is declared detected if the normalized correlation is greater than 0.8 in the case of template matching and if the Number of corresponding keypoints is greater than 8 in the case of SIFT. The object is declared tracked correctly if the estimated distance travelled between two consecutives frames is less than 30 cm or difference of yaw, roll or pitch angle is less than 15 degrees. traditional PID controller. The other two rotational degrees of freedom (pitch and roll) cannot be used since they do not allow for position holding, they are used by the on-board embedded system on the AR Drone 2.0 to allow the quadcopter to move in different directions.

IV. EXPERIMENTS

In order to evaluate the proposed implementation of 3D pose estimation and 3D pose-based servoing, we design three different scenarios. These scenarios are the following: behavior of the system in response to perturbations when asked to inspect an object, autonomous visual inspection of planar object, and autonomous landing. In all these scenarios, the controlled degrees of freedom associated with the quadcopter are the 3D translation and the yaw angle.

a) First scenario: The first experiment is done to test the quality of the homography based visual feedback control system. To this end, we control the quadcopter in such a way that the desired 3D pose of its on-board camera is frontoparallel to the planar object with a translation vector allowing a centered view. The pose used for the visual feedback control is the homography based pose. Since the servoing objective is to maintain a rigid link between the quadcopter and the object of interest, any motion induced to the object will force the quadcopter to compensate for it. We can induce such motion by a walking person that carries the object or by giving manual kicks to the quadcopter. The quadcopter then follows the object, centering it in the image as show in Figure 5. Two videos of this scenario are available online [17], [18].

b) Second scenario: In remote lab context, an interesting scenario is the following: the remote student will send a command to the quadcopter to go and inspect an electrical device. After receiving this command, the server tells the quadcopter to carry out the following tasks: it should first take off, initialize the SLAM algorithm, and initiate a search procedure for the required instrument. In a general case, to be able to search for the instrument a path planning and search algorithm must be used. However, here this is simplified by considering that the electrical instrument is already in the camera field of view and hence only detection and servoing are required. The instrument is searched for in the image by using template matching applied on the pyramid of the image to cope with scale change. Once the object is detected, the homography from the 3D world plane of the electrical instrument to the image plane is estimated. Based on the estimated homography, the 3D pose is estimated. We have now a 3D rigid transformation between coordinate systems of the instrument and the camera. Since the 3D pose of the quadcopter with respect to the visual SLAM coordinate system is known, the 3D pose of the planar object in that coordinate system can be calculated by cascading multiple rigid transforms between coordinate systems as shown in Figure 4. Thus, two localization sources are now available for visual feedback control. Based on the pose that is provided, it is possible to control the quadcopter through visual servoing in order to have a rigid link between the quadcopter and the instrument. To this end, at any time one needs the current localization information for the feedback control loops of the quadcopter. We emphasize the fact that the two sources of localization cannot be both available for all configurations and for all actual poses of the quadcopter. Indeed, the visual SLAM works well when there is enough keypoints in the image to detect and put in correspondence with 3D map points. However, as the quadcopter approaches the planar instrument, most of the keypoints will disappear and the visual SLAM algorithm might loose tracking. In the latter case, we use the 3D pose estimate given by the homography algorithm. In this way the quadcopter is able to fly and inspect an electrical instrument as shown in figure 6.

c) Third scenario: Another scenario is getting the quadcopter home. The same principle is used, by relying on the homography algorithm to fly away from the electrical instrument and then switching to the visual SLAM to go back to the start point. Once being there, the bottom camera of the quadcopter and the homography algorithm are used to detect a landing zone. By doing that, the landing maneouvre can be acheived in an accurate manner. The ECC and the SIFT based homography estimation are both robust to partial occlusion as shown in figure 7 V. CONCLUSION This paper presents the implementation of a visual servoing system of a quadcopter in a remote lab environment to increase student immersion in the lab and hence his motivation. The localization system is based on two complementary algorithms that work in real-time at video rate in different scenarios. Qualitative results are presented demonstrating the ability to use a low cost quadcopter to inspect an object of interest and return to its base autonomously using only its on-board sensors. For future work, we intend to allow remote studentteacher interaction by using visual servoing for quadcopter control in order to follow and track the teacher's face.

Fig. 1 .

 1 Fig. 1. Main components of the remote lab LaboREM.

Fig. 3 .

 3 Fig. 3. Control loop using either the visual SLAM when exploring the environment or the homography estimation algorithm when inspecting a planar object at a short distance.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Different coordinate systems and rigid transformations used in the application.

  . A video showing the hovering and landing maneouvre is available online [19]. The image-based localization and control work in real-time at an average of 30 FPS in different scenarios.

Fig. 6 .

 6 Fig.6. Localization based on an electrical instrument (oscilloscope): From left to right, images taken from the quadcopter video stream that show how the system can control the quadcopter to obtain a front view of the instrument.

Fig. 7 .

 7 Fig.7. Visual servoing for homing. On the left: the quadcopter hovering above the landing template and performing a controlled landing. On the right: the view seen from the bottom camera of the quadcopter that shows robustness to occlusion (when the landing object is partially out of the field of view).


Abhishek Anand

Simon Boulier

Cyril Cohen

Matthieu Sozeau

Nicolas Tabareau

Towards Certified Meta-Programming

come

Introduction

Meta-programming is the art of writing programs (in a meta-language) that produce or manipulate programs (written in an object language). In the setting of dependent type theory, the expressivity of the language permits to consider the case were the meta and object languages are actually the same, accounting for well-typedness. This idea has been pursued in the work on inductive-recursive (IR) and quotient inductive-inductive types (QIIT) in Agda to reflect a syntactic model of a dependently-typed language within another one [START_REF] Chapman | Type Theory Should Eat Itself[END_REF][START_REF] Altenkirch | Type Theory in Type Theory Using Quotient Inductive Types[END_REF]. These term encodings include type-correcteness internally by considering only well-typed terms of the syntax, i.e. derivations. However, the use of IR or QIITs complicates considerably the meta-theory of the meta-language which makes it difficult to coincide with the object language represented by an inductive type. More problematically in practice, the concision and encapsulation of the syntactic encoding has the drawback that it is very difficult to use because any function from the syntax can be built only at the price of a proof that it respects typing, conversion or any other features described by the intrinsically typed syntax right away.

Other works have taken advantage of the power of dependent types to do meta-programming in a more progressive manner, by first defining the syntax of terms and types; and then defining out of it the notions of reduction, conversion and typing derivation [START_REF] Devriese | Typed Syntactic Meta-programming[END_REF][START_REF] Van Der Walt | Engineering Proof by Reflection in Agda[END_REF] (the introduction of [START_REF] Devriese | Typed Syntactic Meta-programming[END_REF] provides a comprehensive review of related work in this area). This can be seen as a type-theoretic version of the functional programming language designs such as Template Haskell [START_REF] Sheard | Template Meta-programming for Haskell[END_REF] or MetaML [START_REF] Taha | Multi-stage Programming with Explicit Annotations[END_REF]. This is also the approach taken by Malecha in his thesis [START_REF] Malecha | Extensible Proof Engineering in Intensional Type Theory[END_REF], where he defined Template-Coq, a plugin which defines a correspondence-using quoting and unquoting functions-between Coq kernel terms and inhabitants of an inductive type representing internally the syntax of the calculus of inductive constructions (CIC), as implemented in Coq. It becomes thus possible to define programs in Coq that manipulate the representation of Coq terms and reify them as functions on Coq terms. Recently, its use was extended for the needs of the CertiCoq certified compiler project [START_REF] Anand | CertiCoq: A verified compiler for Coq[END_REF], which uses it as its front-end language. It was also used by Anand and Morissett [START_REF] Anand | Revisiting Parametricity: Inductives and Uniformity of Propositions[END_REF] to formalize a modified parametricity translation, and to extract Coq terms to a CBV λ-calculus [START_REF] Forster | Verified Extraction from Coq to a Lambda-Calculus[END_REF]. All of these translations however lacked any means to talk about the semantics of the reified programs, only syntax was provided by Template-Coq. This is an issue for CertiCoq for example where both a non-deterministic small step semantics and a deterministic call-by-value big step semantics for CIC terms had to be defined and preserved by the compiler, without an "official" specification to refer to. This paper proposes to remedy this situation and provides a formal semantics of Coq's implemented type theory, that can independently be refined and studied. The advantage of having a very concrete untyped description of Coq terms (as opposed to IR or QIITs definitions) together with an explicit type checker is that the extracted type-checking algorithm gives rise to an OCaml program that can directly be used to type-check Coq kernel terms. This opens a way to a concrete solution to bootstrap Coq by implementing the Coq kernel in Coq. However, a complete reification of CIC terms and a definition of the checker are not enough to provide a meta-programming framework in which Coq plugins could be implemented. One needs to get access to Coq logical environments. This is achieved using a monad that reifies Coq general commands, such as lookups and declarations of constants and inductive types.

As far as we know this is the only reflection framework in a dependently-typed language allowing such manipulations of terms and datatypes, thanks to the relatively concise representation of terms and inductive families in CIC. Compared to the MetaCoq project [START_REF] Ziliani | Mtac: A Monad for Typed Tactic Programming in Coq[END_REF], Lean's tactic monad [START_REF] Ebner | A Metaprogramming Framework for Formal Verification[END_REF], or Agda's reflection framework [START_REF] Van Der Walt | Engineering Proof by Reflection in Agda[END_REF], our ultimate goal is not to interface with Coq's unification and type-checking algorithms, but to provide a self-hosted, bootstrappable and verifiable implementation of these algorithms. On one hand, this opens the possibility to verify the kernel's implementation, a problem tackled by Barras [6] using set-theoretic models. On the other hand we also advocate for the use of Template-Coq as a foundation on which higher-level tools can be built: metaprograms implementing translations, boilerplate-generating tools, domain-specific proof languages, or even general purpose tactic languages.

Inductive term : Set | tRel : N → term | tVar : ident → term | tEvar : N → list term → term | tSort : universe → term | tCast : term → cast_kind → term → term | tProd : name → term → term → term | tLambda : name → term → term → term | tLetIn : name → term → term → term → term | tApp : term → list term → term | tConst : kername → universe_instance → term | tInd : inductive → universe_instance → term | tConstruct: inductive → N → universe_instance → term | tCase : inductive * N → term → term → list (N * term) → term | tProj : projection → term → term | tFix : mfixpoint term → N → term | tCoFix : mfixpoint term → N → term.
Plan of the paper. In Section 2, we present the complete reification of Coq terms, covering the entire CIC and define in Section 3 the type-checking algorithm of Coq reified terms in Coq. In Section 4, we show the definition of a monad for general manipulation of Coq's logical environment and use it to define plugins for various translations from Coq to Coq (Section 5). Finally, we discuss related and future work in Section 6. On the converse, the command Make Definition constructs a term from its syntax. This example below defines zero to be 0 of type N. where mkInd n k is the k th inductive of the mutual block of the name n.

Reification of Coq Terms

Reification of environment. In Coq, the meaning of a term is relative to an environment, which must be reified as well. Environments consist of three parts: (i) a graph of universes (ii) declarations of definitions, axioms and inductives (iii) a local context registering types of De Bruijn indexes.

As we have seen in the syntax of terms, universe levels are not given explicitly in Coq. Instead, level variables are introduced and constraints between them are registered in a graph of universes. This is the way typical ambiguity is implemented in Coq. A constraint is given by two levels and a constraint_type (Lt, Le or Eq):

Definition univ_constraint

Level * constraint_type * Level.

Then the graph is given by a set of level variables and one of constraints. Sets, coming from the Coq standard library, are implemented using lists without duplicates. LevelSet.t means the type t of the module LevelSet.

Functions to query the graph are provided, for the moment they rely on a naive implementation of the Bellman-Ford algorithm. check_leq u1 u2 checks if the graph enforces u1 ≤ u2 and no_universe_inconsistency checks that the graph has no negative cycle. Constant and inductive declarations are grouped together, properly ordered according to dependencies, in a global context (global_ctx), which is a list of global declarations (global_decl).

Inductive global_decl | ConstantDecl : ident → constant_decl → global_decl | InductiveDecl : ident → minductive_decl → global_decl.
Definitions and axioms just associate a name to a universe context, and two terms for the optional body and type. Inductives are more involved: In Coq internals, there are in fact two ways of representing a declaration: either as a "declaration" or as an "entry". The kernel takes entries as input, type-check them and elaborate them to declarations. In Template-Coq, we provide both, and provide an erasing function mind_decl_to_entry from declarations to entries for inductive types.

Finally, local contexts are just list of local declarations: a type for lambda bindings and a type and a body for let bindings.

Quoting and unquoting the environment Template-Coq provides the command Quote Recursively Definition to quote an environment. This command crawls the environment and quote all declarations needed to typecheck a given term.

The other way, the commands Make Inductive allows declaring an inductive type from its entry. For instance the following redefines a copy of

Σ) t u = true → Σ ; Γ t ≤ u | cumul_red_l t u v : red1 Σ Γ t v → Σ ; Γ v ≤ u → Σ ; Γ t ≤ u | cumul_red_r t u v : Σ ; Γ t ≤ v → red1 Σ Γ u v → Σ ; Γ t ≤ u where " Σ ; Γ t ≤ u " (cumul Σ Γ t u).
Inductive typing (Σ : global_ctx More examples of use of quoting/unquoting commands can be found in the file test-suite/demo.v.

) (Γ : context) : term → term → Set | type_Rel n : ∀ (H : n < List.length Γ ), Σ ; Γ tRel n : lift0 (S n) (safe_nth Γ (exist _ n H)).(decl_type) | type_Sort (l : level) : Σ ; Γ tSort (Universe.make l) : tSort (Universe.super l) | type_Prod n t b s1 s2 : Σ ; Γ t : tSort s1 → Σ ; Γ , vass n t b : tSort s2 → Σ ; Γ tProd n t b : tSort (max_universe s1 s2) | type_App t l t_ty t' : Σ ; Γ t : t_ty → typing_spine Σ Γ t_ty l t' → Σ ; Γ tApp t l : t' | ... where " Σ ; Γ t : T " (typing Σ Γ t T) with typing_spine Σ Γ : term → list term → term → Prop | type_spine_nil ty : typing_spine Σ Γ ty [ ] ty | type_spine_const hd tl na A B B' T : Σ ; Γ T ≤ tProd na A B → Σ ; Γ hd : A → typing_spine Σ Γ (subst0 hd B) tl B' → typing_spine Σ Γ T (cons hd tl) B'

Type Checking Coq in Coq

In Fig. 2, we present (an excerpt of) the specification of the typing judgment of the kernel of Coq using the inductive type typing. It represents all the typing rules of Coq6 . This includes the basic dependent lambda calculus with lets, global references to inductives and constants, the match construct and primitive projections. Universe polymorphic definitions and the well-formedness judgment for global declarations are dealt with as well.

The only ingredients missing are the guard check for fixpoint and productivity of cofixpoints and the positivity condition of mutual (co-) inductive types. They are work-in-progress.

The typing judgment typing is mutually defined with typing_spine to account for n-ary applications. Untyped reduction red1 and cumulativity cumul can be defined separately.

Implementation. To test this specification, we have implemented the basic algorithms for type-checking in Coq, that is, we implement type inference: given a context and a term, output its type or produce a type error. All the rules of type inference are straightforward except for cumulativity. The cumulativity test is implemented by comparing head normal forms for a fast-path failure and potentially calling itself recursively, unfolding definitions at the head in Coq's kernel in case the heads are equal. We implemented weak-head reduction by mimicking Coq's kernel implementation, which is based on an abstract machine inspired by the KAM. Coq's machine optionally implements a variant of lazy, memoizing evaluation (which can have mixed results, see Coq's PR #555 for example), that feature has not been implemented yet.

The main difference with the OCaml implementation is that all of the functions are required to be shown terminating in Coq. One possibility could be to prove the termination of type-checking separately but this amounts to prove in particular the normalization of CIC which is a complex task. Instead, we simply add a fuel parameter to make them syntactically recursive and make OutOfFuel a type error, i.e., we are working in a variant of the option monad.

Bootstrapping it. We can extract this checker to OCaml and reuse the setup described in Section 2 to connect it with the reifier and easily derive a (partialy verified) alternative checker for Coq's .vo object files. Our plugin provides a new command Template Check for typechecking definitions using the alternative checker, that can be used as follows:

Require Import Template.TemplateCoqChecker List. Import ListNotations.

Definition foo

List.map (fun x ⇒ x + 3) [0; 1]. Template Check foo.

Our initial tests indicate that its running time is comparable to the coqchk checker of Coq, as expected.

Reification of Coq Commands

Coq plugins need to interact with the environment, for example by repeatedly looking up definitions by name, declaring new constants using fresh names, or performing computations. It is desirable to allow such programs to be written in Coq (Gallina) because of the two following advantages. Plugin-writers no longer need to understand the OCaml implementation of Coq and plugins are no longer sensitive to changes made in the OCaml implementation. Also, when plugins implementing syntactic models are proven correct in Coq, they provide a mechanism to add axioms to Coq without compromising consistency ( §5.3).

In general, interactions with the environment have side effects, e.g. the declaration of new constants, which must be described in Coq's pure setting. To overcome this difficulty, we use the standard "free" monadic setting to represent the operations involved in interacting with the environment, as done for instance in Mtac [START_REF] Ziliani | Mtac: A Monad for Typed Tactic Programming in Coq[END_REF]. TemplateMonad is an inductive family (Fig. 3) such that TemplateMonad A represents a program which will finally output a term of type A. There are special constructor tmReturn and tmBind to provide (freely) the basic monadic operations. We use the monadic syntactic sugar x ← t ; u for tmBind t (fun x ⇒ u).

The other operations of the monad can be classified in two categories: the traditional Coq operations (tmDefinition to declare a new definition, . . . ) and the quoting and unquoting operations to move between Coq term and their syntax or to work directly on the syntax (tmMkInductive to declare a new inductive from its syntax for instance). An overview is given in Table 1.

A program prog of type TemplateMonad A can be executed with the command Run TemplateProgram prog. This command is thus an interpreter for TemplateMonad programs, implemented in OCaml as a traditional Coq plugin. The term pro- The program below asks the user to provide an inhabitant of N (here we provide 3 * 3) and records it in the lemma foo ; prints its normal form ; and records the syntax of its normal form in foo_nf_syntax (hence of type term).

We use Program's obligation mechanism 7 to ask for missing proofs, running the rest of the program when the user finishes providing it. This enables the implementation of interactive plugins.

Run TemplateProgram (foo ← tmLemma "foo" N ;

nf ← tmEval all foo ; tmPrint "normal form: " ; tmPrint nf ; nf_ ← tmQuote nf ; tmDefinition "foo_nf_syntax" nf_). Next Obligation. exact (3 * 3). Defined.

Writing Coq plugins in Coq

The reification of syntax, typing and commands of Coq allow writing a Coq plugin directly inside Coq, without requiring another language like OCaml and an external compilation phase.

In this section, we describe three examples of such plugins: (i) a plugin that adds a constructor to an inductive type, (ii) a re-implementation of Lasson's parametricity plugin 8 , and (iii) an implementation of a plugin that provides an extension of CIC-using a syntactic translation-in which it is possible to prove the negation of functional extensionality [START_REF] Boulier | The Next 700 Syntactical Models of Type Theory[END_REF].

A Plugin to Add a Constructor

Our first example is a toy example to show the methodology of writing plugins in Template-Coq. Given an inductive type I, we want to declare a new inductive type I' which corresponds to I plus one more constructor.

For instance, let's say we have a syntax for lambda calculus:

Inductive tm : Set | var : nat → tm | lam : tm → tm | app : tm → tm → tm.
And that in some part of our development, we want to consider a variation of tm with a new constructor, e.g., let in. Then we declare tm' with the plugin by: Run TemplateProgram (add_constructor tm "letin" (fun tm' ⇒ tm' → tm' → tm')).

This command has the same effect as declaring the inductive tm' by hand:

Inductive tm' : Set | var' : nat → tm' | lam' : tm' → tm' | app' : tm' → tm' → tm' | letin : tm' → tm' → tm'.
but with the benefit that if tm is changed, for instance by adding one new constructor, then tm' is automatically changed accordingly. We provide other examples in the file test-suite/add_constructor.v, e.g. with mutual inductives.

We will see that it is fairly easy to define this plugin using Template-Coq. The main function is add_constructor which takes an inductive type ind (whose type is not necessarily Type if it is an inductive family), a name idc for the new constructor and the type ctor of the new constructor, abstracted with respect to the new inductive. It works in the following way. First the inductive type ind is quoted, the obtained term tm is expected to be a tInd constructor otherwise the function fails. Then the declaration of this inductive is obtained by calling tmQuoteInductive, the constructor is reified too, and an auxiliary function is called to add the constructor to the declaration. After evaluation, the new inductive type is added to the current context with tmMkInductive.

It remains to define the add_ctor auxiliary function to complete the definition of the plugin. It takes a minductive_decl which is the declaration of a block of mutual inductive types and returns a minductive_decl. [t]0 = t

[x]1 = x t [∀(x : A).B]1 = λf.∀(x : [A]0)(x t : [A]1x).[B]1(f x) [λ(x : A).t]1 = λ(x : [A]0)(x t : [A]1x).[t]1 Γ, x : A = Γ , x : [A]0, x t : [A]1 x Γ t : A Γ [t]0 : [A]0 Γ [t]1 : [A]1 [t]0
Fig. 4. Unary parametricity translation and soundness theorem, excerpt (from [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF])

The declaration of the block of mutual inductive types is a record. The field ind_bodies contains the list of declarations of each inductive of the block. We see that most of the fields of the records are propagated, except for the names which are translated to add some primes and ind_ctors, the list of types of constructors, for which, in the case of the relevant inductive (i0 is its number), the new constructor is added.

Parametricity Plugin

We now show how Template-Coq permits to define a parametricity plugin that computes the translation of a term following Reynolds' parametricity [START_REF] Reynolds | Types, Abstraction and Parametric Polymorphism[END_REF][START_REF] Wadler | Theorems for Free! In: Functional Programming Languages and Computer Architecture[END_REF]. We follow the already known approaches of parametricity for dependent type theories [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF][START_REF] Keller | Parametricity in an Impredicative Sort[END_REF], and provide an alternative to Keller and Lasson's plugin.

The definition in the unary case is described in Fig. 4. The soundness theorem ensures that, for a term t of type A, [t] 1 computes a proof of parametricity of [t] 0 in the sense that it has type [A] 1 [t] 0 . The definition of the plugin goes in two steps: first the definition of the translation on the syntax of term in Template-Coq and then the instrumentation to connect it with terms of Coq using the TemplateMonad. It can be found in the file translations/tsl param.v.

The parametricity translation of Fig. 4 is total and syntax directed, the two components of the translation [ ] 0 and [ ] 1 are implemented by two recursive functions tsl param0 and tsl param1.

Fixpoint tsl param0 (n : nat) (t : term) {struct t} : term match t with

| tRel k ⇒ if k >= n then (* global variable *) tRel (2*k-n+1) else (* local variable *) tRel k | tProd na A B ⇒ tProd na (tsl param0 n A) (tsl param0 (n+1) B) | _ ⇒ ... end. Fixpoint tsl param1 (E : tsl_table) (t : term) : term match t with | tRel k ⇒ tRel (2 * k) | tSort s ⇒ tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s)) | tProd na A B ⇒ let A0 tsl param0 0 A in let A1 tsl param1 E A in let B0 tsl param0 1 B in let B1 tsl param1 E B in tLambda (nNamed "f") (tProd na A0 B0) (tProd na (lift0 1 A0) (tProd (tsl_name na) (subst_app (lift0 2 A1) [tRel 0]) (subst_app (lift 1 2 B1) [tApp (tRel 2) [tRel 1] ]))) | tConst s univs ⇒ match lookup_tsl_table E (ConstRef s) with | Some t ⇒ t | None ⇒ default_term end | _ ⇒ ... end.
On Fig. 4, the translation is presented in a named setting, so the introduction of new variables does not change references to existing ones. That's why, [ ] 0 is the identity. In the De Bruijn setting of Template-Coq, the translation has to take into account the shift induced by the duplication of the context. Therefore, the implementation tsl param0 of [ ] 0 is not the identity anymore. The argument n of tsl param0 represents the De Bruijn level from which the variables have been duplicated. There is no need for such an argument in tsl param1, the implementation of [ ] 1 , because in this function all variables are duplicated.

The parametricity plugin not only has to be defined on terms of CIC but also on additional terms dealing with the global context. In particular, constants are translated using a translation table which records the translations of previously processed constants.

Definition tsl_table list (global_reference * term).

If a constant is not in the translation table we return a dummy default_term, considered as an error (this could also be handled by an option monad).

We have also implemented the translation of inductives and pattern matching. For instance the translation of the equality type eq produces the inductive type:

Inductive eq t A (A t : A → Type) (x : A) (x t : A t x) : ∀ H, A t H → x = H → Prop | eq_refl t : eq t A A t x x t x x t eq_refl.
Then [eq]1 is given by eq t and [eq_refl]1 by eq_refl t . Given tsl param0 and tsl param1 the translation of the declaration of a block of mutual inductive types is not so hard to get. Indeed, such a declaration mainly consists of the arities of the inductives and the types of constructors ; and the one of the translated inductive are produced by translation of the original ones.

Definition tsl_mind_decl (E : tsl_table) (kn : kername) (mind : minductive_decl) : minductive_decl.

In a similar manner, we can translate pattern-matching. Note that the plugin does not support fixpoints and cofixpoints for the moment. Now, it remains to connect this translation defined on reified syntax term to terms of Coq. For this, we define the new command tTranslate in the TemplateMonad.

Definition tTranslate (E : tsl_table) (id : ident) : TemplateMonad tsl_table.

When id is a definition, the command recovers the body of id (as a term) using tmQuoteConstant and then translates it and records it in a new definition id t . The command returns the translation table E extended by (id, id t ). In the case id is an inductive type or a constructor then the command does basically the same but extends the translation table with both the inductive and the constructors.

If id is an axiom or not a constant the command fails.

Here is an illustration coming from the work of Lasson [START_REF] Lasson | Canonicity of Weak ω-groupoid Laws Using Parametricity Theory[END_REF] on the automatic proofs of (ω-)groupoid laws using parametricity. We show that all function of type ID ∀ A x y, x = y → x = y are identity functions. First we need to record the translations of eq and ID in a term Then we show that every parametric function on ID is pointwise equal to the identity using the predicate fun y ⇒ x = y.

Lemma param_ID (f : ID) : ID t f → ∀ A x y p, f A x y p = p. Proof. intros H A x y p. destruct p. destruct (H A (fun y ⇒ x = y) x eq_refl x eq_refl eq_refl (eq_refl t _ _)). reflexivity. Qed.

Then we define a function myf p → p p -1 p and get its parametricity proof using the plugin. It is then possible to deduce automatically that p p -1 p = p for all p : x = y.

Definition free_thm_myf : ∀ A x y p, myf A x y p = p param_ID myf myf t .

Intensional Function Plugin

Our last illustration is a plugin that provides an intensional flavour to functions and thus allows negating functional extensionality (FunExt). This is a simple example of syntactical translation which enriches the logical power of Coq, in the sense that new theorems can be proven (as opposed to the parametricity translation which is conservative over CIC). See [START_REF] Boulier | The Next 700 Syntactical Models of Type Theory[END_REF] for an introduction to syntactical translations and a complete description of the intensional function translation.

Even if the translation is very simple as it just adds a boolean to every function (Fig. 5), this time, it is not fully syntax directed. Indeed the notation for pairs hide some types: and we can not recover the type ?T from the source term. There is thus a mismatch between the lambdas which are not fully annotated and the pairs which are. 9However we can use the type inference algorithm of Section 3 implemented on Template-Coq terms to recover the missing information.

[fun (

x:A) ⇒ t] let B infer Σ (Γ , x:[A]) t in pair (∀ (x:[A]). B) bool (fun (x:[A]) ⇒ [t]) true
Compared to the parametricity plugin, the translation function has a more complex type as it requires the global and local contexts. However, we can generalize the tTranslate command so that it can be used for both the parametricity and the intensional function plugins. The implementation is in the files translations/translation_utils.v and translations/tsl_fun.v.

Extending Coq using plugins. The intensional translation extends the logical power of Coq as it is possible for instance to negate FunExt. In this perspective, we defined a new command:

Definition tImplement (Σ : global_ctx * tsl_table) (id : ident) (A : Type) : TemplateMonad (global_ctx * tsl_table).

which computes the translation A' of A, then asks the user to inhabit the type A' by generating a proof obligation and then safely adds the axiom id of type A to the current context. By safely, we mean that the correction of the translation ensures that no inconsistencies are introduced.

For instance, here is how to negate FunExt. We use for that two pairs (fun x ⇒ x; true) and (fun x ⇒ x; false) in the interpretation of functions from unit to unit, which are extensionally both the identity, but differ intensionally on their boolean.

Run TemplateProgram (TC ← tTranslate ([ ],[ ]) "eq" ;

TC ← tTranslate TC "False" ; tImplement TC "notFunext" ((∀ A B (f g : A → B), (∀ x:A, f x = g x) → f = g) → False) where tIntro and tSpecialize are special versions of the corresponding intro and specialize tactics of Coq to deal with extra booleans appearing in the translated terms. After this command, the axiom notFunext belongs to the environment, as if it where added with the Axiom command. But as we have inhabited the translation of its type, the correcteness of the translation ensures that no inconsistency were introduced.

Note that we could also define another translation, e.g. the setoid translation, in which FunExt is inhabited. This is not contradictory as the two translations induce two different logical extensions of Coq, which can not be combined.

Related Work and Future Work

Meta-Programming is a whole field of research in the programming languages community, we will not attempt to give a detailed review of related work here. In contrast to most work on meta-programming, we provide a very rough interface to the object language: one can easily build ill-scoped and ill-typed terms in our framework, and staging is basic. However, with typing derivations we provide a way to verify meta-programs and ensure that they do make sense.

The closest cousin of our work is the Typed Syntactic Meta-Programming [START_REF] Devriese | Typed Syntactic Meta-programming[END_REF] proposal in Agda, which provides a well-scoped and well-typed interface to a denotation function, that can be used to implement tactics by reflection. We could also implement such an interface, asking for a proof of well-typedness on top of the tmUnquoteTyped primitive of our monad.

Intrinsically typed representations of terms in dependent type-theory is an area of active research. Most solutions are based on extensions of Martin-Löf Intensional Type Theory with inductive-recursive or quotient inductive-inductive types [START_REF] Chapman | Type Theory Should Eat Itself[END_REF][START_REF] Altenkirch | Type Theory in Type Theory Using Quotient Inductive Types[END_REF], therefore extending the meta-theory. Recent work on verifying soundness and completeness of the conversion algorithm of a dependent type theory (with natural numbers, dependent products and a universe) in a type theory with IR types [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF] gives us hope that this path can nonetheless be taken to provide the strongest guarantees on our conversion algorithm. The intrinsically-typed syntax used there is quite close to our typing derivations.

Another direction is taken by the OEuf certified compiler [START_REF] Mullen | OEuf: minimizing the Coq extraction TCB[END_REF], which restricts itself to a fragment of Coq for which a total denotation function can be defined, in the tradition of definitional interpreters advocated by Chlipala [START_REF] Chlipala | Certified Programming with Dependent Types[END_REF]. This setup should be readily accomodated by Template-Coq.

The translation+plugin technique paves the way for certified translations and the last piece will be to prove correctness of such translations. By correctness we mean computational soundness and typing soundness (see [START_REF] Boulier | The Next 700 Syntactical Models of Type Theory[END_REF]), and both can be stated in Template-Coq. Anand has made substantial attempts in this direction to prove the computational soundness, in Template-Coq, of a variant of parametricity providing stronger theorems for free on propositions [START_REF] Anand | Revisiting Parametricity: Inductives and Uniformity of Propositions[END_REF]. This included as a first step a move to named syntax that could be reused in other translations.

Our long term goal is to leverage this technique to extend the logical and computational power of Coq using, for instance, the forcing translation [START_REF] Jaber | The Definitional Side of the Forcing[END_REF] or the weaning translation [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF].

When performance matters, we can extract the translation to OCaml and use it like any ordinary Coq plugin. This relies on the correctness of extraction, but in the untyped syntax + typing judgment setting, extraction of translations is almost an identity pretty-printing phase, so we do not lose much confidence. We can also implement a template monad runner in OCaml to run the plugins outside Coq. Our first experiments show that we could gain a factor 10 for the time needed to compute the translation of a term. Another solution would be to use the certified CertiCoq compiler, once it supports a kind of foreign function interface, to implement the TemplateMonad evaluation.

The last direction of extension is to build higher-level tools on top of the syntax: the unification algorithm described in [START_REF] Ziliani | A Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading[END_REF] is our first candidate. Once unification is implemented, we can look at even higher-level tools: elaboration from concrete syntax trees, unification hints like canonical structures and type class resolution, domain-specific and general purpose tactic languages. A key inspiration in this regard is the work of Malecha and Bengston [START_REF] Malecha | ESOP 2016, chap. Extensible and Efficient Automation Through Reflective Tactics[END_REF] which implemented this idea on a restricted fragment of CIC.

Fig. 1 .

 1 Fig. 1. Representation of the syntax in Template-Coq

(

  * Declaration of one inductive type *) Record inductive_body { ind_name : ident; ind_type : term; (* closed arity *) ind_kelim : list sort_family; (* allowed elimination sorts *) (* names, types, number of arguments of constructors *) ind_ctors : list (ident * term * nat); ind_projs : list (ident * term) (* names and types of projections *)}. (* Declaration of a block of mutual inductive types *) Record minductive_decl { ind_npars : nat; (* number of parameters *) ind_bodies : list inductive_body; (* inductives of the mutual block *) ind_universes : universe_context (* universe constraints *) }.

Fig. 2 .

 2 Fig. 2. Typing judment for terms, excerpt

Fig. 3 .

 3 Fig. 3. The monad of commands

Fig. 5 .

 5 Fig. 5. Intensional Function Translation, excerpt (from [8])

[

  fun (x:A) ⇒ t] pair (∀ x:[A]. ?T) bool (fun (x:[A]) ⇒ [t]) true

  Reification of syntax. The central piece of Template-Coq is the inductive type term which represents the syntax of Coq terms, as defined in Fig.1. This inductive follows directly the constr datatype of Coq terms in the OCaml code of Coq, except for the use of OCaml's native arrays and strings; an upcoming extension of Coq[START_REF] Armand | Extending Coq with Imperative Features and Its Application to SAT Verification[END_REF] with such features should solve this mismatch.Constructor tRel represents variables bound by abstractions (introduced by tLambda), dependent products (introduced by tProd) and local definitions (introduced by tLetIn), the natural number is a De Bruijn index. The name is a printing annotation.Sorts are represented with tSort, which takes a universe as argument. A universe is the supremum of a (non-empty) list of level expressions, and a level is either Prop, Set, a global level or a De Bruijn polymorphic level variable.The application (introduced by tApp) is n-ary. The tConst, tInd and tConstruct constructors represent references to constants (definitions or axioms), inductives, or constructors of an inductive type. The universe_instances are non-empty only for polymorphic constants. Finally, tCase represents pattern-matchings, tProj primitive projections, tFix fixpoints and tCoFix cofixpoints.

	Inductive level	lProp | lSet | Level (_ : string) | Var (_ : N).
	Definition universe	list (level * bool). (* level+1 if true *)
	Quoting and unquoting of terms. Template-Coq provides a lifting from concrete
	syntax to reified syntax (quoting) and the converse (unquoting). It can reify and
	reflect all kernel Coq terms.
	The command Quote Definition reifies the syntax of a term. For instance,
	Quote Definition f		(fun x ⇒ x + 0).
	generates the term f defined as
	f = tLambda (nNamed "x") (tInd {| inductive_mind	"Coq.Init.Datatypes.
	nat"; inductive_ind	0 |} [ ]) (tApp (tConst "Coq.Init.Nat.add" [ ])
	[tRel 0; tConstruct {| inductive_mind	"Coq.Init.Datatypes.nat";
	inductive_ind		0 |} 0 [ ]) : term

Table 1 .

 1 Returns Some gr if id is a constant in the current environment and gr is the corresponding global reference. Returns None otherwise. Main Template-Coq commands

	Vernacular command	Reified command with its arguments	Description
		Eval		tmEval red t	Returns the evaluation of t following the evalu-ation strategy red (cbv, cbn, hnf, all or lazy)
	Definition	tmDefinition id t	Makes the definition id created constant id	t and returns the
		Axiom		tmAxiom id A	Adds the axiom id of type A and returns the created constant id
		Lemma		tmLemma id A	Generates an obligation of type A, returns the created constant id after all obligations close
	About or Locate		tmAbout id
				tmQuote t	Returns the syntax of t (of type term)
				tmQuoteRec t	Returns the syntax of t and all the declarations on which it depends
			tmQuoteInductive kn	Returns the declaration of the inductive kn
			tmQuoteConstant kn b	Returns the declaration of the constant kn, if b is true the implementation bypass opacity to get the body of the constant
		Make	tmMkDefinition id	Adds the definition id	t where t is denoted
	Definition		tm	by tm
	Make Inductive		tmMkInductive d	Declares the inductive denoted by the declara-tion d
				tmUnquote tm	Returns the pair (A;t) where t is the term whose syntax is tm and A it's type
			tmUnquoteTyped A tm	Returns the term whose syntax is tm and checks that it is indeed of type A
	duced by the program is discarded but, and it is the point, a program can have
	many side effects like declaring a new definition or a new inductive type, printing
	something, . . . .
		Let's look at some examples. The following program adds the definitions
	foo	12 and bar	foo + 1 to the current context.
	Run TemplateProgram (foo ← tmDefinition "foo" 12 ;
				tmDefinition "bar" (foo +1)).

  table of type tsl_table. Run TemplateProgram (table ← tTranslate [ ] "eq" ; table ← tTranslate table "ID" ; tmDefinition "table" table).

https://template-coq.github.io/template-coq

We do not treat metavariables which are absent from kernel terms and require a separate environment for their declarations.

In Coq, a proof obligation is a goal which has to be solved to complete a definition. Obligations were introduced by Sozeau[START_REF] Sozeau | Program-ing Finger Trees in Coq[END_REF] in the Program mode.

https://github.com/parametricity-coq/paramcoq

Note that there is a similar issue with applications and projections, but which can be circumvented this time using (untyped) primitive projections.

Acknowledgments

This work is supported by the CoqHoTT ERC Grant 64399 and the NSF grants CCF-1407794, CCF-1521602, and CCF-1646417.