Skip to content

Commit aa2a2c4

Browse files
gmalechagmalecha
committed
remove the dependency of TemplateMonad on monad_utils
- monad_utils comtains a partial monad library, it should be replaced will a full-featured monad library (in another package). in the meantime, this allows users to import only the core TemplateMonad and not pull in the monad_utils dependency.
1 parent 5900f1b commit aa2a2c4

File tree

6 files changed

+105
-95
lines changed

6 files changed

+105
-95
lines changed

‎template-coq/_CoqProject‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,9 @@ src/template_coq.mlpack
1313

1414
theories/utils.v
1515
theories/config.v
16-
theories/monad_utils.v
1716
theories/kernel/univ.v
1817
theories/kernel/uGraph.v
1918
theories/Ast.v
20-
theories/TemplateMonad.v
2119
theories/AstUtils.v
2220
theories/Loader.v
2321
theories/Induction.v
@@ -27,4 +25,10 @@ theories/UnivSubst.v
2725
theories/Typing.v
2826
theories/Checker.v
2927
theories/All.v
30-
theories/Extraction.v
28+
theories/Extraction.v
29+
30+
# the Template monad
31+
theories/TemplateMonad.v
32+
theories/TemplateMonad/Core.v
33+
theories/TemplateMonad/Monad.v
34+
theories/monad_utils.v

‎template-coq/theories/AstUtils.v‎

Lines changed: 4 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
From Coq Require Import String Bool.
22
From Coq Require Import List.
3-
From Template Require Import Ast TemplateMonad utils monad_utils.
4-
Import List.ListNotations MonadNotation.
3+
From Template Require Import Ast utils.
4+
Import List.ListNotations.
55

