Giter Club home page Giter Club logo

Comments (7)

ztatlock avatar ztatlock commented on July 18, 2024

@Ptival

RE: Num (a, b) vs. Num a b, Let's do whatever Coq.Ascii does.

Looks like Ascii is defined like this:

Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).

So we could be:

Inductive num : Set := Num (_ _ : ascii).

Let's also copy Ascii on low/high, which is least significant first:

Coq < Eval cbv in (nat_of_ascii (Ascii false true true true true true true true)).
     = 254
     : nat

So we would be low then high.

from kraken.

Ptival avatar Ptival commented on July 18, 2024

@ztatlock

Small problem:

You used to take apart a num in KrakenImpl.ml in such a way:

let int_of_num n =
  Char.code (MlCoq.char_of_ascii n)

Maybe the num type used to be just an ascii and the constructor could be ignored. But now, the extracted num is:

type num =
| Num of MlCoq.ascii * MlCoq.ascii

Thus, I can't take the type apart since it doesn't exist yet... (otherwise, circular build KrakenImpl <-> Message).

There are two solutions I can think of ATM.

One is to force the extraction to a couple of asciis. This way, no "Num" constructor problem...

Another is to resolve the circularity somehow. For instance, defining the num type in KrakenImpl.ml, and axiomatizing it in Message.v, or something...

What think?

from kraken.

ztatlock avatar ztatlock commented on July 18, 2024

I think your first solution is the right one for now: force extraction of Num to be a pair of Ascii values.

Would it work to just define Num as ascii * ascii ? Does it need to be a proper Inductive type?

from kraken.

Ptival avatar Ptival commented on July 18, 2024

A bit stuck on recv_msg.

It used to create goals like these:

subgoal 2 is:
 forall v : num,
 hprop_unpack tr (fun tr0 : Trace => traced (RecvNum c v ++ tr0) * bound c) ==>
 ?1561 v
subgoal 3 is:
 ?1561 (Num (Ascii true true b1 b2 b3 b4 b5 b6)) ==> ?1583 * emp
subgoal 4 is:
 forall v : msg,
 ?1583 * [v = BadTag m] ==>
 hprop_unpack tr (fun tr0 : Trace => traced (RecvMsg c v ++ tr0) * bound c)
subgoal 5 is:
 ?1561 (Num (Ascii true false true b2 b3 b4 b5 b6)) ==> ?1599 * emp
subgoal 6 is:
 forall v : msg,
 ?1599 * [v = BadTag m] ==>
 hprop_unpack tr (fun tr0 : Trace => traced (RecvMsg c v ++ tr0) * bound c)
subgoal 7 is:
 ?1561 (Num (Ascii true false false true b3 b4 b5 b6)) ==> ?1615 * emp
subgoal 8 is:
 forall v : msg,
 ?1615 * [v = BadTag m] ==>
 hprop_unpack tr (fun tr0 : Trace => traced (RecvMsg c v ++ tr0) * bound c)
subgoal 9 is:
 ?1561 (Num (Ascii true false false false true b4 b5 b6)) ==> ?1631 * emp
subgoal 10 is:
 forall v : msg,
 ?1631 * [v = BadTag m] ==>
 hprop_unpack tr (fun tr0 : Trace => traced (RecvMsg c v ++ tr0) * bound c)
subgoal 11 is:
 ?1561 (Num (Ascii true false false false false true b5 b6)) ==> ?1647 * emp

For some reason, they contain very specific values of Num, I don't even know why... It looks like it is "sortof" enumerating possible values of Num in a very weird fashion...

In my case, it gets worse as it gives me unsolvable goals :(

subgoal 2 is:
 traced (Recv c (Ascii true false true b2 b3 b4 b5 b6 :: a0 :: nil) :: x) ==>
 traced (Recv c (a1 :: b7 :: nil) :: x)
subgoal 3 is:
 traced (Recv c (Ascii true false false true b3 b4 b5 b6 :: a0 :: nil) :: x) ==>
 traced (Recv c (a1 :: b7 :: nil) :: x)
subgoal 4 is:
 traced
   (Recv c (Ascii true false false false true b4 b5 b6 :: a0 :: nil) :: x) ==>
 traced (Recv c (a1 :: b7 :: nil) :: x)
subgoal 5 is:
 traced
   (Recv c (Ascii true false false false false true b5 b6 :: a0 :: nil) :: x) ==>
 traced (Recv c (a1 :: b7 :: nil) :: x)
subgoal 6 is:
 traced
   (Recv c (Ascii true false false false false false true b6 :: a0 :: nil)
    :: x) ==> traced (Recv c (a1 :: b7 :: nil) :: x)
subgoal 7 is:
 traced (Recv c ("129" :: a0 :: nil) :: x) ==>
 traced (Recv c (a1 :: b7 :: nil) :: x)
subgoal 8 is:
 traced (Recv c ("001" :: Ascii true b8 b9 b10 b11 b12 b13 b14 :: nil) :: x) ==>
 traced (Recv c (a1 :: b15 :: nil) :: x)

from kraken.

Ptival avatar Ptival commented on July 18, 2024

P.S. Did not have such trouble when I had a Num constructor.

Maybe I should keep the constructor, and force the extraction to pairs :(

from kraken.

ztatlock avatar ztatlock commented on July 18, 2024

@Ptival is there a branch I can pull to look at this?

What do the type of Num and defn of recv_num look like now?

from kraken.

Ptival avatar Ptival commented on July 18, 2024

Fixed by 9c87abb

from kraken.

Related Issues (20)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.