effectalias init

desalias inline alias = effectname and typename | init merge into 1 construct ok; still 2 contexts merge type and effect aliases contexts effectname body desugared into effectname allow better printing Revert "desalias inline" This reverts commit 49a9a61. Revert "effectname body desugared into effectname" This reverts commit 5150615. "effectname" in links-mode.el cleaning before pr re-cleaning effectname -> typename _::Kind Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/desugarDatatypes.mli Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/defaultAliases.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/desugarDatatypes.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/desugarDatatypes.ml Co-authored-by: Daniel Hillerström <[email protected]> rename alias_env -> tycon_env as originally Update core/desugarDatatypes.ml Co-authored-by: Daniel Hillerström <[email protected]> idem fixes & add primary kind in aliases new error kind mismatch fix : embeded errors fixes fix : underscore in effect app various fixes short type in effectname + short fun non desugar comment Attempted workaround for links-lang#1136 (links-lang#1138) always desugar op type with type application correction tests default arg in repl Effect aliasing (links-lang#1141) I added the possibility to write effect aliases, similarly as what already exists for types. - there is a new keyword `effectname` - to write an alias for an effect row : `effectname MyEffectRow(a, ... ,e::Eff, ...) = { Op1 : type, ... | e }` the arguments being type variable of any kind (kinds other than type must be explicit) - we can have, as above, an open row (the row variable is a parameter of the effect alias) or a closed one (just do not write the `| e` - To use it in a signature or in another type or effect alias just apply it with the right arguments as for `typename` things. - In arrows, we can use them as row variables: `() -MyEffectRow(args)-> ()` (idem with `~>`) - However, due to lack of kind inference, row variables and aliases have to be used carefully so that links does not think they are of kind type. We need to write them most of the time between braces ` { | ... }`. For instance, if you have `effectname E(a::Eff) = {X : ... | a }` and a row variable `e::Eff`, you will have to write `E({ |e})`. (Idem for another effect alias instead of the variable). This makes the usage of several nested aliases a bit messy, it would be nice if we could avoid it. - We cannot write recursive effect aliases for now. In the branch `visitor`, I added another transformer that makes possible simple recursion by inlining a mu type in one pass. - For now the aliases are replaced by the row they correspond to : we do not keep aliases. - In the repl, effect alias definitions are printed but without the braces ! Rows are in general printed without braces and the alias body is a row. => this might need to be enhanced About implementation, I copied and then merged most of the time what existed for `typename`. Co-authored-by: Daniel Hillerström <[email protected]> Fix assert error with relational lenses (links-lang#1143) The `Lens` type traversal was unimplemented and filled in with an `assert false`. As a result, all RL code fails. I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for `Lens.Type.t` type and plug it in as usual. Make `custom_js_runtime` a multi option (links-lang#1146) Added the ability to link multiple custom js runtime files. Co-authored-by: s1908422 <[email protected]> Co-authored-by: Daniel Hillerström <[email protected]> Allow 'default' as an argument to settings in the REPL (links-lang#1147) Some settings has the value 'default'. Prior to this patch the value 'default' could not be written in the REPL, because it is token. This patch rectifies this problem by allowing the token 'default' to appear in settings argument position in the REPL. Co-authored-by: Daniel Hillerström <[email protected]> Allow record extension in presence of temporal projections (links-lang#1129) * Allow record extension in presence of temporal projections This allows record extension to play nicely with temporal projections. I was forgetting that all arguments to reduce_artifacts are already eta-expanded, so we can work with record literals. Fixes links-lang#1124. * Allow extension to work with (shallow) temporal projections We don't have the full generality due to links-lang#1130, but this patch should allow record extension to be used on temporal projections on variables / record literals. Removal of unused headless testing (links-lang#1152) The headless testing has been unused for about a year, because it is unmaintained. Even though it is not used, it generates a ton of security warnings here on GitHub. I am not interested in dealing with those, therefore this patch removes the headless testing directory from the source tree. Attempted workaround for links-lang#1136 (links-lang#1138) always desugar op type with type application correction tests default arg in repl Option -> Maybe fix (links-lang#1142) The `Option -> Maybe` refactoring patch links-lang#1131 missed one instance: the `max` function. This patch changes the type signature of `max` to use `Maybe` rather than `Option`. Effect aliasing (links-lang#1141) I added the possibility to write effect aliases, similarly as what already exists for types. - there is a new keyword `effectname` - to write an alias for an effect row : `effectname MyEffectRow(a, ... ,e::Eff, ...) = { Op1 : type, ... | e }` the arguments being type variable of any kind (kinds other than type must be explicit) - we can have, as above, an open row (the row variable is a parameter of the effect alias) or a closed one (just do not write the `| e` - To use it in a signature or in another type or effect alias just apply it with the right arguments as for `typename` things. - In arrows, we can use them as row variables: `() -MyEffectRow(args)-> ()` (idem with `~>`) - However, due to lack of kind inference, row variables and aliases have to be used carefully so that links does not think they are of kind type. We need to write them most of the time between braces ` { | ... }`. For instance, if you have `effectname E(a::Eff) = {X : ... | a }` and a row variable `e::Eff`, you will have to write `E({ |e})`. (Idem for another effect alias instead of the variable). This makes the usage of several nested aliases a bit messy, it would be nice if we could avoid it. - We cannot write recursive effect aliases for now. In the branch `visitor`, I added another transformer that makes possible simple recursion by inlining a mu type in one pass. - For now the aliases are replaced by the row they correspond to : we do not keep aliases. - In the repl, effect alias definitions are printed but without the braces ! Rows are in general printed without braces and the alias body is a row. => this might need to be enhanced About implementation, I copied and then merged most of the time what existed for `typename`. Co-authored-by: Daniel Hillerström <[email protected]> Fix assert error with relational lenses (links-lang#1143) The `Lens` type traversal was unimplemented and filled in with an `assert false`. As a result, all RL code fails. I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for `Lens.Type.t` type and plug it in as usual. Make `custom_js_runtime` a multi option (links-lang#1146) Added the ability to link multiple custom js runtime files. Co-authored-by: s1908422 <[email protected]> Co-authored-by: Daniel Hillerström <[email protected]> wip Allow 'default' as an argument to settings in the REPL (links-lang#1147) Some settings has the value 'default'. Prior to this patch the value 'default' could not be written in the REPL, because it is token. This patch rectifies this problem by allowing the token 'default' to appear in settings argument position in the REPL. Co-authored-by: Daniel Hillerström <[email protected]> Allow record extension in presence of temporal projections (links-lang#1129) * Allow record extension in presence of temporal projections This allows record extension to play nicely with temporal projections. I was forgetting that all arguments to reduce_artifacts are already eta-expanded, so we can work with record literals. Fixes links-lang#1124. * Allow extension to work with (shallow) temporal projections We don't have the full generality due to links-lang#1130, but this patch should allow record extension to be used on temporal projections on variables / record literals. Removal of unused headless testing (links-lang#1152) The headless testing has been unused for about a year, because it is unmaintained. Even though it is not used, it generates a ton of security warnings here on GitHub. I am not interested in dealing with those, therefore this patch removes the headless testing directory from the source tree.
Orbion-J · Jul 8, 2022 · e21950d · e21950d
1 parent 474137f
commit e21950d
Show file tree

