rewriting

This commit is contained in:
Galfour 2019-03-27 13:02:38 +00:00
parent 89a7821e87
commit 4025e9e169
6 changed files with 243 additions and 48 deletions

View File

@ -58,12 +58,17 @@ and expression =
| Application of ae * ae
(* Tuple *)
| Tuple of ae list
| Tuple_accessor of ae * int (* Access n'th tuple's element *)
(* Sum *)
| Constructor of name * ae (* For user defined constructors *)
(* Record *)
| Record of ae_map
| Record_accessor of ae * string
| Accessor of ae * access_path
and access =
| Tuple_access of int
| Record_access of string
and access_path = access list
and literal =
| Unit
@ -81,7 +86,7 @@ and instruction =
| Loop of ae * b
| Skip
| Fail of ae
| Record_patch of ae * (string * ae) list
| Record_patch of name * access_path * (string * ae) list
and matching =
| Match_bool of {
@ -130,22 +135,29 @@ module PP = struct
| Constructor (name, ae) -> fprintf ppf "%s(%a)" name annotated_expression ae
| Constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep annotated_expression) lst
| Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
| Tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
| Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
| Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
| Lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
binder type_expression input_type type_expression output_type
block body annotated_expression result
and access ppf (a:access) =
match a with
| Tuple_access n -> fprintf ppf "%d" n
| Record_access s -> fprintf ppf "%s" s
and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep ~pp_sep:(const ".") access) p
and annotated_expression ppf (ae:annotated_expression) = match ae.type_annotation with
| None -> fprintf ppf "%a" expression ae.expression
| Some t -> fprintf ppf "(%a) : %a" expression ae.expression type_expression t
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 single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
and matching ppf (m:matching) = match m with
| Match_tuple (lst, b) ->
@ -160,7 +172,7 @@ module PP = struct
and instruction ppf (i:instruction) = match i with
| Skip -> fprintf ppf "skip"
| Fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| Record_patch (ae, lst) -> fprintf ppf "%a.[%a]" annotated_expression ae (list_sep single_record_patch) lst
| Record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep single_record_patch) lst
| 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
@ -177,6 +189,116 @@ module PP = struct
fprintf ppf "%a" (list_sep declaration) p
end
module Rename = struct
module Type = struct
(* Type renaming, not needed. Yet. *)
end
module Value = struct
type renaming = string * (string * access_path) (* src -> dst *)
type renamings = renaming list
let filter (r:renamings) (s:string) : renamings =
List.filter (fun (x, _) -> not (x = s)) r
let filters (r:renamings) (ss:string list) : renamings =
List.filter (fun (x, _) -> not (List.mem x ss)) r
let rec rename_instruction (r:renamings) (i:instruction) : instruction result =
match i with
| Assignment ({name;annotated_expression = e} as a) ->
let%bind annotated_expression = rename_annotated_expression (filter r name) e in
ok (Assignment {a with annotated_expression})
| Skip -> ok Skip
| Fail e ->
let%bind e' = rename_annotated_expression r e in
ok (Fail e')
| Loop (cond, body) ->
let%bind cond' = rename_annotated_expression r cond in
let%bind body' = rename_block r body in
ok (Loop (cond', body'))
| Matching (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching r m in
ok (Matching (ae', m'))
| Record_patch (v, path, lst) ->
let aux (x, y) =
let%bind y' = rename_annotated_expression (filter r v) y in
ok (x, y') in
let%bind lst' = bind_map_list aux lst in
match List.assoc_opt v r with
| None -> (
ok (Record_patch (v, path, lst'))
)
| Some (v, path') -> (
ok (Record_patch (v, path' @ path, lst'))
)
and rename_block (r:renamings) (bl:block) : block result =
bind_map_list (rename_instruction r) bl
and rename_matching (r:renamings) (m:matching) : matching result =
match m with
| Match_bool { match_true = mt ; match_false = mf } ->
let%bind match_true = rename_block r mt in
let%bind match_false = rename_block r mf in
ok (Match_bool {match_true ; match_false})
| Match_option { match_none = mn ; match_some = (some, ms) } ->
let%bind match_none = rename_block r mn in
let%bind ms' = rename_block (filter r some) ms in
ok (Match_option {match_none ; match_some = (some, ms')})
| Match_list { match_nil = mn ; match_cons = (hd, tl, mc) } ->
let%bind match_nil = rename_block r mn in
let%bind mc' = rename_block (filters r [hd;tl]) mc in
ok (Match_list {match_nil ; match_cons = (hd, tl, mc')})
| Match_tuple (lst, body) ->
let%bind body' = rename_block (filters r lst) body in
ok (Match_tuple (lst, body'))
and rename_annotated_expression (r:renamings) (ae:annotated_expression) : annotated_expression result =
let%bind expression = rename_expression r ae.expression in
ok {ae with expression}
and rename_expression (r:renamings) (e:expression) : expression result =
match e with
| Literal _ as l -> ok l
| Constant (name, lst) ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (Constant (name, lst'))
| Constructor (name, ae) ->
let%bind ae' = rename_annotated_expression r ae in
ok (Constructor (name, ae'))
| Variable v -> (
match List.assoc_opt v r with
| None -> ok (Variable v)
| Some (name, path) -> ok (Accessor (ae (Variable (name)), path))
)
| Lambda ({binder;body;result} as l) ->
let r' = filter r binder in
let%bind body = rename_block r' body in
let%bind result = rename_annotated_expression r' result in
ok (Lambda {l with body ; result})
| Application (f, arg) ->
let%bind f' = rename_annotated_expression r f in
let%bind arg' = rename_annotated_expression r arg in
ok (Application (f', arg'))
| Tuple lst ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (Tuple lst')
| Accessor (ae, p) ->
let%bind ae' = rename_annotated_expression r ae in
ok (Accessor (ae', p))
(* let aux prev hd =
* match hd with
* | Tuple_access n -> Tuple_accessor (prev, n)
* | Record_access s -> Record_accessor (prev, s)
* in
* let lst = List.fold_left aux ae p in
* ok lst *)
| Record sm ->
let%bind sm' = bind_smap
@@ SMap.map (rename_annotated_expression r) sm in
ok (Record sm')
end
end
module Simplify = struct
module Raw = Ligo_parser.AST
@ -191,6 +313,9 @@ module Simplify = struct
("nat", 0) ;
("int", 0) ;
("bool", 0) ;
("list", 1) ;
("set", 1) ;
("map", 2) ;
]
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
@ -269,7 +394,7 @@ module Simplify = struct
let record = p.value.record_name.value in
let lst = List.map (fun (x:_ Raw.reg) -> x.value) @@ npseq_to_list p.value.field_path in
let aux prev cur =
ae @@ Record_accessor (prev, cur)
ae @@ Accessor (prev, [Record_access cur])
in
let init = ae @@ Variable record in
ok @@ List.fold_left aux init lst
@ -382,23 +507,65 @@ module Simplify = struct
ok @@ Constant_declaration {name=name.value;annotated_expression={expression with type_annotation}}
| LambdaDecl (FunDecl x) ->
let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in
let%bind param = match npseq_to_list param.value.inside with
| [a] -> ok a
| _ -> simple_fail "only one param allowed" in
let%bind input = simpl_param param in
let name = name.value in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations = bind_list @@ List.map simpl_local_declaration local_decls in
let%bind instructions = bind_list
@@ List.map simpl_instruction
@@ npseq_to_list block.value.instr in
let%bind result = simpl_expression return in
let%bind output_type = simpl_type_expression ret_type in
let body = local_declarations @ instructions in
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (Type_function (input_type, output_type)) in
ok @@ Constant_declaration {name;annotated_expression = {expression;type_annotation}}
(match npseq_to_list param.value.inside with
| [] -> simple_fail "function without parameters are not allowed"
| [a] -> (
let%bind input = simpl_param a in
let name = name.value in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations = bind_list @@ List.map simpl_local_declaration local_decls in
let%bind instructions = bind_list
@@ List.map simpl_instruction
@@ npseq_to_list block.value.instr in
let%bind result = simpl_expression return in
let%bind output_type = simpl_type_expression ret_type in
let body = local_declarations @ instructions in
let decl =
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (Type_function (input_type, output_type)) in
Constant_declaration {name;annotated_expression = {expression;type_annotation}}
in
ok decl
)
| lst -> (
let%bind params = bind_map_list simpl_param lst in
let input =
let type_expression = Type_record (
SMap.of_list
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
params
) in
{ type_name = "arguments" ; type_expression } in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations =
bind_list @@ List.map simpl_local_declaration local_decls in
let%bind output_type = simpl_type_expression ret_type in
let%bind instructions = bind_list
@@ List.map simpl_instruction
@@ npseq_to_list block.value.instr in
let%bind (body, result) =
let renamings =
let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
type_name, ("arguments", [Record_access type_name])
in
List.map aux params
in
let%bind r = simpl_expression return in
let%bind b =
let tmp = local_declarations @ instructions in
Rename.Value.rename_block renamings tmp
in
ok (b, r) in
let decl =
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (Type_function (input_type, output_type)) in
Constant_declaration {name="arguments";annotated_expression = {expression;type_annotation}}
in
ok decl
)
)
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
@ -453,7 +620,7 @@ module Simplify = struct
@@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
@@ List.map (fun (x:_ Raw.reg) -> x.value)
@@ npseq_to_list r.record_inj.value.fields in
ok @@ Record_patch ({expression=Variable record;type_annotation=None}, inj)
ok @@ Record_patch (record, [], inj)
| MapPatch _ -> simple_fail "no map patch yet"
and simpl_cases (t:(Raw.pattern * block) list) : matching result =

View File

@ -3,7 +3,10 @@ module SMap = X_map.String
let const s ppf () = pp_print_string ppf s
let list_sep pp = pp_print_list ~pp_sep:(const " ; ") pp
let list_sep ?(pp_sep = const " ; ") pp =
pp_print_list ~pp_sep pp
let pair_sep pp ppf (a, b) = fprintf ppf "(%a, %a)" pp a pp b
let smap_sep pp ppf m =
let aux k v prev = (k, v) :: prev in

View File

@ -66,6 +66,8 @@ let bind_smap (s:_ X_map.String.t) =
ok @@ add k v' prev' in
fold aux s (ok empty)
let bind_map_list f lst = bind_list (List.map f lst)
let bind_fold_list f init lst =
let aux x y =
x >>? fun x ->

View File

@ -1 +1,17 @@
module String = Map.Make(String)
module Make(Ord : Map.OrderedType) = struct
include Map.Make(Ord)
let of_list (lst: (key * 'a) list) : 'a t =
let aux prev (k, v) = add k v prev in
List.fold_left aux empty lst
let to_list (t: 'a t) : 'a list =
let aux _k v prev = v :: prev in
fold aux t []
let to_kv_list (t: 'a t) : (key * 'a) list =
let aux k v prev = (k, v) :: prev in
fold aux t []
end
module String = Make(String)

View File

@ -32,7 +32,7 @@ module TestExpressions = struct
let unit () : unit result = test_expression (unit ()) (make_t_unit)
let int () : unit result = test_expression (number 32) (make_t_int)
let bool () : unit result = test_expression (bool true) (make_t_bool)
let bool () : unit result = test_expression (Simplified.Combinators.bool true) (make_t_bool)
let string () : unit result = test_expression (string "s") (make_t_string)
let bytes () : unit result = test_expression (bytes "b") (make_t_bytes)

View File

@ -259,14 +259,29 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let tv_lst = List.map get_annotation lst' in
let%bind type_annotation = check (make_t_tuple tv_lst) in
ok O.{expression = Tuple lst' ; type_annotation }
| Tuple_accessor (tpl, ind) ->
let%bind tpl' = type_annotated_expression e tpl in
let%bind tpl_tv = get_t_tuple tpl'.type_annotation in
let%bind tv =
generic_try (simple_error "bad tuple index")
@@ (fun () -> List.nth tpl_tv ind) in
let%bind type_annotation = check tv in
ok O.{expression = O.Tuple_accessor (tpl', ind) ; type_annotation}
| Accessor (ae, path) ->
let%bind e' = type_annotated_expression e ae in
let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
match a with
| Tuple_access index -> (
let%bind tpl_tv = get_t_tuple prev.type_annotation in
let%bind tv =
generic_try (simple_error "bad tuple index")
@@ (fun () -> List.nth tpl_tv index) in
let%bind type_annotation = check tv in
ok O.{expression = O.Tuple_accessor (prev, index) ; type_annotation}
)
| Record_access property -> (
let%bind r_tv = get_t_record prev.type_annotation in
let%bind tv =
generic_try (simple_error "bad record index")
@@ (fun () -> SMap.find property r_tv) in
let%bind type_annotation = check tv in
ok O.{expression = O.Record_accessor (prev, property) ; type_annotation }
)
in
bind_fold_list aux e' path
(* Sum *)
| Constructor (c, expr) ->
let%bind (c_tv, sum_tv) =
@ -286,14 +301,6 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind m' = SMap.fold aux m (ok SMap.empty) in
let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in
ok O.{expression = O.Record m' ; type_annotation }
| Record_accessor (r, ind) ->
let%bind r' = type_annotated_expression e r in
let%bind r_tv = get_t_record r'.type_annotation in
let%bind tv =
generic_try (simple_error "bad record index")
@@ (fun () -> SMap.find ind r_tv) in
let%bind type_annotation = check tv in
ok O.{expression = O.Record_accessor (r', ind) ; type_annotation }
| Lambda {
binder ;
input_type ;
@ -386,7 +393,7 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
return (Tuple lst')
| Tuple_accessor (tpl, ind) ->
let%bind tpl' = untype_annotated_expression tpl in
return (Tuple_accessor (tpl', ind))
return (Accessor (tpl', [Tuple_access ind]))
| Constructor (n, p) ->
let%bind p' = untype_annotated_expression p in
return (Constructor (n, p'))
@ -396,7 +403,7 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
return (Record r')
| Record_accessor (r, s) ->
let%bind r' = untype_annotated_expression r in
return (Record_accessor (r', s))
return (Accessor (r', [Record_access s]))
and untype_block (b:O.block) : (I.block) result =
bind_list @@ List.map untype_instruction b