Added a reifiction function for modular reification without pmaps. by jesper-bengtson · Pull Request #102 · gmalecha/mirror-core

jesper-bengtson · 2016-12-11T02:11:22Z

No description provided.

gmalecha

Tiny bit of cleanup.

gmalecha · 2016-12-11T02:25:06Z

theories/Reify/ReifyView.v

+        (rf ++
+         ((Patterns.CVar (@ExprCore.Var typ func)) ::
+          (Patterns.CApp (Patterns.CRec 0) (Patterns.CRec 0) (@ExprCore.App typ func)) ::
+	  (Patterns.CAbs (CCall (reify_scheme typ)) (CRec 0) (@ExprCore.Abs typ func)) :: nil))).


Would it make sense to factor out the common code here? Maybe make something that takes both before and after commands and then instantiate it appropriately for both reify_func and reify_func'?

gmalecha · 2016-12-11T02:25:38Z

theories/Reify/ReifyView.v

 Arguments Reify_func _ _ {_ _} _.
+
+Arguments reify_func' _ _ {_} _.
+Arguments Reify_func' _ _ {_} _.


What are the first two arguments to this function?

jesper-bengtson · 2016-12-11T09:40:55Z

It would make sense both to refactor the code and to give it a bette name than just adding a prime. The two first arguments are typ and func, the last is the list of reification rules that are to be wrapped in the CFix. The two implicit arguments are the Reify type class for typ and the partial view to the lookup table (which the primed version lacks). On 11 Dec 2016, at 03:26, Gregory Malecha <notifications@github.com<mailto:notifications@github.com>> wrote: @gmalecha requested changes on this pull request. Tiny bit of cleanup.

________________________________ In theories/Reify/ReifyView.v<#102 (review)>:

Polymorphic Instance Reify_func (rf : list (Command (expr typ func))) : Reify (expr typ func) := { reify_scheme := reify_func rf }. + Polymorphic Definition reify_func' (rf : list (Command (expr typ func))) : Command (expr typ func) := + @Patterns.CFix (expr typ func) + (@Patterns.CFirst_ _ + (rf ++ + ((Patterns.CVar (@ExprCore.Var typ func)) :: + (Patterns.CApp (Patterns.CRec 0) (Patterns.CRec 0) (@ExprCore.App typ func)) :: + (Patterns.CAbs (CCall (reify_scheme typ)) (CRec 0) (@ExprCore.Abs typ func)) :: nil))). Would it make sense to factor out the common code here? Maybe make something that takes both before and after commands and then instantiate it appropriately for both reify_func and reify_func'?

________________________________ In theories/Reify/ReifyView.v<#102 (review)>:

End ReifyFunc.

Arguments reify_func _ _ {_ _} _. Arguments Reify_func _ _ {_ _} _. + +Arguments reify_func' _ _ {_} _. +Arguments Reify_func' _ _ {_} _. What are the first two arguments to this function? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub<#102 (review)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AE_rNaVgAbpX2eVPP9YQcA3paSMYo-Fiks5rG187gaJpZM4LJ0RJ>.

…olyApply/Test.v

- fixing the Test file.

- NOTE: since type checking was failing, it seems likely that there is an issue with the environments. It would be better to figure out what the problem is and fix it. - we should drop that information entirely

gmalecha · 2016-12-17T00:27:45Z

This PR is now a lot bigger, it fixes several issue in the plugin.

gmalecha · 2016-12-17T00:29:03Z

examples/PolyApply/Test.v

+Typeclasses Opaque IgnorePatterns.
+
+Arguments reify_IgnorePatterns {_} _ {_}.
+*)


IgnorePatterns should be moved to another file.

gmalecha · 2016-12-17T00:29:28Z

examples/PolyApply/Test.v

+Require Import MirrorCore.Lib.EqView.
+Require Import MirrorCore.CTypes.BaseType.
+Require Import MirrorCore.Lemma.
+(* Require Import MirrorCore.TCLemma. *)


This should be removed.

gmalecha · 2016-12-17T00:29:46Z

examples/PolyApply/Test.v

+    (* This reifies *)
+    reify_poly (forall x : nat, True -> True -> x = x -> x = x).
+    apply I.
+  Qed.


Should probably be removed?

gmalecha · 2016-12-17T00:30:34Z

