bugBRILLANT - Bugs: bug #13485, has type "Z ⇒ Prop"...

 
 
Show feedback again

You are not allowed to post comments on this tracker with your current authentification level.

bug #13485: has type "Z ⇒ Prop" while it is expected to have type "Z"

Submitted by:  Georges Mariano <gmariano>
Submitted on:  Tue May 5 14:06:36 2009  
 
Category: DevelopmentModule: BiCoax
Priority: 7 - HighSeverity: 4 - Important
Status: PostponedPrivacy: Public
Assigned to: Samuel Colin <scolin>Open/Closed: Open

Thu Feb 3 23:00:58 2011, comment #4:

Why not... it's ok for me...

I would be able to add this (this belongs to the very small set of my ocaml skills) but I'm rather busy/distracted with thousands of other things these days ;)

But maybe it's worth for you to keep working on btyper2 ;)

The bug should be closed since it will disappear wrt Bicoax, but I agree with you until we find a better solution than defining a new bug "we need a type checker" ;)

Georges Mariano <gmariano>
Project Administrator
Thu Feb 3 22:02:06 2011, comment #3:

Then I suggest '>*<' for cartesian product, because the ASCII '><' notation is already reserved for the direct product (in mathematical unicode notation it corresponds to something like '⨂').

If it is agreed upon I shall add support for it.

And I'd rather not close the bug until we have a typechecker able to correct this problem.

Samuel Colin <scolin>
Project AdministratorIn charge of this item.
Thu Feb 3 21:41:32 2011, comment #2:

"This bug stems from the multiplication/cartesian product ambiguity currently not solved by the upstream tools"

Yes.
Maybe we can try to add a new lexeme (says '><') for the cartesian product in what we use to call B' language

(recall B' is B without the few ugly lexical ambiguities)

Same hint for '-' and '\' ambiguity (but '\' is already available in bparser)

This is not the perfect correction but we can also elaborate that "one" type checking can be provided by the discharged obligation proofs ... Of course, we also need to hack manually the B specifications to be able to test bparser/bgop/bicoax chain on that... This is why we used to have so called ..._1 projects in our benchmark (_1 stands for B1 == B')

Georges Mariano <gmariano>
Project Administrator
Tue May 5 18:55:31 2009, comment #1:

This bug stems from the multiplication/cartesian product ambiguity currently not solved by the upstream tools (need a typechecker phase before the bgop phase to solve the problem).

Samuel Colin <scolin>
Project AdministratorIn charge of this item.
Tue May 5 14:06:36 2009, original submission:

Running BiCoax on BOILER...

find . -name "*.v.log" | xargs grep "it is expected"

./bgop/Acq_1/Initialization__00013.v.log:The term "1 ‥ NB_PUMP" has type "Z ⇒ Prop" while it is expected to have type "Z"
./bgop/Acq_1/Initialization__00011.v.log:
./bgop/Acq_1/Initialization__00020.v.log:
./bgop/Acq_1/Initialization__00015.v.log:
./bgop/Acq_1/Op__main_Acquisition__00038.v.log:
./bgop/Acq_1/Op__main_Acquisition__00039.v.log:
./bgop/Acq_1/Initialization__00010.v.log:
./bgop/Acq_1/Initialization__00017.v.log:
./bgop/Acq_1/Initialization__00019.v.log:
./bgop/Acq_1/Initialization__00018.v.log:
./bgop/Acq_1/Op__main_Acquisition__00040.v.log:
./bgop/Acq_1/Initialization__00012.v.log:
./bgop/Acq_1/Op__main_Acquisition__00037.v.log:
./bgop/Acq_1/Initialization__00014.v.log:
./bgop/Acq_1/Initialization__00016.v.log:
./bgop/Acq_1/Initialization__00009.v.log:

Georges Mariano <gmariano>
Project Administrator

 

No files currently attached

 

Depends on the following items: None found

Items that depend on this one: None found

 

Carbon-Copy List
  • -unavailable- added by scolin (Posted a comment)
  • -unavailable- added by gmariano (Submitted the item)
  •  

    Do you think this task is very important?
    If so, you can click here to add your encouragement to it.
    This task has 0 encouragements so far.

    Only logged-in users can vote.

     

    Error: not logged in

     

     

    Follow 3 latest changes.

    Date Changed By Updated Field Previous Value => Replaced By
    Tue May 5 18:55:31 2009scolinPriority5 - Normal=>7 - High
      Severity3 - Normal=>4 - Important
      StatusNone=>Postponed
    Show feedback again

    Back to the top


    Powered by Savane 3.1-cleanup