Updating: adding libats/ML/argvec

libats/ML/DATS/argvec.dats

@@ -0,0 +1,82 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                         Applied Type System                         *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** ATS is free software;  you can  redistribute it and/or modify it under
+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
+** Free Software Foundation; either version 3, or (at  your  option)  any
+** later version.
+**
+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
+** for more details.
+**
+** You  should  have  received  a  copy of the GNU General Public License
+** along  with  ATS;  see the  file COPYING.  If not, please write to the
+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
+** 02110-1301, USA.
+*)
+
+(* ****** ****** *)
+
+(* Author: Hongwei Xi *)
+(* Start time: March, 2018 *)
+(* Authoremail: gmhwxiATgmailDOTcom *)
+
+(* ****** ****** *)
+
+#define ATS_DYNLOADFLAG 0
+
+(* ****** ****** *)
+
+staload
+UN = "prelude/SATS/unsafe.sats"
+
+(* ****** ****** *)
+
+staload "libats/ML/SATS/basis.sats"
+
+(* ****** ****** *)
+
+staload "libats/ML/SATS/list0.sats"
+staload "libats/ML/SATS/argvec.sats"
+
+(* ****** ****** *)
+
+implement
+listize_argc_argv
+{n}(argc, argv) = let
+//
+fun
+loop
+{i:nat | i <= n}
+( i: int(i)
+,
+argv: !argv(n)
+,
+args: list0(string)): list0(string) =
+if
+(i >= 1)
+then let
+  val
+  arg = argv[i-1]
+in
+  loop
+  (i-1, argv, list0_cons(arg, args))
+end else args
+//
+in
+  loop(argc, argv, list0_nil((*void*)))
+end // end of [listize_argc_argv]
+
+(* ****** ****** *)
+
+(* end of [argvec.dats] *)

libats/ML/SATS/argvec.sats

@@ -0,0 +1,55 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                         Applied Type System                         *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** ATS is free software;  you can  redistribute it and/or modify it under
+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
+** Free Software Foundation; either version 3, or (at  your  option)  any
+** later version.
+** 
+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
+** for more details.
+** 
+** You  should  have  received  a  copy of the GNU General Public License
+** along  with  ATS;  see the  file COPYING.  If not, please write to the
+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
+** 02110-1301, USA.
+*)
+
+(* ****** ****** *)
+
+(* Author: Hongwei Xi *)
+(* Start time: March, 2018 *)
+(* Authoremail: gmmhwxiATgmailDOTcom *)
+
+(* ****** ****** *)
+//
+#define
+ATS_PACKNAME "ATSLIB.libats.ML"
+//
+#define
+ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
+//
+(* ****** ****** *)
+
+staload "libats/ML/SATS/basis.sats"
+
+(* ****** ****** *)
+//
+fun
+listize_argc_argv
+  {n:pos}
+  (argc: int(n), argv: !argv(n)): list0(string)
+//
+(* ****** ****** *)
+
+(* end of [list0.sats] *)

share/HATS/atspre_staload_libats_ML.hats

@@ -91,6 +91,11 @@ LIBATSML_targetloc "$PATSHOME/libats/ML"
 #staload _ =
 "{$LIBATSML}/DATS/stream_vt.dats"
 //
+(* ****** ****** *)
+
+staload
+"{$LIBATSML}/SATS/argvec.sats"
+
 (* ****** ****** *)
 //
 #staload