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

commenting a little bit the typesystem

Browse Source
This commit is contained in:
Pierre-Emmanuel Wulfman 2019-10-30 19:35:26 +01:00
parent c0397f68a0
commit 770bdda9df
3 changed files with 81 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

124
src/stages/typesystem/core.ml
View File

@ -1,68 +1,74 @@
type type_variable = string type type_variable = (*Type_variable *) string
let fresh_type_variable : ?name:string -> unit -> type_variable = (* generate a new type variable and gave it an id *)
let id = ref 0 in let fresh_type_variable : ?name:string -> unit -> type_variable =
let inc () = id := !id + 1 in let id = ref 0 in
fun ?name () -> let inc () = id := !id + 1 in
inc () ; fun ?name () ->
match name with inc () ;
| None -> "type_variable_" ^ (string_of_int !id) match name with
| Some name -> "tv_" ^ name ^ "_" ^ (string_of_int !id) | None -> (*Type_variable*) "type_variable_" ^ (string_of_int !id)
| Some name -> (*Type_variable*)"tv_" ^ name ^ "_" ^ (string_of_int !id)
type constant_tag = (* add information on the type or the kind for operator*)
| C_arrow (* * -> * -> * *) type constant_tag =
| C_option (* * -> * *) | C_arrow (* * -> * -> * *) (* isn't this wrong*)
| C_tuple (* * … -> * *) | C_option (* * -> * *)
| C_record (* ( label , * ) … -> * *) | C_tuple (* * … -> * *)
| C_variant (* ( label , * ) … -> * *) | C_record (* ( label , * ) … -> * *)
| C_map (* * -> * -> * *) | C_variant (* ( label , * ) … -> * *)
| C_big_map (* * -> * -> * *) | C_map (* * -> * -> * *)
| C_list (* * -> * *) | C_big_map (* * -> * -> * *)
| C_set (* * -> * *) | C_list (* * -> * *)
| C_unit (* * *) | C_set (* * -> * *)
| C_bool (* * *) | C_unit (* * *)
| C_string (* * *) | C_bool (* * *)
| C_nat (* * *) | C_string (* * *)
| C_tez (* * *) | C_nat (* * *)
| C_timestamp (* * *) | C_tez (* * *)
| C_int (* * *) | C_timestamp (* * *)
| C_address (* * *) | C_int (* * *)
| C_bytes (* * *) | C_address (* * *)
| C_key_hash (* * *) | C_bytes (* * *)
| C_key (* * *) | C_key_hash (* * *)
| C_signature (* * *) | C_key (* * *)
| C_operation (* * *) | C_signature (* * *)
| C_contract (* * -> * *) | C_operation (* * *)
| C_contract (* * -> * *)
type label = type label =
| L_int of int | L_int of int
| L_string of string | L_string of string
type type_value = (* Weird stuff; please explain *)
| P_forall of p_forall type type_value =
| P_variable of type_variable | P_forall of p_forall
| P_constant of (constant_tag * type_value list) | P_variable of type_variable (* how a value can be a variable? *)
| P_apply of (type_value * type_value) | P_constant of (constant_tag * type_value list)
| P_apply of (type_value * type_value)
and p_forall = { and p_forall = {
binder : type_variable ; binder : type_variable ;
constraints : type_constraint list ; constraints : type_constraint list ;
body : type_value body : type_value
} }
and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *) (* Different type of constraint *) (* why isn't this a variant ? *)
and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *) and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *)
and c_const = (type_variable * type_value) and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *)
and c_equation = (type_value * type_value) and c_const = (type_variable * type_value)
and c_typeclass = (type_value list * typeclass) and c_equation = (type_value * type_value)
and c_access_label = (type_value * label * type_variable) and c_typeclass = (type_value list * typeclass)
and c_access_label = (type_value * label * type_variable)
and type_constraint = (*What i was saying just before *)
(* | C_assignment of (type_variable * type_pattern) *) and type_constraint =
| C_equation of c_equation (* TVA = TVB *) (* | C_assignment of (type_variable * type_pattern) *)
| C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *) | C_equation of c_equation (* TVA = TVB *)
| C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *) | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
(* | … *) | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *)
(* | … *)
and typeclass = type_value list list (* is the first list in case on of the type of the type class as a kind *->*->* ? *)
and typeclass = type_value list list

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

