balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

rewrite type environments

Browse Source
This commit is contained in:
Galfour 2019-04-21 09:03:50 +00:00
parent af6da6bfa0
commit c2ac9ab361
7 changed files with 104 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/lib_utils/tezos_utils.ml
View File

@ -22,3 +22,4 @@ module Dictionary = Dictionary
module Tree = Tree
module Region = Region
module Pos = Pos

7
src/lib_utils/x_list.ml
View File

@ -97,9 +97,12 @@ module Ne = struct
let of_list lst = List.(hd lst, tl lst)
let to_list (hd, tl : _ t) = hd :: tl
let singleton hd : 'a t = hd , []
let hd : 'a t -> 'a = fst
let cons : 'a -> 'a t -> 'a t = fun hd' (hd , tl) -> hd' , hd :: tl
let iter f (hd, tl : _ t) = f hd ; List.iter f tl
let map f (hd, tl : _ t) = f hd, List.map f tl
let hd_map : _ -> 'a t -> 'a t = fun f (hd , tl) -> (f hd , tl)
let mapi f (hd, tl : _ t) =
let lst = List.mapi f (hd::tl) in
of_list lst
@ -110,5 +113,9 @@ module Ne = struct
| lst ->
let r = List.rev lst in
(List.hd r, List.tl r @ [hd])
let find_map = fun f (hd , tl : _ t) ->
match f hd with
| Some x -> Some x
| None -> find_map f tl
end

31
src/ligo/ast_typed/combinators.ml
View File

@ -3,6 +3,7 @@ open Types
let make_t type_value' simplified = { type_value' ; simplified }
let make_a_e expression type_annotation environment = { expression ; type_annotation ; dummy_field = () ; environment }
let make_a_e_empty expression type_annotation = make_a_e expression type_annotation Environment.full_empty
let make_n_e name a_e = { name ; annotated_expression = a_e }
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
@ -116,19 +117,19 @@ let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y
let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ())
let e_a_list lst t = make_a_e (e_list lst) (t_list t ())
let e_a_empty_unit = e_a_unit Environment.empty
let e_a_empty_int n = e_a_int n Environment.empty
let e_a_empty_nat n = e_a_nat n Environment.empty
let e_a_empty_bool b = e_a_bool b Environment.empty
let e_a_empty_string s = e_a_string s Environment.empty
let e_a_empty_pair a b = e_a_pair a b Environment.empty
let e_a_empty_some s = e_a_some s Environment.empty
let e_a_empty_none t = e_a_none t Environment.empty
let e_a_empty_tuple lst = e_a_tuple lst Environment.empty
let e_a_empty_record r = e_a_record r Environment.empty
let e_a_empty_map lst k v = e_a_map lst k v Environment.empty
let e_a_empty_list lst t = e_a_list lst t Environment.empty
let ez_e_a_empty_record r = ez_e_a_record r Environment.empty
let e_a_empty_unit = e_a_unit Environment.full_empty
let e_a_empty_int n = e_a_int n Environment.full_empty
let e_a_empty_nat n = e_a_nat n Environment.full_empty
let e_a_empty_bool b = e_a_bool b Environment.full_empty
let e_a_empty_string s = e_a_string s Environment.full_empty
let e_a_empty_pair a b = e_a_pair a b Environment.full_empty
let e_a_empty_some s = e_a_some s Environment.full_empty
let e_a_empty_none t = e_a_none t Environment.full_empty
let e_a_empty_tuple lst = e_a_tuple lst Environment.full_empty
let e_a_empty_record r = e_a_record r Environment.full_empty
let e_a_empty_map lst k v = e_a_map lst k v Environment.full_empty
let e_a_empty_list lst t = e_a_list lst t Environment.full_empty
let ez_e_a_empty_record r = ez_e_a_record r Environment.full_empty
let get_a_int (t:annotated_expression) =
match t.expression with
@ -148,6 +149,6 @@ let get_a_bool (t:annotated_expression) =
open Environment
let env_sum_type ?(env = full_empty)
?(name = "a_sum_type")
(lst : (string * ele) list) =
add env name (make_t_ez_sum lst)
(lst : (string * element) list) =
add_type name (make_t_ez_sum lst) env

81
src/ligo/ast_typed/environment.ml
View File

