Implementation of Extractable monad

template-coq/.gitignore

@@ -0,0 +1,2 @@
+Makefile.plugin
+Makefile.plugin.conf

template-coq/Makefile

@@ -1,4 +1,12 @@
-all: Makefile.coq
+all: coq plugin
+
+gen-src/Extraction.vo: coq gen-src/Extraction.v
+	$(COQPATH)coqc -I src -Q theories Template gen-src/Extraction.v
+
+plugin: coq Makefile.plugin
+	$(MAKE) -f Makefile.plugin
+
+coq: Makefile.coq
 	$(MAKE) -f Makefile.coq
 
 .PHONY: all install html clean mrproper
@@ -9,14 +17,18 @@ install: Makefile.coq
 html: all
 	$(MAKE) -f Makefile.coq html
 
-clean: Makefile.coq
+clean: Makefile.coq Makefile.plugin
 	$(MAKE) -f Makefile.coq clean
+	$(MAKE) -f Makefile.plugin clean
 
 mrproper: clean
-	rm -f Makefile.coq
+	rm -f Makefile.coq Makefile.plugin
 
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
+Makefile.plugin: coq _PluginProject
+	$(COQPATH)coq_makefile -f _PluginProject -o Makefile.plugin
+
 .merlin: Makefile.coq
 	$(MAKE) -f Makefile.coq .merlin

template-coq/_CoqProject

@@ -1,6 +1,8 @@
 -I src
+-I gen-src
 -R theories Template
 
+# the MetaCoq plugin
 src/tm_util.ml
 # src/quoter.mli
 src/quoter.ml
@@ -14,8 +16,8 @@ src/template_coq.mlpack
 src/template_monad.ml
 src/run_template_monad.mli
 src/run_template_monad.ml
-src/pluginCore.mli
-src/pluginCore.ml
+src/plugin_core.mli
+src/plugin_core.ml
 
 theories/LibHypsNaming.v
 theories/utils.v theories/config.v theories/kernel/univ.v
@@ -26,12 +28,15 @@ theories/LiftSubst.v theories/UnivSubst.v theories/Typing.v
 theories/TypingWf.v theories/Generation.v theories/WeakeningEnv.v
 theories/Closed.v theories/Weakening.v theories/Substitution.v
 theories/MetaTheory.v theories/Checker.v theories/WcbvEval.v
-theories/Retyping.v theories/All.v theories/Extraction.v
+theories/Retyping.v theories/All.v
 
 # the Template monad
 theories/TemplateMonad.v
 theories/TemplateMonad/Common.v
 theories/TemplateMonad/Core.v
 theories/TemplateMonad/Extractable.v
 theories/TemplateMonad/Monad.v
-theories/monad_utils.v
+theories/monad_utils.v
+
+# for Extraction
+gen-src/Extraction.v

template-coq/_PluginProject

@@ -0,0 +1,87 @@
+-I src
+-I gen-src
+-Q theories Template
+
+gen-src/Ascii.ml
+gen-src/Ascii.mli
+gen-src/Ast0.ml
+gen-src/Ast0.mli
+gen-src/AstUtils.ml
+gen-src/AstUtils.mli
+gen-src/BasicAst.ml
+gen-src/BasicAst.mli
+gen-src/Basics.ml
+gen-src/Basics.mli
+gen-src/BinInt.ml
+gen-src/BinInt.mli
+gen-src/BinNat.ml
+gen-src/BinNat.mli
+gen-src/BinNums.ml
+gen-src/BinNums.mli
+gen-src/BinPosDef.ml
+gen-src/BinPosDef.mli
+gen-src/BinPos.ml
+gen-src/BinPos.mli
+gen-src/Bool.ml
+gen-src/Bool.mli
+gen-src/Checker0.ml
+gen-src/Checker0.mli
+gen-src/Common.ml
+gen-src/Common.mli
+gen-src/config0.ml
+gen-src/config0.mli
+gen-src/Datatypes.ml
+gen-src/Datatypes.mli
+gen-src/DecidableType.ml
+gen-src/DecidableType.mli
+gen-src/Decimal.ml
+gen-src/Decimal.mli
+gen-src/Equalities.ml
+gen-src/Equalities.mli
+gen-src/Extractable.ml
+gen-src/Extractable.mli
+gen-src/FMapWeakList.ml
+gen-src/FMapWeakList.mli
+gen-src/LiftSubst.ml
+gen-src/LiftSubst.mli
+gen-src/List0.ml
+gen-src/List0.mli
+gen-src/Logic.ml
+gen-src/Logic.mli
+gen-src/monad_utils.ml
+gen-src/monad_utils.mli
+gen-src/MSetWeakList.ml
+gen-src/MSetWeakList.mli
+gen-src/Nat0.ml
+gen-src/Nat0.mli
+gen-src/OrderedType0.ml
+gen-src/OrderedType0.mli
+gen-src/Orders.ml
+gen-src/Orders.mli
+gen-src/OrdersTac.ml
+gen-src/OrdersTac.mli
+gen-src/PeanoNat.ml
+gen-src/PeanoNat.mli
+gen-src/Retyping0.ml
+gen-src/Retyping0.mli
+gen-src/Specif.ml
+gen-src/Specif.mli
+gen-src/String0.ml
+gen-src/String0.mli
+gen-src/Typing0.ml
+gen-src/Typing0.mli
+gen-src/TypingWf.ml
+gen-src/TypingWf.mli
+gen-src/uGraph0.ml
+gen-src/uGraph0.mli
+gen-src/univ0.ml
+gen-src/univ0.mli
+gen-src/UnivSubst0.ml
+gen-src/UnivSubst0.mli
+gen-src/utils.ml
+gen-src/utils.mli
+gen-src/Wf.ml
+gen-src/Wf.mli
+
+gen-src/run_extractable.ml
+gen-src/meta_coq_plugin.mlpack