@ -3,6 +3,7 @@ open Core
let pair_map = fun f (x , y) -> (f x , f y) let pair_map = fun f (x , y) -> (f x , f y)
module Substitution = struct module Substitution = struct
(* Replace Types variables by the infered type *)
module Pattern = struct module Pattern = struct
@ -14,11 +15,11 @@ module Substitution = struct
let rec rec_yes = true let rec rec_yes = true
and s_environment_element_definition ~v ~expr = function and s_environment_element_definition ~v ~expr = function
| T.ED_binder -> ok @@ T.ED_binder | T.ED_binder -> ok @@ T.ED_binder
| T.ED_declaration (val_, free_variables) -> | T.ED_declaration (val_, free_variables) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind free_variables = bind_map_list (s_type_variable ~v ~expr) free_variables in let%bind free_variables = bind_map_list (s_type_variable ~v ~expr) free_variables in
ok @@ T.ED_declaration (val_, free_variables) ok @@ T.ED_declaration (val_, free_variables)
and s_environment ~v ~expr = fun lst -> and s_environment ~v ~expr = fun lst ->
bind_map_list (fun (type_variable, T.{ type_value; source_environment; definition }) -> bind_map_list (fun (type_variable, T.{ type_value; source_environment; definition }) ->
let _ = type_value in let _ = type_value in
@ -47,10 +48,10 @@ module Substitution = struct
and s_type_variable ~v ~expr : T.name w = fun tvar -> and s_type_variable ~v ~expr : T.name w = fun tvar ->
let _TODO = ignore (v, expr, tvar) in let _TODO = ignore (v, expr, tvar) in
failwith "TODO: subst: unimplemented case s_type_variable" failwith "TODO: subst: unimplemented case s_type_variable"
(* if String.equal tvar v then (* if String.equal tvar v then
* expr * expr
* else * else
* ok tvar *) * ok tvar *)
and s_type_value' ~v ~expr : T.type_value' w = fun _ -> and s_type_value' ~v ~expr : T.type_value' w = fun _ ->
let _TODO = (v, expr) in let _TODO = (v, expr) in
@ -114,11 +115,11 @@ module Substitution = struct
| T.E_record aemap -> | T.E_record aemap ->
let _TODO = aemap in let _TODO = aemap in
failwith "TODO: subst in record" failwith "TODO: subst in record"
(* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ -> (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
* let key = s_type_variable ~v ~expr key in * let key = s_type_variable ~v ~expr key in
* let val_ = s_annotated_expression ~v ~expr val_ in * let val_ = s_annotated_expression ~v ~expr val_ in
* ok @@ (key , val_)) aemap in * ok @@ (key , val_)) aemap in
* ok @@ T.E_record aemap *) * ok @@ T.E_record aemap *)
| T.E_record_accessor (val_, tvar) -> | T.E_record_accessor (val_, tvar) ->
let%bind val_ = s_annotated_expression ~v ~expr val_ in let%bind val_ = s_annotated_expression ~v ~expr val_ in
let%bind tvar = s_type_variable ~v ~expr tvar in let%bind tvar = s_type_variable ~v ~expr tvar in

1
src/stages/typesystem/shorthands.ml
View File

@ -14,6 +14,7 @@ let forall_tc binder f =
let (tc, ty) = f (P_variable freshvar) in let (tc, ty) = f (P_variable freshvar) in
P_forall { binder = freshvar ; constraints = tc ; body = ty } P_forall { binder = freshvar ; constraints = tc ; body = ty }
(* chained forall *)
let forall2 a b f = let forall2 a b f =
forall a @@ fun a' -> forall a @@ fun a' ->
forall b @@ fun b' -> forall b @@ fun b' ->