Merge done and repo build with no error
This commit is contained in:
Pierre-Emmanuel Wulfman
parent
0c6f233507
commit
f657c71753
@ -7,6 +7,7 @@
|
||||
ast_simplified
|
||||
ast_typed
|
||||
operators
|
||||
union_find
|
||||
)
|
||||
(preprocess
|
||||
(pps ppx_let)
|
||||
|
||||
716
src/passes/4-typer/solver.ml
Normal file
716
src/passes/4-typer/solver.ml
Normal file
@ -0,0 +1,716 @@
|
||||
open Trace
|
||||
|
||||
module Core = Typesystem.Core
|
||||
|
||||
module Wrap = struct
|
||||
module I = Ast_simplified
|
||||
module O = Core
|
||||
|
||||
type constraints = O.type_constraint list
|
||||
|
||||
(* let add_type state t = *)
|
||||
(* let constraints = Wrap.variable type_name t in *)
|
||||
(* let%bind state' = aggregate_constraints state constraints in *)
|
||||
(* ok state' in *)
|
||||
(* let return_add_type ?(state = state) expr t = *)
|
||||
(* let%bind state' = add_type state t in *)
|
||||
(* return expr state' in *)
|
||||
|
||||
let rec type_expression_to_type_value : I.type_expression -> O.type_value = fun te ->
|
||||
match te with
|
||||
| T_tuple types ->
|
||||
P_constant (C_tuple, List.map type_expression_to_type_value types)
|
||||
| T_sum kvmap ->
|
||||
P_constant (C_variant, Map.String.to_list @@ Map.String.map type_expression_to_type_value kvmap)
|
||||
| T_record kvmap ->
|
||||
P_constant (C_record, Map.String.to_list @@ Map.String.map type_expression_to_type_value kvmap)
|
||||
| T_function (arg , ret) ->
|
||||
P_constant (C_arrow, List.map type_expression_to_type_value [ arg ; ret ])
|
||||
| T_variable type_name -> P_variable type_name
|
||||
| T_constant (type_name , args) ->
|
||||
let csttag = Core.(match type_name with
|
||||
| "arrow" -> C_arrow
|
||||
| "option" -> C_option
|
||||
| "tuple" -> C_tuple
|
||||
| "map" -> C_map
|
||||
| "list" -> C_list
|
||||
| "set" -> C_set
|
||||
| "unit" -> C_unit
|
||||
| "bool" -> C_bool
|
||||
| "string" -> C_string
|
||||
| _ -> failwith "TODO")
|
||||
in
|
||||
P_constant (csttag, List.map type_expression_to_type_value args)
|
||||
|
||||
(** TODO *)
|
||||
let type_declaration : I.declaration -> constraints = fun td ->
|
||||
match td with
|
||||
| Declaration_type (name , te) ->
|
||||
let pattern = type_expression_to_type_value te in
|
||||
[C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *)
|
||||
| Declaration_constant (name, te, _) ->(
|
||||
match te with
|
||||
| Some (exp) ->
|
||||
let pattern = type_expression_to_type_value exp in
|
||||
[C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *)
|
||||
| None ->
|
||||
(** TODO *)
|
||||
[]
|
||||
)
|
||||
|
||||
(* TODO: this should be renamed to failwith_ *)
|
||||
let failwith : unit -> (constraints * O.type_variable) = fun () ->
|
||||
let type_name = Core.fresh_type_variable () in
|
||||
[] , type_name
|
||||
|
||||
let variable : I.name -> I.type_expression -> (constraints * O.type_variable) = fun _name expr ->
|
||||
let pattern = type_expression_to_type_value expr in
|
||||
let type_name = Core.fresh_type_variable () in
|
||||
[C_equation (P_variable (type_name) , pattern)] , type_name
|
||||
|
||||
let literal : I.type_expression -> (constraints * O.type_variable) = fun t ->
|
||||
let pattern = type_expression_to_type_value t in
|
||||
let type_name = Core.fresh_type_variable () in
|
||||
[C_equation (P_variable (type_name) , pattern)] , type_name
|
||||
|
||||
(*
|
||||
let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
|
||||
let pattern = type_expression_to_type_value I.t_bool in
|
||||
let type_name = Core.fresh_type_variable () in
|
||||
[C_equation (P_variable (type_name) , pattern)] , type_name
|
||||
|
||||
let literal_string : unit -> (constraints * O.type_variable) = fun () ->
|
||||
let pattern = type_expression_to_type_value I.t_string in
|
||||
let type_name = Core.fresh_type_variable () in
|
||||
[C_equation (P_variable (type_name) , pattern)] , type_name
|
||||
*)
|
||||
|
||||
let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys ->
|
||||
let patterns = List.map type_expression_to_type_value tys in
|
||||
let pattern = O.(P_constant (C_tuple , patterns)) in
|
||||
let type_name = Core.fresh_type_variable () in
|
||||
[C_equation (P_variable (type_name) , pattern)] , type_name
|
||||
|
||||
(* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *)
|
||||
(* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *)
|
||||
(* let t_record = ('label:string, 'v) … -> record ('label : 'v) … with independent choices for each 'label and 'v *)
|
||||
(* let t_variable = t_of_var_in_env *)
|
||||
(* let t_access_int = record ('label:int , 'v) … -> 'label:int -> 'v *)
|
||||
(* let t_access_string = record ('label:string , 'v) … -> 'label:string -> 'v *)
|
||||
|
||||
module Prim_types = struct
|
||||
open Typesystem.Shorthands
|
||||
|
||||
let t_cons = forall "v" @@ fun v -> v --> list v --> list v (* was: list *)
|
||||
let t_setcons = forall "v" @@ fun v -> v --> set v --> set v (* was: set *)
|
||||
let t_mapcons = forall2 "k" "v" @@ fun k v -> (k * v) --> map k v --> map k v (* was: map *)
|
||||
let t_failwith = forall "a" @@ fun a -> a
|
||||
(* let t_literal_t = t *)
|
||||
let t_literal_bool = bool
|
||||
let t_literal_string = string
|
||||
let t_access_map = forall2 "k" "v" @@ fun k v -> map k v --> k --> v
|
||||
let t_application = forall2 "a" "b" @@ fun a b -> (a --> b) --> a --> b
|
||||
let t_look_up = forall2 "ind" "v" @@ fun ind v -> map ind v --> ind --> option v
|
||||
let t_sequence = forall "b" @@ fun b -> unit --> b --> b
|
||||
let t_loop = bool --> unit --> unit
|
||||
end
|
||||
|
||||
(* TODO: I think we should take an I.expression for the base+label *)
|
||||
let access_label ~base ~label : (constraints * O.type_variable) =
|
||||
let base' = type_expression_to_type_value base in
|
||||
let expr_type = Core.fresh_type_variable () in
|
||||
[O.C_access_label (base' , label , expr_type)] , expr_type
|
||||
|
||||
let access_int ~base ~index = access_label ~base ~label:(L_int index)
|
||||
let access_string ~base ~property = access_label ~base ~label:(L_string property)
|
||||
|
||||
let access_map : base:I.type_expression -> key:I.type_expression -> (constraints * O.type_variable) =
|
||||
let mk_map_type key_type element_type =
|
||||
O.P_constant O.(C_map , [P_variable element_type; P_variable key_type]) in
|
||||
fun ~base ~key ->
|
||||
let key_type = Core.fresh_type_variable () in
|
||||
let element_type = Core.fresh_type_variable () in
|
||||
let base' = type_expression_to_type_value base in
|
||||
let key' = type_expression_to_type_value key in
|
||||
let base_expected = mk_map_type key_type element_type in
|
||||
let expr_type = Core.fresh_type_variable () in
|
||||
O.[C_equation (base' , base_expected);
|
||||
C_equation (key' , P_variable key_type);
|
||||
C_equation (P_variable expr_type , P_variable element_type)] , expr_type
|
||||
|
||||
let constructor
|
||||
: I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable)
|
||||
= fun t_arg c_arg sum ->
|
||||
let t_arg = type_expression_to_type_value t_arg in
|
||||
let c_arg = type_expression_to_type_value c_arg in
|
||||
let sum = type_expression_to_type_value sum in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
[
|
||||
C_equation (P_variable (whole_expr) , sum) ;
|
||||
C_equation (t_arg , c_arg)
|
||||
] , whole_expr
|
||||
|
||||
let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields ->
|
||||
let record_type = type_expression_to_type_value (I.t_record fields) in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
[C_equation (P_variable whole_expr , record_type)] , whole_expr
|
||||
|
||||
let collection : O.constant_tag -> I.type_expression list -> (constraints * O.type_variable) =
|
||||
fun ctor element_tys ->
|
||||
let elttype = O.P_variable (Core.fresh_type_variable ()) in
|
||||
let aux elt =
|
||||
let elt' = type_expression_to_type_value elt
|
||||
in O.C_equation (elttype , elt') in
|
||||
let equations = List.map aux element_tys in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (P_variable whole_expr , O.P_constant (ctor , [elttype]))
|
||||
] @ equations , whole_expr
|
||||
|
||||
let list = collection O.C_list
|
||||
let set = collection O.C_set
|
||||
|
||||
let map : (I.type_expression * I.type_expression) list -> (constraints * O.type_variable) =
|
||||
fun kv_tys ->
|
||||
let k_type = O.P_variable (Core.fresh_type_variable ()) in
|
||||
let v_type = O.P_variable (Core.fresh_type_variable ()) in
|
||||
let aux_k (k , _v) =
|
||||
let k' = type_expression_to_type_value k in
|
||||
O.C_equation (k_type , k') in
|
||||
let aux_v (_k , v) =
|
||||
let v' = type_expression_to_type_value v in
|
||||
O.C_equation (v_type , v') in
|
||||
let equations_k = List.map aux_k kv_tys in
|
||||
let equations_v = List.map aux_v kv_tys in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type]))
|
||||
] @ equations_k @ equations_v , whole_expr
|
||||
|
||||
let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun f arg ->
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
let f' = type_expression_to_type_value f in
|
||||
let arg' = type_expression_to_type_value arg in
|
||||
O.[
|
||||
C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
|
||||
] , whole_expr
|
||||
|
||||
let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun ds ind ->
|
||||
let ds' = type_expression_to_type_value ds in
|
||||
let ind' = type_expression_to_type_value ind in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
let v = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (ds' , P_constant (C_map, [ind' ; P_variable v])) ;
|
||||
C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v]))
|
||||
] , whole_expr
|
||||
|
||||
let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun a b ->
|
||||
let a' = type_expression_to_type_value a in
|
||||
let b' = type_expression_to_type_value b in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (a' , P_constant (C_unit , [])) ;
|
||||
C_equation (b' , P_variable whole_expr)
|
||||
] , whole_expr
|
||||
|
||||
let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun expr body ->
|
||||
let expr' = type_expression_to_type_value expr in
|
||||
let body' = type_expression_to_type_value body in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (expr' , P_constant (C_bool , [])) ;
|
||||
C_equation (body' , P_constant (C_unit , [])) ;
|
||||
C_equation (P_variable whole_expr , P_constant (C_unit , []))
|
||||
] , whole_expr
|
||||
|
||||
let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun rhs rhs_tv_opt result ->
|
||||
let rhs' = type_expression_to_type_value rhs in
|
||||
let result' = type_expression_to_type_value result in
|
||||
let rhs_tv_opt' = match rhs_tv_opt with
|
||||
None -> []
|
||||
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (result' , P_variable whole_expr)
|
||||
] @ rhs_tv_opt', whole_expr
|
||||
|
||||
let assign : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun v e ->
|
||||
let v' = type_expression_to_type_value v in
|
||||
let e' = type_expression_to_type_value e in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (v' , e') ;
|
||||
C_equation (P_variable whole_expr , P_constant (C_unit , []))
|
||||
] , whole_expr
|
||||
|
||||
let annotation : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
|
||||
fun e annot ->
|
||||
let e' = type_expression_to_type_value e in
|
||||
let annot' = type_expression_to_type_value annot in
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
O.[
|
||||
C_equation (e' , annot') ;
|
||||
C_equation (e' , P_variable whole_expr)
|
||||
] , whole_expr
|
||||
|
||||
let matching : I.type_expression list -> (constraints * O.type_variable) =
|
||||
fun es ->
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
let type_values = (List.map type_expression_to_type_value es) in
|
||||
let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values
|
||||
in cs, whole_expr
|
||||
|
||||
let fresh_binder () =
|
||||
Core.fresh_type_variable ()
|
||||
|
||||
let lambda
|
||||
: I.type_expression ->
|
||||
I.type_expression option ->
|
||||
I.type_expression option ->
|
||||
(constraints * O.type_variable) =
|
||||
fun fresh arg body ->
|
||||
let whole_expr = Core.fresh_type_variable () in
|
||||
let unification_arg = Core.fresh_type_variable () in
|
||||
let unification_body = Core.fresh_type_variable () in
|
||||
let arg' = match arg with
|
||||
None -> []
|
||||
| Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in
|
||||
let body' = match body with
|
||||
None -> []
|
||||
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)]
|
||||
in O.[
|
||||
C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
|
||||
C_equation (P_variable whole_expr ,
|
||||
P_constant (C_arrow , [P_variable unification_arg ;
|
||||
P_variable unification_body]))
|
||||
] @ arg' @ body' , whole_expr
|
||||
|
||||
end
|
||||
|
||||
(* begin unionfind *)
|
||||
|
||||
module TV =
|
||||
struct
|
||||
type t = Core.type_variable
|
||||
let compare = String.compare
|
||||
let to_string = (fun s -> s)
|
||||
end
|
||||
|
||||
module UF = Union_find.Partition0.Make(TV)
|
||||
|
||||
type unionfind = UF.t
|
||||
|
||||
let empty = UF.empty (* DEMO *)
|
||||
let representative_toto = UF.repr "toto" empty (* DEMO *)
|
||||
let merge x y = UF.equiv x y (* DEMO *)
|
||||
|
||||
(* end unionfind *)
|
||||
|
||||
(* representant for an equivalence class of type variables *)
|
||||
module TypeVariable = String
|
||||
module TypeVariableMap = Map.Make(TypeVariable)
|
||||
|
||||
|
||||
(*
|
||||
|
||||
Components:
|
||||
* assignments (passive data structure).
|
||||
Now: just a map from unification vars to types (pb: what about partial types?)
|
||||
maybe just local assignments (allow only vars as children of pair(α,β))
|
||||
* constraint propagation: (buch of constraints) → (new constraints * assignments)
|
||||
* sub-component: constraint selector (worklist / dynamic queries)
|
||||
* sub-sub component: constraint normalizer: remove dupes and give structure
|
||||
right now: union-find of unification vars
|
||||
later: better database-like organisation of knowledge
|
||||
* sub-sub component: lazy selector (don't re-try all selectors every time)
|
||||
For now: just re-try everytime
|
||||
* sub-component: propagation rule
|
||||
For now: break pair(a, b) = pair(c, d) into a = c, b = d
|
||||
* generalizer
|
||||
For now: ?
|
||||
|
||||
Workflow:
|
||||
Start with empty assignments and structured database
|
||||
Receive a new constraint
|
||||
For each normalizer:
|
||||
Use the pre-selector to see if it can be applied
|
||||
Apply the normalizer, get some new items to insert in the structured database
|
||||
For each propagator:
|
||||
Use the selector to query the structured database and see if it can be applied
|
||||
Apply the propagator, get some new constraints and assignments
|
||||
Add the new assignments to the data structure.
|
||||
|
||||
At some point (when?)
|
||||
For each generalizer:
|
||||
Use the generalizer's selector to see if it can be applied
|
||||
Apply the generalizer to produce a new type, possibly with some ∀s injected
|
||||
|
||||
*)
|
||||
|
||||
open Core
|
||||
|
||||
type structured_dbs = {
|
||||
all_constraints : type_constraint_simpl list ;
|
||||
aliases : unionfind ;
|
||||
(* assignments (passive data structure).
|
||||
Now: just a map from unification vars to types (pb: what about partial types?)
|
||||
maybe just local assignments (allow only vars as children of pair(α,β)) *)
|
||||
assignments : c_constructor_simpl TypeVariableMap.t ;
|
||||
grouped_by_variable : constraints TypeVariableMap.t ; (* map from (unionfind) variables to constraints containing them *)
|
||||
cycle_detection_toposort : unit ; (* example of structured db that we'll add later *)
|
||||
}
|
||||
|
||||
and constraints = {
|
||||
constructor : c_constructor_simpl list ;
|
||||
tc : c_typeclass_simpl list ;
|
||||
}
|
||||
|
||||
and c_constructor_simpl = {
|
||||
tv : type_variable;
|
||||
c_tag : constant_tag;
|
||||
tv_list : type_variable list;
|
||||
}
|
||||
(* copy-pasted from core.ml *)
|
||||
and c_const = (type_variable * type_value)
|
||||
and c_equation = (type_value * type_value)
|
||||
and c_typeclass_simpl = {
|
||||
tc : typeclass ;
|
||||
args : type_variable list ;
|
||||
}
|
||||
and type_constraint_simpl =
|
||||
SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *)
|
||||
| SC_Alias of (type_variable * type_variable) (* α = β *)
|
||||
| SC_Typeclass of c_typeclass_simpl (* TC(α, …) *)
|
||||
|
||||
module UnionFindWrapper = struct
|
||||
(* TODO: API for the structured db, to access it modulo unification variable aliases. *)
|
||||
let get_constraints_related_to : type_variable -> structured_dbs -> constraints =
|
||||
fun variable dbs ->
|
||||
let variable , aliases = UF.get_or_set variable dbs.aliases in
|
||||
let dbs = { dbs with aliases } in
|
||||
match TypeVariableMap.find_opt variable dbs.grouped_by_variable with
|
||||
Some l -> l
|
||||
| None -> {
|
||||
constructor = [] ;
|
||||
tc = [] ;
|
||||
}
|
||||
let add_constraints_related_to : type_variable -> constraints -> structured_dbs -> structured_dbs =
|
||||
fun variable c dbs ->
|
||||
(* let (variable_repr , _height) , aliases = UF.get_or_set variable dbs.aliases in
|
||||
let dbs = { dbs with aliases } in *)
|
||||
let variable_repr , aliases = UF.get_or_set variable dbs.aliases in
|
||||
let dbs = { dbs with aliases } in
|
||||
let grouped_by_variable = TypeVariableMap.update variable_repr (function
|
||||
None -> Some c
|
||||
| Some x -> Some {
|
||||
constructor = c.constructor @ x.constructor ;
|
||||
tc = c.tc @ x.tc ;
|
||||
})
|
||||
dbs.grouped_by_variable
|
||||
in
|
||||
let dbs = { dbs with grouped_by_variable } in
|
||||
dbs
|
||||
let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs =
|
||||
fun variable_a variable_b dbs ->
|
||||
let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
|
||||
let dbs = { dbs with aliases } in
|
||||
let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
|
||||
let dbs = { dbs with aliases } in
|
||||
let default d = function None -> d | Some y -> y in
|
||||
let get_constraints ab =
|
||||
TypeVariableMap.find_opt ab dbs.grouped_by_variable
|
||||
|> default { constructor = [] ; tc = [] } in
|
||||
let constraints_a = get_constraints variable_repr_a in
|
||||
let constraints_b = get_constraints variable_repr_b in
|
||||
let all_constraints = {
|
||||
(* TODO: should be a Set.union, not @ *)
|
||||
constructor = constraints_a.constructor @ constraints_b.constructor ;
|
||||
tc = constraints_a.tc @ constraints_b.tc ;
|
||||
} in
|
||||
let grouped_by_variable =
|
||||
TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
|
||||
let dbs = { dbs with grouped_by_variable} in
|
||||
let grouped_by_variable =
|
||||
TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
|
||||
let dbs = { dbs with grouped_by_variable} in
|
||||
dbs
|
||||
end
|
||||
|
||||
(* sub-sub component: constraint normalizer: remove dupes and give structure
|
||||
* right now: union-find of unification vars
|
||||
* later: better database-like organisation of knowledge *)
|
||||
|
||||
(* Each normalizer returns a *)
|
||||
type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list)
|
||||
|
||||
let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer =
|
||||
fun dbs new_constraint ->
|
||||
({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint])
|
||||
|
||||
let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer =
|
||||
fun dbs new_constraint ->
|
||||
let store_constraint tvars constraints =
|
||||
let aux dbs (tvar : type_variable) =
|
||||
UnionFindWrapper.add_constraints_related_to tvar constraints dbs
|
||||
in List.fold_left aux dbs tvars
|
||||
in
|
||||
let merge_constraints a b =
|
||||
UnionFindWrapper.merge_variables a b dbs in
|
||||
let dbs = match new_constraint with
|
||||
SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; tc = []}
|
||||
| SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; tc = [c]}
|
||||
| SC_Alias (a , b) -> merge_constraints a b
|
||||
in (dbs , [new_constraint])
|
||||
|
||||
(* Stores the first assinment ('a = ctor('b, …)) seen *)
|
||||
let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
|
||||
fun dbs new_constraint ->
|
||||
match new_constraint with
|
||||
| SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) ->
|
||||
let assignments = TypeVariableMap.update tv (function None -> Some c | e -> e) dbs.assignments in
|
||||
let dbs = {dbs with assignments} in
|
||||
(dbs , [new_constraint])
|
||||
| _ ->
|
||||
(dbs , [new_constraint])
|
||||
|
||||
let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer =
|
||||
fun dbs new_constraint ->
|
||||
match new_constraint with
|
||||
| C_equation (P_forall _, P_forall _) -> failwith "TODO"
|
||||
| C_equation ((P_forall _ as a), (P_variable _ as b)) -> normalizer_simpl dbs (C_equation (b , a))
|
||||
| C_equation (P_forall _, P_constant _) -> failwith "TODO"
|
||||
| C_equation (P_variable _, P_forall _) -> failwith "TODO"
|
||||
| C_equation (P_variable a, P_variable b) -> (dbs , [SC_Alias (a, b)])
|
||||
| C_equation (P_variable a, P_constant (c_tag, args)) ->
|
||||
let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
|
||||
let fresh_eqns = List.map (fun (v,t) -> C_equation (P_variable v, t)) (List.combine fresh_vars args) in
|
||||
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
|
||||
(dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars}] @ List.flatten recur)
|
||||
| C_equation (P_constant _, P_forall _) -> failwith "TODO"
|
||||
| C_equation ((P_constant _ as a), (P_variable _ as b)) -> normalizer_simpl dbs (C_equation (b , a))
|
||||
| C_equation ((P_constant _ as a), (P_constant _ as b)) ->
|
||||
(* break down c(args) = c'(args') into 'a = c(args) and 'a = c'(args') *)
|
||||
let fresh = Core.fresh_type_variable () in
|
||||
let (dbs , cs1) = normalizer_simpl dbs (C_equation (P_variable fresh, a)) in
|
||||
let (dbs , cs2) = normalizer_simpl dbs (C_equation (P_variable fresh, b)) in
|
||||
(dbs , cs1 @ cs2) (* TODO: O(n) concatenation! *)
|
||||
| C_typeclass (args, tc) ->
|
||||
(* break down TC(args) into TC('a, …) and ('a = arg) … *)
|
||||
let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
|
||||
let fresh_eqns = List.map (fun (v,t) -> C_equation (P_variable v, t)) (List.combine fresh_vars args) in
|
||||
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
|
||||
(dbs, [SC_Typeclass { tc ; args = fresh_vars }] @ List.flatten recur)
|
||||
| C_access_label (tv, label, result) -> let _todo = ignore (tv, label, result) in failwith "TODO"
|
||||
|
||||
type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list }
|
||||
let lift_state_list_monad ~state ~list = { state ; list }
|
||||
let lift f =
|
||||
fun { state ; list } ->
|
||||
let (new_state , new_lists) = List.fold_map_acc f state list in
|
||||
{ state = new_state ; list = List.flatten new_lists }
|
||||
|
||||
(* TODO: move this to the List module *)
|
||||
let named_fold_left f ~acc ~lst = List.fold_left (fun acc lst -> f ~acc ~lst) acc lst
|
||||
|
||||
(* TODO: place the list of normalizers in a map *)
|
||||
(* (\* cons for heterogeneous lists *\)
|
||||
* type 'b f = { f : 'a . ('a -> 'b) -> 'a -> 'b }
|
||||
* type ('hd , 'tl) hcons = { hd : 'hd ; tl : 'tl ; map : 'b . 'b f -> ('b , 'tl) hcons }
|
||||
* let (+::) hd tl = { hd ; tl ; map = fun x -> }
|
||||
*
|
||||
* let list_of_normalizers =
|
||||
* normalizer_simpl +::
|
||||
* normalizer_all_constraints +::
|
||||
* normalizer_assignments +::
|
||||
* normalizer_grouped_by_variable +::
|
||||
* () *)
|
||||
|
||||
module Fun = struct let id x = x end (* in stdlib as of 4.08, we're in 4.07 for now *)
|
||||
|
||||
let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad =
|
||||
fun new_constraint dbs ->
|
||||
Fun.id
|
||||
@@ lift normalizer_grouped_by_variable
|
||||
@@ lift normalizer_assignments
|
||||
@@ lift normalizer_all_constraints
|
||||
@@ lift normalizer_simpl
|
||||
@@ lift_state_list_monad ~state:dbs ~list:[new_constraint]
|
||||
|
||||
(* sub-sub component: lazy selector (don't re-try all selectors every time)
|
||||
* For now: just re-try everytime *)
|
||||
|
||||
type todo = unit
|
||||
let todo : todo = ()
|
||||
type 'old_constraint_type selector_input = 'old_constraint_type (* some info about the constraint just added, so that we know what to look for *)
|
||||
type 'selector_output selector_outputs =
|
||||
WasSelected of 'selector_output list
|
||||
| WasNotSelected
|
||||
type new_constraints = type_constraint list
|
||||
type new_assignments = c_constructor_simpl list
|
||||
|
||||
type ('old_constraint_type, 'selector_output) selector = 'old_constraint_type selector_input -> structured_dbs -> 'selector_output selector_outputs
|
||||
|
||||
(* selector / propagation rule for breaking down composite types
|
||||
* For now: do something with ('a = 'b) constraints.
|
||||
|
||||
Or maybe this one should be a normalizer. *)
|
||||
|
||||
(* selector / propagation rule for breaking down composite types
|
||||
* For now: break pair(a, b) = pair(c, d) into a = c, b = d *)
|
||||
|
||||
type output_break_ctor = < a_k_var : c_constructor_simpl ; a_k'_var' : c_constructor_simpl >
|
||||
let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector =
|
||||
(* find two rules with the shape a = k(var …) and a = k'(var' …) *)
|
||||
fun todo dbs ->
|
||||
match todo with
|
||||
SC_Constructor c ->
|
||||
let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).constructor in
|
||||
let cs_pairs = List.map (fun x -> object method a_k_var = c method a_k'_var' = x end) other_cs in
|
||||
WasSelected cs_pairs
|
||||
| SC_Alias _ -> WasNotSelected (* TODO: ??? *)
|
||||
| SC_Typeclass _ -> WasNotSelected
|
||||
|
||||
type 'selector_output propagator = 'selector_output -> structured_dbs -> new_constraints * new_assignments
|
||||
|
||||
let propagator_break_ctor : output_break_ctor propagator =
|
||||
fun selected dbs ->
|
||||
let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
|
||||
let a = selected#a_k_var in
|
||||
let b = selected#a_k'_var' in
|
||||
(* produce constraints: *)
|
||||
|
||||
(* a.tv = b.tv *)
|
||||
let eq1 = C_equation (P_variable a.tv, P_variable b.tv) in
|
||||
(* a.c_tag = b.c_tag *)
|
||||
if a.c_tag <> b.c_tag then
|
||||
failwith "type error: incompatible types, not same ctor (TODO error message)"
|
||||
else
|
||||
(* a.tv_list = b.tv_list *)
|
||||
if List.length a.tv_list <> List.length b.tv_list then
|
||||
failwith "type error: incompatible types, not same length (TODO error message)"
|
||||
else
|
||||
let eqs3 = List.map2 (fun aa bb -> C_equation (P_variable aa, P_variable bb)) a.tv_list b.tv_list in
|
||||
let eqs = eq1 :: eqs3 in
|
||||
(eqs , []) (* no new assignments *)
|
||||
|
||||
let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'a -> structured_dbs -> new_constraints * new_assignments =
|
||||
fun selector propagator ->
|
||||
fun todo dbs ->
|
||||
match selector todo dbs with
|
||||
WasSelected selected_outputs ->
|
||||
(* Call the propagation rule *)
|
||||
let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in
|
||||
let (new_constraints , new_assignments) = List.split new_contraints_and_assignments in
|
||||
(* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
|
||||
(List.flatten new_constraints , List.flatten new_assignments)
|
||||
| WasNotSelected ->
|
||||
([] , [])
|
||||
|
||||
let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor
|
||||
|
||||
let select_and_propagate_all' : type_constraint_simpl selector_input -> structured_dbs -> 'todo_result =
|
||||
fun new_constraint dbs ->
|
||||
let (new_constraints, new_assignments) = select_and_propagate_break_ctor new_constraint dbs in
|
||||
let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> TypeVariableMap.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in
|
||||
let dbs = { dbs with assignments } in
|
||||
(* let blah2 = select_ … in … *)
|
||||
(* We should try each selector in turn. If multiple selectors work, what should we do? *)
|
||||
(new_constraints , dbs)
|
||||
|
||||
let rec select_and_propagate_all : type_constraint selector_input list -> structured_dbs -> 'todo_result =
|
||||
fun new_constraints dbs ->
|
||||
match new_constraints with
|
||||
| [] -> dbs
|
||||
| new_constraint :: tl ->
|
||||
let { state = dbs ; list = modified_constraints } = normalizers new_constraint dbs in
|
||||
let (new_constraints' , dbs) =
|
||||
List.fold_left
|
||||
(fun (nc , dbs) c ->
|
||||
let (new_constraints' , dbs) = select_and_propagate_all' c dbs in
|
||||
(new_constraints' @ nc , dbs))
|
||||
([] , dbs)
|
||||
modified_constraints in
|
||||
let new_constraints = new_constraints' @ tl in
|
||||
select_and_propagate_all new_constraints dbs
|
||||
|
||||
(* sub-component: constraint selector (worklist / dynamic queries) *)
|
||||
|
||||
(* constraint propagation: (buch of constraints) → (new constraints * assignments) *)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* Below is a draft *)
|
||||
|
||||
type state = {
|
||||
(* when α-renaming x to y, we put them in the same union-find class *)
|
||||
unification_vars : unionfind ;
|
||||
|
||||
(* assigns a value to the representant in the unionfind *)
|
||||
assignments : type_value TypeVariableMap.t ;
|
||||
|
||||
(* constraints related to a type variable *)
|
||||
constraints : constraints TypeVariableMap.t ;
|
||||
}
|
||||
|
||||
let initial_state : state = {
|
||||
unification_vars = UF.empty ;
|
||||
constraints = TypeVariableMap.empty ;
|
||||
assignments = TypeVariableMap.empty ;
|
||||
}
|
||||
|
||||
(* let replace_var_in_state = fun (v : type_variable) (state : state) -> *)
|
||||
(* let aux_tv : type_value -> _ = function *)
|
||||
(* | P_forall (w , cs , tval) -> failwith "TODO" *)
|
||||
(* | P_variable (w) -> *)
|
||||
(* if w = v then *)
|
||||
(* (*…*) *)
|
||||
(* else *)
|
||||
(* (*…*) *)
|
||||
(* | P_constant (c , args) -> failwith "TODO" *)
|
||||
(* | P_access_label (tv , label) -> failwith "TODO" in *)
|
||||
(* let aux_tc tc = *)
|
||||
(* List.map (fun l -> List.map aux_tv l) tc in *)
|
||||
(* let aux : type_constraint -> _ = function *)
|
||||
(* | C_equation (l , r) -> C_equation (aux_tv l , aux_tv r) *)
|
||||
(* | C_typeclass (l , rs) -> C_typeclass (List.map aux_tv l , aux_tc rs) *)
|
||||
(* in List.map aux state *)
|
||||
|
||||
(* let check_equal a b = failwith "TODO"
|
||||
* let check_same_length l1 l2 = failwith "TODO"
|
||||
*
|
||||
* let rec unify : type_value * type_value -> type_constraint list result = function
|
||||
* | (P_variable v , P_constant (y , argsy)) ->
|
||||
* failwith "TODO: replace v with the constant everywhere."
|
||||
* | (P_constant (x , argsx) , P_variable w) ->
|
||||
* failwith "TODO: "
|
||||
* | (P_variable v , P_variable w) ->
|
||||
* failwith "TODO: replace v with w everywhere"
|
||||
* | (P_constant (x , argsx) , P_constant (y , argsy)) ->
|
||||
* let%bind () = check_equal x y in
|
||||
* let%bind () = check_same_length argsx argsy in
|
||||
* let%bind _ = bind_map_list unify (List.combine argsx argsy) in
|
||||
* ok []
|
||||
* | _ -> failwith "TODO" *)
|
||||
|
||||
(* (\* unify a and b, possibly produce new constraints *\) *)
|
||||
(* let () = ignore (a,b) in *)
|
||||
(* ok [] *)
|
||||
|
||||
(* This is the solver *)
|
||||
let aggregate_constraints : state -> type_constraint list -> state result = fun state newc ->
|
||||
(* TODO: Iterate over constraints *)
|
||||
(* TODO: try to unify things:
|
||||
if we have a = X and b = Y, try to unify X and Y *)
|
||||
let _todo = ignore (state, newc) in
|
||||
failwith "TODO"
|
||||
(*let { constraints ; eqv } = state in
|
||||
ok { constraints = constraints @ newc ; eqv }*)
|
||||
@ -8,6 +8,8 @@ module SMap = O.SMap
|
||||
|
||||
module Environment = O.Environment
|
||||
|
||||
module Solver = Solver
|
||||
|
||||
type environment = Environment.t
|
||||
|
||||
module Errors = struct
|
||||
@ -216,6 +218,7 @@ module Errors = struct
|
||||
] in
|
||||
error ~data title message
|
||||
end
|
||||
|
||||
open Errors
|
||||
|
||||
let rec type_program (p:I.program) : O.program result =
|
||||
@ -238,6 +241,9 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
|
||||
let env' = Environment.add_type type_name tv env in
|
||||
ok (env', None)
|
||||
| Declaration_constant (name , tv_opt , expression) -> (
|
||||
(*
|
||||
Determine the type of the expression and add it to the environment
|
||||
*)
|
||||
let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
|
||||
let%bind ae' =
|
||||
trace (constant_declaration_error name expression tv'_opt) @@
|
||||
@ -340,6 +346,10 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
||||
bind_map_list aux lst in
|
||||
ok (O.Match_variant (lst' , variant))
|
||||
|
||||
(*
|
||||
Recursively search the type_expression and return a result containing the
|
||||
type_value at the leaves
|
||||
*)
|
||||
and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
|
||||
let return tv' = ok (make_t tv' (Some t)) in
|
||||
match t with
|
||||
@ -782,6 +792,9 @@ let untype_literal (l:O.literal) : I.literal result =
|
||||
| Literal_address s -> ok (Literal_address s)
|
||||
| Literal_operation s -> ok (Literal_operation s)
|
||||
|
||||
(*
|
||||
Tranform a Ast_typed expression into an ast_simplified matching
|
||||
*)
|
||||
let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
|
||||
let open I in
|
||||
let return e = ok e in
|
||||
@ -849,6 +862,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
|
||||
let%bind result = untype_expression result in
|
||||
return (e_let_in (binder , (Some tv)) rhs result)
|
||||
|
||||
(*
|
||||
Tranform a Ast_typed matching into an ast_simplified matching
|
||||
*)
|
||||
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
|
||||
let open I in
|
||||
match m with
|
||||
|
||||
879
src/passes/4-typer/typer.ml.old
Normal file
879
src/passes/4-typer/typer.ml.old
Normal file
@ -0,0 +1,879 @@
|
||||
open Trace
|
||||
|
||||
module I = Ast_simplified
|
||||
module O = Ast_typed
|
||||
open O.Combinators
|
||||
|
||||
module SMap = O.SMap
|
||||
|
||||
module Environment = O.Environment
|
||||
|
||||
type environment = Environment.t
|
||||
|
||||
module Errors = struct
|
||||
let unbound_type_variable (e:environment) (n:string) () =
|
||||
let title = (thunk "unbound type variable") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("variable" , fun () -> Format.asprintf "%s" n) ;
|
||||
(* TODO: types don't have srclocs for now. *)
|
||||
(* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *)
|
||||
("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let unbound_variable (e:environment) (n:string) (loc:Location.t) () =
|
||||
let title = (thunk "unbound variable") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("variable" , fun () -> Format.asprintf "%s" n) ;
|
||||
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let match_empty_variant : type a . a I.matching -> Location.t -> unit -> _ =
|
||||
fun matching loc () ->
|
||||
let title = (thunk "match with no cases") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let match_missing_case : type a . a I.matching -> Location.t -> unit -> _ =
|
||||
fun matching loc () ->
|
||||
let title = (thunk "missing case in match") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let match_redundant_case : type a . a I.matching -> Location.t -> unit -> _ =
|
||||
fun matching loc () ->
|
||||
let title = (thunk "missing case in match") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let unbound_constructor (e:environment) (n:string) (loc:Location.t) () =
|
||||
let title = (thunk "unbound constructor") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("constructor" , fun () -> Format.asprintf "%s" n) ;
|
||||
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let unrecognized_constant (n:string) (loc:Location.t) () =
|
||||
let title = (thunk "unrecognized constant") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("constant" , fun () -> Format.asprintf "%s" n) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () =
|
||||
let title () = "wrong arity" in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("function" , fun () -> Format.asprintf "%s" n) ;
|
||||
("expected" , fun () -> Format.asprintf "%d" expected) ;
|
||||
("actual" , fun () -> Format.asprintf "%d" actual) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () =
|
||||
let title () = "matching tuple of different size" in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ;
|
||||
("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
(* TODO: this should be a trace_info? *)
|
||||
let program_error (p:I.program) () =
|
||||
let message () = "" in
|
||||
let title = (thunk "typing program") in
|
||||
let data = [
|
||||
("program" , fun () -> Format.asprintf "%a" I.PP.program p)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let constant_declaration_error (name:string) (ae:I.expr) (expected: O.type_expression option) () =
|
||||
let title = (thunk "typing constant declaration") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("constant" , fun () -> Format.asprintf "%s" name) ;
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
("expected" , fun () ->
|
||||
match expected with
|
||||
None -> "(no annotation for the expected type)"
|
||||
| Some expected -> Format.asprintf "%a" O.PP.type_expression expected) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_expression -> Location.t -> unit -> _ =
|
||||
fun ?(msg = "") ~expected ~actual loc () ->
|
||||
let title = (thunk "typing match") in
|
||||
let message () = msg in
|
||||
let data = [
|
||||
("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
|
||||
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let needs_annotation (e : I.expression) (case : string) () =
|
||||
let title = (thunk "this expression must be annotated with its type") in
|
||||
let message () = Format.asprintf "%s needs an annotation" case in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp e.location)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
|
||||
let title = (thunk "type error") in
|
||||
let message () = msg in
|
||||
let data = [
|
||||
("expected" , fun () -> Format.asprintf "%s" expected);
|
||||
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual);
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
|
||||
let title = (thunk "type error") in
|
||||
let message () = msg in
|
||||
let data = [
|
||||
("expected" , fun () -> Format.asprintf "%a" O.PP.type_expression expected);
|
||||
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual);
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let bad_tuple_index (index : int) (ae : I.expression) (t : O.type_expression) (loc:Location.t) () =
|
||||
let title = (thunk "invalid tuple index") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("index" , fun () -> Format.asprintf "%d" index) ;
|
||||
("tuple_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_expression t) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let bad_record_access (field : string) (ae : I.expression) (t : O.type_expression) (loc:Location.t) () =
|
||||
let title = (thunk "invalid record field") in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("field" , fun () -> Format.asprintf "%s" field) ;
|
||||
("record_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_expression t) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let not_supported_yet (message : string) (ae : I.expression) () =
|
||||
let title = (thunk "not supported yet") in
|
||||
let message () = message in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let not_supported_yet_untranspile (message : string) (ae : O.expression) () =
|
||||
let title = (thunk "not supported yet") in
|
||||
let message () = message in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" O.PP.expression ae)
|
||||
] in
|
||||
error ~data title message ()
|
||||
|
||||
let constant_error loc lst tv_opt =
|
||||
let title () = "typing constant" in
|
||||
let message () = "" in
|
||||
let data = [
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
|
||||
("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_expression (const " , ")) lst) ;
|
||||
("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_expression) tv_opt) ;
|
||||
] in
|
||||
error ~data title message
|
||||
end
|
||||
open Errors
|
||||
|
||||
let rec type_program (p:I.program) : O.program result =
|
||||
let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
|
||||
let%bind ed' = (bind_map_location (type_declaration e)) d in
|
||||
let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
|
||||
let (e', d') = Location.unwrap ed' in
|
||||
match d' with
|
||||
| None -> ok (e', acc)
|
||||
| Some d' -> ok (e', loc ed' d' :: acc)
|
||||
in
|
||||
let%bind (_, lst) =
|
||||
trace (fun () -> program_error p ()) @@
|
||||
bind_fold_list aux (Environment.full_empty, []) p in
|
||||
ok @@ List.rev lst
|
||||
|
||||
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 type_name tv env in
|
||||
ok (env', None)
|
||||
| Declaration_constant (name , tv_opt , expression) -> (
|
||||
let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
|
||||
let%bind ae' =
|
||||
trace (constant_declaration_error name expression tv'_opt) @@
|
||||
type_expression ?tv_opt:tv'_opt env expression in
|
||||
let env' = Environment.add_ez_ae name ae' env in
|
||||
ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
|
||||
)
|
||||
|
||||
and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_expression -> i I.matching -> I.expression -> Location.t -> o O.matching result =
|
||||
fun f e t i ae loc -> match i with
|
||||
| Match_bool {match_true ; match_false} ->
|
||||
let%bind _ =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ get_t_bool t in
|
||||
let%bind match_true = f e match_true in
|
||||
let%bind match_false = f e match_false in
|
||||
ok (O.Match_bool {match_true ; match_false})
|
||||
| Match_option {match_none ; match_some} ->
|
||||
let%bind t_opt =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ get_t_option t in
|
||||
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_ez_binder 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} ->
|
||||
let%bind t_list =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ 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_ez_binder hd t_list e in
|
||||
let e' = Environment.add_ez_binder 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) ->
|
||||
let%bind t_tuple =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ get_t_tuple t in
|
||||
let%bind lst' =
|
||||
generic_try (match_tuple_wrong_arity t_tuple lst loc)
|
||||
@@ (fun () -> List.combine lst t_tuple) in
|
||||
let aux prev (name, tv) = Environment.add_ez_binder 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'))
|
||||
| Match_variant lst ->
|
||||
let%bind variant_opt =
|
||||
let aux acc ((constructor_name , _) , _) =
|
||||
let%bind (_ , variant) =
|
||||
trace_option (unbound_constructor e constructor_name loc) @@
|
||||
Environment.get_constructor constructor_name e in
|
||||
let%bind acc = match acc with
|
||||
| None -> ok (Some variant)
|
||||
| Some variant' -> (
|
||||
trace (type_error
|
||||
~msg:"in match variant"
|
||||
~expected:variant
|
||||
~actual:variant'
|
||||
~expression:ae
|
||||
loc
|
||||
) @@
|
||||
Ast_typed.assert_type_expression_eq (variant , variant') >>? fun () ->
|
||||
ok (Some variant)
|
||||
) in
|
||||
ok acc in
|
||||
trace (simple_info "in match variant") @@
|
||||
bind_fold_list aux None lst in
|
||||
let%bind variant =
|
||||
trace_option (match_empty_variant i loc) @@
|
||||
variant_opt in
|
||||
let%bind () =
|
||||
let%bind variant_cases' =
|
||||
trace (match_error ~expected:i ~actual:t loc)
|
||||
@@ Ast_typed.Combinators.get_t_sum variant in
|
||||
let variant_cases = List.map fst @@ Map.String.to_kv_list variant_cases' in
|
||||
let match_cases = List.map (Function.compose fst fst) lst in
|
||||
let test_case = fun c ->
|
||||
Assert.assert_true (List.mem c match_cases)
|
||||
in
|
||||
let%bind () =
|
||||
trace_strong (match_missing_case i loc) @@
|
||||
bind_iter_list test_case variant_cases in
|
||||
let%bind () =
|
||||
trace_strong (match_redundant_case i loc) @@
|
||||
Assert.assert_true List.(length variant_cases = length match_cases) in
|
||||
ok ()
|
||||
in
|
||||
let%bind lst' =
|
||||
let aux ((constructor_name , name) , b) =
|
||||
let%bind (constructor , _) =
|
||||
trace_option (unbound_constructor e constructor_name loc) @@
|
||||
Environment.get_constructor constructor_name e in
|
||||
let e' = Environment.add_ez_binder name constructor e in
|
||||
let%bind b' = f e' b in
|
||||
ok ((constructor_name , name) , b')
|
||||
in
|
||||
bind_map_list aux lst in
|
||||
ok (O.Match_variant (lst' , variant))
|
||||
|
||||
and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result =
|
||||
let return tv' = ok (make_t tv' (Some t)) in
|
||||
match t with
|
||||
| T_function (a, b) ->
|
||||
let%bind a' = evaluate_type e a in
|
||||
let%bind b' = evaluate_type e b in
|
||||
return (T_function (a', b'))
|
||||
| T_tuple lst ->
|
||||
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
|
||||
return (T_tuple lst')
|
||||
| T_sum m ->
|
||||
let aux k v prev =
|
||||
let%bind prev' = prev in
|
||||
let%bind v' = evaluate_type e v in
|
||||
ok @@ SMap.add k v' prev'
|
||||
in
|
||||
let%bind m = SMap.fold aux m (ok SMap.empty) in
|
||||
return (T_sum m)
|
||||
| T_record m ->
|
||||
let aux k v prev =
|
||||
let%bind prev' = prev in
|
||||
let%bind v' = evaluate_type e v in
|
||||
ok @@ SMap.add k v' prev'
|
||||
in
|
||||
let%bind m = SMap.fold aux m (ok SMap.empty) in
|
||||
return (T_record m)
|
||||
| T_variable name ->
|
||||
let%bind tv =
|
||||
trace_option (unbound_type_variable e name)
|
||||
@@ 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
|
||||
return (T_constant(cst, lst'))
|
||||
|
||||
and type_expression : environment -> ?tv_opt:O.type_expression -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae ->
|
||||
let module L = Logger.Stateful() in
|
||||
let return expr tv =
|
||||
let%bind () =
|
||||
match tv_opt with
|
||||
| None -> ok ()
|
||||
| Some tv' -> O.assert_type_expression_eq (tv' , tv) in
|
||||
let location = Location.get_location ae in
|
||||
ok @@ make_a_e ~location expr tv e in
|
||||
let main_error =
|
||||
let title () = "typing expression" in
|
||||
let content () = "" in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp @@ Location.get_location ae) ;
|
||||
("misc" , fun () -> L.get ()) ;
|
||||
] in
|
||||
error ~data title content in
|
||||
trace main_error @@
|
||||
match Location.unwrap ae with
|
||||
(* Basic *)
|
||||
| E_failwith _ -> fail @@ needs_annotation ae "the failwith keyword"
|
||||
| E_variable name ->
|
||||
let%bind tv' =
|
||||
trace_option (unbound_variable e name ae.location)
|
||||
@@ Environment.get_opt name e in
|
||||
return (E_variable name) tv'.type_expression
|
||||
| E_literal (Literal_bool b) ->
|
||||
return (E_literal (Literal_bool b)) (t_bool ())
|
||||
| E_literal Literal_unit | E_skip ->
|
||||
return (E_literal (Literal_unit)) (t_unit ())
|
||||
| E_literal (Literal_string s) -> (
|
||||
L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ;
|
||||
match Option.map Ast_typed.get_type' tv_opt with
|
||||
| Some (T_constant ("address" , [])) -> return (E_literal (Literal_address s)) (t_address ())
|
||||
| _ -> return (E_literal (Literal_string s)) (t_string ())
|
||||
)
|
||||
| E_literal (Literal_bytes s) ->
|
||||
return (E_literal (Literal_bytes s)) (t_bytes ())
|
||||
| E_literal (Literal_int n) ->
|
||||
return (E_literal (Literal_int n)) (t_int ())
|
||||
| E_literal (Literal_nat n) ->
|
||||
return (E_literal (Literal_nat n)) (t_nat ())
|
||||
| E_literal (Literal_timestamp n) ->
|
||||
return (E_literal (Literal_timestamp n)) (t_timestamp ())
|
||||
| E_literal (Literal_tez n) ->
|
||||
return (E_literal (Literal_tez n)) (t_tez ())
|
||||
| E_literal (Literal_address s) ->
|
||||
return (e_address s) (t_address ())
|
||||
| E_literal (Literal_operation op) ->
|
||||
return (e_operation op) (t_operation ())
|
||||
(* Tuple *)
|
||||
| E_tuple lst ->
|
||||
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
|
||||
let tv_lst = List.map get_type_annotation lst' in
|
||||
return (E_tuple lst') (t_tuple tv_lst ())
|
||||
| E_accessor (ae', path) ->
|
||||
let%bind e' = type_expression e ae' in
|
||||
let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
|
||||
match a with
|
||||
| Access_tuple index -> (
|
||||
let%bind tpl_tv = get_t_tuple prev.type_annotation in
|
||||
let%bind tv =
|
||||
generic_try (bad_tuple_index index ae' prev.type_annotation ae.location)
|
||||
@@ (fun () -> List.nth tpl_tv index) in
|
||||
return (E_tuple_accessor (prev , index)) tv
|
||||
)
|
||||
| Access_record property -> (
|
||||
let%bind r_tv = get_t_record prev.type_annotation in
|
||||
let%bind tv =
|
||||
generic_try (bad_record_access property ae' prev.type_annotation ae.location)
|
||||
@@ (fun () -> SMap.find property r_tv) in
|
||||
return (E_record_accessor (prev , property)) tv
|
||||
)
|
||||
| Access_map ae' -> (
|
||||
let%bind ae'' = type_expression e ae' in
|
||||
let%bind (k , v) = get_t_map prev.type_annotation in
|
||||
let%bind () =
|
||||
Ast_typed.assert_type_expression_eq (k , get_type_annotation ae'') in
|
||||
return (E_look_up (prev , ae'')) v
|
||||
)
|
||||
in
|
||||
trace (simple_info "accessing") @@
|
||||
bind_fold_list aux e' path
|
||||
|
||||
(* Sum *)
|
||||
| E_constructor (c, expr) ->
|
||||
let%bind (c_tv, sum_tv) =
|
||||
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_expression e expr in
|
||||
let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in
|
||||
return (E_constructor (c , expr')) sum_tv
|
||||
(* Record *)
|
||||
| E_record m ->
|
||||
let aux prev k expr =
|
||||
let%bind expr' = type_expression e expr in
|
||||
ok (SMap.add k expr' prev)
|
||||
in
|
||||
let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
|
||||
return (E_record m') (t_record (SMap.map get_type_annotation m') ())
|
||||
(* Data-structure *)
|
||||
| E_list lst ->
|
||||
let%bind lst' = bind_map_list (type_expression e) lst in
|
||||
let%bind tv =
|
||||
let aux opt c =
|
||||
match opt with
|
||||
| None -> ok (Some c)
|
||||
| Some c' ->
|
||||
let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in
|
||||
ok (Some c') in
|
||||
let%bind init = match tv_opt with
|
||||
| None -> ok None
|
||||
| Some ty ->
|
||||
let%bind ty' = get_t_list ty in
|
||||
ok (Some ty') in
|
||||
let%bind ty =
|
||||
let%bind opt = bind_fold_list aux init
|
||||
@@ List.map get_type_annotation lst' in
|
||||
trace_option (needs_annotation ae "empty list") opt in
|
||||
ok (t_list ty ())
|
||||
in
|
||||
return (E_list lst') tv
|
||||
| E_set lst ->
|
||||
let%bind lst' = bind_map_list (type_expression e) lst in
|
||||
let%bind tv =
|
||||
let aux opt c =
|
||||
match opt with
|
||||
| None -> ok (Some c)
|
||||
| Some c' ->
|
||||
let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in
|
||||
ok (Some c') in
|
||||
let%bind init = match tv_opt with
|
||||
| None -> ok None
|
||||
| Some ty ->
|
||||
let%bind ty' = get_t_set ty in
|
||||
ok (Some ty') in
|
||||
let%bind ty =
|
||||
let%bind opt = bind_fold_list aux init
|
||||
@@ List.map get_type_annotation lst' in
|
||||
trace_option (needs_annotation ae "empty set") opt in
|
||||
ok (t_set ty ())
|
||||
in
|
||||
return (E_set lst') tv
|
||||
| E_map lst ->
|
||||
let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
|
||||
let%bind tv =
|
||||
let aux opt c =
|
||||
match opt with
|
||||
| None -> ok (Some c)
|
||||
| Some c' ->
|
||||
let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in
|
||||
ok (Some c') in
|
||||
let%bind key_type =
|
||||
let%bind sub =
|
||||
bind_fold_list aux None
|
||||
@@ List.map get_type_annotation
|
||||
@@ List.map fst lst' in
|
||||
let%bind annot = bind_map_option get_t_map_key tv_opt in
|
||||
trace (simple_info "empty map expression without a type annotation") @@
|
||||
O.merge_annotation annot sub (needs_annotation ae "this map literal")
|
||||
in
|
||||
let%bind value_type =
|
||||
let%bind sub =
|
||||
bind_fold_list aux None
|
||||
@@ List.map get_type_annotation
|
||||
@@ List.map snd lst' in
|
||||
let%bind annot = bind_map_option get_t_map_value tv_opt in
|
||||
trace (simple_info "empty map expression without a type annotation") @@
|
||||
O.merge_annotation annot sub (needs_annotation ae "this map literal")
|
||||
in
|
||||
ok (t_map key_type value_type ())
|
||||
in
|
||||
return (E_map lst') tv
|
||||
| E_lambda {
|
||||
binder ;
|
||||
input_type ;
|
||||
output_type ;
|
||||
result ;
|
||||
} -> (
|
||||
let%bind input_type =
|
||||
let%bind input_type =
|
||||
(* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
|
||||
let default_action e () = fail @@ (needs_annotation e "the returned value") in
|
||||
match input_type with
|
||||
| Some ty -> ok ty
|
||||
| None -> (
|
||||
match Location.unwrap result with
|
||||
| I.E_let_in li -> (
|
||||
match Location.unwrap li.rhs with
|
||||
| I.E_variable name when name = (fst binder) -> (
|
||||
match snd li.binder with
|
||||
| Some ty -> ok ty
|
||||
| None -> default_action li.rhs ()
|
||||
)
|
||||
| _ -> default_action li.rhs ()
|
||||
)
|
||||
| _ -> default_action result ()
|
||||
)
|
||||
in
|
||||
evaluate_type e input_type in
|
||||
let%bind output_type =
|
||||
bind_map_option (evaluate_type e) output_type
|
||||
in
|
||||
let e' = Environment.add_ez_binder (fst binder) input_type e in
|
||||
let%bind result = type_expression ?tv_opt:output_type e' result in
|
||||
let output_type = result.type_annotation in
|
||||
return (E_lambda {binder = fst binder;input_type;output_type;result}) (t_function input_type output_type ())
|
||||
)
|
||||
| E_constant (name, lst) ->
|
||||
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
|
||||
let tv_lst = List.map get_type_annotation lst' in
|
||||
let%bind (name', tv) =
|
||||
type_constant name tv_lst tv_opt ae.location in
|
||||
return (E_constant (name' , lst')) tv
|
||||
| E_application (f, arg) ->
|
||||
let%bind f' = type_expression e f in
|
||||
let%bind arg = type_expression e arg in
|
||||
let%bind tv = match f'.type_annotation.type_expression' with
|
||||
| T_function (param, result) ->
|
||||
let%bind _ = O.assert_type_expression_eq (param, arg.type_annotation) in
|
||||
ok result
|
||||
| _ ->
|
||||
fail @@ type_error_approximate
|
||||
~expected:"should be a function type"
|
||||
~expression:f
|
||||
~actual:f'.type_annotation
|
||||
f'.location
|
||||
in
|
||||
return (E_application (f' , arg)) tv
|
||||
| E_look_up dsi ->
|
||||
let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
|
||||
let%bind (src, dst) = get_t_map ds.type_annotation in
|
||||
let%bind _ = O.assert_type_expression_eq (ind.type_annotation, src) in
|
||||
return (E_look_up (ds , ind)) (t_option dst ())
|
||||
(* Advanced *)
|
||||
| E_matching (ex, m) -> (
|
||||
let%bind ex' = type_expression e ex in
|
||||
match m with
|
||||
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
|
||||
| I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> (
|
||||
let%bind fw = I.get_e_failwith match_true in
|
||||
let%bind fw' = type_expression e fw in
|
||||
let%bind mf' = type_expression e match_false in
|
||||
let t = get_type_annotation ex' in
|
||||
let%bind () =
|
||||
trace_strong (match_error ~expected:m ~actual:t ae.location)
|
||||
@@ assert_t_bool t in
|
||||
let%bind () =
|
||||
trace_strong (match_error
|
||||
~msg:"matching not-unit on an assert"
|
||||
~expected:m
|
||||
~actual:t
|
||||
ae.location)
|
||||
@@ assert_t_unit (get_type_annotation mf') in
|
||||
let mt' = make_a_e
|
||||
(E_constant ("ASSERT_INFERRED" , [ex' ; fw']))
|
||||
(t_unit ())
|
||||
e
|
||||
in
|
||||
let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in
|
||||
return (O.E_matching (ex' , m')) (t_unit ())
|
||||
)
|
||||
| _ -> (
|
||||
let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
|
||||
let tvs =
|
||||
let aux (cur:O.value O.matching) =
|
||||
match cur with
|
||||
| Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
|
||||
| Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ]
|
||||
| Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
|
||||
| Match_tuple (_ , match_tuple) -> [ match_tuple ]
|
||||
| Match_variant (lst , _) -> List.map snd lst in
|
||||
List.map get_type_annotation @@ aux m' in
|
||||
let aux prec cur =
|
||||
let%bind () =
|
||||
match prec with
|
||||
| None -> ok ()
|
||||
| Some cur' -> Ast_typed.assert_type_expression_eq (cur , cur') in
|
||||
ok (Some cur) in
|
||||
let%bind tv_opt = bind_fold_list aux None tvs in
|
||||
let%bind tv =
|
||||
trace_option (match_empty_variant m ae.location) @@
|
||||
tv_opt in
|
||||
return (O.E_matching (ex', m')) tv
|
||||
)
|
||||
)
|
||||
| E_sequence (a , b) ->
|
||||
let%bind a' = type_expression e a in
|
||||
let%bind b' = type_expression e b in
|
||||
let a'_type_annot = get_type_annotation a' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"first part of the sequence should be of unit type"
|
||||
~expected:(O.t_unit ())
|
||||
~actual:a'_type_annot
|
||||
~expression:a
|
||||
a'.location) @@
|
||||
Ast_typed.assert_type_expression_eq (t_unit () , a'_type_annot) in
|
||||
return (O.E_sequence (a' , b')) (get_type_annotation b')
|
||||
| E_loop (expr , body) ->
|
||||
let%bind expr' = type_expression e expr in
|
||||
let%bind body' = type_expression e body in
|
||||
let t_expr' = get_type_annotation expr' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"while condition isn't of type bool"
|
||||
~expected:(O.t_bool ())
|
||||
~actual:t_expr'
|
||||
~expression:expr
|
||||
expr'.location) @@
|
||||
Ast_typed.assert_type_expression_eq (t_bool () , t_expr') in
|
||||
let t_body' = get_type_annotation body' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"while body isn't of unit type"
|
||||
~expected:(O.t_unit ())
|
||||
~actual:t_body'
|
||||
~expression:body
|
||||
body'.location) @@
|
||||
Ast_typed.assert_type_expression_eq (t_unit () , t_body') in
|
||||
return (O.E_loop (expr' , body')) (t_unit ())
|
||||
| E_assign (name , path , expr) ->
|
||||
let%bind typed_name =
|
||||
let%bind ele = Environment.get_trace name e in
|
||||
ok @@ make_n_t name ele.type_expression in
|
||||
let%bind (assign_tv , path') =
|
||||
let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path ->
|
||||
match cur_path with
|
||||
| Access_tuple index -> (
|
||||
let%bind tpl = get_t_tuple prec_tv in
|
||||
let%bind tv' =
|
||||
trace_option (bad_tuple_index index ae prec_tv ae.location) @@
|
||||
List.nth_opt tpl index in
|
||||
ok (tv' , prec_path @ [O.Access_tuple index])
|
||||
)
|
||||
| Access_record property -> (
|
||||
let%bind m = get_t_record prec_tv in
|
||||
let%bind tv' =
|
||||
trace_option (bad_record_access property ae prec_tv ae.location) @@
|
||||
Map.String.find_opt property m in
|
||||
ok (tv' , prec_path @ [O.Access_record property])
|
||||
)
|
||||
| Access_map _ ->
|
||||
fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
|
||||
in
|
||||
bind_fold_list aux (typed_name.type_expression , []) path in
|
||||
let%bind expr' = type_expression e expr in
|
||||
let t_expr' = get_type_annotation expr' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"type of the expression to assign doesn't match left-hand-side"
|
||||
~expected:assign_tv
|
||||
~actual:t_expr'
|
||||
~expression:expr
|
||||
expr'.location) @@
|
||||
Ast_typed.assert_type_expression_eq (assign_tv , t_expr') in
|
||||
return (O.E_assign (typed_name , path' , expr')) (t_unit ())
|
||||
| E_let_in {binder ; rhs ; result} ->
|
||||
let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
|
||||
let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in
|
||||
let e' = Environment.add_ez_declaration (fst binder) rhs e in
|
||||
let%bind result = type_expression e' result in
|
||||
return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation
|
||||
| E_annotation (expr , te) ->
|
||||
let%bind tv = evaluate_type e te in
|
||||
let%bind expr' = type_expression ~tv_opt:tv e expr in
|
||||
let%bind type_annotation =
|
||||
O.merge_annotation
|
||||
(Some tv)
|
||||
(Some expr'.type_annotation)
|
||||
(internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
|
||||
ok {expr' with type_annotation}
|
||||
|
||||
|
||||
and type_constant (name:string) (lst:O.type_expression list) (tv_opt:O.type_expression option) (loc : Location.t) : (string * O.type_expression) result =
|
||||
(* Constant poorman's polymorphism *)
|
||||
let ct = Operators.Typer.constant_typers in
|
||||
let%bind typer =
|
||||
trace_option (unrecognized_constant name loc) @@
|
||||
Map.String.find_opt name ct in
|
||||
trace (constant_error loc lst tv_opt) @@
|
||||
typer lst tv_opt
|
||||
|
||||
let untype_type_expression (t:O.type_expression) : (I.type_expression) result =
|
||||
match t.simplified with
|
||||
| Some s -> ok s
|
||||
| _ -> fail @@ internal_assertion_failure "trying to untype generated type"
|
||||
|
||||
let untype_literal (l:O.literal) : I.literal result =
|
||||
let open I in
|
||||
match l with
|
||||
| Literal_unit -> ok Literal_unit
|
||||
| Literal_bool b -> ok (Literal_bool b)
|
||||
| Literal_nat n -> ok (Literal_nat n)
|
||||
| Literal_timestamp n -> ok (Literal_timestamp n)
|
||||
| Literal_tez n -> ok (Literal_tez n)
|
||||
| Literal_int n -> ok (Literal_int n)
|
||||
| Literal_string s -> ok (Literal_string s)
|
||||
| Literal_bytes b -> ok (Literal_bytes b)
|
||||
| Literal_address s -> ok (Literal_address s)
|
||||
| Literal_operation s -> ok (Literal_operation s)
|
||||
|
||||
let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
|
||||
let open I in
|
||||
let return e = ok e in
|
||||
match e.expression with
|
||||
| E_literal l ->
|
||||
let%bind l = untype_literal l in
|
||||
return (e_literal l)
|
||||
| E_constant (n, lst) ->
|
||||
let%bind lst' = bind_map_list untype_expression lst in
|
||||
return (e_constant n lst')
|
||||
| E_variable n ->
|
||||
return (e_variable n)
|
||||
| E_application (f, arg) ->
|
||||
let%bind f' = untype_expression f in
|
||||
let%bind arg' = untype_expression arg in
|
||||
return (e_application f' arg')
|
||||
| E_lambda {binder;input_type;output_type;result} ->
|
||||
let%bind input_type = untype_type_expression input_type in
|
||||
let%bind output_type = untype_type_expression output_type in
|
||||
let%bind result = untype_expression result in
|
||||
return (e_lambda binder (Some input_type) (Some output_type) result)
|
||||
| E_tuple lst ->
|
||||
let%bind lst' = bind_list
|
||||
@@ List.map untype_expression lst in
|
||||
return (e_tuple lst')
|
||||
| E_tuple_accessor (tpl, ind) ->
|
||||
let%bind tpl' = untype_expression tpl in
|
||||
return (e_accessor tpl' [Access_tuple ind])
|
||||
| E_constructor (n, p) ->
|
||||
let%bind p' = untype_expression p in
|
||||
return (e_constructor n p')
|
||||
| E_record r ->
|
||||
let%bind r' = bind_smap
|
||||
@@ SMap.map untype_expression r in
|
||||
return (e_record r')
|
||||
| E_record_accessor (r, s) ->
|
||||
let%bind r' = untype_expression r in
|
||||
return (e_accessor r' [Access_record s])
|
||||
| E_map m ->
|
||||
let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
|
||||
return (e_map m')
|
||||
| E_list lst ->
|
||||
let%bind lst' = bind_map_list untype_expression lst in
|
||||
return (e_list lst')
|
||||
| E_set lst ->
|
||||
let%bind lst' = bind_map_list untype_expression lst in
|
||||
return (e_set lst')
|
||||
| E_look_up dsi ->
|
||||
let%bind (a , b) = bind_map_pair untype_expression dsi in
|
||||
return (e_look_up a b)
|
||||
| E_matching (ae, m) ->
|
||||
let%bind ae' = untype_expression ae in
|
||||
let%bind m' = untype_matching untype_expression m in
|
||||
return (e_matching ae' m')
|
||||
| E_failwith ae ->
|
||||
let%bind ae' = untype_expression ae in
|
||||
return (e_failwith ae')
|
||||
| E_sequence _
|
||||
| E_loop _
|
||||
| E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression
|
||||
| E_let_in {binder;rhs;result} ->
|
||||
let%bind tv = untype_type_expression rhs.type_annotation in
|
||||
let%bind rhs = untype_expression rhs in
|
||||
let%bind result = untype_expression result in
|
||||
return (e_let_in (binder , (Some tv)) rhs result)
|
||||
|
||||
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
|
||||
let open I in
|
||||
match m with
|
||||
| Match_bool {match_true ; match_false} ->
|
||||
let%bind match_true = f match_true in
|
||||
let%bind match_false = f match_false in
|
||||
ok @@ Match_bool {match_true ; match_false}
|
||||
| Match_tuple (lst, b) ->
|
||||
let%bind b = f b in
|
||||
ok @@ Match_tuple (lst, b)
|
||||
| Match_option {match_none ; match_some = (v, some)} ->
|
||||
let%bind match_none = f match_none in
|
||||
let%bind some = f some in
|
||||
let match_some = fst v, some in
|
||||
ok @@ Match_option {match_none ; match_some}
|
||||
| Match_list {match_nil ; match_cons = (hd, tl, cons)} ->
|
||||
let%bind match_nil = f match_nil in
|
||||
let%bind cons = f cons in
|
||||
let match_cons = hd, tl, cons in
|
||||
ok @@ Match_list {match_nil ; match_cons}
|
||||
| Match_variant (lst , _) ->
|
||||
let aux ((a,b),c) =
|
||||
let%bind c' = f c in
|
||||
ok ((a,b),c') in
|
||||
let%bind lst' = bind_map_list aux lst in
|
||||
ok @@ Match_variant lst'
|
||||
@ -5,6 +5,7 @@
|
||||
simple-utils
|
||||
tezos-utils
|
||||
ast_typed
|
||||
typesystem
|
||||
mini_c
|
||||
)
|
||||
(preprocess
|
||||
|
||||
@ -219,6 +219,65 @@ module Typer = struct
|
||||
open Helpers.Typer
|
||||
open Ast_typed
|
||||
|
||||
module Operators_types = struct
|
||||
open Typesystem.Shorthands
|
||||
|
||||
let tc_subarg a b c = tc [a;b;c] [ (*TODO…*) ]
|
||||
let tc_sizearg a = tc [a] [ [int] ]
|
||||
let tc_packable a = tc [a] [ [int] ; [string] ; [bool] (*TODO…*) ]
|
||||
let tc_timargs a b c = tc [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
|
||||
let tc_divargs a b c = tc [a;b;c] [ (*TODO…*) ]
|
||||
let tc_modargs a b c = tc [a;b;c] [ (*TODO…*) ]
|
||||
let tc_addargs a b c = tc [a;b;c] [ (*TODO…*) ]
|
||||
|
||||
let t_none = forall "a" @@ fun a -> option a
|
||||
let t_sub = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_subarg a b c] => a --> b --> c (* TYPECLASS *)
|
||||
let t_some = forall "a" @@ fun a -> a --> option a
|
||||
let t_map_remove = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> map src dst
|
||||
let t_map_add = forall2 "src" "dst" @@ fun src dst -> src --> dst --> map src dst --> map src dst
|
||||
let t_map_update = forall2 "src" "dst" @@ fun src dst -> src --> option dst --> map src dst --> map src dst
|
||||
let t_map_mem = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> bool
|
||||
let t_map_find = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> dst
|
||||
let t_map_find_opt = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> option dst
|
||||
let t_map_fold = forall3 "src" "dst" "acc" @@ fun src dst acc -> ( ( (src * dst) * acc ) --> acc ) --> map src dst --> acc --> acc
|
||||
let t_map_map = forall3 "k" "v" "result" @@ fun k v result -> ((k * v) --> result) --> map k v --> map k result
|
||||
|
||||
(* TODO: the type of map_map_fold might be wrong, check it. *)
|
||||
let t_map_map_fold = forall4 "k" "v" "acc" "dst" @@ fun k v acc dst -> ( ((k * v) * acc) --> acc * dst ) --> map k v --> (k * v) --> (map k dst * acc)
|
||||
let t_map_iter = forall2 "k" "v" @@ fun k v -> ( (k * v) --> unit ) --> map k v --> unit
|
||||
let t_size = forall_tc "c" @@ fun c -> [tc_sizearg c] => c --> nat (* TYPECLASS *)
|
||||
let t_slice = nat --> nat --> string --> string
|
||||
let t_failwith = string --> unit
|
||||
let t_get_force = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> dst
|
||||
let t_int = nat --> int
|
||||
let t_bytes_pack = forall_tc "a" @@ fun a -> [tc_packable a] => a --> bytes (* TYPECLASS *)
|
||||
let t_bytes_unpack = forall_tc "a" @@ fun a -> [tc_packable a] => bytes --> a (* TYPECLASS *)
|
||||
let t_hash256 = bytes --> bytes
|
||||
let t_hash512 = bytes --> bytes
|
||||
let t_blake2b = bytes --> bytes
|
||||
let t_hash_key = key --> key_hash
|
||||
let t_check_signature = key --> signature --> bytes --> bool
|
||||
let t_sender = address
|
||||
let t_source = address
|
||||
let t_unit = unit
|
||||
let t_amount = tez
|
||||
let t_address = address
|
||||
let t_now = timestamp
|
||||
let t_transaction = forall "a" @@ fun a -> a --> tez --> contract a --> operation
|
||||
let t_get_contract = forall "a" @@ fun a -> contract a
|
||||
let t_abs = int --> nat
|
||||
let t_cons = forall "a" @@ fun a -> a --> list a --> list a
|
||||
let t_assertion = bool --> unit
|
||||
let t_times = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_timargs a b c] => a --> b --> c (* TYPECLASS *)
|
||||
let t_div = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_divargs a b c] => a --> b --> c (* TYPECLASS *)
|
||||
let t_mod = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_modargs a b c] => a --> b --> c (* TYPECLASS *)
|
||||
let t_add = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_addargs a b c] => a --> b --> c (* TYPECLASS *)
|
||||
let t_set_mem = forall "a" @@ fun a -> a --> set a --> bool
|
||||
let t_set_add = forall "a" @@ fun a -> a --> set a --> set a
|
||||
let t_set_remove = forall "a" @@ fun a -> a --> set a --> set a
|
||||
let t_not = bool --> bool
|
||||
end
|
||||
|
||||
let none = typer_0 "NONE" @@ fun tv_opt ->
|
||||
match tv_opt with
|
||||
| None -> simple_fail "untyped NONE"
|
||||
@ -647,6 +706,7 @@ module Typer = struct
|
||||
get_contract ;
|
||||
neg ;
|
||||
abs ;
|
||||
cons ;
|
||||
now ;
|
||||
slice ;
|
||||
address ;
|
||||
|
||||
60
src/typesystem/core.ml
Normal file
60
src/typesystem/core.ml
Normal file
@ -0,0 +1,60 @@
|
||||
type type_variable = string
|
||||
|
||||
let fresh_type_variable : ?name:string -> unit -> type_variable =
|
||||
let id = ref 0 in
|
||||
let inc () = id := !id + 1 in
|
||||
fun ?name () ->
|
||||
inc () ;
|
||||
match name with
|
||||
| None -> "type_variable_" ^ (string_of_int !id)
|
||||
| Some name -> "tv_" ^ name ^ "_" ^ (string_of_int !id)
|
||||
|
||||
|
||||
type constant_tag =
|
||||
| C_arrow (* * -> * -> * *)
|
||||
| C_option (* * -> * *)
|
||||
| C_tuple (* * … -> * *)
|
||||
| C_record (* ( label , * ) … -> * *)
|
||||
| C_variant (* ( label , * ) … -> * *)
|
||||
| C_map (* * -> * -> * *)
|
||||
| C_list (* * -> * *)
|
||||
| C_set (* * -> * *)
|
||||
| C_unit (* * *)
|
||||
| C_bool (* * *)
|
||||
| C_string (* * *)
|
||||
| C_nat (* * *)
|
||||
| C_tez (* * *)
|
||||
| C_timestamp (* * *)
|
||||
| C_int (* * *)
|
||||
| C_address (* * *)
|
||||
| C_bytes (* * *)
|
||||
| C_key_hash (* * *)
|
||||
| C_key (* * *)
|
||||
| C_signature (* * *)
|
||||
| C_operation (* * *)
|
||||
| C_contract (* * -> * *)
|
||||
|
||||
type label =
|
||||
| L_int of int
|
||||
| L_string of string
|
||||
|
||||
type type_value =
|
||||
| P_forall of (type_variable * type_constraint list * type_value)
|
||||
| P_variable of type_variable
|
||||
| P_constant of (constant_tag * type_value list)
|
||||
|
||||
and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *)
|
||||
and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *)
|
||||
and c_const = (type_variable * type_value)
|
||||
and c_equation = (type_value * type_value)
|
||||
and c_typeclass = (type_value list * typeclass)
|
||||
and c_access_label = (type_value * label * type_variable)
|
||||
|
||||
and type_constraint =
|
||||
(* | C_assignment of (type_variable * type_pattern) *)
|
||||
| C_equation of c_equation (* TVA = TVB *)
|
||||
| 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
|
||||
14
src/typesystem/dune
Normal file
14
src/typesystem/dune
Normal file
@ -0,0 +1,14 @@
|
||||
(library
|
||||
(name typesystem)
|
||||
(public_name ligo.typesystem)
|
||||
(libraries
|
||||
simple-utils
|
||||
tezos-utils
|
||||
ast_typed
|
||||
mini_c
|
||||
)
|
||||
(preprocess
|
||||
(pps ppx_let)
|
||||
)
|
||||
(flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
|
||||
)
|
||||
62
src/typesystem/shorthands.ml
Normal file
62
src/typesystem/shorthands.ml
Normal file
@ -0,0 +1,62 @@
|
||||
open Core
|
||||
|
||||
let tc type_vars allowed_list =
|
||||
Core.C_typeclass (type_vars , allowed_list)
|
||||
|
||||
let forall binder f =
|
||||
let () = ignore binder in
|
||||
let freshvar = fresh_type_variable () in
|
||||
P_forall (freshvar , [] , f (P_variable freshvar))
|
||||
|
||||
let forall_tc binder f =
|
||||
let () = ignore binder in
|
||||
let freshvar = fresh_type_variable () in
|
||||
let (tc, ty) = f (P_variable freshvar) in
|
||||
P_forall (freshvar , tc , ty)
|
||||
|
||||
let forall2 a b f =
|
||||
forall a @@ fun a' ->
|
||||
forall b @@ fun b' ->
|
||||
f a' b'
|
||||
|
||||
let forall3 a b c f =
|
||||
forall a @@ fun a' ->
|
||||
forall b @@ fun b' ->
|
||||
forall c @@ fun c' ->
|
||||
f a' b' c'
|
||||
|
||||
let forall4 a b c d f =
|
||||
forall a @@ fun a' ->
|
||||
forall b @@ fun b' ->
|
||||
forall c @@ fun c' ->
|
||||
forall d @@ fun d' ->
|
||||
f a' b' c' d'
|
||||
|
||||
let forall3_tc a b c f =
|
||||
forall a @@ fun a' ->
|
||||
forall b @@ fun b' ->
|
||||
forall_tc c @@ fun c' ->
|
||||
f a' b' c'
|
||||
|
||||
let (-->) arg ret = P_constant (C_arrow , [arg; ret])
|
||||
let (=>) tc ty = (tc , ty)
|
||||
let option t = P_constant (C_option , [t])
|
||||
let pair a b = P_constant (C_tuple , [a; b])
|
||||
let map k v = P_constant (C_map , [k; v])
|
||||
let unit = P_constant (C_unit , [])
|
||||
let list t = P_constant (C_list , [t])
|
||||
let set t = P_constant (C_set , [t])
|
||||
let bool = P_constant (C_bool , [])
|
||||
let string = P_constant (C_string , [])
|
||||
let nat = P_constant (C_nat , [])
|
||||
let tez = P_constant (C_tez , [])
|
||||
let timestamp = P_constant (C_timestamp , [])
|
||||
let int = P_constant (C_int , [])
|
||||
let address = P_constant (C_address , [])
|
||||
let bytes = P_constant (C_bytes , [])
|
||||
let key = P_constant (C_key , [])
|
||||
let key_hash = P_constant (C_key_hash , [])
|
||||
let signature = P_constant (C_signature , [])
|
||||
let operation = P_constant (C_operation , [])
|
||||
let contract t = P_constant (C_contract , [t])
|
||||
let ( * ) a b = pair a b
|
||||
2
src/typesystem/typesystem.ml
Normal file
2
src/typesystem/typesystem.ml
Normal file
@ -0,0 +1,2 @@
|
||||
module Core = Core
|
||||
module Shorthands = Shorthands
|
||||
0
src/union_find/.PartitionMain.tag
Normal file
0
src/union_find/.PartitionMain.tag
Normal file
1
src/union_find/.links
Normal file
1
src/union_find/.links
Normal file
@ -0,0 +1 @@
|
||||
../OCaml-build/Makefile
|
||||
21
src/union_find/LICENSE
Normal file
21
src/union_find/LICENSE
Normal file
@ -0,0 +1,21 @@
|
||||
MIT License
|
||||
|
||||
Copyright (c) 2018 Christian Rinderknecht
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all
|
||||
copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
SOFTWARE.
|
||||
4
src/union_find/Makefile.cfg
Normal file
4
src/union_find/Makefile.cfg
Normal file
@ -0,0 +1,4 @@
|
||||
SHELL := dash
|
||||
BFLAGS := -strict-sequence -w +A-48-4
|
||||
#OCAMLC := ocamlcp
|
||||
#OCAMLOPT := ocamloptp
|
||||
64
src/union_find/Partition.mli
Normal file
64
src/union_find/Partition.mli
Normal file
@ -0,0 +1,64 @@
|
||||
(** This module offers the abstract data type of a partition of
|
||||
classes of equivalent items (Union & Find). *)
|
||||
|
||||
(** The items are of type [Item.t], that is, they have to obey
|
||||
a total order, but also they must be printable to ease
|
||||
debugging. The signature [Item] is the input signature of
|
||||
the functor {!Partition.Make}. *)
|
||||
module type Item =
|
||||
sig
|
||||
(** Type of items *)
|
||||
type t
|
||||
|
||||
(** Same convention as {!Pervasives.compare} *)
|
||||
val compare : t -> t -> int
|
||||
|
||||
val to_string : t -> string
|
||||
end
|
||||
|
||||
(** The module signature [S] is the output signature of the functor
|
||||
{!Partition.Make}. *)
|
||||
module type S =
|
||||
sig
|
||||
type item
|
||||
type partition
|
||||
type t = partition
|
||||
|
||||
(** {1 Creation} *)
|
||||
|
||||
(** The value [empty] is an empty partition. *)
|
||||
val empty : partition
|
||||
|
||||
(** The value of [equiv i j p] is the partition [p] extended with
|
||||
the equivalence of items [i] and [j]. If both [i] and [j] are
|
||||
already known to be equivalent, then [equiv i j p == p]. *)
|
||||
val equiv : item -> item -> partition -> partition
|
||||
|
||||
(** The value of [alias i j p] is the partition [p] extended with
|
||||
the fact that item [i] is an alias of item [j]. This is the
|
||||
same as [equiv i j p], except that it is guaranteed that the
|
||||
item [i] is not the representative of its equivalence class in
|
||||
[alias i j p]. *)
|
||||
val alias : item -> item -> partition -> partition
|
||||
|
||||
(** {1 Projection} *)
|
||||
|
||||
(** The value of the call [repr i p] is the representative of item
|
||||
[i] in the partition [p]. The built-in exception [Not_found]
|
||||
is raised if [i] is not in [p]. *)
|
||||
val repr : item -> partition -> item
|
||||
|
||||
(** The side-effect of the call [print p] is the printing of the
|
||||
partition [p] on standard output, based on [Ord.to_string]. *)
|
||||
val print : partition -> unit
|
||||
|
||||
(** {1 Predicates} *)
|
||||
|
||||
(** The value of [is_equiv i j p] is [true] if, and only if, the
|
||||
items [i] and [j] belong to the same equivalence class in the
|
||||
partition [p], that is, [i] and [j] have the same
|
||||
representative. *)
|
||||
val is_equiv : item -> item -> partition -> bool
|
||||
end
|
||||
|
||||
module Make (Ord : Item) : S with type item = Ord.t
|
||||
47
src/union_find/Partition0.ml
Normal file
47
src/union_find/Partition0.ml
Normal file
@ -0,0 +1,47 @@
|
||||
(* Naive persistent implementation of Union/Find: O(n^2) worst case *)
|
||||
|
||||
module Make (Item: Partition.Item) =
|
||||
struct
|
||||
|
||||
type item = Item.t
|
||||
type repr = item (** Class representatives *)
|
||||
|
||||
let equal i j = Item.compare i j = 0
|
||||
|
||||
module ItemMap = Map.Make (Item)
|
||||
|
||||
type height = int
|
||||
|
||||
type partition = item ItemMap.t
|
||||
type t = partition
|
||||
|
||||
let empty = ItemMap.empty
|
||||
|
||||
let rec repr item partition =
|
||||
let parent = ItemMap.find item partition in
|
||||
if equal parent item
|
||||
then item
|
||||
else repr parent partition
|
||||
|
||||
let is_equiv (i: item) (j: item) (p: partition) =
|
||||
equal (repr i p) (repr j p)
|
||||
|
||||
let get_or_set (i: item) (p: partition) : item * partition =
|
||||
try repr i p, p with Not_found -> i, ItemMap.add i i p
|
||||
|
||||
let equiv (i: item) (j :item) (p: partition) : partition =
|
||||
let ri, p = get_or_set i p in
|
||||
let rj, p = get_or_set j p in
|
||||
if equal ri rj then p else ItemMap.add ri rj p
|
||||
|
||||
let alias = equiv
|
||||
|
||||
(* Printing *)
|
||||
|
||||
let print p =
|
||||
let print src dst =
|
||||
Printf.printf "%s -> %s\n"
|
||||
(Item.to_string src) (Item.to_string dst)
|
||||
in ItemMap.iter print p
|
||||
|
||||
end
|
||||
69
src/union_find/Partition1.ml
Normal file
69
src/union_find/Partition1.ml
Normal file
@ -0,0 +1,69 @@
|
||||
(* Persistent implementation of Union/Find with height-balanced
|
||||
forests and without path compression: O(n*log(n)).
|
||||
|
||||
In the definition of type [t], the height component is that of the
|
||||
source, that is, if [ItemMap.find i m = (j,h)], then [h] is the
|
||||
height of [i] (_not_ [j]).
|
||||
*)
|
||||
|
||||
module Make (Item: Partition.Item) =
|
||||
struct
|
||||
|
||||
type item = Item.t
|
||||
type repr = item (** Class representatives *)
|
||||
|
||||
let equal i j = Item.compare i j = 0
|
||||
|
||||
module ItemMap = Map.Make (Item)
|
||||
|
||||
type height = int
|
||||
|
||||
type partition = (item * height) ItemMap.t
|
||||
type t = partition
|
||||
|
||||
let empty = ItemMap.empty
|
||||
|
||||
let rec seek (i: item) (p: partition) : repr * height =
|
||||
let j, _ as i' = ItemMap.find i p in
|
||||
if equal i j then i' else seek j p
|
||||
|
||||
let repr item partition = fst (seek item partition)
|
||||
|
||||
let is_equiv (i: item) (j: item) (p: partition) =
|
||||
equal (repr i p) (repr j p)
|
||||
|
||||
let get_or_set (i: item) (p: partition) =
|
||||
try seek i p, p with
|
||||
Not_found -> let i' = i,0 in (i', ItemMap.add i i' p)
|
||||
|
||||
let equiv (i: item) (j: item) (p: partition) : partition =
|
||||
let (ri,hi), p = get_or_set i p in
|
||||
let (rj,hj), p = get_or_set j p in
|
||||
let add = ItemMap.add in
|
||||
if equal ri rj
|
||||
then p
|
||||
else if hi > hj
|
||||
then add rj (ri,hj) p
|
||||
else add ri (rj,hi) (if hi < hj then p else add rj (rj,hj+1) p)
|
||||
|
||||
let alias (i: item) (j: item) (p: partition) : partition =
|
||||
let (ri,hi), p = get_or_set i p in
|
||||
let (rj,hj), p = get_or_set j p in
|
||||
let add = ItemMap.add in
|
||||
if equal ri rj
|
||||
then p
|
||||
else if hi = hj || equal ri i
|
||||
then add ri (rj,hi) @@ add rj (rj, max hj (hi+1)) p
|
||||
else if hi < hj then add ri (rj,hi) p
|
||||
else add rj (ri,hj) p
|
||||
|
||||
(* Printing *)
|
||||
|
||||
let print (p: partition) =
|
||||
let print i (j,hi) =
|
||||
let _,hj = ItemMap.find j p in
|
||||
Printf.printf "%s,%d -> %s,%d\n"
|
||||
(Item.to_string i) hi (Item.to_string j) hj
|
||||
in ItemMap.iter print p
|
||||
|
||||
end
|
||||
115
src/union_find/Partition2.ml
Normal file
115
src/union_find/Partition2.ml
Normal file
@ -0,0 +1,115 @@
|
||||
(** Persistent implementation of the Union/Find algorithm with
|
||||
height-balanced forests and without path compression. *)
|
||||
|
||||
module Make (Item: Partition.Item) =
|
||||
struct
|
||||
|
||||
type item = Item.t
|
||||
type repr = item (** Class representatives *)
|
||||
|
||||
let equal i j = Item.compare i j = 0
|
||||
|
||||
type height = int
|
||||
|
||||
(** Each equivalence class is implemented by a Catalan tree linked
|
||||
upwardly and otherwise is a link to another node. Those trees
|
||||
are height-balanced. The type [node] implements nodes in those
|
||||
trees. *)
|
||||
type node =
|
||||
Root of height
|
||||
(** The value of [Root h] denotes the root of a tree, that is,
|
||||
the representative of the associated class. The height [h]
|
||||
is that of the tree, so a tree reduced to its root alone has
|
||||
heigh 0. *)
|
||||
|
||||
| Link of item * height
|
||||
(** If not a root, a node is a link to another node. Because the
|
||||
links are upward, that is, bottom-up, and we seek a purely
|
||||
functional implementation, we need to uncouple the nodes and
|
||||
the items here, so the first component of [Link] is an item,
|
||||
not a node. That is why the type [node] is not recursive,
|
||||
and called [node], not [tree]: to become a traversable tree,
|
||||
it needs to be complemented by the type [partition] below to
|
||||
associate items back to nodes. In order to follow a path
|
||||
upward in the tree until the root, we start from a link node
|
||||
giving us the next item, then find the node corresponding to
|
||||
the item thanks to [partition], and again until we arrive at
|
||||
the root.
|
||||
|
||||
The height component is that of the source of the link, that
|
||||
is, [h] is the height of the node linking to the node [Link
|
||||
(j,h)], _not_ of [j], except when [equal i j]. *)
|
||||
|
||||
module ItemMap = Map.Make (Item)
|
||||
|
||||
(** The type [partition] implements a partition of classes of
|
||||
equivalent items by means of a map from items to nodes of type
|
||||
[node] in trees. *)
|
||||
type partition = node ItemMap.t
|
||||
|
||||
type t = partition
|
||||
|
||||
let empty = ItemMap.empty
|
||||
|
||||
let root (item, height) = ItemMap.add item (Root height)
|
||||
|
||||
let link (src, height) dst = ItemMap.add src (Link (dst, height))
|
||||
|
||||
let rec seek (i: item) (p: partition) : repr * height =
|
||||
match ItemMap.find i p with
|
||||
Root hi -> i,hi
|
||||
| Link (j,_) -> seek j p
|
||||
|
||||
let repr item partition = fst (seek item partition)
|
||||
|
||||
let is_equiv (i: item) (j: item) (p: partition) =
|
||||
equal (repr i p) (repr j p)
|
||||
|
||||
let get_or_set (i: item) (p: partition) =
|
||||
try seek i p, p with
|
||||
Not_found -> let n = i,0 in (n, root n p)
|
||||
|
||||
let equiv (i: item) (j: item) (p: partition) : partition =
|
||||
let (ri,hi as ni), p = get_or_set i p in
|
||||
let (rj,hj as nj), p = get_or_set j p in
|
||||
if equal ri rj
|
||||
then p
|
||||
else if hi > hj
|
||||
then link nj ri p
|
||||
else link ni rj (if hi < hj then p else root (rj, hj+1) p)
|
||||
|
||||
(** The call [alias i j p] results in the same partition as [equiv
|
||||
i j p], except that [i] is not the representative of its class
|
||||
in [alias i j p] (whilst it may be in [equiv i j p]).
|
||||
|
||||
This property is irrespective of the heights of the
|
||||
representatives of [i] and [j], that is, of the trees
|
||||
implementing their classes. If [i] is not a representative of
|
||||
its class before calling [alias], then the height criteria is
|
||||
applied (which, without the constraint above, would yield a
|
||||
height-balanced new tree). *)
|
||||
let alias (i: item) (j: item) (p: partition) : partition =
|
||||
let (ri,hi as ni), p = get_or_set i p in
|
||||
let (rj,hj as nj), p = get_or_set j p in
|
||||
if equal ri rj
|
||||
then p
|
||||
else if hi = hj || equal ri i
|
||||
then link ni rj @@ root (rj, max hj (hi+1)) p
|
||||
else if hi < hj then link ni rj p
|
||||
else link nj ri p
|
||||
|
||||
(** {1 Printing} *)
|
||||
|
||||
let print (p: partition) =
|
||||
let print i node =
|
||||
let hi, hj, j =
|
||||
match node with
|
||||
Root hi -> hi,hi,i
|
||||
| Link (j,hi) ->
|
||||
match ItemMap.find j p with
|
||||
Root hj | Link (_,hj) -> hi,hj,j in
|
||||
Printf.printf "%s,%d -> %s,%d\n"
|
||||
(Item.to_string i) hi (Item.to_string j) hj
|
||||
in ItemMap.iter print p
|
||||
|
||||
end
|
||||
86
src/union_find/Partition3.ml
Normal file
86
src/union_find/Partition3.ml
Normal file
@ -0,0 +1,86 @@
|
||||
(* Destructive implementation of union/find with height-balanced
|
||||
forests but without path compression: O(n*log(n)). *)
|
||||
|
||||
module Make (Item: Partition.Item) =
|
||||
struct
|
||||
|
||||
type item = Item.t
|
||||
type repr = item (** Class representatives *)
|
||||
|
||||
let equal i j = Item.compare i j = 0
|
||||
|
||||
type height = int
|
||||
|
||||
(** Each equivalence class is implemented by a Catalan tree linked
|
||||
upwardly and otherwise is a link to another node. Those trees
|
||||
are height-balanced. The type [node] implements nodes in those
|
||||
trees. *)
|
||||
type node = {item: item; mutable height: int; mutable parent: node}
|
||||
|
||||
module ItemMap = Map.Make (Item)
|
||||
|
||||
(** The type [partition] implements a partition of classes of
|
||||
equivalent items by means of a map from items to nodes of type
|
||||
[node] in trees. *)
|
||||
type partition = node ItemMap.t
|
||||
|
||||
type t = partition
|
||||
|
||||
let empty = ItemMap.empty
|
||||
|
||||
(** The function [repr] is faster than a persistent implementation
|
||||
in the worst case because, in the latter case, the cost is O(log n)
|
||||
for accessing each node in the path to the root, whereas, in the
|
||||
former, only the access to the first node in the path incurs a cost
|
||||
of O(log n) -- the other nodes are accessed in constant time by
|
||||
following the [next] field of type [node]. *)
|
||||
let seek (i: item) (p: partition) : node =
|
||||
let rec find_root node =
|
||||
if node.parent == node then node else find_root node.parent
|
||||
in find_root (ItemMap.find i p)
|
||||
|
||||
let repr item partition = (seek item partition).item
|
||||
|
||||
let is_equiv (i: item) (j: item) (p: partition) =
|
||||
equal (repr i p) (repr j p)
|
||||
|
||||
let get_or_set item (p: partition) =
|
||||
try seek item p, p with
|
||||
Not_found -> let rec loop = {item; height=0; parent=loop}
|
||||
in loop, ItemMap.add item loop p
|
||||
|
||||
let link src dst = src.parent <- dst
|
||||
|
||||
let equiv (i: item) (j: item) (p: partition) : partition =
|
||||
let ni,p = get_or_set i p in
|
||||
let nj,p = get_or_set j p in
|
||||
let hi,hj = ni.height, nj.height in
|
||||
let () =
|
||||
if not (equal ni.item nj.item)
|
||||
then if hi > hj
|
||||
then link nj ni
|
||||
else (link ni nj; nj.height <- max hj (hi+1))
|
||||
in p
|
||||
|
||||
let alias (i: item) (j: item) (p: partition) : partition =
|
||||
let ni,p = get_or_set i p in
|
||||
let nj,p = get_or_set j p in
|
||||
let hi,hj = ni.height, nj.height in
|
||||
let () =
|
||||
if not (equal ni.item nj.item)
|
||||
then if hi = hj || equal ni.item i
|
||||
then (link ni nj; nj.height <- max hj (hi+1))
|
||||
else if hi < hj then link ni nj
|
||||
else link nj ni
|
||||
in p
|
||||
|
||||
(* Printing *)
|
||||
|
||||
let print p =
|
||||
let print _ node =
|
||||
Printf.printf "%s,%d -> %s,%d\n"
|
||||
(Item.to_string node.item) node.height
|
||||
(Item.to_string node.parent.item) node.parent.height
|
||||
in ItemMap.iter print p
|
||||
|
||||
end
|
||||
40
src/union_find/PartitionMain.ml
Normal file
40
src/union_find/PartitionMain.ml
Normal file
@ -0,0 +1,40 @@
|
||||
module Int =
|
||||
struct
|
||||
type t = int
|
||||
let compare (i: int) (j: int) = Pervasives.compare i j
|
||||
let to_string = string_of_int
|
||||
end
|
||||
|
||||
module Test (Part: Partition.S with type item = Int.t) =
|
||||
struct
|
||||
open Part
|
||||
|
||||
let () = empty
|
||||
|> equiv 4 3
|
||||
|> equiv 3 8
|
||||
|> equiv 6 5
|
||||
|> equiv 9 4
|
||||
|> equiv 2 1
|
||||
|> equiv 8 9
|
||||
|> equiv 5 0
|
||||
|> equiv 7 2
|
||||
|> equiv 6 1
|
||||
|> equiv 1 0
|
||||
|> equiv 6 7
|
||||
|> equiv 8 0
|
||||
|> equiv 7 7
|
||||
|> equiv 10 10
|
||||
|> print
|
||||
end
|
||||
|
||||
|
||||
module Test0 = Test (Partition0.Make(Int))
|
||||
let () = print_newline ()
|
||||
|
||||
module Test1 = Test (Partition1.Make(Int))
|
||||
let () = print_newline ()
|
||||
|
||||
module Test2 = Test (Partition2.Make(Int))
|
||||
let () = print_newline ()
|
||||
|
||||
module Test3 = Test (Partition3.Make(Int))
|
||||
39
src/union_find/README.md
Normal file
39
src/union_find/README.md
Normal file
@ -0,0 +1,39 @@
|
||||
# Some implementations in OCaml of the Union/Find algorithm
|
||||
|
||||
All modules implementing Union/Find can be coerced by the same
|
||||
signature `Partition.S`.
|
||||
|
||||
Note the function `alias` which is equivalent to `equiv`, but not
|
||||
symmetric: `alias x y` means that `x` is an alias of `y`, which
|
||||
translates in the present context as `x` not being the representative
|
||||
of the equivalence class containing the equivalence between `x` and
|
||||
`y`. The function `alias` is useful when managing aliases during the
|
||||
static analyses of programming languages, so the representatives of
|
||||
the classes are always the original object.
|
||||
|
||||
The module `PartitionMain` tests each with the same equivalence
|
||||
relations.
|
||||
|
||||
## `Partition0.ml`
|
||||
|
||||
This is a naive, persistent implementation of Union/Find featuring an
|
||||
asymptotic worst case cost of O(n^2).
|
||||
|
||||
## `Partition1.ml`
|
||||
|
||||
This is a persistent implementation of Union/Find with height-balanced
|
||||
forests and without path compression, featuring an asymptotic worst
|
||||
case cost of O(n*log(n)).
|
||||
|
||||
## `Partition2.ml`
|
||||
|
||||
This is an alternate version of `Partition1.ml`, using a different
|
||||
data type.
|
||||
|
||||
## `Partition3.ml`
|
||||
|
||||
This is a destructive implementation of Union/Find with
|
||||
height-balanced forests but without path compression, featuring an
|
||||
asymptotic worst case of O(n*log(n)). In practice, though, this
|
||||
implementation should be faster than the previous ones, due to a
|
||||
smaller multiplicative constant term.
|
||||
14
src/union_find/build.sh
Executable file
14
src/union_find/build.sh
Executable file
@ -0,0 +1,14 @@
|
||||
#!/bin/sh
|
||||
set -x
|
||||
ocamlfind ocamlc -strict-sequence -w +A-48-4 -c Partition.mli
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition0.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition2.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition1.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition3.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition1.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition3.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition0.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition2.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c PartitionMain.ml
|
||||
ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c PartitionMain.ml
|
||||
ocamlfind ocamlopt -o PartitionMain.opt Partition0.cmx Partition1.cmx Partition2.cmx Partition3.cmx PartitionMain.cmx
|
||||
3
src/union_find/clean.sh
Executable file
3
src/union_find/clean.sh
Executable file
@ -0,0 +1,3 @@
|
||||
#!/bin/sh
|
||||
|
||||
\rm -f *.cmi *.cmo *.cmx *.o *.byte *.opt
|
||||
16
src/union_find/dune
Normal file
16
src/union_find/dune
Normal file
@ -0,0 +1,16 @@
|
||||
(library
|
||||
(name union_find)
|
||||
(public_name ligo.union_find)
|
||||
(wrapped false) ;; TODO: do we need this?
|
||||
(modules Partition0 Partition1 Partition2 Partition3 Partition Union_find)
|
||||
(modules_without_implementation Partition)
|
||||
;; (preprocess
|
||||
;; (pps simple-utils.ppx_let_generalized)
|
||||
;; )
|
||||
;; (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
|
||||
)
|
||||
|
||||
(test
|
||||
(modules PartitionMain)
|
||||
(libraries UnionFind)
|
||||
(name PartitionMain))
|
||||
2
src/union_find/union_find.ml
Normal file
2
src/union_find/union_find.ml
Normal file
@ -0,0 +1,2 @@
|
||||
module Partition = Partition
|
||||
module Partition0 = Partition0
|
||||
1
vendors/ligo-utils/simple-utils/trace.ml
vendored
1
vendors/ligo-utils/simple-utils/trace.ml
vendored
@ -667,6 +667,7 @@ let bind_map_pair f (a, b) =
|
||||
bind_pair (f a, f b)
|
||||
|
||||
|
||||
|
||||
(**
|
||||
Wraps a call that might trigger an exception in a result.
|
||||
*)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user