@ -1,49 +1,64 @@
open Types
type ele = type_value
type element = type_value
module Small = struct
type t = small_environment
let empty : t = ([] , [])
let get_environment : t -> environment = fst
let get_type_environment : t -> type_environment = snd
let map_environment : _ -> t -> t = fun f (a , b) -> (f a , b)
let map_type_environment : _ -> t -> t = fun f (a , b) -> (a , f b)
let add : string -> element -> t -> t = fun k v -> map_environment (fun x -> (k , v) :: x)
let add_type : string -> element -> t -> t = fun k v -> map_type_environment (fun x -> (k , v) :: x)
let get_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_environment x)
let get_type_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_type_environment x)
end
type t = full_environment
let empty : environment = Small.(get_environment empty)
let full_empty : t = List.Ne.singleton Small.empty
let add : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add k v)
let add_type : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type k v)
let get_opt : string -> t -> element option = fun k x -> List.Ne.find_map (Small.get_opt k) x
let get_type_opt : string -> t -> element option = fun k x -> List.Ne.find_map (Small.get_type_opt k) x
let empty = []
let full_empty : t = {
(* TODO: use maps *)
environment = [] ;
type_environment = [] ;
}
let dummy : environment = []
let get (e:t) (s:string) : ele option =
List.assoc_opt s e.environment
let get_constructor (e:t) (s:string) : (ele * ele) option =
let rec aux = function
| [] -> None
| (_, ({type_value'=(T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
| _ :: tl -> aux tl
let get_constructor : string -> t -> (element * element) option = fun k x -> (* Left is the constructor, right is the sum type *)
let aux = fun x ->
let aux = fun (_type_name , x) ->
match x.type_value' with
| T_sum m when Map.String.mem k m -> Some (Map.String.find k m , x)
| _ -> None
in
aux e.environment
List.find_map aux (Small.get_type_environment x) in
List.Ne.find_map aux x
let add (e:t) (s:string) (tv:ele) : t =
{e with environment = (s, tv) :: e.environment}
let get_type (e:t) (s:string) : ele option =
List.assoc_opt s e.type_environment
let add_type (e:t) (s:string) (tv:ele) : t =
{e with type_environment = (s, tv) :: e.type_environment}
module PP = struct
open Format
open PP_helpers
let list_sep_d x = list_sep x (const " , ")
let list_sep_scope x = list_sep x (const " | ")
let value ppf (e:t) =
let pp ppf (s, e) = fprintf ppf "%s -> %a" s PP.type_value e in
fprintf ppf "ValueEnv[%a]" (list_sep_d pp) e.environment
let assoc = fun ppf (k , tv) ->
fprintf ppf "%s -> %a" k PP.type_value tv
let type_ ppf e =
let pp ppf (s, e) = fprintf ppf "%s -> %a" s PP.type_value e in
fprintf ppf "TypeEnv[%a]" (list_sep_d pp) e.type_environment
let environment : _ -> environment -> unit = fun ppf lst ->
fprintf ppf "E[%a]" (list_sep assoc (const " , ")) lst
let full ppf e =
fprintf ppf "%a\n%a" value e type_ e
let type_environment = fun ppf lst ->
fprintf ppf "T[%a]" (list_sep assoc (const " , ")) lst
let small_environment : _ -> small_environment -> unit = fun ppf e ->
fprintf ppf "- %a\t%a"
environment (Small.get_environment e)
type_environment (Small.get_type_environment e)
let full_environment : _ -> full_environment -> unit = fun ppf e ->
fprintf ppf "@[%a]"
(ne_list_sep small_environment (tag "@;")) e
end

8
src/ligo/ast_typed/types.ml
View File

@ -18,15 +18,13 @@ and declaration =
and environment = (string * type_value) list
and type_environment = (string * type_value) list
and full_environment = {
environment : environment ;
type_environment : type_environment ;
}
and small_environment = (environment * type_environment)
and full_environment = small_environment List.Ne.t
and annotated_expression = {
expression: expression ;
type_annotation: tv ;
environment: environment ;
environment: full_environment ;
dummy_field: unit ;
}

6
src/ligo/transpiler.ml
View File

@ -489,7 +489,7 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result =
let open! AST in
let return e = ok (make_a_e e t Environment.empty) in
let return e = ok (make_a_e_empty e t) in
match t.type_value' with
| T_constant ("unit", []) ->
let%bind () = get_unit v in
@ -508,10 +508,10 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
return (E_literal (Literal_string n))
| T_constant ("option", [o]) -> (
match%bind get_option v with
| None -> ok (e_a_none o Environment.empty)
| None -> ok (e_a_empty_none o)
| Some s ->
let%bind s' = untranspile s o in
ok (e_a_some s' Environment.empty)
ok (e_a_empty_some s')
)
| T_constant ("map", [k_ty;v_ty]) -> (
let%bind lst = get_map v in

43
src/ligo/typer.ml
View File

@ -13,12 +13,12 @@ type environment = Environment.t
module Errors = struct
let unbound_type_variable (e:environment) (n:string) () =
let title = (thunk "unbound type variable") in
let full () = Format.asprintf "%s in %a" n Environment.PP.type_ e in
let full () = Format.asprintf "%s in %a" n Environment.PP.full_environment e in
error title full ()
let unbound_variable (e:environment) (n:string) () =
let title = (thunk "unbound variable") in
let full () = Format.asprintf "%s in %a" n Environment.PP.value e in
let full () = Format.asprintf "%s in %a" n Environment.PP.full_environment e in
error title full ()
let unrecognized_constant (n:string) () =
@ -67,13 +67,13 @@ let rec type_program (p:I.program) : O.program result =
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
| Declaration_type {type_name;type_expression} ->
let%bind tv = evaluate_type env type_expression in
let env' = Environment.add_type env type_name tv in
let env' = Environment.add_type type_name tv env in
ok (env', None)
| Declaration_constant {name;annotated_expression} ->
let%bind ae' =
trace (constant_declaration_error name annotated_expression) @@
type_annotated_expression env annotated_expression in
let env' = Environment.add env name ae'.type_annotation in
let env' = Environment.add name ae'.type_annotation env in
ok (env', Some (O.Declaration_constant (make_n_e name ae')))
and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
@ -102,11 +102,11 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
let%bind body = type_block e body in
return @@ O.I_loop (cond, body)
| I_assignment {name;annotated_expression} -> (
match annotated_expression.type_annotation, Environment.get e name with
match annotated_expression.type_annotation, Environment.get_opt name e with
| None, None -> simple_fail "Initial assignments need type annotation"
| Some _, None ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in
let e' = Environment.add e name annotated_expression.type_annotation in
let e' = Environment.add name annotated_expression.type_annotation e in
ok (e', [O.I_declaration (make_n_e name annotated_expression)])
| None, Some prev ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in
@ -117,7 +117,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
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
let e' = Environment.add name annotated_expression.type_annotation e in
ok (e', [O.I_assignment (make_n_e name annotated_expression)])
)
| I_matching (ex, m) ->
@ -129,7 +129,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
let%bind ae' = type_annotated_expression e ae in
let%bind ty =
trace_option (simple_error "unbound variable in record_patch") @@
Environment.get e r in
Environment.get_opt r e in
let tv = O.{type_name = r ; type_value = ty} in
let aux ty access =
match access with
@ -165,7 +165,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
let%bind match_none = f e match_none in
let (n, b) = match_some in
let n' = n, t_opt in
let e' = Environment.add e n t_opt in
let e' = Environment.add n t_opt e in
let%bind b' = f e' b in
ok (O.Match_option {match_none ; match_some = (n', b')})
| Match_list {match_nil ; match_cons} ->
@ -174,8 +174,8 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
@@ get_t_list t in
let%bind match_nil = f e match_nil in
let (hd, tl, b) = match_cons in
let e' = Environment.add e hd t_list in
let e' = Environment.add e' tl t in
let e' = Environment.add hd t_list e in
let e' = Environment.add tl t e' in
let%bind b' = f e' b in
ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')})
| Match_tuple (lst, b) ->
@ -185,7 +185,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
let%bind lst' =
generic_try (simple_error "Matching tuple of different size")
@@ (fun () -> List.combine lst t_tuple) in
let aux prev (name, tv) = Environment.add prev name tv in
let aux prev (name, tv) = Environment.add name tv prev in
let e' = List.fold_left aux e lst' in
let%bind b' = f e' b in
ok (O.Match_tuple (lst, b'))
@ -219,7 +219,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
| T_variable name ->
let%bind tv =
trace_option (unbound_type_variable e name)
@@ Environment.get_type e name in
@@ Environment.get_type_opt name e in
ok tv
| T_constant (cst, lst) ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
@ -232,13 +232,13 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
let check tv = O.(merge_annotation tv_opt (Some tv)) in
let return expr tv =
let%bind type_annotation = check tv in
ok @@ make_a_e expr type_annotation e.environment in
ok @@ make_a_e expr type_annotation e in
match ae.expression with
(* Basic *)
| E_variable name ->
let%bind tv' =
trace_option (unbound_variable e name)
@@ Environment.get e name in
@@ Environment.get_opt name e in
return (E_variable name) tv'
| E_literal (Literal_bool b) ->
return (E_literal (Literal_bool b)) (t_bool ())
@ -282,8 +282,15 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
(* Sum *)
| E_constructor (c, expr) ->
let%bind (c_tv, sum_tv) =
trace_option (simple_error "no such constructor")
@@ Environment.get_constructor e c in
let error =
let title () = "no such constructor" in
let content () =
Format.asprintf "%s in:\n%a\n"
c O.Environment.PP.full_environment e
in
error title content in
trace_option error @@
Environment.get_constructor c e in
let%bind expr' = type_annotated_expression e expr in
let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
return (E_constructor (c , expr')) sum_tv
@ -352,7 +359,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
} ->
let%bind input_type = evaluate_type e input_type in
let%bind output_type = evaluate_type e output_type in
let e' = Environment.add e binder input_type in
let e' = Environment.add binder input_type e in
let%bind (body, e'') = type_block_full e' body in
let%bind result = type_annotated_expression e'' result in
return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ())