pipeline works

This commit is contained in:
Galfour 2019-03-23 13:47:18 +00:00
parent ecefa598f7
commit ccd4a17aac
6 changed files with 99 additions and 15 deletions

View File

@ -132,6 +132,61 @@ module PP = struct
and type_value ppf (tv:type_value) : unit = and type_value ppf (tv:type_value) : unit =
type_value' ppf tv.type_value type_value' ppf tv.type_value
let rec annotated_expression ppf (ae:annotated_expression) : unit =
match ae.type_annotation.simplified with
| Some _ -> fprintf ppf "%a:%a" expression ae.expression type_value ae.type_annotation
| _ -> expression ppf ae.expression
and expression ppf (e:expression) : unit =
match e with
| Literal l -> literal ppf l
| Constant (c, lst) -> fprintf ppf "%s(%a)" c (list_sep annotated_expression) lst
| Constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
| Variable a -> fprintf ppf "%s" a
| Application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
| Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
| Lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
binder type_value input_type type_value output_type
block body annotated_expression result
| Tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
| Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
and literal ppf (l:literal) : unit =
match l with
| Unit -> fprintf ppf "unit"
| Bool b -> fprintf ppf "%b" b
| Int n -> fprintf ppf "%d" n
| Nat n -> fprintf ppf "%d" n
| String s -> fprintf ppf "%s" s
| Bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
and block ppf (b:block) = (list_sep instruction) ppf b
and single_record_patch ppf ((s, ae) : string * ae) =
fprintf ppf "%s <- %a" s annotated_expression ae
and matching ppf (m:matching) = match m with
| Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep (fun ppf -> fprintf ppf "%s")) lst block b
| Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" block match_true block match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" block match_nil hd tl block match_cons
| Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none some block match_some
and instruction ppf (i:instruction) = match i with
| Skip -> fprintf ppf "skip"
| Fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| Assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| Matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae matching m
end end
@ -165,16 +220,18 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
@@ Assert.assert_true List.(length ta = length tb) in @@ Assert.assert_true List.(length ta = length tb) in
bind_list_iter assert_type_value_eq (List.combine ta tb) bind_list_iter assert_type_value_eq (List.combine ta tb)
) )
| Type_tuple _, _ -> fail @@ different_kinds a b
| Type_constant (ca, lsta), Type_constant (cb, lstb) -> ( | Type_constant (ca, lsta), Type_constant (cb, lstb) -> (
let%bind _ = let%bind _ =
trace_strong (different_size_constants a b) trace_strong (different_size_constants a b)
@@ Assert.assert_true List.(length lsta = length lstb) in @@ Assert.assert_true List.(length lsta = length lstb) in
let%bind _ = let%bind _ =
trace_strong (different_constants ca cb) trace_strong (different_constants ca cb)
@@ Assert.assert_true (a = b) in @@ Assert.assert_true (ca = cb) in
trace (simple_error "constant sub-expression") trace (simple_error "constant sub-expression")
@@ bind_list_iter assert_type_value_eq (List.combine lsta lstb) @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
) )
| Type_constant _, _ -> fail @@ different_kinds a b
| Type_sum a, Type_sum b -> ( | Type_sum a, Type_sum b -> (
let a' = list_of_smap a in let a' = list_of_smap a in
let b' = list_of_smap b in let b' = list_of_smap b in
@ -188,6 +245,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
@@ bind_list_iter aux (List.combine a' b') @@ bind_list_iter aux (List.combine a' b')
) )
| Type_sum _, _ -> fail @@ different_kinds a b
| Type_record a, Type_record b -> ( | Type_record a, Type_record b -> (
let a' = list_of_smap a in let a' = list_of_smap a in
let b' = list_of_smap b in let b' = list_of_smap b in
@ -201,7 +259,12 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
@@ bind_list_iter aux (List.combine a' b') @@ bind_list_iter aux (List.combine a' b')
) )
| _ -> fail @@ different_kinds a b | Type_record _, _ -> fail @@ different_kinds a b
| Type_function (param, result), Type_function (param', result') ->
let%bind _ = assert_type_value_eq (param, param') in
let%bind _ = assert_type_value_eq (result, result') in
ok ()
| Type_function _, _ -> fail @@ different_kinds a b
(* No information about what made it fail *) (* No information about what made it fail *)
let type_value_eq ab = match assert_type_value_eq ab with let type_value_eq ab = match assert_type_value_eq ab with

View File

@ -0,0 +1,4 @@
function main (const i : int) : int is
begin
skip
end with i

View File

@ -4,5 +4,3 @@ type toto is record
end end
const foo : int = 3 const foo : int = 3

View File

@ -175,11 +175,13 @@ module PP = struct
| Literal v -> fprintf ppf "%a" value v | Literal v -> fprintf ppf "%a" value v
| Function_expression c -> function_ ppf c | Function_expression c -> function_ ppf c
and function_ ppf ({input ; output ; body}:anon_function_content) = and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) =
fprintf ppf "fun (%a) : %a %a" fprintf ppf "fun (%s:%a) : %a %a return %a"
binder
type_ input type_ input
type_ output type_ output
block body block body
expression result
and assignment ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e and assignment ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e
@ -852,7 +854,7 @@ module Translate_program = struct
let%bind expr = translate_expression result in let%bind expr = translate_expression result in
let code = seq [ let code = seq [
body ; body ;
expr ; i_car ; i_push_unit ; expr ; i_car ;
dip i_drop ; dip i_drop ;
] in ] in

View File

@ -22,15 +22,23 @@ module Ligo = struct
let%bind typed = let%bind typed =
trace (simple_error "typing") @@ trace (simple_error "typing") @@
type_ simplified in type_ simplified in
let%bind _mini_c = let%bind mini_c =
trace (simple_error "transpiling") @@ trace (simple_error "transpiling") @@
transpile typed in transpile typed in
Format.printf "mini_c code : %a" Mini_c.PP.program mini_c ;
ok () ok ()
let basic () : unit result = let basic () : unit result =
Format.printf "basic test" ; Format.printf "basic test" ;
pass "./contracts/toto.ligo" pass "./contracts/toto.ligo"
let function_ () : unit result =
Format.printf "function test" ;
let%bind _ = pass "./contracts/function.ligo" in
let%bind result = easy_run_main "./contracts/function.ligo" "2" in
Format.printf "result : %a" AST_Typed.PP.annotated_expression result ;
ok ()
(* let display_basic () : unit result = (* let display_basic () : unit result =
* parse_file "./contracts/toto.ligo" >>? fun program_ast -> * parse_file "./contracts/toto.ligo" >>? fun program_ast ->
* Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program -> * Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program ->
@ -42,6 +50,7 @@ module Ligo = struct
let main = "Ligo", [ let main = "Ligo", [
test "basic" basic ; test "basic" basic ;
test "function" function_ ;
] ]
end end

View File

@ -14,6 +14,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
| Type_constant ("bool", []) -> ok (`Base Bool) | Type_constant ("bool", []) -> ok (`Base Bool)
| Type_constant ("int", []) -> ok (`Base Int) | Type_constant ("int", []) -> ok (`Base Int)
| Type_constant ("string", []) -> ok (`Base String) | Type_constant ("string", []) -> ok (`Base String)
| Type_constant _ -> simple_fail "unrecognized constant"
| Type_sum m -> | Type_sum m ->
let node = Append_tree.of_list @@ list_of_map m in let node = Append_tree.of_list @@ list_of_map m in
let aux a b : type_value result = let aux a b : type_value result =
@ -38,28 +39,35 @@ let rec translate_type (t:AST.type_value) : type_value result =
ok (`Pair (a, b)) ok (`Pair (a, b))
in in
Append_tree.fold_ne translate_type aux node Append_tree.fold_ne translate_type aux node
| _ -> simple_fail "todo" | Type_function (param, result) ->
let%bind param' = translate_type param in
let%bind result' = translate_type result in
ok (`Function (param', result'))
let rec translate_block env (b:AST.block) : block result = let rec translate_block env (b:AST.block) : block result =
let env' = Environment.extend env in let env' = Environment.extend env in
let%bind instructions = bind_list @@ List.map (translate_instruction env) b in let%bind instructionss = bind_list @@ List.map (translate_instruction env) b in
let instructions = List.concat instructionss in
ok (instructions, env') ok (instructions, env')
and translate_instruction (env:Environment.t) (i:AST.instruction) : statement result = and translate_instruction (env:Environment.t) (i:AST.instruction) : statement list result =
let return x = ok [x] in
match i with match i with
| Assignment {name;annotated_expression} -> | Assignment {name;annotated_expression} ->
let%bind expression = translate_annotated_expression env annotated_expression in let%bind expression = translate_annotated_expression env annotated_expression in
ok @@ (Assignment (name, expression), env) return (Assignment (name, expression), env)
| Matching (expr, Match_bool {match_true ; match_false}) -> | Matching (expr, Match_bool {match_true ; match_false}) ->
let%bind expr' = translate_annotated_expression env expr in let%bind expr' = translate_annotated_expression env expr in
let%bind true_branch = translate_block env match_true in let%bind true_branch = translate_block env match_true in
let%bind false_branch = translate_block env match_false in let%bind false_branch = translate_block env match_false in
ok @@ (Cond (expr', true_branch, false_branch), env) return (Cond (expr', true_branch, false_branch), env)
| Matching _ -> simple_fail "todo : match"
| Loop (expr, body) -> | Loop (expr, body) ->
let%bind expr' = translate_annotated_expression env expr in let%bind expr' = translate_annotated_expression env expr in
let%bind body' = translate_block env body in let%bind body' = translate_block env body in
ok @@ (While (expr', body'), env) return (While (expr', body'), env)
| _ -> simple_fail "todo" | Skip -> ok []
| Fail _ -> simple_fail "todo : fail"
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result = and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
let%bind tv = translate_type ae.type_annotation in let%bind tv = translate_type ae.type_annotation in