The Coq mailing list

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