A monad for programming with template-coq operations #37

aa755 · 2016-12-24T00:47:27Z

See Ast.TemplateMonad and some example programs in demo.v
There are 2 more enhancements/fixes:

This monad has a more informative quote function (Ast.tmQuote) for quoting inductives (fixes It would be nice if inductives stored their types #17).
Now, the denote_term function unquotes constants and fixpoints as well.

Just created a new vernac command "Make Inductive". As of now, it does nothing. Tested the dummy command in demo.v

The body is ignored for now. Tested this part in demo.v

The name and arity are obtained properly populated. However the resultant definition changes arity from Set to Prop.

Found the correct input by snooping on the paramcoq plugin (using coq/dev/top_printer.ml) Also, needed to recompile coq so that top_printer.ml gets included in coqtop/coqc: coq/dev$ echo "Top_printer" > printer.mllib then add dev/printer.cma to $CORECMA in coq/Makefile.common

…to coq-8.5

However, it is not clear how to access the body of a definition.

The case when the name is an inductive declaration is not handled yet

Many fields are currently dummy and not properly quoted. Also, the quote operations fails on fixpoints

…ote) Suddently, quoting Nat.add works now, perhaps because now I use the Names.constant returned by Nametab.locate, instead of manually cooking up something.

@SkySkimmer

Thanks @SkySkimmer

Thus, we can now make definitions after quoting and hence achieve the functionality of "Quote (Recursively) Definition .. :="

In some programs, the strings may not be in normal form.

This fixes a previous bug where unqupoting constants in modules inside files failed. As a side benefit, because of Locate, the names in tConst need not be fully qualified

gmalecha · 2017-01-01T22:04:56Z

@aa755 What is the current status of this? Is it ready to review or are there more things that you are looking at?

gmalecha · 2017-01-01T22:12:51Z

The quoting operation here is beginning to look a lot more involved than I thought that it would. There also seems to be a lot of overlap with MetaCoq in terms of implementation and operation (the reification plugin in MirrorCore also works in a similar way). I'm wondering if some of this functionality should be merged into that project.

aa755 · 2017-01-01T22:43:26Z

Thanks for those pointers. Indeed, now I notice that some operations overlap with MetaCoq. I thought MetaCoq's monad was mainly for ltac-style proof automation, whereas I am mainly interested in program transformations. I will sometime take a closer look at MetaCoq and MirrorCore.

I currently don't plan to add any more operations to the monad in this PR. It seems that the current operations suffice for my project. The only thing that I am missing now is the ability to properly reify and reflect universes.

gmalecha · 2017-01-02T20:46:11Z

theories/Ast.v

+(** A monad for programming with template-coq operations.
+Using this monad, it should be possible to write many plugins (e.g. paramcoq)
+in Gallina *)
+Inductive TemplateMonad : Type -> Type :=


This seems like it should go in a separate file.

gmalecha · 2017-01-02T20:47:33Z

theories/Ast.v

+  To actually make the definition, use (tmMkDefinition false) *)
+| tmQuoteTerm : forall {A:Type}, A  -> TemplateMonad term
+(** similar to Quote Recursively Definition ... := ...*)
+| tmQuoteTermRec : forall {A:Type}, A  -> TemplateMonad program


It seems like we could implement tmQuoteTermRec in terms of tmQuoteTerm and maybe some sort of fixpoint combinator. That seems like it would be simpler to implement.

gmalecha · 2017-01-02T20:49:03Z

theories/Ast.v

+(** FIXME: strategy is currently ignored in the implementation -- it does all reductions.*)
+| tmReduce : reductionStrategy -> forall {A:Type}, A -> TemplateMonad A
+| tmMkDefinition : bool (* unquote? *) -> ident -> forall {A:Type}, A -> TemplateMonad unit (* bool indicating success? *)
+| tmMkInductive : mutual_inductive_entry -> TemplateMonad unit (* bool indicating success? *)


Are these generated as side-effects immediately or are the aggregated and then applied atomically at the end?

gmalecha · 2017-01-02T20:50:48Z

theories/Ast.v

+| tmPrint : forall {A:Type}, A -> TemplateMonad unit
+(** Quote the body of a definition or inductive. Its name need not be fully qualified --
+  the implementation uses Locate *)
+| tmQuote : ident -> bool (** bypass opacity?*)-> TemplateMonad (option (term+mutual_inductive_entry))


