Commit 67c1adfb authored by Andrei Paskevich's avatar Andrei Paskevich

update extraction drivers and Mlinterp

parent 8de79cf7
......@@ -5,14 +5,15 @@ prelude "#include <stdint.h>"
prelude "#include <stdio.h>"
prelude "#include <assert.h>"
module ref.Ref
module Ref
syntax type ref "%1"
syntax val ref "%1"
syntax val contents "%1"
end
module ref.Ref
syntax val (!_) "%1"
syntax converter (!_) "%1"
syntax val (:=) "%1 = %2"
syntax converter contents "%1"
end
module mach.int.Unsigned
......
......@@ -48,10 +48,13 @@ theory list.Length
syntax function length "List.length %1"
end
module ref.Ref
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
......
......@@ -69,6 +69,17 @@ end
(* WhyML *)
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
module stack.Stack
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
......
......@@ -68,10 +68,13 @@ theory list.Combine
syntax function combine "List.combine %1 %2"
end
module ref.Ref
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
......
......@@ -391,7 +391,7 @@ let exec_print _ args =
let built_in_modules =
[
["bool"],"Bool", [],
["why3"; "Bool"],"Bool", [],
[ "True", eval_true ;
"False", eval_false ;
] ;
......@@ -505,16 +505,16 @@ let built_in_modules =
"set", exec_matrix_set ;
"copy", exec_matrix_copy ;
] ;
["ref"],"Ref",
[], (* ? *)
["why3"; "Ref"],"Ref", [],
["ref", exec_ref_make ;
"mk ref", exec_ref_make ;
"contents", exec_ref_get ;
Ident.op_prefix "!", exec_ref_get;
] ;
["ref"],"Ref", [],
[Ident.op_prefix "!", exec_ref_get;
Ident.op_infix ":=", exec_ref_set;
] ;
["debug"],"Debug",
[],
["debug"],"Debug", [],
["print", exec_print ] ;
]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment