rename ast-simplified

This commit is contained in:
Galfour 2019-04-01 09:03:38 +00:00
parent f8dcca8a12
commit 2de68d4a00
3 changed files with 232 additions and 239 deletions

View File

@ -9,8 +9,8 @@ type 'a type_name_map = 'a SMap.t
type program = declaration list type program = declaration list
and declaration = and declaration =
| Type_declaration of named_type_expression | Declaration_type of named_type_expression
| Constant_declaration of named_expression | Declaration_constant of named_expression
(* | Macro_declaration of macro_declaration *) (* | Macro_declaration of macro_declaration *)
and annotated_expression = { and annotated_expression = {
@ -34,12 +34,12 @@ and te_map = type_expression type_name_map
and ae_map = annotated_expression name_map and ae_map = annotated_expression name_map
and type_expression = and type_expression =
| Type_tuple of te list | T_tuple of te list
| Type_sum of te_map | T_sum of te_map
| Type_record of te_map | T_record of te_map
| Type_function of te * te | T_function of te * te
| Type_variable of type_name | T_variable of type_name
| Type_constant of type_name * te list | T_constant of type_name * te list
and lambda = { and lambda = {
binder: name ; binder: name ;
@ -51,47 +51,47 @@ and lambda = {
and expression = and expression =
(* Base *) (* Base *)
| Literal of literal | E_literal of literal
| Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *) | E_constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
| Variable of name | E_variable of name
| Lambda of lambda | E_lambda of lambda
| Application of ae * ae | E_application of ae * ae
(* Tuple *) (* E_Tuple *)
| Tuple of ae list | E_tuple of ae list
(* Sum *) (* Sum *)
| Constructor of name * ae (* For user defined constructors *) | E_constructor of name * ae (* For user defined constructors *)
(* Record *) (* E_record *)
| Record of ae_map | E_record of ae_map
| Accessor of ae * access_path | E_accessor of ae * access_path
(* Data Structures *) (* Data Structures *)
| Map of (ae * ae) list | E_map of (ae * ae) list
| LookUp of (ae * ae) | E_look_up of (ae * ae)
(* Matching *) (* Matching *)
| Matching_expr of (ae * matching_expr) | E_matching of (ae * matching_expr)
and access = and access =
| Tuple_access of int | Access_tuple of int
| Record_access of string | Access_record of string
and access_path = access list and access_path = access list
and literal = and literal =
| Unit | Literal_unit
| Bool of bool | Literal_bool of bool
| Number of int | Literal_number of int
| String of string | Literal_string of string
| Bytes of bytes | Literal_bytes of bytes
and block = instruction list and block = instruction list
and b = block and b = block
and instruction = and instruction =
| Assignment of named_expression | I_assignment of named_expression
| Matching_instr of ae * matching_instr | I_matching of ae * matching_instr
| Loop of ae * b | I_loop of ae * b
| Skip | I_skip
| Fail of ae | I_fail of ae
| Record_patch of name * access_path * (string * ae) list | I_record_patch of name * access_path * (string * ae) list
and 'a matching = and 'a matching =
| Match_bool of { | Match_bool of {
@ -123,36 +123,36 @@ module PP = struct
open Format open Format
let rec type_expression ppf (te:type_expression) = match te with let rec type_expression ppf (te:type_expression) = match te with
| Type_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_expression) lst | T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_expression) lst
| Type_sum m -> fprintf ppf "sum[%a]" (smap_sep type_expression) m | T_sum m -> fprintf ppf "sum[%a]" (smap_sep type_expression) m
| Type_record m -> fprintf ppf "record[%a]" (smap_sep type_expression) m | T_record m -> fprintf ppf "record[%a]" (smap_sep type_expression) m
| Type_function (p, r) -> fprintf ppf "%a -> %a" type_expression p type_expression r | T_function (p, r) -> fprintf ppf "%a -> %a" type_expression p type_expression r
| Type_variable name -> fprintf ppf "%s" name | T_variable name -> fprintf ppf "%s" name
| Type_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep type_expression) lst | T_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep type_expression) lst
let literal ppf (l:literal) = match l with let literal ppf (l:literal) = match l with
| Unit -> fprintf ppf "Unit" | Literal_unit -> fprintf ppf "Unit"
| Bool b -> fprintf ppf "%b" b | Literal_bool b -> fprintf ppf "%b" b
| Number n -> fprintf ppf "%d" n | Literal_number n -> fprintf ppf "%d" n
| String s -> fprintf ppf "%S" s | Literal_string s -> fprintf ppf "%S" s
| Bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
let rec expression ppf (e:expression) = match e with let rec expression ppf (e:expression) = match e with
| Literal l -> literal ppf l | E_literal l -> literal ppf l
| Variable name -> fprintf ppf "%s" name | E_variable name -> fprintf ppf "%s" name
| Application (f, arg) -> fprintf ppf "(%a)@(%a)" annotated_expression f annotated_expression arg | E_application (f, arg) -> fprintf ppf "(%a)@(%a)" annotated_expression f annotated_expression arg
| Constructor (name, ae) -> fprintf ppf "%s(%a)" name annotated_expression ae | E_constructor (name, ae) -> fprintf ppf "%s(%a)" name annotated_expression ae
| Constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep annotated_expression) lst | E_constant (name, lst) -> fprintf ppf "%s(%a)" name (list_sep annotated_expression) lst
| Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst | E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
| Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p | E_accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m | E_record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m | E_map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
| LookUp (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
| Lambda {binder;input_type;output_type;result;body} -> | E_lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {%a} return %a" fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
binder type_expression input_type type_expression output_type binder type_expression input_type type_expression output_type
block body annotated_expression result block body annotated_expression result
| Matching_expr (ae, m) -> | E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) 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) -> and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
@ -160,8 +160,8 @@ module PP = struct
and access ppf (a:access) = and access ppf (a:access) =
match a with match a with
| Tuple_access n -> fprintf ppf "%d" n | Access_tuple n -> fprintf ppf "%d" n
| Record_access s -> fprintf ppf "%s" s | Access_record s -> fprintf ppf "%s" s
and access_path ppf (p:access_path) = and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep ~pp_sep:(const ".") access) p fprintf ppf "%a" (list_sep ~pp_sep:(const ".") access) p
@ -191,19 +191,19 @@ module PP = struct
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some
and instruction ppf (i:instruction) = match i with and instruction ppf (i:instruction) = match i with
| Skip -> fprintf ppf "skip" | I_skip -> fprintf ppf "skip"
| Fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae | I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| Record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep single_record_patch) lst | I_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 | I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| Assignment {name;annotated_expression = ae} -> | I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae fprintf ppf "%s := %a" name annotated_expression ae
| Matching_instr (ae, m) -> | I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
let declaration ppf (d:declaration) = match d with let declaration ppf (d:declaration) = match d with
| Type_declaration {type_name ; type_expression = te} -> | Declaration_type {type_name ; type_expression = te} ->
fprintf ppf "type %s = %a" type_name type_expression te fprintf ppf "type %s = %a" type_name type_expression te
| Constant_declaration {name ; annotated_expression = ae} -> | Declaration_constant {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae fprintf ppf "const %s = %a" name annotated_expression ae
let program ppf (p:program) = let program ppf (p:program) =
@ -225,32 +225,32 @@ module Rename = struct
let rec rename_instruction (r:renamings) (i:instruction) : instruction result = let rec rename_instruction (r:renamings) (i:instruction) : instruction result =
match i with match i with
| Assignment ({name;annotated_expression = e} as a) -> | I_assignment ({name;annotated_expression = e} as a) ->
let%bind annotated_expression = rename_annotated_expression (filter r name) e in let%bind annotated_expression = rename_annotated_expression (filter r name) e in
ok (Assignment {a with annotated_expression}) ok (I_assignment {a with annotated_expression})
| Skip -> ok Skip | I_skip -> ok I_skip
| Fail e -> | I_fail e ->
let%bind e' = rename_annotated_expression r e in let%bind e' = rename_annotated_expression r e in
ok (Fail e') ok (I_fail e')
| Loop (cond, body) -> | I_loop (cond, body) ->
let%bind cond' = rename_annotated_expression r cond in let%bind cond' = rename_annotated_expression r cond in
let%bind body' = rename_block r body in let%bind body' = rename_block r body in
ok (Loop (cond', body')) ok (I_loop (cond', body'))
| Matching_instr (ae, m) -> | I_matching (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching rename_block r m in let%bind m' = rename_matching rename_block r m in
ok (Matching_instr (ae', m')) ok (I_matching (ae', m'))
| Record_patch (v, path, lst) -> | I_record_patch (v, path, lst) ->
let aux (x, y) = let aux (x, y) =
let%bind y' = rename_annotated_expression (filter r v) y in let%bind y' = rename_annotated_expression (filter r v) y in
ok (x, y') in ok (x, y') in
let%bind lst' = bind_map_list aux lst in let%bind lst' = bind_map_list aux lst in
match List.assoc_opt v r with match List.assoc_opt v r with
| None -> ( | None -> (
ok (Record_patch (v, path, lst')) ok (I_record_patch (v, path, lst'))
) )
| Some (v, path') -> ( | Some (v, path') -> (
ok (Record_patch (v, path' @ path, lst')) ok (I_record_patch (v, path' @ path, lst'))
) )
and rename_block (r:renamings) (bl:block) : block result = and rename_block (r:renamings) (bl:block) : block result =
bind_map_list (rename_instruction r) bl bind_map_list (rename_instruction r) bl
@ -284,96 +284,89 @@ module Rename = struct
and rename_expression : renamings -> expression -> expression result = fun r e -> and rename_expression : renamings -> expression -> expression result = fun r e ->
match e with match e with
| Literal _ as l -> ok l | E_literal _ as l -> ok l
| Constant (name, lst) -> | E_constant (name, lst) ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (Constant (name, lst')) ok (E_constant (name, lst'))
| Constructor (name, ae) -> | E_constructor (name, ae) ->
let%bind ae' = rename_annotated_expression r ae in let%bind ae' = rename_annotated_expression r ae in
ok (Constructor (name, ae')) ok (E_constructor (name, ae'))
| Variable v -> ( | E_variable v -> (
match List.assoc_opt v r with match List.assoc_opt v r with
| None -> ok (Variable v) | None -> ok (E_variable v)
| Some (name, path) -> ok (Accessor (ae (Variable (name)), path)) | Some (name, path) -> ok (E_accessor (ae (E_variable (name)), path))
) )
| Lambda ({binder;body;result} as l) -> | E_lambda ({binder;body;result} as l) ->
let r' = filter r binder in let r' = filter r binder in
let%bind body = rename_block r' body in let%bind body = rename_block r' body in
let%bind result = rename_annotated_expression r' result in let%bind result = rename_annotated_expression r' result in
ok (Lambda {l with body ; result}) ok (E_lambda {l with body ; result})
| Application (f, arg) -> | E_application (f, arg) ->
let%bind f' = rename_annotated_expression r f in let%bind f' = rename_annotated_expression r f in
let%bind arg' = rename_annotated_expression r arg in let%bind arg' = rename_annotated_expression r arg in
ok (Application (f', arg')) ok (E_application (f', arg'))
| Tuple lst -> | E_tuple lst ->
let%bind lst' = bind_map_list (rename_annotated_expression r) lst in let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
ok (Tuple lst') ok (E_tuple lst')
| Accessor (ae, p) -> | E_accessor (ae, p) ->
let%bind ae' = rename_annotated_expression r ae in let%bind ae' = rename_annotated_expression r ae in
ok (Accessor (ae', p)) ok (E_accessor (ae', p))
(* let aux prev hd = | E_record sm ->
* 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 let%bind sm' = bind_smap
@@ SMap.map (rename_annotated_expression r) sm in @@ SMap.map (rename_annotated_expression r) sm in
ok (Record sm') ok (E_record sm')
| Map m -> | E_map m ->
let%bind m' = bind_map_list let%bind m' = bind_map_list
(fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
ok (Map m') ok (E_map m')
| LookUp m -> | E_look_up m ->
let%bind m' = bind_map_pair (rename_annotated_expression r) m in let%bind m' = bind_map_pair (rename_annotated_expression r) m in
ok (LookUp m') ok (E_look_up m')
| Matching_expr (ae, m) -> | E_matching (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching rename_annotated_expression r m in let%bind m' = rename_matching rename_annotated_expression r m in
ok (Matching_expr (ae', m')) ok (E_matching (ae', m'))
end end
end end
module Combinators = struct module Combinators = struct
let t_bool : type_expression = Type_constant ("bool", []) let t_bool : type_expression = T_constant ("bool", [])
let t_string : type_expression = Type_constant ("string", []) let t_string : type_expression = T_constant ("string", [])
let t_bytes : type_expression = Type_constant ("bytes", []) let t_bytes : type_expression = T_constant ("bytes", [])
let t_int : type_expression = Type_constant ("int", []) let t_int : type_expression = T_constant ("int", [])
let t_unit : type_expression = Type_constant ("unit", []) let t_unit : type_expression = T_constant ("unit", [])
let t_option o : type_expression = Type_constant ("option", [o]) let t_option o : type_expression = T_constant ("option", [o])
let t_tuple lst : type_expression = Type_tuple lst let t_tuple lst : type_expression = T_tuple lst
let t_pair a b = t_tuple [a ; b] let t_pair a b = t_tuple [a ; b]
let t_record m : type_expression = (Type_record m) let t_record m : type_expression = (T_record m)
let t_ez_record (lst:(string * type_expression) list) : type_expression = let t_ez_record (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in let map = List.fold_left aux SMap.empty lst in
Type_record map T_record map
let t_record_ez lst = let t_record_ez lst =
let m = SMap.of_list lst in let m = SMap.of_list lst in
t_record m t_record m
let t_sum m : type_expression = Type_sum m let t_sum m : type_expression = T_sum m
let make_t_ez_sum (lst:(string * type_expression) list) : type_expression = let make_t_ez_sum (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in let map = List.fold_left aux SMap.empty lst in
Type_sum map T_sum map
let t_function param result : type_expression = Type_function (param, result) let t_function param result : type_expression = T_function (param, result)
let annotated_expression ?type_annotation expression = {expression ; type_annotation} let annotated_expression ?type_annotation expression = {expression ; type_annotation}
let name (s : string) : name = s let name (s : string) : name = s
let var (s : string) : expression = Variable s let var (s : string) : expression = E_variable s
let unit () : expression = Literal (Unit) let unit () : expression = E_literal (Literal_unit)
let number n : expression = Literal (Number n) let number n : expression = E_literal (Literal_number n)
let bool b : expression = Literal (Bool b) let bool b : expression = E_literal (Literal_bool b)
let string s : expression = Literal (String s) let string s : expression = E_literal (Literal_string s)
let bytes b : expression = Literal (Bytes (Bytes.of_string b)) let bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b))
let lambda (binder : string) let lambda (binder : string)
(input_type : type_expression) (input_type : type_expression)
@ -381,7 +374,7 @@ module Combinators = struct
(result : expression) (result : expression)
(body : block) (body : block)
: expression = : expression =
Lambda { E_lambda {
binder = (name binder) ; binder = (name binder) ;
input_type = input_type ; input_type = input_type ;
output_type = output_type ; output_type = output_type ;
@ -389,16 +382,16 @@ module Combinators = struct
body ; body ;
} }
let tuple (lst : ae list) : expression = Tuple lst let tuple (lst : ae list) : expression = E_tuple lst
let ez_tuple (lst : expression list) : expression = let ez_tuple (lst : expression list) : expression =
tuple (List.map (fun e -> ae e) lst) tuple (List.map (fun e -> ae e) lst)
let constructor (s : string) (e : ae) : expression = Constructor (name s, e) let constructor (s : string) (e : ae) : expression = E_constructor (name s, e)
let record (lst : (string * ae) list) : expression = let record (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in let map = List.fold_left aux SMap.empty lst in
Record map E_record map
let ez_record (lst : (string * expression) list) : expression = let ez_record (lst : (string * expression) list) : expression =
(* TODO: define a correct implementation of List.map (* TODO: define a correct implementation of List.map

View File

@ -27,11 +27,11 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
| TAlias v -> ( | TAlias v -> (
match List.assoc_opt v.value type_constants with match List.assoc_opt v.value type_constants with
| Some 0 -> | Some 0 ->
ok @@ Type_constant (v.value, []) ok @@ T_constant (v.value, [])
| Some _ -> | Some _ ->
simple_fail "type constructor with wrong number of args" simple_fail "type constructor with wrong number of args"
| None -> | None ->
ok @@ Type_variable v.value ok @@ T_variable v.value
) )
| TApp x -> | TApp x ->
let (name, tuple) = x.value in let (name, tuple) = x.value in
@ -41,7 +41,7 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
| Some _ -> simple_fail "type constructor with wrong number of args" | Some _ -> simple_fail "type constructor with wrong number of args"
| None -> simple_fail "unrecognized type constants" in | None -> simple_fail "unrecognized type constants" in
let%bind lst' = bind_list @@ List.map simpl_type_expression lst in let%bind lst' = bind_list @@ List.map simpl_type_expression lst in
ok @@ Type_constant (name.value, lst') ok @@ T_constant (name.value, lst')
| TProd p -> | TProd p ->
let%bind tpl = simpl_list_type_expression let%bind tpl = simpl_list_type_expression
@@ npseq_to_list p.value in @@ npseq_to_list p.value in
@ -53,7 +53,7 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
@@ List.map (fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type)) @@ List.map (fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type))
@@ npseq_to_list r.value.field_decls in @@ npseq_to_list r.value.field_decls in
let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in
ok @@ Type_record m ok @@ T_record m
| TSum s -> | TSum s ->
let aux (v:Raw.variant Raw.reg) = let aux (v:Raw.variant Raw.reg) =
let%bind te = simpl_list_type_expression let%bind te = simpl_list_type_expression
@ -64,7 +64,7 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
@@ List.map aux @@ List.map aux
@@ npseq_to_list s.value in @@ npseq_to_list s.value in
let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in
ok @@ Type_sum m ok @@ T_sum m
and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result = and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result =
match lst with match lst with
@ -72,7 +72,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
| [hd] -> simpl_type_expression hd | [hd] -> simpl_type_expression hd
| lst -> | lst ->
let%bind lst = bind_list @@ List.map simpl_type_expression lst in let%bind lst = bind_list @@ List.map simpl_type_expression lst in
ok @@ Type_tuple lst ok @@ T_tuple lst
let constants = [ let constants = [
("get_force", 2) ; ("get_force", 2) ;
@ -83,22 +83,22 @@ let rec simpl_expression (t:Raw.expr) : ae result =
let simpl_projection = fun (p:Raw.projection) -> let simpl_projection = fun (p:Raw.projection) ->
let var = let var =
let name = p.record_name.value in let name = p.record_name.value in
ae @@ Variable name in ae @@ E_variable name in
let path = p.field_path in let path = p.field_path in
let path' = let path' =
let aux (s:Raw.selection) = let aux (s:Raw.selection) =
match s with match s with
| FieldName property -> Record_access property.value | FieldName property -> Access_record property.value
| Component index -> Tuple_access (Z.to_int (snd index.value)) | Component index -> Access_tuple (Z.to_int (snd index.value))
in in
List.map aux @@ npseq_to_list path in List.map aux @@ npseq_to_list path in
ok @@ ae @@ Accessor (var, path') ok @@ ae @@ E_accessor (var, path')
in in
match t with match t with
| EVar c -> | EVar c ->
if c.value = "unit" if c.value = "unit"
then ok @@ ae @@ Literal Unit then ok @@ ae @@ E_literal Literal_unit
else ok @@ ae @@ Variable c.value else ok @@ ae @@ E_variable c.value
| ECall x -> ( | ECall x -> (
let (name, args) = x.value in let (name, args) = x.value in
let f = name.value in let f = name.value in
@ -106,17 +106,17 @@ let rec simpl_expression (t:Raw.expr) : ae result =
match List.assoc_opt f constants with match List.assoc_opt f constants with
| None -> | None ->
let%bind arg = simpl_list_expression args' in let%bind arg = simpl_list_expression args' in
ok @@ ae @@ Application (ae @@ Variable f, arg) ok @@ ae @@ E_application (ae @@ E_variable f, arg)
| Some arity -> | Some arity ->
let%bind _arity = let%bind _arity =
trace (simple_error "wrong arity for constants") @@ trace (simple_error "wrong arity for constants") @@
Assert.assert_equal_int arity (List.length args') in Assert.assert_equal_int arity (List.length args') in
let%bind lst = bind_map_list simpl_expression args' in let%bind lst = bind_map_list simpl_expression args' in
ok @@ ae @@ Constant (f, lst) ok @@ ae @@ E_constant (f, lst)
) )
| EPar x -> simpl_expression x.value.inside | EPar x -> simpl_expression x.value.inside
| EUnit _ -> ok @@ ae @@ Literal Unit | EUnit _ -> ok @@ ae @@ E_literal Literal_unit
| EBytes x -> ok @@ ae @@ Literal (Bytes (Bytes.of_string @@ fst x.value)) | EBytes x -> ok @@ ae @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value))
| ETuple tpl -> | ETuple tpl ->
let (Raw.TupleInj tpl') = tpl in let (Raw.TupleInj tpl') = tpl in
simpl_list_expression simpl_list_expression
@ -127,7 +127,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)) @@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
@@ npseq_to_list r.value.fields in @@ npseq_to_list r.value.fields in
let aux prev (k, v) = SMap.add k v prev in let aux prev (k, v) = SMap.add k v prev in
ok @@ ae @@ Record (List.fold_left aux SMap.empty fields) ok @@ ae @@ E_record (List.fold_left aux SMap.empty fields)
| EProj p' -> ( | EProj p' -> (
let p = p'.value in let p = p'.value in
simpl_projection p simpl_projection p
@ -137,25 +137,25 @@ let rec simpl_expression (t:Raw.expr) : ae result =
let%bind arg = let%bind arg =
simpl_list_expression simpl_list_expression
@@ npseq_to_list args.value.inside in @@ npseq_to_list args.value.inside in
ok @@ ae @@ Constructor (c.value, arg) ok @@ ae @@ E_constructor (c.value, arg)
| EConstr (SomeApp a) -> | EConstr (SomeApp a) ->
let (_, args) = a.value in let (_, args) = a.value in
let%bind arg = let%bind arg =
simpl_list_expression simpl_list_expression
@@ npseq_to_list args.value.inside in @@ npseq_to_list args.value.inside in
ok @@ ae @@ Constant ("SOME", [arg]) ok @@ ae @@ E_constant ("SOME", [arg])
| EConstr (NoneExpr n) -> | EConstr (NoneExpr n) ->
let type_expr = n.value.inside.opt_type in let type_expr = n.value.inside.opt_type in
let%bind type_expr' = simpl_type_expression type_expr in let%bind type_expr' = simpl_type_expression type_expr in
ok @@ annotated_expression (Constant ("NONE", [])) (Some (Combinators.t_option type_expr')) ok @@ annotated_expression (E_constant ("NONE", [])) (Some (Combinators.t_option type_expr'))
| EArith (Add c) -> | EArith (Add c) ->
simpl_binop "ADD" c.value simpl_binop "ADD" 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 @@ ae @@ Literal (Number n) ok @@ ae @@ E_literal (Literal_number n)
| EArith _ -> simple_fail "arith: not supported yet" | EArith _ -> simple_fail "arith: not supported yet"
| EString (String s) -> | EString (String s) ->
ok @@ ae @@ Literal (String s.value) ok @@ ae @@ E_literal (Literal_string s.value)
| EString _ -> simple_fail "string: not supported yet" | EString _ -> simple_fail "string: not supported yet"
| ELogic l -> simpl_logic_expression l | ELogic l -> simpl_logic_expression l
| EList _ -> simple_fail "list: not supported yet" | EList _ -> simple_fail "list: not supported yet"
@ -171,7 +171,7 @@ let rec simpl_expression (t:Raw.expr) : ae result =
@@ List.map get_value @@ List.map get_value
@@ npseq_to_list c.value.cases_expr.value in @@ npseq_to_list c.value.cases_expr.value in
let%bind cases = simpl_cases lst in let%bind cases = simpl_cases lst in
ok @@ ae @@ Matching_expr (e, cases) ok @@ ae @@ E_matching (e, cases)
| EMap (MapInj mi) -> | EMap (MapInj mi) ->
let%bind lst = let%bind lst =
let lst = List.map get_value @@ pseq_to_list mi.value.elements in let lst = List.map get_value @@ pseq_to_list mi.value.elements in
@ -180,21 +180,21 @@ let rec simpl_expression (t:Raw.expr) : ae result =
let%bind dst = simpl_expression b.image in let%bind dst = simpl_expression b.image in
ok (src, dst) in ok (src, dst) in
bind_map_list aux lst in bind_map_list aux lst in
return (Map lst) return (E_map lst)
| EMap (MapLookUp lu) -> | EMap (MapLookUp lu) ->
let%bind path = match lu.value.path with let%bind path = match lu.value.path with
| Name v -> return (Variable v.value) | Name v -> return (E_variable v.value)
| Path p -> simpl_projection p.value | Path p -> simpl_projection p.value
in in
let%bind index = simpl_expression lu.value.index.value.inside in let%bind index = simpl_expression lu.value.index.value.inside in
return (LookUp (path, index)) return (E_look_up (path, index))
and simpl_logic_expression (t:Raw.logic_expr) : ae result = and simpl_logic_expression (t:Raw.logic_expr) : ae result =
match t with match t with
| BoolExpr (False _) -> | BoolExpr (False _) ->
ok @@ ae @@ Literal (Bool false) ok @@ ae @@ E_literal (Literal_bool false)
| BoolExpr (True _) -> | BoolExpr (True _) ->
ok @@ ae @@ Literal (Bool true) ok @@ ae @@ E_literal (Literal_bool true)
| BoolExpr (Or b) -> | BoolExpr (Or b) ->
simpl_binop "OR" b.value simpl_binop "OR" b.value
| BoolExpr (And b) -> | BoolExpr (And b) ->
@ -217,19 +217,19 @@ and simpl_logic_expression (t:Raw.logic_expr) : ae result =
and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result = and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result =
let%bind a = simpl_expression t.arg1 in let%bind a = simpl_expression t.arg1 in
let%bind b = simpl_expression t.arg2 in let%bind b = simpl_expression t.arg2 in
ok @@ ae @@ Constant (name, [a;b]) ok @@ ae @@ 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) : ae result =
let%bind a = simpl_expression t.arg in let%bind a = simpl_expression t.arg in
ok @@ ae @@ Constant (name, [a]) ok @@ ae @@ E_constant (name, [a])
and simpl_list_expression (lst:Raw.expr list) : ae result = and simpl_list_expression (lst:Raw.expr list) : ae result =
match lst with match lst with
| [] -> ok @@ ae @@ Literal Unit | [] -> ok @@ ae @@ E_literal Literal_unit
| [hd] -> simpl_expression hd | [hd] -> simpl_expression hd
| lst -> | lst ->
let%bind lst = bind_list @@ List.map simpl_expression lst in let%bind lst = bind_list @@ List.map simpl_expression lst in
ok @@ ae @@ Tuple lst ok @@ ae @@ E_tuple lst
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result = and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
match t with match t with
@ -237,7 +237,7 @@ and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression
| LocalLam _ -> simple_fail "no local lambdas yet" | LocalLam _ -> simple_fail "no local lambdas yet"
and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result = and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result =
let return x = ok (Assignment x, x) in let return x = ok (I_assignment x, x) in
match t with match t with
| LocalVar x -> | LocalVar x ->
let x = x.value in let x = x.value in
@ -274,13 +274,13 @@ and simpl_declaration : Raw.declaration -> declaration result = fun t ->
| TypeDecl x -> | TypeDecl x ->
let {name;type_expr} : Raw.type_decl = x.value in let {name;type_expr} : Raw.type_decl = x.value in
let%bind type_expression = simpl_type_expression type_expr in let%bind type_expression = simpl_type_expression type_expr in
ok @@ Type_declaration {type_name=name.value;type_expression} ok @@ Declaration_type {type_name=name.value;type_expression}
| ConstDecl x -> | ConstDecl x ->
let {name;const_type;init} = x.value in let {name;const_type;init} = x.value in
let%bind expression = simpl_expression init in let%bind expression = simpl_expression init in
let%bind t = simpl_type_expression const_type in let%bind t = simpl_type_expression const_type in
let type_annotation = Some t in let type_annotation = Some t in
ok @@ Constant_declaration {name=name.value;annotated_expression={expression with type_annotation}} ok @@ Declaration_constant {name=name.value;annotated_expression={expression with type_annotation}}
| LambdaDecl (FunDecl x) -> | LambdaDecl (FunDecl x) ->
let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in
(match npseq_to_list param.value.inside with (match npseq_to_list param.value.inside with
@ -301,16 +301,16 @@ and simpl_declaration : Raw.declaration -> declaration result = fun t ->
let%bind output_type = simpl_type_expression ret_type in let%bind output_type = simpl_type_expression ret_type in
let body = local_declarations @ instructions in let body = local_declarations @ instructions in
let decl = let decl =
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (Type_function (input_type, output_type)) in let type_annotation = Some (T_function (input_type, output_type)) in
Constant_declaration {name;annotated_expression = {expression;type_annotation}} Declaration_constant {name;annotated_expression = {expression;type_annotation}}
in in
ok decl ok decl
) )
| lst -> ( | lst -> (
let%bind params = bind_map_list simpl_param lst in let%bind params = bind_map_list simpl_param lst in
let input = let input =
let type_expression = Type_record ( let type_expression = T_record (
SMap.of_list SMap.of_list
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression) @@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
params params
@ -329,7 +329,7 @@ and simpl_declaration : Raw.declaration -> declaration result = fun t ->
let%bind (body, result) = let%bind (body, result) =
let renamings = let renamings =
let aux ({type_name}:named_type_expression) : Rename.Value.renaming = let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
type_name, ("arguments", [Record_access type_name]) type_name, ("arguments", [Access_record type_name])
in in
List.map aux params List.map aux params
in in
@ -343,9 +343,9 @@ and simpl_declaration : Raw.declaration -> declaration result = fun t ->
in in
ok (b, r) in ok (b, r) in
let decl = let decl =
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (Type_function (input_type, output_type)) in let type_annotation = Some (T_function (input_type, output_type)) in
Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}} Declaration_constant {name = name.value;annotated_expression = {expression;type_annotation}}
in in
ok decl ok decl
) )
@ -363,13 +363,13 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| ProcCall _ -> simple_fail "no proc call" | ProcCall _ -> simple_fail "no proc call"
| Fail e -> | Fail e ->
let%bind expr = simpl_expression e.value.fail_expr in let%bind expr = simpl_expression e.value.fail_expr in
ok @@ Fail expr ok @@ I_fail expr
| Skip _ -> ok @@ Skip | Skip _ -> ok @@ I_skip
| Loop (While l) -> | Loop (While l) ->
let l = l.value in let l = l.value in
let%bind cond = simpl_expression l.cond in let%bind cond = simpl_expression l.cond in
let%bind body = simpl_block l.block.value in let%bind body = simpl_block l.block.value in
ok @@ Loop (cond, body) ok @@ I_loop (cond, body)
| Loop (For _) -> | Loop (For _) ->
simple_fail "no for yet" simple_fail "no for yet"
| Cond c -> | Cond c ->
@ -381,7 +381,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
let%bind match_false = match c.ifnot with let%bind match_false = match c.ifnot with
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in | ClauseBlock b -> simpl_statements @@ fst b.value.inside in
ok @@ Matching_instr (expr, (Match_bool {match_true; match_false})) ok @@ I_matching (expr, (Match_bool {match_true; match_false}))
| Assign a -> | Assign a ->
let a = a.value in let a = a.value in
let%bind name = match a.lhs with let%bind name = match a.lhs with
@ -392,7 +392,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| Expr e -> simpl_expression e | Expr e -> simpl_expression e
| _ -> simple_fail "no weird assignments yet" | _ -> simple_fail "no weird assignments yet"
in in
ok @@ Assignment {name ; annotated_expression} ok @@ I_assignment {name ; annotated_expression}
| Case_instr c -> | Case_instr c ->
let c = c.value in let c = c.value in
let%bind expr = simpl_expression c.expr in let%bind expr = simpl_expression c.expr in
@ -404,7 +404,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
@@ List.map aux @@ List.map aux
@@ npseq_to_list c.cases_instr.value in @@ npseq_to_list c.cases_instr.value in
let%bind m = simpl_cases cases in let%bind m = simpl_cases cases in
ok @@ Matching_instr (expr, m) ok @@ I_matching (expr, m)
| RecordPatch r -> | RecordPatch r ->
let r = r.value in let r = r.value in
let%bind record = match r.path with let%bind record = match r.path with
@ -415,7 +415,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
@@ 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.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) @@ List.map (fun (x:_ Raw.reg) -> x.value)
@@ npseq_to_list r.record_inj.value.fields in @@ npseq_to_list r.record_inj.value.fields in
ok @@ Record_patch (record, [], inj) ok @@ I_record_patch (record, [], inj)
| MapPatch _ -> simple_fail "no map patch yet" | MapPatch _ -> simple_fail "no map patch yet"
| SetPatch _ -> simple_fail "no set patch yet" | SetPatch _ -> simple_fail "no set patch yet"
| MapRemove _ -> simple_fail "no map remove yet" | MapRemove _ -> simple_fail "no map remove yet"

View File

@ -108,11 +108,11 @@ let rec type_program (p:I.program) : O.program result =
ok @@ List.rev lst ok @@ List.rev lst
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
| Type_declaration {type_name;type_expression} -> | Declaration_type {type_name;type_expression} ->
let%bind tv = evaluate_type env type_expression in let%bind tv = evaluate_type env type_expression in
let env' = Environment.add_type env type_name tv in let env' = Environment.add_type env type_name tv in
ok (env', None) ok (env', None)
| Constant_declaration {name;annotated_expression} -> | Declaration_constant {name;annotated_expression} ->
let%bind ae' = let%bind ae' =
trace (constant_declaration_error name annotated_expression) @@ trace (constant_declaration_error name annotated_expression) @@
type_annotated_expression env annotated_expression in type_annotated_expression env annotated_expression in
@ -132,17 +132,17 @@ and type_block (e:environment) (b:I.block) : O.block result =
ok block ok block
and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function
| Skip -> ok (e, O.Skip) | I_skip -> ok (e, O.Skip)
| Fail x -> | I_fail x ->
let%bind expression = type_annotated_expression e x in let%bind expression = type_annotated_expression e x in
ok (e, O.Fail expression) ok (e, O.Fail expression)
| Loop (cond, body) -> | I_loop (cond, body) ->
let%bind cond = type_annotated_expression e cond in let%bind cond = type_annotated_expression e cond in
let%bind _ = let%bind _ =
O.assert_type_value_eq (cond.type_annotation, make_t_bool) in O.assert_type_value_eq (cond.type_annotation, make_t_bool) in
let%bind body = type_block e body in let%bind body = type_block e body in
ok (e, O.Loop (cond, body)) ok (e, O.Loop (cond, body))
| Assignment {name;annotated_expression} -> ( | I_assignment {name;annotated_expression} -> (
match annotated_expression.type_annotation, Environment.get e name with match annotated_expression.type_annotation, Environment.get e name with
| None, None -> simple_fail "Initial assignments need type" | None, None -> simple_fail "Initial assignments need type"
| Some _, None -> | Some _, None ->
@ -162,11 +162,11 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
let e' = Environment.add e name annotated_expression.type_annotation in let e' = Environment.add e name annotated_expression.type_annotation in
ok (e', O.Assignment {name;annotated_expression}) ok (e', O.Assignment {name;annotated_expression})
) )
| Matching_instr (ex, m) -> | I_matching (ex, m) ->
let%bind ex' = type_annotated_expression e ex in let%bind ex' = type_annotated_expression e ex in
let%bind m' = type_match type_block e ex'.type_annotation m in let%bind m' = type_match type_block e ex'.type_annotation m in
ok (e, O.Matching_instr (ex', m')) ok (e, O.Matching_instr (ex', m'))
| Record_patch _ -> simple_fail "no record_patch yet" | I_record_patch _ -> simple_fail "no record_patch yet"
and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result = and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result =
fun f e t i -> match i with fun f e t i -> match i with
@ -212,14 +212,14 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let return tv' = ok O.(type_value tv' (Some t)) in let return tv' = ok O.(type_value tv' (Some t)) in
match t with match t with
| Type_function (a, b) -> | T_function (a, b) ->
let%bind a' = evaluate_type e a in let%bind a' = evaluate_type e a in
let%bind b' = evaluate_type e b in let%bind b' = evaluate_type e b in
return (Type_function (a', b')) return (Type_function (a', b'))
| Type_tuple lst -> | T_tuple lst ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (Type_tuple lst') return (Type_tuple lst')
| Type_sum m -> | T_sum m ->
let aux k v prev = let aux k v prev =
let%bind prev' = prev in let%bind prev' = prev in
let%bind v' = evaluate_type e v in let%bind v' = evaluate_type e v in
@ -227,7 +227,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
in in
let%bind m = SMap.fold aux m (ok SMap.empty) in let%bind m = SMap.fold aux m (ok SMap.empty) in
return (Type_sum m) return (Type_sum m)
| Type_record m -> | T_record m ->
let aux k v prev = let aux k v prev =
let%bind prev' = prev in let%bind prev' = prev in
let%bind v' = evaluate_type e v in let%bind v' = evaluate_type e v in
@ -235,12 +235,12 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
in in
let%bind m = SMap.fold aux m (ok SMap.empty) in let%bind m = SMap.fold aux m (ok SMap.empty) in
return (Type_record m) return (Type_record m)
| Type_variable name -> | T_variable name ->
let%bind tv = let%bind tv =
trace_option (unbound_type_variable e name) trace_option (unbound_type_variable e name)
@@ Environment.get_type e name in @@ Environment.get_type e name in
ok tv ok tv
| Type_constant (cst, lst) -> | T_constant (cst, lst) ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (Type_constant(cst, lst')) return (Type_constant(cst, lst'))
@ -251,38 +251,38 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let check tv = O.(merge_annotation tv_opt (Some tv)) in let check tv = O.(merge_annotation tv_opt (Some tv)) in
match ae.expression with match ae.expression with
(* Basic *) (* Basic *)
| Variable name -> | E_variable name ->
let%bind tv' = let%bind tv' =
trace_option (unbound_variable e name) trace_option (unbound_variable e name)
@@ Environment.get e name in @@ Environment.get e name in
let%bind type_annotation = check tv' in let%bind type_annotation = check tv' in
ok O.{expression = Variable name ; type_annotation} ok O.{expression = Variable name ; type_annotation}
| Literal (Bool b) -> | E_literal (Literal_bool b) ->
let%bind type_annotation = check make_t_bool in let%bind type_annotation = check make_t_bool in
ok O.{expression = Literal (Bool b) ; type_annotation } ok O.{expression = Literal (Bool b) ; type_annotation }
| Literal Unit -> | E_literal Literal_unit ->
let%bind type_annotation = check make_t_unit in let%bind type_annotation = check make_t_unit in
ok O.{expression = Literal (Unit) ; type_annotation } ok O.{expression = Literal (Unit) ; type_annotation }
| Literal (String s) -> | E_literal (Literal_string s) ->
let%bind type_annotation = check make_t_string in let%bind type_annotation = check make_t_string in
ok O.{expression = Literal (String s) ; type_annotation } ok O.{expression = Literal (String s) ; type_annotation }
| Literal (Bytes s) -> | E_literal (Literal_bytes s) ->
let%bind type_annotation = check make_t_bytes in let%bind type_annotation = check make_t_bytes in
ok O.{expression = Literal (Bytes s) ; type_annotation } ok O.{expression = Literal (Bytes s) ; type_annotation }
| Literal (Number n) -> | E_literal (Literal_number n) ->
let%bind type_annotation = check make_t_int in let%bind type_annotation = check make_t_int in
ok O.{expression = Literal (Int n) ; type_annotation } ok O.{expression = Literal (Int n) ; type_annotation }
(* Tuple *) (* Tuple *)
| Tuple lst -> | E_tuple lst ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
let tv_lst = List.map get_annotation lst' in let tv_lst = List.map get_annotation lst' in
let%bind type_annotation = check (make_t_tuple tv_lst) in let%bind type_annotation = check (make_t_tuple tv_lst) in
ok O.{expression = Tuple lst' ; type_annotation } ok O.{expression = Tuple lst' ; type_annotation }
| Accessor (ae, path) -> | E_accessor (ae, path) ->
let%bind e' = type_annotated_expression e ae in let%bind e' = type_annotated_expression e ae in
let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result = let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
match a with match a with
| Tuple_access index -> ( | Access_tuple index -> (
let%bind tpl_tv = get_t_tuple prev.type_annotation in let%bind tpl_tv = get_t_tuple prev.type_annotation in
let%bind tv = let%bind tv =
generic_try (simple_error "bad tuple index") generic_try (simple_error "bad tuple index")
@ -290,7 +290,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind type_annotation = check tv in let%bind type_annotation = check tv in
ok O.{expression = O.Tuple_accessor (prev, index) ; type_annotation} ok O.{expression = O.Tuple_accessor (prev, index) ; type_annotation}
) )
| Record_access property -> ( | Access_record property -> (
let%bind r_tv = get_t_record prev.type_annotation in let%bind r_tv = get_t_record prev.type_annotation in
let%bind tv = let%bind tv =
generic_try (simple_error "bad record index") generic_try (simple_error "bad record index")
@ -303,7 +303,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
bind_fold_list aux e' path bind_fold_list aux e' path
(* Sum *) (* Sum *)
| Constructor (c, expr) -> | E_constructor (c, expr) ->
let%bind (c_tv, sum_tv) = let%bind (c_tv, sum_tv) =
trace_option (simple_error "no such constructor") trace_option (simple_error "no such constructor")
@@ Environment.get_constructor e c in @@ Environment.get_constructor e c in
@ -312,7 +312,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind type_annotation = check sum_tv in let%bind type_annotation = check sum_tv in
ok O.{expression = O.Constructor(c, expr') ; type_annotation } ok O.{expression = O.Constructor(c, expr') ; type_annotation }
(* Record *) (* Record *)
| Record m -> | E_record m ->
let aux prev k expr = let aux prev k expr =
let%bind expr' = type_annotated_expression e expr in let%bind expr' = type_annotated_expression e expr in
ok (SMap.add k expr' prev) ok (SMap.add k expr' prev)
@ -321,7 +321,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in
ok O.{expression = O.Record m' ; type_annotation } ok O.{expression = O.Record m' ; type_annotation }
(* Data-structure *) (* Data-structure *)
| Map lst -> | E_map lst ->
let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in
let%bind type_annotation = let%bind type_annotation =
let aux opt c = let aux opt c =
@ -347,7 +347,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
check (make_t_map key_type value_type) check (make_t_map key_type value_type)
in in
ok O.{expression = O.Map lst' ; type_annotation} ok O.{expression = O.Map lst' ; type_annotation}
| Lambda { | E_lambda {
binder ; binder ;
input_type ; input_type ;
output_type ; output_type ;
@ -361,13 +361,13 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind result = type_annotated_expression e'' result in let%bind result = type_annotated_expression e'' result in
let%bind type_annotation = check @@ make_t_function input_type output_type in let%bind type_annotation = check @@ make_t_function input_type output_type in
ok O.{expression = Lambda {binder;input_type;output_type;result;body} ; type_annotation} ok O.{expression = Lambda {binder;input_type;output_type;result;body} ; type_annotation}
| Constant (name, lst) -> | E_constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
let tv_lst = List.map get_annotation lst' in let tv_lst = List.map get_annotation lst' in
let%bind (name', tv) = type_constant name tv_lst tv_opt in let%bind (name', tv) = type_constant name tv_lst tv_opt in
let%bind type_annotation = check tv in let%bind type_annotation = check tv in
ok O.{expression = O.Constant (name', lst') ; type_annotation} ok O.{expression = O.Constant (name', lst') ; type_annotation}
| Application (f, arg) -> | E_application (f, arg) ->
let%bind f = type_annotated_expression e f in let%bind f = type_annotated_expression e f in
let%bind arg = type_annotated_expression e arg in let%bind arg = type_annotated_expression e arg in
let%bind type_annotation = match f.type_annotation.type_value with let%bind type_annotation = match f.type_annotation.type_value with
@ -377,7 +377,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
| _ -> simple_fail "applying to not-a-function" | _ -> simple_fail "applying to not-a-function"
in in
ok O.{expression = Application (f, arg) ; type_annotation} ok O.{expression = Application (f, arg) ; type_annotation}
| LookUp dsi -> | E_look_up dsi ->
let%bind (ds, ind) = bind_map_pair (type_annotated_expression e) dsi in let%bind (ds, ind) = bind_map_pair (type_annotated_expression e) dsi in
let%bind (src, dst) = get_t_map ds.type_annotation in let%bind (src, dst) = get_t_map ds.type_annotation in
let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
@ -385,7 +385,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind type_annotation = check dst_opt in let%bind type_annotation = check dst_opt in
ok O.{expression = LookUp (ds, ind) ; type_annotation} ok O.{expression = LookUp (ds, ind) ; type_annotation}
(* Advanced *) (* Advanced *)
| Matching_expr (ex, m) -> ( | E_matching (ex, m) -> (
let%bind ex' = type_annotated_expression e ex in let%bind ex' = type_annotated_expression e ex in
let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in
let%bind type_annotation = match m' with let%bind type_annotation = match m' with
@ -433,12 +433,12 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
let untype_literal (l:O.literal) : I.literal result = let untype_literal (l:O.literal) : I.literal result =
let open I in let open I in
match l with match l with
| Unit -> ok Unit | Unit -> ok Literal_unit
| Bool b -> ok (Bool b) | Bool b -> ok (Literal_bool b)
| Nat n -> ok (Number n) | Nat n -> ok (Literal_number n)
| Int n -> ok (Number n) | Int n -> ok (Literal_number n)
| String s -> ok (String s) | String s -> ok (Literal_string s)
| Bytes b -> ok (Bytes b) | Bytes b -> ok (Literal_bytes b)
let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result = let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
let open I in let open I in
@ -447,50 +447,50 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
match e.expression with match e.expression with
| Literal l -> | Literal l ->
let%bind l = untype_literal l in let%bind l = untype_literal l in
return (Literal l) return (E_literal l)
| Constant (n, lst) -> | Constant (n, lst) ->
let%bind lst' = bind_list let%bind lst' = bind_list
@@ List.map untype_annotated_expression lst in @@ List.map untype_annotated_expression lst in
return (Constant (n, lst')) return (E_constant (n, lst'))
| Variable n -> | Variable n ->
return (Variable n) return (E_variable n)
| Application (f, arg) -> | Application (f, arg) ->
let%bind f' = untype_annotated_expression f in let%bind f' = untype_annotated_expression f in
let%bind arg' = untype_annotated_expression arg in let%bind arg' = untype_annotated_expression arg in
return (Application (f', arg')) return (E_application (f', arg'))
| Lambda {binder;input_type;output_type;body;result} -> | Lambda {binder;input_type;output_type;body;result} ->
let%bind input_type = untype_type_value input_type in let%bind input_type = untype_type_value input_type in
let%bind output_type = untype_type_value output_type in let%bind output_type = untype_type_value output_type in
let%bind result = untype_annotated_expression result in let%bind result = untype_annotated_expression result in
let%bind body = untype_block body in let%bind body = untype_block body in
return (Lambda {binder;input_type;output_type;body;result}) return (E_lambda {binder;input_type;output_type;body;result})
| Tuple lst -> | Tuple lst ->
let%bind lst' = bind_list let%bind lst' = bind_list
@@ List.map untype_annotated_expression lst in @@ List.map untype_annotated_expression lst in
return (Tuple lst') return (E_tuple lst')
| Tuple_accessor (tpl, ind) -> | Tuple_accessor (tpl, ind) ->
let%bind tpl' = untype_annotated_expression tpl in let%bind tpl' = untype_annotated_expression tpl in
return (Accessor (tpl', [Tuple_access ind])) return (E_accessor (tpl', [Access_tuple ind]))
| Constructor (n, p) -> | Constructor (n, p) ->
let%bind p' = untype_annotated_expression p in let%bind p' = untype_annotated_expression p in
return (Constructor (n, p')) return (E_constructor (n, p'))
| Record r -> | Record r ->
let%bind r' = bind_smap let%bind r' = bind_smap
@@ SMap.map untype_annotated_expression r in @@ SMap.map untype_annotated_expression r in
return (Record r') return (E_record r')
| Record_accessor (r, s) -> | Record_accessor (r, s) ->
let%bind r' = untype_annotated_expression r in let%bind r' = untype_annotated_expression r in
return (Accessor (r', [Record_access s])) return (E_accessor (r', [Access_record s]))
| Map m -> | Map m ->
let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
return (Map m') return (E_map m')
| LookUp dsi -> | LookUp dsi ->
let%bind dsi' = bind_map_pair untype_annotated_expression dsi in let%bind dsi' = bind_map_pair untype_annotated_expression dsi in
return (LookUp dsi') return (E_look_up dsi')
| Matching_expr (ae, m) -> | Matching_expr (ae, m) ->
let%bind ae' = untype_annotated_expression ae in let%bind ae' = untype_annotated_expression ae in
let%bind m' = untype_matching untype_annotated_expression m in let%bind m' = untype_matching untype_annotated_expression m in
return (Matching_expr (ae', m')) return (E_matching (ae', m'))
and untype_block (b:O.block) : (I.block) result = and untype_block (b:O.block) : (I.block) result =
bind_list @@ List.map untype_instruction b bind_list @@ List.map untype_instruction b
@ -498,21 +498,21 @@ and untype_block (b:O.block) : (I.block) result =
and untype_instruction (i:O.instruction) : (I.instruction) result = and untype_instruction (i:O.instruction) : (I.instruction) result =
let open I in let open I in
match i with match i with
| Skip -> ok Skip | Skip -> ok I_skip
| Fail e -> | Fail e ->
let%bind e' = untype_annotated_expression e in let%bind e' = untype_annotated_expression e in
ok (Fail e') ok (I_fail e')
| Loop (e, b) -> | Loop (e, b) ->
let%bind e' = untype_annotated_expression e in let%bind e' = untype_annotated_expression e in
let%bind b' = untype_block b in let%bind b' = untype_block b in
ok @@ Loop (e', b') ok @@ I_loop (e', b')
| Assignment a -> | Assignment a ->
let%bind annotated_expression = untype_annotated_expression a.annotated_expression in let%bind annotated_expression = untype_annotated_expression a.annotated_expression in
ok @@ Assignment {name = a.name ; annotated_expression} ok @@ I_assignment {name = a.name ; annotated_expression}
| Matching_instr (e, m) -> | Matching_instr (e, m) ->
let%bind e' = untype_annotated_expression e in let%bind e' = untype_annotated_expression e in
let%bind m' = untype_matching untype_block m in let%bind m' = untype_matching untype_block m in
ok @@ Matching_instr (e', m') ok @@ I_matching (e', m')
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m -> and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
let open I in let open I in