Why quote identifiers and not terms? It seems like we could have two operations: quoteTerm and getBody/unfold that performs delta reduction. Those would provide for simpler primitives.

If we are going to use Locate here, maybe we should export it? e.g.

tmLocate : ident -> TemplateMonad (option ident)

or maybe even separate the module name and return something like list ident * ident

gmalecha · 2017-01-02T20:52:30Z

theories/Ast.v

+(** A monad for programming with template-coq operations.
+Using this monad, it should be possible to write many plugins (e.g. paramcoq)
+in Gallina *)
+Inductive TemplateMonad : Type -> Type :=


Universes might become an issue with this. In MetaCoq (and MirrorCore) the monad is defined as a Prop to avoid universe issues (though I'm not convinced that it works at all).

gmalecha · 2017-01-02T20:53:17Z

src/reify.ml4

@@ -724,6 +911,58 @@ struct
      Command.declare_mutual_inductive_with_eliminations (mut_ind mr mf mp mi mpol mpr) [] [];()
    | _ -> raise (Failure "ill-typed mutual_inductive_entry")

+  let rec run_template_program_rec  ((env,evm,pgm): Environ.env * Evd.evar_map * Term.constr) : Environ.env * Evd.evar_map * Term.constr =


This should be implemented in a separate file.

gmalecha · 2017-01-02T20:54:44Z

theories/Ast.v

@@ -97,3 +97,37 @@ Record mutual_inductive_entry : Set := {
 (*  mind_entry_universes : Univ.universe_context; *)
  mind_entry_private : option bool
 }.
+
+Inductive reductionStrategy : Set :=
+  cbv | cbn | hnf | all.


Why not expose the flags?

gmalecha · 2017-01-02T21:00:47Z

src/reify.ml4

+    if Term.eq_constr coConstr tmReturn then
+      match args with
+      | _::h::[] -> (env,evm,h)
+      | _ -> raise (Failure "tmReturn must take 2 arguments. Please file a bug with Template-Coq.")


It would be nice to unify these error messages. Something like:

raise (BadCommand pgm)

where pgm is the TemplateMonad. At the toplevel, we can print it out.

gmalecha · 2017-01-02T21:02:21Z

src/reify.ml4

+      | _(*reduction strategy*)::_(*type*)::trm::[] -> 
+          let (evm,trm) = reduce_all env (evm,trm) in (env, evm, trm)
+      | _ -> raise (Failure "tmReduce must take 3 arguments. Please file a bug with Template-Coq.")
+    else raise (Failure "Invalid argument or yot yet implemented. The argument must be a TemplateProgram")


I like TemplateProgram better than TemplateMonad, but we should at least be consistent.

gmalecha · 2017-01-02T21:03:00Z

src/reify.ml4

+
+  let run_template_program (env: Environ.env) (evm: Evd.evar_map) (body: Constrexpr.constr_expr) : unit =
+  	let (body,_) = Constrintern.interp_constr env evm body in
+    let _ = run_template_program_rec (env,evm,body) in ()


Maybe we should check the type here? That might produce a better error message than delaying it until we get into the interpreter.

…al inductives.

where they where pushed to the environment in the correct order.

gmalecha · 2017-01-04T13:58:36Z

@aa755 Do you mind if I write a PR on top of this with a few cosmetic changes?

aa755 · 2017-01-04T14:24:27Z

Feel free to use the code here in any way you wish. I agree with all the changes you suggested -- thanks. However, I have been very busy lately because of some deadlines. It may take me a while to address all those changes.

gmalecha · 2017-01-04T14:39:24Z

Completely understandable given the time of year.

aa755 added 30 commits November 14, 2016 23:33

started work on reflecting inductive definitions.

7c2969d

Just created a new vernac command "Make Inductive". As of now, it does nothing. Tested the dummy command in demo.v

The command can now declare an empty inductive of a give name.

4fac2ee

The body is ignored for now. Tested this part in demo.v

documented a bug in unquoting. It incorrectly changes Prop to Set.

4a71321

preliminary work on transparentification.

6a07c23

Defined kernel's representation of inductive datatypes.

3e025d6

started populating the inductive entries properly.

1d75c3f

The name and arity are obtained properly populated. However the resultant definition changes arity from Set to Prop.

bugfix : Prop and Set were switched

70bfe07

unable to construct the type of constructors. error.

11e9c1c

unquoted params, tested mutual and parametrized inductives.

7db60c9

Merge branch 'coq-8.5' of https://github.com/gmalecha/template-coq in…

c66334d

…to coq-8.5

cleaned up the demo

24cdc10

more cleanup for PR

6506e45

clearnup for PR

03905b7

removed the unused argument (name) in Make Inductive

834cbb1

defined&implemented a monad for programming template-coq operations.

c3baa35

minor changes. was trying to implement the monad's tmQuote.

c8a7634

However, it is not clear how to access the body of a definition.

implemented the quote(rec) operation in the monad.

dd8187b

implemented printing

9e61432

exported all members of mutual entry, except universe contexts

bdc1171

properly unquoted mind_entry_record

2fa5fdc

properly unquoted mind_entry_finite

10f3993

properly unquoted mind_private

596619d

Make Inductive does reduction

fac3650

Merge branch 'pr2' into coq-8.5

445a2a6

partially implemented the new tmQuote operation of the monad

c255b3a

The case when the name is an inductive declaration is not handled yet

toward fully quoting inductives..this commits breaks compilation.

b3b680e

the quote inductive code compiles now. works for Init.nat

043967e

Many fields are currently dummy and not properly quoted. Also, the quote operations fails on fixpoints

documented the failure on Init.Nat.add

554ac86

Now using Locate to autocomplete partially qualified names (arg to qu…

4b11e03

…ote) Suddently, quoting Nat.add works now, perhaps because now I use the Names.constant returned by Nametab.locate, instead of manually cooking up something.

aa755 added 11 commits December 14, 2016 08:44

Discharge.process_inductive seems to be doing the right thing.

710e540

Thanks @SkySkimmer

quoting followed by unquoting is now id for demoList

4b27262

fixed a bug

a5b7205

unquoting is now optional in tmMkDefinition.

1dbd845

Thus, we can now make definitions after quoting and hence achieve the functionality of "Quote (Recursively) Definition .. :="

fixed the order of arguments of bind

01c882e

fixed a bug : need to reduce_all before unquoting string/bool.

d7e388e

In some programs, the strings may not be in normal form.

implemented tmReduce. properly unquoted tConst

94ec6fc

more robust unquoting of tConst, using Nametab.Locate

63b61bd

This fixes a previous bug where unqupoting constants in modules inside files failed. As a side benefit, because of Locate, the names in tConst need not be fully qualified

Merge branch 'gmalecha/template-coq:coq-8.5' into coq-8.5

fc5f05f

fixed some TODOs in quoting of inductives, cleanup

1c9d99a

cleanup

9c62807

aa755 changed the title ~~A monad for programming with template coq operations~~ A monad for programming with template-coq operations Dec 24, 2016

aa755 added 6 commits December 25, 2016 11:19

trying to fix the env during quoting inductives

e9588a4

need to reduces redundancy as it is confusing.

0bac82c

some refractoring

5b7a6a0

now properly populatinv env while quoting inductives

0d49802

cleanup

5dbadda

properly unquoted fixpoints

2bc821b

gmalecha added enhancement question labels Jan 1, 2017

gmalecha requested changes Jan 2, 2017

View reviewed changes

aa755 added 3 commits January 3, 2017 23:39

now pushing params in the right order while unquoting inductives.

9ede284

now pushing inductives to env in the correct order when unquoting mut…

a952a45

…al inductives.

undid the accidental reversal of parameters in HEAD^2,

574c895

where they where pushed to the environment in the correct order.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

A monad for programming with template-coq operations #37

A monad for programming with template-coq operations #37

aa755 commented Dec 24, 2016 •

edited

Loading

gmalecha commented Jan 1, 2017

gmalecha commented Jan 1, 2017

aa755 commented Jan 1, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha Jan 2, 2017

gmalecha commented Jan 4, 2017

aa755 commented Jan 4, 2017

gmalecha commented Jan 4, 2017

A monad for programming with template-coq operations #37

Are you sure you want to change the base?

A monad for programming with template-coq operations #37

Conversation

aa755 commented Dec 24, 2016 • edited Loading

gmalecha commented Jan 1, 2017

gmalecha commented Jan 1, 2017

aa755 commented Jan 1, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gmalecha commented Jan 4, 2017

aa755 commented Jan 4, 2017

gmalecha commented Jan 4, 2017

aa755 commented Dec 24, 2016 •

edited

Loading