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 05 May 2009 02:06:36 PM UTC  
 
Category: DevelopmentModule: BiCoax
Priority: 7 - HighSeverity: 4 - Important
Status: PostponedPrivacy: Public
Assigned to: Samuel Colin <scolin>Open/Closed: Open

Thu 03 Feb 2011 11:00:58 PM UTC, 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 03 Feb 2011 10:02:06 PM UTC, 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 03 Feb 2011 09:41:32 PM UTC, 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 05 May 2009 06:55:31 PM UTC, 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 05 May 2009 02:06:36 PM UTC, 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.

     

    Please enter the title of George Orwell's famous dystopian book (it's a date):

     

     

    Follow 3 latest changes.

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

    Back to the top


    Powered by Savane 3.1-cleanup