stedolan / malfunction Goto Github PK
View Code? Open in Web Editor NEWMalfunctional Programming
License: Other
Malfunctional Programming
License: Other
I tried to run the primerec
-example (I didn't edit any files). It compiled with warning and crashed at runtime:
$ dune build examples/primrec.exe
File "_none_", line 1:
Warning 58: no cmx file was found in path for module Middle_end, and its interface was not compiled with -opaque
$ dune exec -- examples/primrec.exe
Fatal error: exception Failure("camlMalfunction_Code_1")
But if the usage of compile_and_load
-function (primrec.ml, lines 122, 147) is commented out, then there will be no error.
Could you please tell me what I'm doing wrong. My compiler verison is 4.07.1.
Hi!
Maybe you can add a missing installation step in the README, between opam install and malfunction compile ...
? Like ocamlbuild -use-findlib
or however you do it. Also, for me, it was not added to ocamlfind when I did the opam pin and installation, had to do it manually.
Regards
Olle
Here's a program reading out of bounds:
$ echo '(module (_ (load.byte "" 1)) (export))' > example.mlf
$ malfunction compile example.mlf -o example
The program compiles fine. Then I run it.
$ ./example
Fatal error: exception Invalid_argument("index out of bounds")
It seems that the read is checked but I would expect to get a segfault or (most likely) nothing printed at all because that's what Malfunction does whenever you make any other mistake. I have not benchmarked how much overhead it incurs but not having unchecked array access feels wrong, especially in such an inherently unsafe environment.
Given that we don't want to add %primitives
, I can see two options:
Making Mvecget
and Mvecset
translate to the unchecked primitives instead. This will make them faster, and give you undefined behaviour if you get it wrong, which is consistent with the behaviour of Malfunction everywhere else.
Creating new unchecked builtins. Then for debugging purposes, a compiler targetting Malfunction could switch to checked builtins to get a bit of runtime checking for free.
I'm happy to implement either. Are there better ways to do this?
When I use Malfunction_compiler.compile_and_load
with [`Verbose]
flag I get the following error:
Fatal error: exception Unix.Unix_error(Unix.ENOTEMPTY, "rmdir", "/tmp/malfunction46896e.tmp")
It works fine without this option. This error appears every time I use this flag. In particular, you can call with verbose
option in compile_and_load
from examples/primrec.ml
and get the same error.
The error message when you try to apply a value that is not a function could be more helpful.
As a minimal example when I try to compile this file:
(module
($f 0)
(_ (apply $f))
(export)
)
I get the error:
Fatal error: exception File "asmcomp/compilenv.ml", line 336, characters 2-8: Assertion failed
OCaml has many primitives in Lambda, which are mostly generated from %
-primitives in the source code. It would be nice to add support for these.
During the talk, you mentioned a "type system which will solve the world's programming problems forever, unifying every possible type of language feature into one grand abstraction", and presented a slide showing "Higher-kinded dependently-typed GOTO".
But Malfunction doesn't have continuations, just lambdas. You can't even write GOTO, much less COMEFROM. Furthermore it seems like continuations are an elegant way to unify eager and lazy programming.
My point here is that while OCaml doesn't support continuations, SML/NJ does. I guess it's a little slower than OCaml, but not by much (7.8 vs 9.3 seconds in a toy benchmark).
There is a difference between the interpreter(1) and the Compiler in handling zero argument functions.
Updated the comment to only report the inconsistency.
Support for FFI would be nice.
Installing Malfunction with version 4.03.0+flambda works like a breeze. Doing the same using 4.04.0+flambda however results in this error:
#=== ERROR while installing malfunction.~unknown ==============================#
# opam-version 1.2.2
# os darwin
# command ocaml pkg/pkg.ml build --pinned true
# path /Users/Tim/.opam/4.04.0+flambda/build/malfunction.~unknown
# compiler 4.04.0+flambda
# exit-code 1
# env-file /Users/Tim/.opam/4.04.0+flambda/build/malfunction.~unknown/malfunction-57250-ad8886.env
# stdout-file /Users/Tim/.opam/4.04.0+flambda/build/malfunction.~unknown/malfunction-57250-ad8886.out
# stderr-file /Users/Tim/.opam/4.04.0+flambda/build/malfunction.~unknown/malfunction-57250-ad8886.err
### stdout ###
# [...]
# ocamlfind ocamlc -c -g -bin-annot -package unix -package str -package compiler-libs.optcomp -package zarith -package findlib -package dynlink -w @8 -I src -o src/malfunction_interpreter.cmi src/malfunction_interpreter.mli
# + ocamlfind ocamlc -c -g -bin-annot -package unix -package str -package compiler-libs.optcomp -package zarith -package findlib -package dynlink -w @8 -I src -o src/malfunction_interpreter.cmi src/malfunction_interpreter.mli
# findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /Users/Tim/.opam/4.04.0+flambda/lib/ocaml/compiler-libs, /Users/Tim/.opam/4.04.0+flambda/lib/ocaml
# ocamlfind ocamlopt -c -g -bin-annot -package unix -package str -package compiler-libs.optcomp -package zarith -package findlib -package dynlink -w @8 -I src -o src/malfunction_compiler.cmx src/malfunction_compiler.ml
# + ocamlfind ocamlopt -c -g -bin-annot -package unix -package str -package compiler-libs.optcomp -package zarith -package findlib -package dynlink -w @8 -I src -o src/malfunction_compiler.cmx src/malfunction_compiler.ml
# findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /Users/Tim/.opam/4.04.0+flambda/lib/ocaml/compiler-libs, /Users/Tim/.opam/4.04.0+flambda/lib/ocaml
# File "src/malfunction_compiler.ml", line 205, characters 27-41:
# Error: The constructor Lprim expects 3 argument(s),
# but is applied here to 2 argument(s)
# Command exited with code 2.
### stderr ###
# pkg.ml: [ERROR] cmd ['ocamlbuild' '-use-ocamlfind' '-classic-display' '-tag' 'debug'
# [...]
# 'src/malfunction.cmxa' 'src/malfunction.cma'
# 'src/malfunction_interpreter.cmx' 'src/malfunction_interpreter.cmi'
# 'src/malfunction_interpreter.mli' 'src/malfunction_compiler.cmx'
# 'src/malfunction_compiler.cmi' 'src/malfunction_compiler.mli'
# 'src/malfunction_parser.cmx' 'src/malfunction_parser.cmi'
# 'src/malfunction_parser.mli' 'src/malfunction_sexp.cmx'
# 'src/malfunction_sexp.cmi' 'src/malfunction_sexp.mli'
# 'src/malfunction.cmx' 'src/malfunction.cmi' 'src/malfunction.mli'
# 'src/malfunction_main.native']: exited with 10
I'm not an OCaml user. Any idea what changed between 4.03 and 4.04? I'm on macOS 10.0.1.
Hi!
How about adding a chapter to the spec about floats? This is what I've tried so far:
(dum, List [
(dum, Atom "block");
(dum, List [
(dum, Atom "tag");
(dum, Int Obj.double_tag)
]);
(dum, String "1.0")
]);
but
Fatal error: exception Malfunction_sexp.SyntaxError(_, "tag 253 out of range [0,199]")
The malf code (trying to make ref a = 1.0
):
(let ($a (block (tag 0) (block (tag 253) "1.0")))
Better to use vectors of length 1 for references?
Error message I get in my fork. OK, so I fail to add the floating point primitives in the right environment. Any tips for debugging? I'd like to dump Env.t
, but can't find a way how.
Does malfunction expose ocaml exceptions (and if not, what's required to make that happen)? Both for ocaml interop and as a target for languages supporting exceptions, that would be a very welcome feature.
If I change the implementation of module X
but not its interface, it would be nice to not have to recompile all modules (transitively) depending on X
. With ocamlopt
, this can be achieved using -opaque
, which will disable cross-module optimisations (with the obvious tradeoffs). It would be nice to have that option for Malfunction, too.
This would make the compile-test loop faster and more convenient for large projects, where you're usually fiddling with only a small number of modules. It would avoid unnecessarily triggering full rebuilds if you are editing the implementation of a module at the top of the dependency hierarchy.
Sadly the lsl
operator is not very well defined in OCaml when shifting by more than a word size.
For instance on amd64, x lsl 65
is equivalent to x lsl 1
, while on arm64 it will be 0
. The evaluator should reject it.
The current check implemented to verify that recursive bindings are correct is, I think, too simplistic.
It currently only accepts immediate functions or lazy, already at parsing time:
malfunction/src/malfunction_parser.ml
Line 110 in 4227093
According to https://v2.ocaml.org/manual/letrecvalues.html, many more programs can be accepted on the right hand-side of a let rec
. This causes a problem in particular for our extraction from Coq, where a typical pattern of definition can be:
CoInductive stream := Cons { head : nat; tail : stream }.
CoFixpoint ones : stream :=
let x := bla in {| head := x; tail := ones |}.
This gets translated to (in pseudo malfunction syntax):
let rec ones = let x = bla in lazy (Cons x ones)
and is rejected. As Coq supports a kind of "positive" view of coinductives, and only optionally, by user choice, co-pattern matching, some cofixpoint definitions in the wild might actually compute a few things before calling the constructor. Of course any cofixpoint with at least one argument will be fine as it starts with a lambda.
But currently malfunction will also reject let rec ones_list = 1 :: ones_list
which is accepted by OCaml. Is there any rationale for this? As for our application in Coq, this does not matter as one cannot produce such cyclic values from Coq: every let rec
has at least one argument, except for the images of cofixpoints, but then the body's head must be a constructor.
Hey, sorry to bother you. Maybe you can help me out with this one?
(module
(let ($myVar 10) ; $myVar = 10
(_ (apply (global $Pervasives $print_string) "Hello, world!\n"))) ; body of let
(export))
Get error "no bindings?"
Malfunction is currently restricted to looking up identifiers on the standard OCaml search path, which limits malfunction programs to only accessing the standard library. It would be nice to be able to provide additional search paths to other .cmi files.
Extra nice would be ocamlfind integration.
Is there any documentation on how to add primitives to Malfunction so that we can use the OCaml standard library? Currently, I'm reading (and grepping) the sources of the OCaml compiler, the stdlib, and Malfunction, and slowly trying to figure out how everything works. Some primitives seem to be implemented as C functions; some seem to be builtins.
I tried copy-pasting bits and pieces around and editing them, which made the compiler stop complaining about some unimplemented primitives such as %string_length
(and start complaining about the next one), but don't know if it will work once it eventually compiles.
Is there any recommended reference to look at?
malfunction/src/malfunction_parser.ml
Line 110 in c4d24c5
There exist recursive values in agda , functions that have zero arguments.
For example , this code does not compile with malfunction. :
open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Nat
record Stream (A : Set) : Set where
coinductive
field
head : A
tail : Stream A
open Stream public
repeat : Stream String
head repeat = "hello"
tail repeat = repeat
lookup : ∀ {A} → Stream A → Nat → A
lookup xs zero = xs .head
lookup xs (suc n) = lookup (xs .tail) n
main : IO Unit
main = putStr (lookup repeat 1000000)
I could introduce a dummy variable , but I was wondering if you could do something from your side.
Are there any plans to support the recent versions of OCaml? If not, could you please estimate how hard it could be to upgrade Malfunction? (given the lack of previous experience with OCaml compiler hacking).
Hi, is there any hope of support for OCaml 4.14 and below. The Coq developers have been thinking about using malfunction as a target for our native compilation.
I keep getting the error "module path required" after trying to hard-code the hello world-example in sexp format:
let dum = (Lexing.dummy_pos, Lexing.dummy_pos)
let test_code =
(dum, List ([
(dum, Atom "module");
(dum, List [
(dum, Atom "_");
(dum, List [
(dum, Atom "apply");
(dum, List [
(dum, Atom "global");
(dum, Atom "$Pervasives");
(dum, Atom "$print_string")
]);
(dum, String "Hello, world!\n");
])
]);
(dum, List [
(dum, Atom "export");
])
]))
Then doing
let e = Malfunction_parser.parse_mod test_code in
after I've added parse_mod to the mli, I get the error. Any tips? How is module path supposed to look like?
Is it possible to use malfunction to compile a .mlf file to OCaml byte code?
The below file triggers an assertion in 4.07.0 OCaml.
https://github.com/ocaml/ocaml/blob/4.07/asmcomp/cmmgen.ml#L1983
I was trying to add Float support.
One weird thing that I noticed was that this was acceptable :
( $agdaIdent8.952a3c475e16a2d6.Common.IO.return
(global $ForeignCode $Common $IO $ioReturn)
)
while this was not :
( $agdaIdent2a.2ed69e510f00fd1e.Agda.Builtin.Float.primSin
(global $Stdlib $Float $sin)
)
( module
( $agdaIdenta.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatEquality
( lambda ($a $b) ( ==.f64 $a $b ) )
)
( $agdaIdentc.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatLess
( lambda ($a $b) ( <.f64 $a $b ) )
)
( $agdaIdente.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalEquality
( lambda ($a $b) ( ==.f64 $a $b ) )
)
( $agdaIdent10.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalLess
( lambda ($a $b) ( <.f64 $a $b ) )
)
( $agdaIdent1a.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNegate
( lambda ($a) ( neg.f64 $a ) )
)
( $agdaIdent1c.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatDiv
( lambda ($a $b) ( /.f64 $a $b ) )
)
( $agdaIdent26.2ed69e510f00fd1e.Agda.Builtin.Float.primExp
( lambda ($a) ( apply (global $Stdlib $Float $exp) $a ) )
)
( $agdaIdent2a.2ed69e510f00fd1e.Agda.Builtin.Float.primSin
( lambda ($a) ( apply (global $Stdlib $Float $sin) $a ) )
)
( $agdaIdent2c.2ed69e510f00fd1e.Agda.Builtin.Float.primCos
( lambda ($a) ( apply (global $Stdlib $Float $cos) $a ) )
)
( $agdaIdent2e.2ed69e510f00fd1e.Agda.Builtin.Float.primTan
( lambda ($a) ( apply (global $Stdlib $Float $tan) $a ) )
)
( $agdaIdent30.2ed69e510f00fd1e.Agda.Builtin.Float.primASin
( lambda ($a) ( apply (global $Stdlib $Float $asin) $a ) )
)
( $agdaIdent32.2ed69e510f00fd1e.Agda.Builtin.Float.primACos
( lambda ($a) ( apply (global $Stdlib $Float $acos) $a ) )
)
( $agdaIdent34.2ed69e510f00fd1e.Agda.Builtin.Float.primATan
( lambda ($a) ( apply (global $Stdlib $Float $atan) $a ) )
)
( $agdaIdent36.2ed69e510f00fd1e.Agda.Builtin.Float.primATan2
( lambda ($a) ( apply (global $Stdlib $Float $atan2) $a ) )
)
( $agdaIdent38.2ed69e510f00fd1e.Agda.Builtin.Float.primShowFloat
( lambda ($a) ( apply (global $Stdlib $Float $to_string) $a ) )
)
( $agdaIdent8.952a3c475e16a2d6.Common.IO.return
(global $ForeignCode $Common $IO $ioReturn)
)
( $agdaIdent12.952a3c475e16a2d6.Common.IO._{62}{62}{61}_
(global $ForeignCode $Common $IO $ioBind)
)
( $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
(global $ForeignCode $Common $IO $printString)
)
( $agdaIdent50.952a3c475e16a2d6.Common.IO.then
( lambda ($v0 $v1 $v2 $v3 $v4 $v5 $world)
( apply ( apply $agdaIdent12.952a3c475e16a2d6.Common.IO._{62}{62}{61}_
$v0
$v1
0
0
$v4
( lambda ($v6) $v5 )
)
$world
)
)
)
( $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
( lambda ($v0)
( switch $v0
( _ (tag _)
( switch ( ==.f64 $v0 0.0 ) ( 1 "pos" ) ( _ (tag _) "nonzero" ) )
)
)
)
)
( $agdaIdent26.d2c4f4e5116ac5f5.Floats.atan2
$agdaIdent36.2ed69e510f00fd1e.Agda.Builtin.Float.primATan2
)
( $agdaIdent24.d2c4f4e5116ac5f5.Floats.atan
$agdaIdent34.2ed69e510f00fd1e.Agda.Builtin.Float.primATan
)
( $agdaIdent22.d2c4f4e5116ac5f5.Floats.acos
$agdaIdent32.2ed69e510f00fd1e.Agda.Builtin.Float.primACos
)
( $agdaIdent20.d2c4f4e5116ac5f5.Floats.asin
$agdaIdent30.2ed69e510f00fd1e.Agda.Builtin.Float.primASin
)
( $agdaIdent1e.d2c4f4e5116ac5f5.Floats.tan
$agdaIdent2e.2ed69e510f00fd1e.Agda.Builtin.Float.primTan
)
( $agdaIdent1c.d2c4f4e5116ac5f5.Floats.cos
$agdaIdent2c.2ed69e510f00fd1e.Agda.Builtin.Float.primCos
)
( $agdaIdent1a.d2c4f4e5116ac5f5.Floats.sin
$agdaIdent2a.2ed69e510f00fd1e.Agda.Builtin.Float.primSin
)
( $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
( lambda ($v0 $world)
( apply ( apply $agdaIdent12.952a3c475e16a2d6.Common.IO._{62}{62}{61}_
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr $v0 )
( lambda ($v1)
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr "\n" )
)
)
$world
)
)
)
( $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdentc.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatLess
)
( $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent10.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalLess
)
( $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
$agdaIdente.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalEquality
)
( $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
$agdaIdenta.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatEquality
)
( $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_
$agdaIdent1c.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatDiv
)
( $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
( apply $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_ 0.0 0.0 )
)
( $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
( apply $agdaIdent1a.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNegate
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( $agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
( apply $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_ 1.0 0.0 )
)
( $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
( apply $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_ -1.0 0.0 )
)
( $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( lambda ($v0 $world)
( apply ( switch $v0
( 0
( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn "false" )
)
( 1
( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn "true" )
)
( _ (tag _)
( apply (global $Stdlib $failwith) "__UNREACHABLE__" )
)
)
$world
)
)
)
( $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
( lambda ($v0 $world)
( apply ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
( apply $agdaIdent38.2ed69e510f00fd1e.Agda.Builtin.Float.primShowFloat
$v0
)
)
$world
)
)
)
( $main
( apply (global $ForeignCode $main_run)
( apply ( lambda ($world)
( apply ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr "123.4 = " )
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print 123.4 )
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr "-42.9 = " )
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print -42.9 )
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"Inf = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
$agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-Inf = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
$agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"Inf == Inf = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
$agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
$agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN == NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN == -NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
( apply $agdaIdent1a.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNegate
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"0.0 == -0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
0.0
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"isZero 0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
( apply $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"isZero -0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
( apply $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"isZero 1.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
( apply $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
1.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN =N= NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"0.0 =N= -0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
0.0
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"0.0 =N= 12.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
0.0
12.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN < -Inf = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-Inf < NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"0.0 < -0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
0.0
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-0.0 < 0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
0.0
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN < NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-NaN < -NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN < -NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-NaN < NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN < -5.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
-5.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-5.0 < NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
-5.0
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN <N -Inf = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-Inf <N NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"0.0 <N -0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
0.0
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-0.0 <N 0.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
0.0
0.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN <N NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-NaN <N -NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN <N -NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-NaN <N NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"NaN <N -5.0 = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
-5.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"-5.0 <N NaN = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
-5.0
$agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"e = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
( apply $agdaIdent26.2ed69e510f00fd1e.Agda.Builtin.Float.primExp
1.0
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"sin (asin 0.6) = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
( apply $agdaIdent1a.d2c4f4e5116ac5f5.Floats.sin
( apply $agdaIdent20.d2c4f4e5116ac5f5.Floats.asin
0.6
)
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"cos (acos 0.6) = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
( apply $agdaIdent1c.d2c4f4e5116ac5f5.Floats.cos
( apply $agdaIdent22.d2c4f4e5116ac5f5.Floats.acos
0.6
)
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"tan (atan 0.4) = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
( apply $agdaIdent1e.d2c4f4e5116ac5f5.Floats.tan
( apply $agdaIdent24.d2c4f4e5116ac5f5.Floats.atan
0.4
)
)
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
"tan (atan2 0.4 1.0) = "
)
( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
0
0
0
0
( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
( apply $agdaIdent1e.d2c4f4e5116ac5f5.Floats.tan
( apply $agdaIdent26.d2c4f4e5116ac5f5.Floats.atan2
0.4
1.0
)
)
)
( apply $agdaIdent8.952a3c475e16a2d6.Common.IO.return
0
0
0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
$world
)
)
0
)
)
)
( export )
)
We would like to have a new release including PR #38 (we can take care of opam packaging if you like, and don't need ocaml 5 support), so as to release https://github.com/yforster/coq-malfunction on opam.
The spec asks to file a report If a program runs to completion in the interpreter producing a result, it is a bug in Malfunction if the compiled version of the same program either crashes or produces a different value
I have such a situation: a program (obtained through extraction from Coq):
compare : bytestring -> bytestring -> comparison
with string
from https://github.com/MetaCoq/metacoq/blob/coq-8.16/utils/theories/bytestring.v#L32 and type comparison = Eq | Lt | Gt
.
Running compare "" "diff"
correctly yields 1
(corresponding to Lt
) in the interpreter. The compiled program yields
Lt
on OCaml 4.13Lt
on OCaml 4.13+flambdaLt
on OCaml 4.14, andGt
on OCaml 4.14+flambdainspecting the actual value using Obj
tools shows that the return value is not really 2
(Gt
), but the full string "diff"
.
See https://github.com/yforster/malfunction-malfunctioning/actions/runs/6533871602/job/17739907316
The error can alternatively be circumvented by disabling optimisation passes in malfunction cmx
(the linked repository uses a patched version where optimisation has to be explicitly enabled via malfunction cmx -O2
).
malfunction currently fails with the following error on OCaml 5.2:
#=== ERROR while compiling malfunction.0.5 ====================================#
# context 2.2.0~beta2~dev | linux/x86_64 | ocaml-variants.5.2.0+trunk | file:///home/opam/opam-repository
# path ~/.opam/5.2/.opam-switch/build/malfunction.0.5
# command ~/.opam/5.2/bin/dune build -p malfunction -j 1
# exit-code 1
# env-file ~/.opam/log/malfunction-20-93572e.env
# output-file ~/.opam/log/malfunction-20-93572e.out
### output ###
# (cd _build/default && /home/opam/.opam/5.2/bin/ocamlc.opt -w -40 -g -bin-annot -I src/.malfunction.objs/byte -I /home/opam/.opam/5.2/lib/findlib -I /home/opam/.opam/5.2/lib/ocaml/compiler-libs -I /home/opam/.opam/5.2/lib/ocaml/dynlink -I /home/opam/.opam/5.2/lib/ocaml/str -I /home/opam/.opam/5.2/lib/ocaml/unix -I /home/opam/.opam/5.2/lib/zarith -no-alias-deps -o src/.malfunction.objs/byte/malfunction_compat.cmo -c -impl src/malfunction_compat.ml)
# File "malfunction_compat.cppo.ml", lines 15-25, characters 13-3:
# Error: Some record fields are undefined: "may_fuse_arity"
opam cannot find a solution so as to install malfunction.
Some OCaml code uses mixed mutable and immutable blocks, such as this:
type q = { x : int; mutable y : int; }
It would be useful for Malfunction to support this.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.