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

Implemented some missing cases of the subst. First kinda actual typer test passes!

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-11-09 02:45:43 +01:00 committed by Suzanne Dupéron
parent d351d585b0
commit 614970d2d7
7 changed files with 200 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
src/passes/4-typer-new/solver.ml
View File

@ -729,94 +729,98 @@ let compare_simple_c_constant = function
| C_arrow -> (function | C_arrow -> (function
(* N/A -> 1 *) (* N/A -> 1 *)
| C_arrow -> 0 | C_arrow -> 0
| C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_option -> (function | C_option -> (function
| C_arrow -> 1 | C_arrow -> 1
| C_option -> 0 | C_option -> 0
| C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_tuple -> (function | C_tuple -> (function
| C_arrow | C_option -> 1 | C_arrow | C_option -> 1
| C_tuple -> 0 | C_tuple -> 0
| C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_record -> (function | C_record -> (function
| C_arrow | C_option | C_tuple -> 1 | C_arrow | C_option | C_tuple -> 1
| C_record -> 0 | C_record -> 0
| C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_variant -> (function | C_variant -> (function
| C_arrow | C_option | C_tuple | C_record -> 1 | C_arrow | C_option | C_tuple | C_record -> 1
| C_variant -> 0 | C_variant -> 0
| C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_map -> (function | C_map -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant -> 1
| C_map -> 0 | C_map -> 0
| C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_big_map -> (function | C_big_map -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map -> 1
| C_big_map -> 0 | C_big_map -> 0
| C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_list -> (function | C_list -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map -> 1
| C_list -> 0 | C_list -> 0
| C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_set -> (function | C_set -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list -> 1
| C_set -> 0 | C_set -> 0
| C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_unit -> (function | C_unit -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1
| C_unit -> 0 | C_unit -> 0
| C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_bool -> (function | C_bool -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
| C_bool -> 0 | C_bool -> 0
| C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_string -> (function | C_string -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1
| C_string -> 0 | C_string -> 0
| C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_nat -> (function | C_nat -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1
| C_nat -> 0 | C_nat -> 0
| C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_mutez -> (function | C_mutez -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1
| C_mutez -> 0 | C_mutez -> 0
| C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_timestamp -> (function | C_timestamp -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1
| C_timestamp -> 0 | C_timestamp -> 0
| C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_int -> (function | C_int -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1
| C_int -> 0 | C_int -> 0
| C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_address -> (function | C_address -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
| C_address -> 0 | C_address -> 0
| C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_bytes -> (function | C_bytes -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
| C_bytes -> 0 | C_bytes -> 0
| C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key_hash -> (function | C_key_hash -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
| C_key_hash -> 0 | C_key_hash -> 0
| C_key | C_signature | C_operation | C_contract -> -1) | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key -> (function | C_key -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
| C_key -> 0 | C_key -> 0
| C_signature | C_operation | C_contract -> -1) | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_signature -> (function | C_signature -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
| C_signature -> 0 | C_signature -> 0
| C_operation | C_contract -> -1) | C_operation | C_contract | C_chain_id -> -1)
| C_operation -> (function | C_operation -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
| C_operation -> 0 | C_operation -> 0
| C_contract -> -1) | C_contract | C_chain_id -> -1)
| C_contract -> (function | C_contract -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1 | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
| C_contract -> 0 | C_contract -> 0
| C_chain_id -> -1)
| C_chain_id -> (function
| C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
| C_chain_id -> 0
(* N/A -> -1 *) (* N/A -> -1 *)
) )
let rec compare_typeclass a b = compare_list (compare_list compare_type_value) a b let rec compare_typeclass a b = compare_list (compare_list compare_type_value) a b

29
src/passes/4-typer-new/typer.ml
View File

@ -956,12 +956,41 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
(* module TSMap = TMap(Solver.TypeVariable) *) (* module TSMap = TMap(Solver.TypeVariable) *)
(* let c_tag_to_string : Solver.Core.constant_tag -> string = function
* | Solver.Core.C_arrow -> "arrow"
* | Solver.Core.C_option -> "option"
* | Solver.Core.C_tuple -> "tuple"
* | Solver.Core.C_record -> failwith "record"
* | Solver.Core.C_variant -> failwith "variant"
* | Solver.Core.C_map -> "map"
* | Solver.Core.C_big_map -> "big"
* | Solver.Core.C_list -> "list"
* | Solver.Core.C_set -> "set"
* | Solver.Core.C_unit -> "unit"
* | Solver.Core.C_bool -> "bool"
* | Solver.Core.C_string -> "string"
* | Solver.Core.C_nat -> "nat"
* | Solver.Core.C_mutez -> "mutez"
* | Solver.Core.C_timestamp -> "timestamp"
* | Solver.Core.C_int -> "int"
* | Solver.Core.C_address -> "address"
* | Solver.Core.C_bytes -> "bytes"
* | Solver.Core.C_key_hash -> "key_hash"
* | Solver.Core.C_key -> "key"
* | Solver.Core.C_signature -> "signature"
* | Solver.Core.C_operation -> "operation"
* | Solver.Core.C_contract -> "contract"
* | Solver.Core.C_chain_id -> "chain_id" *)
let type_program (p : I.program) : (O.program * Solver.state) result = let type_program (p : I.program) : (O.program * Solver.state) result =
let%bind (env, state, program) = type_program_returns_state p in let%bind (env, state, program) = type_program_returns_state p in
let subst_all = let subst_all =
let assignments = state.structured_dbs.assignments in let assignments = state.structured_dbs.assignments in
let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) = let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) =
let%bind p = p in let%bind p = p in
let Solver.{ tv ; c_tag ; tv_list } = expr in
let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in
let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in
Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in
(* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *) (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *)
let p = Solver.TypeVariableMap.fold aux assignments (ok program) in let p = Solver.TypeVariableMap.fold aux assignments (ok program) in

1
src/stages/ast_typed/misc.ml
View File

@ -1,5 +1,6 @@
open Trace open Trace
open Types open Types
include Stage_common.Misc
module Errors = struct module Errors = struct
let different_kinds a b () = let different_kinds a b () =

1
src/stages/common/ast_common.ml
View File

@ -1,2 +1,3 @@
module Types = Types module Types = Types
module PP = PP module PP = PP
module Misc = Misc

85
src/stages/common/misc.ml Normal file
View File

@ -0,0 +1,85 @@
open Types
open Trace
let map_type_operator f = function
TC_contract x -> TC_contract (f x)
| TC_option x -> TC_option (f x)
| TC_list x -> TC_list (f x)
| TC_set x -> TC_set (f x)
| TC_map (x , y) -> TC_map (f x , f y)
| TC_big_map (x , y)-> TC_big_map (f x , f y)
let bind_map_type_operator f = function
TC_contract x -> let%bind x = f x in ok @@ TC_contract x
| TC_option x -> let%bind x = f x in ok @@ TC_option x
| TC_list x -> let%bind x = f x in ok @@ TC_list x
| TC_set x -> let%bind x = f x in ok @@ TC_set x
| TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y)
| TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
let type_operator_name = function
TC_contract _ -> "TC_contract"
| TC_option _ -> "TC_option"
| TC_list _ -> "TC_list"
| TC_set _ -> "TC_set"
| TC_map _ -> "TC_map"
| TC_big_map _ -> "TC_big_map"
let type_expression'_of_string = function
| "TC_contract" , [x] -> ok @@ T_operator(TC_contract x)
| "TC_option" , [x] -> ok @@ T_operator(TC_option x)
| "TC_list" , [x] -> ok @@ T_operator(TC_list x)
| "TC_set" , [x] -> ok @@ T_operator(TC_set x)
| "TC_map" , [x ; y] -> ok @@ T_operator(TC_map (x , y))
| "TC_big_map" , [x ; y] -> ok @@ T_operator(TC_big_map (x, y))
| ("TC_contract" | "TC_option" | "TC_list" | "TC_set" | "TC_map" | "TC_big_map"), _ ->
failwith "internal error: wrong number of arguments for type operator"
| "TC_unit" , [] -> ok @@ T_constant(TC_unit)
| "TC_string" , [] -> ok @@ T_constant(TC_string)
| "TC_bytes" , [] -> ok @@ T_constant(TC_bytes)
| "TC_nat" , [] -> ok @@ T_constant(TC_nat)
| "TC_int" , [] -> ok @@ T_constant(TC_int)
| "TC_mutez" , [] -> ok @@ T_constant(TC_mutez)
| "TC_bool" , [] -> ok @@ T_constant(TC_bool)
| "TC_operation" , [] -> ok @@ T_constant(TC_operation)
| "TC_address" , [] -> ok @@ T_constant(TC_address)
| "TC_key" , [] -> ok @@ T_constant(TC_key)
| "TC_key_hash" , [] -> ok @@ T_constant(TC_key_hash)
| "TC_chain_id" , [] -> ok @@ T_constant(TC_chain_id)
| "TC_signature" , [] -> ok @@ T_constant(TC_signature)
| "TC_timestamp" , [] -> ok @@ T_constant(TC_timestamp)
| _, [] ->
failwith "internal error: wrong number of arguments for type constant"
| _ ->
failwith "internal error: unknown type operator"
let string_of_type_operator = function
| TC_contract x -> "TC_contract" , [x]
| TC_option x -> "TC_option" , [x]
| TC_list x -> "TC_list" , [x]
| TC_set x -> "TC_set" , [x]
| TC_map (x , y) -> "TC_map" , [x ; y]
| TC_big_map (x , y) -> "TC_big_map" , [x ; y]
let string_of_type_constant = function
| TC_unit -> "TC_unit", []
| TC_string -> "TC_string", []
| TC_bytes -> "TC_bytes", []
| TC_nat -> "TC_nat", []
| TC_int -> "TC_int", []
| TC_mutez -> "TC_mutez", []
| TC_bool -> "TC_bool", []
| TC_operation -> "TC_operation", []
| TC_address -> "TC_address", []
| TC_key -> "TC_key", []
| TC_key_hash -> "TC_key_hash", []
| TC_chain_id -> "TC_chain_id", []
| TC_signature -> "TC_signature", []
| TC_timestamp -> "TC_timestamp", []
let string_of_type_expression' = function
| T_operator o -> string_of_type_operator o
| T_constant c -> string_of_type_constant c
| T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
failwith "not a type operator or constant"

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

@ -31,6 +31,7 @@ type constant_tag =
| C_signature (* * *) | C_signature (* * *)
| C_operation (* * *) | C_operation (* * *)
| C_contract (* * -> * *) | C_contract (* * -> * *)
| C_chain_id (* * *)
type accessor = type accessor =
| L_int of int | L_int of int
@ -67,3 +68,34 @@ and type_constraint =
(* is the first list in case on of the type of the type class as a kind *->*->* ? *) (* is the first list in case on of the type of the type class as a kind *->*->* ? *)
and typeclass = type_value list list and typeclass = type_value list list
open Trace
let type_expression'_of_simple_c_constant = function
| C_contract , [x] -> ok @@ T_operator(TC_contract x)
| C_option , [x] -> ok @@ T_operator(TC_option x)
| C_list , [x] -> ok @@ T_operator(TC_list x)
| C_set , [x] -> ok @@ T_operator(TC_set x)
| C_map , [x ; y] -> ok @@ T_operator(TC_map (x , y))
| C_big_map , [x ; y] -> ok @@ T_operator(TC_big_map (x, y))
| (C_contract | C_option | C_list | C_set | C_map | C_big_map), _ ->
failwith "internal error: wrong number of arguments for type operator"
| C_unit , [] -> ok @@ T_constant(TC_unit)
| C_string , [] -> ok @@ T_constant(TC_string)
| C_bytes , [] -> ok @@ T_constant(TC_bytes)
| C_nat , [] -> ok @@ T_constant(TC_nat)
| C_int , [] -> ok @@ T_constant(TC_int)
| C_mutez , [] -> ok @@ T_constant(TC_mutez)
| C_bool , [] -> ok @@ T_constant(TC_bool)
| C_operation , [] -> ok @@ T_constant(TC_operation)
| C_address , [] -> ok @@ T_constant(TC_address)
| C_key , [] -> ok @@ T_constant(TC_key)
| C_key_hash , [] -> ok @@ T_constant(TC_key_hash)
| C_chain_id , [] -> ok @@ T_constant(TC_chain_id)
| C_signature , [] -> ok @@ T_constant(TC_signature)
| C_timestamp , [] -> ok @@ T_constant(TC_timestamp)
| _ , [] ->
failwith "internal error: wrong number of arguments for type constant"
| _ , _ ->
failwith "internal error: unknown type operator"

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

@ -78,23 +78,37 @@ module Substitution = struct
| T.T_constant (type_name) -> | T.T_constant (type_name) ->
let%bind type_name = s_type_name_constant ~v ~expr type_name in let%bind type_name = s_type_name_constant ~v ~expr type_name in
ok @@ T.T_constant (type_name) ok @@ T.T_constant (type_name)
| T.T_variable _ -> failwith "TODO: T_variable" | T.T_variable variable ->
| T.T_operator _ -> failwith "TODO: T_operator" if Var.equal variable v
then ok @@ expr
else ok @@ T.T_variable variable
| T.T_operator (type_name_and_args) ->
let bind_map_type_operator = Stage_common.Misc.bind_map_type_operator in (* TODO: write T.Misc.bind_map_type_operator, but it doesn't work *)
let%bind type_name_and_args = bind_map_type_operator (s_type_value ~v ~expr) type_name_and_args in
ok @@ T.T_operator type_name_and_args
| T.T_arrow _ -> | T.T_arrow _ ->
let _TODO = (v, expr) in let _TODO = (v, expr) in
failwith "TODO: T_function" failwith "TODO: T_function"
and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} -> and s_type_expression' ~v ~expr : _ Ast_simplified.type_expression' w = fun type_expression' ->
match type_expression' with match type_expression' with
| Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression" | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple"
| Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression" | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum"
| Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression" | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record"
| Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression" | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow"
| Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression" | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable"
| Ast_simplified.T_operator _ -> failwith "TODO: subst: unimplemented case s_type_expression" | Ast_simplified.T_operator op ->
| Ast_simplified.T_constant _ -> let%bind op =
let _TODO = (v, expr) in Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *)
failwith "TODO: subst: unimplemented case s_type_expression" (s_type_expression ~v ~expr)
op in
ok @@ Ast_simplified.T_operator op
| Ast_simplified.T_constant constant ->
ok @@ Ast_simplified.T_constant constant
and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} ->
let%bind type_expression' = s_type_expression' ~v ~expr type_expression' in
ok @@ Ast_simplified.{type_expression'}
and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } -> 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 type_value' = s_type_value' ~v ~expr type_value' in