Hide file tree

Showing 60 changed files with 752 additions and 4,174 deletions.
diff --git a/bin/driver.ml b/bin/driver.ml
@@ -235,30 +235,35 @@ module Phases = struct
         if Settings.get Basicsettings.System.link_js_runtime
         then begin
             Js_CodeGen.output oc Compiler.primitive_bindings;
-            let runtime_file =
+            let runtime_files =
               match Settings.get Basicsettings.System.custom_js_runtime with
-              | None ->
-                 begin match Settings.get jslib_dir with
-                   | None | Some "" ->
+              | [] ->
+                let file =
+                  begin match Settings.get jslib_dir with
+                    | None | Some "" ->
                       begin
                         Filename.concat
                           (match Utility.getenv "LINKS_LIB" with
-                           | None -> Filename.dirname Sys.executable_name
-                           | Some path -> path)
-                          (Filename.concat "js" "jslib.js")
+                            | None -> Filename.dirname Sys.executable_name
+                            | Some path -> path)
+                            (Filename.concat "js" "jslib.js")
                       end
-                   | Some path -> Filename.concat path "jslib.js"
-                 end
-              | Some file -> file
+                    | Some path -> Filename.concat path "jslib.js"
+                  end
+                in [file]
+              | files -> files
             in
-            let ic =
-              try open_in runtime_file
-              with Sys_error reason -> raise (Errors.cannot_open_file runtime_file reason)
-            in
-            try
-              Utility.IO.Channel.cat ic oc;
-              close_in ic
-            with e -> close_in ic; raise e
+            List.iter
+              (fun runtime_file ->
+                let ic =
+                  try open_in runtime_file
+                  with Sys_error reason -> raise (Errors.cannot_open_file runtime_file reason)
+                in
+                try
+                  Utility.IO.Channel.cat ic oc;
+                  close_in ic
+                with e -> close_in ic; raise e)
+              runtime_files;
           end;
         (* Copy contents of FFI files. *)
         List.iter

