Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Initial commit. Template plugin and simple tactic.

  • Loading branch information...
commit e6059e78893bca2b85f93d682b17f156ad6daefa 0 parents
Matthieu Sozeau authored
13 Make
@@ -0,0 +1,13 @@
+-I src -R theories Constructors
+-custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o src/constructors_plugin.cmxs src/constructors.cmx src/constructors_plugin_mod.cmx" "src/constructors.cmx src/constructors_plugin_mod.cmx" src/constructors_plugin.cmxs
+-custom "$(CAMLLINK) -g -a -o src/constructors_plugin.cma src/constructors.cmo src/constructors_plugin_mod.cmo" "src/constructors.cmo src/constructors_plugin_mod.cmo" src/constructors_plugin.cma
+-custom "$(COQBIN)coqc $(COQDEBUG) $(COQFLAGS) $*" "%.v $(CONSTRUCTORS_PLUGINOPT) $(CONSTRUCTORS_PLUGIN)" "%.vo %.glob"
+CONSTRUCTORS_PLUGIN = "src/constructors_plugin.cma"
+CONSTRUCTORS_PLUGINOPT = "src/constructors_plugin.cmxs"
+COQDOC = "$(COQBIN)coqdoc -interpolate -utf8"
+CAMLP4OPTIONS = "-loc loc"
+src/constructors.ml
+src/constructors_plugin_mod.ml
+theories/Dynamic.v
+theories/Constructors.v
+test-suite/constructortac.v
37 README
@@ -0,0 +1,37 @@
+Constructors: an example Coq plugin
+===================================
+Copyright 2010 Matthieu Sozeau <mattam@mattam.org>
+
+This archive contains an example Coq plugin that implements a
+tactic to get the constructors of an inductive type in Ltac.
+It serves as a documented example on both the plugin system
+and how to write simple tactics in OCaml.
+
+The archive has 3 subdirectories:
+src/ contains the code of the plugin in constructors.ml and
+ a set of support file for building the constructors plugin.
+
+theories/ contains support Coq files for the plugin. Dynamic
+ is referenced from the code of the plugin above.
+
+test-suite/ just demonstrates a use of the plugin
+
+
+Installation
+============
+
+First, you should have coqc, ocamlc and make in your path.
+Then simply do:
+
+# coq_makefile -f Make -o Makefile
+
+To generate a makefile from the description in Make, then [make].
+This will consecutively build the plugin, the supporting
+theories and the test-suite file.
+
+You can then either [make install] the plugin or leave it in its
+current directory. To be able to import it from anywhere in Coq,
+simply add the following to ~/.coqrc:
+
+Add Rec LoadPath "path_to_constructors/theories" as Constructors.
+Add ML Path "path_to_constructors/src".
63 src/constructors.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
+
+(* $$ *)
+
+open Term
+open Names
+open Coqlib
+
+let find_constant contrib dir s =
+ Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
+
+let contrib_name = "constructors"
+let init_constant dir s = find_constant contrib_name dir s
+let init_reference dir s = Coqlib.find_reference contrib_name dir s
+
+let constructors_path = ["Constructors";"Dynamic"]
+let coq_dynamic_ind = lazy (init_constant constructors_path "dyn")
+let coq_dynamic_constr = lazy (init_constant constructors_path "mkDyn")
+let coq_dynamic_type = lazy (init_constant constructors_path "dyn_type")
+let coq_dynamic_obj = lazy (init_constant constructors_path "dyn_value")
+
+let mkDyn ty value =
+ mkApp (Lazy.force coq_dynamic_constr, [| ty ; value |])
+
+let list_path = ["Coq";"Init";"Datatypes"]
+let coq_list_ind = lazy (init_constant list_path "list")
+let coq_list_nil = lazy (init_constant list_path "nil")
+let coq_list_cons = lazy (init_constant list_path "cons")
+
+open Tacmach
+open Tacticals
+open Tacexpr
+
+let nowhere = { onhyps = Some []; concl_occs = Rawterm.no_occurrences_expr }
+
+let constructors c id gl =
+ let ind, args = Inductive.find_rectype (pf_env gl) c in
+ let mindspec = Global.lookup_inductive ind in
+ let listty = mkApp (Lazy.force coq_list_ind, [| Lazy.force coq_dynamic_ind |]) in
+ let listval =
+ Util.array_fold_right_i (fun i v l ->
+ let cd = mkConstruct (ind, succ i) in
+ let d = mkDyn v cd in
+ mkApp (Lazy.force coq_list_cons, [| Lazy.force coq_dynamic_ind; d; l |]))
+ (Inductive.type_of_constructors ind mindspec)
+ (mkApp (Lazy.force coq_list_nil, [| Lazy.force coq_dynamic_ind |]))
+ in
+ Tactics.letin_tac None (Name id) listval (Some listty) nowhere gl
+
+TACTIC EXTEND constructors
+| ["constructors" "of" constr(c) "in" ident(id) ] ->
+ [ constructors c id ]
+END
+
2  src/constructors_plugin_mod.ml
@@ -0,0 +1,2 @@
+let _=Mltop.add_known_module"Constructors"
+let _=Mltop.add_known_module"Constructors_plugin_mod"
23 test-suite/constructortac.v
@@ -0,0 +1,23 @@
+Require Import Constructors Bvector.
+
+Ltac apply_in_dyn_list v :=
+ match v with
+ | cons (mkDyn _ ?x) ?rest => apply x || apply_in_dyn_list rest
+ | nil => fail
+ end.
+
+Ltac constructor_of ind :=
+ let x := fresh in
+ constructors of ind in x ;
+ let v := eval cbv in x in
+ clear x;
+ apply_in_dyn_list v.
+
+Ltac constructor_tac :=
+ match goal with
+ | |- ?T => repeat constructor_of T
+ end.
+
+Goal vector nat (S 0).
+constructor_tac. exact 0.
+Defined.
3  theories/Constructors.v
@@ -0,0 +1,3 @@
+Require Export Constructors.Dynamic.
+
+Declare ML Module "constructors_plugin".
3  theories/Dynamic.v
@@ -0,0 +1,3 @@
+Record dyn : Type := mkDyn {
+ dyn_type : Type;
+ dyn_value : dyn_type }.
Please sign in to comment.
Something went wrong with that request. Please try again.