refactor ast_simplified

This commit is contained in:
Galfour 2019-04-21 12:08:12 +00:00
parent 7a2bd3d73d
commit 0e04a152bb
9 changed files with 476 additions and 474 deletions

View File

@ -0,0 +1,95 @@
open Types
open PP_helpers
open Format
let list_sep_d x = list_sep x (const " , ")
let smap_sep_d x = smap_sep x (const " , ")
let rec type_expression ppf (te:type_expression) = match te with
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d type_expression) lst
| T_sum m -> fprintf ppf "sum[%a]" (smap_sep_d type_expression) m
| T_record m -> fprintf ppf "record[%a]" (smap_sep_d type_expression) m
| T_function (p, r) -> fprintf ppf "%a -> %a" type_expression p type_expression r
| T_variable name -> fprintf ppf "%s" name
| T_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep_d type_expression) lst
let literal ppf (l:literal) = match l with
| Literal_unit -> fprintf ppf "Unit"
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int n -> fprintf ppf "%d" n
| Literal_nat n -> fprintf ppf "%d" n
| Literal_string s -> fprintf ppf "%S" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
let rec expression ppf (e:expression) = match e with
| E_literal l -> literal ppf l
| E_variable name -> fprintf ppf "%s" name
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" annotated_expression f annotated_expression arg
| E_constructor (name, ae) -> fprintf ppf "%s(%a)" name annotated_expression ae
| E_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep_d annotated_expression) lst
| E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d annotated_expression) lst
| E_accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
| E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m
| E_list lst -> fprintf ppf "list[%a]" (list_sep_d annotated_expression) lst
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
| E_lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
binder type_expression input_type type_expression output_type
block body annotated_expression result
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and access ppf (a:access) =
match a with
| Access_tuple n -> fprintf ppf "%d" n
| Access_record s -> fprintf ppf "%s" s
and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep access (const ".")) p
and type_annotation ppf (ta:type_expression option) = match ta with
| None -> fprintf ppf ""
| Some t -> type_expression ppf t
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 (tag "@;")) ppf b
and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
and matching : type a . (formatter -> a -> unit) -> formatter -> a matching -> unit =
fun f ppf m -> match m with
| Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep_d string) lst f b
| Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" f match_nil hd tl f match_cons
| Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst
| I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
let declaration ppf (d:declaration) = match d with
| Declaration_type {type_name ; type_expression = te} ->
fprintf ppf "type %s = %a" type_name type_expression te
| Declaration_constant {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae
let program ppf (p:program) =
fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) (List.map Location.unwrap p)

View File