diff --git a/core/basicsettings.ml b/core/basicsettings.ml
@@ -116,11 +116,11 @@ module System = struct
               |> sync)
 
   let custom_js_runtime =
-    Settings.(option "custom_js_runtime"
+    Settings.(multi_option "custom_js_runtime"
               |> privilege `User
               |> synopsis "If link_js_runtime is set to true, then the JS compiler will link the provided file(s) rather than the standard Links JS runtime"
-              |> to_string from_string_option
-              |> convert (fun s -> Some s)
+              |> to_string string_of_paths
+              |> convert parse_paths
               |> hidden
               |> CLI.(add (long "Xcustom-js-runtime"))
               |> sync)

diff --git a/core/defaultAliases.ml b/core/defaultAliases.ml
@@ -15,21 +15,21 @@ let alias_env : Types.tycon_environment =
   let wq, w = mk_arg () in
   let nq, n = mk_arg () in
   let th_alias_type =
-      `Alias ([rq; wq; nq], Types.make_tablehandle_alias (r, w, n))
+      `Alias (pk_type, [rq; wq; nq], Types.make_tablehandle_alias (r, w, n))
   in
 
   List.fold_left
     (fun env (name, t) ->
       AliasEnv.bind name t env)
     AliasEnv.empty
     [ (* "String"  , `Alias ([], `Application (Types.list, [`Type (`Primitive Primitive.Char)])); *)
-      "Xml"     , `Alias ([], Types.Application (Types.list, [(PrimaryKind.Type, Types.Primitive Primitive.XmlItem)]));
+      "Xml"     , `Alias (pk_type, [], Types.Application (Types.list, [(PrimaryKind.Type, Types.Primitive Primitive.XmlItem)]));
       "Event"   , `Abstract Types.event;
       "List"    , `Abstract Types.list;
       "Process" , `Abstract Types.process;
       "DomNode" , `Abstract Types.dom_node;
       "AP"      , `Abstract Types.access_point;
-      "EndBang" , `Alias ([], Types.make_endbang_type);
+      "EndBang" , `Alias (pk_type, [], Types.make_endbang_type);
       "Socket"  , `Abstract Types.socket;
       "ValidTime", `Abstract Types.valid_time_data;
       "TransactionTime", `Abstract Types.transaction_time_data;

diff --git a/core/desugarDatatypes.ml b/core/desugarDatatypes.ml
@@ -45,6 +45,10 @@ object (self)
       (_, None) -> {< all_desugared = false >}
     | _ -> self
 
+  method! row' = function
+      (_, None) -> {< all_desugared = false >}
+    | _ -> self
+
   method! type_arg' = function
       (_, None) -> {< all_desugared = false >}
     | _ -> self
@@ -125,13 +129,9 @@ module Desugar = struct
                 let t_kind = primary_kind_of_type_arg t in
                 if q_kind <> t_kind then
                   raise
-                    (TypeApplicationKindMismatch
-                       { pos;
-                         name = tycon;
-                         tyarg_number = i;
-                         expected = PrimaryKind.to_string q_kind;
-                         provided = PrimaryKind.to_string t_kind
-                       })
+                    (type_application_kind_mismatch pos tycon i
+                        (PrimaryKind.to_string q_kind)
+                        (PrimaryKind.to_string t_kind))
                 else t
               in
               let type_args qs ts =
@@ -149,10 +149,14 @@ module Desugar = struct
                 raise (TypeApplicationArityMismatch { pos; name = tycon; expected = qn; provided = tn })
             in
             begin match SEnv.find_opt tycon alias_env with
-              | None -> raise (UnboundTyCon (pos, tycon))
-              | Some (`Alias (qs, _dt)) ->
-                  let ts = match_quantifiers snd qs in
-                  Instantiate.alias tycon ts alias_env
+              | None -> raise (unbound_tycon pos tycon)
+              | Some (`Alias (k, qs, _dt)) ->
+                  if k = pk_type then
+                    let ts = match_quantifiers snd qs in
+                    Instantiate.alias tycon ts alias_env
+                  else
+                    raise (type_application_global_kind_mismatch pos tycon
+                        "Type" (PrimaryKind.to_string k))
               | Some (`Abstract abstype) ->
                   let ts = match_quantifiers identity (Abstype.arity abstype) in
                   Application (abstype, ts)
@@ -209,6 +213,70 @@ module Desugar = struct
     let seed =
       let open Datatype in
       match rv with
+        | EffectApplication (name, ts) ->
+            let match_quantifiers : type a. (a -> Kind.t) -> a list -> Types.type_arg list = fun proj qs ->
+              let match_kinds i (q, t) =
+                let primary_kind_of_type_arg : Datatype.type_arg -> PrimaryKind.t = function
+                  | Type _ -> PrimaryKind.Type
+                  | Row _ -> PrimaryKind.Row
+                  | Presence _ -> PrimaryKind.Presence
+                in
+                let q_kind, _ = proj q in
+                let t_kind = primary_kind_of_type_arg t in
+                if q_kind <> t_kind then
+                  raise
+                    (type_application_kind_mismatch node.pos name i
+                        (PrimaryKind.to_string q_kind)
+                        (PrimaryKind.to_string t_kind))
+                else t
+              in
+              let type_args qs ts =
+                List.combine qs ts
+                |> List.mapi
+                     (fun i (q,t) ->
+                       let  t = match_kinds i (q, t) in
+                       type_arg alias_env t node)
+              in
+              let qn = List.length qs and tn = List.length ts in
+              if qn = tn then
+                type_args qs ts
+              else
+                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)
+              | Some (`Alias (k, qs, _r)) ->
+                  if k = pk_row then
+                    let ts = match_quantifiers snd qs in
+                    begin match Instantiate.alias name ts alias_env with
+                      | Alias(PrimaryKind.Row, _, body) -> body
+                      | _ -> raise (internal_error "Instantiation failed")
+                    end
+                  else
+                    raise (type_application_global_kind_mismatch node.pos name
+                        "Row" (PrimaryKind.to_string k))
+              | Some (`Abstract abstype) ->
+                  let ts = match_quantifiers identity (Abstype.arity abstype) in
+                  Application (abstype, ts)
+              | Some (`Mutual (qs, tygroup_ref)) ->
+                  (* Check that the quantifiers / kinds match up, then generate
+                   * a `RecursiveApplication. *)
+                  let r_args = match_quantifiers snd qs in
+                  let r_unwind args dual =
+                    let _, body = StringMap.find name !tygroup_ref.type_map in
+                    let body = Instantiate.recursive_application name qs args body in
+                    if dual then dual_type body else body
+                  in
+                  let r_unique_name = name ^ string_of_int !tygroup_ref.id in
+                  let r_linear () = StringMap.lookup name !tygroup_ref.linearity_map in
+                  RecursiveApplication
+                    { r_name = name;
+                      r_dual = false;
+                      r_unique_name;
+                      r_quantifiers = List.map snd qs;
+                      r_args; r_unwind; r_linear
+                    }
+            end
         | Closed -> Types.make_empty_closed_row ()
         | Open srv ->
            let rv = SugarTypeVar.get_resolved_row_exn srv in
@@ -236,11 +304,16 @@ module Desugar = struct
     | Row r      -> Row, row alias_env r node
     | Presence f -> Presence, fieldspec alias_env f node
 
-
-
   let datatype' alias_env ((dt, _) : datatype') =
     (dt, Some (datatype alias_env dt))
 
+  let row' alias_env ((r, _) :row') =
+    (r, Some (row alias_env r (WithPos.make (Datatype.Effect r)))) (* should we keep the pos ? have a real node ? *)
+
+  let aliasbody alias_env = function
+    | Typename dt' -> Typename (datatype' alias_env dt')
+    | Effectname r' -> Effectname (row' alias_env r')
+
   let type_arg' alias_env ((ta, _) : type_arg') : type_arg' =
     let unlocated = WithPos.make Datatype.Unit in
     (ta, Some (type_arg alias_env ta unlocated))
