rename ast-typed
This commit is contained in:
Galfour
parent
2de68d4a00
commit
7bb594af0c
@ -11,7 +11,7 @@ type 'a type_name_map = 'a SMap.t
|
||||
type program = declaration list
|
||||
|
||||
and declaration =
|
||||
| Constant_declaration of named_expression
|
||||
| Declaration_constant of named_expression
|
||||
(* | Macro_declaration of macro_declaration *)
|
||||
|
||||
and annotated_expression = {
|
||||
@ -30,11 +30,11 @@ and tv_map = type_value type_name_map
|
||||
and ae_map = annotated_expression name_map
|
||||
|
||||
and type_value' =
|
||||
| Type_tuple of tv list
|
||||
| Type_sum of tv_map
|
||||
| Type_record of tv_map
|
||||
| Type_constant of type_name * tv list
|
||||
| Type_function of tv * tv
|
||||
| T_tuple of tv list
|
||||
| T_sum of tv_map
|
||||
| T_record of tv_map
|
||||
| T_constant of type_name * tv list
|
||||
| T_function of tv * tv
|
||||
|
||||
and type_value = {
|
||||
type_value : type_value' ;
|
||||
@ -51,44 +51,44 @@ and lambda = {
|
||||
|
||||
and expression =
|
||||
(* Base *)
|
||||
| Literal of literal
|
||||
| Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
|
||||
| Variable of name
|
||||
| Application of ae * ae
|
||||
| Lambda of lambda
|
||||
| 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_application of ae * ae
|
||||
| E_lambda of lambda
|
||||
(* Tuple *)
|
||||
| Tuple of ae list
|
||||
| Tuple_accessor of ae * int (* Access n'th tuple's element *)
|
||||
| E_tuple of ae list
|
||||
| E_tuple_accessor of ae * int (* Access n'th tuple's element *)
|
||||
(* Sum *)
|
||||
| Constructor of name * ae (* For user defined constructors *)
|
||||
| E_constructor of name * ae (* For user defined constructors *)
|
||||
(* Record *)
|
||||
| Record of ae_map
|
||||
| Record_accessor of ae * string
|
||||
| E_record of ae_map
|
||||
| E_record_accessor of ae * string
|
||||
(* Data Structures *)
|
||||
| Map of (ae * ae) list
|
||||
| LookUp of (ae * ae)
|
||||
| E_map of (ae * ae) list
|
||||
| E_look_up of (ae * ae)
|
||||
(* Advanced *)
|
||||
| Matching_expr of (ae * matching_expr)
|
||||
| E_matching of (ae * matching_expr)
|
||||
|
||||
and value = annotated_expression (* todo (for refactoring) *)
|
||||
|
||||
and literal =
|
||||
| Unit
|
||||
| Bool of bool
|
||||
| Int of int
|
||||
| Nat of int
|
||||
| String of string
|
||||
| Bytes of bytes
|
||||
| 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 =
|
||||
| Assignment of named_expression
|
||||
| Matching_instr of ae * matching_instr
|
||||
| Loop of ae * b
|
||||
| Skip
|
||||
| Fail of ae
|
||||
| I_assignment of named_expression
|
||||
| I_matching of ae * matching_instr
|
||||
| I_loop of ae * b
|
||||
| I_skip
|
||||
| I_fail of ae
|
||||
|
||||
and 'a matching =
|
||||
| Match_bool of {
|
||||
@ -119,8 +119,8 @@ let get_type_annotation x = x.type_annotation
|
||||
let get_entry (p:program) (entry : string) : annotated_expression result =
|
||||
let aux (d:declaration) =
|
||||
match d with
|
||||
| Constant_declaration {name ; annotated_expression} when entry = name -> Some annotated_expression
|
||||
| Constant_declaration _ -> None
|
||||
| Declaration_constant {name ; annotated_expression} when entry = name -> Some annotated_expression
|
||||
| Declaration_constant _ -> None
|
||||
in
|
||||
let%bind result =
|
||||
trace_option (simple_error "no entry point with given name") @@
|
||||
@ -130,7 +130,7 @@ let get_entry (p:program) (entry : string) : annotated_expression result =
|
||||
let get_functional_entry (p:program) (entry : string) : (lambda * type_value) result =
|
||||
let%bind entry = get_entry p entry in
|
||||
match entry.expression with
|
||||
| Lambda l -> ok (l, entry.type_annotation)
|
||||
| E_lambda l -> ok (l, entry.type_annotation)
|
||||
| _ -> simple_fail "given entry point is not functional"
|
||||
|
||||
module PP = struct
|
||||
@ -139,12 +139,12 @@ module PP = struct
|
||||
|
||||
let rec type_value' ppf (tv':type_value') : unit =
|
||||
match tv' with
|
||||
| Type_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_value) lst
|
||||
| Type_sum m -> fprintf ppf "sum[%a]" (smap_sep type_value) m
|
||||
| Type_record m -> fprintf ppf "record[%a]" (smap_sep type_value) m
|
||||
| Type_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
|
||||
| Type_constant (c, []) -> fprintf ppf "%s" c
|
||||
| Type_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep type_value) n
|
||||
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_value) lst
|
||||
| T_sum m -> fprintf ppf "sum[%a]" (smap_sep type_value) m
|
||||
| T_record m -> fprintf ppf "record[%a]" (smap_sep type_value) m
|
||||
| T_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
|
||||
| T_constant (c, []) -> fprintf ppf "%s" c
|
||||
| T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep type_value) n
|
||||
|
||||
and type_value ppf (tv:type_value) : unit =
|
||||
type_value' ppf tv.type_value
|
||||
@ -156,22 +156,22 @@ module PP = struct
|
||||
|
||||
and expression ppf (e:expression) : unit =
|
||||
match e with
|
||||
| Literal l -> literal ppf l
|
||||
| Constant (c, lst) -> fprintf ppf "%s(%a)" c (list_sep annotated_expression) lst
|
||||
| Constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
|
||||
| Variable a -> fprintf ppf "%s" a
|
||||
| Application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
|
||||
| Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
|
||||
| Lambda {binder;input_type;output_type;result;body} ->
|
||||
| E_literal l -> literal ppf l
|
||||
| E_constant (c, lst) -> fprintf ppf "%s(%a)" c (list_sep annotated_expression) lst
|
||||
| E_constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
|
||||
| E_variable a -> fprintf ppf "%s" a
|
||||
| E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
|
||||
| E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
|
||||
| E_lambda {binder;input_type;output_type;result;body} ->
|
||||
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
|
||||
binder type_value input_type type_value output_type
|
||||
block body annotated_expression result
|
||||
| Tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
|
||||
| Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
|
||||
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
|
||||
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
|
||||
| LookUp (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
|
||||
| Matching_expr (ae, m) ->
|
||||
| E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
|
||||
| E_record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
|
||||
| E_record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
|
||||
| E_map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
|
||||
| E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
|
||||
| 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) ->
|
||||
@ -179,12 +179,12 @@ module PP = struct
|
||||
|
||||
and literal ppf (l:literal) : unit =
|
||||
match l with
|
||||
| Unit -> fprintf ppf "unit"
|
||||
| Bool b -> fprintf ppf "%b" b
|
||||
| Int n -> fprintf ppf "%d" n
|
||||
| Nat n -> fprintf ppf "%d" n
|
||||
| String s -> fprintf ppf "%s" s
|
||||
| Bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
|
||||
| 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
|
||||
|
||||
and block ppf (b:block) = (list_sep instruction) ppf b
|
||||
|
||||
@ -202,17 +202,17 @@ module PP = struct
|
||||
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some
|
||||
|
||||
and instruction ppf (i:instruction) = match i with
|
||||
| Skip -> fprintf ppf "skip"
|
||||
| Fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
|
||||
| Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
|
||||
| Assignment {name;annotated_expression = ae} ->
|
||||
| I_skip -> fprintf ppf "skip"
|
||||
| I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
|
||||
| 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
|
||||
| Matching_instr (ae, m) ->
|
||||
| I_matching (ae, m) ->
|
||||
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
|
||||
|
||||
let declaration ppf (d:declaration) =
|
||||
match d with
|
||||
| Constant_declaration {name ; annotated_expression = ae} ->
|
||||
| Declaration_constant {name ; annotated_expression = ae} ->
|
||||
fprintf ppf "const %s = %a" name annotated_expression ae
|
||||
|
||||
let program ppf (p:program) =
|
||||
@ -249,14 +249,14 @@ end
|
||||
open Errors
|
||||
|
||||
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value, b.type_value) with
|
||||
| Type_tuple ta, Type_tuple tb -> (
|
||||
| T_tuple ta, T_tuple tb -> (
|
||||
let%bind _ =
|
||||
trace_strong (different_size_tuples a b)
|
||||
@@ Assert.assert_true List.(length ta = length tb) in
|
||||
bind_list_iter assert_type_value_eq (List.combine ta tb)
|
||||
)
|
||||
| Type_tuple _, _ -> fail @@ different_kinds a b
|
||||
| Type_constant (ca, lsta), Type_constant (cb, lstb) -> (
|
||||
| T_tuple _, _ -> fail @@ different_kinds a b
|
||||
| T_constant (ca, lsta), T_constant (cb, lstb) -> (
|
||||
let%bind _ =
|
||||
trace_strong (different_size_constants a b)
|
||||
@@ Assert.assert_true List.(length lsta = length lstb) in
|
||||
@ -266,8 +266,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
|
||||
trace (simple_error "constant sub-expression")
|
||||
@@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
|
||||
)
|
||||
| Type_constant _, _ -> fail @@ different_kinds a b
|
||||
| Type_sum sa, Type_sum sb -> (
|
||||
| T_constant _, _ -> fail @@ different_kinds a b
|
||||
| T_sum sa, T_sum sb -> (
|
||||
let sa' = SMap.to_kv_list sa in
|
||||
let sb' = SMap.to_kv_list sb in
|
||||
let aux ((ka, va), (kb, vb)) =
|
||||
@ -283,8 +283,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
|
||||
bind_list_iter aux (List.combine sa' sb')
|
||||
|
||||
)
|
||||
| Type_sum _, _ -> fail @@ different_kinds a b
|
||||
| Type_record ra, Type_record rb -> (
|
||||
| T_sum _, _ -> fail @@ different_kinds a b
|
||||
| T_record ra, T_record rb -> (
|
||||
let ra' = SMap.to_kv_list ra in
|
||||
let rb' = SMap.to_kv_list rb in
|
||||
let aux ((ka, va), (kb, vb)) =
|
||||
@ -300,12 +300,12 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
|
||||
@@ bind_list_iter aux (List.combine ra' rb')
|
||||
|
||||
)
|
||||
| Type_record _, _ -> fail @@ different_kinds a b
|
||||
| Type_function (param, result), Type_function (param', result') ->
|
||||
| T_record _, _ -> fail @@ different_kinds a b
|
||||
| T_function (param, result), T_function (param', result') ->
|
||||
let%bind _ = assert_type_value_eq (param, param') in
|
||||
let%bind _ = assert_type_value_eq (result, result') in
|
||||
ok ()
|
||||
| Type_function _, _ -> fail @@ different_kinds a b
|
||||
| T_function _, _ -> fail @@ different_kinds a b
|
||||
|
||||
(* No information about what made it fail *)
|
||||
let type_value_eq ab = match assert_type_value_eq ab with
|
||||
@ -314,61 +314,61 @@ let type_value_eq ab = match assert_type_value_eq ab with
|
||||
|
||||
let assert_literal_eq (a, b : literal * literal) : unit result =
|
||||
match (a, b) with
|
||||
| Bool a, Bool b when a = b -> ok ()
|
||||
| Bool _, Bool _ -> simple_fail "different bools"
|
||||
| Bool _, _ -> simple_fail "bool vs non-bool"
|
||||
| Int a, Int b when a = b -> ok ()
|
||||
| Int _, Int _ -> simple_fail "different ints"
|
||||
| Int _, _ -> simple_fail "int vs non-int"
|
||||
| Nat a, Nat b when a = b -> ok ()
|
||||
| Nat _, Nat _ -> simple_fail "different nats"
|
||||
| Nat _, _ -> simple_fail "nat vs non-nat"
|
||||
| String a, String b when a = b -> ok ()
|
||||
| String _, String _ -> simple_fail "different strings"
|
||||
| String _, _ -> simple_fail "string vs non-string"
|
||||
| Bytes a, Bytes b when a = b -> ok ()
|
||||
| Bytes _, Bytes _ -> simple_fail "different bytess"
|
||||
| Bytes _, _ -> simple_fail "bytes vs non-bytes"
|
||||
| Unit, Unit -> ok ()
|
||||
| Unit, _ -> simple_fail "unit vs non-unit"
|
||||
| Literal_bool a, Literal_bool b when a = b -> ok ()
|
||||
| Literal_bool _, Literal_bool _ -> simple_fail "different bools"
|
||||
| Literal_bool _, _ -> simple_fail "bool vs non-bool"
|
||||
| Literal_int a, Literal_int b when a = b -> ok ()
|
||||
| Literal_int _, Literal_int _ -> simple_fail "different ints"
|
||||
| Literal_int _, _ -> simple_fail "int vs non-int"
|
||||
| Literal_nat a, Literal_nat b when a = b -> ok ()
|
||||
| Literal_nat _, Literal_nat _ -> simple_fail "different nats"
|
||||
| Literal_nat _, _ -> simple_fail "nat vs non-nat"
|
||||
| Literal_string a, Literal_string b when a = b -> ok ()
|
||||
| Literal_string _, Literal_string _ -> simple_fail "different strings"
|
||||
| Literal_string _, _ -> simple_fail "string vs non-string"
|
||||
| Literal_bytes a, Literal_bytes b when a = b -> ok ()
|
||||
| Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess"
|
||||
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
|
||||
| Literal_unit, Literal_unit -> ok ()
|
||||
| Literal_unit, _ -> simple_fail "unit vs non-unit"
|
||||
|
||||
|
||||
let rec assert_value_eq (a, b: (value*value)) : unit result = match (a.expression, b.expression) with
|
||||
| Literal a, Literal b ->
|
||||
| E_literal a, E_literal b ->
|
||||
assert_literal_eq (a, b)
|
||||
|
||||
| Constant (ca, lsta), Constant (cb, lstb) when ca = cb -> (
|
||||
| E_constant (ca, lsta), E_constant (cb, lstb) when ca = cb -> (
|
||||
let%bind lst =
|
||||
generic_try (simple_error "constants with different numbers of elements")
|
||||
(fun () -> List.combine lsta lstb) in
|
||||
let%bind _all = bind_list @@ List.map assert_value_eq lst in
|
||||
ok ()
|
||||
)
|
||||
| Constant _, Constant _ ->
|
||||
| E_constant _, E_constant _ ->
|
||||
simple_fail "different constants"
|
||||
| Constant _, _ ->
|
||||
| E_constant _, _ ->
|
||||
simple_fail "comparing constant with other stuff"
|
||||
|
||||
| Constructor (ca, a), Constructor (cb, b) when ca = cb -> (
|
||||
| E_constructor (ca, a), E_constructor (cb, b) when ca = cb -> (
|
||||
let%bind _eq = assert_value_eq (a, b) in
|
||||
ok ()
|
||||
)
|
||||
| Constructor _, Constructor _ ->
|
||||
| E_constructor _, E_constructor _ ->
|
||||
simple_fail "different constructors"
|
||||
| Constructor _, _ ->
|
||||
| E_constructor _, _ ->
|
||||
simple_fail "comparing constructor with other stuff"
|
||||
|
||||
| Tuple lsta, Tuple lstb -> (
|
||||
| E_tuple lsta, E_tuple lstb -> (
|
||||
let%bind lst =
|
||||
generic_try (simple_error "tuples with different numbers of elements")
|
||||
(fun () -> List.combine lsta lstb) in
|
||||
let%bind _all = bind_list @@ List.map assert_value_eq lst in
|
||||
ok ()
|
||||
)
|
||||
| Tuple _, _ ->
|
||||
| E_tuple _, _ ->
|
||||
simple_fail "comparing tuple with other stuff"
|
||||
|
||||
| Record sma, Record smb -> (
|
||||
| E_record sma, E_record smb -> (
|
||||
let aux _ a b =
|
||||
match a, b with
|
||||
| Some a, Some b -> Some (assert_value_eq (a, b))
|
||||
@ -377,10 +377,10 @@ let rec assert_value_eq (a, b: (value*value)) : unit result = match (a.expressio
|
||||
let%bind _all = bind_smap @@ SMap.merge aux sma smb in
|
||||
ok ()
|
||||
)
|
||||
| Record _, _ ->
|
||||
| E_record _, _ ->
|
||||
simple_fail "comparing record with other stuff"
|
||||
|
||||
| Map lsta, Map lstb -> (
|
||||
| E_map lsta, E_map lstb -> (
|
||||
let%bind lst = generic_try (simple_error "maps of different lengths")
|
||||
(fun () ->
|
||||
let lsta' = List.sort compare lsta in
|
||||
@ -393,7 +393,7 @@ let rec assert_value_eq (a, b: (value*value)) : unit result = match (a.expressio
|
||||
let%bind _all = bind_map_list aux lst in
|
||||
ok ()
|
||||
)
|
||||
| Map _, _ ->
|
||||
| E_map _, _ ->
|
||||
simple_fail "comparing map with other stuff"
|
||||
|
||||
| _, _ -> simple_fail "comparing not a value"
|
||||
@ -411,102 +411,102 @@ let merge_annotation (a:type_value option) (b:type_value option) : type_value re
|
||||
|
||||
module Combinators = struct
|
||||
|
||||
let t_bool s : type_value = type_value (Type_constant ("bool", [])) s
|
||||
let t_bool s : type_value = type_value (T_constant ("bool", [])) s
|
||||
let simplify_t_bool s = t_bool (Some s)
|
||||
let make_t_bool = t_bool None
|
||||
|
||||
let t_string s : type_value = type_value (Type_constant ("string", [])) s
|
||||
let t_string s : type_value = type_value (T_constant ("string", [])) s
|
||||
let simplify_t_string s = t_string (Some s)
|
||||
let make_t_string = t_string None
|
||||
|
||||
let t_bytes s : type_value = type_value (Type_constant ("bytes", [])) s
|
||||
let t_bytes s : type_value = type_value (T_constant ("bytes", [])) s
|
||||
let simplify_t_bytes s = t_bytes (Some s)
|
||||
let make_t_bytes = t_bytes None
|
||||
|
||||
let t_int s : type_value = type_value (Type_constant ("int", [])) s
|
||||
let t_int s : type_value = type_value (T_constant ("int", [])) s
|
||||
let simplify_t_int s = t_int (Some s)
|
||||
let make_t_int = t_int None
|
||||
|
||||
let t_unit s : type_value = type_value (Type_constant ("unit", [])) s
|
||||
let t_unit s : type_value = type_value (T_constant ("unit", [])) s
|
||||
let simplify_t_unit s = t_unit (Some s)
|
||||
let make_t_unit = t_unit None
|
||||
|
||||
let t_option o s : type_value = type_value (Type_constant ("option", [o])) s
|
||||
let t_option o s : type_value = type_value (T_constant ("option", [o])) s
|
||||
let make_t_option o = t_option o None
|
||||
|
||||
let t_tuple lst s : type_value = type_value (Type_tuple lst) s
|
||||
let t_tuple lst s : type_value = type_value (T_tuple lst) s
|
||||
let simplify_t_tuple lst s = t_tuple lst (Some s)
|
||||
let make_t_tuple lst = t_tuple lst None
|
||||
let make_t_pair a b = make_t_tuple [a ; b]
|
||||
|
||||
let t_record m s : type_value = type_value (Type_record m) s
|
||||
let t_record m s : type_value = type_value (T_record m) s
|
||||
let make_t_ez_record (lst:(string * type_value) list) : type_value =
|
||||
let aux prev (k, v) = SMap.add k v prev in
|
||||
let map = List.fold_left aux SMap.empty lst in
|
||||
type_value (Type_record map) None
|
||||
type_value (T_record map) None
|
||||
let make_t_record m = t_record m None
|
||||
let make_t_record_ez lst =
|
||||
let m = SMap.of_list lst in
|
||||
make_t_record m
|
||||
|
||||
let t_map key value s = type_value (Type_constant ("map", [key ; value])) s
|
||||
let t_map key value s = type_value (T_constant ("map", [key ; value])) s
|
||||
let make_t_map key value = t_map key value None
|
||||
|
||||
let t_sum m s : type_value = type_value (Type_sum m) s
|
||||
let t_sum m s : type_value = type_value (T_sum m) s
|
||||
let make_t_sum m = t_sum m None
|
||||
let make_t_ez_sum (lst:(string * type_value) list) : type_value =
|
||||
let aux prev (k, v) = SMap.add k v prev in
|
||||
let map = List.fold_left aux SMap.empty lst in
|
||||
type_value (Type_sum map) None
|
||||
type_value (T_sum map) None
|
||||
|
||||
let t_function param result s : type_value = type_value (Type_function (param, result)) s
|
||||
let t_function param result s : type_value = type_value (T_function (param, result)) s
|
||||
let make_t_function param result = t_function param result None
|
||||
|
||||
let get_annotation (x:annotated_expression) = x.type_annotation
|
||||
|
||||
let get_t_bool (t:type_value) : unit result = match t.type_value with
|
||||
| Type_constant ("bool", []) -> ok ()
|
||||
| T_constant ("bool", []) -> ok ()
|
||||
| _ -> simple_fail "not a bool"
|
||||
|
||||
let get_t_option (t:type_value) : type_value result = match t.type_value with
|
||||
| Type_constant ("option", [o]) -> ok o
|
||||
| T_constant ("option", [o]) -> ok o
|
||||
| _ -> simple_fail "not a option"
|
||||
|
||||
let get_t_list (t:type_value) : type_value result = match t.type_value with
|
||||
| Type_constant ("list", [o]) -> ok o
|
||||
| T_constant ("list", [o]) -> ok o
|
||||
| _ -> simple_fail "not a list"
|
||||
|
||||
let get_t_tuple (t:type_value) : type_value list result = match t.type_value with
|
||||
| Type_tuple lst -> ok lst
|
||||
| T_tuple lst -> ok lst
|
||||
| _ -> simple_fail "not a tuple"
|
||||
|
||||
let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value with
|
||||
| Type_sum m -> ok m
|
||||
| T_sum m -> ok m
|
||||
| _ -> simple_fail "not a sum"
|
||||
|
||||
let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value with
|
||||
| Type_record m -> ok m
|
||||
| T_record m -> ok m
|
||||
| _ -> simple_fail "not a record"
|
||||
|
||||
let get_t_map (t:type_value) : (type_value * type_value) result =
|
||||
match t.type_value with
|
||||
| Type_constant ("map", [k;v]) -> ok (k, v)
|
||||
| T_constant ("map", [k;v]) -> ok (k, v)
|
||||
| _ -> simple_fail "not a map"
|
||||
|
||||
let record map : expression = Record map
|
||||
let record map : expression = E_record map
|
||||
let record_ez (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
|
||||
record map
|
||||
let some s : expression = Constant ("SOME", [s])
|
||||
let none : expression = Constant ("NONE", [])
|
||||
let some s : expression = E_constant ("SOME", [s])
|
||||
let none : expression = E_constant ("NONE", [])
|
||||
|
||||
let map lst : expression = Map lst
|
||||
let map lst : expression = E_map lst
|
||||
|
||||
let unit : expression = Literal (Unit)
|
||||
let int n : expression = Literal (Int n)
|
||||
let bool b : expression = Literal (Bool b)
|
||||
let pair a b : expression = Constant ("PAIR", [a; b])
|
||||
let unit : expression = E_literal (Literal_unit)
|
||||
let int n : expression = E_literal (Literal_int n)
|
||||
let bool b : expression = E_literal (Literal_bool b)
|
||||
let pair a b : expression = E_constant ("PAIR", [a; b])
|
||||
|
||||
let a_unit = annotated_expression unit make_t_unit
|
||||
let a_int n = annotated_expression (int n) make_t_int
|
||||
@ -514,23 +514,23 @@ module Combinators = struct
|
||||
let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
|
||||
let a_some s = annotated_expression (some s) (make_t_option s.type_annotation)
|
||||
let a_none t = annotated_expression none (make_t_option t)
|
||||
let a_tuple lst = annotated_expression (Tuple lst) (make_t_tuple (List.map get_type_annotation lst))
|
||||
let a_tuple lst = annotated_expression (E_tuple lst) (make_t_tuple (List.map get_type_annotation lst))
|
||||
let a_record r = annotated_expression (record r) (make_t_record (SMap.map get_type_annotation r))
|
||||
let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
|
||||
let a_map lst k v = annotated_expression (map lst) (make_t_map k v)
|
||||
|
||||
let get_a_int (t:annotated_expression) =
|
||||
match t.expression with
|
||||
| Literal (Int n) -> ok n
|
||||
| E_literal (Literal_int n) -> ok n
|
||||
| _ -> simple_fail "not an int"
|
||||
|
||||
let get_a_unit (t:annotated_expression) =
|
||||
match t.expression with
|
||||
| Literal (Unit) -> ok ()
|
||||
| E_literal (Literal_unit) -> ok ()
|
||||
| _ -> simple_fail "not a unit"
|
||||
|
||||
let get_a_bool (t:annotated_expression) =
|
||||
match t.expression with
|
||||
| Literal (Bool b) -> ok b
|
||||
| E_literal (Literal_bool b) -> ok b
|
||||
| _ -> simple_fail "not a bool"
|
||||
end
|
||||
|
||||
@ -165,7 +165,7 @@ let easy_run_typed
|
||||
let%bind main_result_type =
|
||||
let%bind typed_main = Ast_typed.get_functional_entry program entry in
|
||||
match (snd typed_main).type_value with
|
||||
| Type_function (_, result) -> ok result
|
||||
| T_function (_, result) -> ok result
|
||||
| _ -> simple_fail "main doesn't have fun type" in
|
||||
untranspile_value mini_c_result main_result_type in
|
||||
ok typed_result
|
||||
|
||||
@ -13,18 +13,18 @@ let map_of_kv_list lst =
|
||||
|
||||
let rec translate_type (t:AST.type_value) : type_value result =
|
||||
match t.type_value with
|
||||
| Type_constant ("bool", []) -> ok (`Base Bool)
|
||||
| Type_constant ("int", []) -> ok (`Base Int)
|
||||
| Type_constant ("string", []) -> ok (`Base String)
|
||||
| Type_constant ("unit", []) -> ok (`Base Unit)
|
||||
| Type_constant ("map", [key;value]) ->
|
||||
| T_constant ("bool", []) -> ok (`Base Bool)
|
||||
| T_constant ("int", []) -> ok (`Base Int)
|
||||
| T_constant ("string", []) -> ok (`Base String)
|
||||
| T_constant ("unit", []) -> ok (`Base Unit)
|
||||
| T_constant ("map", [key;value]) ->
|
||||
let%bind kv' = bind_map_pair translate_type (key, value) in
|
||||
ok (`Map kv')
|
||||
| Type_constant ("option", [o]) ->
|
||||
| T_constant ("option", [o]) ->
|
||||
let%bind o' = translate_type o in
|
||||
ok (`Option o')
|
||||
| Type_constant (name, _) -> fail (error "unrecognized constant" name)
|
||||
| Type_sum m ->
|
||||
| T_constant (name, _) -> fail (error "unrecognized constant" name)
|
||||
| T_sum m ->
|
||||
let node = Append_tree.of_list @@ list_of_map m in
|
||||
let aux a b : type_value result =
|
||||
let%bind a = a in
|
||||
@ -32,7 +32,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
|
||||
ok (`Or (a, b))
|
||||
in
|
||||
Append_tree.fold_ne translate_type aux node
|
||||
| Type_record m ->
|
||||
| T_record m ->
|
||||
let node = Append_tree.of_list @@ list_of_map m in
|
||||
let aux a b : type_value result =
|
||||
let%bind a = a in
|
||||
@ -40,7 +40,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
|
||||
ok (`Pair (a, b))
|
||||
in
|
||||
Append_tree.fold_ne translate_type aux node
|
||||
| Type_tuple lst ->
|
||||
| T_tuple lst ->
|
||||
let node = Append_tree.of_list lst in
|
||||
let aux a b : type_value result =
|
||||
let%bind a = a in
|
||||
@ -48,7 +48,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
|
||||
ok (`Pair (a, b))
|
||||
in
|
||||
Append_tree.fold_ne translate_type aux node
|
||||
| Type_function (param, result) ->
|
||||
| T_function (param, result) ->
|
||||
let%bind param' = translate_type param in
|
||||
let%bind result' = translate_type result in
|
||||
ok (`Function (param', result'))
|
||||
@ -70,11 +70,11 @@ let rec translate_block env (b:AST.block) : block result =
|
||||
and translate_instruction (env:Environment.t) (i:AST.instruction) : statement option result =
|
||||
let return ?(env' = env) x : statement option result = ok (Some (x, environment_wrap env env')) in
|
||||
match i with
|
||||
| Assignment {name;annotated_expression} ->
|
||||
| I_assignment {name;annotated_expression} ->
|
||||
let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in
|
||||
let env' = Environment.add (name, t) env in
|
||||
return ~env' (Assignment (name, expression))
|
||||
| Matching_instr (expr, m) -> (
|
||||
| I_matching (expr, m) -> (
|
||||
let%bind expr' = translate_annotated_expression env expr in
|
||||
let env' = Environment.extend env in
|
||||
match m with
|
||||
@ -93,30 +93,30 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
|
||||
)
|
||||
| _ -> simple_fail "todo : match"
|
||||
)
|
||||
| Loop (expr, body) ->
|
||||
| I_loop (expr, body) ->
|
||||
let%bind expr' = translate_annotated_expression env expr in
|
||||
let%bind body' = translate_block env body in
|
||||
return (While (expr', body'))
|
||||
| Skip -> ok None
|
||||
| Fail _ -> simple_fail "todo : fail"
|
||||
| I_skip -> ok None
|
||||
| I_fail _ -> simple_fail "todo : fail"
|
||||
|
||||
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
|
||||
let%bind tv = translate_type ae.type_annotation in
|
||||
let return (expr, tv) = ok (expr, tv, env) in
|
||||
let f = translate_annotated_expression env in
|
||||
match ae.expression with
|
||||
| Literal (Bool b) -> ok (Literal (`Bool b), tv, env)
|
||||
| Literal (Int n) -> ok (Literal (`Int n), tv, env)
|
||||
| Literal (Nat n) -> ok (Literal (`Nat n), tv, env)
|
||||
| Literal (Bytes s) -> ok (Literal (`Bytes s), tv, env)
|
||||
| Literal (String s) -> ok (Literal (`String s), tv, env)
|
||||
| Literal Unit -> ok (Literal `Unit, tv, env)
|
||||
| Variable name -> ok (Var name, tv, env)
|
||||
| Application (a, b) ->
|
||||
| E_literal (Literal_bool b) -> ok (Literal (`Bool b), tv, env)
|
||||
| E_literal (Literal_int n) -> ok (Literal (`Int n), tv, env)
|
||||
| E_literal (Literal_nat n) -> ok (Literal (`Nat n), tv, env)
|
||||
| E_literal (Literal_bytes s) -> ok (Literal (`Bytes s), tv, env)
|
||||
| E_literal (Literal_string s) -> ok (Literal (`String s), tv, env)
|
||||
| E_literal Literal_unit -> ok (Literal `Unit, tv, env)
|
||||
| E_variable name -> ok (Var name, tv, env)
|
||||
| E_application (a, b) ->
|
||||
let%bind a = translate_annotated_expression env a in
|
||||
let%bind b = translate_annotated_expression env b in
|
||||
ok (Apply (a, b), tv, env)
|
||||
| Constructor (m, param) ->
|
||||
| E_constructor (m, param) ->
|
||||
let%bind (param'_expr, param'_tv, _) = translate_annotated_expression env ae in
|
||||
let%bind map_tv = get_t_sum ae.type_annotation in
|
||||
let node_tv = Append_tree.of_list @@ kv_list_of_map map_tv in
|
||||
@ -146,7 +146,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
ae_opt in
|
||||
ok (ae, tv, env) in
|
||||
ok ae'
|
||||
| Tuple lst ->
|
||||
| E_tuple lst ->
|
||||
let node = Append_tree.of_list lst in
|
||||
let aux (a:expression result) (b:expression result) : expression result =
|
||||
let%bind (_, a_ty, _) as a = a in
|
||||
@ -154,7 +154,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
ok (Predicate ("PAIR", [a; b]), `Pair(a_ty, b_ty), env)
|
||||
in
|
||||
Append_tree.fold_ne (translate_annotated_expression env) aux node
|
||||
| Tuple_accessor (tpl, ind) ->
|
||||
| E_tuple_accessor (tpl, ind) ->
|
||||
let%bind tpl' = translate_annotated_expression env tpl in
|
||||
let%bind tpl_tv = get_t_tuple tpl.type_annotation in
|
||||
let node_tv = Append_tree.of_list @@ List.mapi (fun i a -> (i, a)) tpl_tv in
|
||||
@ -178,7 +178,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
trace_strong (simple_error "bad index in tuple (shouldn't happen here)") @@
|
||||
Append_tree.fold_ne leaf node node_tv in
|
||||
ok expr
|
||||
| Record m ->
|
||||
| E_record m ->
|
||||
let node = Append_tree.of_list @@ list_of_map m in
|
||||
let aux a b : expression result =
|
||||
let%bind (_, a_ty, _) as a = a in
|
||||
@ -186,7 +186,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
ok (Predicate ("PAIR", [a; b]), `Pair(a_ty, b_ty), env)
|
||||
in
|
||||
Append_tree.fold_ne (translate_annotated_expression env) aux node
|
||||
| Record_accessor (record, property) ->
|
||||
| E_record_accessor (record, property) ->
|
||||
let%bind translation = translate_annotated_expression env record in
|
||||
let%bind record_type_map =
|
||||
trace (simple_error (Format.asprintf "Accessing field of %a, that has type %a, which isn't a record" AST.PP.annotated_expression record AST.PP.type_value record.type_annotation)) @@
|
||||
@ -212,7 +212,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
trace_strong (simple_error "bad key in record (shouldn't happen here)") @@
|
||||
Append_tree.fold_ne leaf node node_tv in
|
||||
ok expr
|
||||
| Constant (name, lst) ->
|
||||
| E_constant (name, lst) ->
|
||||
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in (
|
||||
match name, lst with
|
||||
| "NONE", [] ->
|
||||
@ -220,8 +220,8 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
ok (Make_None o, tv, env)
|
||||
| _ -> ok (Predicate (name, lst'), tv, env)
|
||||
)
|
||||
| Lambda l -> translate_lambda env l tv
|
||||
| Map m ->
|
||||
| E_lambda l -> translate_lambda env l tv
|
||||
| E_map m ->
|
||||
let%bind (src, dst) = Mini_c.Combinators.get_t_map tv in
|
||||
let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev (k, v) ->
|
||||
let%bind prev' = prev in
|
||||
@ -232,10 +232,10 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
in
|
||||
let init = return (Empty_map (src, dst), tv) in
|
||||
List.fold_left aux init m
|
||||
| LookUp dsi ->
|
||||
| E_look_up dsi ->
|
||||
let%bind (ds', i') = bind_map_pair f dsi in
|
||||
return (Predicate ("GET", [i' ; ds']), tv)
|
||||
| Matching_expr (expr, m) -> (
|
||||
| E_matching (expr, m) -> (
|
||||
let%bind expr' = translate_annotated_expression env expr in
|
||||
match m with
|
||||
| AST.Match_bool {match_true ; match_false} ->
|
||||
@ -281,7 +281,7 @@ and translate_lambda env l tv =
|
||||
|
||||
let translate_declaration env (d:AST.declaration) : toplevel_statement result =
|
||||
match d with
|
||||
| Constant_declaration {name;annotated_expression} ->
|
||||
| Declaration_constant {name;annotated_expression} ->
|
||||
let%bind ((_, tv, _) as expression) = translate_annotated_expression env annotated_expression in
|
||||
let env' = Environment.add (name, tv) env in
|
||||
ok @@ ((name, expression), environment_wrap env env')
|
||||
@ -311,7 +311,7 @@ let functionalize (e:AST.annotated_expression) : AST.lambda * AST.type_value =
|
||||
input_type = Combinators.make_t_unit ;
|
||||
output_type = t ;
|
||||
result = e ;
|
||||
body = [Skip]
|
||||
body = [I_skip]
|
||||
}, Combinators.(make_t_function make_t_unit t)
|
||||
|
||||
let translate_entry (lst:AST.program) (name:string) : anon_function result =
|
||||
@ -319,16 +319,16 @@ let translate_entry (lst:AST.program) (name:string) : anon_function result =
|
||||
match lst with
|
||||
| [] -> None
|
||||
| hd :: tl -> (
|
||||
let AST.Constant_declaration an = hd in
|
||||
let AST.Declaration_constant an = hd in
|
||||
if an.name = name
|
||||
then (
|
||||
match an.annotated_expression.expression with
|
||||
| Lambda l -> Some (acc, l, an.annotated_expression.type_annotation)
|
||||
| E_lambda l -> Some (acc, l, an.annotated_expression.type_annotation)
|
||||
| _ ->
|
||||
let (a, b) = functionalize an.annotated_expression in
|
||||
Some (acc, a, b)
|
||||
) else (
|
||||
aux ((AST.Assignment an) :: acc) tl
|
||||
aux ((AST.I_assignment an) :: acc) tl
|
||||
)
|
||||
)
|
||||
in
|
||||
@ -396,26 +396,26 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
|
||||
let open! AST in
|
||||
let return e = ok AST.(annotated_expression e t) in
|
||||
match t.type_value with
|
||||
| Type_constant ("unit", []) ->
|
||||
| T_constant ("unit", []) ->
|
||||
let%bind () = get_unit v in
|
||||
return (Literal Unit)
|
||||
| Type_constant ("bool", []) ->
|
||||
return (E_literal Literal_unit)
|
||||
| T_constant ("bool", []) ->
|
||||
let%bind b = get_bool v in
|
||||
return (Literal (Bool b))
|
||||
| Type_constant ("int", []) ->
|
||||
return (E_literal (Literal_bool b))
|
||||
| T_constant ("int", []) ->
|
||||
let%bind n = get_int v in
|
||||
return (Literal (Int n))
|
||||
| Type_constant ("string", []) ->
|
||||
return (E_literal (Literal_int n))
|
||||
| T_constant ("string", []) ->
|
||||
let%bind n = get_string v in
|
||||
return (Literal (String n))
|
||||
| Type_constant ("option", [o]) -> (
|
||||
return (E_literal (Literal_string n))
|
||||
| T_constant ("option", [o]) -> (
|
||||
match%bind get_option v with
|
||||
| None -> ok (a_none o)
|
||||
| Some s ->
|
||||
let%bind s' = untranspile s o in
|
||||
ok (a_some s')
|
||||
)
|
||||
| Type_constant ("map", [k_ty;v_ty]) -> (
|
||||
| T_constant ("map", [k_ty;v_ty]) -> (
|
||||
let%bind lst = get_map v in
|
||||
let%bind lst' =
|
||||
let aux = fun (k, v) ->
|
||||
@ -423,11 +423,11 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
|
||||
let%bind v' = untranspile v v_ty in
|
||||
ok (k', v') in
|
||||
bind_map_list aux lst in
|
||||
return (Map lst')
|
||||
return (E_map lst')
|
||||
)
|
||||
| Type_constant _ ->
|
||||
| T_constant _ ->
|
||||
simple_fail "unknown type_constant"
|
||||
| Type_sum m ->
|
||||
| T_sum m ->
|
||||
let lst = kv_list_of_map m in
|
||||
let%bind node = match Append_tree.of_list lst with
|
||||
| Empty -> simple_fail "empty sum type"
|
||||
@ -435,16 +435,16 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
|
||||
in
|
||||
let%bind (name, v, tv) = extract_constructor v node in
|
||||
let%bind sub = untranspile v tv in
|
||||
return (Constructor (name, sub))
|
||||
| Type_tuple lst ->
|
||||
return (E_constructor (name, sub))
|
||||
| T_tuple lst ->
|
||||
let%bind node = match Append_tree.of_list lst with
|
||||
| Empty -> simple_fail "empty tuple"
|
||||
| Full t -> ok t in
|
||||
let%bind tpl = extract_tuple v node in
|
||||
let%bind tpl' = bind_list
|
||||
@@ List.map (fun (x, y) -> untranspile x y) tpl in
|
||||
return (Tuple tpl')
|
||||
| Type_record m ->
|
||||
return (E_tuple tpl')
|
||||
| T_record m ->
|
||||
let lst = kv_list_of_map m in
|
||||
let%bind node = match Append_tree.of_list lst with
|
||||
| Empty -> simple_fail "empty record"
|
||||
@ -453,5 +453,5 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
|
||||
let%bind lst = bind_list
|
||||
@@ List.map (fun (x, (y, z)) -> let%bind yz = untranspile y z in ok (x, yz)) lst in
|
||||
let m' = map_of_kv_list lst in
|
||||
return (Record m')
|
||||
| Type_function _ -> simple_fail "no untranspilation for functions yet"
|
||||
return (E_record m')
|
||||
| T_function _ -> simple_fail "no untranspilation for functions yet"
|
||||
|
||||
@ -24,7 +24,7 @@ module Environment = struct
|
||||
let get_constructor (e:t) (s:string) : (ele * ele) option =
|
||||
let rec aux = function
|
||||
| [] -> None
|
||||
| (_, (O.{type_value=(O.Type_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
|
||||
| (_, (O.{type_value=(O.T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
|
||||
| _ :: tl -> aux tl
|
||||
in
|
||||
aux e.environment
|
||||
@ -117,7 +117,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
|
||||
trace (constant_declaration_error name annotated_expression) @@
|
||||
type_annotated_expression env annotated_expression in
|
||||
let env' = Environment.add env name ae'.type_annotation in
|
||||
ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'}))
|
||||
ok (env', Some (O.Declaration_constant {name;annotated_expression=ae'}))
|
||||
|
||||
and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
|
||||
let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
|
||||
@ -132,40 +132,40 @@ and type_block (e:environment) (b:I.block) : O.block result =
|
||||
ok block
|
||||
|
||||
and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function
|
||||
| I_skip -> ok (e, O.Skip)
|
||||
| I_skip -> ok (e, O.I_skip)
|
||||
| I_fail x ->
|
||||
let%bind expression = type_annotated_expression e x in
|
||||
ok (e, O.Fail expression)
|
||||
ok (e, O.I_fail expression)
|
||||
| I_loop (cond, body) ->
|
||||
let%bind cond = type_annotated_expression e cond in
|
||||
let%bind _ =
|
||||
O.assert_type_value_eq (cond.type_annotation, make_t_bool) in
|
||||
let%bind body = type_block e body in
|
||||
ok (e, O.Loop (cond, body))
|
||||
ok (e, O.I_loop (cond, body))
|
||||
| I_assignment {name;annotated_expression} -> (
|
||||
match annotated_expression.type_annotation, Environment.get e name with
|
||||
| None, None -> simple_fail "Initial assignments need type"
|
||||
| Some _, None ->
|
||||
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
||||
let e' = Environment.add e name annotated_expression.type_annotation in
|
||||
ok (e', O.Assignment {name;annotated_expression})
|
||||
ok (e', O.I_assignment {name;annotated_expression})
|
||||
| None, Some prev ->
|
||||
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
||||
let e' = Environment.add e name annotated_expression.type_annotation in
|
||||
let%bind _ =
|
||||
O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
|
||||
ok (e', O.Assignment {name;annotated_expression})
|
||||
ok (e', O.I_assignment {name;annotated_expression})
|
||||
| Some _, Some prev ->
|
||||
let%bind annotated_expression = type_annotated_expression e annotated_expression in
|
||||
let%bind _assert = trace (simple_error "Annotation doesn't match environment")
|
||||
@@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
|
||||
let e' = Environment.add e name annotated_expression.type_annotation in
|
||||
ok (e', O.Assignment {name;annotated_expression})
|
||||
ok (e', O.I_assignment {name;annotated_expression})
|
||||
)
|
||||
| I_matching (ex, m) ->
|
||||
let%bind ex' = type_annotated_expression e ex in
|
||||
let%bind m' = type_match type_block e ex'.type_annotation m in
|
||||
ok (e, O.Matching_instr (ex', m'))
|
||||
ok (e, O.I_matching (ex', m'))
|
||||
| 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 =
|
||||
@ -215,10 +215,10 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
|
||||
| T_function (a, b) ->
|
||||
let%bind a' = evaluate_type e a in
|
||||
let%bind b' = evaluate_type e b in
|
||||
return (Type_function (a', b'))
|
||||
return (T_function (a', b'))
|
||||
| T_tuple lst ->
|
||||
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
|
||||
return (Type_tuple lst')
|
||||
return (T_tuple lst')
|
||||
| T_sum m ->
|
||||
let aux k v prev =
|
||||
let%bind prev' = prev in
|
||||
@ -226,7 +226,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
|
||||
ok @@ SMap.add k v' prev'
|
||||
in
|
||||
let%bind m = SMap.fold aux m (ok SMap.empty) in
|
||||
return (Type_sum m)
|
||||
return (T_sum m)
|
||||
| T_record m ->
|
||||
let aux k v prev =
|
||||
let%bind prev' = prev in
|
||||
@ -234,7 +234,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
|
||||
ok @@ SMap.add k v' prev'
|
||||
in
|
||||
let%bind m = SMap.fold aux m (ok SMap.empty) in
|
||||
return (Type_record m)
|
||||
return (T_record m)
|
||||
| T_variable name ->
|
||||
let%bind tv =
|
||||
trace_option (unbound_type_variable e name)
|
||||
@ -242,7 +242,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
|
||||
ok tv
|
||||
| T_constant (cst, lst) ->
|
||||
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
|
||||
return (Type_constant(cst, lst'))
|
||||
return (T_constant(cst, lst'))
|
||||
|
||||
and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.annotated_expression result =
|
||||
let%bind tv_opt = match ae.type_annotation with
|
||||
@ -256,28 +256,28 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
trace_option (unbound_variable e name)
|
||||
@@ Environment.get e name in
|
||||
let%bind type_annotation = check tv' in
|
||||
ok O.{expression = Variable name ; type_annotation}
|
||||
ok O.{expression = E_variable name ; type_annotation}
|
||||
| E_literal (Literal_bool b) ->
|
||||
let%bind type_annotation = check make_t_bool in
|
||||
ok O.{expression = Literal (Bool b) ; type_annotation }
|
||||
ok O.{expression = E_literal (Literal_bool b) ; type_annotation }
|
||||
| E_literal Literal_unit ->
|
||||
let%bind type_annotation = check make_t_unit in
|
||||
ok O.{expression = Literal (Unit) ; type_annotation }
|
||||
ok O.{expression = E_literal (Literal_unit) ; type_annotation }
|
||||
| E_literal (Literal_string s) ->
|
||||
let%bind type_annotation = check make_t_string in
|
||||
ok O.{expression = Literal (String s) ; type_annotation }
|
||||
ok O.{expression = E_literal (Literal_string s) ; type_annotation }
|
||||
| E_literal (Literal_bytes s) ->
|
||||
let%bind type_annotation = check make_t_bytes in
|
||||
ok O.{expression = Literal (Bytes s) ; type_annotation }
|
||||
ok O.{expression = E_literal (Literal_bytes s) ; type_annotation }
|
||||
| E_literal (Literal_number n) ->
|
||||
let%bind type_annotation = check make_t_int in
|
||||
ok O.{expression = Literal (Int n) ; type_annotation }
|
||||
ok O.{expression = E_literal (Literal_int n) ; type_annotation }
|
||||
(* Tuple *)
|
||||
| E_tuple lst ->
|
||||
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
|
||||
let tv_lst = List.map get_annotation lst' in
|
||||
let%bind type_annotation = check (make_t_tuple tv_lst) in
|
||||
ok O.{expression = Tuple lst' ; type_annotation }
|
||||
ok O.{expression = E_tuple lst' ; type_annotation }
|
||||
| E_accessor (ae, path) ->
|
||||
let%bind e' = type_annotated_expression e ae in
|
||||
let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
|
||||
@ -288,7 +288,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
generic_try (simple_error "bad tuple index")
|
||||
@@ (fun () -> List.nth tpl_tv index) in
|
||||
let%bind type_annotation = check tv in
|
||||
ok O.{expression = O.Tuple_accessor (prev, index) ; type_annotation}
|
||||
ok O.{expression = O.E_tuple_accessor (prev, index) ; type_annotation}
|
||||
)
|
||||
| Access_record property -> (
|
||||
let%bind r_tv = get_t_record prev.type_annotation in
|
||||
@ -296,7 +296,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
generic_try (simple_error "bad record index")
|
||||
@@ (fun () -> SMap.find property r_tv) in
|
||||
let%bind type_annotation = check tv in
|
||||
ok O.{expression = O.Record_accessor (prev, property) ; type_annotation }
|
||||
ok O.{expression = O.E_record_accessor (prev, property) ; type_annotation }
|
||||
)
|
||||
in
|
||||
trace (simple_error "accessing") @@
|
||||
@ -310,7 +310,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
let%bind expr' = type_annotated_expression e expr in
|
||||
let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
|
||||
let%bind type_annotation = check sum_tv in
|
||||
ok O.{expression = O.Constructor(c, expr') ; type_annotation }
|
||||
ok O.{expression = O.E_constructor(c, expr') ; type_annotation }
|
||||
(* Record *)
|
||||
| E_record m ->
|
||||
let aux prev k expr =
|
||||
@ -319,7 +319,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
in
|
||||
let%bind m' = bind_fold_smap aux (ok SMap.empty) 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.E_record m' ; type_annotation }
|
||||
(* Data-structure *)
|
||||
| E_map lst ->
|
||||
let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in
|
||||
@ -346,7 +346,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
in
|
||||
check (make_t_map key_type value_type)
|
||||
in
|
||||
ok O.{expression = O.Map lst' ; type_annotation}
|
||||
ok O.{expression = O.E_map lst' ; type_annotation}
|
||||
| E_lambda {
|
||||
binder ;
|
||||
input_type ;
|
||||
@ -360,30 +360,30 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
let%bind (body, e'') = type_block_full e' body in
|
||||
let%bind result = type_annotated_expression e'' result 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 = E_lambda {binder;input_type;output_type;result;body} ; type_annotation}
|
||||
| E_constant (name, lst) ->
|
||||
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) 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 type_annotation = check tv in
|
||||
ok O.{expression = O.Constant (name', lst') ; type_annotation}
|
||||
ok O.{expression = O.E_constant (name', lst') ; type_annotation}
|
||||
| E_application (f, arg) ->
|
||||
let%bind f = type_annotated_expression e f in
|
||||
let%bind arg = type_annotated_expression e arg in
|
||||
let%bind type_annotation = match f.type_annotation.type_value with
|
||||
| Type_function (param, result) ->
|
||||
| T_function (param, result) ->
|
||||
let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
|
||||
ok result
|
||||
| _ -> simple_fail "applying to not-a-function"
|
||||
in
|
||||
ok O.{expression = Application (f, arg) ; type_annotation}
|
||||
ok O.{expression = E_application (f, arg) ; type_annotation}
|
||||
| E_look_up dsi ->
|
||||
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 _ = O.assert_type_value_eq (ind.type_annotation, src) in
|
||||
let dst_opt = make_t_option dst in
|
||||
let%bind type_annotation = check dst_opt in
|
||||
ok O.{expression = LookUp (ds, ind) ; type_annotation}
|
||||
ok O.{expression = E_look_up (ds, ind) ; type_annotation}
|
||||
(* Advanced *)
|
||||
| E_matching (ex, m) -> (
|
||||
let%bind ex' = type_annotated_expression e ex in
|
||||
@ -393,7 +393,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
let%bind _ = O.assert_type_value_eq (match_true.type_annotation, match_false.type_annotation) in
|
||||
ok match_true.type_annotation
|
||||
| _ -> simple_fail "can only type match_bool expressions yet" in
|
||||
ok O.{expression = Matching_expr (ex', m') ; type_annotation}
|
||||
ok O.{expression = E_matching (ex', m') ; type_annotation}
|
||||
)
|
||||
|
||||
and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =
|
||||
@ -433,61 +433,61 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
|
||||
let untype_literal (l:O.literal) : I.literal result =
|
||||
let open I in
|
||||
match l with
|
||||
| Unit -> ok Literal_unit
|
||||
| Bool b -> ok (Literal_bool b)
|
||||
| Nat n -> ok (Literal_number n)
|
||||
| Int n -> ok (Literal_number n)
|
||||
| String s -> ok (Literal_string s)
|
||||
| Bytes b -> ok (Literal_bytes b)
|
||||
| Literal_unit -> ok Literal_unit
|
||||
| Literal_bool b -> ok (Literal_bool b)
|
||||
| Literal_nat n -> ok (Literal_number n)
|
||||
| Literal_int n -> ok (Literal_number n)
|
||||
| Literal_string s -> ok (Literal_string s)
|
||||
| Literal_bytes b -> ok (Literal_bytes b)
|
||||
|
||||
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
|
||||
match e.expression with
|
||||
| Literal l ->
|
||||
| E_literal l ->
|
||||
let%bind l = untype_literal l in
|
||||
return (E_literal l)
|
||||
| Constant (n, lst) ->
|
||||
| E_constant (n, lst) ->
|
||||
let%bind lst' = bind_list
|
||||
@@ List.map untype_annotated_expression lst in
|
||||
return (E_constant (n, lst'))
|
||||
| Variable n ->
|
||||
| E_variable n ->
|
||||
return (E_variable n)
|
||||
| Application (f, arg) ->
|
||||
| E_application (f, arg) ->
|
||||
let%bind f' = untype_annotated_expression f in
|
||||
let%bind arg' = untype_annotated_expression arg in
|
||||
return (E_application (f', arg'))
|
||||
| Lambda {binder;input_type;output_type;body;result} ->
|
||||
| E_lambda {binder;input_type;output_type;body;result} ->
|
||||
let%bind input_type = untype_type_value input_type in
|
||||
let%bind output_type = untype_type_value output_type in
|
||||
let%bind result = untype_annotated_expression result in
|
||||
let%bind body = untype_block body in
|
||||
return (E_lambda {binder;input_type;output_type;body;result})
|
||||
| Tuple lst ->
|
||||
| E_tuple lst ->
|
||||
let%bind lst' = bind_list
|
||||
@@ List.map untype_annotated_expression lst in
|
||||
return (E_tuple lst')
|
||||
| Tuple_accessor (tpl, ind) ->
|
||||
| E_tuple_accessor (tpl, ind) ->
|
||||
let%bind tpl' = untype_annotated_expression tpl in
|
||||
return (E_accessor (tpl', [Access_tuple ind]))
|
||||
| Constructor (n, p) ->
|
||||
| E_constructor (n, p) ->
|
||||
let%bind p' = untype_annotated_expression p in
|
||||
return (E_constructor (n, p'))
|
||||
| Record r ->
|
||||
| E_record r ->
|
||||
let%bind r' = bind_smap
|
||||
@@ SMap.map untype_annotated_expression r in
|
||||
return (E_record r')
|
||||
| Record_accessor (r, s) ->
|
||||
| E_record_accessor (r, s) ->
|
||||
let%bind r' = untype_annotated_expression r in
|
||||
return (E_accessor (r', [Access_record s]))
|
||||
| Map m ->
|
||||
| E_map m ->
|
||||
let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
|
||||
return (E_map m')
|
||||
| LookUp dsi ->
|
||||
| E_look_up dsi ->
|
||||
let%bind dsi' = bind_map_pair untype_annotated_expression dsi in
|
||||
return (E_look_up dsi')
|
||||
| Matching_expr (ae, m) ->
|
||||
| E_matching (ae, m) ->
|
||||
let%bind ae' = untype_annotated_expression ae in
|
||||
let%bind m' = untype_matching untype_annotated_expression m in
|
||||
return (E_matching (ae', m'))
|
||||
@ -498,18 +498,18 @@ and untype_block (b:O.block) : (I.block) result =
|
||||
and untype_instruction (i:O.instruction) : (I.instruction) result =
|
||||
let open I in
|
||||
match i with
|
||||
| Skip -> ok I_skip
|
||||
| Fail e ->
|
||||
| I_skip -> ok I_skip
|
||||
| I_fail e ->
|
||||
let%bind e' = untype_annotated_expression e in
|
||||
ok (I_fail e')
|
||||
| Loop (e, b) ->
|
||||
| I_loop (e, b) ->
|
||||
let%bind e' = untype_annotated_expression e in
|
||||
let%bind b' = untype_block b in
|
||||
ok @@ I_loop (e', b')
|
||||
| Assignment a ->
|
||||
| I_assignment a ->
|
||||
let%bind annotated_expression = untype_annotated_expression a.annotated_expression in
|
||||
ok @@ I_assignment {name = a.name ; annotated_expression}
|
||||
| Matching_instr (e, m) ->
|
||||
| I_matching (e, m) ->
|
||||
let%bind e' = untype_annotated_expression e in
|
||||
let%bind m' = untype_matching untype_block m in
|
||||
ok @@ I_matching (e', m')
|
||||
|
||||
Loading…
Reference in New Issue
Block a user