copilot-language / copilot Goto Github PK

The travis file still tries to compile with GHC 7.10. Since we don't support it, it needs to be removed.

Currently, it seems it is not possible to get either the integer (truncate) or decimal part (like modf does in C) of a Stream Double, or to truncate, say, a Stream Float into a Stream Int32 with unsafeCast.

This makes for instance difficult the implementation of combination of oscillators dealing with floating-point values, like the following (which doesn't work):

-- Program outputs analog values within the interval [0, maxAnalogOut]
maxAnalogOut = 255

type Millis = Word32

-- Milliseconds since the program has started
timeMillis :: Stream Millis
timeMillis = externFun "millis" [] (Just simu)
    where simu = [0] ++ (10 + simu)

sawtoothOsc, sinOsc :: Stream Double  -- ^ period (in milliseconds)
                   -> Stream Millis  -- ^ time since beginning
                   -> Stream Double

sawtoothOsc period millis = modf (cast millis / period)  -- decimal part

sinOsc period millis = sin $ 2*pi * cast millis / period

-- Modulate period of sawtoothOsc from output of sinOsc
intensity = maxAnalogOut * sawtoothOsc (250 * sinOsc 4000 timeMillis + 250) timeMillis

(sawtoothOsc could be expressed using only Stream Word32 but sinOsc couldn't. So we need either be able to use Doubles everywhere or to force cast a Stream Double to a Stream Word32 in order to compose the two oscillators)

Gitignore does not include things that new building tools use, profiling files, etc.

The Copilot website is referring to the old repo

Submodule references should be updated to match the release of 3.0

The current version of copilot fails to compile with GHC 7.*.

The issues in particular have to do with the use of underscore in type families and the syntax for language extensions. The latter is easily solvable, the former, I think not.

It might be smarter to remove these from the travis file, and add only 8.0 and 8.2 for now, unless we want to remain compatible with 7.* for some reason.

The type signature for the list index function !! is too strict by requiring the type variable of the list of streams and the index stream to be of the same type. This makes it impossible to index a list of Floats. See below for example and a new version with the type signature updated.
Type signature for !! now:

(!!) :: (Integral a, Typed a) => [Stream a] -> Stream a -> Stream a

Example

listF = [constF 3, constF 4]
listI = [constI32 3, constI32 (-4)]

bangbang :: (Typed a, Eq b, Num b, Typed b) => [Stream a] -> Stream b -> Stream a
bangbang ls n =
  let indices = map (constant . fromIntegral) [0 .. P.length ls - 1]
      select [] _ = last ls
      select (i:is) (x:xs) = mux (i == n) x (select is xs)
  in select indices ls

listFspec :: Spec
listFspec = do
  observer "listF" $ listF `bangbang` (constI32 0)
-- Whereas using !!
--  observer "listF!!" $ listF !! (constI32 0)
-- results in
--     Couldn't match type `Int32' with `Float'
--     Expected type: Stream Float
--       Actual type: Stream Int32
--     In the second argument of `(!!)', namely `(constI32 0)'
--     In the second argument of `($)', namely `listF !! (constI32 0)'

As they stand, the installation instructions would not initialize or download the submodules.

When I try to build copilot core I get this error:
https://gist.github.com/octopuscabbage/abf529a426ce8c6de1d2

I think it has to do with Applicative now being a superclass of monad.

Update readme for version 3.0 deprecating some libraries (SBV, C99, CBMC) and include the new backend (cbackend).

Update examples to match new syntax and features, remove some of them as well.

We can start from the old website that @leepike created. The sources are here:

https://github.com/leepike/Copilot/tree/gh-pages

The README.md currently says that an executable XXX will be created during installation, but, obviously, that does not exist.

Gitignore does not include things that new building tools use, profiling files, etc.

The copilot3.0-dev branch fails to compile with GHC 8.6/base-4.12:

src/Copilot/Theorem/TransSys/Spec.hs:129:6: error:
    • Data.Map.fold is gone. Use foldr.

It compiles fine with GHC 8.4/base-4.11.

Submodules for 2.x should point to the latest 2.x commits

The file tutorial.log is a latex file uploaded by mistake. It should be removed.

Gitignore does not include things that new building tools use, profiling files, etc.

Frank has done a lot of the work in the new copilot, and he is still not credited.

The cabal file still lists the old repo as the reference for copilot.

It should point to this organization's github.

The travis file still tries to compile with GHC 7.10. Since we don't support it, it needs to be removed.

The cabal file points to Lee Pike's repos for the examples and the discussion.

Cast operator cast to source type, not target type

There's a few typos in the readme, and the style could be clearer.

To be more consistent with package name, rename to modules from C to C99

The manifest should explain the git repo structure, and how it should be used for development and releases.

Gitignore does not include things that new building tools use, profiling files, etc.

Gitignore does not include things that new building tools use, profiling files, etc.

This library depends on pretty-ncols, which fails to compile with versions of GHC >= 8.4 (base >= 4.11) because Prelude exports (<>), which conflicts with Text.PrettyPrint.<>:

Preprocessing library pretty-ncols-0.1...
[1 of 1] Compiling Text.PrettyPrint.NCol ( Text/PrettyPrint/NCol.hs, dist/dist-sandbox-11467d12/build/Text/PrettyPrint/NCol.o )

Text/PrettyPrint/NCol.hs:27:25: error:
    Ambiguous occurrence ‘<>’
    It could refer to either ‘Prelude.<>’,
                             imported from ‘Prelude’ at Text/PrettyPrint/NCol.hs:1:8-28
                             (and originally defined in ‘GHC.Base’)
                          or ‘Text.PrettyPrint.<>’,
                             imported from ‘Text.PrettyPrint’ at Text/PrettyPrint/NCol.hs:4:1-23
                             (and originally defined in ‘Text.PrettyPrint.HughesPJ’)
   |
27 |         where buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
   |                         ^^

Text/PrettyPrint/NCol.hs:27:55: error:
    Ambiguous occurrence ‘<>’
    It could refer to either ‘Prelude.<>’,
                             imported from ‘Prelude’ at Text/PrettyPrint/NCol.hs:1:8-28
                             (and originally defined in ‘GHC.Base’)
                          or ‘Text.PrettyPrint.<>’,
                             imported from ‘Text.PrettyPrint’ at Text/PrettyPrint/NCol.hs:4:1-23
                             (and originally defined in ‘Text.PrettyPrint.HughesPJ’)
   |
27 |         where buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
   |                                                       ^^
cabal: Leaving directory '/tmp/cabal-tmp-19047/pretty-ncols-0.1'
Failed to install pretty-ncols-0.1
cabal: Entering directory '/tmp/cabal-tmp-19047/random-1.1'

Pretty-ncols is not on github and has not been updated in a very long time. I just sent an email to the author.

The heater example contains a few bugs and typos

Having the prefix first and then the spec allows use to write reify spec >>= compile "prefix" in a main function.

Gitignore does not include things that new building tools use, profiling files, etc.

Currently, due to pretty-ncols not being updated to base >= 4.11, the interpreter is unable to show output. We should (temporarily) copy the functions in pretty-ncols to the interpreter.

The travis file still tries to compile with GHC 7.*. Since we don't support it, it needs to be removed.

While compiling a spec with an array, compilation loops until the stack is full

The travis file still tries to compile with GHC 7.10. Since we don't support it, it needs to be removed.

The travis file still tries to compile with GHC 7.10. Since we don't support it, it needs to be removed.