@@ -288,6 +361,8 @@ object (self)
 
   method! datatype' node = (self, Desugar.datatype' alias_env node)
 
+  method! row' node = (self, Desugar.row' alias_env node)
+
   method! type_arg' node = (self, Desugar.type_arg' alias_env node)
 
   method! phrasenode = function
@@ -325,7 +400,7 @@ object (self)
 
 
   method! bindingnode = function
-    | Typenames ts ->
+    | Aliases ts ->
         (* Maps syntactic types in the recursive group to semantic types. *)
         (* This must be empty to start off with, because there's a cycle
          * in calculating the semantic types: we need the alias environment
@@ -340,36 +415,43 @@ object (self)
 
         (* Add all type declarations in the group to the alias
          * environment, as mutuals. Quantifiers need to be desugared. *)
-        let ((mutual_env : tycon_spec SEnv.t), ts) =
-          List.fold_left (fun (alias_env, ts) {node=(t, args, (d, _)); pos} ->
+        let ((mutual_env : Types.tycon_environment), ts) =
+          List.fold_left (fun (alias_env, ts) {node=(t, args, b); pos} ->
             let qs = Desugar.desugar_quantifiers args  in
-            let alias_env = SEnv.bind t (`Mutual (qs, tygroup_ref)) alias_env in
-            (alias_env, WithPos.make ~pos (t, args, (d, None)) :: ts))
+            match b with
+              | Typename (d,_) ->
+                let alias_env = SEnv.bind t (`Mutual (qs, tygroup_ref)) alias_env in
+                (alias_env, WithPos.make ~pos (t, args, Typename (d, None)) :: ts)
+              | Effectname (r,_) ->
+                let alias_env = SEnv.bind t (`Mutual (qs, tygroup_ref)) alias_env in
+                (alias_env, WithPos.make ~pos (t, args, Effectname (r, None)) :: ts))
             (alias_env, []) ts in
 
         (* Desugar all DTs, given the temporary new alias environment. *)
         let desugared_mutuals =
-          List.map (fun {node=(name, args, dt); pos} ->
+          List.map (fun {node=(name, args, b); pos} ->
             (* Desugar the datatype *)
-            let dt' = Desugar.datatype' mutual_env dt in
             (* Check if the datatype has actually been desugared *)
-            let (t, dt) =
-              match dt' with
-               | (t, Some dt) -> (t, dt)
-               | _ -> assert false in
-            WithPos.make ~pos (name, args, (t, Some dt))
+            let b' = match Desugar.aliasbody mutual_env b with
+                | Typename     (_, Some _) as b' -> b'
+                | Effectname   (_, Some _) as b' -> b'
+                | _ -> raise (internal_error "Datatype not desugared")
+            in
+            WithPos.make ~pos (name, args, b')
           ) ts in
 
         (* Given the desugared datatypes, we now need to handle linearity.
            First, calculate linearity up to recursive application *)
         let (linearity_env, dep_graph) =
           List.fold_left (fun (lin_map, dep_graph) mutual   ->
-            let (name, _, (_, dt)) = SourceCode.WithPos.node mutual in
-            let dt = OptionUtils.val_of dt in
-            let lin_map = StringMap.add name (not @@ Unl.type_satisfies dt) lin_map in
-            let deps = recursive_applications dt in
-            let dep_graph = (name, deps) :: dep_graph in
-            (lin_map, dep_graph)
+            match SourceCode.WithPos.node mutual with
+            | (name, _, Typename     (_, dt))
+            | (name, _, Effectname   (_, dt)) ->
+              let dt = OptionUtils.val_of dt in
+              let lin_map = StringMap.add name (not @@ Unl.type_satisfies dt) lin_map in
+              let deps = recursive_applications dt in
+              let dep_graph = (name, deps) :: dep_graph in
+              (lin_map, dep_graph)
           ) (StringMap.empty, []) desugared_mutuals in
         (* Next, use the toposorted dependency graph from above. We need to
            reverse since we propagate linearity information downwards from the
@@ -400,19 +482,22 @@ object (self)
         (* NB: type aliases are scoped; we allow shadowing.
            We also allow type aliases to shadow abstract types. *)
         let alias_env =
-          List.fold_left (fun alias_env {node=(t, args, (_, dt')); _} ->
-            let dt = OptionUtils.val_of dt' in
+          List.fold_left (fun alias_env {node=(t, args, b); _} ->
             let semantic_qs = List.map SugarQuantifier.get_resolved_exn args in
-            let alias_env =
-              SEnv.bind t (`Alias (semantic_qs, dt)) alias_env in
+            let dt, k = match b with
+              | Typename     (_, dt') -> OptionUtils.val_of dt', pk_type
+              | Effectname   (_, dt') -> OptionUtils.val_of dt', pk_row
+            in
+            let alias_env = SEnv.bind t (`Alias (k , semantic_qs, dt)) alias_env in
             tygroup_ref :=
               { !tygroup_ref with
                   type_map = (StringMap.add t (semantic_qs, dt) !tygroup_ref.type_map);
                   linearity_map };
             alias_env
         ) alias_env desugared_mutuals in
 
-        ({< alias_env = alias_env >}, Typenames desugared_mutuals)
+        ({< alias_env = alias_env >}, Aliases desugared_mutuals)
+
     | Foreign alien ->
        let binder, datatype = Alien.declaration alien in
        let _, binder = self#binder binder in