diff --git a/bin/repl.ml b/bin/repl.ml index 4364a3ee3..9c7727086 100644 --- a/bin/repl.ml +++ b/bin/repl.ml @@ -185,7 +185,7 @@ let rec directives : (string * ((Context.t -> string list -> Context.t) * string else (Module_hacks.Name.prettify name) in Printf.fprintf stderr " %-16s : %s\n" - name ty) + name ty) (* TODO(dhil): should really "prettify" ty here too as it may contain unique labels that have been expanded. *) nenv (); context), "display the current value environment"); diff --git a/core/buildTables.ml b/core/buildTables.ml index 5ac05cb13..5d5421d5d 100644 --- a/core/buildTables.ml +++ b/core/buildTables.ml @@ -255,7 +255,7 @@ struct let bindings tyenv bound_vars cont_vars bs = let o = new visitor tyenv bound_vars cont_vars in - let _ = o#computation (bs, Return (Extend (StringMap.empty, None))) in () + let _ = o#computation (bs, Return (Extend (Label.Map.empty, None))) in () let program tyenv bound_vars cont_vars e = let _ = (new visitor tyenv bound_vars cont_vars)#computation e in () diff --git a/core/channelVarUtils.ml b/core/channelVarUtils.ml index 369296a7a..7ff50a7a9 100644 --- a/core/channelVarUtils.ml +++ b/core/channelVarUtils.ml @@ -11,9 +11,9 @@ let variables_in_computation comp = let variable_set = ref IntSet.empty in let add_variable var = variable_set := (IntSet.add var !variable_set) in - let rec traverse_stringmap : 'a . ('a -> unit) -> 'a stringmap -> unit = + let rec traverse_name_map : 'a . ('a -> unit) -> 'a name_map -> unit = fun proj_fn smap -> (* (proj_fn: 'a . 'a -> 'b) (smap: 'a stringmap) : unit = *) - StringMap.fold (fun _ v _ -> proj_fn v) smap () + Label.Map.fold (fun _ v _ -> proj_fn v) smap () and traverse_value = function | Variable v -> add_variable v | Closure (_, _, value) @@ -24,13 +24,13 @@ let variables_in_computation comp = | Coerce (value, _) | Erase (_, value) -> traverse_value value | XmlNode (_, v_map, vs) -> - traverse_stringmap (traverse_value) v_map; + traverse_name_map (traverse_value) v_map; List.iter traverse_value vs | ApplyPure (v, vs) -> traverse_value v; List.iter traverse_value vs | Extend (v_map, v_opt) -> - traverse_stringmap (traverse_value) v_map; + traverse_name_map (traverse_value) v_map; begin match v_opt with | Some v -> traverse_value v | None -> () end | Constant _ -> () and traverse_tail_computation = function @@ -42,7 +42,7 @@ let variables_in_computation comp = traverse_value v; List.iter traverse_computation [c1 ; c2] | Case (scrutinee, cases, case_opt) -> traverse_value scrutinee; - traverse_stringmap (fun (_, c) -> traverse_computation c) cases; + traverse_name_map (fun (_, c) -> traverse_computation c) cases; OptionUtils.opt_iter (fun (_, c) -> traverse_computation c) case_opt and traverse_fundef {fn_binder = bnd; _} = let fun_var = Var.var_of_binder bnd in @@ -109,7 +109,7 @@ let variables_in_computation comp = | DoOperation (_, vs, _) -> List.iter (traverse_value) vs | Choice (v, clauses) -> traverse_value v; - traverse_stringmap (fun (_, c) -> + traverse_name_map (fun (_, c) -> traverse_computation c) clauses | Lens (value, _) | LensSerial { lens = value; _ } @@ -124,7 +124,7 @@ let variables_in_computation comp = and traverse_clause (_, _, c) = traverse_computation c and traverse_handler (h: Ir.handler) = traverse_computation (h.ih_comp); - traverse_stringmap (traverse_clause) h.ih_cases; + traverse_name_map (traverse_clause) h.ih_cases; traverse_computation (snd h.ih_return) in traverse_computation comp; diff --git a/core/closures.ml b/core/closures.ml index 7c7d2145f..2a07ca9e0 100644 --- a/core/closures.ml +++ b/core/closures.ml @@ -428,9 +428,9 @@ struct let close f zs tyargs = Closure (f, tyargs, Extend (List.fold_right (fun (zname, zv) fields -> - StringMap.add zname zv fields) + Label.Map.add zname zv fields) zs - StringMap.empty, None)) + Label.Map.empty, None)) class visitor tenv fenv = object (o : 'self) inherit IrTraversals.Transform.visitor(tenv) as super @@ -456,7 +456,7 @@ struct if IntSet.mem x cvars then (* We cannot return t as the type of the result here. If x refers to a hoisted function that was generalised, then t has additional quantifiers that are not present in the corresponding type of projecting x from parent_env *) - let projected_t = TypeUtils.project_type (string_of_int x) (thd3 (o#var parent_env)) in + let projected_t = TypeUtils.project_type (Label.of_int x) (thd3 (o#var parent_env)) in Project (string_of_int x, Variable parent_env), projected_t else if IntMap.mem x fenv then let zs = (IntMap.find x fenv).termvars in @@ -476,7 +476,7 @@ struct (fun b -> let z = Var.var_of_binder b in let v = fst (var_val z) in - (string_of_int z, v)) + (Label.of_int z, v)) zs in close x zs tyargs, overall_type @@ -534,14 +534,14 @@ struct | [], [] -> o, None | _ -> let zt = - Types.make_record_type + Types.(make_record_type (List.fold_left (fun fields b -> let x = Var.var_of_binder b in let xt = Var.type_of_binder b in - StringMap.add (string_of_int x) xt fields) - StringMap.empty - zs) + Label.Map.add (Label.of_int x) xt fields) + Label.Map.empty + zs)) in (* fresh variable for the closure environment *) let zb = Var.(fresh_binder (make_local_info (zt, "env_" ^ string_of_int f))) in @@ -610,14 +610,14 @@ struct | [], [] -> o, None | _ -> let zt = - Types.make_record_type + Types.(make_record_type (List.fold_left (fun fields b -> let x = Var.var_of_binder b in let xt = Var.type_of_binder b in - StringMap.add (string_of_int x) xt fields) - StringMap.empty - zs) + Label.Map.add (Label.of_int x) xt fields) + Label.Map.empty + zs)) in (* fresh variable for the closure environment *) let zb = Var.(fresh_binder (make_local_info (zt, "env_" ^ string_of_int f))) in diff --git a/core/commonTypes.ml b/core/commonTypes.ml index 8db12331b..332872e90 100644 --- a/core/commonTypes.ml +++ b/core/commonTypes.ml @@ -282,11 +282,6 @@ module Name = struct [@@deriving show] end -module Label = struct - type t = string - [@@deriving show] -end - module ForeignLanguage = struct type t = | JavaScript diff --git a/core/compilePatterns.ml b/core/compilePatterns.ml index e46c71c45..c76a1c812 100644 --- a/core/compilePatterns.ml +++ b/core/compilePatterns.ml @@ -29,22 +29,22 @@ struct type t = | Any | Nil - | Cons of t * t - | Variant of Name.t * t - | Operation of Name.t * t list * t - | Negative of StringSet.t - | Record of t StringMap.t * t option - | Constant of Constant.t - | Variable of binder - | As of binder * t - | HasType of t * Types.datatype + | Cons of t * t + | Variant of Label.t * t + | Operation of Label.t * t list * t + | Negative of Label.Set.t + | Record of t Label.Map.t * t option + | Constant of Constant.t + | Variable of binder + | As of binder * t + | HasType of t * Types.datatype [@@deriving show] type context = | CNil | CCons - | CVariant of string - | CNVariant of StringSet.t + | CVariant of Label.t + | CNVariant of Label.Set.t | CConstant of Constant.t | CNConstant of ConstSet.t @@ -138,15 +138,15 @@ let rec desugar_pattern : Types.row -> Sugartypes.Pattern.with_pos -> Pattern.t in let k, env' = desugar_pattern k in Pattern.Operation (name, ps, k), env ++ env' - | Negative names -> Pattern.Negative (StringSet.from_list names), empty + | Negative names -> Pattern.Negative (Label.Set.from_list names), empty | Record (bs, p) -> let bs, env = List.fold_right (fun (name, p) (bs, env) -> let p, env' = desugar_pattern p in - StringMap.add name p bs, env ++ env') + Label.Map.add name p bs, env ++ env') bs - (StringMap.empty, empty) in + (Label.Map.empty, empty) in let p, env = match p with | None -> None, env @@ -156,7 +156,7 @@ let rec desugar_pattern : Types.row -> Sugartypes.Pattern.with_pos -> Pattern.t in Pattern.Record (bs, p), env | Tuple ps -> - let bs = mapIndex (fun p i -> (string_of_int (i+1), p)) ps in + let bs = mapIndex (fun p i -> (Label.of_int (i+1), p)) ps in desugar_pattern (WithPos.make ~pos (Record (bs, None))) | Constant constant -> Pattern.Constant constant, empty @@ -258,7 +258,7 @@ let let_pattern : raw_env -> Pattern.t -> value * Types.datatype -> computation let case_type = TypeUtils.variant_at name t in let case_binder, case_variable = Var.fresh_var_of_type case_type in let body = lp case_type patt (Variable case_variable) body in - let cases = StringMap.singleton name (case_binder, body) in + let cases = Label.Map.singleton name (case_binder, body) in [], Case (value, cases, None) | Pattern.Negative names -> (* The following expands the negative pattern into @@ -273,18 +273,18 @@ let let_pattern : raw_env -> Pattern.t -> value * Types.datatype -> computation } *) let negative_cases, t' = - StringSet.fold + Label.Set.fold (fun label (cases, t) -> let case_type = TypeUtils.variant_at label t in let case_binder = Var.fresh_binder_of_type case_type in let body = ([], Special (Wrong body_type)) in - let cases' = StringMap.add label (case_binder, body) cases in + let cases' = Label.Map.add label (case_binder, body) cases in let t' = let row = TypeUtils.extract_row t in Types.Variant (Types.row_with (label, Types.Absent) row) in (cases', t')) - names (StringMap.empty, t) + names (Label.Map.empty, t) in let success_case = let case_binder = Var.fresh_binder_of_type t' in @@ -297,19 +297,19 @@ let let_pattern : raw_env -> Pattern.t -> value * Types.datatype -> computation | None -> body | Some p -> let names = - StringMap.fold + Label.Map.fold (fun name _ names -> - StringSet.add name names) + Label.Set.add name names) fields - StringSet.empty in + Label.Set.empty in let rt = TypeUtils.erase_type names t in lp rt p (Erase (names, value)) body (* lp rt p (`Coerce (value, rt)) body *) in - StringMap.fold + Label.Map.fold (fun name p body -> let t' = (TypeUtils.project_type name t) in - (lp t' p (Project (name, value)) body)) + (lp t' p (Project (Label.name name, value)) body)) fields body | Pattern.Constant c -> @@ -404,21 +404,21 @@ let arrange_list_clauses : clause list -> (annotated_clause list * annotated_cla (* arrange variant clauses by constructor *) let arrange_variant_clauses - : clause list -> (annotated_clause list) StringMap.t = + : clause list -> (annotated_clause list) Label.Map.t = fun clauses -> (List.fold_right (fun (ps, body) env -> match ps with | (annotation, Pattern.Variant (name, pattern))::ps -> let annotated_clauses = - if StringMap.mem name env then - StringMap.find name env + if Label.Map.mem name env then + Label.Map.find name env else [] in let pattern = reduce_pattern pattern in - StringMap.add name ((annotation, (pattern::ps, body))::annotated_clauses) env + Label.Map.add name ((annotation, (pattern::ps, body))::annotated_clauses) env | _ -> assert false - ) clauses StringMap.empty) + ) clauses Label.Map.empty) (* arrange constant clauses by constant value *) let arrange_constant_clauses @@ -444,7 +444,7 @@ let arrange_constant_clauses This function flattens all the record clauses. *) let arrange_record_clauses - : clause list -> (annotated_pattern StringMap.t * annotated_pattern option * annotated_clause) list = + : clause list -> (annotated_pattern Label.Map.t * annotated_pattern option * annotated_clause) list = fun clauses -> let rec flatten = function @@ -452,16 +452,16 @@ let arrange_record_clauses bs, None | Pattern.Record (bs, Some p) -> let bs', p' = flatten p in - StringMap.union_disjoint bs bs', p' + Label.Map.union_disjoint bs bs', p' | p -> - StringMap.empty, Some p + Label.Map.empty, Some p in List.fold_right (fun (ps, body) xs -> match ps with | (annotation, p)::ps -> let bs, p = flatten p in - let bs = StringMap.map reduce_pattern bs in + let bs = Label.Map.map reduce_pattern bs in let p = opt_map reduce_pattern p in (bs, p, (annotation, (ps, body)))::xs | _ -> assert false @@ -616,7 +616,7 @@ and match_list *) and match_variant - : var list -> (annotated_clause list) StringMap.t -> bound_computation -> var -> bound_computation = + : var list -> (annotated_clause list) Label.Map.t -> bound_computation -> var -> bound_computation = fun vars bs def var env -> let t = lookup_type var env in @@ -624,14 +624,14 @@ and match_variant if mem_context var env then lookup_context var env else - Pattern.CNVariant StringSet.empty, Variable var + Pattern.CNVariant Label.Set.empty, Variable var in match context with | Pattern.CVariant name -> - if StringMap.mem name bs then + if Label.Map.mem name bs then match cexp with | Inject (_, (Variable case_variable), _) -> - let annotated_clauses = StringMap.find name bs in + let annotated_clauses = Label.Map.find name bs in (* let case_type = lookup_type case_variable env in *) (* let inject_type = TypeUtils.inject_type name case_type in *) let clauses = apply_annotations cexp annotated_clauses in @@ -641,9 +641,9 @@ and match_variant def env | Pattern.CNVariant names -> let cases, cs = - StringMap.fold + Label.Map.fold (fun name annotated_clauses (cases, cs) -> - if StringSet.mem name names then + if Label.Set.mem name names then (cases, cs) else let case_type = TypeUtils.variant_at name t in @@ -653,20 +653,20 @@ and match_variant let match_env = bind_context var (Pattern.CVariant name, - Inject (name, Variable case_variable, t)) match_env in + Inject (Label.name name, Variable case_variable, t)) match_env in let clauses = apply_annotations - (Inject (name, Variable case_variable, t)) annotated_clauses + (Inject (Label.name name, Variable case_variable, t)) annotated_clauses in - (StringMap.add name + (Label.Map.add name (case_binder, match_cases (case_variable::vars) clauses def match_env) cases, - StringSet.add name cs)) + Label.Set.add name cs)) bs - (StringMap.empty, names) in + (Label.Map.empty, names) in let default_type = - StringSet.fold + Label.Set.fold (fun name t -> let _, t = TypeUtils.split_variant_type name t in t) cs t in begin @@ -703,21 +703,21 @@ and match_negative if mem_context var env then lookup_context var env else - Pattern.CNVariant StringSet.empty, Variable var + Pattern.CNVariant Label.Set.empty, Variable var in begin match context with - | Pattern.CVariant name when StringSet.mem name names -> + | Pattern.CVariant name when Label.Set.mem name names -> def env | Pattern.CVariant _name -> let body = apply_annotation (Variable var) (annotation, body) in match_cases vars [(ps, body)] def env | Pattern.CNVariant names' -> - let diff = StringSet.diff names names' in - let cs = StringSet.union names names' in + let diff = Label.Set.diff names names' in + let cs = Label.Set.union names names' in let cases = - StringSet.fold + Label.Set.fold (fun name cases -> let case_type = TypeUtils.variant_at name t in (* let inject_type = TypeUtils.inject_type name case_type in *) @@ -726,13 +726,13 @@ and match_negative let match_env = bind_context var (Pattern.CVariant name, - Inject (name, Variable case_variable, t)) match_env + Inject (Label.name name, Variable case_variable, t)) match_env in - StringMap.add name (case_binder, def match_env) cases) + Label.Map.add name (case_binder, def match_env) cases) diff - StringMap.empty in + Label.Map.empty in let default_type = - StringSet.fold + Label.Set.fold (fun name t -> let _, t = TypeUtils.split_variant_type name t in t) cs t in let (default_binder, default_variable) = Var.fresh_var_of_type default_type in @@ -796,7 +796,7 @@ and match_constant | _ -> assert false and match_record - : var list -> (annotated_pattern StringMap.t * annotated_pattern option * annotated_clause) list -> + : var list -> (annotated_pattern Label.Map.t * annotated_pattern option * annotated_clause) list -> bound_computation -> var -> bound_computation = fun vars xs def var env -> let t = lookup_type var env in @@ -804,7 +804,7 @@ and match_record let names = List.fold_right (fun (bs, _, _) names -> - StringMap.fold (fun name _ names -> StringSet.add name names) bs names) xs StringSet.empty in + Label.Map.fold (fun name _ names -> Label.Set.add name names) bs names) xs Label.Set.empty in let all_closed = List.for_all (function | (_, None, _) -> true | (_, Some _, _) -> false) xs in @@ -822,19 +822,19 @@ and match_record | Some p -> p, false in let rps, fields = - StringSet.fold + Label.Set.fold (fun name (ps, fields) -> - if StringMap.mem name bs then - StringMap.find name bs :: ps, fields + if Label.Map.mem name bs then + Label.Map.find name bs :: ps, fields else if closed then ([], Pattern.Any)::ps, fields else let xt = TypeUtils.project_type name t in let xb, x = Var.fresh_var_of_type xt in - ([], Pattern.Variable xb)::ps, StringMap.add name (Variable x) fields) + ([], Pattern.Variable xb)::ps, Label.Map.add name (Variable x) fields) names - ([], StringMap.empty) in + ([], Label.Map.empty) in let rps, body = if all_closed then rps, body @@ -842,11 +842,11 @@ and match_record ([], Pattern.Any)::List.rev rps, body else let original_names = - StringMap.fold + Label.Map.fold (fun name _ names -> - StringSet.add name names) + Label.Set.add name names) bs - StringSet.empty in + Label.Set.empty in (* type of the original record continuation *) let pt = TypeUtils.erase_type original_names t in @@ -874,11 +874,11 @@ and match_record ) xs [] in let bindings, xs, env = - StringSet.fold + Label.Set.fold (fun name (bindings, xs, env) -> let xt = TypeUtils.project_type name t in let xb, x = Var.fresh_var_of_type xt in - let binding = letmv (xb, Project (name, Variable var)) in + let binding = letmv (xb, Project (Label.name name, Variable var)) in binding::bindings, x::xs, bind_type x xt env) names ([], [], env) in @@ -968,13 +968,13 @@ let compile_handle_cases in let compiled_effect_cases = (* The compiled cases *) if List.length raw_effect_clauses = 0 then - StringMap.empty + Label.Map.empty else begin let (comp_eff, comp_ty, _, _) = Sugartypes.(desc.shd_types) in let variant_type = let (fields,_,_) = comp_eff |> TypeUtils.extract_row_parts in let fields' = - StringMap.filter + Label.Map.filter (fun _ -> function | Types.Present _ -> true @@ -984,9 +984,9 @@ let compile_handle_cases let rec extract t = match TypeUtils.concrete_type t with | Types.Operation (domain, _) -> let (fields, _, _) = TypeUtils.extract_row domain |> TypeUtils.extract_row_parts in - let arity = StringMap.size fields in + let arity = Label.Map.size fields in if arity = 1 then - match StringMap.find "1" fields with + match Label.Map.find Label.one fields with | Types.Present t -> t | _ -> assert false else @@ -995,11 +995,25 @@ let compile_handle_cases | _ -> Types.unit_type (* nullary operation *) in let fields'' = - StringMap.map + Label.Map.map (function | Types.Present t -> extract t | _ -> assert false) + (* | Types.Present t -> *) + (* begin match TypeUtils.concrete_type t with *) + (* | Types.Function (domain, _, _) -> *) + (* let (fields, _, _) = TypeUtils.extract_row domain |> TypeUtils.extract_row_parts in *) + (* let arity = Label.Map.size fields in *) + (* if arity = 1 then *) + (* match Label.Map.find Label.one fields with *) + (* | Types.Present t -> t *) + (* | _ -> assert false *) + (* else *) + (* domain (\* n-ary operation *\) *) + (* | _ -> Types.unit_type (\* nullary operation *\) *) + (* end *) + (* | _ -> assert false) *) fields' in Types.make_variant_type fields'' @@ -1017,9 +1031,9 @@ let compile_handle_cases | [Pattern.Operation (name, ps, _)] -> let packaged_args = let fields = - List.mapi (fun i p -> (string_of_int (i+1), p)) ps + List.mapi (fun i p -> (Label.of_int (i+1), p)) ps in - Pattern.Record (StringMap.from_alist fields, None) + Pattern.Record (Label.Map.from_alist fields, None) in Pattern.Variant (name, packaged_args) | _ -> assert false @@ -1039,9 +1053,9 @@ let compile_handle_cases in let continuation_binders = let upd effname ks map = - match StringMap.lookup effname map with - | None -> StringMap.add effname ks map - | Some ks' -> StringMap.add effname (ks @ ks') map + match Label.Map.lookup effname map with + | None -> Label.Map.add effname ks map + | Some ks' -> Label.Map.add effname (ks @ ks') map in let rec gather_binders = function | Pattern.Any -> [] @@ -1054,14 +1068,14 @@ let compile_handle_cases | [Pattern.Operation (name, _, k)] -> upd name (gather_binders k) acc | _ -> assert false) - StringMap.empty (List.map fst raw_effect_clauses) + Label.Map.empty (List.map fst raw_effect_clauses) in - StringMap.mapi + Label.Map.mapi (fun effname (x, body) -> let body = with_parameters body in - match StringMap.find effname continuation_binders with + match Label.Map.find effname continuation_binders with | [] -> let resume = Var.(make_local_info ->- fresh_binder) (Types.Not_typed, "_resume") @@ -1132,9 +1146,9 @@ let match_choices : var -> clause list -> bound_computation = failwith ("Only choice patterns are supported in choice compilation") in let x = Var.var_of_binder b in let body = apply_annotation (Variable x) (annotation, body) in - StringMap.add name (b, body env) cases + Label.Map.add name (b, body env) cases | _ -> assert false) - StringMap.empty + Label.Map.empty clauses))) let compile_choices diff --git a/core/desugarCP.ml b/core/desugarCP.ml index dda621626..6f0c1ab67 100644 --- a/core/desugarCP.ml +++ b/core/desugarCP.ml @@ -13,7 +13,6 @@ let receive_str = "receive" let request_str = "request" let send_str = "send" let wait_str = "wait" -let wild_str = "wild" class desugar_cp env = let open CommonTypes.PrimaryKind in @@ -48,8 +47,8 @@ object (o : 'self_type) let o = o#restore_envs envs in o, block_node ([val_binding (with_dummy_pos ( - Pattern.Record ([("1", variable_pat ~ty:u x); - ("2", variable_pat ~ty:s c)], None))) + Pattern.Record ([(Label.one, variable_pat ~ty:u x); + (Label.two, variable_pat ~ty:s c)], None))) (fn_appl receive_str grab_tyargs [var c])], with_dummy_pos e), t | CPGive ((c, _), None, p) -> @@ -71,7 +70,8 @@ object (o : 'self_type) let c = Binder.to_name bndr in let t = Binder.to_type bndr in o, Var c, t - | CPSelect (bndr, label, p) -> + | CPSelect (bndr, name, p) -> + let label = Label.make name in let c = Binder.to_name bndr in let s = Binder.to_type bndr in let envs = o#backup_envs in @@ -85,11 +85,12 @@ object (o : 'self_type) | CPOffer (bndr, cases) -> let c = Binder.to_name bndr in let s = Binder.to_type bndr in - let desugar_branch (label, p) (o, cases) = + let desugar_branch (name, p) (o, cases) = + let label = Label.make name in let envs = o#backup_envs in let o = {< var_env = TyEnv.bind c (TypeUtils.choice_at label s) (o#get_var_env ()) >} in let (o, p, t) = desugar_cp o p in - let pat : Pattern.with_pos = with_dummy_pos (Pattern.Variant (label, + let pat : Pattern.with_pos = with_dummy_pos (Pattern.Variant (Label.make name, Some (variable_pat ~ty:(TypeUtils.choice_at label s) c))) in o#restore_envs envs, ((pat, with_dummy_pos p), t) :: cases in let (o, cases) = List.fold_right desugar_branch cases (o, []) in @@ -115,10 +116,10 @@ object (o : 'self_type) let (eff_fields, eff_row, eff_closed) = Types.flatten_row o#lookup_effects |> TypeUtils.extract_row_parts in - let eff_fields = StringMap.remove wild_str eff_fields in + let eff_fields = Label.Map.remove Types.wild eff_fields in let eff_fields = if Settings.get Basicsettings.Sessions.exceptions_enabled then - StringMap.remove Value.session_exception_operation eff_fields + Label.Map.remove Value.session_exception_operation eff_fields else eff_fields in diff --git a/core/desugarDatatypes.ml b/core/desugarDatatypes.ml index e6f774954..3c28b6d16 100644 --- a/core/desugarDatatypes.ml +++ b/core/desugarDatatypes.ml @@ -105,7 +105,7 @@ module Desugar = struct ForAll (qs, t) | Unit -> Types.unit_type | Tuple ks -> - let labels = map string_of_int (Utility.fromTo 1 (1 + length ks)) in + let labels = map Label.of_int (Utility.fromTo 1 (1 + length ks)) in let unit = Types.make_empty_closed_row () in let present (s, x) = (s, Types.Present x) in @@ -243,7 +243,10 @@ module Desugar = struct if qn = tn then type_args qs ts else - raise (TypeApplicationArityMismatch { pos = node.pos; name = name; expected = qn; provided = tn }) + raise (TypeApplicationArityMismatch + { pos = node.pos; + name = name; + expected = qn; provided = tn }) in begin match SEnv.find_opt name alias_env with | None -> raise (unbound_tycon node.pos name) @@ -282,7 +285,7 @@ module Desugar = struct | Closed -> Types.make_empty_closed_row () | Open srv -> let rv = SugarTypeVar.get_resolved_row_exn srv in - Types.Row (StringMap.empty, rv, false) + Types.Row (Label.Map.empty, rv, false) | Recursive (stv, r) -> let mrv = SugarTypeVar.get_resolved_row_exn stv in @@ -291,7 +294,7 @@ module Desugar = struct (* Turn mrv into a proper recursive row *) Unionfind.change mrv (Types.Recursive (var, sk, r)); - Types.Row (StringMap.empty, mrv, false) + Types.Row (Label.Map.empty, mrv, false) in let fields = List.map (fun (k, p) -> (k, fieldspec alias_env p node)) fields in @@ -335,7 +338,7 @@ module Desugar = struct let write_row, needed_row = match TypeUtils.concrete_type read_type with | Record (Row (fields, _, _)) -> - StringMap.fold + Label.Map.fold (fun label t (write, needed) -> match lookup label constraints with | Some cs -> diff --git a/core/desugarEffects.ml b/core/desugarEffects.ml index 05023e9cb..86b522df4 100644 --- a/core/desugarEffects.ml +++ b/core/desugarEffects.ml @@ -492,7 +492,7 @@ let gather_operation_of_type tp let seen_recapps = StringSet.add name seen_recapps in {< seen_recapps >} - val operations : stringset RowVarMap.t = RowVarMap.empty + val operations : Label.Set.t RowVarMap.t = RowVarMap.empty method operations = operations val implicit_shared_var : int option = None @@ -504,8 +504,8 @@ let gather_operation_of_type tp method with_label vid label = let operations = RowVarMap.update vid (function - | None -> Some (StringSet.singleton label) - | Some sset -> Some (StringSet.add label sset)) + | None -> Some (Label.Set.singleton label) + | Some sset -> Some (Label.Set.add label sset)) operations in {< operations >} @@ -522,7 +522,7 @@ let gather_operation_of_type tp then o#set_implicit_shared_var vid else o in - FieldEnv.fold + Label.Map.fold (fun label _field acc -> acc#with_label vid label) fields o @@ -601,13 +601,13 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt = method operations = operations method with_operations operations = {< operations >} - val hidden_operations : stringset stringmap = StringMap.empty + val hidden_operations : Label.Set.t stringmap = StringMap.empty method hidden_operations = hidden_operations method add_hidden_op alias_name label = let hidden_operations = StringMap.update alias_name (function - | None -> Some (StringSet.singleton label) - | Some lset -> Some (StringSet.add label lset)) + | None -> Some (Label.Set.singleton label) + | Some lset -> Some (Label.Set.add label lset)) hidden_operations in {< hidden_operations >} @@ -632,8 +632,8 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt = else let ops = match RowVarMap.find_opt var operations with - | None -> StringSet.singleton op - | Some t -> StringSet.add op t + | None -> Label.Set.singleton op + | Some t -> Label.Set.add op t in {} @@ -673,14 +673,14 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt = RowVarMap.update vid (function | None -> Some sset - | Some opset -> Some (StringSet.union opset sset)) + | Some opset -> Some (Label.Set.union opset sset)) acc) ops self#operations in let self = match RowVarMap.find_raw_opt (-1) ops with | None -> self | Some hide_ops -> - StringSet.fold + Label.Set.fold (fun label acc -> acc#add_hidden_op name label) hide_ops self @@ -724,14 +724,14 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt = RowVarMap.update vid (function | None -> Some sset - | Some opset -> Some (StringSet.union opset sset)) + | Some opset -> Some (Label.Set.union opset sset)) acc) ops self#operations in let self = match RowVarMap.find_raw_opt (-1) ops with | None -> self | Some hide_ops -> - StringSet.fold + Label.Set.fold (fun label acc -> acc#add_hidden_op name label) hide_ops self @@ -763,15 +763,15 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt = let o = o#datatype dt in (o#operations |> RowVarMap.map (fun v -> - StringSet.fold + Label.Set.fold (fun op m -> let point = lazy (let var = Types.fresh_raw_variable () in Unionfind.fresh (Types.Var (var, (PrimaryKind.Presence, default_subkind), `Rigid))) in - StringMap.add op point m) - v StringMap.empty), + Label.Map.add op point m) + v Label.Map.empty), o#hidden_operations) else (RowVarMap.empty, StringMap.empty) @@ -819,11 +819,11 @@ class main_traversal simple_tycon_env = (** Map of effect variables to all mentioned operations, and their corresponding effect variables. *) - val row_operations : Types.meta_presence_var Lazy.t StringMap.t RowVarMap.t + val row_operations : Types.meta_presence_var Lazy.t Label.Map.t RowVarMap.t = RowVarMap.empty - val hidden_operations : stringset stringmap = StringMap.empty + val hidden_operations : Label.Set.t stringmap = StringMap.empty method set_inside_type inside_type = {} @@ -957,12 +957,12 @@ class main_traversal simple_tycon_env = | None -> [] | Some ops -> let ops_to_hide = match StringMap.find_opt tycon hidden_operations with - | None -> StringSet.empty + | None -> Label.Set.empty | Some hidden -> hidden in - StringMap.fold + Label.Map.fold (fun op p fields -> - if StringSet.mem op ops_to_hide + if Label.Set.mem op ops_to_hide then fields else begin let mpv : Types.meta_presence_var = @@ -973,7 +973,7 @@ class main_traversal simple_tycon_env = (SugarTypeVar.mk_resolved_presence mpv) in if not allow_implictly_bound_vars then - raise (cannot_insert_presence_var2 pos op); + raise (cannot_insert_presence_var2 pos (Label.show op)); (op, fieldspec) :: fields end) ops [] @@ -1050,27 +1050,27 @@ class main_traversal simple_tycon_env = match RowVarMap.find_opt stv row_operations with | Some ops -> let ops_to_hide = match in_alias with - | None -> StringSet.empty + | None -> Label.Set.empty | Some name -> (match StringMap.find_opt name hidden_operations with - | None -> StringSet.empty + | None -> Label.Set.empty | Some hidden -> hidden) in let ops_to_add = List.fold_left - (fun ops (op, _) -> StringMap.remove op ops) + (fun ops (op, _) -> Label.Map.remove op ops) ops fields in let add_op op pres_var fields = if not allow_implictly_bound_vars then (* Alternatively, we could just decide not to touch the row and let the type checker complain about the incompatible rows? *) - raise (cannot_insert_presence_var dpos op); - if StringSet.mem op ops_to_hide + raise (cannot_insert_presence_var dpos (Label.show op)); + if Label.Set.mem op ops_to_hide then fields else let rpv = SugarTypeVar.mk_resolved_presence (Lazy.force pres_var) in (op, Datatype.Var rpv) :: fields in - StringMap.fold add_op ops_to_add fields + Label.Map.fold add_op ops_to_add fields | None -> fields ) | _ -> fields in diff --git a/core/desugarFuns.ml b/core/desugarFuns.ml index e87db890e..0b941254c 100644 --- a/core/desugarFuns.ml +++ b/core/desugarFuns.ml @@ -132,7 +132,7 @@ object (o : 'self_type) let (fields, rho, _) = TypeUtils.extract_row_parts row in let effb, row = fresh_row_quantifier default_effect_subkind in - let r = Record (Row (StringMap.add name (Present a) fields, rho, false)) in + let r = Record (Row (Label.Map.add name (Present a) fields, rho, false)) in let f = gensym ~prefix:"_fun_" () in let x = gensym ~prefix:"_fun_" () in diff --git a/core/desugarLabels.ml b/core/desugarLabels.ml new file mode 100644 index 000000000..8f059f271 --- /dev/null +++ b/core/desugarLabels.ml @@ -0,0 +1,65 @@ +open Utility +open Sugartypes + +module Env = Label.Env + +let visitor = + object (self) + inherit SugarTraversals.map as super + + val mutable label_env : Env.t = Env.empty + + method! label lbl = + if Label.is_global lbl || not (Label.is_free lbl) then + lbl + else + match Env.find_homonyms lbl label_env with + | bind_with :: _ -> Label.bind_local ~bind_with lbl + | _ -> failwith ("The local label " ^ Label.show lbl ^ " is not bound") + + method! bindingnode = function + | FreshLabel labels -> + let labels = List.map Label.bind_local labels in + label_env <- Env.bind_labels labels label_env ; + FreshLabel labels + | Module { binder; members } -> + let env = label_env in + let members = self#list (fun o -> o#binding) members in + label_env <- env; + Module { binder; members } + | b -> super#bindingnode b + + method! phrasenode = function + | Block (bs, e) -> + let env = label_env in + let bs = self#list (fun o -> o#binding) bs in + let e = self#phrase e in + label_env <- env; + Block (bs, e) + | e -> super#phrasenode e + end + +let program p = visitor#program p + +let sentence = function + | Definitions bs -> + let bs' = visitor#list (fun o b -> o#binding b) bs in + Definitions bs' + | Expression p -> + let p' = visitor#phrase p in + Expression p' + | Directive d -> Directive d + +module Untyped = struct + open Transform.Untyped + + let name = "labels" + + let program state program' = + let program' = program program' in + return state program' + + let sentence state sentence' = + let sentence' = sentence sentence' in + return state sentence' +end diff --git a/core/desugarModules.ml b/core/desugarModules.ml index c2a481ea7..1a0f0a439 100644 --- a/core/desugarModules.ml +++ b/core/desugarModules.ml @@ -514,6 +514,11 @@ and desugar ?(toplevel=false) (renamer' : Epithet.t) (scope' : Scope.t) = let b = self#binding b in b :: self#bindings bs + method! label = function + | Label.Local (textual_name, uid) -> + Label.Local (Epithet.expand renamer textual_name, uid) + | l -> l + method! program (bs, exp) = (* It is crucial that we enforce left-to-right evaluation of [bs] and [exp]. Note that OCaml uses right-to-left evaluation diff --git a/core/desugarProcesses.ml b/core/desugarProcesses.ml index ae073231d..e0c9c22d0 100644 --- a/core/desugarProcesses.ml +++ b/core/desugarProcesses.ml @@ -1,4 +1,3 @@ -open Utility open CommonTypes open Sugartypes open SugarConstructors.DummyPositions @@ -81,7 +80,7 @@ object (o : 'self_type) Types.(remove_field hear (remove_field wild (Row (fieldenv, rho, false)))) in begin - match StringMap.find Types.hear fieldenv with + match Label.Map.find Types.hear fieldenv with | (Types.Present mbt) -> o#phrasenode (Switch (fn_appl "recv" [(Type, mbt); (Row, other_effects)] [], diff --git a/core/desugarSessionExceptions.ml b/core/desugarSessionExceptions.ml index 06a632e60..0943aaff5 100644 --- a/core/desugarSessionExceptions.ml +++ b/core/desugarSessionExceptions.ml @@ -108,7 +108,8 @@ object (o : 'self_type) let outer_effects = o#lookup_effects in let fail_cont_ty = - Types.make_pure_function_type [] (Types.empty_type) in + Types.make_operation_type [] Types.empty_type + in let inner_effects = effect_row @@ -127,7 +128,7 @@ object (o : 'self_type) let effect_cases = [otherwise_clause] in (* Manually construct a row with the two hardwired handler cases. *) - let raw_row = Types.row_with ("Return", (Types.Present try_dt)) inner_effects in + let raw_row = Types.row_with (Label.return, (Types.Present try_dt)) inner_effects in (* Dummy types *) let types = (inner_effects, try_dt, outer_effects, otherwise_dt) in @@ -193,8 +194,8 @@ let wrap_linear_handlers = constructor ~body:(var fresh_var) "Just", constructor "Nothing", dtopt)), [ - (with_dummy_pos (Pattern.Variant ("Just", (Some x))), super#phrase m); - (with_dummy_pos (Pattern.Variant ("Nothing", None)), super#phrase n) + (with_dummy_pos (Pattern.Variant (Label.make "Just", (Some x))), super#phrase m); + (with_dummy_pos (Pattern.Variant (Label.make "Nothing", None)), super#phrase n) ], None)) | p -> super#phrase p end diff --git a/core/evalir.ml b/core/evalir.ml index 505bcdafd..12769099e 100644 --- a/core/evalir.ml +++ b/core/evalir.ml @@ -167,7 +167,7 @@ struct opt_app (value env) (Lwt.return (`Record [])) r >>= fun res -> match res with | `Record fs -> - let fields = StringMap.bindings fields in + let fields = StringMap.bindings (Label.label_to_string_map fields) in LwtHelpers.foldr_lwt (fun (label, v) (fs: (string * Value.t) list) -> if List.mem_assoc label fs then @@ -194,11 +194,11 @@ struct begin match v with | `Record fields when - StringSet.for_all (fun label -> List.mem_assoc label fields) labels -> + Label.Set.for_all (fun label -> List.mem_assoc (Label.name label) fields) labels -> Lwt.return ( - `Record (StringSet.fold (fun label fields -> List.remove_assoc label fields) labels fields)) + `Record (Label.Set.fold (fun label fields -> List.remove_assoc (Label.name label) fields) labels fields)) | v -> - type_error ~action:(Printf.sprintf "erase labels {%s}" (String.concat "," (StringSet.elements labels))) + type_error ~action:(Printf.sprintf "erase labels {%s}" (String.concat "," (StringSet.elements (Label.label_to_string_set labels)))) "record" v end | Inject (label, v, _) -> @@ -211,7 +211,7 @@ struct value env v >>= fun v -> Lwt.return (List.map Value.unbox_xml (Value.unbox_list v) @ children)) children (Lwt.return []) >>= fun children -> - let attrs = StringMap.bindings attrs in + let attrs = StringMap.bindings (Label.label_to_string_map attrs) in LwtHelpers.foldr_lwt (fun (name, v) attrs -> value env v >>= fun str -> @@ -574,7 +574,7 @@ struct begin match v with | `Variant (label, _) as v -> begin - match StringMap.lookup label cases, default, v with + match StringMap.lookup label (Label.label_to_string_map cases), default, v with | Some (b, c), _, `Variant (_, v) | _, Some (b, c), v -> let var = Var.var_of_binder b in @@ -781,11 +781,11 @@ struct let r, _ = Types.unwrap_row (TypeUtils.extract_row t) in TypeUtils.extract_row_parts r in let fields = - StringMap.fold + Label.Map.fold (fun name t fields -> let open Types in match t with - | Present t -> (name, t)::fields + | Present t -> (Label.name name, t)::fields | _ -> assert false) fieldMap [] @@ -880,7 +880,7 @@ struct StringMap.map (function | Types.Present t -> t - | _ -> assert false) fields + | _ -> assert false) (Label.label_to_string_map fields) in Lwt.return (db, table, field_types, temporal_fields) @@ -918,7 +918,7 @@ struct StringMap.map (function | Types.Present t -> t - | _ -> assert false) fields + | _ -> assert false) (Label.label_to_string_map fields) in Lwt.return (db, table, field_types, temporal_fields) @@ -1016,7 +1016,7 @@ struct Debug.print ("chose label: " ^ label); begin - match StringMap.lookup label cases with + match StringMap.lookup label (Label.label_to_string_map cases) with | Some (b, body) -> let var = Var.var_of_binder b in computation (Value.Env.bind var (chan, Scope.Local) env) cont body diff --git a/core/frontend.ml b/core/frontend.ml index acdedb7f6..27a629b8e 100644 --- a/core/frontend.ml +++ b/core/frontend.ml @@ -133,6 +133,7 @@ module Untyped = struct ; (module DesugarLAttributes) ; (module LiftRecursive) ; (module DesugarTypeVariables) + ; (module DesugarLabels) ; (module DesugarEffects) ; (module DesugarDatatypes) |] diff --git a/core/generalise.ml b/core/generalise.ml index 7a3f0eba6..8103a026f 100644 --- a/core/generalise.ml +++ b/core/generalise.ml @@ -78,7 +78,7 @@ let rec get_type_args : gen_kind -> TypeVarSet.t -> datatype -> type_arg list = (* Row *) | Row (field_env, row_var, _) -> let field_vars = - StringMap.fold + Label.Map.fold (fun _ field_spec vars -> vars @ get_presence_type_args kind bound_vars field_spec ) field_env [] in @@ -149,7 +149,7 @@ let rigidify_type_arg : type_arg -> unit = | Type, Meta point -> rigidify_point point | Presence, Meta point -> rigidify_point point | Row, Row (fields, point, _dual) -> - assert (StringMap.is_empty fields); + assert (Label.Map.is_empty fields); rigidify_point point (* HACK: probably shouldn't happen *) | Row, Meta point -> rigidify_point point @@ -169,7 +169,7 @@ let mono_type_args : type_arg -> unit = | Type, Meta point -> check_sk point | Presence, Meta point -> check_sk point | Row, Row (fields, point, _dual) -> - assert (StringMap.is_empty fields); + assert (Label.Map.is_empty fields); check_sk point (* HACK: probably shouldn't happen *) | Row, Meta point -> check_sk point diff --git a/core/instantiate.ml b/core/instantiate.ml index dedd92e68..234cfa7d3 100644 --- a/core/instantiate.ml +++ b/core/instantiate.ml @@ -128,14 +128,14 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) * | Closed -> true | _ -> false in - let field_env' = StringMap.fold + let field_env' = Label.Map.fold (fun label f field_env' -> let rec add = function - | Present t -> StringMap.add label (Present (inst t)) field_env' + | Present t -> Label.Map.add label (Present (inst t)) field_env' | Absent -> if is_closed then field_env' - else StringMap.add label Absent field_env' + else Label.Map.add label Absent field_env' | Meta point -> begin match Unionfind.find point with @@ -146,7 +146,7 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) * else Meta point in - StringMap.add label f field_env' + Label.Map.add label f field_env' | f -> add f end @@ -157,9 +157,9 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) * in add f) field_env - StringMap.empty in + Label.Map.empty in let field_env'', row_var', dual' = inst_row_var inst_map rec_env row_var dual |> TypeUtils.extract_row_parts in - Row (StringMap.fold StringMap.add field_env' field_env'', row_var', dual') + Row (Label.Map.fold Label.Map.add field_env' field_env'', row_var', dual') (* precondition: row_var has been flattened *) and inst_row_var : instantiation_maps -> inst_env -> row_var -> bool -> row = fun inst_map rec_env row_var dual -> (* HACK: fix the ill-formed rows that are introduced in the @@ -169,28 +169,28 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) * let rowify t = match t with | Row _ -> t - | Meta row_var -> Row (StringMap.empty, row_var, false) + | Meta row_var -> Row (Label.Map.empty, row_var, false) | Alias (PrimaryKind.Row, _,row) -> row | _ -> assert false in let instr = inst_row inst_map rec_env in let dual_if = if dual then dual_row else fun x -> x in match Unionfind.find row_var with - | Closed -> Row (StringMap.empty, row_var, dual) + | Closed -> Row (Label.Map.empty, row_var, dual) | Var (var, _, _) -> if IntMap.mem var inst_map then dual_if (rowify (snd (IntMap.find var inst_map))) else - Row (StringMap.empty, row_var, dual) + Row (Label.Map.empty, row_var, dual) | Recursive (var, kind, rec_row) -> if IntMap.mem var rec_env then - Row (StringMap.empty, IntMap.find var rec_env, dual) + Row (Label.Map.empty, IntMap.find var rec_env, dual) else begin let var' = Types.fresh_raw_variable () in let point' = Unionfind.fresh (Var (var', kind, `Flexible)) in let rec_row' = inst_row inst_map (IntMap.add var point' rec_env) rec_row in let _ = Unionfind.change point' (Recursive (var', kind, rec_row')) in - Row (StringMap.empty, point', dual) + Row (Label.Map.empty, point', dual) end | row -> dual_if (instr row) @@ -234,7 +234,7 @@ let instantiate_typ : bool -> datatype -> (type_arg list * datatype) = fun rigid let open PrimaryKind in match Kind.primary_kind kind with | (Type | Presence) as pk -> pk, Meta point - | Row -> Row, Row (StringMap.empty, point, false) in + | Row -> Row, Row (Label.Map.empty, point, false) in IntMap.add var ty inst_env, ty :: tys in let inst_map, tys = diff --git a/core/ir.ml b/core/ir.ml index 1a7b660bb..81ce44c8e 100644 --- a/core/ir.ml +++ b/core/ir.ml @@ -18,9 +18,9 @@ type tyvar = Quantifier.t type tyarg = Types.type_arg [@@deriving show] -type name_set = Utility.stringset +type name_set = Label.Set.t [@@deriving show] -type 'a name_map = 'a Utility.stringmap +type 'a name_map = 'a Label.Map.t [@@deriving show] type 'a var_map = 'a Utility.intmap @@ -117,7 +117,7 @@ and special = | Select of Name.t * value | Choice of value * (binder * computation) name_map | Handle of handler - | DoOperation of Name.t * value list * Types.t + | DoOperation of Label.t * value list * Types.t and computation = binding list * tail_computation and effect_case = binder * binder * computation and handler = { @@ -174,7 +174,7 @@ let rec is_atom = let with_bindings bs' (bs, tc) = (bs' @ bs, tc) -let unit = Extend (Utility.StringMap.empty, None) +let unit = Extend (Label.Map.empty, None) let unit_comp = ([], Return unit) type program = computation diff --git a/core/ir.mli b/core/ir.mli index 060918cb8..280e71285 100644 --- a/core/ir.mli +++ b/core/ir.mli @@ -18,9 +18,9 @@ type tyvar = Quantifier.t type tyarg = Types.type_arg [@@deriving show] -type name_set = Utility.stringset +type name_set = Label.Set.t [@@deriving show] -type 'a name_map = 'a Utility.stringmap +type 'a name_map = 'a Label.Map.t [@@deriving show] type 'a var_map = 'a Utility.intmap @@ -119,7 +119,7 @@ and special = | Select of Name.t * value | Choice of value * (binder * computation) name_map | Handle of handler - | DoOperation of Name.t * value list * Types.t + | DoOperation of Label.t * value list * Types.t and computation = binding list * tail_computation and effect_case = binder * binder * computation and handler = { diff --git a/core/irCheck.ml b/core/irCheck.ml index e68989795..88f454216 100644 --- a/core/irCheck.ml +++ b/core/irCheck.ml @@ -222,7 +222,7 @@ let eq_types occurrence : type_eq_context -> (Types.datatype * Types.datatype) - row |> TypeUtils.extract_row_parts in if Types.is_closed_row row then let field_env' = - Utility.StringMap.filter + Label.Map.filter ( fun _ v -> match v with | T.Absent -> false | _ -> true ) @@ -433,12 +433,12 @@ let eq_types occurrence : type_eq_context -> (Types.datatype * Types.datatype) - | _, _ -> false and eq_field_envs (context, lfield_env, rfield_env) = let lfields_in_rfields = - StringMap.for_all (fun field lp -> - match StringMap.find_opt field rfield_env with + Label.Map.for_all (fun field lp -> + match Label.Map.find_opt field rfield_env with | Some rp -> eq_presence (context, lp, rp) | None -> false ) lfield_env in - lfields_in_rfields && StringMap.cardinal lfield_env = StringMap.cardinal rfield_env + lfields_in_rfields && Label.Map.cardinal lfield_env = Label.Map.cardinal rfield_env and eq_row_vars (context, lpoint, rpoint) = match Unionfind.find lpoint, Unionfind.find rpoint with | Closed, Closed -> true @@ -476,9 +476,9 @@ let check_eq_type_lists = fun (ctx : type_eq_context) exptl actl occurrence -> let ensure_effect_present_in_row ctx allowed_effects required_effect_name required_effect_type occurrence = let (map, _, _) = fst (Types.unwrap_row allowed_effects) |> TypeUtils.extract_row_parts in - match StringMap.find_opt required_effect_name map with + match Label.Map.find_opt required_effect_name map with | Some (T.Present et) -> check_eq_types ctx et required_effect_type occurrence - | _ -> raise_ir_type_error ("Required effect " ^ required_effect_name ^ " not present in effect row " ^ Types.string_of_row allowed_effects) occurrence + | _ -> raise_ir_type_error ("Required effect " ^ Label.show required_effect_name ^ " not present in effect row " ^ Types.string_of_row allowed_effects) occurrence @@ -592,7 +592,7 @@ struct o, Extend (fields, base), t | Project (name, v) -> let (o, v, vt) = o#value v in - o, Project (name, v), project_type ~overstep_quantifiers:false name vt + o, Project (name, v), project_type ~overstep_quantifiers:false (Label.make name) vt | Erase (names, v) -> let (o, v, vt) = o#value v in @@ -602,9 +602,7 @@ struct let o, v, vt = o#value v in let _ = match TypeUtils.concrete_type t with | Variant _ -> - Debug.print "2" ; - let x = o#check_eq_types (variant_at ~overstep_quantifiers:false name t) vt (SVal orig) - in Debug.print "22" ; x + o#check_eq_types (variant_at ~overstep_quantifiers:false (Label.make name) t) vt (SVal orig) | _ -> raise_ir_type_error "trying to inject into non-variant type" (SVal orig) in o, Inject (name, v, t), t | TAbs (tyvars, v) -> @@ -626,7 +624,7 @@ struct let (o, attributes, attribute_types) = o#name_map (fun o -> o#value) attributes in let (o, children , children_types) = o#list (fun o -> o#value) children in - let _ = StringMap.iter (fun _ t -> o#check_eq_types (Primitive Primitive.String) t (SVal orig)) attribute_types in + let _ = Label.Map.iter (fun _ t -> o#check_eq_types (Primitive Primitive.String) t (SVal orig)) attribute_types in let _ = List.iter (fun t -> o#check_eq_types Types.xml_type t (SVal orig)) children_types in o, XmlNode (tag, attributes, children), Types.xml_type @@ -734,32 +732,32 @@ struct | Variant row as variant -> let unwrapped_row = fst (unwrap_row row) |> TypeUtils.extract_row_parts in let present_fields, has_bad_presence_polymorphism = - StringMap.fold (fun field field_spec (fields, poly) -> match field_spec with - | Present _ -> (StringSet.add field fields), poly - | Meta _ -> fields, StringMap.mem field cases + Label.Map.fold (fun field field_spec (fields, poly) -> match field_spec with + | Present _ -> (Label.Set.add field fields), poly + | Meta _ -> fields, Label.Map.mem field cases | Absent -> fields, poly | _ -> raise Types.tag_expectation_mismatch) - (fst3 unwrapped_row) (StringSet.empty, false) in + (fst3 unwrapped_row) (Label.Set.empty, false) in let is_closed = is_closed_row row in let has_default = OptionUtils.is_some default in - let case_fields = StringMap.fold (fun field _ fields -> StringSet.add field fields) cases StringSet.empty in + let case_fields = Label.Map.fold (fun field _ fields -> Label.Set.add field fields) cases Label.Set.empty in ensure (not has_bad_presence_polymorphism) "row contains presence-polymorphic labels with corresponding \ match clauses. These can only be handled by a default case." (STC orig); if has_default then - ensure (StringSet.subset case_fields present_fields) "superfluous case" (STC orig) + ensure (Label.Set.subset case_fields present_fields) "superfluous case" (STC orig) else begin - ensure (not (StringSet.is_empty present_fields)) "Case with neither cases nor default" (STC orig); + ensure (not (Label.Set.is_empty present_fields)) "Case with neither cases nor default" (STC orig); ensure (is_closed) "case without default over open row" (STC orig); - ensure (StringSet.equal case_fields present_fields) + ensure (Label.Set.equal case_fields present_fields) "cases not identical to present fields in closed row, no default case" (STC orig) end; let o, cases, types = - StringMap.fold + Label.Map.fold (fun name (binder, comp) (o, cases, types) -> let type_binder = Var.type_of_binder binder in Debug.print "1" ; @@ -769,14 +767,14 @@ struct let o, b = o#binder binder in let o, c, t = o#computation comp in let o = o#remove_binder binder in - o, StringMap.add name (b,c) cases, t :: types) - cases (o, StringMap.empty, []) in + o, Label.Map.add name (b,c) cases, t :: types) + cases (o, Label.Map.empty, []) in let o, default, default_type = o#option (fun o (b, c) -> let o, b = o#binder b in let actual_default_type = Var.type_of_binder b in let expected_default_t = - StringMap.fold + Label.Map.fold (fun case _ v -> TypeUtils.split_variant_type case v |> snd) cases variant @@ -811,7 +809,8 @@ struct | Database v -> let o, v, vt = o#value v in (* v must be a record containing string fields name, args, and driver*) - List.iter (fun field -> + List.iter (fun name -> + let field = Label.make name in o#check_eq_types (project_type field vt) Types.string_type (SSpec special) ) ["name"; "args"; "driver"]; o, Database v, Primitive Primitive.DB @@ -915,7 +914,7 @@ struct | InsertReturning (tmp, _, _, (Constant (Constant.String id) as ret)) -> (* The return value must be encoded as a string literal, denoting a column *) - let ret_type = TypeUtils.project_type id table_read in + let ret_type = TypeUtils.project_type (Label.make id) table_read in o#check_eq_types Types.int_type ret_type (SSpec special); o, InsertReturning (tmp, source, rows, ret), Types.int_type | InsertReturning (_, _, _, _) -> @@ -991,7 +990,7 @@ struct let o, b = o#binder b in let o, c, t = o#computation c in o, (b, c), t) bs in - let t = (StringMap.to_alist ->- List.hd ->- snd) branch_types in + let t = (Label.Map.to_alist ->- List.hd ->- snd) branch_types in o, Choice (v, bs), t | Handle ({ ih_comp; ih_cases; ih_return; ih_depth }) -> (* outer effects is R_d in the IR formalization *) @@ -1050,19 +1049,19 @@ struct (* We now construct the inner effects from the outer effects and branch_presence_spec_types *) let (outer_effects_map, outer_effects_var, outer_effects_dualized) = outer_effects_parts in (* For each case branch, the corresponding entry goes directly into the field spec map of the inner effect row *) - let inner_effects_map_from_branches = StringMap.map (fun x -> Present x) branch_presence_spec_types in + let inner_effects_map_from_branches = Label.Map.map (fun x -> Present x) branch_presence_spec_types in (* We now add all entries from the outer effects that were not touched by the handler to the inner effects *) - let inner_effects_map = StringMap.fold (fun effect outer_presence_spec map -> - if StringMap.mem effect inner_effects_map_from_branches then + let inner_effects_map = Label.Map.fold (fun effect outer_presence_spec map -> + if Label.Map.mem effect inner_effects_map_from_branches then map else - StringMap.add effect outer_presence_spec map + Label.Map.add effect outer_presence_spec map ) inner_effects_map_from_branches outer_effects_map in let inner_effects = Row (inner_effects_map, outer_effects_var, outer_effects_dualized) in (if not (Types.is_closed_row outer_effects) then - let outer_effects_contain e = StringMap.mem e outer_effects_map in - ensure (StringMap.for_all (fun e _ -> outer_effects_contain e) cases) "Outer effects are open but do not mention an effect handled by handler" (SSpec special)); + let outer_effects_contain e = Label.Map.mem e outer_effects_map in + ensure (Label.Map.for_all (fun e _ -> outer_effects_contain e) cases) "Outer effects are open but do not mention an effect handled by handler" (SSpec special)); (* comp_t is A_c in the IR formalization *) let o, _ = o#set_allowed_effects inner_effects in diff --git a/core/irTraversals.ml b/core/irTraversals.ml index 64d4b731b..01c30cbc0 100644 --- a/core/irTraversals.ml +++ b/core/irTraversals.ml @@ -130,13 +130,13 @@ struct ('self_type -> 'a -> ('self_type * 'a * datatype)) -> 'a name_map -> 'self_type * 'a name_map * datatype name_map = fun f vmap -> - StringMap.fold + Label.Map.fold (fun name v (o, vmap, tmap) -> let (o, v, t) = f o v in - (o, StringMap.add name v vmap, - StringMap.add name t tmap)) + (o, Label.Map.add name v vmap, + Label.Map.add name t tmap)) vmap - (o, StringMap.empty, StringMap.empty) + (o, Label.Map.empty, Label.Map.empty) method var_map : 'a. @@ -196,7 +196,7 @@ struct o, Extend (fields, base), t | Project (name, v) -> let (o, v, vt) = o#value v in - o, Project (name, v), deconstruct (project_type name) vt + o, Project (name, v), deconstruct (project_type (Label.make name)) vt | Erase (names, v) -> let (o, v, vt) = o#value v in let t = deconstruct (erase_type names) vt in @@ -284,8 +284,8 @@ struct let o, c, t = o#computation c in o, (b, c), t) default in let t = - if not (StringMap.is_empty case_types) then - (StringMap.to_alist ->- List.hd ->- snd) case_types + if not (Label.Map.is_empty case_types) then + (Label.Map.to_alist ->- List.hd ->- snd) case_types else val_of default_type in @@ -389,7 +389,7 @@ struct let o, b = o#binder b in let o, c, t = o#computation c in o, (b, c), t) bs in - let t = (StringMap.to_alist ->- List.hd ->- snd) branch_types in + let t = (Label.Map.to_alist ->- List.hd ->- snd) branch_types in o, Choice (v, bs), t | Handle ({ ih_comp; ih_cases; ih_return; ih_depth }) -> let (o, comp, _) = o#computation ih_comp in diff --git a/core/irtojs.ml b/core/irtojs.ml index 8ef409e8b..6e5471509 100644 --- a/core/irtojs.ml +++ b/core/irtojs.ml @@ -1,7 +1,7 @@ -1 (** JavaScript generation *) open Utility open CommonTypes +module L = Label let js_hide_database_info = Js.hide_database_info let session_exceptions_enabled = Settings.get Basicsettings.Sessions.exceptions_enabled @@ -861,9 +861,9 @@ end = functor (K : CONTINUATION) -> struct | Ir.Extend (field_map, rest) -> let dict = Dict - (StringMap.fold + (L.Map.fold (fun name v dict -> - (name, gv v) :: dict) + (L.name name, gv v) :: dict) field_map []) in begin @@ -876,7 +876,7 @@ end = functor (K : CONTINUATION) -> struct project (gv v) name | Ir.Erase (names, v) -> call Runtime.Links.erase - [gv v; Aux.set_of_array (Arr (List.map strlit (StringSet.elements names)))] + [gv v; Aux.set_of_array (Arr (List.map strlit (StringSet.elements (L.label_to_string_set names))))] | Ir.Inject (name, v, _t) -> Dict [("_label", strlit name); ("_value", gv v)] @@ -926,8 +926,8 @@ end = functor (K : CONTINUATION) -> struct let open Code in call Runtime.Links.xml [Constructors.strlit tag; - Dict (StringMap.fold (fun name v bs -> - (name, generate_value env v) :: bs) attrs []); + Dict (L.Map.fold (fun name v bs -> + (L.name name, generate_value env v) :: bs) attrs []); Aux.List.of_array (Arr (List.map (generate_value env) children))] let generate_remote_call f_var xs_names env = @@ -1106,7 +1106,7 @@ end = functor (K : CONTINUATION) -> struct let comp = snd (generate_computation (VEnv.bind x x_name env) comp kappa) in Bind (x_name, project scrutinee "_value", comp) in - let cases = StringMap.map gen_cont cases in + let cases = L.Map.map gen_cont cases |> L.label_to_string_map in let default = opt_map gen_cont default in k (Switch (project scrutinee "_label", cases, default))) | Ir.If (v, c1, c2) -> @@ -1171,7 +1171,7 @@ end = functor (K : CONTINUATION) -> struct let (ch, chname) = name_binder cb in Bind (chname, channel, snd (generate_computation (VEnv.bind ch chname env) comp K.(skappa <> kappa))) in - let branches = StringMap.map generate_branch bs in + let branches = L.Map.map generate_branch bs |> L.label_to_string_map in Fn ([result], (Bind (received, message, (Switch (project (Var received) "_label", branches, None)))))) in let cont = K.(skappa' <> skappas) in @@ -1200,15 +1200,15 @@ end = functor (K : CONTINUATION) -> struct * environment passed as an argument already) need to be compiled specially *) let op = if (session_exceptions_enabled && - name = Value.session_exception_operation && + L.equal name Value.session_exception_operation && List.length args = 0) then let affected_variables = VariableInspection.get_affected_variables (K.reify kappa) in let affected_arr = Dict ([("1", Aux.List.of_array (Arr affected_variables))]) in - Dict [ ("_label", strlit name) + Dict [ ("_label", strlit (L.name name)) ; ("_value", Dict [("p", affected_arr); ("s", resumption)]) ] else - Dict [ ("_label", strlit name) + Dict [ ("_label", strlit (L.name name)) ; ("_value", Dict [("p", maybe_box args); ("s", resumption)]) ] in bind_skappa (bind_seta (return (apply_yielding (K.reify seta) [op] kappas)))) @@ -1242,8 +1242,8 @@ end = functor (K : CONTINUATION) -> struct let name_map = List.fold_left (fun box (i, _, initial_value) -> - StringMap.add (string_of_int i) initial_value box) - StringMap.empty params + L.Map.add (L.of_int i) initial_value box) + L.Map.empty params in (Ir.Let (param_ptr_binder, ([], Ir.Return (Ir.Extend (name_map, None)))) :: bs, tc) in @@ -1307,12 +1307,12 @@ end = functor (K : CONTINUATION) -> struct StringMap.fold (fun operation_name clause cases -> StringMap.add operation_name - (if session_exceptions_enabled && operation_name = Value.session_exception_operation + (if session_exceptions_enabled && operation_name = L.name Value.session_exception_operation then let (xb,_,body) = clause in translate_exn_case env scrutinee (xb, body) kappas else translate_eff_case env scrutinee clause kappas) cases) - eff_cases StringMap.empty + (L.label_to_string_map eff_cases) StringMap.empty in let forward y ks = K.bind ks diff --git a/core/label.ml b/core/label.ml new file mode 100644 index 000000000..381585d4a --- /dev/null +++ b/core/label.ml @@ -0,0 +1,191 @@ +open Utility +open CommonTypes + +let show_unique_labels_idents = + Settings.(flag ~default:false "show_unique_labels_idents" + |> privilege `User + |> synopsis "Show the internal numeric identifier for each unique label" + |> convert parse_bool + |> sync) + +let internal_error message = + Errors.internal_error ~filename:"label.ml" ~message +let local_error show lbl = + internal_error ("Label " ^ show lbl ^ " is local but a global label was expected") +let not_local_error show lbl = + internal_error ("Label " ^ show lbl ^ " is global but a local label was expected") +let not_free_error show lbl = + internal_error ("Label " ^ show lbl ^ " is not free") + +module Uid = struct + type t = Id of Int.t | Free + + let show = function + | Free -> "free" + | Id id -> string_of_int id + + let compare uid uid' = match uid, uid' with + | Id id, Id id' -> Int.compare id id' + | Free, Free -> 0 + | Id _, _ -> -1 + | _, Id _ -> 1 + + let counter = ref 0 + + let new_uid () = counter:=!counter+1 ; Id !counter + + let is_free = function + | Free -> true + | _ -> false +end + +module Label = struct + type local = Name.t * Uid.t + type global = Name.t + + type t = + | Local of local + | Global of global + | Number of int + type label = t + + let show = function + | Local (name, id) -> + if Settings.get show_unique_labels_idents + then Printf.sprintf "`%s<%s>" name (Uid.show id) + else Printf.sprintf "`%s" name + | Global name -> name + | Number n -> string_of_int n + + let pp f l = + Format.pp_print_string f begin match l with + | Local (name, id) -> "`"^name ^ "<" ^ Uid.show id ^ ">" + | Global name -> name + | Number n -> string_of_int n + end + + let of_int i = Number i + + let to_int = function + | Number n -> n + | Global i -> int_of_string i + | l -> raise (local_error show l) + + let make_local ?(uid=Uid.Free) name = Local (name, uid) + + let make_global name = Global name + + let make textual_name = + let is_digit ch = + Char.code ch >= 48 && Char.code ch <= 57 + in + if String.for_all is_digit textual_name + then of_int (int_of_string textual_name) + else make_global textual_name + + let name = function + | Local (name,_) -> "`"^name + | Global name -> name + | Number n -> string_of_int n + + let compare lbl lbl' = match lbl,lbl' with + | Local (name, Uid.Free), Local (name', Uid.Free) -> String.compare name name' + | Local (_, uid), Local (_, uid') -> Uid.compare uid uid' + | Global g, Global g' -> String.compare g g' + | Local _, Global _ -> 1 + | Local _, Number _ -> 1 + | Global _, Number _ -> 1 + | Number _, Global _ -> -1 + | Number _, Local _ -> -1 + | Global _, Local _ -> -1 + | Number n, Number m -> Int.compare n m + + let equal lbl lbl' = compare lbl lbl' = 0 + + let textual_equal lbl lbl' = String.compare (name lbl) (name lbl') = 0 + + let name_is lbl name' = String.compare (name lbl) name' = 0 + + let is_local = function + | Local _ -> true + | _ -> false + + let is_global l = not (is_local l) + + let is_free = function + | Local (_, uid) -> Uid.is_free uid + | l -> raise (not_local_error show l) + + let uid = function + | Local (_, uid) -> uid + | l -> raise (not_local_error show l) + + let bind_local ?bind_with lbl = match bind_with, lbl with + | Some bind_lbl, Local (name, Uid.Free) -> Local (name, uid bind_lbl) + | Some _ , Local _ -> raise (not_free_error show lbl) + | None , Local (name, _) -> Local (name, Uid.new_uid ()) + | _ -> raise (not_local_error show lbl) + + let one = of_int 1 + let two = of_int 2 + let return = make_global "return" +end + +include Label + +module type LABELMAP = Utility.Map with type key = t +module Map : LABELMAP = Utility.Map.Make(Label) + +module type LABELSET = Utility.Set with type elt = t +module Set : LABELSET = Utility.Set.Make(Label) + +let string_to_label_map m = + Utility.StringMap.fold + (fun k v m -> Map.add (Label.make k) v m) + m Map.empty + +let label_to_string_map m = + Map.fold + (fun k v m -> Utility.StringMap.add (Label.name k) v m) + m Utility.StringMap.empty + +let string_to_label_set m = + Utility.StringSet.fold + (fun k m -> Set.add (Label.make k) m) + m Set.empty + +let label_to_string_set m = + Set.fold + (fun k m -> Utility.StringSet.add (Label.name k) m) + m Utility.StringSet.empty + +module Env = struct + module M = Utility.StringMap + + type t = (label list) M.t + + let pp = M.pp (Format.pp_print_list Label.pp) + + let empty = M.empty + + let extend = M.superimpose + + let bind env label = + let old_ls = match M.find_opt (name label) env with + | None -> [] + | Some ls -> ls in + M.add (name label) (label::old_ls) env + + let unbind env label = + match M.find_opt (name label) env with + | None -> env + | Some [] | Some [_] -> M.remove (name label) env + | Some (_::ls) -> M.add (name label) ls env + + let bind_labels labels env = List.fold_left bind env labels + let unbind_labels labels env = List.fold_left unbind env labels + + let find_homonyms l env = match M.find_opt (name l) env with + | Some ls -> ls + | None -> [] +end diff --git a/core/label.mli b/core/label.mli new file mode 100644 index 000000000..0c014ebbc --- /dev/null +++ b/core/label.mli @@ -0,0 +1,70 @@ +val show_unique_labels_idents : bool Settings.setting + +module Uid : sig + type t = Id of Int.t | Free +end + +type local = string * Uid.t +type global = string + +type t = + | Local of local + | Global of global + | Number of int + [@@deriving show] +type label = t + +val make_local : ?uid:Uid.t -> string -> t +val make_global : string -> t +val make : string -> t + +val of_int : Int.t -> t +val to_int : t -> Int.t +val name : t -> string + +val compare : t -> t -> int +val equal : t -> t -> bool +val textual_equal : t -> t -> bool +val name_is : t -> string -> bool + +val is_local : t -> bool +val is_global : t -> bool +val is_free : t -> bool + +val uid : t -> Uid.t +val bind_local : ?bind_with:t -> t -> t + + +val one : t +val two : t +val return : t + + +module type LABELMAP = Utility.Map with type key = t +module Map : LABELMAP + +module type LABELSET = Utility.Set with type elt = t +module Set : LABELSET + +val string_to_label_map : 'a Utility.StringMap.t -> 'a Map.t +val label_to_string_map : 'a Map.t -> 'a Utility.StringMap.t +val string_to_label_set : Utility.StringSet.t -> Set.t +val label_to_string_set : Set.t -> Utility.StringSet.t + +module Env : sig + type t + + val pp : Format.formatter -> t -> unit + + val empty : t + + val extend : t -> t -> t + + val bind : t -> label -> t + val unbind : t -> label -> t + + val bind_labels : label list -> t -> t + val unbind_labels : label list -> t -> t + + val find_homonyms : label -> t -> label list +end diff --git a/core/lens_ir_conv.ml b/core/lens_ir_conv.ml index 5f1b0fead..13c3e6743 100644 --- a/core/lens_ir_conv.ml +++ b/core/lens_ir_conv.ml @@ -348,7 +348,9 @@ let lens_sugar_phrase_of_ir p env = | I.Extend (ext_fields, r) -> let r = Option.map ~f:(links_value env) r in Option.value r ~default:(`Record [] |> Result.return) >>= fun r -> - let fields = StringMap.to_alist ext_fields in + let fields = + StringMap.to_alist (Label.label_to_string_map ext_fields) + in List.map_result ~f:(fun (k, v) -> links_value env v >>| fun v -> (k, v)) fields diff --git a/core/lens_sugar_conv.ml b/core/lens_sugar_conv.ml index 9d755e2c6..197f3474c 100644 --- a/core/lens_sugar_conv.ml +++ b/core/lens_sugar_conv.ml @@ -95,7 +95,7 @@ let rec lens_sugar_phrase_of_body v p = Format.asprintf "Unexpected expression to project on: %a" S.pp_phrase var |> Error.internal_error_res) - >>| fun () -> LPS.Var field + >>| fun () -> LPS.Var (Label.name field) | _ -> Format.asprintf "Unsupported sugar phrase in lens sugar phrase of body: %a" S.pp_phrase diff --git a/core/lens_type_conv.ml b/core/lens_type_conv.ml index d971c0fe9..95968dc24 100644 --- a/core/lens_type_conv.ml +++ b/core/lens_type_conv.ml @@ -8,8 +8,13 @@ type 'a die = string -> 'a let to_links_map m = String.Map.fold - (fun k v m -> Utility.StringMap.add k v m) - m Utility.StringMap.empty + (fun k v m -> Label.Map.add (Label.make k) v m) + m Label.Map.empty + +let to_string_map m = + Label.Map.fold + (fun k v m -> String.Map.add (Label.name k) v m) + m String.Map.empty let lookup_alias context ~alias = match Env.String.find_opt alias context with @@ -50,9 +55,9 @@ let rec lens_phrase_type_of_type t = | T.Record r -> lens_phrase_type_of_type r | T.Row (fields, _, _) -> let fields = - Utility.StringMap.to_alist fields - |> String.Map.from_alist - |> String.Map.map (fun v -> + Label.Map.to_alist fields + |> Label.Map.from_alist + |> Label.Map.map (fun v -> match v with | T.Present t -> lens_phrase_type_of_type t | _ -> @@ -60,7 +65,7 @@ let rec lens_phrase_type_of_type t = "lens_phrase_type_of_type only works on records with \ present types.") in - LPT.Record fields + LPT.Record (to_string_map fields) | _ -> failwith @@ Format.asprintf "Unsupported type %a in lens_phrase_type_of_type." T.pp diff --git a/core/lexer.mll b/core/lexer.mll index 47d3f92e4..30b014570 100644 --- a/core/lexer.mll +++ b/core/lexer.mll @@ -98,6 +98,7 @@ let keywords = [ "false" , FALSE; "for" , FOR; "forall" , FORALL; + "fresh" , FRESH; "from" , FROM; "fun" , FUN; "formlet" , FORMLET; @@ -265,6 +266,9 @@ rule lex ctxt nl = parse if op = "<" then ctxt#enter_effect_pattern else if op = ">" then ctxt#leave_effect_pattern); OPERATOR op } + | "`" (def_id as var) { if List.mem_assoc var keywords || not (Char.isUpper var.[0]) then + raise (LexicalError (lexeme lexbuf, lexeme_end_p lexbuf)) + else BTCONSTRUCTOR var } | '`' (def_id as var) '`' { if List.mem_assoc var keywords || Char.isUpper var.[0] then raise (LexicalError (lexeme lexbuf, lexeme_end_p lexbuf)) else OPERATOR var } diff --git a/core/lib.ml b/core/lib.ml index f5f9ac2ba..b0e880674 100644 --- a/core/lib.ml +++ b/core/lib.ml @@ -1726,6 +1726,7 @@ let type_env : Types.environment = let typing_env = {Types.var_env = type_env; Types.rec_vars = StringSet.empty; tycon_env = alias_env; + label_env = Label.Env.empty; Types.effect_row = Types.closed_wild_row; Types.desugared = false } @@ -1746,7 +1747,7 @@ let rec function_arity = function | Function (Record row, _, _) -> let (l, _, _) = TypeUtils.extract_row_parts row in - (Some (StringMap.size l)) + (Some (Label.Map.size l)) | ForAll (_, t) -> function_arity t | _ -> None diff --git a/core/moduleUtils.ml b/core/moduleUtils.ml index 3012a8a34..8a1ce7918 100644 --- a/core/moduleUtils.ml +++ b/core/moduleUtils.ml @@ -168,7 +168,7 @@ let get_data_constructors init_constrs = method! datatypenode = function | Datatype.Variant (xs, _) -> - self#list (fun o (lbl, _) -> o#add_constr lbl) xs + self#list (fun o (lbl, _) -> o#add_constr (Label.name lbl)) xs | dt -> super#datatypenode dt end diff --git a/core/operators.ml b/core/operators.ml index 764017065..6a7fced14 100644 --- a/core/operators.ml +++ b/core/operators.ml @@ -57,6 +57,6 @@ end (* Operator section *) module Section = struct - type t = Minus | FloatMinus | Project of Name.t | Name of Name.t + type t = Minus | FloatMinus | Project of Label.t | Name of Name.t [@@deriving show] end diff --git a/core/page.ml b/core/page.ml index 33c74c6da..17daf4bf7 100644 --- a/core/page.ml +++ b/core/page.ml @@ -120,7 +120,7 @@ module Make_RealPage (C : JS_PAGE_COMPILER) (G : JS_CODEGEN) = struct let escaped_state_string = `String state_string |> Json.json_to_string in let printed_code = - let _venv, code = C.generate_program venv ([], Ir.Return (Ir.Extend (StringMap.empty, None))) in + let _venv, code = C.generate_program venv ([], Ir.Return (Ir.Extend (Label.Map.empty, None))) in let code = f code in let code = code |> (C.generate_stubs valenv defs) |> C.wrap_with_server_lib_stubs diff --git a/core/parser.mly b/core/parser.mly index 97c44b167..d7f7be57b 100644 --- a/core/parser.mly +++ b/core/parser.mly @@ -299,6 +299,8 @@ let parse_foreign_language pos lang = (pos, Printf.sprintf "Unrecognised foreign language '%s'." lang)) let any = any_pat dp +let local_label = Label.make_local +let label = Label.make %} %token EOF @@ -335,7 +337,7 @@ let any = any_pat dp %token UFLOAT %token STRING CDATA REGEXREPL %token CHAR -%token VARIABLE CONSTRUCTOR KEYWORD PERCENTVAR +%token VARIABLE CONSTRUCTOR KEYWORD PERCENTVAR BTCONSTRUCTOR %token LXML ENDTAG %token RXML SLASHRXML %token MU FORALL ALIEN SIG UNSAFE @@ -348,7 +350,7 @@ let any = any_pat dp %token SLASHFLAGS %token UNDERSCORE AS %token FIXITY -%token TYPENAME EFFECTNAME +%token TYPENAME EFFECTNAME FRESH %token TRY OTHERWISE RAISE %token OPERATOR %token USING @@ -454,6 +456,7 @@ nofun_declaration: | typedecl SEMICOLON { $1 } | links_module | links_open SEMICOLON { $1 } | pollute = boption(OPEN) IMPORT CONSTRUCTOR SEMICOLON { import ~ppos:$loc($2) ~pollute [$3] } +| FRESH separated_nonempty_list(COMMA, BTCONSTRUCTOR) SEMICOLON { with_pos $loc (FreshLabel (List.map local_label $2))} alien_datatype: | VARIABLE COLON datatype SEMICOLON { (binder ~ppos:$loc($1) $1, datatype $3) } @@ -678,7 +681,7 @@ unary_expression: | MINUSDOT unary_expression { unary_appl ~ppos:$loc UnaryOp.FloatMinus $2 } | OPERATOR unary_expression { unary_appl ~ppos:$loc (UnaryOp.Name $1) $2 } | postfix_expression | constructor_expression { $1 } -| DOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None)) } +| DOOP constructor loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None)) } infix_appl: | unary_expression { $1 } @@ -979,6 +982,7 @@ binding: | fun_kind VARIABLE arg_lists perhaps_location switch_funlit_body { switch_fun_binding ~ppos:$loc None ($1, $2, $3, $4, $5) } | typedecl SEMICOLON | links_module | links_open SEMICOLON { $1 } +| FRESH separated_nonempty_list(COMMA, BTCONSTRUCTOR) SEMICOLON { with_pos $loc (FreshLabel (List.map local_label $2))} mutual_binding_block: | MUTUAL LBRACE mutual_bindings RBRACE { MutualBindings.flatten $3 } @@ -1010,7 +1014,7 @@ block_contents: | /* empty */ { ([], with_pos $loc (TupleLit [])) } labeled_exp: -| preceded(EQ, VARIABLE) { ($1, with_pos $loc (Var $1)) } +| preceded(EQ, VARIABLE) { (label $1, with_pos $loc (Var $1)) } | separated_pair(record_label, EQ, exp) { $1 } labeled_exps: @@ -1178,14 +1182,14 @@ fields: | fields_def(field, COMMA, row_var, kinded_row_var) { $1 } field: -| CONSTRUCTOR /* allows nullary variant labels */ { ($1, present) } +| CONSTRUCTOR /* allows nullary variant labels */ { (label $1, present) } | field_label fieldspec { ($1, $2) } field_label: -| CONSTRUCTOR { $1 } -| VARIABLE { $1 } -| STRING { $1 } -| UINTEGER { string_of_int $1 } +| CONSTRUCTOR { label $1 } +| VARIABLE { label $1 } +| STRING { label $1 } +| UINTEGER { Label.Number $1 } rfields: | fields_def(rfield, COMMA, row_var, kinded_row_var) { $1 } @@ -1206,8 +1210,8 @@ vfields: | kinded_vrow_var { ([] , $1 ) } vfield: -| CONSTRUCTOR { ($1, present) } -| CONSTRUCTOR fieldspec { ($1, $2) } +| CONSTRUCTOR { (label $1, present) } +| CONSTRUCTOR fieldspec { (label $1, $2) } efields: | efield { ([$1], make_effect_var ~is_dot:false $loc) } @@ -1221,8 +1225,13 @@ efield: | effect_label fieldspec { ($1, $2) } effect_label: -| CONSTRUCTOR { $1 } -| VARIABLE { $1 } +| constructor { $1 } +| VARIABLE { label $1 } + +constructor: +| CONSTRUCTOR { label $1 } +| BTCONSTRUCTOR { local_label $1 } + effect_app: | CONSTRUCTOR { Datatype.EffectApplication($1, []) } @@ -1332,8 +1341,8 @@ resumable_operation_pattern: { with_pos $loc (Pattern.Operation (fst $1, snd $1, any)) } operation_pattern: -| CONSTRUCTOR { ($1, []) } -| CONSTRUCTOR multi_args { ($1, $2) } +| constructor { ($1, []) } +| constructor multi_args { ($1, $2) } typed_pattern: | cons_pattern { $1 } @@ -1345,14 +1354,14 @@ cons_pattern: constructor_pattern: | negative_pattern { $1 } -| CONSTRUCTOR parenthesized_pattern? { with_pos $loc (Pattern.Variant ($1, $2)) } +| constructor parenthesized_pattern? { with_pos $loc (Pattern.Variant ($1, $2)) } constructors: -| separated_nonempty_list(COMMA, CONSTRUCTOR) { $1 } +| separated_nonempty_list(COMMA, constructor) { $1 } negative_pattern: | primary_pattern { $1 } -| MINUS CONSTRUCTOR { with_pos $loc (Pattern.Negative [$2]) } +| MINUS constructor { with_pos $loc (Pattern.Negative [$2]) } | MINUS LPAREN constructors RPAREN { with_pos $loc (Pattern.Negative $3) } parenthesized_pattern: @@ -1373,7 +1382,7 @@ patterns: | separated_nonempty_list(COMMA, pattern) { $1 } labeled_pattern: -| preceded(EQ, VARIABLE) { ($1, variable_pat ~ppos:$loc $1) } +| preceded(EQ, VARIABLE) { (label $1, variable_pat ~ppos:$loc $1) } | separated_pair(record_label, EQ, pattern) { $1 } labeled_patterns: diff --git a/core/query/delateralize.ml b/core/query/delateralize.ml index d34ab5e6e..6d6c27381 100644 --- a/core/query/delateralize.ml +++ b/core/query/delateralize.ml @@ -33,7 +33,7 @@ let graph_query (q1,ty1) x (q2,ty2) = let prom_delateralize gs q1 x (q2,ty2) y (q3,ty3) = let p = Var.fresh_raw_var () in let graph, ftys = graph_query (QL.Dedup q2,ty2) x (q3,ty3) in - let vp = QL.Var (p,Types.make_record_type ftys) in + let vp = QL.Var (p,Types.make_record_type (Label.string_to_label_map ftys)) in let vx = QL.Var (x,ty2) in let eq_test a b = QL.Apply (QL.Primitive "==", [a;b]) in let and_query a b = QL.Apply (QL.Primitive "&&", [a;b]) in diff --git a/core/query/evalNestedQuery.ml b/core/query/evalNestedQuery.ml index 321425222..1d037a342 100644 --- a/core/query/evalNestedQuery.ml +++ b/core/query/evalNestedQuery.ml @@ -90,7 +90,7 @@ struct match TypeUtils.concrete_type t with | Types.Primitive t -> `Primitive t | Types.Record row -> - let (fields, _, _) = TypeUtils.extract_row_parts row in + let fields = TypeUtils.extract_row_parts row |> fst3 |> Label.label_to_string_map in `Record (StringMap.map (function | Present t -> nested_type_of_type t @@ -463,7 +463,7 @@ struct (fun (x, source) -> match source with | QL.Table t -> - let tyx = Types.make_record_type (QL.table_field_types t) in + let tyx = Types.make_record_type (QL.table_field_types t |> Label.string_to_label_map) in QL.eta_expand_var (x, tyx) | _ -> assert false) gs_out) in @@ -487,6 +487,7 @@ struct QL.recdty_field_types (Types.make_tuple_type [r_out_type; index_type]) + |> Label.string_to_label_map |> Types.make_record_type in (q, QL.For (None, gs_out, [], where x_out (QL.Singleton (pair r_out index))), diff --git a/core/query/evalQuery.ml b/core/query/evalQuery.ml index f3faa2b08..57ff5d8d9 100644 --- a/core/query/evalQuery.ml +++ b/core/query/evalQuery.ml @@ -104,7 +104,7 @@ struct function | (x, QL.Table t) -> let field_types = QL.table_field_types t in - let tyx = Types.make_record_type field_types in + let tyx = Types.make_record_type (Label.string_to_label_map field_types) in List.rev (StringMap.fold (fun name _t es -> diff --git a/core/query/mixingQuery.ml b/core/query/mixingQuery.ml index 16173272f..eae33001b 100644 --- a/core/query/mixingQuery.ml +++ b/core/query/mixingQuery.ml @@ -111,8 +111,8 @@ let rec flattened_pair_ft x y = in StringMap.fold (fun f t acc -> StringMap.add (flatfield "2" f) t acc) (Q.field_types_of_row rowy) out1 (* XXX: same as above, using a field with an empty name to deal with variables of non-record type ... will it work? *) - | Q.Var (nx, tyx), _ -> flattened_pair_ft (Q.Var (nx, Types.make_record_type (StringMap.from_alist ["", tyx]))) y - | _, Q.Var (ny, tyy) -> flattened_pair_ft x (Q.Var (ny, Types.make_record_type (StringMap.from_alist ["", tyy]))) + | Q.Var (nx, tyx), _ -> flattened_pair_ft (Q.Var (nx, Types.make_record_type (Label.Map.from_alist [Label.make "", tyx]))) y + | _, Q.Var (ny, tyy) -> flattened_pair_ft x (Q.Var (ny, Types.make_record_type (Label.Map.from_alist [Label.make "", tyy]))) | _ -> assert false (* gs must ALWAYS be non-empty, both input and output!*) @@ -410,12 +410,12 @@ struct label else StringMap.add label (xlate env v) fields) - ext_fields + (Label.label_to_string_map ext_fields) fields) | _ -> Q.query_error "Error adding fields: non-record" end | Project (label, r) -> Q.Project (xlate env r, label) - | Erase (labels, r) -> Q.Erase (xlate env r, labels) + | Erase (labels, r) -> Q.Erase (xlate env r, Label.label_to_string_set labels) | Inject (label, v, _) -> Q.Variant (label, xlate env v) | TAbs (_, v) -> xlate env v | TApp (v, _) -> xlate env v @@ -429,9 +429,9 @@ struct List.map Q.unbox_xml (Q.unbox_list v) @ children) children [] in let children = - StringMap.fold + Label.Map.fold (fun name v attrs -> - Value.Attr (name, Q.unbox_string (xlate env v)) :: attrs) + Value.Attr (Label.name name, Q.unbox_string (xlate env v)) :: attrs) attrs children in Q.Singleton (Q.XML (Value.Node (tag, children))) @@ -513,7 +513,7 @@ struct raise (Errors.runtime_error "special not allowed in query block") | Case (v, cases, default) -> let v' = xlate env v in - let cases' = StringMap.map (fun (x,y) -> (x, computation env y)) cases in + let cases' = Label.Map.map (fun (x,y) -> (x, computation env y)) cases |> Label.label_to_string_map in let default' = opt_app (fun (x,y) -> Some (x, computation env y)) None default in Q.Case (v', cases', default') | If (c, t, e) -> @@ -806,7 +806,7 @@ struct end let compile_update : Value.database -> Value.env -> - ((Ir.var * string * Types.datatype StringMap.t) * Ir.computation option * Ir.computation) -> Sql.query = + ((Ir.var * string * Types.datatype Label.Map.t) * Ir.computation option * Ir.computation) -> Sql.query = fun db env ((x, table, field_types), where, body) -> let tyx = Types.make_record_type field_types in let env = Q.bind (Q.env_of_value_env QueryPolicy.Mixing env) (x, Q.Var (x, tyx)) in @@ -819,7 +819,7 @@ let compile_update : Value.database -> Value.env -> q let compile_delete : Value.database -> Value.env -> - ((Ir.var * string * Types.datatype StringMap.t) * Ir.computation option) -> Sql.query = + ((Ir.var * string * Types.datatype Label.Map.t) * Ir.computation option) -> Sql.query = fun db env ((x, table, field_types), where) -> let tyx = Types.make_record_type field_types in let env = Q.bind (Q.env_of_value_env QueryPolicy.Mixing env) (x, Q.Var (x, tyx)) in diff --git a/core/query/mixingQuery.mli b/core/query/mixingQuery.mli index 789daab11..f393adcd2 100644 --- a/core/query/mixingQuery.mli +++ b/core/query/mixingQuery.mli @@ -29,7 +29,7 @@ sig end val compile_update : Value.database -> Value.env -> - ((Ir.var * string * Types.datatype StringMap.t) * Ir.computation option * Ir.computation) -> Sql.query + ((Ir.var * string * Types.datatype Label.Map.t) * Ir.computation option * Ir.computation) -> Sql.query val compile_delete : Value.database -> Value.env -> - ((Ir.var * string * Types.datatype StringMap.t) * Ir.computation option) -> Sql.query \ No newline at end of file + ((Ir.var * string * Types.datatype Label.Map.t) * Ir.computation option) -> Sql.query diff --git a/core/query/query.ml b/core/query/query.ml index 408425660..81a5e754a 100644 --- a/core/query/query.ml +++ b/core/query/query.ml @@ -173,7 +173,7 @@ let rec reduce_for_source : Q.t * (Q.t -> Q.t) -> Q.t = let (from_field, to_field) = OptionUtils.val_of temporal_fields in (* Transaction / Valid-time tables: Need to wrap as metadata *) (* First, generate a fresh variable for the table *) - let make_spec_map = StringMap.map (fun x -> Types.Present x) in + let make_spec_map m = Label.Map.map (fun x -> Types.Present x) (Label.string_to_label_map m) in let field_types = Q.table_field_types table in let base_field_types = StringMap.filter @@ -341,12 +341,12 @@ struct label else StringMap.add label (xlate env v) fields) - ext_fields + (Label.label_to_string_map ext_fields) fields) | _ -> Q.query_error "Error adding fields: non-record" end | Project (label, r) -> Q.Project (xlate env r, label) - | Erase (labels, r) -> Q.Erase (xlate env r, labels) + | Erase (labels, r) -> Q.Erase (xlate env r, Label.label_to_string_set labels) | Inject (label, v, _) -> Q.Variant (label, xlate env v) | TAbs (_, v) -> xlate env v | TApp (v, _) -> xlate env v @@ -360,9 +360,9 @@ struct List.map Q.unbox_xml (Q.unbox_list v) @ children) children [] in let children = - StringMap.fold + Label.Map.fold (fun name v attrs -> - Value.Attr (name, Q.unbox_string (xlate env v)) :: attrs) + Value.Attr (Label.name name, Q.unbox_string (xlate env v)) :: attrs) attrs children in Q.Singleton (Q.XML (Value.Node (tag, children))) @@ -444,7 +444,7 @@ struct raise (Errors.runtime_error "special not allowed in query block") | Case (v, cases, default) -> let v' = xlate env v in - let cases' = StringMap.map (fun (x,y) -> (x, computation env y)) cases in + let cases' = Label.Map.map (fun (x,y) -> (x, computation env y)) cases |> Label.label_to_string_map in let default' = opt_app (fun (x,y) -> Some (x, computation env y)) None default in Q.Case (v', cases', default') | If (c, t, e) -> @@ -616,7 +616,7 @@ end let compile_update : Value.database -> Value.env -> ((Ir.var * string * Types.datatype StringMap.t) * Ir.computation option * Ir.computation) -> Sql.query = fun db env ((x, table, field_types), where, body) -> - let tyx = Types.make_record_type field_types in + let tyx = Types.make_record_type (Label.string_to_label_map field_types) in let env = Q.bind (Q.env_of_value_env QueryPolicy.Flat env) (x, Q.Var (x, tyx)) in (* let () = opt_iter (fun where -> Debug.print ("where: "^Ir.show_computation where)) where in*) let where = opt_map (Eval.norm_comp env) where in @@ -629,7 +629,7 @@ let compile_update : Value.database -> Value.env -> let compile_delete : Value.database -> Value.env -> ((Ir.var * string * Types.datatype StringMap.t) * Ir.computation option) -> Sql.query = fun db env ((x, table, field_types), where) -> - let tyx = Types.make_record_type field_types in + let tyx = Types.make_record_type (Label.string_to_label_map field_types) in let env = Q.bind (Q.env_of_value_env QueryPolicy.Flat env) (x, Q.Var (x, tyx)) in let where = opt_map (Eval.norm_comp env) where in let q = Q.delete ((x, table), where) in diff --git a/core/query/queryLang.ml b/core/query/queryLang.ml index c76f073ec..9ba31c66e 100644 --- a/core/query/queryLang.ml +++ b/core/query/queryLang.ml @@ -164,10 +164,10 @@ let rec expression_of_base_value : Value.t -> t = function raise (internal_error ("expression_of_base_value undefined for " ^ Value.string_of_value other)) -let field_types_of_spec_map = - StringMap.map (function +let field_types_of_spec_map m = + Label.label_to_string_map (Label.Map.map (function | Types.Present t -> t - | _ -> assert false) + | _ -> assert false) m) let field_types_of_row r = let (field_spec_map,_,_) = TypeUtils.extract_row_parts r in @@ -299,7 +299,7 @@ let rec occurs_free_gens (gs : (Var.var * t) list) q = let rec type_of_expression : t -> Types.datatype = fun v -> let te = type_of_expression in let record fields : Types.datatype = - Types.make_record_type (StringMap.map te fields) + Types.make_record_type (Label.Map.map te (Label.string_to_label_map fields)) in match v with | Var (_,ty) -> ty @@ -634,8 +634,8 @@ let rec select_clause : Sql.index -> bool -> t -> Sql.select_clause = let fields = Sql.Fields (List.rev - (StringMap.fold - (fun name _ fields -> + (Label.Map.fold + (fun label _ fields -> let name = Label.name label in (Sql.Project (var, name), name)::fields) fields [])) diff --git a/core/query/temporalQuery.ml b/core/query/temporalQuery.ml index 913fd2e1b..7302e1429 100644 --- a/core/query/temporalQuery.ml +++ b/core/query/temporalQuery.ml @@ -191,7 +191,7 @@ module TransactionTime = struct let env = Q.bind (Q.env_of_value_env QueryPolicy.Nested env) - (x, Q.Var (x, Types.make_record_type field_types)) + (x, Q.Var (x, Types.make_record_type (Label.string_to_label_map field_types))) in let where = opt_map (Query.Eval.norm_comp env) where in let body = Query.Eval.norm_comp env body in @@ -207,7 +207,7 @@ module TransactionTime = struct let env = Q.bind (Q.env_of_value_env QueryPolicy.Nested env) - (x, Q.Var (x, Types.make_record_type field_types)) in + (x, Q.Var (x, Types.make_record_type (Label.string_to_label_map field_types))) in let where = opt_map (Query.Eval.norm_comp env) where in let q = delete ((x, table), where) to_field in Debug.print ("Generated delete query: " ^ (db#string_of_query q)); @@ -221,8 +221,8 @@ module ValidTime = struct let metadata x field_types from_field to_field = let extended_field_types = field_types - |> StringMap.add from_field Types.datetime_type - |> StringMap.add to_field Types.datetime_type in + |> Label.Map.add (Label.make from_field) Types.datetime_type + |> Label.Map.add (Label.make to_field) Types.datetime_type in let table_var = Q.Var (x, Types.make_record_type extended_field_types) in let metadata_record = StringMap.from_alist [ @@ -681,11 +681,12 @@ module ValidTime = struct fun upd db env ((x, table, field_types), where, body) from_field to_field -> + let field_types' = Label.string_to_label_map field_types in let to_bind = match upd with | Ir.NonsequencedUpdate _ -> - metadata x field_types from_field to_field - | _ -> Q.Var (x, Types.make_record_type field_types) in + metadata x field_types' from_field to_field + | _ -> Q.Var (x, Types.make_record_type field_types') in let env = Q.bind @@ -727,6 +728,7 @@ module ValidTime = struct string (* to field *) -> Sql.query = fun del db env ((x, table, field_types), where) from_field to_field -> + let field_types' = Label.string_to_label_map field_types in let env to_bind = Q.bind (Q.env_of_value_env QueryPolicy.Nested env) @@ -736,7 +738,7 @@ module ValidTime = struct begin match del with | CurrentDeletion -> - let env = env (Q.Var (x, Types.make_record_type field_types)) in + let env = env (Q.Var (x, Types.make_record_type field_types')) in let where = opt_map (Query.Eval.norm_comp env) where in Delete.current ((x, table), where) from_field to_field @@ -744,11 +746,11 @@ module ValidTime = struct (* Same logic as deletion -- just that the metadata * we've bound will be different *) let md = - metadata x field_types from_field to_field in + metadata x field_types' from_field to_field in let where = opt_map (Query.Eval.norm_comp (env md)) where in QueryLang.delete ((x, table), where) | SequencedDeletion { validity_from; validity_to } -> - let env = env (Q.Var (x, Types.make_record_type field_types)) in + let env = env (Q.Var (x, Types.make_record_type field_types')) in let where = opt_map (Query.Eval.norm_comp env) where in Delete.sequenced field_types ((x, table), where, @@ -842,10 +844,10 @@ module TemporalJoin = struct List.fold_left (fun acc (k, x) -> match x with - | Present t -> StringMap.add k t acc + | Present t -> Label.Map.add k t acc | _ -> assert false) - (StringMap.empty) - (fst3 x.row |> StringMap.to_alist) in + (Label.Map.empty) + (fst3 x.row |> Label.Map.to_alist) in (Q.Var (v, Types.make_record_type ty), from_field, to_field) ) tables in diff --git a/core/sugarConstructors.ml b/core/sugarConstructors.ml index bd357ba61..e24c6b93f 100644 --- a/core/sugarConstructors.ml +++ b/core/sugarConstructors.ml @@ -76,7 +76,7 @@ module SugarConstructors (Position : Pos) (* Create a tuple for orderby clauses (includes a hack to ensure that 1-tuples are preserved) *) let orderby_tuple ?(ppos=dp) = function - | [e] -> record ~ppos [("1", e)] + | [e] -> record ~ppos [(Label.one, e)] | es -> with_pos ppos (TupleLit es) let cp_unit ppos = with_pos ppos (CPUnquote ([], tuple ~ppos [])) diff --git a/core/sugarConstructorsIntf.ml b/core/sugarConstructorsIntf.ml index 9959f761c..d1f1fa99d 100644 --- a/core/sugarConstructorsIntf.ml +++ b/core/sugarConstructorsIntf.ml @@ -56,7 +56,7 @@ module type SugarConstructorsSig = sig val block_node : block_body -> phrasenode val datatype : Datatype.with_pos -> Datatype.with_pos * 'a option val cp_unit : t -> cp_phrase - val record : ?ppos:t -> ?exp:phrase -> (Name.t * phrase) list -> phrase + val record : ?ppos:t -> ?exp:phrase -> (Label.t * phrase) list -> phrase val tuple : ?ppos:t -> phrase list -> phrase val orderby_tuple : ?ppos:t -> phrase list -> phrase val list : @@ -138,9 +138,9 @@ module type SugarConstructorsSig = sig (* Database queries *) val db_exps - : ?ppos:t -> (Name.t * phrase) list -> phrase + : ?ppos:t -> (Label.t * phrase) list -> phrase val db_insert - : ?ppos:t -> temporal_insertion option -> phrase -> Name.t list -> phrase -> string option + : ?ppos:t -> temporal_insertion option -> phrase -> Label.t list -> phrase -> string option -> phrase val query : ?ppos:t -> (phrase * phrase) option -> QueryPolicy.t -> phrase -> phrase @@ -171,8 +171,8 @@ module type SugarConstructorsSig = sig -> tbl_keys:(phrase option) -> phrase (* Name *) -> Datatype.with_pos (* Type *) - -> (Name.t * fieldconstraint list) list (* Field constraints *) - -> (Temporality.t * (string * string)) option (* Temporal to/from fields *) + -> (Label.t * fieldconstraint list) list (* Field constraints *) + -> (Temporality.t * (Label.t * Label.t)) option (* Temporal to/from fields *) -> phrase (* Database *) -> phrase (* TableLit *) end diff --git a/core/sugarTraversals.ml b/core/sugarTraversals.ml index 0204f6d57..27a836b51 100644 --- a/core/sugarTraversals.ml +++ b/core/sugarTraversals.ml @@ -70,7 +70,7 @@ class map = let open Section in function | Minus -> Minus | FloatMinus -> FloatMinus - | Project _x -> let _x = o#name _x in Project _x + | Project _x -> let _x = o#label _x in Project _x | Name _x -> let _x = o#name _x in Name _x method subkind : Subkind.t -> Subkind.t = fun x -> x @@ -121,7 +121,7 @@ class map = let _x = o#list (fun o (_x, _x_i1) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#fieldspec _x_i1 in (_x, _x_i1)) _x in let _x_i1 = o#row_var _x_i1 in (_x, _x_i1) @@ -280,20 +280,20 @@ class map = let _x = o#list (fun o (_x, _x_i1) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#phrase _x_i1 in (_x, _x_i1)) _x in let _x_i1 = o#option (fun o -> o#phrase) _x_i1 in RecordLit ((_x, _x_i1)) | Projection ((_x, _x_i1)) -> let _x = o#phrase _x in - let _x_i1 = o#name _x_i1 in Projection ((_x, _x_i1)) + let _x_i1 = o#label _x_i1 in Projection ((_x, _x_i1)) | With ((_x, _x_i1)) -> let _x = o#phrase _x in let _x_i1 = o#list (fun o (_x, _x_i1) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#phrase _x_i1 in (_x, _x_i1)) _x_i1 in With ((_x, _x_i1)) @@ -321,7 +321,7 @@ class map = let t = o#option (fun o -> o#typ) t in DoOperation (op, ps, t) | Operation _x -> - let _x = o#name _x in + let _x = o#label _x in Operation _x | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let m = o#phrase sh_expr in @@ -368,7 +368,7 @@ class map = (* let _x = o#phrase _x in *) (* let _x_i1 = o#phrase _x_i1 in Link ((_x, _x_i1)) *) | Select ((_x, _x_i1)) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#phrase _x_i1 in Select (_x, _x_i1) | Offer ((_x, _x_i1, _x_i2)) -> @@ -404,7 +404,7 @@ class map = let tbl_field_constraints = o#list (fun o (_x, _x_i1) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#list (fun o -> o#fieldconstraint) _x_i1 in (_x, _x_i1)) tbl_field_constraints in @@ -432,8 +432,8 @@ class map = LensFunDepsLit (_x, _x_i1, _x_i2) | LensDropLit ((_x, _x_i1, _x_i2, _x_i3, _x_i4)) -> let _x = o#phrase _x in - let _x_i1 = o#string _x_i1 in - let _x_i2 = o#string _x_i2 in + let _x_i1 = o#label _x_i1 in + let _x_i2 = o#label _x_i2 in let _x_i3 = o#phrase _x_i3 in let _x_i4 = o#option (fun o -> o#unknown) _x_i4 in LensDropLit((_x, _x_i1, _x_i2, _x_i3, _x_i4)) @@ -470,7 +470,7 @@ class map = in DBDelete ((_del, _x, _x_i1, _x_i2)) | DBInsert ((_mode, _x, _x_i1, _x_i2, _x_i3)) -> let _x = o#phrase _x in - let _x_i1 = o#list (fun o -> o#name) _x_i1 in + let _x_i1 = o#list (fun o -> o#label) _x_i1 in let _x_i2 = o#phrase _x_i2 in let _x_i3 = o#option (fun o -> o#phrase) _x_i3 in DBInsert ((_mode, _x, _x_i1, _x_i2, _x_i3)) @@ -482,7 +482,7 @@ class map = let _x_i3 = o#list (fun o (_x, _x_i1) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#phrase _x_i1 in (_x, _x_i1)) _x_i3 in DBUpdate ((_upd, _x, _x_i1, _x_i2, _x_i3)) @@ -556,22 +556,22 @@ class map = let _x_i1 = o#pattern _x_i1 in Cons ((_x, _x_i1)) | List _x -> let _x = o#list (fun o -> o#pattern) _x in List _x | Variant ((_x, _x_i1)) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#option (fun o -> o#pattern) _x_i1 in Variant ((_x, _x_i1)) | Operation (name, ps, k) -> - let name = o#name name in + let name = o#label name in let ps = o#list (fun o -> o#pattern) ps in let k = o#pattern k in Operation (name, ps, k) | Negative _x -> - let _x = o#list (fun o -> o#name) _x + let _x = o#list (fun o -> o#label) _x in Negative _x | Record ((_x, _x_i1)) -> let _x = o#list (fun o (_x, _x_i1) -> - let _x = o#name _x in + let _x = o#label _x in let _x_i1 = o#pattern _x_i1 in (_x, _x_i1)) _x in let _x_i1 = o#option (fun o -> o#pattern) _x_i1 @@ -639,6 +639,20 @@ class map = | Absent -> Absent | Var _x -> let _x = o#type_variable _x in Var _x + method label : Datatype.label -> Datatype.label = + let open Label in function + | Global _x -> let _x = o#name _x in Global _x + | Local (_x, _x_i1) -> + let _x = o#name _x in + let _x_i1 = o#uid _x_i1 in + Local (_x, _x_i1) + | Number n -> let n = o#int n in Number n + + method uid : Label.Uid.t -> Label.Uid.t = + let open Label.Uid in function + | Free -> Free + | Id _x -> let _x = o#int _x in Id _x + method fieldconstraint : fieldconstraint -> fieldconstraint = fun fc -> fc @@ -791,6 +805,9 @@ class map = in let language = o#foreign_language (Alien.language alien) in AlienBlock (Alien.modify ~language ~declarations alien) + | FreshLabel ls -> + let ls = o#list (fun o -> o#label) ls in + FreshLabel ls method binding : binding -> binding = fun p -> @@ -928,7 +945,7 @@ class fold = let open Section in function | Minus -> o | FloatMinus -> o - | Project _x -> let o = o#name _x in o + | Project _x -> let o = o#label _x in o | Name _x -> let o = o#name _x in o method subkind : Subkind.t -> 'self_type = fun _ -> o @@ -973,7 +990,7 @@ class fold = let o = o#list (fun o (_x, _x_i1) -> - let o = o#name _x in let o = o#fieldspec _x_i1 in o) + let o = o#label _x in let o = o#fieldspec _x_i1 in o) _x in let o = o#row_var _x_i1 in o @@ -1109,17 +1126,17 @@ class fold = let o = o#list (fun o (_x, _x_i1) -> - let o = o#name _x in let o = o#phrase _x_i1 in o) + let o = o#label _x in let o = o#phrase _x_i1 in o) _x in let o = o#option (fun o -> o#phrase) _x_i1 in o | Projection ((_x, _x_i1)) -> - let o = o#phrase _x in let o = o#name _x_i1 in o + let o = o#phrase _x in let o = o#label _x_i1 in o | With ((_x, _x_i1)) -> let o = o#phrase _x in let o = o#list (fun o (_x, _x_i1) -> - let o = o#name _x in let o = o#phrase _x_i1 in o) + let o = o#label _x in let o = o#phrase _x_i1 in o) _x_i1 in o | TypeAnnotation ((_x, _x_i1)) -> @@ -1136,8 +1153,8 @@ class fold = let o = o#phrase op in let o = o#option (fun o -> o#unknown) t in let o = o#list (fun o -> o#phrase) ps in o - | Operation (_x) -> - let o = o#name _x in o + | Operation _x -> + let o = o#label _x in o | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let o = o#phrase sh_expr in let o = @@ -1181,7 +1198,7 @@ class fold = (* let o = o#phrase _x_i1 *) (* in o *) | Select ((_x, _x_i1)) -> - let o = o#name _x in + let o = o#label _x in let o = o#phrase _x_i1 in o | Offer ((_x, _x_i1, _x_i2)) -> @@ -1214,7 +1231,7 @@ class fold = let o = o#list (fun o (_x, _x_i1) -> - let o = o#name _x in + let o = o#label _x in let o = o#list (fun o -> o#fieldconstraint) _x_i1 in o) tbl_field_constraints in let o = o#phrase tbl_keys in @@ -1238,8 +1255,8 @@ class fold = o | LensDropLit ((_x, _x_i1, _x_i2, _x_i3, _x_i4)) -> let o = o#phrase _x in - let o = o#string _x_i1 in - let o = o#string _x_i2 in + let o = o#label _x_i1 in + let o = o#label _x_i2 in let o = o#phrase _x_i3 in let o = o#option (fun o -> o#unknown) _x_i4 in o @@ -1274,7 +1291,7 @@ class fold = let o = o#option (fun o -> o#phrase) _x_i2 in o | DBInsert ((_mode, _x, _x_i1, _x_i2, _x_i3)) -> let o = o#phrase _x in - let o = o#list (fun o -> o#name) _x_i1 in + let o = o#list (fun o -> o#label) _x_i1 in let o = o#phrase _x_i2 in let o = o#option (fun o -> o#phrase) _x_i3 in o | DBUpdate ((_upd, _x, _x_i1, _x_i2, _x_i3)) -> let o = o#option (fun o -> o#temporal_update) _upd in @@ -1284,7 +1301,7 @@ class fold = let o = o#list (fun o (_x, _x_i1) -> - let o = o#name _x in let o = o#phrase _x_i1 in o) + let o = o#label _x in let o = o#phrase _x_i1 in o) _x_i3 in o | Xml ((_x, _x_i1, _x_i2, _x_i3)) -> @@ -1347,20 +1364,20 @@ class fold = let o = o#pattern _x in let o = o#pattern _x_i1 in o | List _x -> let o = o#list (fun o -> o#pattern) _x in o | Variant ((_x, _x_i1)) -> - let o = o#name _x in + let o = o#label _x in let o = o#option (fun o -> o#pattern) _x_i1 in o | Operation (name, ps, k) -> - let o = o#name name in + let o = o#label name in let o = o#list (fun o -> o#pattern) ps in let o = o#pattern k in o | Negative _x -> - let o = o#list (fun o -> o#name) _x in o + let o = o#list (fun o -> o#label) _x in o | Record ((_x, _x_i1)) -> let o = o#list (fun o (_x, _x_i1) -> - let o = o#name _x in let o = o#pattern _x_i1 in o) + let o = o#label _x in let o = o#pattern _x_i1 in o) _x in let o = o#option (fun o -> o#pattern) _x_i1 in o | Tuple _x -> let o = o#list (fun o -> o#pattern) _x in o @@ -1423,6 +1440,20 @@ class fold = method fieldconstraint : fieldconstraint -> 'self_type = fun _ -> o + method label : Datatype.label -> 'self_type = + let open Label in function + | Global _x -> let o = o#name _x in o + | Local (_x, _x_i1) -> + let o = o#name _x in + let o = o#uid _x_i1 in + o + | Number n -> o#int n + + method uid : Label.Uid.t -> 'self_type = + let open Label.Uid in function + | Free -> o + | Id _x -> let o = o#int _x in o + method directive : directive -> 'self_type = fun (_x, _x_i1) -> let o = o#string _x in let o = o#list (fun o -> o#string) _x_i1 in o @@ -1562,6 +1593,9 @@ class fold = let o = o#binder b in o#datatype' dt) (Alien.declarations alien) + | FreshLabel ls -> + let o = o#list (fun o -> o#label) ls in + o method binding : binding -> 'self_type = WithPos.traverse @@ -1700,7 +1734,7 @@ class fold_map = let open Section in function | Minus -> (o, Minus) | FloatMinus -> (o, FloatMinus) - | Project _x -> let (o, _x) = o#name _x in (o, Project _x) + | Project _x -> let (o, _x) = o#label _x in (o, Project _x) | Name _x -> let (o, _x) = o#name _x in (o, Name _x) method subkind : Subkind.t -> ('self_type * Subkind.t) = fun k -> (o, k) @@ -1734,7 +1768,7 @@ class fold_map = method row_var : Datatype.row_var -> ('self_type * Datatype.row_var) = let open Datatype in function | EffectApplication (_x, _x_i1) -> - let (o, _x) = o#string _x in + let (o, _x) = o#name _x in let (o, _x_i1) = o#list (fun o -> o#type_arg) _x_i1 in (o, EffectApplication (_x, _x_i1)) | Closed -> (o, Closed) @@ -1749,7 +1783,7 @@ class fold_map = let (o, _x) = o#list (fun o (_x, _x_i1) -> - let (o, _x) = o#string _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#fieldspec _x_i1 in (o, (_x, _x_i1))) _x in let (o, _x_i1) = o#row_var _x_i1 in (o, (_x, _x_i1)) @@ -1911,20 +1945,20 @@ class fold_map = let (o, _x) = o#list (fun o (_x, _x_i1) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#phrase _x_i1 in (o, (_x, _x_i1))) _x in let (o, _x_i1) = o#option (fun o -> o#phrase) _x_i1 in (o, (RecordLit ((_x, _x_i1)))) | Projection ((_x, _x_i1)) -> let (o, _x) = o#phrase _x in - let (o, _x_i1) = o#name _x_i1 in (o, (Projection ((_x, _x_i1)))) + let (o, _x_i1) = o#label _x_i1 in (o, (Projection ((_x, _x_i1)))) | With ((_x, _x_i1)) -> let (o, _x) = o#phrase _x in let (o, _x_i1) = o#list (fun o (_x, _x_i1) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#phrase _x_i1 in (o, (_x, _x_i1))) _x_i1 in (o, (With ((_x, _x_i1)))) @@ -1954,7 +1988,7 @@ class fold_map = let (o, ps) = o#list (fun o -> o#phrase) ps in (o, DoOperation (op, ps, t)) | Operation _x -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in (o, Operation _x) | Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } -> let (o, m) = o#phrase sh_expr in @@ -2001,7 +2035,7 @@ class fold_map = (* let (o, _x) = o#phrase _x in *) (* let (o, _x_i1) = o#phrase _x in (o, (Link(_x, _x_i1))) *) | Select ((_x, _x_i1)) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#phrase _x_i1 in (o, (Select (_x, _x_i1))) | Offer ((_x, _x_i1, _x_i2)) -> @@ -2047,7 +2081,7 @@ class fold_map = let (o, tbl_field_constraints) = o#list (fun o (_x, _x_i1) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#list (fun o -> o#fieldconstraint) _x_i1 in (o, (_x, _x_i1))) tbl_field_constraints in @@ -2076,8 +2110,8 @@ class fold_map = (o, (LensFunDepsLit (_x, _x_i1, _x_i2))) | LensDropLit ((_x, _x_i1, _x_i2, _x_i3, _x_i4)) -> let (o, _x) = o#phrase _x in - let (o, _x_i1) = o#string _x_i1 in - let (o, _x_i2) = o#string _x_i2 in + let (o, _x_i1) = o#label _x_i1 in + let (o, _x_i2) = o#label _x_i2 in let (o, _x_i3) = o#phrase _x_i3 in let (o, _x_i4) = o#option (fun o -> o#unknown) _x_i4 in (o, (LensDropLit ((_x, _x_i1, _x_i2, _x_i3, _x_i4)))) @@ -2114,7 +2148,7 @@ class fold_map = in (o, (DBDelete ((_del, _x, _x_i1, _x_i2)))) | DBInsert ((_mode, _x, _x_i1, _x_i2, _x_i3)) -> let (o, _x) = o#phrase _x in - let (o, _x_i1) = o#list (fun o -> o#name) _x_i1 in + let (o, _x_i1) = o#list (fun o -> o#label) _x_i1 in let (o, _x_i2) = o#phrase _x_i2 in let (o, _x_i3) = o#option (fun o -> o#phrase) _x_i3 in (o, (DBInsert ((_mode, _x, _x_i1, _x_i2, _x_i3)))) @@ -2126,7 +2160,7 @@ class fold_map = let (o, _x_i3) = o#list (fun o (_x, _x_i1) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#phrase _x_i1 in (o, (_x, _x_i1))) _x_i3 in (o, (DBUpdate ((_upd, _x, _x_i1, _x_i2, _x_i3)))) @@ -2231,21 +2265,21 @@ class fold_map = | List _x -> let (o, _x) = o#list (fun o -> o#pattern) _x in (o, (List _x)) | Variant ((_x, _x_i1)) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#option (fun o -> o#pattern) _x_i1 in (o, (Variant ((_x, _x_i1)))) | Operation (name, ps, k) -> - let (o, name) = o#name name in + let (o, name) = o#label name in let (o, ps) = o#list (fun o -> o#pattern) ps in let (o, k) = o#pattern k in (o, Operation (name, ps, k)) | Negative _x -> - let (o, _x) = o#list (fun o -> o#name) _x in (o, (Negative _x)) + let (o, _x) = o#list (fun o -> o#label) _x in (o, (Negative _x)) | Record ((_x, _x_i1)) -> let (o, _x) = o#list (fun o (_x, _x_i1) -> - let (o, _x) = o#name _x in + let (o, _x) = o#label _x in let (o, _x_i1) = o#pattern _x_i1 in (o, (_x, _x_i1))) _x in let (o, _x_i1) = o#option (fun o -> o#pattern) _x_i1 @@ -2320,6 +2354,22 @@ class fold_map = method fieldconstraint : fieldconstraint -> ('self_type * fieldconstraint) = fun fc -> (o, fc) + method label : Datatype.label -> ('self_type * Datatype.label) = + let open Label in function + | Global _x -> let (o,_x) = o#name _x in (o, Global _x) + | Local (_x, _x_i1) -> + let (o, _x) = o#name _x in + let (o, _x_i1) = o#uid _x_i1 in + (o, Local (_x, _x_i1)) + | Number n -> + let (o, n) = o#int n in + (o, Number n) + + method uid : Label.Uid.t -> ('self_type * Label.Uid.t) = + let open Label.Uid in function + | Free -> (o, Free) + | Id _x -> let (o, _x) = o#int _x in (o, Id _x) + method directive : directive -> ('self_type * directive) = fun (_x, _x_i1) -> let (o, _x) = o#string _x in @@ -2499,6 +2549,10 @@ class fold_map = (Alien.declarations alien) in o, AlienBlock (Alien.modify ~language:lang ~declarations alien) + | FreshLabel ls -> + let (o, ls) = o#list (fun o -> o#label) ls in + (o, FreshLabel ls) + method binding : binding -> ('self_type * binding) = WithPos.traverse_map diff --git a/core/sugarTraversals.mli b/core/sugarTraversals.mli index d3fb2a34d..8a5f45e3f 100644 --- a/core/sugarTraversals.mli +++ b/core/sugarTraversals.mli @@ -59,6 +59,8 @@ class map : method handle_params : handler_parameterisation -> handler_parameterisation method fieldspec : Datatype.fieldspec -> Datatype.fieldspec method fieldconstraint : fieldconstraint -> fieldconstraint + method label : Datatype.label -> Datatype.label + method uid : Label.Uid.t -> Label.Uid.t method directive : directive -> directive method datatype : Datatype.with_pos -> Datatype.with_pos method datatypenode : Datatype.t -> Datatype.t @@ -143,6 +145,8 @@ class fold : method handle_params : handler_parameterisation -> 'self method fieldspec : Datatype.fieldspec -> 'self method fieldconstraint : fieldconstraint -> 'self + method label : Datatype.label -> 'self + method uid : Label.Uid.t -> 'self method directive : directive -> 'self method datatype : Datatype.with_pos -> 'self method datatypenode : Datatype.t -> 'self @@ -198,6 +202,8 @@ object ('self) method directive : directive -> 'self * directive method fieldconstraint : fieldconstraint -> 'self * fieldconstraint method fieldspec : Datatype.fieldspec -> 'self * Datatype.fieldspec + method label : Datatype.label -> 'self * Datatype.label + method uid : Label.Uid.t -> 'self * Label.Uid.t method int : int -> 'self * int method float : float -> 'self * float method funlit : funlit -> 'self * funlit diff --git a/core/sugartoir.ml b/core/sugartoir.ml index 6d2d8077c..5972d263a 100644 --- a/core/sugartoir.ml +++ b/core/sugartoir.ml @@ -129,11 +129,11 @@ sig val letvar : (var_info * tail_computation sem * tyvar list * (var -> tail_computation sem)) -> tail_computation sem - val xml : value sem * string * (Name.t * (value sem) list) list * (value sem) list -> value sem - val record : (Name.t * value sem) list * (value sem) option -> value sem + val xml : value sem * string * (Label.t * (value sem) list) list * (value sem) list -> value sem + val record : (Label.t * value sem) list * (value sem) option -> value sem val project : value sem * Name.t -> value sem - val update : value sem * (Name.t * value sem) list -> value sem + val update : value sem * (Label.t * value sem) list -> value sem val coerce : value sem * datatype -> value sem @@ -155,7 +155,7 @@ sig | `ValidSequencedDelete of (value sem * value sem) | `ValidNonsequencedDelete ] option * CompilePatterns.Pattern.t * value sem * tail_computation sem option) -> tail_computation sem - val do_operation : Name.t * (value sem) list * Types.datatype -> tail_computation sem + val do_operation : Label.t * (value sem) list * Types.datatype -> tail_computation sem val handle : env -> (tail_computation sem * (CompilePatterns.Pattern.t * (env -> tail_computation sem)) list * @@ -423,14 +423,14 @@ struct (fun attrs -> M.bind children (fun children -> - let attrs = StringMap.from_alist attrs in + let attrs = Label.Map.from_alist attrs in lift (XmlNode (name, attrs, children), Types.xml_type))) let record (fields, r) = let field_types = List.fold_left - (fun field_types (name, s) -> StringMap.add name (sem_type s) field_types) - StringMap.empty + (fun field_types (name, s) -> Label.Map.add name (sem_type s) field_types) + Label.Map.empty fields in let s' = lift_alist fields in match r with @@ -438,16 +438,16 @@ struct let t = Types.make_record_type field_types in M.bind s' (fun fields -> - lift (Extend (StringMap.from_alist fields, None), t)) + lift (Extend (Label.Map.from_alist fields, None), t)) | Some s -> let t = Types.Record (Types.extend_row field_types (TypeUtils.extract_row (sem_type s))) in bind s (fun r -> M.bind s' - (fun fields -> lift (Extend (StringMap.from_alist fields, Some r), t))) + (fun fields -> lift (Extend (Label.Map.from_alist fields, Some r), t))) let project (s, name) = - let t = TypeUtils.project_type name (sem_type s) in + let t = TypeUtils.project_type (Label.make name) (sem_type s) in bind s (fun v -> lift (Project (name, v), t)) let erase (s, names) = @@ -466,8 +466,8 @@ struct let names = List.fold_left (fun names (name, _) -> - StringSet.add name names) - StringSet.empty + Label.Set.add name names) + Label.Set.empty fields in record (fields, Some (erase (s, names))) @@ -492,7 +492,7 @@ struct let case_zero (s, t) = bind s (fun v -> - lift (Case (v, StringMap.empty, None), t)) + lift (Case (v, Label.Map.empty, None), t)) let database s = bind s (fun v -> lift (Special (Database v), Types.Primitive Primitive.DB)) @@ -572,7 +572,7 @@ struct M.bind (alien_binding (x_info, object_name, language)) rest let select (l, e) = - let t = TypeUtils.select_type l (sem_type e) in + let t = TypeUtils.select_type (Label.make l) (sem_type e) in bind e (fun v -> lift (Special (Select (l, v)), t)) let offer env (v, cases, t) = @@ -960,15 +960,15 @@ struct *) ec e | TupleLit es -> - let fields = mapIndex (fun e i -> (string_of_int (i+1), ev e)) es in + let fields = mapIndex (fun e i -> (Label.of_int (i+1), ev e)) es in cofv (I.record (fields, None)) | RecordLit (fields, rest) -> cofv (I.record (List.map (fun (name, e) -> (name, ev e)) fields, opt_map ev rest)) - | Projection (e, name) -> - cofv (I.project (ev e, name)) + | Projection (e, label) -> + cofv (I.project (ev e, Label.name label)) | With (e, fields) -> cofv (I.update (ev e, @@ -1047,7 +1047,7 @@ struct in I.switch env (ev e, cases, t) | DatabaseLit (name, (None, _)) -> - I.database (ev (WithPos.make ~pos (RecordLit ([("name", name)], + I.database (ev (WithPos.make ~pos (RecordLit ([(Label.make "name", name)], Some (WithPos.make ~pos (FnAppl (WithPos.make ~pos (Var "getDatabaseConfig"), []))))))) | DatabaseLit (name, (Some driver, args)) -> let args = @@ -1056,7 +1056,7 @@ struct | Some args -> args in I.database - (ev (WithPos.make ~pos (RecordLit ([("name", name); ("driver", driver); ("args", args)], None)))) + (ev (WithPos.make ~pos (RecordLit ([(Label.make "name", name); (Label.make "driver", driver); (Label.make "args", args)], None)))) | LensLit (table, Some t) -> let table = ev table in I.lens_handle (table, t) @@ -1067,7 +1067,7 @@ struct | LensDropLit (lens, drop, key, default, Some t) -> let lens = ev lens in let default = ev default in - I.lens_drop_handle (lens, drop, key, default, t) + I.lens_drop_handle (lens, Label.name drop, Label.name key, default, t) | LensSelectLit (lens, pred, Some t) -> let lens = ev lens in let trow = Lens.Type.sort t |> Lens.Sort.record_type in @@ -1098,7 +1098,7 @@ struct tbl_name; tbl_type = (tmp, _, Some (readtype, writetype, neededtype)); tbl_keys; tbl_temporal_fields; tbl_database; _ } -> I.table_handle (ev tbl_database, ev tbl_name, ev tbl_keys, - (tmp, readtype, writetype, neededtype), tbl_temporal_fields) + (tmp, readtype, writetype, neededtype), OptionUtils.opt_map (fun (x,y) -> Label.name x, Label.name y) tbl_temporal_fields) (* (name, (_, Some (readtype, writetype, neededtype)), _constraints, keys, db) -> *) | Xml (tag, attrs, attrexp, children) -> if tag = "#" then @@ -1110,6 +1110,7 @@ struct List.map ev children)) else let attrs = alistmap (List.map ev) attrs in + let attrs = List.map (fun (l,v) -> Label.make l, v) attrs in let children = List.map ev children in let body = I.xml (instantiate "^^" [(Row, eff)], tag, attrs, children) in @@ -1185,7 +1186,7 @@ struct I.db_delete env (del, p, source, where) | DBTemporalJoin (mode, e, _) -> I.temporal_join (mode, ec e) | Select (l, e) -> - I.select (l, ev e) + I.select (Label.name l, ev e) | Offer (e, cases, Some t) -> let eff = lookup_effects env in let cases = @@ -1333,6 +1334,7 @@ struct let xt = Binder.to_type binder in I.alien (Var.make_info xt x scope, Alien.object_name alien, Alien.language alien, fun v -> eval_bindings scope (extend [x] [(v, xt)] env) bs e) + | FreshLabel _ -> eval_bindings scope env bs e (* TODO: is that right ? ignore local labels *) | Aliases _ | Infix _ -> (* Ignore type alias and infix declarations - they diff --git a/core/sugartypes.ml b/core/sugartypes.ml index 86de77bfb..48dd4e9c5 100644 --- a/core/sugartypes.ml +++ b/core/sugartypes.ml @@ -208,9 +208,9 @@ module Datatype = struct | Dual of with_pos | End and with_pos = t WithPos.t - and row = (string * fieldspec) list * row_var + and row = (label * fieldspec) list * row_var and row_var = - | EffectApplication of string * type_arg list + | EffectApplication of Name.t * type_arg list | Closed | Open of SugarTypeVar.t | Recursive of SugarTypeVar.t * row @@ -222,6 +222,7 @@ module Datatype = struct | Type of with_pos | Row of row | Presence of fieldspec + and label = Label.t [@@deriving show] end @@ -242,12 +243,10 @@ module Pattern = struct | Nil | Cons of with_pos * with_pos | List of with_pos list - | Variant of Name.t * with_pos option - (* | Effect of Name.t * with_pos list * with_pos *) - (* | Effect2 of with_pos list * with_pos option *) + | Variant of Label.t * with_pos option | Operation of Label.t * with_pos list * with_pos - | Negative of Name.t list - | Record of (Name.t * with_pos) list * with_pos option + | Negative of Label.t list + | Record of (Label.t * with_pos) list * with_pos option | Tuple of with_pos list | Constant of Constant.t | Variable of Binder.with_pos @@ -401,9 +400,9 @@ and table_lit = { tbl_type: (Temporality.t * Datatype.with_pos * (Types.datatype * Types.datatype * Types.datatype) option); - tbl_field_constraints: (Name.t * fieldconstraint list) list; + tbl_field_constraints: (Label.t * fieldconstraint list) list; tbl_keys: phrase; - tbl_temporal_fields: (string * string) option; + tbl_temporal_fields: (Label.t * Label.t) option; tbl_database: phrase } and iterpatt = @@ -466,16 +465,16 @@ and phrasenode = | TAbstr of SugarQuantifier.t list * phrase | TAppl of phrase * type_arg' list | TupleLit of phrase list - | RecordLit of (Name.t * phrase) list * phrase option - | Projection of phrase * Name.t - | With of phrase * (Name.t * phrase) list + | RecordLit of (Label.t * phrase) list * phrase option + | Projection of phrase * Label.t + | With of phrase * (Label.t * phrase) list | TypeAnnotation of phrase * datatype' | Upcast of phrase * datatype' * datatype' | Instantiate of phrase | Generalise of phrase | ConstructorLit of Name.t * phrase option * Types.datatype option | DoOperation of phrase * phrase list * Types.datatype option - | Operation of Name.t + | Operation of Label.t | Handle of handler | Switch of phrase * (Pattern.with_pos * phrase) list * Types.datatype option @@ -483,18 +482,18 @@ and phrasenode = | DatabaseLit of phrase * (phrase option * phrase option) | TableLit of table_lit | DBDelete of temporal_deletion option * Pattern.with_pos * phrase * phrase option - | DBInsert of temporal_insertion option * phrase * Name.t list * phrase * phrase option + | DBInsert of temporal_insertion option * phrase * Label.t list * phrase * phrase option | DBUpdate of temporal_update option * Pattern.with_pos * phrase * - phrase option * (Name.t * phrase) list + phrase option * (Label.t * phrase) list | DBTemporalJoin of Temporality.t * phrase * Types.datatype option | LensLit of phrase * Lens.Type.t option | LensSerialLit of phrase * string list * Lens.Type.t option (* the lens keys lit is a literal that takes an expression and is converted into a LensLit with the corresponding table keys marked in the lens_sort *) | LensKeysLit of phrase * phrase * Lens.Type.t option - | LensFunDepsLit of phrase * (string list * string list) list * + | LensFunDepsLit of phrase * (Label.t list * Label.t list) list * Lens.Type.t option - | LensDropLit of phrase * string * string * phrase * + | LensDropLit of phrase * Label.t * Label.t * phrase * Lens.Type.t option | LensSelectLit of phrase * phrase * Lens.Type.t option | LensJoinLit of phrase * phrase * phrase * phrase * phrase * @@ -511,7 +510,7 @@ and phrasenode = | PagePlacement of phrase | FormBinding of phrase * Pattern.with_pos (* choose *) - | Select of Name.t * phrase + | Select of Label.t * phrase (* choice *) | Offer of phrase * (Pattern.with_pos * phrase) list * Types.datatype option @@ -535,6 +534,7 @@ and bindingnode = | Exp of phrase | Module of { binder: Binder.with_pos; members: binding list } | AlienBlock of Alien.multi Alien.t + | FreshLabel of Label.t list and binding = bindingnode WithPos.t and block_body = binding list * phrase and cp_phrasenode = @@ -817,6 +817,7 @@ struct | Import _ | Open _ | Aliases _ -> empty, empty + | FreshLabel _ -> empty, empty (* This is technically a declaration, thus the name should probably be treated as bound rather than free. *) | Infix { name; _ } -> empty, singleton name diff --git a/core/transformSugar.ml b/core/transformSugar.ml index 3b3d668a1..22b89bcec 100644 --- a/core/transformSugar.ml +++ b/core/transformSugar.ml @@ -24,7 +24,7 @@ let type_section env = let (fields, rho, _) = TypeUtils.extract_row_parts row in let eb, e = Types.fresh_row_quantifier default_effect_subkind in - let r = Record (Row (StringMap.add label (Present a) fields, rho, false)) in + let r = Record (Row (Label.Map.add label (Present a) fields, rho, false)) in ForAll ([ab; rhob; eb], Function (Types.make_tuple_type [r], e, a)) | Name var -> TyEnv.find var env @@ -432,13 +432,13 @@ class transform (env : Types.typing_environment) = let (o, fields, field_types) = let rec list o = function - | [] -> (o, [], StringMap.empty) + | [] -> (o, [], Label.Map.empty) | (name, e)::fields -> let (o, e, t) = o#phrase e in let (o, fields, field_types) = list o fields in (o, (name, e)::fields, - StringMap.add name t field_types) + Label.Map.add name t field_types) in list o fields in let (o, base, base_type) = option o (fun o -> o#phrase) base in @@ -471,7 +471,7 @@ class transform (env : Types.typing_environment) = let ( fs, rv, closed ) = Types.flatten_row row |> TypeUtils.extract_row_parts in - let fs = List.fold_left2 (fun fs (name, _) t -> StringMap.add name (Present t) fs) fs fields ts in + let fs = List.fold_left2 (fun fs (name, _) t -> Label.Map.add name (Present t) fs) fs fields ts in Record (Row (fs, rv, closed)) | _ -> t in @@ -905,6 +905,9 @@ class transform (env : Types.typing_environment) = | (Infix _) as node -> (o, node) | Exp e -> let (o, e, _) = o#phrase e in (o, Exp e) + | FreshLabel ls -> + (* do we wanna do something with labels ? *) + (o, FreshLabel ls) | AlienBlock _ -> assert false | Module _ -> assert false | Import _ -> assert false diff --git a/core/typeSugar.ml b/core/typeSugar.ml index ef4eb0509..a1e59c58f 100644 --- a/core/typeSugar.ml +++ b/core/typeSugar.ml @@ -156,6 +156,7 @@ struct | Funs _ | Infix _ | Aliases _ + | FreshLabel _ | Foreign _ -> true | Exp p -> is_pure p | Val (pat, (_, rhs), _, _) -> @@ -256,6 +257,7 @@ sig val handle_unify_with_context : griper val do_operation : griper + val operation : griper val try_effect : griper @@ -691,6 +693,15 @@ end "but, the currently allowed effects are" ^ nl() ^ tab() ^ code ( show_effectrow (TypeUtils.extract_row lt))) + let operation ~pos ~t1:(lexpr,lt) ~t2:(_,rt) ~error:_ = + build_tyvar_names [lt;rt]; + die pos ("Invocation of the operation " ^ nl() ^ + tab() ^ (code lexpr) ^ nl() ^ + "has type " ^ nl() ^ + tab() ^ code (show_type lt) ^ nl() ^ + "while it is expected to have type" ^ nl() + ^ tab() ^ code ( show_type rt )) + let try_effect ~pos ~t1:(_,lt) ~t2:(_,rt) ~error:_ = build_tyvar_names [lt;rt]; die pos ("Catching a session exception requires an effect context " ^ nli() ^ @@ -1652,6 +1663,9 @@ type context = Types.typing_environment = { and "Formlet". *) tycon_env : Types.tycon_environment; + (* local labels *) + label_env : Label.Env.t; + (* the current effects *) effect_row : Types.row; @@ -1664,6 +1678,7 @@ let empty_context eff desugared = { var_env = Env.empty; rec_vars = StringSet.empty; tycon_env = Env.empty; + label_env = Label.Env.empty; effect_row = eff; desugared } @@ -1674,12 +1689,18 @@ let bind_effects context r = {context with effect_row = Types.flatten_r let lookup_effect context name = match context.effect_row with - | Types.Row (fields, _, _) -> begin match Utility.StringMap.find_opt name fields with + | Types.Row (fields, _, _) -> begin match Label.Map.find_opt name fields with | Some (Types.Present t) -> Some t | _ -> None end | _ -> raise (internal_error "Effect row in the context is not a row") +(* let unbind_alias context v = {context with tycon_env = Env.unbind v context.tycon_env} *) +let bind_labels context ls = {context with label_env = Label.Env.bind_labels ls context.label_env} +(* let unbind_labels context ls = {context with label_env = Label.Env.unbind_labels ls context.label_env} *) + +(* let extend = Types.extend_typing_environment *) + (* TODO(dhil): I have extracted the Usage abstraction from my name hygiene/compilation unit patch. The below module is a compatibility module which will make it easier for me to merge my other branch @@ -1825,8 +1846,8 @@ let type_section pos context s = let a = Types.fresh_type_variable (lin_unl, res_any) in let rho = Types.fresh_row_variable (lin_unl, res_any) in let effects = Types.make_empty_open_row default_effect_subkind in (* projection is pure! *) - let r = Record (Row (StringMap.add label (Present a) StringMap.empty, rho, false)) in - ([(PrimaryKind.Type, a); (PrimaryKind.Row, Row (StringMap.empty, rho, false)); (PrimaryKind.Row, effects)], + let r = Record (Row (Label.Map.add label (Present a) Label.Map.empty, rho, false)) in + ([(PrimaryKind.Type, a); (PrimaryKind.Row, Row (Label.Map.empty, rho, false)); (PrimaryKind.Row, effects)], Function (Types.make_tuple_type [r], effects, a)), Usage.empty | Name var -> @@ -1847,11 +1868,11 @@ let type_frozen_section context s = | Project label -> let a = Types.fresh_rigid_type_variable (lin_unl, res_any) in let rho = Types.fresh_rigid_row_variable (lin_unl, res_any) in - let effects = StringMap.empty, Types.fresh_rigid_row_variable default_effect_subkind, false in - let r = Record (Row (StringMap.add label (Present a) StringMap.empty, rho, false)) in + let effects = Label.Map.empty, Types.fresh_rigid_row_variable default_effect_subkind, false in + let r = Record (Row (Label.Map.add label (Present a) Label.Map.empty, rho, false)) in Types.for_all (Types.quantifiers_of_type_args [(PrimaryKind.Type, a); - (PrimaryKind.Row, Row (StringMap.empty, rho, false)); + (PrimaryKind.Row, Row (Label.Map.empty, rho, false)); (PrimaryKind.Row, Row effects)], Function (Types.make_tuple_type [r], Row effects, a)), Usage.empty @@ -1939,15 +1960,15 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty List.nth ps i | Nil | Cons _ | List _ | Record _ | Variant _ | Negative _ | Operation _ -> assert false in let fields = - StringMap.fold(* true if the row variable is dualised *) + Label.Map.fold(* true if the row variable is dualised *) (fun name -> function | Present t -> - let pats = List.map (unwrap_at ((int_of_string name) - 1)) pats in - StringMap.add name (Present (cpt pats t)) + let pats = List.map (unwrap_at ((Label.to_int name) - 1)) pats in + Label.Map.add name (Present (cpt pats t)) | (Absent | Meta _) -> assert false - | _ -> raise Types.tag_expectation_mismatch) fields StringMap.empty in + | _ -> raise Types.tag_expectation_mismatch) fields Label.Map.empty in Record (Row (fields, row_var, dual)) | Record row -> let fields, row_var, lr = (Types.unwrap_row row |> fst |> TypeUtils.extract_row_parts) in @@ -1968,27 +1989,27 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty end | Nil | Cons _ | List _ | Tuple _ | Variant _ | Negative _ | Operation _ -> assert false in let fields = - StringMap.fold + Label.Map.fold (fun name -> function | Present t -> let pats = List.map (unwrap_at name) pats in - StringMap.add name (Present (cpt pats t)) + Label.Map.add name (Present (cpt pats t)) | (Absent | Meta _) -> assert false - | _ -> raise Types.tag_expectation_mismatch) fields StringMap.empty in + | _ -> raise Types.tag_expectation_mismatch) fields Label.Map.empty in Record (Row (fields, row_var, false)) | Variant row -> let fields, row_var, lr = (Types.unwrap_row row |> fst |> TypeUtils.extract_row_parts) in assert (not lr); - let rec unwrap_at : string -> Pattern.with_pos -> Pattern.with_pos list = fun name p -> + let rec unwrap_at : Label.t -> Pattern.with_pos -> Pattern.with_pos list = fun name p -> let open Pattern in match p.node with | Variable _ | Any -> [ with_pos p.pos Pattern.Any ] | As (_, p) | HasType (p, _) -> unwrap_at name p - | Variant (name', None) when name=name' -> + | Variant (name', None) when Label.equal name name' -> [with_pos p.pos (Pattern.Record ([], None))] - | Variant (name', Some p) when name=name' -> [p] + | Variant (name', Some p) when Label.equal name name' -> [p] | Variant _ -> [] | Negative names when List.mem name names -> [] | Negative _ -> [ with_pos p.pos Pattern.Any ] @@ -2002,15 +2023,15 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty | {node = (Variant _); _} :: ps -> are_open ps | {node = (Nil | Cons _ | List _ | Tuple _ | Record _ | Constant _ | Operation _); _} :: _ -> assert false in let fields = - StringMap.fold + Label.Map.fold (fun name field_spec env -> match field_spec with | Present t -> let pats = concat_map (unwrap_at name) pats in let t = cpt pats t in - (StringMap.add name (Present t)) env + (Label.Map.add name (Present t)) env | (Absent | Meta _) -> assert false - | _ -> raise Types.tag_expectation_mismatch) fields StringMap.empty + | _ -> raise Types.tag_expectation_mismatch) fields Label.Map.empty in if are_open pats then begin @@ -2032,15 +2053,15 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty let fields, row_var, lr = (Types.unwrap_row row |> fst |> TypeUtils.extract_row_parts) in assert (not lr); - let unwrap_at : string -> Pattern.with_pos -> Pattern.with_pos list = fun name p -> + let unwrap_at : Label.t -> Pattern.with_pos -> Pattern.with_pos list = fun name p -> let open Pattern in match p.node with - | Operation (name', ps, _) when name=name' -> ps + | Operation (name', ps, _) when Label.equal name name' -> ps | Operation _ -> [] | Variable _ | Any | As _ | HasType _ | Negative _ | Nil | Cons _ | List _ | Tuple _ | Record _ | Variant _ | Constant _ -> assert false in let fields = - StringMap.fold + Label.Map.fold (fun name field_spec env -> match field_spec with | Present t -> @@ -2087,11 +2108,11 @@ let close_pattern_type : Pattern.with_pos list -> Types.datatype -> Types.dataty Types.make_function_type domain effs codomain in (* Bind name |-> Pre(t) *) - StringMap.add name (Present t) env + Label.Map.add name (Present t) env | _ -> - StringMap.add name (Present t) env + Label.Map.add name (Present t) env end - | t -> StringMap.add name t env) fields StringMap.empty + | t -> Label.Map.add name t env) fields Label.Map.empty in let row = Row (fields, row_var, false) in (* NOTE: type annotations can lead to a closed type even though @@ -2401,9 +2422,9 @@ let type_pattern ?(linear_vars=true) closed List.fold_right (fun name (positive, negative) -> let a = fresh_var () in - (StringMap.add name (Present a) positive, - StringMap.add name Absent negative)) - names (StringMap.empty, StringMap.empty) in + (Label.Map.add name (Present a) positive, + Label.Map.add name Absent negative)) + names (Label.Map.empty, Label.Map.empty) in let outer_type = Types.Variant (Row (positive, row_var, false)) in let inner_type = Types.Variant (Row (negative, row_var, false)) in @@ -2552,6 +2573,207 @@ let resolve_type_annotation : Binder.with_pos -> Sugartypes.datatype' option -> with sufficiently effect-polymorphic operations). *) +(** erase the erasable occurences of local labels from the types in the context *) +(** and remove the bindings with non erasable occurences of local labels *) + +(* remember which points are visited in order not to loop *) +class visit_points = object + val points : Types.datatype Unionfind.point list ref = ref [] + method visit x = points := x :: !points + method visited x = List.filter (Unionfind.equivalent x) !points <> [] +end + +let erase_local_labels_from_type ?(exact=true) pos labels dt = + let exception CannotErase in + let open Types in + let erased_points = new visit_points in + let rec e dt = + let e_arg (pk, t) = (pk, e t) in + let e_args = List.map e_arg in + let e_point p = + if erased_points#visited p then p + else begin + erased_points#visit p ; + let t = Unionfind.find p in + Unionfind.change p (e t) ; + p + end + in + match dt with + | Row (fields, rv, b) -> + let fields = Label.Map.fold (fun k v f -> + let keep () = Label.Map.add k (e v) f in + let remove () = f in + let to_remove k = + if exact then List.mem k labels + else List.filter (Label.textual_equal k) labels <> [] + in + let is_shadowed k = + if exact then List.filter (Label.textual_equal k) labels <> [] + else false + in + if Label.is_global k then keep () + else + if to_remove k then + match v with + | Absent | Present (Var _) -> remove () + | Meta p when (match Unionfind.find p with Var _ -> true | _ -> false) -> remove () + | _ -> raise CannotErase + else if is_shadowed k then + Gripers.die pos ("Label " ^ Label.show k ^ " is shadowed in this scope") + else + keep () + ) fields Label.Map.empty in + Row (fields, e_point rv, b) + | Recursive (id, k, t) -> Recursive (id, k, e t) + | Alias (pk, (name, ks, targs, b) , t) -> Alias (pk, (name, ks, e_args targs, b) , e t) + | Application (abs, targs) -> Application (abs, e_args targs) + | RecursiveApplication r -> RecursiveApplication { r with r_args = e_args r.r_args } + | Meta p -> Meta (e_point p) + | Function (t, t', t'') -> Function (e t, e t', e t'') + | Lolli (t, t', t'') -> Lolli (e t, e t', e t'') + | Record t -> Record (e t) + | Variant t -> Variant (e t) + | Table (temp, t, t', t'') -> Table (temp, e t, e t', e t'') + | ForAll (qs, t) -> ForAll (qs, e t) + | Effect t -> Effect (e t) + | Present t -> Present (e t) + | Input (t,t') -> Input (e t, e t') + | Output (t,t') -> Output (e t, e t') + | Select t -> Select (e t) + | Choice t -> Choice (e t) + | Dual t -> Dual (e t) + | _ -> dt + in + try Some (e dt) + with CannotErase -> None + +let erase_local_labels_from_tycon ?(exact=true) pos labels tycon = + match tycon with + | `Alias (pk, vars, dt) -> + begin match erase_local_labels_from_type ~exact pos labels dt with + | Some dt -> Some (`Alias (pk, vars, dt)) + | None -> None + end + | `Abstract abs -> Some (`Abstract abs) + | `Mutual (qs, tygroup) -> + let open Utility.StringMap in + let open Types in + tygroup := { !tygroup with + type_map = fold (fun k (qs,v) m -> + match erase_local_labels_from_type ~exact pos labels v with + | Some v -> add k (qs,v) m + | None -> m + ) !tygroup.type_map empty + } ; + Some (`Mutual (qs, tygroup)) + +(* let erase_local_labels labels decls ctx = *) +(* let erase_binder pos binder ctx = *) +(* let name = Binder.to_name binder in *) +(* let t' = Env.find_opt name ctx.var_env in *) +(* match OptionUtils.opt_bind (erase_local_labels_from_type pos labels) t' with *) +(* | Some t -> bind_var ctx (name, t) *) +(* | None -> unbind_var ctx name *) +(* in *) +(* let erase_alias pos name ctx = *) +(* let tycon' = Env.find_opt name ctx.tycon_env in *) +(* match OptionUtils.opt_bind (erase_local_labels_from_tycon pos labels) tycon' with *) +(* | Some tycon -> bind_alias ctx (name, tycon) *) +(* | None -> unbind_alias ctx name *) +(* in *) +(* let rec erase_pat pat ctx = *) +(* let e = erase_pat in *) +(* let e_list ps ctx = List.fold_left (fun ctx p -> e p ctx) ctx ps in *) +(* let e_opt p_opt ctx = match p_opt with None -> ctx | Some p -> e p ctx in *) +(* let open Pattern in *) +(* let pos = WithPos.pos pat in *) +(* match WithPos.node pat with *) +(* | Cons (p,p') -> ctx |> e p |> e p' *) +(* | List ps -> ctx |> e_list ps *) +(* | Variant (_, p_opt) -> ctx |> e_opt p_opt *) +(* | Operation (_, ps, p) -> ctx |> e_list ps |> e p *) +(* | Record (lps, p_opt) -> ctx |> e_list (snd (List.split lps)) |> e_opt p_opt *) +(* | Tuple ps -> ctx |> e_list ps *) +(* | Variable b -> ctx |> erase_binder pos b *) +(* | As (b, p) -> ctx |> erase_binder pos b |> e p *) +(* | HasType (p,_) -> ctx |> e p *) +(* | _ -> ctx *) +(* in *) +(* List.fold_left (fun ctx d -> *) +(* let pos = WithPos.pos d in *) +(* match WithPos.node d with *) +(* | Fun { fun_binder ; _ } -> erase_binder pos fun_binder ctx *) +(* | Funs rfuns -> List.fold_left *) +(* (fun ctx rfun -> *) +(* erase_binder (WithPos.pos rfun) (WithPos.node rfun).rec_binder ctx *) +(* ) ctx rfuns *) +(* | Val (pat, _, _, _) -> erase_pat pat ctx *) +(* | FreshLabel _ -> ctx *) +(* | Aliases ts -> List.fold_left (fun ctx { node=(name, _, _); _} -> erase_alias pos name ctx) ctx ts *) +(* | Infix _ *) +(* | Exp _ *) +(* | Foreign _ -> ctx *) +(* | Import _ *) +(* | Open _ *) +(* | Module _ *) +(* | AlienBlock _ -> assert false *) +(* ) ctx decls *) + +(** Check if all local labels in that type are bound and not shadowed **) +let check_labels pos dt ctx = + let checked_points = new visit_points in + let open Types in + let rec ct dt = + let ct_arg (_, t) = ct t in + let ct_args = List.iter ct_arg in + let ct_point p = + if not (checked_points#visited p) then begin + checked_points#visit p ; + ct (Unionfind.find p) + end + in + let ct_name name = + if not (Env.has name ctx.tycon_env) then raise (Errors.UnboundTyCon (pos, name)) + in + match dt with + | Row (fields, rv, _) -> + Label.Map.iter (fun k v -> + let ok () = () in + let unbound () = Gripers.die pos ("The local label " ^ Label.show k ^ " is not bound") in (* could happen since effectnames are inlined before typecheck *) + let shadowed () = Gripers.die pos ("Label " ^ Label.show k ^ " is shadowed in this scope") in + if Label.is_global k then ok () + else + match Label.Env.find_homonyms k ctx.label_env with + | [] -> unbound () + | k' :: _ when Label.equal k k' -> ok () + | _ -> ignore (shadowed ()) (* without the ignore we get a warning ?? *) + ; ct v + ) fields ; + ct_point rv + | Alias (_, (name, _, targs, _) , t) -> ct_name name ; ct_args targs ; ct t + | Application (_, targs) -> ct_args targs + | RecursiveApplication { r_args ; _ } -> ct_args r_args + | Meta p -> ct_point p + | Recursive (_, _, t) + | Record t + | Variant t + | ForAll (_, t) + | Effect t + | Present t + | Select t + | Choice t + | Dual t -> ct t + | Input (t,t') + | Output (t,t') -> ct t ; ct t' + | Function (t, t', t'') + | Lolli (t, t', t'') + | Table (_, t, t', t'') -> ct t ; ct t' ; ct t'' + | _ -> () + in + ct dt + + let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = fun context {node=expr; pos} -> let _UNKNOWN_POS_ = "" in @@ -2691,21 +2913,21 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = (* check that each label only occurs once *) List.fold_left (fun labels (name, _) -> - if StringSet.mem name labels then - Gripers.die pos ("Duplicate labels (" ^ name ^ ") in record.") + if Label.Set.mem name labels then + Gripers.die pos ("Duplicate labels (" ^ Label.show name ^ ") in record.") else - StringSet.add name labels) - StringSet.empty fields in + Label.Set.add name labels) + Label.Set.empty fields in let fields, field_env, absent_field_env, field_usages = List.fold_right (fun (label, e) (fields, field_env, absent_field_env, field_usages) -> let e = tc e in let t = typ e in ((label, e)::fields, - StringMap.add label (T.Present t) field_env, - StringMap.add label T.Absent absent_field_env, + Label.Map.add label (T.Present t) field_env, + Label.Map.add label T.Absent absent_field_env, Usage.combine field_usages (usages e))) - fields ([], StringMap.empty, StringMap.empty, Usage.empty) in + fields ([], Label.Map.empty, Label.Map.empty, Usage.empty) in begin match rest with | None -> let r = T.Row (field_env, Unionfind.fresh T.Closed, false) in @@ -2740,22 +2962,22 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = i.e. all the labels belonging to the record r *) let field_env' = - StringMap.fold (fun label f field_env' -> + Label.Map.fold (fun label f field_env' -> match f with | T.Absent -> - if StringMap.mem label field_env then + if Label.Map.mem label field_env then field_env' else - StringMap.add label T.Absent field_env' + Label.Map.add label T.Absent field_env' | T.Present t -> - if StringMap.mem label field_env then + if Label.Map.mem label field_env then failwith ("Could not extend record "^ expr_string (erase r)^" (of type "^ Types.string_of_datatype rtype^") with the label "^ - label^ + Label.show label^ " (of type"^Types.string_of_datatype (T.Record (T.Row (field_env, Unionfind.fresh T.Closed, false)))^ ") because the labels overlap") else - StringMap.add label (T.Present t) field_env' + Label.Map.add label (T.Present t) field_env' | T.Meta _ -> assert false | _ -> raise Types.tag_expectation_mismatch) rfield_env field_env in @@ -2851,14 +3073,14 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = | ConstructorLit (c, None, _) -> let type' = T.Variant (Types.make_singleton_open_row - (c, T.Present Types.unit_type) + (Label.make c, T.Present Types.unit_type) (lin_any, res_any)) in ConstructorLit (c, None, Some type'), type', Usage.empty | ConstructorLit (c, Some v, _) -> let v = tc v in let type' = T.Variant (Types.make_singleton_open_row - (c, T.Present (typ v)) + (Label.make c, T.Present (typ v)) (lin_any, res_any)) in ConstructorLit (c, Some (erase v), Some type'), type', usages v @@ -2926,6 +3148,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = relational_lenses_guard pos; let table = tc table in let columns = Lens_type_conv.sort_cols_of_table ~table:"" (typ table) in + let fds = List.map (fun (x,y) -> (List.map Label.name x, List.map Label.name y) ) fds in let typ = Lens.Type.type_lens_fun_dep ~fds ~columns |> Lens_errors.unpack_type_lens_result ~die:(Gripers.die pos) in @@ -2938,8 +3161,8 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let typ = let lens = typ lens |> Lens_type_conv.lens_type_of_type ~die:(Gripers.die pos) in let default = typ default |> Lens_type_conv.lens_phrase_type_of_type |> fun a -> [a] in - let drop = [drop] in - let key = Alias.Set.singleton key in + let drop = [Label.name drop] in + let key = Alias.Set.singleton (Label.name key) in Type.type_drop_lens lens ~default ~drop ~key |> Lens_errors.unpack_type_drop_lens_result ~die:(Gripers.die pos) in LensDropLit (erase lens, drop, key, erase default, Some typ), T.Lens typ, Usage.combine (usages lens) (usages default) @@ -3087,11 +3310,11 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let field_env = List.fold_right (fun name field_env -> - if StringMap.mem name field_env then + if Label.Map.mem name field_env then Gripers.die pos "Duplicate labels in insert expression." else - StringMap.add name (T.Present (Types.fresh_type_variable (lin_any, res_base))) field_env) - labels StringMap.empty + Label.Map.add name (T.Present (Types.fresh_type_variable (lin_any, res_base))) field_env) + labels Label.Map.empty in (* Check that the fields in the type of values match the declared labels *) @@ -3111,7 +3334,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = in let needed_env = - StringMap.map + Label.Map.map (fun _f -> Types.fresh_presence_variable (lin_any, res_base)) field_env in @@ -3144,7 +3367,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = the table. *) let row = - T.Row (StringMap.singleton id (T.Present Types.int_type), + T.Row (Label.Map.singleton (Label.make id) (T.Present Types.int_type), Types.fresh_row_variable (lin_any, res_base), false) in unify ~handle:Gripers.insert_id @@ -3211,14 +3434,14 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = List.fold_right (fun (name, exp) (set, field_env) -> let exp = type_check context' exp in - if StringMap.mem name field_env then + if Label.Map.mem name field_env then Gripers.die pos "Duplicate fields in update expression." else - (name, exp)::set, StringMap.add name (T.Present (typ exp)) field_env) - set ([], StringMap.empty) in + (name, exp)::set, Label.Map.add name (T.Present (typ exp)) field_env) + set ([], Label.Map.empty) in let needed_env = - StringMap.map + Label.Map.map (fun _f -> Types.fresh_presence_variable (lin_any, res_base)) field_env in @@ -3351,7 +3574,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = | Flat -> let shape = Types.make_list_type - (T.Record (T.Row (StringMap.empty, + (T.Record (T.Row (Label.Map.empty, Types.fresh_row_variable (lin_any, res_base), false))) in unify ~handle:Gripers.query_base_row (pos_and_typ p, no_pos shape) in @@ -3882,7 +4105,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = in assert (not lr); begin - match StringMap.lookup l field_env with + match Label.Map.lookup l field_env with | Some (T.Present t) -> (* the free type variables in the projected type *) let vars = Types.free_type_vars t in @@ -3940,7 +4163,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let rfields, row_var, lr = (TypeUtils.extract_row (typ r)) |> Types.unwrap_row |> fst |> TypeUtils.extract_row_parts in assert (not lr); let rfields = - StringMap.mapi + Label.Map.mapi (fun name t -> if List.mem_assoc name fields then T.Present (snd3 (List.assoc name fields)) @@ -4058,7 +4281,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = ((uexp_pos pat, effrow), no_pos (T.Effect inner_eff)); let pat, kpat = let rec find_effect_type eff = function - | (eff', t) :: _ when eff = eff' -> + | (eff', t) :: _ when Label.equal eff eff' -> begin match t with | T.Present t -> t | _ -> assert false @@ -4086,7 +4309,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let kname = Binder.to_name bndr in let kt = let (fields,_,_) = TypeUtils.extract_row_parts (TypeUtils.extract_row effrow) in - let kt = find_effect_type effname (StringMap.to_alist fields) in + let kt = find_effect_type effname (Label.Map.to_alist fields) in let op_param = TypeUtils.return_type kt in let typ = Env.find kname env in let domain = @@ -4186,8 +4409,8 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let make_operations_presence_polymorphic : Types.row -> Types.row = fun row -> let (operations, rho, dual) = TypeUtils.extract_row_parts row in - let operations' = - StringMap.mapi + let operations' = + Label.Map.mapi (fun name p -> if TypeUtils.is_builtin_effect name then p @@ -4244,7 +4467,7 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = sh_descr = descr }, body_type, usages | DoOperation (op, ps, _) -> let op = tc op in - let ps = List.map (tc) ps in + let ps = List.map tc ps in let doop, rettyp, usage, opt = match Types.concrete_type (typ op) with | T.ForAll (_, (T.Operation _)) as t -> @@ -4290,14 +4513,14 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let row = Types.make_singleton_open_row (opname, T.Present (typ op)) (lin_unl, res_effect) in let p = Position.resolve_expression pos in let () = - unify ~handle:Gripers.do_operation + unify ~handle:Gripers.operation (term, infer_opt) ; unify ~handle:Gripers.do_operation (no_pos (T.Effect context.effect_row), (p, T.Effect row)) in doop, rettyp, usage | Operation name -> - if String.compare name Value.session_exception_operation = 0 && not context.desugared then + if Label.equal name Value.session_exception_operation && not context.desugared then Gripers.die pos "The session failure effect SessionFail is not directly invocable (use `raise` instead)" else let t = match lookup_effect context name with @@ -4318,11 +4541,11 @@ let rec type_check : context -> phrase -> phrase * Types.datatype * Usage.t = let outer_effects = Types.row_with (Value.session_exception_operation, Types.fresh_presence_variable default_subkind) - (T.Row (StringMap.empty, rho, false)) in + (T.Row (Label.Map.empty, rho, false)) in let try_effects = Types.row_with (Value.session_exception_operation, T.Present (Types.make_operation_type [] Types.empty_type)) - (T.Row (StringMap.empty, rho, false)) in + (T.Row (Label.Map.empty, rho, false)) in unify ~handle:Gripers.try_effect (no_pos (T.Effect context.effect_row), no_pos (T.Effect outer_effects)); @@ -4451,6 +4674,7 @@ and type_binding : context -> binding -> binding * context * Usage.t = let bt = match datatype with | Some (_, Some t) -> + let _ = check_labels pos t context in unify pos ~handle:Gripers.bind_val_annotation (no_pos (typ body), no_pos t); t | _ -> typ body in @@ -4506,6 +4730,7 @@ and type_binding : context -> binding -> binding * context * Usage.t = | Some ft -> (* Debug.print ("t: " ^ Types.string_of_datatype ft); *) (* make sure the annotation has the right shape *) + let _ = check_labels pos ft context in let shape = make_ft lin pats effects return_type in let quantifiers, ft_mono = TypeUtils.split_quantified_type ft in @@ -4685,6 +4910,7 @@ and type_binding : context -> binding -> binding * context * Usage.t = make_ft_poly_curry lin pats (fresh_tame ()) (Types.fresh_type_variable (lin_any, res_any)) | Some t -> (* Debug.print ("t: " ^ Types.string_of_datatype t); *) + let _ = check_labels pos t context in let shape = make_ft lin pats (fresh_tame ()) (Types.fresh_type_variable (lin_any, res_any)) in let ft = match t with | T.ForAll _ -> t @@ -4876,6 +5102,7 @@ and type_binding : context -> binding -> binding * context * Usage.t = ignore (if String.contains (Binder.to_name binder) '\'' then raise (Errors.prime_alien pos)); (* Ensure that we quantify FTVs *) + let _ = check_labels pos datatype context in let (_tyvars, _args), datatype = Utils.generalise context.var_env datatype in let datatype = Instantiate.freshen_quantifiers datatype in let binder = Binder.set_type binder datatype in @@ -4886,10 +5113,12 @@ and type_binding : context -> binding -> binding * context * Usage.t = let env = List.fold_left (fun env {node=(name, vars, b); _} -> match b with | Typename (_, Some dt) -> + let _ = check_labels pos dt context in bind_alias env (name, `Alias (pk_type, List.map (SugarQuantifier.get_resolved_exn) vars, dt)) | Effectname (_, Some dt) -> + let _ = check_labels pos dt context in bind_alias env (name, `Alias (pk_row , List.map (SugarQuantifier.get_resolved_exn) vars, dt)) - | _ -> raise (internal_error "typeSugar.ml: unannotated type") + | _ -> raise (internal_error "unannotated type") ) empty_context ts in (Aliases ts, env, Usage.empty) | Infix def -> Infix def, empty_context, Usage.empty @@ -4898,12 +5127,27 @@ and type_binding : context -> binding -> binding * context * Usage.t = let () = unify pos ~handle:Gripers.bind_exp (pos_and_typ e, no_pos Types.unit_type) in Exp (erase e), empty_context, usages e + | FreshLabel ls -> + let context = { context with + var_env = Env.fold (fun k v env -> + match erase_local_labels_from_type ~exact:false pos ls v with + | Some v -> Env.bind k v env + | None -> env + ) context.var_env Env.empty ; + tycon_env = Env.fold (fun k v env -> + match erase_local_labels_from_tycon ~exact:false pos ls v with + | Some v -> Env.bind k v env + | None -> env + ) context.tycon_env Env.empty + } in + let context = bind_labels context ls in + (FreshLabel ls, context, Usage.empty) | Import _ | Open _ | AlienBlock _ | Module _ -> assert false in - WithPos.make ~pos typed, ctxt, usage + WithPos.make ~pos typed, ctxt, usage and type_regex typing_env : regex -> regex = fun m -> let erase (e, _, _) = e in @@ -5046,7 +5290,7 @@ and type_cp (context : context) = fun {node = p; pos} -> let c = Binder.to_name bndr in let (_, t, _) = type_check context (var c) in let s = Types.fresh_session_variable lin_any in - let r = Types.make_singleton_open_row (label, T.Present s) (lin_any, res_session) in + let r = Types.make_singleton_open_row (Label.make label, T.Present s) (lin_any, res_session) in let ctype = T.Select r in unify ~pos:pos ~handle:(Gripers.cp_select c) (t, ctype); @@ -5063,7 +5307,7 @@ and type_cp (context : context) = fun {node = p; pos} -> *) let check_branch (label, body) = let s = Types.fresh_type_variable (lin_any, res_session) in - let r = Types.make_singleton_open_row (label, T.Present s) (lin_any, res_session) in + let r = Types.make_singleton_open_row (Label.make label, T.Present s) (lin_any, res_session) in unify ~pos:pos ~handle:(Gripers.cp_offer_choice c) (t, T.Choice r); let (p, t, u) = with_channel c s (type_cp (bind_var context (c, s)) body) in (label, p), t, u diff --git a/core/typeUtils.ml b/core/typeUtils.ml index 91a31477d..633b8fd43 100644 --- a/core/typeUtils.ml +++ b/core/typeUtils.ml @@ -15,22 +15,22 @@ let extract_row_parts = Types.extract_row_parts let split_row name row = let (field_env, row_var, dual) = fst (unwrap_row row) |> extract_row_parts in let t = - if StringMap.mem name field_env then - match (StringMap.find name field_env) with + if Label.Map.mem name field_env then + match (Label.Map.find name field_env) with | Present t -> t | Absent -> - error ("Attempt to split row "^string_of_row row ^" on absent field " ^ name) + error ("Attempt to split row "^string_of_row row ^" on absent field " ^ Label.show name) | Meta _ -> - error ("Attempt to split row "^string_of_row row ^" on meta field " ^ name) + error ("Attempt to split row "^string_of_row row ^" on meta field " ^ Label.show name) | _ -> raise Types.tag_expectation_mismatch else - error ("Attempt to split row "^string_of_row row ^" on absent field " ^ name) + error ("Attempt to split row "^string_of_row row ^" on absent field " ^ Label.show name) in let new_field_env = if is_closed_row row then - StringMap.remove name field_env + Label.Map.remove name field_env else - StringMap.add name Absent field_env + Label.Map.add name Absent field_env in t, Row (new_field_env, row_var, dual) @@ -49,20 +49,20 @@ let rec split_variant_type name t = match concrete_type t with | t -> error ("Attempt to split non-variant type "^string_of_datatype t) -let rec project_type ?(overstep_quantifiers=true) name t = match (concrete_type t, overstep_quantifiers) with - | (ForAll (_, t), true) -> project_type name t +let rec project_type ?(overstep_quantifiers=true) label t = match (concrete_type t, overstep_quantifiers) with + | (ForAll (_, t), true) -> project_type label t | (Record row, _) -> - let t, _ = split_row name row in + let t, _ = split_row label row in t | (Application (absty, [PrimaryKind.Type, typ]), _) when (Abstype.name absty) = "TransactionTime" || (Abstype.name absty = "ValidTime") -> - if name = TemporalField.data_field then typ + if Label.name_is label TemporalField.data_field then typ else if - name = TemporalField.from_field || - name = TemporalField.to_field then + Label.name_is label TemporalField.from_field || + Label.name_is label TemporalField.to_field then Primitive (Primitive.DateTime) else - error ("Trying to project " ^ name ^ " from temporal metadata: " ^ string_of_datatype t) + error ("Trying to project " ^ Label.show label ^ " from temporal metadata: " ^ string_of_datatype t) | (t, _) -> error ("Attempt to project non-record type "^string_of_datatype t) @@ -100,22 +100,22 @@ let rec erase_type ?(overstep_quantifiers=true) names t = let closed = is_closed_row row in let (field_env, row_var, duality) = fst (unwrap_row row) |> extract_row_parts in let field_env = - StringSet.fold + Label.Set.fold (fun name field_env -> - match StringMap.lookup name field_env with + match Label.Map.lookup name field_env with | Some (Present _) -> if closed then - StringMap.remove name field_env + Label.Map.remove name field_env else - StringMap.add name Absent field_env + Label.Map.add name Absent field_env | Some Absent -> - error ("Attempt to remove absent field "^name^" from row "^string_of_row row) + error ("Attempt to remove absent field "^Label.show name^" from row "^string_of_row row) | Some (Meta _) -> - error ("Attempt to remove meta field "^name^" from row "^string_of_row row) + error ("Attempt to remove meta field "^Label.show name^" from row "^string_of_row row) | Some _ -> raise Types.tag_expectation_mismatch | None -> - error ("Attempt to remove absent field "^name^" from row "^string_of_row row)) + error ("Attempt to remove absent field "^Label.show name^" from row "^string_of_row row)) names field_env in @@ -152,9 +152,9 @@ let rec effect_row ?(overstep_quantifiers=true) t = match (concrete_type t, over error ("Attempt to take effects of non-function: " ^ string_of_datatype t) -let iter_row (iter_func : string -> field_spec -> unit) row = +let iter_row (iter_func : Label.t -> field_spec -> unit) row = let (field_spec_map, _, _) = fst (unwrap_row row) |> extract_row_parts in - Utility.StringMap.iter iter_func field_spec_map + Label.Map.iter iter_func field_spec_map let is_function_type t = match concrete_type t with | Lolli (_, _, _) @@ -212,13 +212,13 @@ let record_without t names = match concrete_type t with | Record (Row (fields, row_var, dual) as row) -> if is_closed_row row then - let fieldm = StringSet.fold (fun name fields -> StringMap.remove name fields) names fields in + let fieldm = Label.Set.fold (fun name fields -> Label.Map.remove name fields) names fields in Record (Row (fieldm, row_var, dual)) else let fieldm = - StringMap.mapi + Label.Map.mapi (fun name f -> - if StringSet.mem name names then + if Label.Set.mem name names then Absent else f) @@ -370,7 +370,7 @@ let check_type_wellformedness primary_kind t : unit = (* Row *) | Row (field_spec_map, row_var, _dual) -> let handle_fs _label f = ifield_spec f in - StringMap.iter handle_fs field_spec_map; + Label.Map.iter handle_fs field_spec_map; meta rec_env row_var (* Session *) | Input (t, s) @@ -394,7 +394,7 @@ let row_present_types t = extract_row t |> extract_row_parts |> fst3 - |> StringMap.filter_map + |> Label.Map.filter_map (fun _ v -> match v with | Present t -> Some t diff --git a/core/typeUtils.mli b/core/typeUtils.mli index 1191b0220..bfa4298dc 100644 --- a/core/typeUtils.mli +++ b/core/typeUtils.mli @@ -5,15 +5,15 @@ exception TypeDestructionError of string val concrete_type : Types.datatype -> Types.datatype -val project_type : ?overstep_quantifiers:bool -> string -> Types.datatype -> Types.datatype -val erase_type : ?overstep_quantifiers:bool -> Utility.stringset -> Types.datatype -> Types.datatype -val inject_type : string -> Types.datatype -> Types.datatype +val project_type : ?overstep_quantifiers:bool -> Label.t -> Types.datatype -> Types.datatype +val erase_type : ?overstep_quantifiers:bool -> Label.Set.t -> Types.datatype -> Types.datatype +val inject_type : Label.t -> Types.datatype -> Types.datatype val return_type : ?overstep_quantifiers:bool -> Types.datatype -> Types.datatype val arg_types : ?overstep_quantifiers:bool -> Types.datatype -> Types.datatype list val effect_row : ?overstep_quantifiers:bool -> Types.datatype -> Types.row val is_function_type : Types.datatype -> bool val is_thunk_type : Types.datatype -> bool -val is_builtin_effect : string -> bool +val is_builtin_effect : Label.t -> bool val element_type : ?overstep_quantifiers:bool -> Types.datatype -> Types.datatype val table_read_type : Types.datatype -> Types.datatype @@ -25,26 +25,26 @@ val app_type : Types.datatype -> Types.datatype -> Types.datatype val extract_row : Types.datatype -> Types.row val extract_row_parts : Types.datatype -> Types.row' -val iter_row : (string -> Types.field_spec -> unit) -> Types.row -> unit -val split_row : string -> Types.row -> (Types.datatype * Types.row) -val split_variant_type : string -> Types.datatype -> (Types.datatype * Types.datatype) -val variant_at : ?overstep_quantifiers:bool -> string -> Types.datatype -> Types.datatype +val iter_row : (Label.t -> Types.field_spec -> unit) -> Types.row -> unit +val split_row : Label.t -> Types.row -> (Types.datatype * Types.row) +val split_variant_type : Label.t -> Types.datatype -> (Types.datatype * Types.datatype) +val variant_at : ?overstep_quantifiers:bool -> Label.t -> Types.datatype -> Types.datatype val quantifiers : Types.datatype -> Quantifier.t list val split_quantified_type : Types.datatype -> (Quantifier.t list * Types.datatype) -val record_without : Types.datatype -> Utility.StringSet.t -> Types.datatype +val record_without : Types.datatype -> Label.Set.t -> Types.datatype (* Session stuff *) (* val session_of_type : Types.datatype -> Types.session_type *) -val select_type : string -> Types.datatype -> Types.datatype -val split_choice_type : string -> Types.datatype -> (Types.datatype * Types.datatype) -val choice_at : string -> Types.datatype -> Types.datatype +val select_type : Label.t -> Types.datatype -> Types.datatype +val split_choice_type : Label.t -> Types.datatype -> (Types.datatype * Types.datatype) +val choice_at : Label.t -> Types.datatype -> Types.datatype val primary_kind_of_type : Types.datatype -> PrimaryKind.t val check_type_wellformedness : PrimaryKind.t option -> Types.datatype -> unit -val row_present_types : Types.datatype -> Types.datatype Utility.StringMap.t +val row_present_types : Types.datatype -> Types.datatype Label.Map.t val pack_types : Types.datatype list -> Types.datatype diff --git a/core/types.ml b/core/types.ml index 5011f2324..db16eb657 100644 --- a/core/types.ml +++ b/core/types.ml @@ -9,9 +9,10 @@ let internal_error message = let tag_expectation_mismatch = internal_error "Type tag expectation mismatch" -module FieldEnv = Utility.StringMap +module FieldEnv = Label.Map +type 'a field_env = 'a FieldEnv.t [@@deriving show] + type 'a stringmap = 'a Utility.stringmap [@@deriving show] -type 'a field_env = 'a stringmap [@@deriving show] (* type var sets *) module TypeVarSet = struct @@ -172,7 +173,7 @@ and session_type = typ and datatype = typ and type_arg = PrimaryKind.t * typ and field_spec = typ -and field_spec_map = field_spec Utility.StringMap.t +and field_spec_map = field_spec Label.Map.t and meta_type_var = typ point and meta_row_var = row point and meta_presence_var = typ point @@ -292,11 +293,11 @@ struct method field_spec_map : field_spec_map -> ('self_type * field_spec_map) = fun fsmap -> - StringMap.fold + Label.Map.fold (fun lbl fs (o, fsmap') -> let (o, fs) = o#field_spec fs in - (o, StringMap.add lbl fs fsmap')) - fsmap (o, StringMap.empty) + (o, Label.Map.add lbl fs fsmap')) + fsmap (o, Label.Map.empty) method quantifier : Quantifier.t -> ('self_type * Quantifier.t) = fun q -> (o, q) @@ -1008,7 +1009,7 @@ module Env = Env.String let open PrimaryKind in match pk with | Type -> (Type, make_rigid_type_variable var sk) - | Row -> (Row, Row (StringMap.empty, make_rigid_row_variable var sk, false)) + | Row -> (Row, Row (Label.Map.empty, make_rigid_row_variable var sk, false)) | Presence -> (Presence, make_rigid_presence_variable var sk) let is_closed_row : row -> bool = @@ -1102,7 +1103,7 @@ let is_absent_from_row label row (* (field_env, _, _ as row) *) = then FieldEnv.find label field_env = Absent else is_closed_row row -let row_with (label, f : string * field_spec) = function +let row_with (label, f : Label.t * field_spec) = function | Row (field_env, row_var, dual) -> Row (FieldEnv.add label f field_env, row_var, dual) | _ -> raise tag_expectation_mismatch @@ -1344,7 +1345,7 @@ and dual_row : var_map -> row -> row = match fst (unwrap_row row) with | Row (fields, row_var, dual) -> let fields' = - StringMap.map + Label.Map.map (function | Absent -> Absent | Present t -> @@ -1419,7 +1420,7 @@ and subst_dual_row : var_map -> row -> row = match fst (unwrap_row row) with | Row (fields, row_var, dual) -> let fields' = - StringMap.map + Label.Map.map (subst_dual_field_spec rec_points) fields in @@ -1445,7 +1446,7 @@ and flatten_row : row -> row = fun row -> match row with | Row _ -> row (* HACK: this probably shouldn't happen! *) - | Meta row_var -> Row (StringMap.empty, row_var, false) + | Meta row_var -> Row (Label.Map.empty, row_var, false) | _ -> raise (internal_error "attempt to flatten, row expected") in let dual_if = @@ -1669,7 +1670,7 @@ let quantifier_of_type_arg = function | Type, Meta point -> quantifier_of_point point | Row, Row (fields, point, _dual) -> - assert (StringMap.is_empty fields); + assert (Label.Map.is_empty fields); quantifier_of_point point | Presence, Meta point -> quantifier_of_point point (* HACK: this probably shouldn't happen *) @@ -1694,13 +1695,13 @@ let xml_type = Alias (pk_type, ("Xml", [], [], false), Application (list, [ let database_type = Primitive Primitive.DB (* Empty type, used for exceptions *) let empty_type = Variant (make_empty_closed_row ()) -let wild = "wild" -let hear = "hear" +let wild = Label.make "wild" +let hear = Label.make "hear" let wild_present = (wild, Present unit_type) let hear_present t = (hear, Present t) let is_builtin_effect lbl = - lbl = wild || lbl = hear + Label.equal lbl wild || Label.equal lbl hear (* precondition: the row is unwrapped *) @@ -1713,14 +1714,14 @@ let is_tuple ?(allow_onetuples=false) row = in match Unionfind.find row_var with | Closed -> - let n = StringMap.size field_env in + let n = Label.Map.size field_env in let b = n = 0 || (List.for_all (fun i -> - let name = string_of_int i in + let name = Label.of_int i in FieldEnv.mem name field_env - && (match FieldEnv.find (string_of_int i) field_env with + && (match FieldEnv.find name field_env with | Present _ -> true | Absent -> false | Meta _ -> false @@ -2431,7 +2432,7 @@ struct FieldEnv.fold (fun i f tuple_env -> match f with - | Present t -> IntMap.add (int_of_string i) t tuple_env + | Present t -> IntMap.add (Label.to_int i) t tuple_env | (Absent | Meta _) -> assert false | _ -> raise tag_expectation_mismatch) field_env @@ -2540,7 +2541,7 @@ struct | Row (fields, _, _) -> fields | _ -> raise tag_expectation_mismatch in - if StringMap.is_empty fields then + if Label.Map.is_empty fields then ts else let r = row ~name:(fun _ _ -> name_of_eff_var ~allows_shared:true) "," context p r' in @@ -2695,7 +2696,7 @@ struct if strip_wild && label = wild then field_strings else - (label ^ presence context p f) :: field_strings) + (Label.show label ^ presence context p f) :: field_strings) field_env [] in let row_var_string = row_var name sep context p rv in @@ -2708,7 +2709,7 @@ struct (* FIXME: this shouldn't happen *) | Meta rv -> Debug.print ("Row variable where row expected:"^show_datatype (Meta rv)); - row sep context ~name:name ~strip_wild:strip_wild p (Row (StringMap.empty, rv, false)) + row sep context ~name:name ~strip_wild:strip_wild p (Row (Label.Map.empty, rv, false)) | t -> failwith ("Illformed row:"^show_datatype t) (* raise tag_expectation_mismatch *) @@ -3007,10 +3008,10 @@ module RoundtripPrinter : PRETTY_PRINTER = struct o#var module OperationMap = Utility.Map.Make(struct - type t = tid * string [@@deriving show] + type t = tid * Label.t [@@deriving show] let compare (xi,xs) (yi,ys) = if xi = yi - then String.compare xs ys + then Label.compare xs ys else Int.compare xi yi end) type op_entry = tid list @@ -3031,7 +3032,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct method get_operations = OperationMap.map (fun vars -> ListUtils.collect_duplicates (=) vars) operations - method with_nonpoly_operation : tid -> string -> 'self_type + method with_nonpoly_operation : tid -> Label.t -> 'self_type = let upd = function | None -> Some [] @@ -3041,7 +3042,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct let operations = OperationMap.update (effect_vid, label) upd operations in {< operations >} - method with_poly_operation : tid -> string -> tid -> 'self_type + method with_poly_operation : tid -> Label.t -> tid -> 'self_type = let upd vid = function | None -> Some [vid] @@ -3131,7 +3132,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct if d = unit_type then c else tp | tp -> tp in - let decide_field : tid -> string -> field_spec -> 'self_type * field_spec_map -> 'self_type * field_spec_map + let decide_field : tid -> Label.t -> field_spec -> 'self_type * field_spec_map -> 'self_type * field_spec_map (* Here we need to filter out the fields that are polymorphic in their presence with a fresh variable. @@ -3629,7 +3630,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct else if Context.is_ambient_tuple ctx then with_value presence pre :: printers else (Printer (fun ctx () buf -> - StringBuffer.write buf lbl; + StringBuffer.write buf (Label.show lbl); let pre = match pre with | Meta point -> Unionfind.find point | _ -> pre @@ -4225,6 +4226,7 @@ type tycon_environment = tycon_spec Env.t type typing_environment = { var_env : environment ; rec_vars : StringSet.t ; tycon_env : tycon_environment ; + label_env : Label.Env.t; effect_row : row; desugared : bool } [@@deriving show] @@ -4232,6 +4234,7 @@ type typing_environment = { var_env : environment ; let empty_typing_environment = { var_env = Env.empty; rec_vars = StringSet.empty; tycon_env = Env.empty; + label_env = Label.Env.empty; effect_row = make_empty_closed_row (); desugared = false } @@ -4358,11 +4361,12 @@ let normalise_typing_environment env = (* Functions on environments *) let extend_typing_environment - {var_env = l; rec_vars = lvars; tycon_env = al; effect_row = _; desugared = _; } - {var_env = r; rec_vars = rvars; tycon_env = ar; effect_row = er; desugared = dr } : typing_environment = + {var_env = l; rec_vars = lvars; tycon_env = al; label_env = ll; effect_row = _; desugared = _; } + {var_env = r; rec_vars = rvars; tycon_env = ar; label_env = lr; effect_row = er; desugared = dr } : typing_environment = { var_env = Env.extend l r ; rec_vars = StringSet.union lvars rvars ; tycon_env = Env.extend al ar + ; label_env = Label.Env.extend ll lr ; effect_row = er ; desugared = dr } @@ -4421,10 +4425,10 @@ let make_fresh_envs : datatype -> datatype IntMap.t * row IntMap.t * field_spec | Closed -> empties | Var (var, kind, `Flexible) -> let tenv, renv, penv = empties in - (tenv, M.add var (Row (StringMap.empty, fresh_row_variable (Kind.subkind kind), false)) renv, penv) + (tenv, M.add var (Row (Label.Map.empty, fresh_row_variable (Kind.subkind kind), false)) renv, penv) | Var (var, kind, `Rigid) -> let tenv, renv, penv = empties in - (tenv, M.add var (Row (StringMap.empty, fresh_rigid_row_variable (Kind.subkind kind), false)) renv, penv) + (tenv, M.add var (Row (Label.Map.empty, fresh_rigid_row_variable (Kind.subkind kind), false)) renv, penv) | Recursive (l, _, _) when S.mem l boundvars -> empties | Recursive (l, _, row) -> make_env (S.add l boundvars) row | row -> make_env boundvars row @@ -4449,13 +4453,13 @@ let make_fresh_envs : datatype -> datatype IntMap.t * row IntMap.t * field_spec let make_rigid_envs datatype : datatype IntMap.t * row IntMap.t * field_spec Utility.IntMap.t = let tenv, renv, penv = make_fresh_envs datatype in (IntMap.map (fun _ -> fresh_rigid_type_variable (lin_any, res_any)) tenv, - IntMap.map (fun _ -> Row (StringMap.empty, fresh_rigid_row_variable (lin_any, res_any), false)) renv, + IntMap.map (fun _ -> Row (Label.Map.empty, fresh_rigid_row_variable (lin_any, res_any), false)) renv, IntMap.map (fun _ -> fresh_rigid_presence_variable (lin_any, res_any)) penv) let make_wobbly_envs datatype : datatype IntMap.t * row IntMap.t * field_spec Utility.IntMap.t = let tenv, renv, penv = make_fresh_envs datatype in (IntMap.map (fun _ -> fresh_type_variable (lin_any, res_any)) tenv, - IntMap.map (fun _ -> Row (StringMap.empty, fresh_row_variable (lin_any, res_any), false)) renv, + IntMap.map (fun _ -> Row (Label.Map.empty, fresh_row_variable (lin_any, res_any), false)) renv, IntMap.map (fun _ -> fresh_presence_variable (lin_any, res_any)) penv) let combine_per_kind_envs : datatype IntMap.t * row IntMap.t * field_spec IntMap.t -> type_arg IntMap.t = @@ -4612,7 +4616,7 @@ let make_tuple_type (ts : datatype list) : datatype = Record (snd (List.fold_left - (fun (n, row) t -> n+1, row_with (string_of_int n, Present t) row) + (fun (n, row) t -> n+1, row_with (Label.of_int n, Present t) row) (1, make_empty_closed_row ()) ts)) @@ -4663,8 +4667,8 @@ let remove_field : ?idempotent:bool -> Label.t -> row -> row = fun ?(idempotent=true) lbl row -> match row with | Row (fieldenv, var, dual) -> - if idempotent || StringMap.mem lbl fieldenv - then Row (StringMap.remove lbl fieldenv, var, dual) + if idempotent || Label.Map.mem lbl fieldenv + then Row (Label.Map.remove lbl fieldenv, var, dual) else raise (internal_error "attempt to remove non-existent field") | _ -> raise tag_expectation_mismatch diff --git a/core/types.mli b/core/types.mli index e308a6d5a..d3b4ce9e9 100644 --- a/core/types.mli +++ b/core/types.mli @@ -2,8 +2,10 @@ open CommonTypes (* field environments *) +module FieldEnv : Label.LABELMAP +type 'a field_env = 'a Label.Map.t [@@deriving show] + type 'a stringmap = 'a Utility.StringMap.t [@@deriving show] -type 'a field_env = 'a stringmap [@@deriving show] (* type var sets *) module TypeVarSet : sig @@ -163,7 +165,7 @@ and session_type = typ and datatype = typ and type_arg = PrimaryKind.t * typ and field_spec = typ -and field_spec_map = field_spec Utility.StringMap.t +and field_spec_map = field_spec Label.Map.t and meta_type_var = typ point and meta_row_var = row point and meta_presence_var = typ point @@ -171,7 +173,6 @@ and row = typ and row' = field_spec_map * row_var * bool and row_var = meta_row_var - val is_type_body : typ -> bool val is_row_body : row -> bool val is_field_spec_body : field_spec -> bool @@ -220,8 +221,9 @@ type tycon_environment = tycon_spec Env.String.t type typing_environment = { var_env : environment ; rec_vars : Utility.StringSet.t ; tycon_env : tycon_environment ; + label_env : Label.Env.t; effect_row : row ; - desugared : bool } + desugared : bool } val empty_typing_environment : typing_environment @@ -250,7 +252,7 @@ val wild : Label.t val hear : Label.t val wild_present : Label.t * datatype val hear_present : datatype -> (Label.t * datatype) -val is_builtin_effect : string -> bool +val is_builtin_effect : Label.t -> bool (** get type variables *) val free_type_vars : datatype -> TypeVarSet.t @@ -303,12 +305,12 @@ val make_empty_closed_row : unit -> row val make_empty_open_row : Subkind.t -> row (** singleton row constructors *) -val make_singleton_closed_row : (string * field_spec) -> row -val make_singleton_open_row : (string * field_spec) -> Subkind.t -> row +val make_singleton_closed_row : (Label.t * field_spec) -> row +val make_singleton_open_row : (Label.t * field_spec) -> Subkind.t -> row (** row predicates *) val is_closed_row : row -> bool -val is_absent_from_row : string -> row -> bool +val is_absent_from_row : Label.t -> row -> bool val is_tuple : ?allow_onetuples:bool -> row -> bool @@ -317,7 +319,7 @@ val get_row_var : row -> int option (** building rows *) val make_closed_row : datatype field_env -> row -val row_with : (string * field_spec) -> row -> row +val row_with : (Label.t * field_spec) -> row -> row val extend_row : datatype field_env -> row -> row val extend_row_safe : datatype field_env -> row -> row option val open_row : Subkind.t -> row -> row diff --git a/core/typevarcheck.ml b/core/typevarcheck.ml index cc4b35e54..263c453e6 100644 --- a/core/typevarcheck.ml +++ b/core/typevarcheck.ml @@ -1,7 +1,7 @@ open Utility open Types -module FieldEnv = Utility.StringMap +module FieldEnv = Label.Map (* TODO @@ -66,11 +66,11 @@ let rec is_guarded : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool = match row with | Row (fields, row_var, _dual) when - (FieldEnv.mem "1" fields && + (FieldEnv.mem Label.one fields && FieldEnv.size fields = 1 && Unionfind.find row_var = Closed) -> begin - match FieldEnv.find "1" fields with + match FieldEnv.find Label.one fields with | Present t -> isg t | (Absent | Var _) -> true | _ -> raise Types.tag_expectation_mismatch @@ -93,7 +93,7 @@ let rec is_guarded : TypeVarSet.t -> StringSet.t -> int -> datatype -> bool = | Row (fields, row_var, _dual) -> let check_fields = false in (if check_fields then - (StringMap.fold + (Label.Map.fold (fun _ f b -> b && isg f) fields true) diff --git a/core/unify.ml b/core/unify.ml index c92c59848..4f9973a84 100644 --- a/core/unify.ml +++ b/core/unify.ml @@ -223,7 +223,7 @@ and eq_presence = fun (l, r) -> eq_types (l, r) and eq_field_envs (lfield_env, rfield_env) = let eq_specs lf rf = eq_presence (lf, rf) in - StringMap.equal eq_specs lfield_env rfield_env + Label.Map.equal eq_specs lfield_env rfield_env and eq_row_vars (lpoint, rpoint) = (* QUESTION: Do we need to deal with closed rows specially? @@ -797,7 +797,7 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = let is_unguarded_recursive row = let rec is_unguarded rec_rows (field_env, row_var, _) = - StringMap.is_empty field_env && + Label.Map.is_empty field_env && (match Unionfind.find row_var with | Closed | Var _ -> false @@ -807,8 +807,8 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = | _ -> assert false) in is_unguarded IntSet.empty row in - let domain_of_env : field_spec_map -> StringSet.t = - fun env -> StringMap.fold (fun label _ labels -> StringSet.add label labels) env StringSet.empty in + let domain_of_env : field_spec_map -> Label.Set.t = + fun env -> Label.Map.fold (fun label _ labels -> Label.Set.add label labels) env Label.Set.empty in (* unify_field_envs closed rec_env (lenv, renv) @@ -827,22 +827,22 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = let ldom = domain_of_env lenv in let rdom = domain_of_env renv in - let shared_dom = StringSet.inter ldom rdom in + let shared_dom = Label.Set.inter ldom rdom in (* rigid row unifcation cannot tolerate extra fields unless both rows are closed and all fields can be made absent *) if rigid then - let lextras = StringSet.diff ldom rdom in - let rextras = StringSet.diff rdom ldom in + let lextras = Label.Set.diff ldom rdom in + let rextras = Label.Set.diff rdom ldom in - if not (StringSet.is_empty lextras) || not (StringSet.is_empty rextras) then + if not (Label.Set.is_empty lextras) || not (Label.Set.is_empty rextras) then (* some fields don't match *) if closed then (* closed rows don't need to explicitly mention absent *) let kill_extras extras env = - StringSet.iter + Label.Set.iter (fun label -> - match StringMap.find label env with + match Label.Map.find label env with | (Absent | Meta _) as f -> unify_presence' rec_env (f, Absent) | _ -> @@ -865,10 +865,10 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = semantics wrong *) (* unify fields in shared domain *) - StringSet.iter + Label.Set.iter (fun label -> - let lf = StringMap.find label lenv in - let rf = StringMap.find label renv in + let lf = Label.Map.find label lenv in + let rf = Label.Map.find label renv in unify_presence' rec_env (lf, rf)) shared_dom in @@ -940,7 +940,7 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = raise (Failure (`Msg ("Rigid row variable cannot be unified with non-empty row\n" ^string_of_row (Row extension_row)))) | Var (var, ((_, (lin, rest)) as kind), `Flexible) -> - if not (StringMap.is_empty extension_field_env) && + if not (Label.Map.is_empty extension_field_env) && TypeVarSet.mem var (free_row_type_vars (Row extension_row)) then begin if Restriction.is_base rest then @@ -969,9 +969,9 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = in raise (Failure (`Msg message)) end; - if StringMap.is_empty extension_field_env then + if Label.Map.is_empty extension_field_env then if dual then - Unionfind.change point (Row (StringMap.empty, extension_row_var, true)) + Unionfind.change point (Row (Label.Map.empty, extension_row_var, true)) else Unionfind.union point extension_row_var else @@ -981,7 +981,7 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = Unionfind.change point (Row extension_row) end | Recursive _ -> - unify_rows' rec_env ((StringMap.empty, point, dual), extension_row) + unify_rows' rec_env ((Label.Map.empty, point, dual), extension_row) | row -> unify_rows' rec_env (TypeUtils.extract_row_parts (if dual then dual_row row else row), extension_row) in extend row_var in @@ -992,19 +992,19 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = precondition: big_field_env contains small_field_env *) - let matching_labels : field_spec_map * field_spec_map -> StringSet.t = + let matching_labels : field_spec_map * field_spec_map -> Label.Set.t = fun (big_field_env, small_field_env) -> - StringMap.fold (fun label _ labels -> - if StringMap.mem label small_field_env then - StringSet.add label labels + Label.Map.fold (fun label _ labels -> + if Label.Map.mem label small_field_env then + Label.Set.add label labels else - labels) big_field_env StringSet.empty in + labels) big_field_env Label.Set.empty in - let row_without_labels : StringSet.t -> row' -> row' = + let row_without_labels : Label.Set.t -> row' -> row' = fun labels (field_env, row_var, dual) -> let restricted_field_env = - StringSet.fold (fun label field_env -> - StringMap.remove label field_env) labels field_env in + Label.Set.fold (fun label field_env -> + Label.Map.remove label field_env) labels field_env in (restricted_field_env, row_var, dual) in (* @@ -1027,7 +1027,7 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = if IntMap.mem var rec_rows then IntMap.find var rec_rows else - [Row (StringMap.empty, row_var, false)] in + [Row (Label.Map.empty, row_var, false)] in if List.exists (fun r -> eq_rows (r, Row restricted_row)) rs then None else @@ -1105,9 +1105,9 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = let (flexible_field_env', flexible_row_var', flexible_dual) as flexible_row' = TypeUtils.extract_row_parts flexible_row' in (* let (flexible_field_env', flexible_row_var', flexible_dual) as flexible_row', flexible_rec_row = unwrap_row flexible_row in *) (* check that the flexible row contains no extra fields *) - StringMap.iter + Label.Map.iter (fun label f -> - if (StringMap.mem label rigid_field_env') then + if (Label.Map.mem label rigid_field_env') then () else match f with @@ -1121,7 +1121,7 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = ^"\nand\n "^ string_of_row (Row flexible_row) ^"\n could not be unified because the former is rigid" ^" and the latter contains fields not present in the former, namely `" - ^ label ^"'."))) + ^ Label.show label ^"'."))) ) flexible_field_env'; let rec_env' = @@ -1133,7 +1133,7 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = | None -> () | Some rec_env -> unify_field_envs ~closed:false ~rigid:false rec_env (rigid_field_env', flexible_field_env'); - let flexible_extension = StringMap.filter (fun label _ -> not (StringMap.mem label flexible_field_env')) rigid_field_env' in + let flexible_extension = Label.Map.filter (fun label _ -> not (Label.Map.mem label flexible_field_env')) rigid_field_env' in unify_row_var_with_row rec_env (flexible_row_var', flexible_dual, (flexible_extension, rigid_row_var', rigid_dual')) in let unify_both_flexible ((lfield_env, _, ldual as lrow), (rfield_env, _, rdual as rrow)) = @@ -1165,11 +1165,11 @@ and unify_rows' : ?var_sk:Subkind.t -> unify_env -> ((row' * row') -> unit) = let fresh_row_var = fresh_row_variable var_sk in (* each row can contain fields missing from the other *) - let rextension = StringMap.filter (fun label _ -> not (StringMap.mem label rfield_env')) lfield_env' in + let rextension = Label.Map.filter (fun label _ -> not (Label.Map.mem label rfield_env')) lfield_env' in (* Debug.print ("rext: "^string_of_row (Row (rextension, fresh_row_var, false))); *) unify_row_var_with_row rec_env (rrow_var', rdual', (rextension, fresh_row_var, false)); - let lextension = StringMap.filter (fun label _ -> not (StringMap.mem label lfield_env')) rfield_env' in + let lextension = Label.Map.filter (fun label _ -> not (Label.Map.mem label lfield_env')) rfield_env' in unify_row_var_with_row rec_env (lrow_var', ldual', (lextension, fresh_row_var, false)) end in diff --git a/core/utility.ml b/core/utility.ml index 2ef7870ef..707bfbfde 100644 --- a/core/utility.ml +++ b/core/utility.ml @@ -301,13 +301,13 @@ struct end module type INTSET = Set with type elt = int +module type INTMAP = Map with type key = int module IntSet = Set.Make(Int) module IntMap = Map.Make(Int) module IntPairMap = Map.Make(IntPair) module type STRINGMAP = Map with type key = string -module type INTMAP = Map with type key = int module StringSet = Set.Make(String) module StringMap : STRINGMAP = Map.Make(String) @@ -600,6 +600,14 @@ struct | [] :: xss -> transpose xss | (x :: xs) :: xss -> (x :: (List.map List.hd xss)) :: transpose (xs :: List.map List.tl xss) + + let fold_left_map f accu l = + let rec aux accu l_accu = function + | [] -> accu, List.rev l_accu + | x :: l -> + let accu, x = f accu x in + aux accu (x :: l_accu) l in + aux accu [] l end include ListUtils diff --git a/core/value.ml b/core/value.ml index 8308c07ed..3ae9e5ea8 100644 --- a/core/value.ml +++ b/core/value.ml @@ -20,7 +20,7 @@ let printing_functions |> convert parse_bool |> sync) -let session_exception_operation = "SessionFail" +let session_exception_operation = Label.make "SessionFail" class type otherfield = object @@ -373,7 +373,7 @@ module type CONTINUATION_EVALUATOR = sig result val trap : v t -> (* the continuation *) - (Name.t * v) -> (* operation name and its argument *) + (Label.t * v) -> (* operation name and its argument *) trap_result end @@ -665,9 +665,9 @@ module Eff_Handler_Continuation = struct let open Trap in let rec handle k' = function | ((User_defined h, pk) :: k) -> - begin match StringMap.lookup opname h.cases with + begin match Label.Map.lookup opname h.cases with | Some (b, _, comp) - when session_exn_enabled && opname = session_exception_operation -> + when session_exn_enabled && Label.equal session_exception_operation opname -> let var = Var.var_of_binder b in let continuation_thunk = fun () -> E.computation (Env.bind var (arg, Scope.Local) h.env) k comp @@ -693,7 +693,7 @@ module Eff_Handler_Continuation = struct | None -> handle ((User_defined h, pk) :: k') k end | (identity, pk) :: k -> handle ((identity, pk) :: k') k - | [] when session_exn_enabled && opname = session_exception_operation -> + | [] when session_exn_enabled && Label.equal session_exception_operation opname -> (* If this is a session exception operation, we need to gather all * of the computations in the pure continuation stack, so we can inspect * their free variables. *) @@ -705,7 +705,7 @@ module Eff_Handler_Continuation = struct in UnhandledSessionException comps | [] -> - Trap (fun () -> E.error (Printf.sprintf "no suitable handler for operation %s has been installed." opname)) + Trap (fun () -> E.error (Printf.sprintf "no suitable handler for operation %s has been installed." (Label.show opname))) in handle [] k end diff --git a/core/value.mli b/core/value.mli index e2f85464b..9ad0ccdd8 100644 --- a/core/value.mli +++ b/core/value.mli @@ -177,7 +177,7 @@ module type CONTINUATION_EVALUATOR = sig (* trap invocation *) val trap : v t -> (* the continuation *) - (Name.t * v) -> (* operation name and its argument *) + (Label.t * v) -> (* operation name and its argument *) trap_result end @@ -325,6 +325,6 @@ val split_html : xml -> xml * xml val is_channel : t -> bool -val session_exception_operation : string +val session_exception_operation : Label.t val row_columns_values : t -> string list * t list list diff --git a/links-mode.el b/links-mode.el index fe45518a5..3d88859e9 100644 --- a/links-mode.el +++ b/links-mode.el @@ -66,6 +66,7 @@ "false" "for" "forall" + "fresh" "from" "fun" "formlet" diff --git a/tests/labels.tests b/tests/labels.tests new file mode 100644 index 000000000..277b2a90f --- /dev/null +++ b/tests/labels.tests @@ -0,0 +1,74 @@ +Unbounded local label +./tests/labels/unbounded.links +filemode : true +stderr : @.* +exit : 1 + +Simple scope and do operation +./tests/labels/simple.links +filemode : true +stdout : () : () + +Simple scope, effectname, typename and do operation +./tests/labels/simple-names.links +filemode : true +stdout : () : () + +Multiple label bounded at a time +./tests/labels/multiple.links +filemode : true +stdout : () : () + +Handler for local effect +./tests/labels/handler.links +filemode : true +stdout : 42 : Int +args : --enable-handlers + +Nested label bindings [1] +./tests/labels/nested.links +filemode : true +stdout : () : () + +Nested label bindings [2] +./tests/labels/nested-names.links +filemode : true +stderr : @.* +exit : 1 + +Wrong local handler +./tests/labels/wrong-handler.links +filemode : true +stderr : @.* +exit : 1 +args : --enable-handlers + +Avoiding pollution [1] +./tests/labels/pollution.links +filemode : true +stdout : (Just(42), Nothing, Just(-1)) : (Maybint, Maybint, Maybint) +args : --enable-handlers + +Avoiding pollution [2] +./tests/labels/nested-pollution.links +filemode : true +stdout : 42 : Int +args : --enable-handlers + +Lexical scoping [1] +fun() { var x = { fresh `A; 42 }; do `A } +stderr : @.* +exit : 1 + +Lexical scoping [2] +fun() { var x = { fresh `A; ignore(42); fun() { do `A } }; x } +stdout : fun : () -> () {`A:() => b|_}-> b + +Lexical scoping [3] +{ module T { fresh `A; } fun() { do `A } } +stderr : @.* +exit : 1 + +Lexical scoping [4] +module T { fresh `A; fun f() { do `A } } +stdout : () : () \ No newline at end of file diff --git a/tests/labels/handler.links b/tests/labels/handler.links new file mode 100644 index 000000000..d8bfbc847 --- /dev/null +++ b/tests/labels/handler.links @@ -0,0 +1,22 @@ +fresh `Ask; + +effectname A(e::Eff) = {`Ask:() => Int|e} ; + +sig h_ask : (Comp(a, { |A({ |e})})) -> Comp(a, {`Ask{_}|e}) +fun h_ask (m) () { + handle (m()) { + case <`Ask => k> -> k(41) + } +} + +sig f : () -A({ |e})-> Int +fun f () { + do `Ask + 1 +} + +sig res : () {`Ask{_}|_}~> Int +fun res () { + h_ask(f)() +} + +res () diff --git a/tests/labels/multiple.links b/tests/labels/multiple.links new file mode 100644 index 000000000..72448a27c --- /dev/null +++ b/tests/labels/multiple.links @@ -0,0 +1,9 @@ +fresh `A, `B, `C; +sig f : () {`A:(), `B:Bool}-> Bool +fun f () { do `A ; do `B } + +sig g : () {`C:Int, `B:Bool}-> Int +fun g () { if (do `B) 1 else do `C } + +sig h : () {`C:Int, `A:()}-> Int +fun h () { do `A ; do `C } diff --git a/tests/labels/nested-names.links b/tests/labels/nested-names.links new file mode 100644 index 000000000..df3a23ef4 --- /dev/null +++ b/tests/labels/nested-names.links @@ -0,0 +1,14 @@ +fresh `A, `B; + +effectname E = { `A:() {}-> Int } ; +typename T = () {`B:Bool | E}-> Bool ; + +sig f : T +fun f () { do `B && (do `A > 42) } + +fresh `A; + +sig f' : T +fun f' () { + do `A > 42 +} diff --git a/tests/labels/nested-pollution.links b/tests/labels/nested-pollution.links new file mode 100644 index 000000000..9401757e9 --- /dev/null +++ b/tests/labels/nested-pollution.links @@ -0,0 +1,43 @@ +fresh `A; +sig h_a : (Comp(a,{`A:(Int) => Int|e})) -> Comp(a, {`A{_}|e}) +fun h_a (m) () { + handle (m ()) { + case <`A(x) => k> -> k (2*x) + } +} + +sig double : (Int) {`A:(Int) => Int|e}-> Int +fun double (x) { do `A(x) } + +sig times_two : (Int) -> Comp(Int, {`A{_}|_}) +fun times_two (x) { h_a ( fun () { double(x) } ) } + +sig times_two' : (Int) {`A{_}|_}~> Int +fun times_two' (x) { times_two (x) () } + +fresh `A; + +sig h_a' : (Comp(a,{`A:(Int) => Int|e})) -> Comp(a, {`A{_}|e}) +fun h_a' (m) () { + handle (m()) { + case <`A(x) => k> -> k (3*x) + } +} + +sig triple : (Int) {`A:(Int) => Int|e}-> Int +fun triple (x) { do `A(x) } + +sig sextuple : (Int) {`A:(Int) => Int|e}~> Int +fun sextuple (x) { triple( times_two'(x) ) } + +sig times_six : (Int) -> Comp(Int, {`A{_}|_}) +fun times_six (x) { h_a' (fun () { sextuple (x) }) } + +sig times_six' : (Int) {`A{_}|_}~> Int +fun times_six' (x) { times_six (x) () } + +var fun_xlii = times_two( 21+21 ) ; + +var xlii = fun_xlii () ; + +xlii - times_six' (7) diff --git a/tests/labels/nested.links b/tests/labels/nested.links new file mode 100644 index 000000000..701465bf0 --- /dev/null +++ b/tests/labels/nested.links @@ -0,0 +1,16 @@ +fresh `A; +fresh `B; + +sig f : () {`A:(), `B:Bool}-> Bool +fun f () { do `A ; do `B } + +sig f' : () {`A:Int}-> Int +fun f' () { do `A * 42 } + +fresh `C, `B, `A; + +sig g : () {`C:Int, `B:Bool}-> Int +fun g () { if (do `B) 1 else do `C } + +sig h : () {`C:Int, `A:()}-> Int +fun h () { do `A ; do `C } diff --git a/tests/labels/pollution.links b/tests/labels/pollution.links new file mode 100644 index 000000000..f1fb84bb3 --- /dev/null +++ b/tests/labels/pollution.links @@ -0,0 +1,72 @@ +effectname A(e::Eff) = { Abort: () => Zero | e } ; +fun aborting () { switch (do Abort) {} } + +typename Maybint = Maybe(Int) ; + +sig maybe : ( Comp(a, { |A({ |e})} ) ) -> Comp (Maybe(a), {Abort{_}|e}) +fun maybe (h) () { + handle (h()) { + case x -> Just(x) + case _> -> Nothing + } +} + +effectname R(s,e::Eff) = { Receive : () => s | e } ; + +sig receives : ([s]) -> ( Comp(a, { |A({ |R(s, { |e})})}) ) -> Comp(a , {Receive{_}|A({ |e})}) +fun receives (ss) (h) () { + handle (h()) (ss<-ss) { + case k> -> switch (ss) { + case [] -> aborting() + case h::t -> k(h,t) + } + } +} + +fresh `Abort; + +sig protect : (Comp(a, {`Abort:Zero, Abort:Zero | e})) -> Comp(a, {Abort{_}, `Abort:Zero|e}) +fun protect (m) () { + handle (m()) { + case k> -> k (do `Abort) + } +} + +sig unprotect : (Comp(a, {`Abort:Zero, Abort:Zero | e})) -> Comp(a, {`Abort{_}, Abort:Zero|e}) +fun unprotect (m) () { + handle (m()) { + case <`Abort => k> -> k (do Abort) + } +} + + +typename CA(a,e::Eff) = Comp(a, {Abort:Zero|e}) ; +typename CNAR(a,s,e::Eff) = Comp(a, {Receive:s, Abort:Zero, `Abort- |e}) ; +typename CAR(a,s,e::Eff) = Comp(a, {Receive:s, Abort:Zero, `Abort:Zero|e}) ; + +sig withtwo21s : (CNAR(a,Int,{ |e})) -> CA(Maybe(a), {Receive{_}, `Abort{_} |e}) +fun withtwo21s (h) { unprotect ( maybe( receives ([21,21]) ( protect ( h : CAR(a,Int,{ |e}) <- (CNAR(a,Int,{ |e})) + ) ) ) ) } + + +typename CRI(e::Eff) = Comp(Int, { |R(Int,{ |e})}) ; + +sig f : CRI({ |e}) fun f () { do Receive + do Receive } +sig g : CRI({ |e}) fun g () { do Receive + do Receive + do Receive } + +fun h () { if (do Receive < 42) switch (do Abort) {} else 0 } + +sig res : ( Comp(Maybint, {Abort:Zero |e}) ) -> Comp(Maybint, {Abort{_}|e}) +fun res (h) () { + handle(h()) { + case _> -> Just(-1) + } +} + + +# return values ############################################################### +( + res(withtwo21s( f )) () , + res(withtwo21s( g )) () , + res(withtwo21s( h )) () +) diff --git a/tests/labels/simple-names.links b/tests/labels/simple-names.links new file mode 100644 index 000000000..df34f18ed --- /dev/null +++ b/tests/labels/simple-names.links @@ -0,0 +1,6 @@ +fresh `A; +effectname E = { `A:() => () } ; +typename T = () -E-> () ; + +sig f : T +fun f () { do `A } diff --git a/tests/labels/simple.links b/tests/labels/simple.links new file mode 100644 index 000000000..05ab3fad5 --- /dev/null +++ b/tests/labels/simple.links @@ -0,0 +1,2 @@ +fresh `A; +fun f () { do `A } diff --git a/tests/labels/unbounded.links b/tests/labels/unbounded.links new file mode 100644 index 000000000..bffd51bde --- /dev/null +++ b/tests/labels/unbounded.links @@ -0,0 +1 @@ +fun f () { do `A } diff --git a/tests/labels/wrong-handler.links b/tests/labels/wrong-handler.links new file mode 100755 index 000000000..cb2ffcab6 --- /dev/null +++ b/tests/labels/wrong-handler.links @@ -0,0 +1,22 @@ +fresh `Ask; +sig h_ask : (Comp(a, {`Ask:Int|e})) -> Comp(a, {`Ask{_}|e}) +fun h_ask (m) () { + handle (m()) { + case <`Ask => k> -> k(42) + } +} + +sig f : () {`Ask:Int|_} -> Int +fun f () { + do `Ask + 1 +} + +fresh `Ask; + +sig h_ask' : (Comp(a, {`Ask:Int|e})) -> Comp(a, {`Ask{_}|e}) +fun h_ask' (m) () { + handle (m()) { + case <`Ask => k> -> k(666) +} + +h_ask'(f) () diff --git a/tests/unit/ir/schinks.ml b/tests/unit/ir/schinks.ml index 376186879..3dfe63355 100644 --- a/tests/unit/ir/schinks.ml +++ b/tests/unit/ir/schinks.ml @@ -29,8 +29,8 @@ let check_assoc_list_for_duplicates assoc description = let has_duplicates = List.fold_left (fun (seen, dupls) (key, _) -> - (StringSet.add key seen, dupls && StringSet.mem key seen)) - (StringSet.empty, [] <> assoc) + (Label.Set.add key seen, dupls && Label.Set.mem key seen)) + (Label.Set.empty, [] <> assoc) assoc |> snd in @@ -195,7 +195,8 @@ let ( |--> ) = fun_ct let wild_fun_ct parameters codomain = let effects = State.return - (Types.make_singleton_closed_row ("wild", Types.Present Types.unit_type)) + (Types.make_singleton_closed_row + (Types.wild, Types.Present Types.unit_type)) |> State.return in fun_t ~effects parameters codomain @@ -203,6 +204,7 @@ let wild_fun_ct parameters codomain = let ( |~~> ) = wild_fun_ct let record_t ?row_var assoc = + let assoc = List.map (fun (x, y) -> (Label.make x, y)) assoc in let row_var = match row_var with | Some rv -> rv @@ -210,10 +212,11 @@ let record_t ?row_var assoc = in check_assoc_list_for_duplicates assoc "record type"; helper_tuple1 assoc row_var (fun assoc row_var -> - let map = StringMap.from_alist assoc in + let map = Label.Map.from_alist assoc in Types.Record (Types.Row (map, row_var, false))) let variant ?row_var assoc = + let assoc = List.map (fun (x, y) -> (Label.make x, y)) assoc in check_assoc_list_for_duplicates assoc "variant type"; let row_var = match row_var with @@ -221,7 +224,7 @@ let variant ?row_var assoc = | None -> Unionfind.fresh Types.Closed |> State.return |> State.return in helper_tuple1 assoc row_var (fun assoc row_var -> - let map = StringMap.from_alist assoc in + let map = Label.Map.from_alist assoc in Types.Variant (Types.Row (map, row_var, false))) (* Rows *) @@ -234,8 +237,9 @@ let row_var rv = Unionfind.fresh (Types.Var (id, (CT.PrimaryKind.Row, sk), `Rigid)) let row assoc rv = + let assoc = List.map (fun (x, y) -> (Label.make x, y)) assoc in let mk_row assoc rv = - let map = StringMap.from_alist assoc in + let map = Label.Map.from_alist assoc in Types.Row (map, rv, false) in check_assoc_list_for_duplicates assoc "row"; @@ -344,15 +348,16 @@ let wi_binder ?(scope = Var.Scope.Local) id ty = let build_record (extendee : Ir.value t option) (assoc : (string * Ir.value t) list) : Ir.value t = + let assoc = List.map (fun (x, y) -> (Label.make x, y)) assoc in let _, has_duplicates = List.fold_left (fun (seen, dupls) (key, _) -> - (StringSet.add key seen, dupls && StringSet.mem key seen)) - (StringSet.empty, [] <> assoc) + (Label.Set.add key seen, dupls && Label.Set.mem key seen)) + (Label.Set.empty, [] <> assoc) assoc in let stage2 (extendee : Ir.value lookup option) - (assoc : (string * Ir.value Repr.lookup) list) : Ir.value lookup = + (assoc : (Label.t * Ir.value Repr.lookup) list) : Ir.value lookup = let* assoc = State.List.map ~f:(fun (x, y) -> @@ -360,7 +365,7 @@ let build_record (extendee : Ir.value t option) (x, y)) assoc in - let map = StringMap.from_alist assoc in + let map = Label.Map.from_alist assoc in let finalize e = if has_duplicates then raise (SchinksError "Duplicate fields in record!") else Ir.Extend (map, e) @@ -371,14 +376,14 @@ let build_record (extendee : Ir.value t option) let+ e = e in finalize (Some e) in - let assoc : (string * Ir.value lookup) list stage1 = + let assoc : (Label.t * Ir.value lookup) list stage1 = State.List.map ~f:(fun (x, y) -> let+ y = y in (x, y)) assoc in - let* (assoc : (string * Ir.value lookup) list) = assoc in + let* (assoc : (Label.t * Ir.value lookup) list) = assoc in match extendee with | Some (e : Ir.value t) -> let+ (e : Ir.value lookup) = e in @@ -424,6 +429,7 @@ let apply f args = let case (v : Ir.value t) ?(default : (Ir.binder t * Ir.computation t) option) (cases : (string * Ir.binder t * Ir.computation t) list) : Ir.tail_computation t = + let cases = List.map (fun (x, y, z) -> (Label.make x, y, z)) cases in let* v = v in let f (x, y) = let* x = x in @@ -442,7 +448,7 @@ let case (v : Ir.value t) ?(default : (Ir.binder t * Ir.computation t) option) let+ cases = State.List.map ~f:g cases in let assoc = List.map (fun (a, b, c) -> (a, (b, c))) cases in check_assoc_list_for_duplicates assoc "variants of case"; - let case_map = StringMap.from_alist assoc in + let case_map = Label.Map.from_alist assoc in Ir.Case (v, case_map, default) (*