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

WIP on understanding where in the AST we need the subst.

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-10-31 13:21:05 -04:00
parent 770bdda9df
commit dce15a79c6
2 changed files with 70 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/stages/ast_typed/types.ml
View File

@ -24,18 +24,18 @@ and environment_element_definition =
and free_variables = name list
and environment_element = {
type_value : type_value ;
type_value : type_value ; (* SUBST ??? *)
source_environment : full_environment ;
definition : environment_element_definition ;
}
and environment = (string * environment_element) list
and type_environment = (string * type_value) list
and type_environment = (string * type_value) list (* SUBST ??? *)
and small_environment = (environment * type_environment)
and full_environment = small_environment List.Ne.t
and annotated_expression = {
expression : expression ;
type_annotation : tv ;
type_annotation : tv ; (* SUBST *)
environment : full_environment ;
location : Location.t ;
}
@ -54,20 +54,24 @@ and type_value' =
| T_tuple of tv list
| T_sum of tv_map
| T_record of tv_map
| T_constant of type_name * tv list
| T_variable of type_name
| T_constant of type_name * tv list (* SUBST ??? I think not, at least not necessary for now and the types don't match *)
| T_variable of type_name (* SUBST *)
| T_function of (tv * tv)
and type_value = {
type_value' : type_value' ;
simplified : S.type_expression option ;
simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *)
}
(* This is used in E_assign of (named_type_value * access_path * ae).
In mini_c, we need the type associated with `x` in the assignment
expression `x.y.z := 42`, so it is stored here. *)
and named_type_value = {
type_name: name ;
type_value : type_value ;
}
(* E_lamba and other expressions are always wrapped as an annotated_expression. *)
and lambda = {
binder : name ;
(* input_type: tv ;

84
src/stages/typesystem/misc.ml
View File

@ -3,7 +3,6 @@ open Core
let pair_map = fun f (x , y) -> (f x , f y)
module Substitution = struct
(* Replace Types variables by the infered type *)
module Pattern = struct
@ -29,9 +28,11 @@ module Substitution = struct
let%bind definition = s_environment_element_definition ~v ~expr definition in
ok @@ (type_variable, T.{ type_value; source_environment; definition })
) lst
and s_type_environment ~v ~expr : T.type_environment w = fun _ ->
let _TODO = (v, expr) in
failwith "TODO: subst: unimplemented case s_type_environment"
and s_type_environment ~v ~expr : T.type_environment w = fun tenv ->
bind_map_list (fun (type_variable , type_value) ->
let%bind type_variable = s_type_variable ~v ~expr type_variable in
let%bind type_value = s_type_value ~v ~expr type_value in
ok @@ (type_variable , type_value)) tenv
and s_small_environment ~v ~expr : T.small_environment w = fun (environment, type_environment) ->
let%bind environment = s_environment ~v ~expr environment in
let%bind type_environment = s_type_environment ~v ~expr type_environment in
@ -46,27 +47,62 @@ module Substitution = struct
ok var
and s_type_variable ~v ~expr : T.name w = fun tvar ->
let _TODO = ignore (v, expr, tvar) in
failwith "TODO: subst: unimplemented case s_type_variable"
(* if String.equal tvar v then
* expr
* else
* ok tvar *)
let _TODO = ignore (v, expr) in
Printf.printf "TODO: subst: unimplemented case s_type_variable";
ok @@ tvar
(* if String.equal tvar v then
* expr
* else
* ok tvar *)
and s_type_value' ~v ~expr : T.type_value' w = fun _ ->
let _TODO = (v, expr) in
failwith "TODO: subst: unimplemented case s_type_value'"
and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun _ ->
let _TODO = (v, expr) in
failwith "TODO: subst: unimplemented case s_type_expression"
and s_type_name_constant ~v ~expr : T.type_name w = fun type_name ->
(* TODO: we don't need to subst anything, right? *)
let () = ignore (v , expr) in
ok @@ type_name
and s_type_value' ~v ~expr : T.type_value' w = function
| T.T_tuple type_value_list ->
let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
ok @@ T.T_tuple type_value_list
| T.T_sum _ -> failwith "TODO: T_sum"
| T.T_record _ -> failwith "TODO: T_record"
| T.T_constant (type_name, type_value_list) ->
let%bind type_name = s_type_name_constant ~v ~expr type_name in
let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
ok @@ T.T_constant (type_name, type_value_list)
| T.T_variable _ -> failwith "TODO: T_variable"
| T.T_function _ ->
let _TODO = (v, expr) in
failwith "TODO: T_function"
and s_type_expression ~v ~expr : Ast_simplified.type_expression w = function
| Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression"
| Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression"
| Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression"
| Ast_simplified.T_function (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression"
| Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression"
| Ast_simplified.T_constant (_, _) ->
let _TODO = (v, expr) in
failwith "TODO: subst: unimplemented case s_type_expression"
and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } ->
let%bind type_value' = s_type_value' ~v ~expr type_value' in
let%bind simplified = bind_map_option (s_type_expression ~v ~expr) simplified in
ok @@ T.{ type_value'; simplified }
and s_literal ~v ~expr : T.literal w = fun _ ->
let _TODO = v, expr in
failwith "TODO: subst: unimplemented case s_literal"
and s_literal ~v ~expr : T.literal w = function
| T.Literal_unit ->
let () = ignore (v, expr) in
ok @@ T.Literal_unit
| (T.Literal_bool _ as x)
| (T.Literal_int _ as x)
| (T.Literal_nat _ as x)
| (T.Literal_timestamp _ as x)
| (T.Literal_mutez _ as x)
| (T.Literal_string _ as x)
| (T.Literal_bytes _ as x)
| (T.Literal_address _ as x)
| (T.Literal_operation _ as x) ->
ok @@ x
and s_matching_expr ~v ~expr : T.matching_expr w = fun _ ->
let _TODO = v, expr in
failwith "TODO: subst: unimplemented case s_matching"
@ -115,11 +151,11 @@ module Substitution = struct
| T.E_record aemap ->
let _TODO = aemap in
failwith "TODO: subst in record"
(* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
* let key = s_type_variable ~v ~expr key in
* let val_ = s_annotated_expression ~v ~expr val_ in
* ok @@ (key , val_)) aemap in
* ok @@ T.E_record aemap *)
(* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
* let key = s_type_variable ~v ~expr key in
* let val_ = s_annotated_expression ~v ~expr val_ in
* ok @@ (key , val_)) aemap in
* ok @@ T.E_record aemap *)
| T.E_record_accessor (val_, tvar) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind tvar = s_type_variable ~v ~expr tvar in