@ -1,430 +1,4 @@
module SMap = Map.String
type name = string
type type_name = string
type 'a name_map = 'a SMap.t
type 'a type_name_map = 'a SMap.t
type program = declaration Location.wrap list
and declaration =
| Declaration_type of named_type_expression
| Declaration_constant of named_expression
(* | Macro_declaration of macro_declaration *)
and annotated_expression = {
expression: expression ;
type_annotation: te option ;
}
and named_expression = {
name: name ;
annotated_expression: ae ;
}
and named_type_expression = {
type_name: type_name ;
type_expression: type_expression ;
}
and te = type_expression
and ae = annotated_expression
and te_map = type_expression type_name_map
and ae_map = annotated_expression name_map
and type_expression =
| T_tuple of te list
| T_sum of te_map
| T_record of te_map
| T_function of te * te
| T_variable of type_name
| T_constant of type_name * te list
and lambda = {
binder: name ;
input_type: type_expression ;
output_type: type_expression ;
result: ae ;
body: block ;
}
and expression =
(* Base *)
| E_literal of literal
| E_constant of (name * ae list) (* For language constants, like (Cons hd tl) or (plus i j) *)
| E_variable of name
| E_lambda of lambda
| E_application of (ae * ae)
(* E_Tuple *)
| E_tuple of ae list
(* Sum *)
| E_constructor of (name * ae) (* For user defined constructors *)
(* E_record *)
| E_record of ae_map
| E_accessor of (ae * access_path)
(* Data Structures *)
| E_map of (ae * ae) list
| E_list of ae list
| E_look_up of (ae * ae)
(* Matching *)
| E_matching of (ae * matching_expr)
and access =
| Access_tuple of int
| Access_record of string
and access_path = access list
and literal =
| Literal_unit
| Literal_bool of bool
| Literal_int of int
| Literal_nat of int
| Literal_string of string
| Literal_bytes of bytes
and block = instruction list
and b = block
and instruction =
| I_assignment of named_expression
| I_matching of ae * matching_instr
| I_loop of ae * b
| I_skip
| I_fail of ae
| I_record_patch of name * access_path * (string * ae) list
and 'a matching =
| Match_bool of {
match_true : 'a ;
match_false : 'a ;
}
| Match_list of {
match_nil : 'a ;
match_cons : name * name * 'a ;
}
| Match_option of {
match_none : 'a ;
match_some : name * 'a ;
}
| Match_tuple of name list * 'a
and matching_instr = b matching
and matching_expr = annotated_expression matching
let ae expression = {expression ; type_annotation = None}
let annotated_expression expression type_annotation = {expression ; type_annotation}
open Trace
module PP = struct
open PP_helpers
open Format
let list_sep_d x = list_sep x (const " , ")
let smap_sep_d x = smap_sep x (const " , ")
let rec type_expression ppf (te:type_expression) = match te with
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d type_expression) lst
| T_sum m -> fprintf ppf "sum[%a]" (smap_sep_d type_expression) m
| T_record m -> fprintf ppf "record[%a]" (smap_sep_d type_expression) m
| T_function (p, r) -> fprintf ppf "%a -> %a" type_expression p type_expression r
| T_variable name -> fprintf ppf "%s" name
| T_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep_d type_expression) lst
let literal ppf (l:literal) = match l with
| Literal_unit -> fprintf ppf "Unit"
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int n -> fprintf ppf "%d" n
| Literal_nat n -> fprintf ppf "%d" n
| Literal_string s -> fprintf ppf "%S" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
let rec expression ppf (e:expression) = match e with
| E_literal l -> literal ppf l
| E_variable name -> fprintf ppf "%s" name
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" annotated_expression f annotated_expression arg
| E_constructor (name, ae) -> fprintf ppf "%s(%a)" name annotated_expression ae
| E_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep_d annotated_expression) lst
| E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d annotated_expression) lst
| E_accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
| E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m
| E_list lst -> fprintf ppf "list[%a]" (list_sep_d annotated_expression) lst
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
| E_lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
binder type_expression input_type type_expression output_type
block body annotated_expression result
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and access ppf (a:access) =
match a with
| Access_tuple n -> fprintf ppf "%d" n
| Access_record s -> fprintf ppf "%s" s
and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep access (const ".")) p
and type_annotation ppf (ta:type_expression option) = match ta with
| None -> fprintf ppf ""
| Some t -> type_expression ppf t
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 (tag "@;")) ppf b
and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
and matching : type a . (formatter -> a -> unit) -> formatter -> a matching -> unit =
fun f ppf m -> match m with
| Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep_d string) lst f b
| Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" f match_nil hd tl f match_cons
| Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst
| I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
let declaration ppf (d:declaration) = match d with
| Declaration_type {type_name ; type_expression = te} ->
fprintf ppf "type %s = %a" type_name type_expression te
| Declaration_constant {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae
let program ppf (p:program) =
fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) (List.map Location.unwrap 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
| I_assignment ({name;annotated_expression = e} as a) -> (
match List.assoc_opt name r with
| None ->
let%bind annotated_expression = rename_annotated_expression (filter r name) e in
ok (I_assignment {a with annotated_expression})
| Some (name', lst) -> (
let%bind annotated_expression = rename_annotated_expression r e in
match lst with
| [] -> ok (I_assignment {name = name' ; annotated_expression})
| lst ->
let (hds, tl) =
let open List in
let r = rev lst in
rev @@ tl r, hd r
in
let%bind tl' = match tl with
| Access_record n -> ok n
| Access_tuple _ -> simple_fail "no support for renaming into tuples yet" in
ok (I_record_patch (name', hds, [tl', annotated_expression]))
)
)
| I_skip -> ok I_skip
| I_fail e ->
let%bind e' = rename_annotated_expression r e in
ok (I_fail e')
| I_loop (cond, body) ->
let%bind cond' = rename_annotated_expression r cond in
let%bind body' = rename_block r body in
ok (I_loop (cond', body'))
| I_matching (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching rename_block r m in
ok (I_matching (ae', m'))
| I_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 (I_record_patch (v, path, lst'))
)
| Some (v', path') -> (
ok (I_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 : type a . (renamings -> a -> a result) -> renamings -> a matching -> a matching result =
fun f r m ->
match m with
| Match_bool { match_true = mt ; match_false = mf } ->
let%bind match_true = f r mt in
let%bind match_false = f r mf in
ok (Match_bool {match_true ; match_false})
| Match_option { match_none = mn ; match_some = (some, ms) } ->
let%bind match_none = f r mn in
let%bind ms' = f (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 = f r mn in
let%bind mc' = f (filters r [hd;tl]) mc in
ok (Match_list {match_nil ; match_cons = (hd, tl, mc')})
| Match_tuple (lst, body) ->
let%bind body' = f (filters r lst) body in
ok (Match_tuple (lst, body'))
and rename_matching_instruction = fun x -> rename_matching rename_block x
and rename_matching_expr = fun x -> rename_matching rename_expression x
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 : renamings -> expression -> expression result = fun r e ->
match e with
| E_literal _ as l -> ok l
| E_constant (name, lst) ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (E_constant (name, lst'))
| E_constructor (name, ae) ->
let%bind ae' = rename_annotated_expression r ae in
ok (E_constructor (name, ae'))
| E_variable v -> (
match List.assoc_opt v r with
| None -> ok (E_variable v)
| Some (name, path) -> ok (E_accessor (ae (E_variable (name)), path))
)
| E_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 (E_lambda {l with body ; result})
| E_application (f, arg) ->
let%bind f' = rename_annotated_expression r f in
let%bind arg' = rename_annotated_expression r arg in
ok (E_application (f', arg'))
| E_tuple lst ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (E_tuple lst')
| E_accessor (ae, p) ->
let%bind ae' = rename_annotated_expression r ae in
ok (E_accessor (ae', p))
| E_record sm ->
let%bind sm' = bind_smap
@@ SMap.map (rename_annotated_expression r) sm in
ok (E_record sm')
| E_map m ->
let%bind m' = bind_map_list
(fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
ok (E_map m')
| E_list lst ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (E_list lst')
| E_look_up m ->
let%bind m' = bind_map_pair (rename_annotated_expression r) m in
ok (E_look_up m')
| E_matching (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching rename_annotated_expression r m in
ok (E_matching (ae', m'))
end
end
module Combinators = struct
let t_bool : type_expression = T_constant ("bool", [])
let t_string : type_expression = T_constant ("string", [])
let t_bytes : type_expression = T_constant ("bytes", [])
let t_int : type_expression = T_constant ("int", [])
let t_unit : type_expression = T_constant ("unit", [])
let t_option o : type_expression = T_constant ("option", [o])
let t_list t : type_expression = T_constant ("list", [t])
let t_tuple lst : type_expression = T_tuple lst
let t_pair a b = t_tuple [a ; b]
let t_record m : type_expression = (T_record m)
let t_ez_record (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
T_record map
let t_record_ez lst =
let m = SMap.of_list lst in
t_record m
let t_sum m : type_expression = T_sum m
let ez_t_sum (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
T_sum map
let t_function param result : type_expression = T_function (param, result)
let e_annotated_expression ?type_annotation expression = {expression ; type_annotation}
let name (s : string) : name = s
let e_var (s : string) : expression = E_variable s
let e_unit () : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b))
let e_lambda (binder : string)
(input_type : type_expression)
(output_type : type_expression)
(result : expression)
(body : block)
: expression =
E_lambda {
binder = (name binder) ;
input_type = input_type ;
output_type = output_type ;
result = (ae result) ;
body ;
}
let e_tuple (lst : ae list) : expression = E_tuple lst
let ez_e_tuple (lst : expression list) : expression =
e_tuple (List.map (fun e -> ae e) lst)
let e_constructor (s : string) (e : ae) : expression = E_constructor (name s, e)
let e_record (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
E_record map
let ez_e_record (lst : (string * expression) list) : expression =
(* TODO: define a correct implementation of List.map
* (an implementation that does not fail with stack overflow) *)
e_record (List.map (fun (s,e) -> (s, ae e)) lst)
end
include Types
module Types = Types
module PP = PP
module Combinators = Combinators

View File

@ -0,0 +1,74 @@
open Types
module SMap = Map.String
let t_bool : type_expression = T_constant ("bool", [])
let t_string : type_expression = T_constant ("string", [])
let t_bytes : type_expression = T_constant ("bytes", [])
let t_int : type_expression = T_constant ("int", [])
let t_unit : type_expression = T_constant ("unit", [])
let t_option o : type_expression = T_constant ("option", [o])
let t_list t : type_expression = T_constant ("list", [t])
let t_tuple lst : type_expression = T_tuple lst
let t_pair a b = t_tuple [a ; b]
let t_record m : type_expression = (T_record m)
let t_ez_record (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
T_record map
let t_record_ez lst =
let m = SMap.of_list lst in
t_record m
let t_sum m : type_expression = T_sum m
let ez_t_sum (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
T_sum map
let t_function param result : type_expression = T_function (param, result)
let make_e_a ?type_annotation expression = {expression ; type_annotation}
let make_e_a_full expression type_annotation = make_e_a ~type_annotation expression
let name (s : string) : name = s
let e_var (s : string) : expression = E_variable s
let e_unit () : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b))
let e_lambda (binder : string)
(input_type : type_expression)
(output_type : type_expression)
(result : expression)
(body : block)
: expression =
E_lambda {
binder = (name binder) ;
input_type = input_type ;
output_type = output_type ;
result = (make_e_a result) ;
body ;
}
let e_tuple (lst : ae list) : expression = E_tuple lst
let ez_e_tuple (lst : expression list) : expression =
e_tuple (List.map make_e_a lst)
let e_constructor (s : string) (e : ae) : expression = E_constructor (name s, e)
let e_record (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
E_record map
let ez_e_record (lst : (string * expression) list) : expression =
(* TODO: define a correct implementation of List.map
* (an implementation that does not fail with stack overflow) *)
e_record (List.map (fun (s,e) -> (s, make_e_a e)) lst)

View File

@ -0,0 +1,141 @@
(* module Rename = struct
* open Trace
*
* 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
* | I_assignment ({name;annotated_expression = e} as a) -> (
* match List.assoc_opt name r with
* | None ->
* let%bind annotated_expression = rename_annotated_expression (filter r name) e in
* ok (I_assignment {a with annotated_expression})
* | Some (name', lst) -> (
* let%bind annotated_expression = rename_annotated_expression r e in
* match lst with
* | [] -> ok (I_assignment {name = name' ; annotated_expression})
* | lst ->
* let (hds, tl) =
* let open List in
* let r = rev lst in
* rev @@ tl r, hd r
* in
* let%bind tl' = match tl with
* | Access_record n -> ok n
* | Access_tuple _ -> simple_fail "no support for renaming into tuples yet" in
* ok (I_record_patch (name', hds, [tl', annotated_expression]))
* )
* )
* | I_skip -> ok I_skip
* | I_fail e ->
* let%bind e' = rename_annotated_expression r e in
* ok (I_fail e')
* | I_loop (cond, body) ->
* let%bind cond' = rename_annotated_expression r cond in
* let%bind body' = rename_block r body in
* ok (I_loop (cond', body'))
* | I_matching (ae, m) ->
* let%bind ae' = rename_annotated_expression r ae in
* let%bind m' = rename_matching rename_block r m in
* ok (I_matching (ae', m'))
* | I_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 (I_record_patch (v, path, lst'))
* )
* | Some (v', path') -> (
* ok (I_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 : type a . (renamings -> a -> a result) -> renamings -> a matching -> a matching result =
* fun f r m ->
* match m with
* | Match_bool { match_true = mt ; match_false = mf } ->
* let%bind match_true = f r mt in
* let%bind match_false = f r mf in
* ok (Match_bool {match_true ; match_false})
* | Match_option { match_none = mn ; match_some = (some, ms) } ->
* let%bind match_none = f r mn in
* let%bind ms' = f (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 = f r mn in
* let%bind mc' = f (filters r [hd;tl]) mc in
* ok (Match_list {match_nil ; match_cons = (hd, tl, mc')})
* | Match_tuple (lst, body) ->
* let%bind body' = f (filters r lst) body in
* ok (Match_tuple (lst, body'))
*
* and rename_matching_instruction = fun x -> rename_matching rename_block x
*
* and rename_matching_expr = fun x -> rename_matching rename_expression x
*
* 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 : renamings -> expression -> expression result = fun r e ->
* match e with
* | E_literal _ as l -> ok l
* | E_constant (name, lst) ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_constant (name, lst'))
* | E_constructor (name, ae) ->
* let%bind ae' = rename_annotated_expression r ae in
* ok (E_constructor (name, ae'))
* | E_variable v -> (
* match List.assoc_opt v r with
* | None -> ok (E_variable v)
* | Some (name, path) -> ok (E_accessor (ae (E_variable (name)), path))
* )
* | E_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 (E_lambda {l with body ; result})
* | E_application (f, arg) ->
* let%bind f' = rename_annotated_expression r f in
* let%bind arg' = rename_annotated_expression r arg in
* ok (E_application (f', arg'))
* | E_tuple lst ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_tuple lst')
* | E_accessor (ae, p) ->
* let%bind ae' = rename_annotated_expression r ae in
* ok (E_accessor (ae', p))
* | E_record sm ->
* let%bind sm' = bind_smap
* @@ SMap.map (rename_annotated_expression r) sm in
* ok (E_record sm')
* | E_map m ->
* let%bind m' = bind_map_list
* (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
* ok (E_map m')
* | E_list lst ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_list lst')
* | E_look_up m ->
* let%bind m' = bind_map_pair (rename_annotated_expression r) m in
* ok (E_look_up m')
* | E_matching (ae, m) ->
* let%bind ae' = rename_annotated_expression r ae in
* let%bind m' = rename_matching rename_annotated_expression r m in
* ok (E_matching (ae', m'))
* end
* end *)

View File

@ -0,0 +1,113 @@
type name = string
type type_name = string
type 'a name_map = 'a Map.String.t
type 'a type_name_map = 'a Map.String.t
type program = declaration Location.wrap list
and declaration =
| Declaration_type of named_type_expression
| Declaration_constant of named_expression
(* | Macro_declaration of macro_declaration *)
and annotated_expression = {
expression: expression ;
type_annotation: te option ;
}
and named_expression = {
name: name ;
annotated_expression: ae ;
}
and named_type_expression = {
type_name: type_name ;
type_expression: type_expression ;
}
and te = type_expression
and ae = annotated_expression
and te_map = type_expression type_name_map
and ae_map = annotated_expression name_map
and type_expression =
| T_tuple of te list
| T_sum of te_map
| T_record of te_map
| T_function of te * te
| T_variable of type_name
| T_constant of type_name * te list
and lambda = {
binder: name ;
input_type: type_expression ;
output_type: type_expression ;
result: ae ;
body: block ;
}
and expression =
(* Base *)
| E_literal of literal
| E_constant of (name * ae list) (* For language constants, like (Cons hd tl) or (plus i j) *)
| E_variable of name
| E_lambda of lambda
| E_application of (ae * ae)
(* E_Tuple *)
| E_tuple of ae list
(* Sum *)
| E_constructor of (name * ae) (* For user defined constructors *)
(* E_record *)
| E_record of ae_map
| E_accessor of (ae * access_path)
(* Data Structures *)
| E_map of (ae * ae) list
| E_list of ae list
| E_look_up of (ae * ae)
(* Matching *)
| E_matching of (ae * matching_expr)
and access =
| Access_tuple of int
| Access_record of string
and access_path = access list
and literal =
| Literal_unit
| Literal_bool of bool
| Literal_int of int
| Literal_nat of int
| Literal_string of string
| Literal_bytes of bytes
and block = instruction list
and b = block
and instruction =
| I_assignment of named_expression
| I_matching of ae * matching_instr
| I_loop of ae * b
| I_skip
| I_fail of ae
| I_record_patch of name * access_path * (string * ae) list
and 'a matching =
| Match_bool of {
match_true : 'a ;
match_false : 'a ;
}
| Match_list of {
match_nil : 'a ;
match_cons : name * name * 'a ;
}
| Match_option of {
match_none : 'a ;
match_some : name * 'a ;
}
| Match_tuple of name list * 'a
and matching_instr = b matching
and matching_expr = annotated_expression matching

View File

@ -1,6 +1,10 @@
open Trace
open Ast_simplified
module Raw = Ligo_parser.AST
module SMap = Map.String
open Combinators
let nseq_to_list (hd, tl) = hd :: tl
let npseq_to_list (hd, tl) = hd :: (List.map snd tl)
@ -73,11 +77,11 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
ok @@ T_tuple lst
let rec simpl_expression (t:Raw.expr) : ae result =
let return x = ok @@ ae x in
let return x = ok @@ make_e_a x in
let simpl_projection = fun (p:Raw.projection) ->
let var =
let name = p.struct_name.value in
ae @@ E_variable name in
make_e_a @@ E_variable name in
let path = p.field_path in
let path' =
let aux (s:Raw.selection) =
@ -86,13 +90,13 @@ let rec simpl_expression (t:Raw.expr) : ae result =
| Component index -> Access_tuple (Z.to_int (snd index.value))
in
List.map aux @@ npseq_to_list path in
ok @@ ae @@ E_accessor (var, path')
ok @@ make_e_a @@ E_accessor (var, path')
in
match t with
| EVar c ->
if c.value = "unit"
then ok @@ ae @@ E_literal Literal_unit
else ok @@ ae @@ E_variable c.value
then ok @@ make_e_a @@ E_literal Literal_unit
else ok @@ make_e_a @@ E_variable c.value
| ECall x -> (
let (name, args) = x.value in
let f = name.value in
@ -100,17 +104,17 @@ let rec simpl_expression (t:Raw.expr) : ae result =
match List.assoc_opt f constants with
| None ->
let%bind arg = simpl_tuple_expression args' in
ok @@ ae @@ E_application (ae @@ E_variable f, arg)
ok @@ make_e_a @@ E_application (make_e_a @@ E_variable f, arg)
| Some arity ->
let%bind _arity =
trace (simple_error "wrong arity for constants") @@
Assert.assert_equal_int arity (List.length args') in
let%bind lst = bind_map_list simpl_expression args' in
ok @@ ae @@ E_constant (f, lst)
ok @@ make_e_a @@ E_constant (f, lst)
)
| EPar x -> simpl_expression x.value.inside
| EUnit _ -> ok @@ ae @@ E_literal Literal_unit
| EBytes x -> ok @@ ae @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value))
| EUnit _ -> ok @@ make_e_a @@ E_literal Literal_unit
| EBytes x -> ok @@ make_e_a @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value))
| ETuple tpl ->
let (Raw.TupleInj tpl') = tpl in
simpl_tuple_expression
@ -121,7 +125,7 @@ let rec simpl_expression (t:Raw.expr) : ae result =
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
@@ npseq_to_list r.value.fields in
let aux prev (k, v) = SMap.add k v prev in
ok @@ ae @@ E_record (List.fold_left aux SMap.empty fields)
ok @@ make_e_a @@ E_record (List.fold_left aux SMap.empty fields)
| EProj p' -> (
let p = p'.value in
simpl_projection p
@ -131,17 +135,17 @@ let rec simpl_expression (t:Raw.expr) : ae result =
let%bind arg =
simpl_tuple_expression
@@ npseq_to_list args.value.inside in
ok @@ ae @@ E_constructor (c.value, arg)
ok @@ make_e_a @@ E_constructor (c.value, arg)
| EConstr (SomeApp a) ->
let (_, args) = a.value in
let%bind arg =
simpl_tuple_expression
@@ npseq_to_list args.value.inside in
ok @@ ae @@ E_constant ("SOME", [arg])
ok @@ make_e_a @@ E_constant ("SOME", [arg])
| EConstr (NoneExpr n) ->
let type_expr = n.value.inside.opt_type in
let%bind type_expr' = simpl_type_expression type_expr in
ok @@ annotated_expression (E_constant ("NONE", [])) (Some (Combinators.t_option type_expr'))
ok @@ make_e_a_full (E_constant ("NONE", [])) (Combinators.t_option type_expr')
| EArith (Add c) ->
simpl_binop "ADD" c.value
| EArith (Sub c) ->
@ -150,13 +154,13 @@ let rec simpl_expression (t:Raw.expr) : ae result =
simpl_binop "TIMES" c.value
| EArith (Int n) ->
let n = Z.to_int @@ snd @@ n.value in
ok @@ ae @@ E_literal (Literal_int n)
ok @@ make_e_a @@ E_literal (Literal_int n)
| EArith (Nat n) ->
let n = Z.to_int @@ snd @@ n.value in
ok @@ ae @@ E_literal (Literal_nat n)
ok @@ make_e_a @@ E_literal (Literal_nat n)
| EArith _ -> simple_fail "arith: not supported yet"
| EString (String s) ->
ok @@ ae @@ E_literal (Literal_string s.value)
ok @@ make_e_a @@ E_literal (Literal_string s.value)
| EString _ -> simple_fail "string: not supported yet"
| ELogic l -> simpl_logic_expression l
| EList l -> simpl_list_expression l
@ -172,11 +176,11 @@ let rec simpl_expression (t:Raw.expr) : ae result =
@@ List.map get_value
@@ npseq_to_list c.value.cases.value in
let%bind cases = simpl_cases lst in
ok @@ ae @@ E_matching (e, cases)
ok @@ make_e_a @@ E_matching (e, cases)
| EMap (MapInj mi) ->
let%bind lst =
let lst = List.map get_value @@ pseq_to_list mi.value.elements in
let aux : Raw.binding -> (ae * ae) result = fun b ->
let aux : Raw.binding -> (annotated_expression * annotated_expression) result = fun b ->
let%bind src = simpl_expression b.source in
let%bind dst = simpl_expression b.image in
ok (src, dst) in
@ -190,12 +194,12 @@ let rec simpl_expression (t:Raw.expr) : ae result =
let%bind index = simpl_expression lu.value.index.value.inside in
return (E_look_up (path, index))
and simpl_logic_expression (t:Raw.logic_expr) : ae result =
and simpl_logic_expression (t:Raw.logic_expr) : annotated_expression result =
match t with
| BoolExpr (False _) ->
ok @@ ae @@ E_literal (Literal_bool false)
ok @@ make_e_a @@ E_literal (Literal_bool false)
| BoolExpr (True _) ->
ok @@ ae @@ E_literal (Literal_bool true)
ok @@ make_e_a @@ E_literal (Literal_bool true)
| BoolExpr (Or b) ->
simpl_binop "OR" b.value
| BoolExpr (And b) ->
@ -215,7 +219,7 @@ and simpl_logic_expression (t:Raw.logic_expr) : ae result =
| CompExpr (Neq c) ->
simpl_binop "NEQ" c.value
and simpl_list_expression (t:Raw.list_expr) : ae result =
and simpl_list_expression (t:Raw.list_expr) : annotated_expression result =
match t with
| Cons c ->
simpl_binop "CONS" c.value
@ -223,29 +227,29 @@ and simpl_list_expression (t:Raw.list_expr) : ae result =
let%bind lst' =
bind_map_list simpl_expression @@
pseq_to_list lst.value.elements in
ok (ae (E_list lst'))
ok (make_e_a (E_list lst'))
| Nil n ->
let n' = n.value.inside in
let%bind t' = simpl_type_expression n'.list_type in
let e' = E_list [] in
ok (annotated_expression e' (Some (Combinators.t_list t')))
ok (make_e_a_full e' (t_list t'))
and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result =
and simpl_binop (name:string) (t:_ Raw.bin_op) : annotated_expression result =
let%bind a = simpl_expression t.arg1 in
let%bind b = simpl_expression t.arg2 in
ok @@ ae @@ E_constant (name, [a;b])
ok @@ make_e_a @@ E_constant (name, [a;b])
and simpl_unop (name:string) (t:_ Raw.un_op) : ae result =
and simpl_unop (name:string) (t:_ Raw.un_op) : annotated_expression result =
let%bind a = simpl_expression t.arg in
ok @@ ae @@ E_constant (name, [a])
ok @@ make_e_a @@ E_constant (name, [a])
and simpl_tuple_expression (lst:Raw.expr list) : ae result =
and simpl_tuple_expression (lst:Raw.expr list) : annotated_expression result =
match lst with
| [] -> ok @@ ae @@ E_literal Literal_unit
| [] -> ok @@ make_e_a @@ E_literal Literal_unit
| [hd] -> simpl_expression hd
| lst ->
let%bind lst = bind_list @@ List.map simpl_expression lst in
ok @@ ae @@ E_tuple lst
ok @@ make_e_a @@ E_tuple lst
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
match t with
@ -430,8 +434,8 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| Name name -> ok name
| _ -> simple_fail "no complex map assignments yet" in
let%bind key_expr = simpl_expression v'.index.value.inside in
let old_expr = ae @@ E_variable name.value in
let expr' = ae @@ E_constant ("MAP_UPDATE", [key_expr ; value_expr ; old_expr]) in
let old_expr = make_e_a @@ E_variable name.value in
let expr' = make_e_a @@ E_constant ("MAP_UPDATE", [key_expr ; value_expr ; old_expr]) in
ok @@ I_assignment {name = name.value ; annotated_expression = expr'}
)
)
@ -471,8 +475,8 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| Name v -> ok v.value
| _ -> simple_fail "no complex map remove yet" in
let%bind key' = simpl_expression key in
let expr = E_constant ("MAP_REMOVE", [key' ; ae (E_variable map)]) in
ok @@ I_assignment {name = map ; annotated_expression = ae expr}
let expr = E_constant ("MAP_REMOVE", [key' ; make_e_a (E_variable map)]) in
ok @@ I_assignment {name = map ; annotated_expression = make_e_a expr}
| SetRemove _ -> simple_fail "no set remove yet"
and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->

View File

@ -2,6 +2,7 @@ open Trace
open Function
module I = Multifix.Ast
module O = Ast_simplified
open O.Combinators
let unwrap : type a . a Location.wrap -> a = Location.unwrap
@ -81,10 +82,10 @@ and expression_record : _ -> O.annotated_expression result = fun r ->
let open Map.String in
List.fold_left (fun prec (k , v) -> add k v prec) empty lst
in
ok @@ O.(ae @@ E_record e_map)
ok @@ O.(make_e_a @@ E_record e_map)
and expression_main : I.expression_main -> O.annotated_expression result = fun em ->
let return x = ok O.(ae x) in
let return x = ok @@ make_e_a x in
let simple_binop name ab =
let%bind (a' , b') = bind_map_pair (bind_map_location expression_main) ab in
return @@ E_constant (name, [unwrap a' ; unwrap b']) in
@ -102,7 +103,7 @@ and expression_main : I.expression_main -> O.annotated_expression result = fun e
| None -> ok (unwrap e').expression
| Some _ -> simple_fail "can't double annotate" in
let%bind te' = bind_map_location restricted_type_expression te in
ok @@ O.annotated_expression e'' (Some (unwrap te'))
ok @@ make_e_a_full e'' (unwrap te')
| Eh_lt ab ->
simple_binop "LT" ab
| Eh_gt ab ->
@ -173,7 +174,7 @@ let let_content : I.let_content -> _ result = fun (Let_content (n, args, ty_opt,
let%bind ty' =
let (I.Type_annotation_ ty') = unwrap ty in
bind_map_location type_expression ty' in
let ae = O.annotated_expression e'' (Some (unwrap ty')) in
let ae = make_e_a_full e'' (unwrap ty') in
ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = ae}
let statement : I.statement -> O.declaration result = fun s ->

View File

@ -8,7 +8,7 @@ module Simplified = Ligo.AST_Simplified
let int () : unit result =
let open Combinators in
let pre = ae @@ e_int 32 in
let pre = make_e_a @@ e_int 32 in
let open Typer in
let e = Environment.full_empty in
let%bind post = type_annotated_expression e pre in
@ -21,9 +21,9 @@ module TestExpressions = struct
let test_expression ?(env = Typer.Environment.full_empty)
(expr : expression)
(test_expected_ty : Typed.tv) =
let pre = Combinators.make_e_a @@ expr in
let open Typer in
let open! Typed in
let pre = ae @@ expr in
let%bind post = type_annotated_expression env pre in
let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
ok ()
@ -53,7 +53,7 @@ module TestExpressions = struct
O.[("foo", t_int ()); ("bar", t_string ())]
in test_expression
~env:(E.env_sum_type variant_foo_bar)
I.(e_constructor "foo" (ae @@ e_int 32))
I.(e_constructor "foo" (make_e_a @@ e_int 32))
O.(make_t_ez_sum variant_foo_bar)
let record () : unit result =

View File

@ -444,8 +444,8 @@ let untype_literal (l:O.literal) : I.literal result =
let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
let open I in
let annotation = e.type_annotation.simplified in
let return e = ok @@ annotated_expression e annotation in
let type_annotation = e.type_annotation.simplified in
let return e = ok @@ I.Combinators.make_e_a ?type_annotation e in
match e.expression with
| E_literal l ->
let%bind l = untype_literal l in