Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] rewrite problem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewrite problem


chronological Thread 
  • From: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] rewrite problem
  • Date: Fri, 01 Oct 2010 13:56:08 -0400

You're right, and I'm feeling terribly foolish for not having noticed the binding long ago.

Michael Doerrie

On 10/01/2010 11:59 AM, Alexandre Pilkiewicz wrote:
Hi

I think the problem is :
    (fun (ixi : Sem.S.O.I.t * Sem.S.O.I.t) (s : Sem.S.t) =>

you rebind s, so it's not the same one!

Hope this helps

Alexandre

2010/10/1 M. Scott 
Doerrie<mdoerri AT cs.jhu.edu>:
Adam Chlipala wrote:
M. Scott Doerrie wrote:
Why won't "rewrite Hopt2 in Hopt6" work.  It fails with: Found no subterm
matching "Sem.S.RefMapS.find a s" in Hopt6.  It's clearly present, even when
using "Set Printing All."
Assuming that you've eyeballed the code properly and checked that the
terms really match (which I haven't done), the problem could be that [Hopt6]
would no longer be well-typed after the rewrite.  I suggest running [Check
P], where [P] is a hand-rewritten version of the term.  If this fails, then
you'll have the culprit.  The [rewrite] error message for cases like this
could definitely be improved. ;)
Well, this handwriting the term Checks as type Prop.  Still working the pl2
upgrade angle.

  Check @eq (option Sem.S.O.C.t)
           (@option_map1 Sem.S.O.t (option Sem.S.O.C.t)
              (fun o : Sem.S.O.t =>  Sem.SC.OC.getCap i_src o)
              (@None Sem.S.O.C.t)
              (@option_map
                 (prod
                    (prod
                       (prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                          ObjectLabels.ProjectedObjectLabel.t)
                       ObjectTypes.ProjectedObjectType.t)
                    ObjectSchedules.ProjectedObjectSchedule.t)
                 (Sem.S.O.IndexMapS.t Sem.S.O.C.t) Sem.SC.tupleGetObj
                 (@Sem.S.RefMapS.find
                    (prod
                       (prod
                          (prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                             ObjectLabels.ProjectedObjectLabel.t)
                          ObjectTypes.ProjectedObjectType.t)
                       ObjectSchedules.ProjectedObjectSchedule.t) a
                    (@fold_right Sem.S.t (prod Sem.S.O.I.t Sem.S.O.I.t)
                       (fun (ixi : prod Sem.S.O.I.t Sem.S.O.I.t)
                          (s : Sem.S.t) =>
                        @option_map1 Sem.S.O.C.t Sem.S.t
                          (fun cap : Sem.S.O.C.t =>
                           Sem.SC.addCap (@snd Sem.S.O.I.t Sem.S.O.I.t ixi)
                             cap (Sem.S.O.C.target invoked_cap) s) s
                          (@option_map1 Sem.S.O.t
                             (option Sem.S.O.C.t)
                             (fun o : Sem.S.O.t =>
                              Sem.SC.OC.getCap
                                (@fst Sem.S.O.I.t Sem.S.O.I.t ixi) o)
                             (@None Sem.S.O.C.t)
                             (@option_map
                                (prod
                                   (prod
                                      (prod
                                         (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                                         ObjectLabels.ProjectedObjectLabel.t)
                                      ObjectTypes.ProjectedObjectType.t)
                                   ObjectSchedules.ProjectedObjectSchedule.t)
                                (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                                Sem.SC.tupleGetObj
                                (@Some
                                  (prod
                                    (prod
                                      (prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                                        ObjectLabels.ProjectedObjectLabel.t)
                                      ObjectTypes.ProjectedObjectType.t)

  ObjectSchedules.ProjectedObjectSchedule.t)
                                  (@pair
                                    (prod
                                      (prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                                        ObjectLabels.ProjectedObjectLabel.t)
                                      ObjectTypes.ProjectedObjectType.t)
                                    ObjectSchedules.ProjectedObjectSchedule.t
                                    (@pair
                                      (prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                                        ObjectLabels.ProjectedObjectLabel.t)
                                      ObjectTypes.ProjectedObjectType.t
                                      (@pair (Sem.S.O.IndexMapS.t
Sem.S.O.C.t)
                                        ObjectLabels.ProjectedObjectLabel.t
actor actor_lbl)
                                      actor_type) actor_sched)))))
                       (@option_map1 Sem.S.O.I.t Sem.S.t
                          (fun i : Sem.S.O.I.t =>
                           Sem.SC.addCap i
                             (Sem.S.O.C.mkCap a
                                (AccessRights.AccessRightFSet.singleton
                                   AccessRights.send))
                             (Sem.S.O.C.target invoked_cap) s) s opt_i)
                       ixi_list)))) (@Some Sem.S.O.C.t t_cap).


Michael Doerrie





Archive powered by MhonArc 2.6.16.

Top of Page