66
Definition map_decl f (d : context_decl) :=
77
{| decl_name := d.(decl_name);
@@ -22,6 +22,7 @@ Definition string_of_gref gr :=
2222

2323
Definition gref_eq_dec
2424
: forall gr gr' : global_reference, {gr = gr'} + {~ gr = gr'}.
25+
Proof.
2526
decide equality; eauto with eq_dec.
2627
destruct i, i0.
2728
decide equality; eauto with eq_dec.
@@ -52,13 +53,6 @@ Fixpoint remove_arity (n : nat) (t : term) : term :=
5253
end
5354
end.
5455

55-
Definition print_nf {A} (msg : A) : TemplateMonad unit
56-
:= (tmEval all msg) >>= tmPrint.
57-
58-
Definition fail_nf {A} (msg : string) : TemplateMonad A
59-
:= (tmEval all msg) >>= tmFail.
60-
61-
6256
Fixpoint lookup_mind_decl (id : ident) (decls : global_declarations)
6357
:= match decls with
6458
| nil => None
@@ -99,7 +93,4 @@ Proof.
9993
refine (List.map (fun x => fst (fst x)) ind_ctors).
10094
refine (List.map (fun x => remove_arity decl.(ind_npars)
10195
(snd (fst x))) ind_ctors).
102-
Defined.
103-
104-
Definition tmMkInductive' (mind : mutual_inductive_body) : TemplateMonad unit
105-
:= tmMkInductive (mind_body_to_entry mind).
96+
Defined.

‎template-coq/theories/TemplateMonad.v‎

Lines changed: 2 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -1,79 +1,2 @@
1-
From Coq Require Import Strings.String.
2-
From Template Require Import Ast.
3-
From Template Require Import monad_utils.
4-
5-
Set Universe Polymorphism.
6-
Set Primitive Projections.
7-
Set Printing Universes.
8-
9-
(** ** The Template Monad
10-
11-
A monad for programming with Template Coq structures. *)
12-
13-
(** Reduction strategy to apply, beware [cbv], [cbn] and [lazy] are _strong_. *)
14-
15-
Inductive reductionStrategy : Set :=
16-
cbv | cbn | hnf | all | lazy | unfold (i : ident).
17-
18-
Record typed_term : Type := existT_typed_term
19-
{ my_projT1 : Type
20-
; my_projT2 : my_projT1
21-
}.
22-
(*
23-
Polymorphic Definition typed_term@{t} := {T : Type@{t} & T}.
24-
Polymorphic Definition existT_typed_term a t : typed_term :=
25-
@existT Type (fun T => T) a t. (* todo: need to fix this *)
26-
27-
Definition my_projT1 (t : typed_term) : Type := @projT1 Type (fun T => T) t.
28-
Definition my_projT2 (t : typed_term) : my_projT1 t := @projT2 Type (fun T => T) t.
29-
*)
30-
31-
(** *** The TemplateMonad type *)
32-
33-
Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Type :=
34-
(* Monadic operations *)
35-
| tmReturn : forall {A:Type@{t}}, A -> TemplateMonad A
36-
| tmBind : forall {A B : Type@{t}}, TemplateMonad A -> (A -> TemplateMonad B)
37-
-> TemplateMonad B
38-
39-
(* General commands *)
40-
| tmPrint : forall {A:Type@{t}}, A -> TemplateMonad unit
41-
| tmFail : forall {A:Type@{t}}, string -> TemplateMonad A
42-
| tmEval : reductionStrategy -> forall {A:Type@{t}}, A -> TemplateMonad A
43-
44-
(* Return the defined constant *)
45-
| tmDefinition : ident -> forall {A:Type@{t}}, A -> TemplateMonad A
46-
| tmAxiom : ident -> forall A : Type@{t}, TemplateMonad A
47-
| tmLemma : ident -> forall A : Type@{t}, TemplateMonad A
48-
49-
(* Guaranteed to not cause "... already declared" error *)
50-
| tmFreshName : ident -> TemplateMonad ident
51-
52-
| tmAbout : ident -> TemplateMonad (option global_reference)
53-
| tmCurrentModPath : unit -> TemplateMonad string
54-
55-
(* Quoting and unquoting commands *)
56-
(* Similar to Quote Definition ... := ... *)
57-
| tmQuote : forall {A:Type@{t}}, A -> TemplateMonad Ast.term
58-
(* Similar to Quote Recursively Definition ... := ...*)
59-
| tmQuoteRec : forall {A:Type@{t}}, A -> TemplateMonad program
60-
(* Quote the body of a definition or inductive. Its name need not be fully qualified *)
61-
| tmQuoteInductive : kername -> TemplateMonad mutual_inductive_body
62-
| tmQuoteUniverses : unit -> TemplateMonad uGraph.t
63-
| tmQuoteConstant : kername -> bool (* bypass opacity? *) -> TemplateMonad constant_entry
64-
| tmMkDefinition : ident -> Ast.term -> TemplateMonad unit
65-
(* unquote before making the definition *)
66-
(* FIXME take an optional universe context as well *)
67-
| tmMkInductive : mutual_inductive_entry -> TemplateMonad unit
68-
| tmUnquote : Ast.term -> TemplateMonad typed_term@{u}
69-
| tmUnquoteTyped : forall A : Type@{t}, Ast.term -> TemplateMonad A
70-
71-
(* Typeclass registration and querying for an instance *)
72-
| tmExistingInstance : ident -> TemplateMonad unit
73-
| tmInferInstance : forall A : Type@{t}, TemplateMonad (option A)
74-
.
75-
76-
(** This allow to use notations of MonadNotation *)
77-
78-
Instance TemplateMonad_Monad : Monad TemplateMonad :=
79-
{| ret := @tmReturn ; bind := @tmBind |}.
1+
Require Export Template.TemplateMonad.Core.
2+
Require Export Template.TemplateMonad.Monad.

‎template-coq/theories/TemplateMonad/Core.v‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
From Coq Require Import Strings.String.
2+
From Template Require Import Ast AstUtils.
3+
4+
Set Universe Polymorphism.
5+
Set Primitive Projections.
6+
Set Printing Universes.
7+
8+
(** ** The Template Monad
9+
10+
A monad for programming with Template Coq structures. *)
11+
12+
(** Reduction strategy to apply, beware [cbv], [cbn] and [lazy] are _strong_. *)
13+
14+
Inductive reductionStrategy : Set :=
15+
cbv | cbn | hnf | all | lazy | unfold (i : ident).
16+
17+
Record typed_term : Type := existT_typed_term
18+
{ my_projT1 : Type
19+
; my_projT2 : my_projT1
20+
}.
21+
(*
22+
Polymorphic Definition typed_term@{t} := {T : Type@{t} & T}.
23+
Polymorphic Definition existT_typed_term a t : typed_term :=
24+
@existT Type (fun T => T) a t. (* todo: need to fix this *)
25+
26+
Definition my_projT1 (t : typed_term) : Type := @projT1 Type (fun T => T) t.
27+
Definition my_projT2 (t : typed_term) : my_projT1 t := @projT2 Type (fun T => T) t.
28+
*)
29+
30+
(** *** The TemplateMonad type *)
31+
32+
Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Type :=
33+
(* Monadic operations *)
34+
| tmReturn : forall {A:Type@{t}}, A -> TemplateMonad A
35+
| tmBind : forall {A B : Type@{t}}, TemplateMonad A -> (A -> TemplateMonad B)
36+
-> TemplateMonad B
37+
38+
(* General commands *)
39+
| tmPrint : forall {A:Type@{t}}, A -> TemplateMonad unit
40+
| tmFail : forall {A:Type@{t}}, string -> TemplateMonad A
41+
| tmEval : reductionStrategy -> forall {A:Type@{t}}, A -> TemplateMonad A
42+
43+
(* Return the defined constant *)
44+
| tmDefinition : ident -> forall {A:Type@{t}}, A -> TemplateMonad A
45+
| tmAxiom : ident -> forall A : Type@{t}, TemplateMonad A
46+
| tmLemma : ident -> forall A : Type@{t}, TemplateMonad A
47+
48+
(* Guaranteed to not cause "... already declared" error *)
49+
| tmFreshName : ident -> TemplateMonad ident
50+
51+
| tmAbout : ident -> TemplateMonad (option global_reference)
52+
| tmCurrentModPath : unit -> TemplateMonad string
53+
54+
(* Quoting and unquoting commands *)
55+
(* Similar to Quote Definition ... := ... *)
56+
| tmQuote : forall {A:Type@{t}}, A -> TemplateMonad Ast.term
57+
(* Similar to Quote Recursively Definition ... := ...*)
58+
| tmQuoteRec : forall {A:Type@{t}}, A -> TemplateMonad program
59+
(* Quote the body of a definition or inductive. Its name need not be fully qualified *)
60+
| tmQuoteInductive : kername -> TemplateMonad mutual_inductive_body
61+
| tmQuoteUniverses : unit -> TemplateMonad uGraph.t
62+
| tmQuoteConstant : kername -> bool (* bypass opacity? *) -> TemplateMonad constant_entry
63+
| tmMkDefinition : ident -> Ast.term -> TemplateMonad unit
64+
(* unquote before making the definition *)
65+
(* FIXME take an optional universe context as well *)
66+
| tmMkInductive : mutual_inductive_entry -> TemplateMonad unit
67+
| tmUnquote : Ast.term -> TemplateMonad typed_term@{u}
68+
| tmUnquoteTyped : forall A : Type@{t}, Ast.term -> TemplateMonad A
69+
70+
(* Typeclass registration and querying for an instance *)
71+
| tmExistingInstance : ident -> TemplateMonad unit
72+
| tmInferInstance : forall A : Type@{t}, TemplateMonad (option A)
73+
.
74+
75+
Definition print_nf {A} (msg : A) : TemplateMonad unit
76+
:= tmBind (tmEval all msg) tmPrint.
77+
78+
Definition fail_nf {A} (msg : string) : TemplateMonad A
79+
:= tmBind (tmEval all msg) tmFail.
80+
81+
Definition tmMkInductive' (mind : mutual_inductive_body) : TemplateMonad unit
82+
:= tmMkInductive (mind_body_to_entry mind).

‎template-coq/theories/TemplateMonad/Monad.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
From Template Require Import TemplateMonad.Core.
2+
3+
(** This allow to use notations of MonadNotation *)
4+
From Template Require Import monad_utils.
5+
6+
Instance TemplateMonad_Monad : Monad TemplateMonad :=
7+
{| ret := @tmReturn ; bind := @tmBind |}.

‎template-coq/theories/monad_utils.v‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
(* todo(gmm): This file should really be replaced by a real
2+
* monad library.
3+
*)
14
Require Import List.
25

36
Set Universe Polymorphism.

0 commit comments

Comments
 (0)