The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

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
> >
> >