Merge branch 'dev' into refactor/everything
This commit is contained in:
commit
1b901b1c25
@ -88,6 +88,7 @@ module Simplify = struct
|
||||
("sha_256" , "SHA256") ;
|
||||
("sha_512" , "SHA512") ;
|
||||
("blake2b" , "BLAKE2b") ;
|
||||
("cons" , "CONS") ;
|
||||
]
|
||||
|
||||
let type_constants = type_constants
|
||||
@ -228,6 +229,11 @@ module Typer = struct
|
||||
|
||||
let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
|
||||
|
||||
let list_cons : typer = typer_2 "CONS" @@ fun hd tl ->
|
||||
let%bind tl' = get_t_list tl in
|
||||
let%bind () = assert_type_value_eq (hd , tl') in
|
||||
ok tl
|
||||
|
||||
let map_remove : typer = typer_2 "MAP_REMOVE" @@ fun k m ->
|
||||
let%bind (src , _) = get_t_map m in
|
||||
let%bind () = assert_type_value_eq (src , k) in
|
||||
@ -617,6 +623,7 @@ module Typer = struct
|
||||
slice ;
|
||||
address ;
|
||||
assertion ;
|
||||
list_cons ;
|
||||
]
|
||||
|
||||
end
|
||||
@ -691,6 +698,7 @@ module Compiler = struct
|
||||
("HASH_KEY" , simple_unary @@ prim I_HASH_KEY) ;
|
||||
("PACK" , simple_unary @@ prim I_PACK) ;
|
||||
("CONCAT" , simple_binary @@ prim I_CONCAT) ;
|
||||
("CONS" , simple_binary @@ prim I_CONS) ;
|
||||
]
|
||||
|
||||
(*
|
||||
|
@ -5,6 +5,10 @@ const fb : foobar = list
|
||||
42 ;
|
||||
end
|
||||
|
||||
const fb2 : foobar = 144 # fb
|
||||
|
||||
const fb3 : foobar = cons(688 , fb2)
|
||||
|
||||
function size_ (const m : foobar) : nat is
|
||||
block {skip} with (size(m))
|
||||
|
||||
|
@ -405,6 +405,14 @@ let list () : unit result =
|
||||
let expected = ez [23 ; 42] in
|
||||
expect_eq_evaluate program "fb" expected
|
||||
in
|
||||
let%bind () =
|
||||
let expected = ez [144 ; 23 ; 42] in
|
||||
expect_eq_evaluate program "fb2" expected
|
||||
in
|
||||
let%bind () =
|
||||
let expected = ez [688 ; 144 ; 23 ; 42] in
|
||||
expect_eq_evaluate program "fb3" expected
|
||||
in
|
||||
let%bind () =
|
||||
let make_input = fun n -> (ez @@ List.range n) in
|
||||
let make_expected = e_nat in
|
||||
|
Loading…
Reference in New Issue
Block a user