template-coq/gen-src/.gitignore

@@ -0,0 +1,2 @@
+*.mli
+*.ml

template-coq/theories/Extraction.v → template-coq/gen-src/Extraction.v

@@ -21,6 +21,12 @@ Extraction Blacklist config uGraph univ Ast String List Nat Int
            UnivSubst Typing Checker Retyping OrderedType.
 Set Warnings "-extraction-opaque-accessed".
 
-Recursive Extraction Library TypingWf.
-Recursive Extraction Library Checker.
-Recursive Extraction Library Retyping.
+Require Import Template.Ast.
+
+Cd "gen-src".
+
+Require Import Template.TemplateMonad.Extractable.
+
+Recursive Extraction Library Extractable.
+
+Cd "..".

template-coq/gen-src/coq_constr.ml

@@ -0,0 +1,88 @@
+open Plugin_core
+open Constr
+
+type name = Names.Name.t
+type id = Names.Id.t
+type universe = Univ.Universe.t
+type universe_instance = unit
+type projection = Names.Projection.t
+type 'a mfixpoint = 'a BasicAst.mfixpoint
+type nat = int
+
+let tRel (n : nat) =
+  failwith "tRel"
+let tVar (i : id) : Constr.t =
+  Constr.mkVar i
+
+let tMeta (n : nat) : Constr.t =
+  failwith "tMeta"
+
+let tEvar (n : nat) (ls : Constr.t list) : Constr.t =
+  failwith "tEvar is not supported"
+
+let tSort (u : Univ.Universe.t) : Constr.t =
+  failwith "tSort"
+
+let tCast (a : Constr.t) (b : Constr.cast_kind) (c : Constr.t) : Constr.t =
+  Constr.mkCast (a, b, c)
+
+let tProd (n : name) (a : Constr.t) (b : Constr.t) : Constr.t =
+  Constr.mkProd (n, a, b)
+
+let tLambda (n : name) (a : Constr.t) (b : Constr.t) : Constr.t =
+  Constr.mkLambda (n, a, b)
+
+let tLetIn (n : name) (t : Constr.t) (b : Constr.t) (c : Constr.t) : Constr.t =
+  Constr.mkLetIn (n, t, b, c)
+
+let tApp (f : Constr.t) (ls : Constr.t list) : Constr.t =
+  Constr.mkApp (f, Array.of_list ls)
+
+let tConst (kn : 'a) : 'a =
+  failwith "tConst"
+
+let tConstruct (kn : 'a) : 'a =
+  failwith "tConstruct"
+
+let tCase (_ : 'a) : 'a =
+  failwith "tCase"
+
+let tProj (_ : BasicAst.projection) (_ : Constr.t) : Constr.t =
+  failwith "tProj"
+
+let constr_match
+    (rel : nat -> 'a)
+    (var : ident -> 'a)
+    (meta : nat -> 'a)
+    (evar : nat -> term list -> 'a)
+    (sort : universe -> 'a)
+    (cast : term -> Constr.cast_kind -> term -> 'a)
+    (prod : name -> term -> term -> 'a)
+    (lambda : name -> term -> term -> 'a)
+    (letin : name -> term -> term -> term -> 'a)
+    (app : term -> term list -> 'a)
+    (const : kername -> universe_instance -> 'a)
+    (construct : Names.inductive -> nat -> universe_instance -> 'a)
+    (case : Names.inductive * nat * term -> term -> (nat * term) list -> 'a)
+    (proj : projection -> term -> 'a)
+    (fix : term mfixpoint -> nat -> 'a)
+    (cofix : term mfixpoint -> nat -> 'a)
+    (t : term) : 'a =
+  match Constr.kind t with
+  | Constr.Rel n -> rel n
+  | Constr.Var id -> var id
+  | Constr.Meta m -> meta m
+  | Constr.Evar (a,b) -> evar (Evar.repr a) (Array.to_list b)
+  | Constr.Sort s -> sort s
+  | Constr.Cast (a,b,c) -> cast a b c
+  | Constr.Prod (a,b,c) -> prod a b c
+  | Constr.Lambda (a,b,c) -> lambda a b c
+  | Constr.LetIn (a,b,c,d) -> letin a b c d
+  | Constr.App (f, xs) -> app f (Array.to_list xs)
+  | Constr.Const _
+  | Constr.Ind _
+  | Constr.Construct _
+  | Constr.Case _
+  | Constr.Fix _
+  | Constr.CoFix _
+  | Constr.Proj _ -> failwith "not implemented"

template-coq/gen-src/meta_coq_plugin.mlpack

@@ -0,0 +1,47 @@
+Utils
+Ascii
+Ast0
+Univ0
+AstUtils
+BasicAst
+Basics
+BinInt
+BinNat
+BinNums
+BinPosDef
+BinPos
+Bool
+Common
+Config0
+Datatypes
+DecidableType
+Decimal
+Equalities
+Extractable
+FMapWeakList
+List0
+Logic
+MSetWeakList
+Nat0
+OrderedType0
+Orders
+OrdersTac
+PeanoNat
+Specif
+String0
+UGraph0
+
+
+
+
+
+Tm_util
+Quoter
+Constr_quoter
+Template_monad
+Denote
+Plugin_core
+
+Extractable
+
+Run_extractable