src/reify_Lambda_shell.ml4

    type syntax_data =
      { reify       : lazy_term -> Term.constr reifier
-      ; result_type : Term.constr
+      ; result_type : unit (* Term.constr *)


The result_type field should be removed entirely.

gmalecha · 2016-12-17T00:30:43Z

src/reify_Lambda_shell.ml4

+    (*           ++ Printer.pr_constr_env env evm cmd *)
+    (*           ++ fnl () *)
+    (*           ++ str "has type" ++ fnl () *)
+    (*           ++ Printer.pr_constr_env env evm typ) *)


gmalecha · 2016-12-17T00:30:53Z

src/reify_Lambda_shell.ml4

    let compile_name (prg : Term.constr) =
      let (evm,env) = Lemmas.get_current_context () in
-      let typ = get_Command_type env evm prg in
+      (* let typ = get_Command_type env evm prg in *)


gmalecha · 2016-12-17T00:31:01Z

src/reify_Lambda_shell.ml4

    let reify_type (name : Term.constr) =
      let data = get_entry name in
      data.result_type
+*)


…cation rule for any RSym.

gmalecha · 2017-01-25T07:13:16Z

examples/PolyRewrite/QuantifierPuller/PolyQuantPullRtac.v

  Eval unfold Lemma.add_var, Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises in
    <:: @eq_refl' ::>.
-
+Print lem_eq_refl'.


Needs to be removed.

gmalecha · 2017-01-25T07:13:26Z

examples/PolyRewrite/QuantifierPuller/PolyQuantPullRtac.v

  Eval unfold Lemma.add_var, Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises in
  <:: @Proper_exists ::>.

+Print lem_Proper_exists.


Needs to be removed.

gmalecha · 2017-01-25T07:13:42Z

examples/PolyRewrite/QuantifierPuller/PolyQuantPullRtac.v

         end.
 *)
-
+Locate ctyp.


Needs to be removed.

gmalecha · 2017-01-25T07:13:53Z

examples/PolyRewrite/QuantifierPuller/PolyQuantPullRtac.v

 Qed.
-
-
+Locate RewriteHintDb.


Needs to be removed.

gmalecha · 2017-01-25T07:15:39Z

theories/CTypes/CoreTypes.v

  ; type_cast := ctyp_cast
  ; tyAcc := ctyp_acc }.

+  Program Fixpoint ctyp_noVar (c : ctyp) : Prop :=


Is Program necessary here? It is odd that you didn't need to include anything for it.

gmalecha · 2017-01-25T07:17:40Z

I should have merged this a while ago, but it needs updates now.

gmalecha · 2017-05-31T01:03:43Z

@jesper-bengtson are you developing on 8.5 or have you moved to 8.6?

Added a reifiction function for modular reification without pmaps.

1bd7b45

gmalecha requested changes Dec 11, 2016

View reviewed changes

jesper-bengtson and others added 12 commits December 11, 2016 17:34

Refactored the modular reification wrappers.

3252327

Bug with sections and reification. Example can be found in examples/P…

2e44cbf

…olyApply/Test.v

Pushed another bug to the reifier

7b6cc3d

reporting ill-typedness error now reports error instead of anomoly.

0e7702f

- fixing the Test file.

Working on counter examples for the reifier.

d83c84a

Resolved conflicts

ebfc087

Still have bugs in Test.v

2aa724f

Reverted ReifyView

386b22e

implements tc_lemma reification.

c0657dd

moving tc_lemma into Lemma.

998ecdf

the types of Commands are not relevent to anything.

32ba676

- NOTE: since type checking was failing, it seems likely that there is an issue with the environments. It would be better to figure out what the problem is and fix it. - we should drop that information entirely

makeing PolyApply/Test.v work.

4b809a3

gmalecha requested changes Dec 17, 2016

View reviewed changes

jesper-bengtson added 4 commits December 20, 2016 10:17

Minor updates

6b8cc8d

Minor bug fixes

d67e707

Added unification functions for the modular funcs, as well as a unifi…

5a61a71

…cation rule for any RSym.

Added lemmas to the polymorphic types and lemmas.

bf030bc

gmalecha requested changes Jan 25, 2017

View reviewed changes

Minor changes

f8c5f74

gmalecha self-assigned this May 31, 2017

Conversation

jesper-bengtson commented Dec 11, 2016

Uh oh!

gmalecha left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jesper-bengtson commented Dec 11, 2016 via email

Uh oh!

gmalecha commented Dec 17, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gmalecha commented Jan 25, 2017

Uh oh!

gmalecha commented May 31, 2017

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants