add div and mod ; stabilize before adding deep closures

This commit is contained in:
Galfour 2019-04-30 12:02:22 +00:00
parent 2674e84199
commit 2dc6b4a263
9 changed files with 51 additions and 14 deletions

View File

@ -1,3 +1,6 @@
function mod_op (const n : int) : nat is
begin skip end with n mod 42
function plus_op (const n : int) : int is function plus_op (const n : int) : int is
begin skip end with n + 42 begin skip end with n + 42

View File

@ -38,9 +38,10 @@ function insert (const h : heap ; const e : heap_element) : heap is
var i : nat := size(h) + 1n ; var i : nat := size(h) + 1n ;
h[i] := e ; h[i] := e ;
var largest : nat := i ; var largest : nat := i ;
var parent : nat := 0n ;
while (largest =/= i) block { while (largest =/= i) block {
parent := i / 2n ;
largest := i ; largest := i ;
const parent : nat = i / 2n ;
if (parent >= 1n) then block { if (parent >= 1n) then block {
if (heap_element_lt(get_force(parent , h) , get_force(i , h))) then block { if (heap_element_lt(get_force(parent , h) , get_force(i , h))) then block {
largest := parent ; largest := parent ;

View File

@ -242,6 +242,16 @@ module Typer = struct
* ) * )
* ] *) * ] *)
let num_2 : typer_predicate =
let aux = fun a b ->
(type_value_eq (a , t_int ()) || type_value_eq (a , t_nat ())) &&
(type_value_eq (b , t_int ()) || type_value_eq (b , t_nat ())) in
predicate_2 aux
let mod_ = "MOD" , 2 , [
num_2 , constant_2 "MOD" (t_nat ()) ;
]
let constant_typers = let constant_typers =
let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in
Map.String.of_list Map.String.of_list
@ -255,6 +265,11 @@ module Typer = struct
("TIMES_INT" , t_int ()) ; ("TIMES_INT" , t_int ()) ;
("TIMES_NAT" , t_nat ()) ; ("TIMES_NAT" , t_nat ()) ;
] ; ] ;
same_2 "DIV" [
("DIV_INT" , t_int ()) ;
("DIV_NAT" , t_nat ()) ;
] ;
mod_ ;
sub ; sub ;
none ; none ;
some ; some ;
@ -309,6 +324,9 @@ module Compiler = struct
("SUB_NAT" , simple_binary @@ prim I_SUB) ; ("SUB_NAT" , simple_binary @@ prim I_SUB) ;
("TIMES_INT" , simple_binary @@ prim I_MUL) ; ("TIMES_INT" , simple_binary @@ prim I_MUL) ;
("TIMES_NAT" , simple_binary @@ prim I_MUL) ; ("TIMES_NAT" , simple_binary @@ prim I_MUL) ;
("DIV_INT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
("DIV_NAT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
("MOD" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "MOD by 0") ; i_cdr]) ;
("NEG" , simple_unary @@ prim I_NEG) ; ("NEG" , simple_unary @@ prim I_NEG) ;
("OR" , simple_binary @@ prim I_OR) ; ("OR" , simple_binary @@ prim I_OR) ;
("AND" , simple_binary @@ prim I_AND) ; ("AND" , simple_binary @@ prim I_AND) ;

View File

@ -37,11 +37,12 @@ let parse_file (source: string) : AST_Raw.t result =
in in
simple_error str simple_error str
) )
| _ -> | exn ->
let start = Lexing.lexeme_start_p lexbuf in let start = Lexing.lexeme_start_p lexbuf in
let end_ = Lexing.lexeme_end_p lexbuf in let end_ = Lexing.lexeme_end_p lexbuf in
let str = Format.sprintf let str = Format.sprintf
"Unrecognized error at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n" "Unrecognized error (%s) at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n"
(Printexc.to_string exn)
(Lexing.lexeme lexbuf) (Lexing.lexeme lexbuf)
start.pos_lnum (start.pos_cnum - start.pos_bol) start.pos_lnum (start.pos_cnum - start.pos_bol)
end_.pos_lnum (end_.pos_cnum - end_.pos_bol) end_.pos_lnum (end_.pos_cnum - end_.pos_bol)

View File

@ -464,7 +464,7 @@ let esc = "\\n" | "\\\"" | "\\\\" | "\\b"
let symbol = ';' | ',' | '(' | ')'| '[' | ']' | '{' | '}' let symbol = ';' | ',' | '(' | ')'| '[' | ']' | '{' | '}'
| '#' | '|' | "->" | ":=" | '=' | ':' | '#' | '|' | "->" | ":=" | '=' | ':'
| '<' | "<=" | '>' | ">=" | "=/=" | '<' | "<=" | '>' | ">=" | "=/="
| '+' | '-' | '*' | '.' | '_' | '^' | '+' | '-' | '*' | '/' | '.' | '_' | '^'
let string = [^'"' '\\' '\n']* (* For strings of #include *) let string = [^'"' '\\' '\n']* (* For strings of #include *)
(* RULES *) (* RULES *)

View File

@ -152,6 +152,10 @@ let rec simpl_expression (t:Raw.expr) : ae result =
simpl_binop "SUB" c.value simpl_binop "SUB" c.value
| EArith (Mult c) -> | EArith (Mult c) ->
simpl_binop "TIMES" c.value simpl_binop "TIMES" c.value
| EArith (Div c) ->
simpl_binop "DIV" c.value
| EArith (Mod c) ->
simpl_binop "MOD" c.value
| EArith (Int n) -> | EArith (Int n) ->
let n = Z.to_int @@ snd @@ n.value in let n = Z.to_int @@ snd @@ n.value in
ok @@ make_e_a @@ E_literal (Literal_int n) ok @@ make_e_a @@ E_literal (Literal_int n)

View File

@ -113,12 +113,12 @@ let pop () : unit result =
let%bind _ = bind_list let%bind _ = bind_list
@@ List.map aux @@ List.map aux
@@ [2 ; 7 ; 12] in @@ [2 ; 7 ; 12] in
(* simple_fail "display" *) simple_fail "display"
ok () (* ok () *)
let main = "Heap (End to End)", [ let main = "Heap (End to End)", [
test "is_empty" is_empty ; test "is_empty" is_empty ;
test "get_top" get_top ; test "get_top" get_top ;
test "pop_switch" pop_switch ; test "pop_switch" pop_switch ;
test "pop" pop ; (* test "pop" pop ; *)
] ]

View File

@ -103,9 +103,11 @@ let arithmetic () : unit result =
("plus_op", fun n -> (n + 42)) ; ("plus_op", fun n -> (n + 42)) ;
("minus_op", fun n -> (n - 42)) ; ("minus_op", fun n -> (n - 42)) ;
("times_op", fun n -> (n * 42)) ; ("times_op", fun n -> (n * 42)) ;
("div_op", fun n -> (n / 2)) ; (* ("div_op", fun n -> (n / 2)) ; *)
] in ] in
let%bind () = expect_n_pos program "int_op" e_a_nat e_a_int in let%bind () = expect_n_pos program "int_op" e_a_nat e_a_int in
let%bind () = expect_n_pos program "mod_op" e_a_int (fun n -> e_a_nat (n mod 42)) in
let%bind () = expect_n_pos program "div_op" e_a_int (fun n -> e_a_int (n / 2)) in
ok () ok ()
let unit_expression () : unit result = let unit_expression () : unit result =

View File

@ -14,12 +14,20 @@ let test name f =
open Ast_simplified.Combinators open Ast_simplified.Combinators
let expect program entry_point input expected = let expect program entry_point input expected =
let error = let%bind result =
let run_error =
let title () = "expect run" in let title () = "expect run" in
let content () = Format.asprintf "Entry_point: %s" entry_point in let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content in error title content in
trace error @@ trace run_error @@
let%bind result = Ligo.easy_run_typed_simplified entry_point program input in Ligo.easy_run_typed_simplified entry_point program input in
let expect_error =
let title () = "expect result" in
let content () = Format.asprintf "Expected %a, got %a"
Ast_simplified.PP.value expected
Ast_simplified.PP.value result in
error title content in
trace_strong expect_error @@
Ast_simplified.assert_value_eq (expected , result) Ast_simplified.assert_value_eq (expected , result)
let expect_evaluate program entry_point expected = let expect_evaluate program entry_point expected =
@ -32,10 +40,10 @@ let expect_evaluate program entry_point expected =
Ast_simplified.assert_value_eq (expected , result) Ast_simplified.assert_value_eq (expected , result)
let expect_n_aux lst program entry_point make_input make_expected = let expect_n_aux lst program entry_point make_input make_expected =
Format.printf "expect_n aux\n%!" ;
let aux n = let aux n =
let input = make_input n in let input = make_input n in
let expected = make_expected n in let expected = make_expected n in
trace (simple_error ("expect_n " ^ (string_of_int n))) @@
let result = expect program entry_point input expected in let result = expect program entry_point input expected in
result result
in in