diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6f1c1502e..fd7e6ca2a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -3,7 +3,7 @@ # "build-test-deploy". It is triggered on push or pull request events # on the master branch. It is also triggered when a tag is pushed, in # which case a binary distribution is deployed. The build matrix is -# currently setup to run only with mlton as the primary SML compiler. +# currently setup to run only with mlkit as the primary SML compiler. name: CI @@ -28,8 +28,9 @@ jobs: strategy: matrix: os: [ubuntu-20.04, macos-latest] -# mlcomp: [mlkit, mlton] - mlcomp: [mlton] + mlcomp: [mlkit, mlton] +# mlcomp: [mlton] +# mlcomp: [mlkit] runs-on: ${{ matrix.os }} @@ -43,31 +44,70 @@ jobs: echo "RUNHOME=$(echo $HOME)" >> $GITHUB_ENV - name: Install dependencies (linux) + if: ${{ env.OS == 'linux' }} + run: | + # sudo apt-get -qq update + sudo apt-get install -y gcc autoconf make + + - name: Install dependencies (linux, mlton) if: ${{ env.OS == 'linux' && matrix.mlcomp == 'mlton' }} run: | # sudo apt-get -qq update - sudo apt-get install -y gcc mlton autoconf make + sudo apt-get install -y mlton - name: Install dependencies (macos) - if: ${{ env.OS == 'darwin' && matrix.mlcomp == 'mlton' }} + if: ${{ env.OS == 'darwin' }} run: | brew install gcc autoconf make - # The brew version of MLton has a bug - brew install mlton --HEAD brew tap homebrew/cask brew install --cask phantomjs - - name: Check + - name: Install dependencies (macos, mlton) + if: ${{ env.OS == 'darwin' && matrix.mlcomp == 'mlton' }} + run: | + # The brew version of MLton has a bug + brew install mlton --HEAD + + - name: Install MLKit and smlpkg + working-directory: ${{ env.RUNHOME }} + run: | + echo "[OS: $OS, HOME: $RUNHOME]" + wget https://github.com/diku-dk/smlpkg/releases/download/v0.1.4/smlpkg-bin-dist-${{env.OS}}.tgz + tar xzf smlpkg-bin-dist-${{env.OS}}.tgz + echo "$HOME/smlpkg-bin-dist-${{env.OS}}/bin" >> $GITHUB_PATH + wget https://github.com/melsman/mlkit/releases/download/v4.7.4/mlkit-bin-dist-${{env.OS}}.tgz + tar xzf mlkit-bin-dist-${{env.OS}}.tgz + echo "$HOME/mlkit-bin-dist-${{env.OS}}/bin" >> $GITHUB_PATH + mkdir -p .mlkit + echo "SML_LIB $HOME/mlkit-bin-dist-${{env.OS}}/lib/mlkit" > .mlkit/mlb-path-map + + - name: Check MLton + if: ${{ matrix.mlcomp == 'mlton' }} run: | mlton echo 'github.event_name: ' ${{ github.event_name }} echo 'github.ref: ' ${{ github.ref }} - - name: Configure + - name: Check MLKit + if: ${{ matrix.mlcomp == 'mlkit' }} + run: | + mlkit --version + smlpkg --version + echo 'github.event_name: ' ${{ github.event_name }} + echo 'github.ref: ' ${{ github.ref }} + + - name: Configure With MLton + if: ${{ matrix.mlcomp == 'mlton' }} run: | ./autobuild ./configure + - name: Configure With MLKit + if: ${{ matrix.mlcomp == 'mlkit' }} + run: | + ./autobuild + ./configure --with-compiler=mlkit + - name: Build MLKit run: | make mlkit @@ -87,6 +127,7 @@ jobs: make -C test/parallelism all - name: Configure SmlToJs + if: ${{ matrix.mlcomp == 'mlton' }} run: | ./configure --with-compiler="SML_LIB=`pwd` `pwd`/bin/mlkit" diff --git a/Makefile.in b/Makefile.in index 5603cf8c6..ea4f561bb 100644 --- a/Makefile.in +++ b/Makefile.in @@ -43,6 +43,7 @@ CLEAN=rm -rf MLB *~ .\#* mlkit: $(MKDIR) bin $(MAKE) -C src mlkit + $(MAKE) -C src reml $(MAKE) man_mlkit .PHONY: smltojs @@ -56,6 +57,7 @@ all: mlkit mlkit_basislibs smltojs smltojs_basislibs .PHONY: mlkit_basislibs mlkit_basislibs: mlkit (cd basis && SML_LIB=.. ../bin/mlkit -c -no_gc basis.mlb) + (cd basis && SML_LIB=.. ../bin/mlkit -c -no_gc -par basis.mlb) (cd basis && SML_LIB=.. ../bin/mlkit -c -gc basis.mlb) (cd basis && SML_LIB=.. ../bin/mlkit -c -gc -prof basis.mlb) (cd basis && SML_LIB=.. ../bin/mlkit -c -no_gc -prof -Pcee -Prfg -Ppp -print_rho_types -log_to_file basis.mlb) @@ -197,6 +199,7 @@ install0: $(MKDIR) $(INSTDIR) $(MKDIR) $(BINDIR) $(INSTALL) bin/mlkit $(BINDIR) + $(INSTALL) bin/reml $(BINDIR) $(INSTALL) bin/mlkit-mllex $(BINDIR) $(INSTALL) bin/mlkit-mlyacc $(BINDIR) $(INSTALL) bin/rp2ps $(BINDIR) @@ -209,6 +212,7 @@ install0: $(MKDIR) $(MANDIR) $(MKDIR) $(MANDIR)/man1 $(INSTALLDATA) man/man1/mlkit.1 $(MANDIR)/man1 + $(INSTALLDATA) man/man1/reml.1 $(MANDIR)/man1 $(INSTALLDATA) man/man1/mlkit-mllex.1 $(MANDIR)/man1 $(INSTALLDATA) man/man1/mlkit-mlyacc.1 $(MANDIR)/man1 $(INSTALLDATA) man/man1/rp2ps.1 $(MANDIR)/man1 @@ -348,6 +352,7 @@ bootstrap: man_mlkit: $(MKDIR) man/man1 SML_LIB=$(exec_prefix)/lib/mlkit bin/mlkit -man > man/man1/mlkit.1 + SML_LIB=$(exec_prefix)/lib/reml bin/reml -man > man/man1/reml.1 .PHONY: man_smltojs man_smltojs: @@ -443,6 +448,7 @@ smltojs_x64_tgz: # $ ./autobuild # $ ./configure # $ make mlkit +# $ make reml # $ make mlkit_libs # $ make smltojs # $ make smltojs_basislibs diff --git a/basis/ForkJoin-reml.sml b/basis/ForkJoin-reml.sml new file mode 100644 index 000000000..16746bc6f --- /dev/null +++ b/basis/ForkJoin-reml.sml @@ -0,0 +1,78 @@ +structure ForkJoin :> FORK_JOIN = struct + +fun alloc (n:int) (v:'a) : 'a array = + prim ("word_table0", n) + +local + +fun alloc_unsafe (n:int) : 'a array = + prim ("word_table0", n) + +structure T = Thread + +fun for (lo,hi) (f:int->unit) : unit = + let fun loop i = + if i >= hi then () + else (f i; loop (i+1)) + in loop lo + end +in +fun parfor `e (X:int) (lo:int,hi:int) (f: int #e -> unit) : unit while noput e = + if lo >= hi then () + else let val m = lo+X + in if m >= hi (* last bucket *) + then for (lo,hi) f + else T.spawn (fn () => for (lo,m) f) + (fn _ => parfor X (m,hi) f) + end + +fun pmap `[e] (f:'a #e ->'b) : ('a list -> 'b list) while noput e = + fn (xs:'a list) => + let val v = Vector.fromList xs + val sz = Vector.length v + val a : 'b Array.array = alloc_unsafe sz + in parfor 1000 (0,sz) (fn i => Array.update(a,i,f(Vector.sub(v,i)))) + ; Array.foldr (op ::) nil a + end + +fun par `[e1 e2] (f: unit #e1 -> 'a, g: unit #e2 -> 'b) : 'a * 'b while e1 ## e2 = + let val a1 : 'a array = alloc_unsafe 1 + val b1 : 'b array = alloc_unsafe 1 + in T.spawn (fn () => Array.update(b1,0,g())) (fn _ => (Array.update(a1,0,f()))) + ; (Array.sub(a1,0), Array.sub(b1,0)) + end + +fun pair `[e1 e2] (f: 'a #e1 -> 'b, g: 'c #e2 -> 'd) (x:'a,y:'c) : 'b * 'd while e1 ## e2 = + par (fn () => f x, fn () => g y) + +type gcs = int * int (* max parallelism, min sequential work *) + +val rec parfor'__noinline `[e] : (int*int #e-> unit) -> gcs -> int*int -> unit while noput e = + fn doit => fn (P,G) => fn (lo,hi) => + if hi-lo <= 0 then () else + let val n = hi-lo + val m = Int.min(P+1, 1 + (n-1) div G) (* blocks *) + val k = n div m (* block size *) + val v = Vector.tabulate(m, fn i => + let val first = i*k + val next = first+k + in (first, + if next > hi then hi else next) + end) + fun loop n = + if n >= m-1 then doit (Vector.sub(v,n)) + else T.spawn (fn () => doit (Vector.sub(v,n))) + (fn _ => loop (n+1)) + in loop 0 + end + +val rec parfor' `[e] : gcs -> int*int -> (int #e -> unit) -> unit while noput e = + fn gcs => fn (lo,hi) => fn f => + let fun doit (lo,hi) = for (lo,hi) f + in parfor'__noinline doit gcs (lo,hi) + end + +val parfor' = parfor' + +end +end diff --git a/basis/Thread-reml.sml b/basis/Thread-reml.sml new file mode 100644 index 000000000..b66130991 --- /dev/null +++ b/basis/Thread-reml.sml @@ -0,0 +1,56 @@ +structure Thread :> THREAD = struct + type thread = foreignptr + type 'a t0 = ((unit->'a) * thread) ref + fun get__noinline ((ref (f,t0)): 'a t0) : 'a = prim("thread_get", t0) + fun spawn__noinline `[e1 e2] (f: unit #e1 -> 'a) (k: 'a t0 #e2 -> 'b) : 'b while e1 ## e2 = + let val rf : (unit -> 'a) ref = ref f + val fp_f : foreignptr = prim("pointer", !rf) + + (* From a region inference perspective, coercing the type of + * a function to a pointer type is very unsafe, as the + * pointer type contains no information about which regions + * need to be kept alive for the pointer value to be + * valid. By including the type of the function in the type + * of the thread value, however, we keep all necessary + * regions alive. + * + * Moreover, we encapsulate the function in a ref to avoid + * that the closure is inlined into the "pointer" prim + * argument. If it is inlined, the closure will be allocated + * in a local stack-allocated region inside the "pointer" + * prim value, which cause the program to segfault.. *) + + val t0 : thread = prim("spawnone", fp_f) + val t: 'a t0 = ref (f,t0) + + fun force () = + if !(ref true) (* make sure the thread has terminated before returning *) + then get__noinline t (* and mimic that, from a type perspective, spawn has *) + else !rf() (* the effect of calling f *) + + val res = k t handle e => (force(); raise e) + val _ = force () + + (* Notice that it is not safe to call `thread_free t0` here + * as t0 may be live through later calls to `get t`. + * + * What is needed is for the ThreadInfo structs to be region + * allocated and to add finalisers (thread_free) to objects + * in these regions. Technically, the thread is detached + * already in the thread_get function. However, the mutex + * and the ThreadInfo struct is kept live. + *) + in res + end + + type 'a t = 'a t0 + + fun spawn `[e1 e2] (f: unit #e1 ->'a) (k: 'a t #e2 -> 'b) : 'b while e1 ## e2 = + spawn__noinline f k + + fun get (x:'a t) : 'a = + get__noinline x + + fun numCores () : int = + prim("numCores",()) +end diff --git a/basis/par-reml.mlb b/basis/par-reml.mlb new file mode 100644 index 000000000..6e37684b4 --- /dev/null +++ b/basis/par-reml.mlb @@ -0,0 +1,10 @@ +local + basis.mlb +in + THREAD.sig + ThreadSeq.sml + Thread-reml.sml + FORK_JOIN.sig + ForkJoinSeq.sml + ForkJoin-reml.sml +end diff --git a/man/man1/.gitignore b/man/man1/.gitignore index 04baf4682..bd26af3d1 100644 --- a/man/man1/.gitignore +++ b/man/man1/.gitignore @@ -4,4 +4,5 @@ mlkit-mllex.1 mlkit-mlyacc.1 smltojs.1 mlkit.1 +reml.1 rp2ps.1 diff --git a/src/.gitignore b/src/.gitignore index be7b9f7e9..5397d4d6c 100644 --- a/src/.gitignore +++ b/src/.gitignore @@ -2,6 +2,7 @@ Makefile Version.sml config.h mlkit +reml smltojs smlserverc MLB diff --git a/src/Common/FLAGS.sig b/src/Common/FLAGS.sig index 39fdcd274..0317cc0db 100644 --- a/src/Common/FLAGS.sig +++ b/src/Common/FLAGS.sig @@ -99,15 +99,31 @@ signature FLAGS = item: 'a ref, desc: string} + type baentry = {long: string, (* long option for use with mlkit command + * using `--', script files, and internally + * in the mlkit to lookup the current setting + * during execution. *) + short: string option, (* short option used in commands with - *) + menu: string list, (* entry::path; nil means no-show*) + item: bool ref, (* the actual flag *) + on: unit->unit, (* function to apply to turn entry on *) + off: unit->unit, (* function to apply to turn entry off; + * a toggling function can be made from + * these two and the item. *) + desc: string} (* description string; format manually + * with new-lines *) + + (* Functions to add entries dynamically; remember to add a description * telling what the flag is used for. If a nil-menu is given, the * entry is not shown in help and the option cannot be given at the * command line. *) - val add_bool_entry : bentry -> (unit -> bool) - val add_string_entry : string entry -> (unit -> string) - val add_stringlist_entry : string list entry -> (unit -> string list) - val add_int_entry : int entry -> (unit -> int) + val add_bool_entry : bentry -> (unit -> bool) + val add_string_entry : string entry -> (unit -> string) + val add_stringlist_entry : string list entry -> (unit -> string list) + val add_int_entry : int entry -> (unit -> int) + val add_bool_action_entry : baentry -> (unit -> bool) (* Read and interpret option list by looking in directory and * the extra nullary list and unary list *) @@ -127,6 +143,13 @@ signature FLAGS = val getOptions : unit -> options list + (* Blocked entries are flag entries that do not show up in help + information and that cannot be altered by commandline. Blocking an + entry makes it possible to specialize man-pages and --help info for + ReML and SMLtoJs. It also guards against mis-configurations and some + non-supported combination of flags. *) + val block_entry : string -> unit + structure Statistics : sig val no_dangling_pointers_changes : int ref diff --git a/src/Common/Flags.sml b/src/Common/Flags.sml index f464439bb..a794ffe29 100644 --- a/src/Common/Flags.sml +++ b/src/Common/Flags.sml @@ -1,6 +1,6 @@ (* Global flags *) -structure Flags: FLAGS = +structure Flags : FLAGS = struct structure PP = PrettyPrint fun outLine (s) = print(s ^ "\n") @@ -16,18 +16,17 @@ structure Flags: FLAGS = (a) declare a new boolean reference, r (b) add r to the menu (with a menu text) at an appropriate place (c) add r to the `Adding initial entries' section below, together with - a search key (a string), which can be used by the modules that + a search key (a string), which can be used by the modules that want to access the flag. (d) recompile this functor and the functor which uses the new flag *) - fun has_sml_source_ext (s: string) :bool = - case s of - "sml" => true - | "sig" => true - | _ => false + case s of + "sml" => true + | "sig" => true + | _ => false val install_dir = ref "You_did_not_set_path_to_install_dir" @@ -44,7 +43,7 @@ structure Flags: FLAGS = (* Elimination of polymorphic equality *) val eliminate_polymorphic_equality = ref true - (* Region inference *) + (* Region inference *) val print_types = ref false val region_inference = ref true @@ -68,11 +67,8 @@ structure Flags: FLAGS = val colwidth = PrettyPrint.colwidth val log = ref TextIO.stdOut -(* - val indent_ccode = ref false; -*) - (* Program manager *) + (* Program manager *) fun dummy _ : unit = print "uninitialised function reference in Flags!" val comp_ref: (string -> unit)ref = ref dummy val current_source_file = ref "sources.pm" @@ -97,124 +93,107 @@ structure Flags: FLAGS = val warn_string = warn o Report.line fun report_warnings () = - (case !warnings of - [] => () - | reports => - (if !log_to_file then - print ("\n*** " ^ Int.toString (List.length reports) - ^ " warning" - ^ (case reports of [_] => "" | _ => "s") - ^ " printed on log file\n") - else (); - let val reports = rev reports - val report = Report.//(Report.line " *** Warnings ***", Report.flatten reports) - in Report.print' report (!log) - end)) + (case !warnings of + [] => () + | reports => + (if !log_to_file then + print ("\n*** " ^ Int.toString (List.length reports) + ^ " warning" + ^ (case reports of [_] => "" | _ => "s") + ^ " printed on log file\n") + else (); + let val reports = rev reports + val report = Report.//(Report.line " *** Warnings ***", Report.flatten reports) + in Report.print' report (!log) + end)) end (*local*) - - (* ----------------------------------- - * Parse functions - * ----------------------------------- *) - - type ('a, 'b) reader = ('a, 'b) StringCvt.reader - - fun scan_string getc cs = - let fun loop (cs, acc) = - case getc cs - of SOME(#"\"", cs) => SOME(implode(rev acc),cs) - | SOME(c,cs) => loop(cs,c::acc) - | NONE => NONE - in case getc (StringCvt.skipWS getc cs) - of SOME(#"\"", cs) => loop(cs, []) - | _ => NONE - end - - fun getc [] = NONE - | getc (c::cs) = SOME(c,cs) - - (**************************************************) (* structure Directory *) (* *) (* Directory, holding associations for *) - (* various settings and operations for toggling, *) - (* etc. Also, readScript is here. *) + (* various settings and operations for toggling, *) + (* etc. *) (**************************************************) type bentry = {long: string, (* long option for use with mlkit command - * using `--', script files, and internally - * in the mlkit to lookup the current setting - * during execution. *) - short: string option, (* short option used in commands with - *) - menu: string list, (* entry::path; nil means no-show*) - item: bool ref, (* the actual flag *) - neg: bool, (* should negated flags be introduced? - * -no_opt, --no_optimiser *) - desc: string} (* description string; format manually - * with new-lines *) + * using `--', script files, and internally + * in the mlkit to lookup the current setting + * during execution. *) + short: string option, (* short option used in commands with - *) + menu: string list, (* entry::path; nil means no-show*) + item: bool ref, (* the actual flag *) + neg: bool, (* should negated flags be introduced? + * -no_opt, --no_optimiser *) + desc: string} (* description string; format manually + * with new-lines *) type baentry = {long: string, (* long option for use with mlkit command - * using `--', script files, and internally - * in the mlkit to lookup the current setting - * during execution. *) - short: string option, (* short option used in commands with - *) - menu: string list, (* entry::path; nil means no-show*) - item: bool ref, (* the actual flag *) - on: unit->unit, (* function to apply to turn entry on *) - off: unit->unit, (* function to apply to turn entry off; - * a toggling function can be made from - * these two and the item. *) - desc: string} (* description string; format manually - * with new-lines *) + * using `--', script files, and internally + * in the mlkit to lookup the current setting + * during execution. *) + short: string option, (* short option used in commands with - *) + menu: string list, (* entry::path; nil means no-show*) + item: bool ref, (* the actual flag *) + on: unit->unit, (* function to apply to turn entry on *) + off: unit->unit, (* function to apply to turn entry off; + * a toggling function can be made from + * these two and the item. *) + desc: string} (* description string; format manually + * with new-lines *) type 'a entry = {long: string, - short: string option, - menu: string list, - item: 'a ref, - desc: string} + short: string option, + menu: string list, + item: 'a ref, + desc: string} structure Directory : sig - val bool_entry : bentry -> (unit -> bool) - val string_entry : string entry -> (unit -> string) - val stringlist_entry : string list entry -> (unit -> string list) - val int_entry : int entry -> (unit -> int) - val bool_action_entry : baentry -> unit - - val is_on : string -> bool - val is_on0 : string -> unit -> bool - val turn_on : string -> unit - val turn_off : string -> unit - val add_string_entry : string * string ref -> (unit -> string) - val add_stringlist_entry: string * string list ref -> (unit -> string list) - val add_int_entry : string * int ref -> (unit -> int) - val add_bool_entry : string * bool ref -> (unit -> bool) - val get_string_entry : string -> string - val get_stringlist_entry: string -> string list - val lookup_stringlist_entry : string -> string list ref - val lookup_string_entry : string -> string ref - val lookup_flag_entry : string -> bool ref - val lookup_int_entry : string -> int ref - - (* read and interpret option list by looking in directory and - * the extra nullary list and unary list *) - val read_options : {nullary:(string*(unit->unit))list, - unary:(string*(string->unit))list, - options: string list} -> string list - - (* help key provides help information for the key *) - val help : string -> string - - (* help_all() provides help on all options in the directory *) - val help_all : unit -> string - val getOptions : unit -> + val bool_entry : bentry -> (unit -> bool) + val string_entry : string entry -> (unit -> string) + val stringlist_entry : string list entry -> (unit -> string list) + val int_entry : int entry -> (unit -> int) + val bool_action_entry : baentry -> (unit -> bool) + val is_on : string -> bool + val is_on0 : string -> unit -> bool + val turn_on : string -> unit + val turn_off : string -> unit + val add_string_entry : string * string ref -> (unit -> string) + val add_stringlist_entry: string * string list ref -> (unit -> string list) + val add_int_entry : string * int ref -> (unit -> int) + val add_bool_entry : string * bool ref -> (unit -> bool) + val get_string_entry : string -> string + val get_stringlist_entry: string -> string list + val lookup_stringlist_entry : string -> string list ref + val lookup_string_entry : string -> string ref + val lookup_flag_entry : string -> bool ref + val lookup_int_entry : string -> int ref + + (* read and interpret option list by looking in directory and + * the extra nullary list and unary list *) + val read_options : {nullary:(string*(unit->unit))list, + unary:(string*(string->unit))list, + options: string list} -> string list + + (* help key provides help information for the key *) + val help : string -> string + + (* help_all() provides help on all options in the directory *) + val help_all : unit -> string + val getOptions : unit -> {desc : string, long : string list, short : string list, kind : string option, default : string option} list - end = + val block_entry : string -> unit + val is_blocked : string -> bool + end = struct + val blocked_entries = ref nil + fun block_entry (e:string) = blocked_entries := e :: (!blocked_entries) + fun is_blocked e = List.exists (fn e' => e=e') (!blocked_entries) + datatype entry0 = INT_ENTRY of int entry | BOOL_ENTRY of bentry | BOOLA_ENTRY of baentry (* action entry *) @@ -227,79 +206,80 @@ struct fun bool_entry (e:bentry) : unit -> bool = case M.lookup (!dir) (#long e) - of SOME _ => die ("bool_entry: entry " ^ (#long e) ^ " already in directory") - | NONE => (dir := M.add(#long e, BOOL_ENTRY e, - case #short e of - SOME s => M.add(s, BOOL_ENTRY e, !dir) - | NONE => !dir); - let val r = #item e - in fn () => !r - end) - - fun bool_action_entry (e:baentry) : unit = + of SOME _ => die ("bool_entry: entry " ^ (#long e) ^ " already in directory") + | NONE => (dir := M.add(#long e, BOOL_ENTRY e, + case #short e of + SOME s => M.add(s, BOOL_ENTRY e, !dir) + | NONE => !dir); + let val r = #item e + in fn () => !r + end) + + fun bool_action_entry (e:baentry) : unit -> bool = case M.lookup (!dir) (#long e) - of SOME _ => die ("bool_action_entry: entry " ^ (#long e) ^ " already in directory") - | NONE => dir := M.add(#long e, BOOLA_ENTRY e, - case #short e - of SOME s => M.add(s, BOOLA_ENTRY e, !dir) - | NONE => !dir) + of SOME _ => die ("bool_action_entry: entry " ^ (#long e) ^ " already in directory") + | NONE => ( dir := M.add(#long e, BOOLA_ENTRY e, + case #short e + of SOME s => M.add(s, BOOLA_ENTRY e, !dir) + | NONE => !dir) + ; fn () => !(#item e)) fun string_entry (e:string entry) : unit -> string = case M.lookup (!dir) (#long e) - of SOME _ => die ("string_entry: entry " ^ (#long e) ^ " already in directory") - | NONE => (dir := M.add(#long e, STRING_ENTRY e, - case #short e of - SOME s => M.add(s, STRING_ENTRY e, !dir) - | NONE => !dir); - let val r = #item e - in fn () => !r - end) + of SOME _ => die ("string_entry: entry " ^ (#long e) ^ " already in directory") + | NONE => (dir := M.add(#long e, STRING_ENTRY e, + case #short e of + SOME s => M.add(s, STRING_ENTRY e, !dir) + | NONE => !dir); + let val r = #item e + in fn () => !r + end) fun stringlist_entry (e:string list entry) : unit -> string list = case M.lookup (!dir) (#long e) - of SOME _ => die ("stringlist_entry: entry " ^ (#long e) ^ " already in directory") - | NONE => (dir := M.add(#long e, STRINGLIST_ENTRY e, - case #short e of - SOME s => M.add(s, STRINGLIST_ENTRY e, !dir) - | NONE => !dir); - let val r = #item e - in fn () => !r - end) + of SOME _ => die ("stringlist_entry: entry " ^ (#long e) ^ " already in directory") + | NONE => (dir := M.add(#long e, STRINGLIST_ENTRY e, + case #short e of + SOME s => M.add(s, STRINGLIST_ENTRY e, !dir) + | NONE => !dir); + let val r = #item e + in fn () => !r + end) fun int_entry (e:int entry) : unit -> int = case M.lookup (!dir) (#long e) - of SOME _ => die ("int_entry: entry " ^ (#long e) ^ " already in directory") - | NONE => (dir := M.add(#long e, INT_ENTRY e, - case #short e of - SOME s => M.add(s, INT_ENTRY e, !dir) - | NONE => !dir); - let val r = #item e - in fn () => !r - end) + of SOME _ => die ("int_entry: entry " ^ (#long e) ^ " already in directory") + | NONE => (dir := M.add(#long e, INT_ENTRY e, + case #short e of + SOME s => M.add(s, INT_ENTRY e, !dir) + | NONE => !dir); + let val r = #item e + in fn () => !r + end) fun lookup_flag_entry (key) : bool ref = case M.lookup (!dir) key - of SOME (BOOL_ENTRY e) => #item e - | SOME _ => die ("lookup_flag_entry: entry " ^ key ^ " is of wrong kind") - | NONE => die ("lookup_flag_entry: no entry " ^ key ^ " in directory") + of SOME (BOOL_ENTRY e) => #item e + | SOME _ => die ("lookup_flag_entry: entry " ^ key ^ " is of wrong kind") + | NONE => die ("lookup_flag_entry: no entry " ^ key ^ " in directory") fun lookup_string_entry (key) : string ref = case M.lookup (!dir) key - of SOME (STRING_ENTRY e) => #item e - | SOME _ => die ("lookup_string_entry: entry " ^ key ^ " is of wrong kind") - | NONE => die ("lookup_string_entry: no entry " ^ key ^ " in directory") + of SOME (STRING_ENTRY e) => #item e + | SOME _ => die ("lookup_string_entry: entry " ^ key ^ " is of wrong kind") + | NONE => die ("lookup_string_entry: no entry " ^ key ^ " in directory") fun lookup_stringlist_entry (key) : string list ref = case M.lookup (!dir) key - of SOME (STRINGLIST_ENTRY e) => #item e - | SOME _ => die ("lookup_stringlist_entry: entry " ^ key ^ " is of wrong kind") - | NONE => die ("lookup_stringlist_entry: no entry " ^ key ^ " in directory") + of SOME (STRINGLIST_ENTRY e) => #item e + | SOME _ => die ("lookup_stringlist_entry: entry " ^ key ^ " is of wrong kind") + | NONE => die ("lookup_stringlist_entry: no entry " ^ key ^ " in directory") fun lookup_int_entry (key) : int ref = case M.lookup (!dir) key - of SOME (INT_ENTRY e) => #item e - | SOME _ => die ("lookup_int_entry: entry " ^ key ^ " is of wrong kind") - | NONE => die ("lookup_int_entry: no entry " ^ key ^ " in directory") + of SOME (INT_ENTRY e) => #item e + | SOME _ => die ("lookup_int_entry: entry " ^ key ^ " is of wrong kind") + | NONE => die ("lookup_int_entry: no entry " ^ key ^ " in directory") val get_string_entry = ! o lookup_string_entry @@ -342,97 +322,105 @@ struct fun lookup_notnull_menu dir key = let fun ok (BOOL_ENTRY{menu=nil,...}) = false - | ok (BOOLA_ENTRY{menu=nil,...}) = false - | ok (STRING_ENTRY{menu=nil,...}) = false - | ok (INT_ENTRY{menu=nil,...}) = false - | ok _ = true + | ok (BOOLA_ENTRY{menu=nil,...}) = false + | ok (STRING_ENTRY{menu=nil,...}) = false + | ok (INT_ENTRY{menu=nil,...}) = false + | ok _ = true in case M.lookup dir key - of r as SOME e => if ok e then r - else NONE - | NONE => NONE + of r as SOME e => if ok e then r + else NONE + | NONE => NONE end (* read and interpret option list by looking in directory and * the extra nullary list and unary list *) fun opt s = case explode s - of #"-":: #"-"::rest => SOME (implode rest) - | #"-"::rest => SOME (implode rest) - | _ => NONE + of #"-":: #"-"::rest => SOME (implode rest) + | #"-"::rest => SOME (implode rest) + | _ => NONE fun negation s = case explode s - of #"n":: #"o":: #"_"::rest => SOME (implode rest) - | _ => NONE + of #"n":: #"o":: #"_"::rest => SOME (implode rest) + | _ => NONE fun lookup_key key (l:(string *('a->unit))list) : ('a -> unit) option = let fun look nil = NONE - | look ((x,f)::rest) = if key=x then SOME f else look rest + | look ((x,f)::rest) = if key=x then SOME f else look rest in look l end + fun check_blocked k = + if is_blocked k then raise Fail "Sorry, the option is blocked" + else () + fun read_options {nullary:(string*(unit->unit))list, - unary:(string*(string->unit))list, - options: string list} : string list = + unary:(string*(string->unit))list, + options: string list} : string list = let fun loop nil = nil - | loop (all as s::ss) = - case opt s - of SOME key => - (case negation key - of SOME no_key => - (case lookup_notnull_menu (!dir) no_key - of SOME (BOOL_ENTRY e) => - if #neg e then (#item e := false; loop ss) - else raise Fail ("negation not allowed on option: " ^ no_key) - | SOME (BOOLA_ENTRY e) => (#off e (); loop ss) - | SOME _ => raise Fail ("negation not allowed on option: " ^ no_key) - | NONE => raise Fail ("unknown option: " ^ s)) - | NONE => - (case lookup_notnull_menu (!dir) key - of SOME (BOOL_ENTRY e) => (#item e := true; loop ss) - | SOME (BOOLA_ENTRY e) => (#on e (); loop ss) - | SOME (STRING_ENTRY e) => - (case ss - of s::ss => (#item e := s; loop ss) - | _ => raise Fail ("missing argument to " ^ s)) - | SOME (STRINGLIST_ENTRY e) => - let fun is_opt s = (String.sub(s,0) = #"-") handle _ => false - fun readToOpt (all as [s],acc) = - if is_opt s then (rev acc, all) - else (case OS.Path.ext s of - SOME ext => if has_sml_source_ext ext then (rev acc, all) - else (rev (s::acc),nil) - | _ => (rev (s::acc),nil)) - | readToOpt (all as s::ss,acc) = - if is_opt s then (rev acc,all) - else readToOpt(ss,s::acc) - | readToOpt (nil,acc) = (rev acc,nil) - val (args,rest) = readToOpt (ss,nil) - in (#item e := args; loop rest) - end - | SOME (INT_ENTRY e) => - (case ss - of s::ss => - (case Int.fromString s - of SOME i => (#item e := i; loop ss) - | NONE => raise Fail ("expecting integer argument to " ^ s)) - | _ => raise Fail ("missing argument to " ^ s)) - | NONE => - let - fun try_nullary exn = - case lookup_key key nullary - of SOME f => (f(); loop ss) - | NONE => raise exn - in case lookup_key key unary - of SOME f => - (case ss - of s::ss => (f s; loop ss) - | nil => try_nullary (Fail("missing argument to " ^ s))) - | NONE => try_nullary (Fail("unknown option: " ^ s)) - end)) - | NONE => all + | loop (all as s::ss) = + case opt s + of SOME key => + (case negation key + of SOME no_key => + (case lookup_notnull_menu (!dir) no_key of + SOME (BOOL_ENTRY e) => + (check_blocked (#long e); + if #neg e then (#item e := false; loop ss) + else raise Fail ("negation not allowed on option: " ^ no_key)) + | SOME (BOOLA_ENTRY e) => (check_blocked (#long e); #off e (); loop ss) + | SOME _ => raise Fail ("negation not allowed on option: " ^ no_key) + | NONE => raise Fail ("unknown option: " ^ s)) + | NONE => + (case lookup_notnull_menu (!dir) key of + SOME (BOOL_ENTRY e) => (check_blocked (#long e); #item e := true; loop ss) + | SOME (BOOLA_ENTRY e) => (check_blocked (#long e); #on e (); loop ss) + | SOME (STRING_ENTRY e) => + (check_blocked (#long e); + case ss of + s::ss => (#item e := s; loop ss) + | _ => raise Fail ("missing argument to " ^ s)) + | SOME (STRINGLIST_ENTRY e) => + let fun is_opt s = (String.sub(s,0) = #"-") handle _ => false + fun readToOpt (all as [s],acc) = + if is_opt s then (rev acc, all) + else (case OS.Path.ext s of + SOME ext => if has_sml_source_ext ext then (rev acc, all) + else (rev (s::acc),nil) + | _ => (rev (s::acc),nil)) + | readToOpt (all as s::ss,acc) = + if is_opt s then (rev acc,all) + else readToOpt(ss,s::acc) + | readToOpt (nil,acc) = (rev acc,nil) + val () = check_blocked (#long e) + val (args,rest) = readToOpt (ss,nil) + in (#item e := args; loop rest) + end + | SOME (INT_ENTRY e) => + (check_blocked (#long e); + case ss of + s::ss => + (case Int.fromString s of + SOME i => (#item e := i; loop ss) + | NONE => raise Fail ("expecting integer argument to " ^ s)) + | _ => raise Fail ("missing argument to " ^ s)) + | NONE => + let + fun try_nullary exn = + case lookup_key key nullary + of SOME f => (f(); loop ss) + | NONE => raise exn + in case lookup_key key unary + of SOME f => + (case ss + of s::ss => (f s; loop ss) + | nil => try_nullary (Fail("missing argument to " ^ s))) + | NONE => try_nullary (Fail("unknown option: " ^ s)) + end)) + | NONE => all in loop options end @@ -440,48 +428,47 @@ struct (* help key provides help information for the key *) fun help' (key: string) = - let - fun optToList NONE = [] - | optToList (SOME a) = [a] - - fun bitem true = "on" - | bitem false = "off" - fun opt (SOME s) = ", -" ^ s - | opt NONE = "" - - fun negationNew (e:bentry, kind) = - if not(#neg e) then [] - else [{long = ["no_" ^ (#long e)], short = map (fn x => "no_" ^ x) (optToList (#short e)), - kind = kind, default = NONE, desc = "Opposite of --" ^ #long e ^ opt(#short e) ^ "."}] - - fun negationNew' (e:baentry, kind) = - [{long = ["no_" ^ (#long e)], short = map (fn x => "no_" ^ x) (optToList (#short e)), - kind = kind, default = NONE, desc = "Opposite of --" ^ #long e ^ opt(#short e) ^ "."}] - - in - (case lookup_notnull_menu (!dir) key - of SOME (BOOL_ENTRY e) => - {long = [#long e], short = optToList (#short e), kind = NONE, - default = SOME (bitem (!(#item e))), desc = #desc e} :: - (negationNew (e,NONE)) - | SOME (BOOLA_ENTRY e) => - {long = [#long e], short = optToList (#short e), default = SOME (bitem (!(#item e))), - desc = #desc e, kind = NONE} :: - negationNew' (e,NONE) - | SOME (STRING_ENTRY e) => - {long = [#long e], short = optToList (#short e), - default = let val a = (String.toString(!(#item e))) - in if a = "" then NONE else SOME a - end, - desc = #desc e, kind = SOME "S"} :: [] - | SOME (STRINGLIST_ENTRY e) => - {long = [#long e], short = optToList (#short e), default = NONE, - desc = #desc e, kind = SOME "S"} :: [] - | SOME (INT_ENTRY e) => - {long = [#long e], short = optToList (#short e), default = SOME (Int.toString (!(#item e))), - desc = #desc e, kind = SOME "N"} :: [] - | NONE => raise Fail ("no help available for option: " ^ key)) - end + let fun optToList NONE = [] + | optToList (SOME a) = [a] + + fun bitem true = "on" + | bitem false = "off" + fun opt (SOME s) = ", -" ^ s + | opt NONE = "" + + fun negationNew (e:bentry, kind) = + if not(#neg e) then [] + else [{long = ["no_" ^ (#long e)], short = map (fn x => "no_" ^ x) (optToList (#short e)), + kind = kind, default = NONE, desc = "Opposite of --" ^ #long e ^ opt(#short e) ^ "."}] + + fun negationNew' (e:baentry, kind) = + [{long = ["no_" ^ (#long e)], short = map (fn x => "no_" ^ x) (optToList (#short e)), + kind = kind, default = NONE, desc = "Opposite of --" ^ #long e ^ opt(#short e) ^ "."}] + + in + case lookup_notnull_menu (!dir) key of + SOME (BOOL_ENTRY e) => + {long = [#long e], short = optToList (#short e), kind = NONE, + default = SOME (bitem (!(#item e))), desc = #desc e} :: + (negationNew (e,NONE)) + | SOME (BOOLA_ENTRY e) => + {long = [#long e], short = optToList (#short e), default = SOME (bitem (!(#item e))), + desc = #desc e, kind = NONE} :: + negationNew' (e,NONE) + | SOME (STRING_ENTRY e) => + {long = [#long e], short = optToList (#short e), + default = let val a = (String.toString(!(#item e))) + in if a = "" then NONE else SOME a + end, + desc = #desc e, kind = SOME "S"} :: [] + | SOME (STRINGLIST_ENTRY e) => + {long = [#long e], short = optToList (#short e), default = NONE, + desc = #desc e, kind = SOME "S"} :: [] + | SOME (INT_ENTRY e) => + {long = [#long e], short = optToList (#short e), default = SOME (Int.toString (!(#item e))), + desc = #desc e, kind = SOME "N"} :: [] + | NONE => raise Fail ("no help available for option: " ^ key) + end fun print_help tail x = let @@ -511,84 +498,67 @@ struct in String.concat (List.map p x) end - fun help x = print_help "" (help' x) + fun help x = print_help "" (help' x) (* help_all() provides help on all options in the directory *) fun help_all' () = - let val dom = rev(M.dom (!dir)) - fun add (key, acc) = - let (* add only if menu is non-empty and - * the entry is not a short key *) - fun check (SOME k) = if k = key then acc - else (help' key) @ acc - | check NONE = (help' key) @ acc - in - case lookup_notnull_menu (!dir) key - of SOME (INT_ENTRY e) => check(#short e) - | SOME (BOOL_ENTRY e) => check(#short e) - | SOME (BOOLA_ENTRY e) => check(#short e) - | SOME (STRING_ENTRY e) => check(#short e) - | SOME (STRINGLIST_ENTRY e) => check(#short e) - | NONE => acc - end - fun cmp c ([],[]) = EQUAL - | cmp c ([],_) = LESS - | cmp c (_,[]) = GREATER - | cmp c (x::xs,y::ys) = case c (x,y) - of EQUAL => cmp c (xs,ys) - | GREATER => GREATER - | LESS => LESS - in Listsort.sort - (fn ({long = l1,...},{long = l2,...}) => cmp String.compare (l1,l2)) - (foldl add [] dom) - end + let val dom = rev(M.dom (!dir)) + fun add (key, acc) = + let (* add only if (1) menu is non-empty and + * (2) the entry is not a short key and (3) entry is not blocked *) + fun check (SOME k) l = + if k = key orelse is_blocked l then acc + else (help' key) @ acc + | check NONE l = + if is_blocked l then acc else (help' key) @ acc + in + case lookup_notnull_menu (!dir) key + of SOME (INT_ENTRY e) => check(#short e)(#long e) + | SOME (BOOL_ENTRY e) => check(#short e)(#long e) + | SOME (BOOLA_ENTRY e) => check(#short e)(#long e) + | SOME (STRING_ENTRY e) => check(#short e)(#long e) + | SOME (STRINGLIST_ENTRY e) => check(#short e)(#long e) + | NONE => acc + end + fun cmp c ([],[]) = EQUAL + | cmp c ([],_) = LESS + | cmp c (_,[]) = GREATER + | cmp c (x::xs,y::ys) = case c (x,y) + of EQUAL => cmp c (xs,ys) + | GREATER => GREATER + | LESS => LESS + in Listsort.sort + (fn ({long = l1,...},{long = l2,...}) => cmp String.compare (l1,l2)) + (foldl add [] dom) + end fun help_all () = print_help "\n" (help_all' ()) val getOptions = help_all' end (* Directory *) -(**structure Menu = Menu(val help_topic = Directory.help)**) - fun add_bool_entry e = - case #menu e - of nil => Directory.bool_entry e - | path => ((**Menu.add_flag_to_menu(#long e, path, #item e); **) - Directory.bool_entry e) + Directory.bool_entry e fun add_string_entry e = - case #menu e - of nil => Directory.string_entry e - | path => ((**Menu.add_string_to_menu(#long e, path, #item e);**) - Directory.string_entry e) + Directory.string_entry e fun add_stringlist_entry e = - case #menu e of - nil => Directory.stringlist_entry e - | path => ( (* Menu.add_string_to_menu(#long e, path, #item e); *) - Directory.stringlist_entry e) + Directory.stringlist_entry e fun add_int_entry e = - case #menu e - of nil => Directory.int_entry e - | path => ((**Menu.add_int_to_menu(#long e, path, #item e);**) - Directory.int_entry e) + Directory.int_entry e fun add_bool_entry0 (l,i) = - add_bool_entry {long=l,short=NONE,neg=false,menu=nil,item=i,desc=""} + add_bool_entry {long=l,short=NONE,neg=false,menu=nil,item=i,desc=""} fun add_string_entry0 (l,i) = - add_string_entry {long=l,short=NONE,menu=nil,item=i,desc=""} + add_string_entry {long=l,short=NONE,menu=nil,item=i,desc=""} fun add_bool_action_entry e = - let fun toggle true = (#off e)() - | toggle false = (#on e)() - in - case #menu e - of nil => Directory.bool_action_entry e - | path => ((**Menu.add_bool_action_to_menu(#long e, path, toggle, fn() => !(#item e));**) - Directory.bool_action_entry e) - end + Directory.bool_action_entry e + +val block_entry = Directory.block_entry (*********************************) (* Construction of the Kit Menu *) @@ -599,18 +569,18 @@ fun add_bool_action_entry e = local fun add (l, sh, s, r, desc) : unit = (add_bool_entry {long=l, short=sh, menu=["Printing of intermediate forms",s], - item=r, neg=false, desc=desc}; + item=r, neg=false, desc=desc}; ()) in val _ = add ("print_opt_lambda_expression", SOME "Pole", "print optimised lambda expression", - print_opt_lambda_expression, "Print Lambda Expression after optimisation.") + print_opt_lambda_expression, "Print Lambda Expression after optimisation.") end (*2. Layout*) local fun add neg (l, sh, s, r, desc) : unit = (add_bool_entry {long=l, short=sh, menu=["Layout",s], - item=r, neg=neg, desc=desc}; ()) + item=r, neg=neg, desc=desc}; ()) in val _ = app (add false) [ @@ -620,84 +590,87 @@ in \Region Expressions, region types are printed.") ] val _ = add true - ("raggedRight", NONE, "ragged right margin in pretty-printing", raggedRight, - "Use ragged right margin in pretty-printing of\n\ - \expressions and types.") + ("raggedRight", NONE, "ragged right margin in pretty-printing", raggedRight, + "Use ragged right margin in pretty-printing of\n\ + \expressions and types.") end val _ = add_int_entry {long="width",short=SOME "w", menu=["Layout", "text width in pretty-printing"], - item=colwidth, - desc="Column width used when pretty printing intermediate code."} + item=colwidth, + desc="Column width used when pretty printing intermediate code."} (*3. Control*) val recompile_basislib = ref false val _ = add_bool_entry {long="recompile_basislib",short=SOME "scratch", - menu=["Control", "recompile basis library"], - item=recompile_basislib,neg=false, - desc= - "Recompile basis library from scratch. This option\n\ - \is useful together with other options that control\n\ - \code generation."} + menu=["Control", "recompile basis library"], + item=recompile_basislib,neg=false, + desc= + "Recompile basis library from scratch. This option\n\ + \is useful together with other options that control\n\ + \code generation."} val preserve_tail_calls = ref false val _ = add_bool_entry {long="preserve_tail_calls", short=SOME"ptc", item=preserve_tail_calls, - menu=["Control", "preserve tail calls"], neg=true, - desc= - "Avoid the wrapping of letregion constructs around\n\ - \tail calls. Turning on garbage collection\n\ - \automatically turns on this option."} + menu=["Control", "preserve tail calls"], neg=true, + desc= + "Avoid the wrapping of letregion constructs around\n\ + \tail calls. Turning on garbage collection\n\ + \automatically turns on this option."} val dangling_pointers = ref true val _ = add_bool_entry {long="dangling_pointers", short=SOME"dangle", item=dangling_pointers, - menu=["Control", "dangling pointers"], neg=true, - desc= - "When this option is disabled, dangling pointers\n\ - \are avoided by forcing values captured in\n\ - \closures to live at-least as long as the closure\n\ - \itself. So as to make garbage collection sound,\n\ - \this option is disabled by default when garbage\n\ - \collection is enabled."} + menu=["Control", "dangling pointers"], neg=true, + desc= + "When this option is disabled, dangling pointers\n\ + \are avoided by forcing values captured in\n\ + \closures to live at-least as long as the closure\n\ + \itself. So as to make garbage collection sound,\n\ + \this option is disabled by default when garbage\n\ + \collection is enabled."} val tag_values = ref false val _ = add_bool_entry {long="tag_values", short=SOME"tag", item=tag_values, - menu=["Control", "tag values"], neg=false, - desc= - "Enable tagging of values as used when garbage\n\ - \collection is enabled for implementing pointer\n\ - \traversal."} + menu=["Control", "tag values"], neg=false, + desc= + "Enable tagging of values as used when garbage\n\ + \collection is enabled for implementing pointer\n\ + \traversal."} val _ = add_bool_entry {long="tag_pairs", short=NONE, item=ref false, - menu=["Control", "tag pairs"], neg=false, - desc= - "Use a tagged representation of pairs for garbage\n\ - \collection. Garbage collection works fine with a\n\ - \tag-free representation of pairs, so this option\n\ - \is here for measurement purposes."} + menu=["Control", "tag pairs"], neg=false, + desc= + "Use a tagged representation of pairs for garbage\n\ + \collection. Garbage collection works fine with a\n\ + \tag-free representation of pairs, so this option\n\ + \is here for measurement purposes."} val _ = add_bool_entry {long="values_64bit", short=NONE, item=ref true, - menu=["Control", "values 64bit"], neg=false, - desc= - "Support 64-bit values. Should be enabled for \n\ + menu=["Control", "values 64bit"], neg=false, + desc= + "Support 64-bit values. Should be enabled for \n\ \backends supporting 64-bit integers and words."} local val gc = ref false val gengc = ref false - fun off() = (gc := false; - preserve_tail_calls := false; - dangling_pointers := true; - Directory.turn_on "aggresive_opt"; - tag_values := false) - fun on() = (gc := true; - preserve_tail_calls := true; - dangling_pointers := false; - Directory.turn_on "aggresive_opt"; - tag_values := true) - fun off_gengc() = (off(); (* We also turn gc off *) - gengc := false) - fun on_gengc() = (on(); (* Gen GC needs gc to be turned on as well *) - gengc := true) + fun off () = (gc := false; + preserve_tail_calls := false; + dangling_pointers := true; + Directory.turn_on "aggresive_opt"; + tag_values := false) + fun on () = + if Directory.is_on "reml" then + raise Fail "ReML does not support garbage collection" + else (gc := true; + preserve_tail_calls := true; + dangling_pointers := false; + Directory.turn_on "aggresive_opt"; + tag_values := true) + fun off_gengc () = (off(); (* We also turn gc off *) + gengc := false) + fun on_gengc () = (on(); (* Gen GC needs gc to be turned on as well *) + gengc := true) in val _ = add_bool_action_entry {long="garbage_collection", menu=["Control", "garbage collection"], @@ -723,19 +696,10 @@ end local fun add neg (l, sh, s, r, desc) : unit = (add_bool_entry {long=l, short=sh, menu=["Control",s], - item=r, neg=neg, desc=desc}; ()) + item=r, neg=neg, desc=desc}; ()) in val _ = app (add false) [ -(* - ("all_multiplicities_infinite", NONE, "all multiplicities infinite (for POPL 96)", - all_multiplicities_infinite, - "Use only infinite regions. That is, store all values in\n\ - \infinite regions, which do not reside on the stack, but\n\ - \in the heap. With this flag disabled, all regions that\n\ - \can be inferred that values are allocated in them at\n\ - \most once are allocated on the stack."), -*) ("report_file_sig", SOME "sig", "report signatures", ref false, "Report signatures for each file read."), ("quotation", SOME "quot", "quotation support", ref false, @@ -769,13 +733,6 @@ in \as a repository.") end -(* -val _ = app (fn (s, f) => Menu.add_action_to_menu ("", ["Control", s], f)) - [ - ("print entire menu", Menu.show_full_menu) - ] -*) - (*4. File menu*) val _ = add_bool_entry @@ -797,7 +754,7 @@ val _ = add_string_entry local fun add neg (l, sh, s, r, desc) = (add_bool_entry {long=l, short=sh, menu=["Profiling",s], - item=r, neg=neg, desc=desc}; ()) + item=r, neg=neg, desc=desc}; ()) in val _ = app (add false) [ @@ -818,16 +775,11 @@ in \inference expressions.")] end -(**val _ = Menu.add_int_list_to_menu ("", ["Profiling", "print program points"], program_points)**) -(* -val _ = Menu.add_int_pair_list_to_menu ("", ["Profiling", "paths between two nodes in region flow graph"], region_paths) -*) - (*6. Debug Kit*) local fun add p n (l,sh,s,r,d) : unit = (add_bool_entry {long=l, short=sh, menu=p @[s], - item=r, neg=n, desc=d}; ()) + item=r, neg=n, desc=d}; ()) in val _ = app (add ["Debug", "Lambda"] true) [ @@ -863,11 +815,6 @@ end (*Entries not included in command-line options, but in lookup functions*) -(* - val _ = add_string_entry0 ("c_compiler", c_compiler) - (*e.g. "cc -Aa" or "gcc -ansi"*) -*) - val _ = add_bool_entry0 ("enhanced_atbot_analysis", enhanced_atbot_analysis) val _ = add_bool_entry0 ("eliminate_polymorphic_equality", eliminate_polymorphic_equality) @@ -905,12 +852,10 @@ structure Statistics = val no_dangling_pointers_changes = ref 0 val no_dangling_pointers_changes_total = ref 0 fun reset() = (no_dangling_pointers_changes := 0; - no_dangling_pointers_changes_total := 0) + no_dangling_pointers_changes_total := 0) end -end (* functor Flags *) - - +end (* structure Flags *) structure profRegInf = struct diff --git a/src/Common/KitCompiler.sml b/src/Common/KitCompiler.sml index 43de2e615..3b953e4b8 100644 --- a/src/Common/KitCompiler.sml +++ b/src/Common/KitCompiler.sml @@ -14,13 +14,16 @@ functor KitCompiler(Execution : EXECUTION) : KIT_COMPILER = struct open Execution - - fun cmd_name() = OS.Path.file(CommandLine.name()) + fun cmd_name () = OS.Path.file(CommandLine.name()) structure ManagerObjects = ManagerObjects(struct structure Execution = Execution - val program_name = cmd_name + fun program_name () = + let val n = cmd_name() + in if n = "reml" then "mlkit" + else n + end (* read info from mlkit's mlb-path-map file *) end) structure ModCodeMini = struct @@ -57,8 +60,10 @@ functor KitCompiler(Execution : EXECUTION) : KIT_COMPILER = let val version = Version.version ^ " (" ^ Version.gitversion ^ " - " ^ date ^ ")" val msg = if backend_name = "SmlToJs" then "SmlToJs " ^ version ^ "\n" - else ("MLKit " ^ version ^ " [" - ^ backend_name ^ " Backend]\n") + else + let val m = if cmd_name() = "reml" then "ReML" else "MLKit" + in m ^ " " ^ version ^ " [" ^ backend_name ^ " Backend]\n" + end in print msg end @@ -115,10 +120,18 @@ functor KitCompiler(Execution : EXECUTION) : KIT_COMPILER = val baseDir = case ManagerObjects.Environment.getEnvVal "SML_LIB" of SOME v => v - | NONE => raise Fail ("A library install directory must be provided in an\n" ^ - "environment variable SML_LIB or as a path-definition\n" ^ - "in either the system wide path-map " ^ Configuration.etcdir ^ "/" ^ (cmd_name()) ^ "/mlb-path-map\n" ^ - "or in your personal path-map ~/." ^ (cmd_name()) ^ "/mlb-path-map.") + | NONE => + let val d = if cmd_name() = "smltojs" then "smltojs" else "mlkit" + val notice = if cmd_name() <> "reml" then "" + else ("Notice that ReML shares the runtime system and the compiled\n\ + \basis library with MLKit.") + in raise Fail ("A library install directory must be provided in an\n" ^ + "environment variable SML_LIB or as a path-definition\n" ^ + "in either the system wide path-map " ^ Configuration.etcdir ^ + "/" ^ d ^ "/mlb-path-map\n" ^ + "or in your personal path-map ~/." ^ d ^ "/mlb-path-map.\n" ^ + notice) + end in set_paths baseDir ; go_files rest end diff --git a/src/Common/KitJS.sml b/src/Common/KitJS.sml index 8bcca3a57..d22abec49 100644 --- a/src/Common/KitJS.sml +++ b/src/Common/KitJS.sml @@ -1 +1,12 @@ -structure K = KitMain(KitCompiler(ExecutionJS)) +structure K = +let structure KC = KitCompiler(ExecutionJS) + val () = List.app Flags.block_entry + ["garbage_collection", + "generational_garbage_collection", + "values_64bit", "unbox_reals", "tag_values", "tag_pairs", + "repository", "reml", "region_profiling", "region_inference", + "print_region_flow_graph", "print_all_program_points", + "preserve_tail_calls", "dangling_pointers" + ] +in KitMain(KC) +end diff --git a/src/Common/KitReML.sml b/src/Common/KitReML.sml new file mode 100644 index 000000000..c23883ae0 --- /dev/null +++ b/src/Common/KitReML.sml @@ -0,0 +1,25 @@ + +structure K = + let structure KC = KitCompiler(ExecutionX64) + val _ = Flags.turn_on "reml" + val _ = Flags.turn_on "aggresive_opt" + val _ = Flags.turn_on "parallelism" + val _ = Flags.turn_off "tag_values" + val _ = Flags.turn_on "preserve_tail_calls" + val () = List.app Flags.block_entry + ["garbage_collection", + "warn_spurious", + "values_64bit", + "tag_values", + "tag_pairs", + "statistics_spurious", + "repository", + "regionvar", + "quotation", + "generational_garbage_collection", + "extra_gc_checks", + "export_basis_js", + "disable_spurious_type_variables" + ] + in KitMain(KC) + end diff --git a/src/Common/KitX64.sml b/src/Common/KitX64.sml index 75b287cad..0a04b8492 100644 --- a/src/Common/KitX64.sml +++ b/src/Common/KitX64.sml @@ -2,5 +2,7 @@ structure K = let structure KC = KitCompiler(ExecutionX64) val _ = Flags.turn_on "garbage_collection" + val () = List.app Flags.block_entry + ["export_basis_js"] in KitMain(KC) end diff --git a/src/Common/Man.sml b/src/Common/Man.sml index cfead7216..5d3d72aed 100644 --- a/src/Common/Man.sml +++ b/src/Common/Man.sml @@ -12,6 +12,9 @@ struct fun isSMLtoJs exe : bool = String.isSubstring "smltojs" exe + fun isReML exe : bool = + String.isSubstring "reml" exe + val homepage = "http://melsman.github.io/mlkit" val homepage_smltojs = "http://www.smlserver.org/smltojs" @@ -83,7 +86,7 @@ struct "Peter Sestoft"] val smltojs_developers = ["Martin Elsman"] - + val reml_developers = ["Martin Elsman"] end fun mkStr s = "\"" ^ s ^ "\"" @@ -106,6 +109,8 @@ struct let val text = if isSMLtoJs exe then "Standard ML to JavaScript compiler" + else if isReML exe then + "Standard ML with Explicit Regions and Effects" else "A fullblown Standard ML compiler" in ".SH NAME\n" ^ exe ^ " \\- " ^ text ^ " \n" @@ -122,21 +127,34 @@ struct "All possible options are listed below.\n"] fun description exe = - let val (name, result, homepage) = - if isSMLtoJs exe then - ("SMLtoJs", "an HTML-file, containing references to generated JavaScript files, ", homepage_smltojs) - else - ("MLKit", "an executable file\n.B run\n", homepage) + let val name = + if isSMLtoJs exe then "SMLtoJs" + else if isReML exe then "ReML" + else "MLKit" + val (result, homepage) = + if isSMLtoJs exe + then ("an HTML-file, containing references to generated JavaScript files, ", homepage_smltojs) + else ("an executable file\n.B run\n", homepage) + + val what = + if isReML exe then + "ReML is Standard ML with support for programming with explicit regions, \n\ + \explicit effects, and effect constraints. With ReML, atomic effects \n\ + \include get-effects, put-effects, and mut-effects. Whereas ReML include\n\ + \parallel thread support, ReML does not support integration with \n\ + \reference-tracing garbage collection." + else "" in - String.concat[".SH DESCRIPTION\n", - "When invoked, \n.B ", exe, "\nwill compile the specified sources into ", result, - "through a series of translation phases. Various options (see below) can be used to control the ", - "printing of intermediate forms and to control to which degree various optimizations are performed. If source files ", - "are organised in ML Basis Files (files with extension .mlb), the compiler will memoize symbol table ", - "information and object code in the dedicated MLB directories located together with the source files, so ", - "as to minimize necessary recompilation upon changes of source code.\n\n", - "To learn more about programming with ", name, ", consult the ", name, " web page at\n\n", - ".B ", homepage, "\n"] + String.concat[".SH DESCRIPTION\n", + what, + "When invoked, \n.B ", exe, "\nwill compile the specified sources into ", result, + "through a series of translation phases. Various options (see below) can be used to control the ", + "printing of intermediate forms and to control to which degree various optimizations are performed. If source files ", + "are organised in ML Basis Files (files with extension .mlb), the compiler will memoize symbol table ", + "information and object code in the dedicated MLB directories located together with the source files, so ", + "as to minimize necessary recompilation upon changes of source code.\n\n", + "To learn more about programming with ", name, ", consult the ", if isReML exe then "MLKit" else name, " web page at\n\n", + ".B ", homepage, "\n"] end fun options extraOptions = @@ -163,6 +181,10 @@ struct if isSMLtoJs exe then String.concat [".SH EXAMPLES\n", "For examples, consult the SMLtoJs home page.\n"] + else if isReML exe then + String.concat [".SH EXAMPLES\n", + "For examples, consult the files in the 'test/reml' folder within \n\ + \the github repository at http://github.com/melsman/mlkit.\n"] else let val (name, title) = ("MLKit", "MLKit manual \"Programming with Regions in the MLKit\"") @@ -177,7 +199,9 @@ struct val based_on_mlkit_maybe = if isSMLtoJs exe then "SMLtoJs is based on the MLKit. " - else "" + else if isReML exe then + "ReML is based on the MLKit. " + else "" val maybe_all_basis = if isSMLtoJs exe then ["\n"] else ["See the MLKit home page ", @@ -194,6 +218,9 @@ struct if isSMLtoJs exe then ["SMLtoJs was developed by " ^ concatWith2 (", ", " and ") Devel.smltojs_developers ^ ". ", "Many people have helped developing the MLKit on which SMLtoJs is built; see the MLKit home page for details."] + else if isReML exe then + ["ReML was developed by " ^ concatWith2 (", ", " and ") Devel.reml_developers ^ ". ", + "Many people have helped developing the MLKit on which ReML is built; see the MLKit home page for details."] else ["The MLKit (version 2 and beyond) was developed by ", concatWith2 (", "," and ") Devel.developers, diff --git a/src/Compiler/Backend/X64/ExecutionX64.sml b/src/Compiler/Backend/X64/ExecutionX64.sml index 9b20ef56f..e6a39d0ec 100644 --- a/src/Compiler/Backend/X64/ExecutionX64.sml +++ b/src/Compiler/Backend/X64/ExecutionX64.sml @@ -253,16 +253,13 @@ structure ExecutionX64: EXECUTION = val delete_target_files = Flags.is_on0 "delete_target_files" val libs = Flags.lookup_string_entry "libs" - fun gas0() = + fun gas0 () = !(Flags.lookup_string_entry "assembler") -(* - if onmac_p() then "as -arch x64" else "as --64" -*) - fun gas() = if gdb_support() then - if onmac_p() then gas0() ^ " -g" - else gas0() ^ " --gstabs" - else gas0() + fun gas () = if gdb_support() then + if onmac_p() then gas0() ^ " -g" + else gas0() ^ " --gstabs" + else gas0() fun assemble (file_s, file_o) = (execute_command (gas() ^ " -o " ^ file_o ^ " " ^ file_s); @@ -312,32 +309,33 @@ structure ExecutionX64: EXECUTION = val gengc_p = Flags.is_on0 "generational_garbage_collection" fun path_to_runtime () = - let fun file () = - if parallelism_p() then - (if tag_values() then - die "parallelism enabled - turn off value tagging" - else if gc_p() then - die "parallelism enabled - turn off gc" - else if !region_profiling then - die "parallelism enabled - turn off prof" - else if tag_pairs_p() then - die "parallelism enabled - turn off pair tagging" - else if argobots_p() then "runtimeSystemArPar.a" - else "runtimeSystemPar.a") - else - if !region_profiling andalso gc_p() andalso tag_pairs_p() then "runtimeSystemGCTPProf.a" else - if !region_profiling andalso gc_p() andalso gengc_p() then "runtimeSystemGenGCProf.a" else - if !region_profiling andalso gc_p() then "runtimeSystemGCProf.a" else - if !region_profiling then "runtimeSystemProf.a" else - if gc_p() andalso tag_pairs_p() then "runtimeSystemGCTP.a" else - if gc_p() andalso gengc_p() then "runtimeSystemGenGC.a" else - if gc_p() then "runtimeSystemGC.a" else - if tag_values() andalso tag_pairs_p() then - die "no runtime system supports tagging of values with tagging of pairs" else - if tag_values() then "runtimeSystemTag.a" else - "runtimeSystem.a" - in !Flags.install_dir ## "lib" ## file() - end + let + fun file () = + if parallelism_p() then + (if tag_values() then + die "parallelism enabled - turn off value tagging" + else if gc_p() then + die "parallelism enabled - turn off gc" + else if !region_profiling then + die "parallelism enabled - turn off prof" + else if tag_pairs_p() then + die "parallelism enabled - turn off pair tagging" + else if argobots_p() then "runtimeSystemArPar.a" + else "runtimeSystemPar.a") + else + if !region_profiling andalso gc_p() andalso tag_pairs_p() then "runtimeSystemGCTPProf.a" else + if !region_profiling andalso gc_p() andalso gengc_p() then "runtimeSystemGenGCProf.a" else + if !region_profiling andalso gc_p() then "runtimeSystemGCProf.a" else + if !region_profiling then "runtimeSystemProf.a" else + if gc_p() andalso tag_pairs_p() then "runtimeSystemGCTP.a" else + if gc_p() andalso gengc_p() then "runtimeSystemGenGC.a" else + if gc_p() then "runtimeSystemGC.a" else + if tag_values() andalso tag_pairs_p() then + die "no runtime system supports tagging of values with tagging of pairs" else + if tag_values() then "runtimeSystemTag.a" else + "runtimeSystem.a" + in !Flags.install_dir ## "lib" ## file() + end in val link_files_with_runtime_system = link_files_with_runtime_system0 path_to_runtime end diff --git a/src/Compiler/Compile.sml b/src/Compiler/Compile.sml index 8845c17f2..fd4ac4d74 100644 --- a/src/Compiler/Compile.sml +++ b/src/Compiler/Compile.sml @@ -74,6 +74,12 @@ structure Compile: COMPILE = item=ref false, neg=false, desc= "Print region-spreaded program."} + val print_region_inferred_program = Flags.add_bool_entry + {long="print_region_inferred_program", short=SOME "Prip", + menu=["Printing of intermediate forms","print region-inferred program"], + item=ref false, neg=false, desc= + "Print region-inferred program."} + fun parallelism_p () : bool = Flags.is_on "parallelism" val debug_parallelism_p = Flags.add_bool_entry @@ -254,8 +260,8 @@ structure Compile: COMPILE = val _ = chat "]\n" val pgm' = RegionExp.PGM{expression = spread_lamb_exp, (*side-effected*) - export_datbinds = datbinds, (*unchanged*) - export_basis= new_layer (* list of region variables and arrow effects *)} + export_datbinds = datbinds, (*unchanged*) + export_basis= new_layer (* list of region variables and arrow effects *)} (* call of normPgm no longer commented out; mads *) (* @@ -301,13 +307,14 @@ structure Compile: COMPILE = end else () *) - in - if !Flags.DEBUG_COMPILER then - (say "Resulting region-static environment:\n"; - sayenv(rse'); - display("\nReport: After Region Inference", layoutRegionPgm pgm')) - else (); - (cone,rse',pgm') (* rse' contains rse_con *) + in if !Flags.DEBUG_COMPILER then + (say "Resulting region-static environment:\n"; + sayenv(rse')) + else () + ; if !Flags.DEBUG_COMPILER orelse print_region_inferred_program() then + display("\nReport: After Region Inference", layoutRegionPgm pgm') + else () + ; (cone,rse',pgm') (* rse' contains rse_con *) end (* ---------------------------------------------------------------------- *) diff --git a/src/Compiler/Regions/EFFECT.sig b/src/Compiler/Regions/EFFECT.sig index c8e3ac4df..8ef2259d5 100644 --- a/src/Compiler/Regions/EFFECT.sig +++ b/src/Compiler/Regions/EFFECT.sig @@ -199,21 +199,24 @@ sig val rho_add_constraint : effect -> Report * lvar option * effect -> unit val rho_get_constraints : effect -> (Report * lvar option * effect) list - (* [eps_add_prop_constraint e (p,rep,lvopt)] adds a constraint to e saying it has + (* [eps_add_prop_constraint e (i,p,rep,lvopt)] adds a constraint to e saying it has * to obey the property p; the optional lvar indicates the function with the - * constraint. *) - val eps_add_prop_constraint : effect -> Report * lvar option * prop -> unit - val eps_get_prop_constraints : effect -> (Report * lvar option * prop) list + * constraint. i specifies if it is an instantiated constraint. *) + val eps_add_prop_constraint : effect -> bool * Report * lvar option * prop -> unit + val eps_get_prop_constraints : effect -> (bool * Report * lvar option * prop) list - (* [eps_add_constraint e (rep,lvopt,e',putonly)] adds a constraint + (* [eps_add_constraint e (i,rep,lvopt,e',putonly)] adds a constraint * to e saying it cannot intersect with e' (up to the putonly boolean); the - * optional lvar indicates the function with the constraint. *) + * optional lvar indicates the function with the constraint. i specifies if + * it is an instantiated constraint. *) - val eps_add_constraint : effect -> Report * lvar option * effect * bool -> unit - val eps_get_constraints : effect -> (Report * lvar option * effect * bool) list + type instlist = (effect * effect) list + val rep_instlist : instlist -> Report + + val eps_add_constraint : effect -> bool * Report * instlist * lvar option * effect * bool -> unit + val eps_get_constraints : effect -> (bool * Report * instlist * lvar option * effect * bool) list datatype delta_phi = Lf of effect list | Br of delta_phi * delta_phi - val observe : int * delta_phi * effect -> unit val observeDelta : int * delta_phi * effect -> effect list * delta_phi val update_increment : effect * delta_phi -> unit @@ -247,7 +250,9 @@ sig val topsort : effect list -> effect list val subgraph : effect list -> effect list - val eval_phis : effect list -> unit + val eval_phis : effect list -> effect list (* returns all nodes in graph *) + val check_nodes : {allnodes:effect list, letregions:effect list} -> unit (* check ReML constraints *) + val represents : effect -> effect list val reset_cone : cone -> unit @@ -255,12 +260,13 @@ sig type StringTree = PrettyPrint.StringTree - val layout_effect_deep: effect -> StringTree (* sets and clears visited field *) - val layout_effect : effect->StringTree (* no side-effect *) - val layoutLayer : coneLayer -> StringTree (* sets and clears visited field *) - val layoutLayerRng : coneLayer -> StringTree (* sets and clears visited field *) - val layoutCone : cone -> StringTree (* sets and clears visited field *) - val layoutEtas : effect list -> StringTree list (* sets and clears visited field *) + val layout_effect_deep : effect -> StringTree (* sets and clears visited field *) + val layout_effect : effect->StringTree (* no side-effect *) + val layout_effect_binding : effect->StringTree (* no side-effect; prints constraints *) + val layoutLayer : coneLayer -> StringTree (* sets and clears visited field *) + val layoutLayerRng : coneLayer -> StringTree (* sets and clears visited field *) + val layoutCone : cone -> StringTree (* sets and clears visited field *) + val layoutEtas : effect list -> StringTree list (* sets and clears visited field *) structure PlaceOrEffectMap : MONO_FINMAP where type dom = effect end diff --git a/src/Compiler/Regions/Effect.sml b/src/Compiler/Regions/Effect.sml index 99346def4..63b10cf26 100644 --- a/src/Compiler/Regions/Effect.sml +++ b/src/Compiler/Regions/Effect.sml @@ -64,11 +64,16 @@ struct val print_constraints = Flags.add_bool_entry {long="print_constraints", short=NONE, item=ref false, neg=false, - menu=["Layout", "print effect constraints"], - desc="Print effect constraints when printing region and\n\ - \effect variables"} + menu=["Layout", "print ReML effect constraints"], + desc="Print ReML effect constraints when printing region and\n\ + \effect variables."} - val explicit_regions : unit -> bool = Flags.is_on0 "explicit_regions" + val debug_constraint_solving = Flags.add_bool_entry + {long="debug_constraint_solving", short=SOME "dcs", item=ref false, neg=false, + menu=["ReML", "debug ReML constraint solving"], + desc="Debug ReML constraint solving."} + + val reml_p : unit -> bool = Flags.is_on0 "reml" fun mem x nil = false | mem x (y::ys) = x = y orelse mem x ys @@ -130,8 +135,6 @@ struct fun key_lt (ref i, ref (j:int)) = i "r" ^ show_key key + | SOME rv => "`" ^ RegVar.pr rv ^ "_" ^ show_key key + in PP.LEAF (n ^ + (if print_rho_types() then show_runType ty + else "") ^ + (if print_rho_protection() then show_protection protected + else "") ^ + (if print_rho_levels() then "(" ^ show_level level ^ ")" + else "") ^ + (if print_constraints() then + case !constraints of + nil => "" + | rhos => "[memo]" + else "") + ) + end + + type effect = einfo G.node + + fun pp_atomic_effect (ae:effect) = + let fun layout_einfo_rho_simple einfo = + case einfo of + RHO{key,level,ty,explicit,protected,constraints,...} => + layout_rho0 (key,level,ty,explicit,protected,constraints) + | _ => die "layout_einfo_rho_simple: expecting rho" + fun pp_rho_simple r = + PP.flatten1(G.layout_node layout_einfo_rho_simple r) + fun pp base n = + case G.out_of_node n of + [n] => PP.LEAF (base ^ "(" ^ pp_rho_simple n ^ ")") + | _ => die "layout_einfo_ae_simple.pp.expecting exactly one out node" + fun layout_einfo_ae_simple node einfo = + case einfo of + EPS{key,explicit,...} => + let val n = case explicit of + NONE => "e" ^ show_key key + | SOME ev => "`" ^ RegVar.pr ev ^ "_" ^ show_key key + in PP.LEAF n + end + | PUT => pp "put" node + | GET => pp "get" node + | MUT => pp "mut" node + | _ => die "layout_einfo_ae_simple.expecting atomic effect" + in PP.flatten1(G.layout_node (layout_einfo_ae_simple ae) ae) + end + + fun layout_einfo0 {binding:bool} einfo = case einfo of EPS{key,level,explicit,prop_constraints,constraints,...} => let val n = case explicit of @@ -174,9 +225,20 @@ struct in PP.LEAF(n ^ (if print_rho_levels() then "(" ^ show_level level ^ ")" else "") - ^ (if print_constraints() then - let val cs1 = map (LambdaExp.pp_prop o #3) (!prop_constraints) - val cs2 = map (fn _ => "memo") (!constraints) + ^ (if binding andalso print_constraints() then + let val cs1 = map (fn (i,_,_,p) => + if i then "?" ^ LambdaExp.pp_prop p + else LambdaExp.pp_prop p) + (!prop_constraints) + val cs2 = map (fn (i,_,_,_,ae,p) => + let val s = + case (p,i) of + (true,true) => "?? " + | (false,true) => "? " + | (true,false) => "## " + | (false,false) => "# " + in s ^ pp_atomic_effect ae + end) (!constraints) val cs = cs1 @ cs2 in if List.null cs then "" else "[" ^ String.concatWith "," cs ^ "]" @@ -188,33 +250,26 @@ struct | GET => PP.LEAF "get" | MUT => PP.LEAF "mut" | UNION _ => PP.LEAF "U" - | RHO{key,level,ty,put,explicit,protected,constraints,...} => - let val n = case explicit of - NONE => "r" ^ show_key key - | SOME rv => "`" ^ RegVar.pr rv ^ "_" ^ show_key key - in PP.LEAF (n ^ - (if print_rho_types() then show_runType ty - else "") ^ - (if print_rho_protection() then show_protection protected - else "") ^ - (if print_rho_levels() then "(" ^ show_level level ^ ")" - else "") ^ - (if print_constraints() then - case !constraints of - nil => "" - | rhos => "[memo]" - else "") - ) - end + | RHO{key,level,ty,explicit,protected,constraints,...} => + layout_rho0 (key,level,ty,explicit,protected,constraints) - type effect = einfo G.node + fun layout_einfo ei = + layout_einfo0 {binding=false} ei + + fun layout_einfo_binding ei = + layout_einfo0 {binding=true} ei + + type instlist = (effect * effect) list (* for constraints *) type place = effect + val empty = G.mk_node (UNION{represents = NONE}) fun eq_effect (node1, node2) = G.eq_nodes(node1,node2) + fun mem_effect e es = List.exists (fn e' => eq_effect(e,e')) es fun layout_effect e = G.layout_node layout_einfo e - fun layout_effect_deep e = G.layout_nodes_deep layout_einfo [e] + fun layout_effect_binding e = G.layout_node layout_einfo_binding e + fun layout_effect_deep e = G.layout_nodes_deep layout_einfo_binding [e] fun pr_effect e = PP.flatten1 (layout_effect e) @@ -248,30 +303,30 @@ struct RHO {constraints=ref cs,...} => cs | _ => die "rho_get_constraint.expecting rho" - fun eps_add_prop_constraint e (rep,lvopt,p:prop) : unit = + fun eps_add_prop_constraint e (inst,rep,lvopt,prop) : unit = case G.find_info e of EPS{prop_constraints,...} => let val cs = !prop_constraints - in if mem p (map #3 cs) then () - else prop_constraints := (rep,lvopt,p)::cs + in if List.exists (fn (i,_,_,p) => inst=i andalso prop=p) cs then () + else prop_constraints := (inst,rep,lvopt,prop)::cs end | _ => die "eps_add_prop_constraint.expecting eps" - fun eps_get_prop_constraints (e: effect) : (Report * lvar option * prop) list = + fun eps_get_prop_constraints (e: effect) : (bool * Report * lvar option * prop) list = case G.find_info e of EPS{prop_constraints,...} => !prop_constraints | _ => die "eps_get_prop_constraints.expecting eps" - fun eps_add_constraint e (rep,lvopt,e',putonly:bool) : unit = + fun eps_add_constraint e (i,rep,il,lvopt,ae',putonly:bool) : unit = case G.find_info e of EPS{constraints,...} => let val cs = !constraints - in if List.exists (fn (_,_,e,p) => p=putonly andalso eq_effect (e,e')) cs then () - else constraints := (rep,lvopt,e',putonly)::cs + in if List.exists (fn (i',_,_,_,ae,p) => i=i' andalso p=putonly andalso eq_effect (ae,ae')) cs then () + else constraints := (i,rep,il,lvopt,ae',putonly)::cs end | _ => die "eps_add_constraint.expecting eps" - fun eps_get_constraints (e: effect) : (Report * lvar option * effect * bool) list = + fun eps_get_constraints (e: effect) : (bool * Report * instlist * lvar option * effect * bool) list = case G.find_info e of EPS{constraints,...} => !constraints | _ => die "eps_get_constraints.expecting eps" @@ -307,14 +362,6 @@ struct SOME rv => "`" ^ RegVar.pr rv | NONE => pr_effect e - fun pr_atomic_effect e = - if is_arrow_effect e then pp_eff e - else let val n = case G.out_of_node e of - n :: _ => n - | _ => die "pr_atomic_effect.expecting an out-node" - in pr_effect e ^ "(" ^ pp_eff n ^ ")" - end - fun is_put effect = case G.find_info effect of PUT => true @@ -368,7 +415,12 @@ struct fun get_level_of_rho effect : int = case G.find_info effect of RHO{level as ref l,...} => l - | _ => die "GetLevelOfRho" + | _ => die "get_level_of_rho" + + fun get_level_of_eps effect : int = + case G.find_info effect of + EPS{level as ref l,...} => l + | _ => die "get_level_of_eps" fun key_of_rho effect : int = case G.find_info effect of @@ -1011,6 +1063,12 @@ struct Pickle.cache "Effect.nodeopt" (Pickle.optionGen o #1 o pu_node_nodes) + fun tup6Gen (a,b,c,d,e,f) = + let fun to ((a,b,c),(d,e,f)) = (a,b,c,d,e,f) + fun from (a,b,c,d,e,f) = ((a,b,c),(d,e,f)) + in Pickle.shareGen(Pickle.convert0 (to,from) (Pickle.pairGen0(Pickle.tup3Gen0(a,b,c),Pickle.tup3Gen0(d,e,f)))) + end + val pu_einfo = let fun toInt (EPS _) = 0 | toInt (UNION _) = 1 @@ -1019,9 +1077,15 @@ struct | toInt MUT = 4 | toInt (RHO _) = 5 fun pu_constraints pu_einfo = - Pickle.refOneGen (Pickle.listGen(Pickle.tup4Gen(Report.pu,Pickle.optionGen Lvars.pu, - #1(pu_node_nodes pu_einfo), - Pickle.bool))) + let val pu_effect = #1(pu_node_nodes pu_einfo) + val pu_instlist = Pickle.listGen(Pickle.pairGen(pu_effect,pu_effect)) + in Pickle.refOneGen (Pickle.listGen(tup6Gen(Pickle.bool, + Report.pu, + pu_instlist, + Pickle.optionGen Lvars.pu, + pu_effect, + Pickle.bool))) + end fun fun_EPS pu_einfo = Pickle.newHash (fn EPS {key=ref k,...} => k | _ => die "pu_einfo.newHash.EPS") (Pickle.con1 (fn ((k,l,r,p),y,pcs,cs) => @@ -1033,7 +1097,8 @@ struct | _ => die "pu_einfo.fun_EPS") (Pickle.tup4Gen0(Pickle.tup4Gen0(pu_intref,pu_intref,pu_represents pu_einfo,pu_intref), Pickle.optionGen RegVar.pu, - Pickle.refOneGen(Pickle.listGen (Pickle.tup3Gen(Report.pu, + Pickle.refOneGen(Pickle.listGen (Pickle.tup4Gen(Pickle.bool, + Report.pu, Pickle.optionGen Lvars.pu, LambdaExp.pu_prop))), pu_constraints pu_einfo @@ -1165,7 +1230,7 @@ struct fun current_increment eps = case Increments.lookup (!globalIncs) eps of - SOME delta => delta + SOME delta => delta | NONE => Lf [] (*****************************************************) @@ -1177,12 +1242,12 @@ struct *) fun lower (newlevel:int) : effect -> cone -> cone = - let fun low' ([],b) = b - | low' (x::xs,b) = low'(xs,low(x, b)) - and low (effect, cone:cone) : cone = + let fun lows ([],B) = B + | lows (x::xs,B) = lows(xs,low(x, B)) + and low (effect, B:cone) : cone = case get_level_and_key effect of SOME (l as ref n, key) => - if newlevel >= n then cone + if newlevel >= n then B else (* newlevel < level: lower level *) let val _ = case explicit_var effect of NONE => () @@ -1199,17 +1264,34 @@ struct RegVar.pr v ^ " has insufficient scope.") in raise Report.DeepError (report0 // report) end - val cone' = remove(effect,l,!key,cone) (* take node out of cone *) - handle ? => (print "lower\n"; raise ?) + val B = remove(effect,l,!key,B) (* take node out of cone *) + handle ? => (print "lower\n"; raise ?) val _ = l:= newlevel - val cone'' = add(effect, newlevel, !key,cone') - (* put node back in cone at lower level *) - in low' (G.out_of_node effect, cone'') + val B = add(effect, newlevel, !key,B) (* put node back in cone at lower level *) + (* we now need to lower children and effects in constraints *) +(* + val B = if is_arrow_effect effect then + let val effs = List.map #3 (eps_get_constraints effect) + in lows(effs,B) + end + else B +*) + (* when lowering the level of an eps node, we keep only those constraints that involve + other epss with lower or identical level *) +(* + val () = + case G.find_info effect of + EPS{constraints,...} => + constraints:=List.filter (fn (_,_,e,_) => + get_level_of_eps e <= newlevel) (!constraints) + | _ => () +*) + in lows (G.out_of_node effect, B) end | NONE => (* not EPS or RHO, no level; just lower children *) - low'(G.out_of_node effect,cone) - in fn effect => fn cone => low(effect,cone) - end + lows(G.out_of_node effect,B) + in fn effect => fn B => low(effect,B) + end fun lower_delta level delta B = case delta of @@ -1274,8 +1356,8 @@ struct end fun merge_prop_constraints pcs1 pcs2 = - let fun ins (c:'a*'b*prop,nil) = [c] - | ins (c,c'::cs) = if #3 c = #3 c' then c'::cs + let fun ins (c:bool*'b*'c*prop,nil) = [c] + | ins (c,c'::cs) = if #4 c = #4 c' andalso #1 c = #1 c' then c'::cs else c'::ins(c,cs) fun mer (nil,cs) = cs | mer (cs,nil) = cs @@ -1285,8 +1367,8 @@ struct end fun merge_constraints cs1 cs2 = - let fun ins (c:'a*'b*effect*bool,nil) = [c] - | ins (c,c'::cs) = if eq_effect (#3 c,#3 c') andalso #4 c = #4 c' then c'::cs + let fun ins (c:bool*'b*'c*'d*effect*bool,nil) = [c] + | ins (c,c'::cs) = if eq_effect (#5 c,#5 c') andalso #6 c = #6 c' andalso #1 c = #1 c' then c'::cs else c'::ins(c,cs) fun mer (nil,cs) = cs | mer (cs,nil) = cs @@ -1620,6 +1702,52 @@ struct fun say s = (TextIO.output(TextIO.stdOut, s); TextIO.output(!Flags.log, s)) + (* [elim_constraints dest effects] Eliminate constraints in dest that involve effects *) + fun elim_constraints (dest:effect) (effects:effect list) : unit = + let fun ins (c,cs) = + if memEq (fn (c,c') => #5 c = #5 c' andalso #1 c = #1 c') c cs then cs + else c::cs + val nodes : effect list ref = ref nil + fun visited e = !(G.find_visited e) + fun visit e = G.find_visited e := true + fun elim d = + if visited d then () + else ( visit d + ; nodes := d :: !nodes + ; case G.find_info d of + EPS{constraints,...} => + ( constraints := + List.foldl (fn (c as (i,r,il,lv,ae,p),cs) => + if is_arrow_effect ae then + if mem_effect ae effects then + let val outs = G.out_of_node ae + val outs_es = List.filter (fn e => not(mem_effect e effects)) outs + val cs' = List.map (fn ae' => (i,r,il,lv,ae',p)) outs_es + val cs' = List.filter (fn c => not(#6 c) orelse is_put (#5 c) orelse is_arrow_effect (#5 c)) cs' + in List.foldl ins cs cs' + end + else ins (c,cs) + else + (* put, mut, or get *) + let val r = rho_of ae + in if mem_effect r effects then cs + else ins (c,cs) + end + ) nil (!constraints) + ; List.app elim (G.out_of_node d) + ) + | UNION _ => List.app elim (G.out_of_node d) + | _ => ()) + in elim dest + ; G.unvisit (!nodes) + end + + (* + l+1; TE |- e : t, phi (B,_) = observeDelta(l,phi,phi') + -------------------------------------------------------- + l; TE |- letregion B in e : t, phi' + *) + fun observeDelta (l: int, source: delta_phi, destination: effect): effect list * delta_phi = let (*val _ = Profile.profileOn()*) @@ -1717,13 +1845,12 @@ struct (* say("\nDESTINATION AFTER OBSERVE= "); PP.outputTree(say, layout_effect_deep destination, !Flags.colwidth); (*input(std_in, 1);*) -*) + *) + elim_constraints destination (!r_acc); (* eliminate constraints involving abstracted effects in source *) (!r_acc, Lf nodes_to_add) end end - fun observe x = (observeDelta x; ()) - (* collapse of cycles in effects: *) (* all members of the scc must have the same level; otherwise the graph was ill-formed in the first place. Therefore we do not lower levels. *) @@ -2092,11 +2219,20 @@ struct die "check_represents")) l; l) - fun check_prop_constraint (n:effect) (rep,lvopt,p:prop) (ae:effect) = (*ae: atomic effect *) - let fun violation p = + fun debug_const f = + if debug_constraint_solving() then print(f() ^ "\n") + else () + + fun check_prop_constraint (n:effect) (i,rep,lvopt,p:prop) (ae:effect) = (*ae: atomic effect *) + (*if not i then () (* check only instantiation constraints *) + else*) + let + val () = debug_const (fn () => "Checking " ^ pr_effect n ^ " -> " + ^ pp_atomic_effect ae ^ " " ^ LambdaExp.pp_prop p) + fun violation p = let fun msg s = s ^ " constraint violation. The effect " - ^ pp_eff n ^ " contains\nthe atomic effect " - ^ pr_atomic_effect ae ^ + ^ pr_effect n ^ " contains\nthe atomic effect " + ^ pp_atomic_effect ae ^ (if is_arrow_effect ae then ", which has no " ^ LambdaExp.pp_prop p ^ " property" else "") in case p of @@ -2107,40 +2243,147 @@ struct fun err p = deepError0 rep (violation p) in if is_arrow_effect ae then let val cs_ae = eps_get_prop_constraints ae - in if mem p (map #3 cs_ae) then () + in if List.exists (fn (i,_,_,p') => p=p' andalso not i) cs_ae then + debug_const (fn () => " CHECK - effect var with " ^ LambdaExp.pp_prop p) else err p end else case p of LambdaExp.NOMUTprop => - if is_mut ae then err p else () + if is_mut ae then err p else debug_const (fn () => " CHECK - not arrow effect and not mut") | LambdaExp.NOPUTprop => - if is_put ae then err p else () + if is_put ae then err p else debug_const (fn () => " CHECK - not arrow effect and not put") | LambdaExp.NOEXNprop => - if is_exn ae then err p else () + if is_exn ae then err p else debug_const (fn () => " CHECK - not arrow effect and not exn") end fun not_put ae = not(is_put ae) - - fun check_constraint (n:effect) (rep,lvopt,e:effect,putonly:bool) (ae:effect) = (*ae: atomic effect *) - if putonly andalso not_put ae then () else + infix implies + fun a implies b = b orelse not a + + (* check that ae is consistent with the constraint (second argument); + ae: atomic effect of n + e: e # n (not putonly) and e ## n (putonly) + *) + datatype cerr = ConstraintError of unit -> unit | NoConstraintError + + fun rep_inst (s,t) = Report.line ("Instance " ^ pr_effect s ^ " -> " ^ pr_effect t) + fun rep_instlist nil = Report.null + | rep_instlist [i1,i2] = Report.//(rep_inst i1,rep_inst i2) + | rep_instlist (i::is) = Report.//(rep_inst i,rep_instlist is) + + (* [check_constraint_normal n c ae] checks that the atomic effect + ae, pointed to by the effect variable node n, is satisfied by the + constraint c *) + + fun check_constraint_normal (letregions:effect list) (nopt:effect option) (c as (i,rep,instlist,lvopt,e:effect,putonly:bool)) (ae:effect) : cerr = (*ae: atomic effect *) + (*if not i then NoConstraintError (* check only instantiation constraints *) + else*) let fun violation () = if putonly then "Put-constraint violation" else "Constraint violation" - fun msg () = violation() ^ ". The effect " - ^ pp_eff n ^ " contains\nthe atomic effect " - ^ pr_atomic_effect ae ^ ", which also appears in the effect of " - ^ pr_atomic_effect e - fun err () = deepError0 rep (msg ()) - val aes = - case G.find_info e of - EPS{represents=SOME aes,...} => aes - | EPS _ => die ("check_constraint.no represents for node " ^ pp_eff e) - | _ => die "check_constraint.expects eps" - val aes = if putonly then List.filter is_put aes else aes - in List.app (fn ae' => if eq_effect(ae,ae') then err () - else ()) aes + fun mkrep () = Report.//(rep,rep_instlist instlist) + val () = debug_const (fn () => "Checking " ^ (case nopt of SOME n => pr_effect n ^ " -> " + | NONE => "") + ^ pp_atomic_effect ae ^ " satisfies " ^ + (if putonly then "?? " else "? ") ^ pr_effect e) + in if is_arrow_effect ae then + (* two possibilities: (1) putonly and there is a noput prop_constraint in ae or on n + or (2) there is a #e or a ##e in ae. + *) + let val cs = eps_get_constraints ae + val pcs = eps_get_prop_constraints ae + val pcs2 = case nopt of + SOME n => eps_get_prop_constraints n + | NONE => nil + in if List.exists (fn (i,_,_,p) => not i andalso p = LambdaExp.NOPUTprop) (pcs @ pcs2) then + ( debug_const (fn () => " CHECK satisfied - noput") + ; NoConstraintError) + else if List.exists (fn (i,_,_,_,e',p) => not i andalso eq_effect (e,e') andalso (p implies putonly)) cs then + ( debug_const (fn () => " CHECK satisfied") + ; NoConstraintError) + else + (* look in children if ae is letregion-bound *) + if mem_effect ae letregions then + let val () = debug_const (fn () => " LETREGION Bound ae (start sub): " ^ pr_effect ae) + val aes = case G.find_info ae of + EPS{represents=SOME aes,...} => aes + | _ => die "check_constraint_normal.expects EPS" + fun loop nil = + ( debug_const (fn () => " CHECK satisfied - sub") + ; NoConstraintError) + | loop (ae::aes) = + case check_constraint_normal letregions nopt c ae of + NoConstraintError => loop aes + | ConstraintError rep => + case check_constraint_reversed letregions c ae of + NoConstraintError => loop aes + | _ => ConstraintError rep + in loop aes + end + else if mem_effect e letregions then + check_constraint_reversed letregions c ae + else + ConstraintError (fn () => deepError0 (mkrep()) + (violation() ^ ". Constraint not discharged by a satisfying constraint.")) + end + else if putonly andalso not_put ae then + ( debug_const (fn () => " CHECK satisfied noput") + ; NoConstraintError) + else + (* ae is not an effect variable! *) + let fun msg () = violation() ^ ". The effect " + ^ (case nopt of SOME n => pr_effect n ^ " " + | NONE => "") ^ "contains\nthe atomic effect " + ^ pp_atomic_effect ae ^ ", which also appears in the effect of " + ^ pp_atomic_effect e + fun err () = deepError0 (mkrep()) (msg()) + val aes = + case G.find_info e of + EPS{represents=SOME aes,...} => aes + | EPS _ => die ("check_constraint.no represents for node " ^ pr_effect e) + | PUT => [e] + | GET => [e] + | MUT => [e] + | _ => die "check_constraint.expects atomic effect" + val aes' = if putonly then List.filter is_put aes else aes + in if List.exists (fn ae' => eq_effect(ae,ae')) aes' + then ConstraintError (fn () => err ()) + else let val pcs = eps_get_prop_constraints e + in if putonly andalso + List.exists (fn (i,_,_,p) => not i andalso p = LambdaExp.NOPUTprop) pcs + then + ( debug_const (fn () => " CHECK satisfied - noput2") + ; NoConstraintError) + else + if mem_effect e letregions then + case List.filter is_arrow_effect aes of + nil => NoConstraintError + | eps :: _ => ConstraintError + (fn () => + deepError0 (mkrep()) + (violation() ^ ". The effect " + ^ (case nopt of SOME n => pr_effect n ^ " " + | NONE => "") + ^ "contains\nthe atomic effect " + ^ pp_atomic_effect ae + ^ ", which I cannot conclude does not appear in " + ^ pp_atomic_effect e ^ ", which contains " ^ pr_effect eps)) + else ConstraintError (fn () => err()) + end + end end + and check_constraint_reversed letregions (i,rep,il,lvopt,e,putonly) ae : cerr = + if is_arrow_effect e then + ( debug_const(fn() => "Reverse check") + ; check_constraint_normal letregions NONE (i,rep,il,lvopt,ae,putonly) e) + else NoConstraintError + + fun check_constraint (letregions:effect list) (n:effect) c ae = + case check_constraint_normal letregions (SOME n) c ae of + NoConstraintError => () + | ConstraintError err => err() + fun bottom_up_eval (g : effect list) : effect list = (* * bottom_up_eval g : every EPS or UNION node has a @@ -2215,23 +2458,25 @@ struct *) in ( G.unvisit g - ; if explicit_regions() then MultiMerge.multimerge nodess else nil + ; if reml_p() then MultiMerge.multimerge nodess else nil ) end - fun check_node (n:effect) : unit = + fun check_node (letregions:effect list) (n:effect) : unit = case G.find_info n of EPS{represents,prop_constraints,constraints,...} => - let (*val () = print ("Checking " ^ pp_eff n + let +(* + val () = print ("Checking " ^ pr_effect n ^ " pcs: " ^ Int.toString(length(!prop_constraints)) ^ " cs: " ^ Int.toString (length(!constraints)) ^ "\n") - *) +*) val aes = case represents of SOME aes => aes | NONE => die "check_node.represents list not set" in List.app (fn c => List.app (check_prop_constraint n c) aes) (!prop_constraints) - ; List.app (fn c => List.app (check_constraint n c) aes) + ; List.app (fn c => List.app (check_constraint letregions n c) aes) (!constraints) end | _ => () @@ -2242,16 +2487,20 @@ struct we now first contract all cycles, then do a bottom-up evaluation of the graph *) - fun eval_phis (phis: effect list) : unit = + fun eval_phis (phis: effect list) : effect list = let val nodes = contract_effects phis val allnodes = bottom_up_eval nodes - in List.app check_node allnodes - handle ? as Report.DeepError _ => raise ? - | exn => (say "\neval_phis failed; nodes = "; - say_etas (layoutEtas nodes); - raise exn) + handle ? as Report.DeepError _ => raise ? + | exn => (say "\neval_phis failed; nodes = "; + say_etas (layoutEtas nodes); + raise exn) + in allnodes end + fun check_nodes {allnodes:effect list, letregions: effect list} = + List.app (check_node letregions) allnodes + handle ? as Report.DeepError _ => raise ? + fun represents eps = case G.find_info eps of EPS{represents = SOME l, ...} => diff --git a/src/Compiler/Regions/MulInf.sml b/src/Compiler/Regions/MulInf.sml index 400c643cd..3c39461a3 100644 --- a/src/Compiler/Regions/MulInf.sml +++ b/src/Compiler/Regions/MulInf.sml @@ -571,13 +571,20 @@ struct val _ = if test then say " collecting all effects..." else () (* collect all region variables, locally bound within tr, plus the region and effect variables that are exported by tr *) - val effects= mkPhi(tr,export_basis) + val effects = mkPhi(tr,export_basis) val _ = if test then say " computing transitive closure ..." else () - val _ = eval_phis effects (* computes transitive closure of effect graph, - including only PUT and EPS nodes *) - handle ? as Report.DeepError _ => raise ? - | exn => (say " eval_phis called from MulInf (transitive closure of all effects) "; - raise exn) + + val () = + let val allnodes = eval_phis effects (* computes transitive closure of effect graph, + including only PUT and EPS nodes *) + handle ? as Report.DeepError _ => raise ? + | exn => (say " eval_phis called from MulInf (transitive closure of all effects) "; + raise exn) + val () = Eff.check_nodes {allnodes=allnodes, + letregions=RegionExp.letregionBound tr} + in () + end + val _ = if test then say " making the arrow effect set Phi..." else () val Psi = diff --git a/src/Compiler/Regions/REGION_EXP.sml b/src/Compiler/Regions/REGION_EXP.sml index 4e382c4aa..d00e25b31 100644 --- a/src/Compiler/Regions/REGION_EXP.sml +++ b/src/Compiler/Regions/REGION_EXP.sml @@ -129,6 +129,8 @@ signature REGION_EXP = sig val mkPhi: (place,'b)trip * effect list -> effect list + val letregionBound : (place,'b)trip -> effect list + val normPgm: (place, 'b)LambdaPgm * (unit -> int) -> unit val pr_tyvar : tyvar -> string diff --git a/src/Compiler/Regions/RType.sml b/src/Compiler/Regions/RType.sml index e61f4b832..d71ee5885 100644 --- a/src/Compiler/Regions/RType.sml +++ b/src/Compiler/Regions/RType.sml @@ -15,6 +15,7 @@ struct fun log_tree t = PP.outputTree(logsay, t, !Flags.colwidth) fun show_rho rho = PP.flatten1(E.layout_effect rho) fun show_eps e = PP.flatten1(E.layout_effect e) + fun show_eps_binding e = PP.flatten1(E.layout_effect_binding e) fun show_rhos rhos = ListUtils.stringSep "[" "]" ", " show_rho rhos fun die (s:string) = Crash.impossible ("RType." ^ s) @@ -363,8 +364,8 @@ struct (SOME n1, SOME n2) => if E.is_arrow_effect n1 then if E.is_arrow_effect n2 then - (E.eps_add_constraint n1 (rep,lvopt,n2,putonly); - E.eps_add_constraint n2 (rep,lvopt,n1,putonly); + (E.eps_add_constraint n1 (false,rep,nil,lvopt,n2,putonly); + E.eps_add_constraint n2 (false,rep,nil,lvopt,n1,putonly); B) else deepErr e2 "expecting explicit effect variable" else if E.is_rho n1 then @@ -382,7 +383,7 @@ struct (case lookRegVar e of SOME n => if E.is_arrow_effect n then (* MEMO: ok, but add constraint *) - (E.eps_add_prop_constraint n (rep,lvopt,p); B) + (E.eps_add_prop_constraint n (false,rep,lvopt,p); B) else deepErr e "expecting explicit effect variable" | NONE => deepErr e "effect variable not in scope") | _ => die "unimplemented PROPconstr") @@ -640,7 +641,7 @@ struct let val children = if print_effects() then (*print regions and effect and -perhaps- types: *) - rho_trees @ map lay_node_short epsilons @ + rho_trees @ map E.layout_effect_binding epsilons @ (if !Flags.print_types then map layout_tyvar' alphas else []) else (if print_regions() then rho_trees @@ -728,6 +729,16 @@ struct fun cp_rho rho = cp_var rho fun cp_eps eps = cp_var eps + fun cp_atomic ae = + if E.is_arrow_effect ae then #2(cp_eps ae) + else if E.is_put ae then + E.mkPut(#2(cp_rho(E.rho_of ae))) + else if E.is_get ae then + E.mkGet(#2(cp_rho(E.rho_of ae))) + else if E.is_mut ae then + E.mkMut(#2(cp_rho(E.rho_of ae))) + else if E.is_rho ae then die "cp_atomic.expects atomic effect - got rho!" + else die "cp_atomic.expects atomic effect - not a rho" fun cp_ty ty = case ty of @@ -797,20 +808,23 @@ struct val () = List.app E.setInstance Se val () = List.app (fn (s,t) => let val pcs = E.eps_get_prop_constraints s (* copy constraints to target *) - in List.app (fn (rep,lv,p) => + in List.app (fn (_,rep,lv,p) => let val rep' = Report.line ("Instance " ^ E.pp_eff s ^ " -> " ^ E.pp_eff t ^ ".") - in E.eps_add_prop_constraint t (Report.//(rep,rep'),lvopt,p) + in E.eps_add_prop_constraint t (true,Report.//(rep,rep'),lvopt,p) end) pcs end) Se val () = List.app (fn (s,t) => let val cs = E.eps_get_constraints s (* copy constraints to target *) - in List.app (fn (rep,lv,e,p) => - let val e' = #2(cp_eps e) + in List.app (fn (_,rep,il,lv,ae,p) => + let val ae' = cp_atomic ae +(* val rep' = Report.line ("Instance " ^ E.pp_eff e ^ " -> " ^ E.pp_eff e' ^ " and " ^ E.pp_eff s ^ " -> " ^ E.pp_eff t ^ ".") - in E.eps_add_constraint t (Report.//(rep,rep'),lvopt,e',p) +*) + val il' = (ae,ae')::(s,t)::il + in E.eps_add_constraint t (true,rep,il',lvopt,ae',p) end) cs end) Se diff --git a/src/Compiler/Regions/RegionExp.sml b/src/Compiler/Regions/RegionExp.sml index 83852f660..a415fdb26 100644 --- a/src/Compiler/Regions/RegionExp.sml +++ b/src/Compiler/Regions/RegionExp.sml @@ -198,6 +198,56 @@ and mkPhiExp e acc = fun mkPhi (tr,exported_regvars_and_arroweffects) = mkPhiTr tr exported_regvars_and_arroweffects +fun letregionBound tr = + let + fun sw f (SWITCH(tr0, l, opt)) acc = + f tr0 (foldl (uncurry f) acc + (cons_if_there(opt,map #2 l))) + fun f (TR(e,_,_)) acc = g e acc + and g e acc = + case e of + UB_RECORD ts => foldl (uncurry f) acc ts + | FN {body, ...} => f body acc + | LETREGION_B{B, body, ...} => f body (!B @ acc) + | LET{pat,bind,scope} => f scope (f bind acc) + | FIX{shared_clos,functions,scope} => + let val acc' = foldl (fn ({epss as ref arreffs,bind, ...}, acc) => + f bind acc) + acc functions + in f scope acc' + end + | APP(tr1, tr2) => f tr1 (f tr2 acc) + | EXCEPTION(_,_,_,_, tr) => f tr acc + | RAISE tr => f tr acc + | HANDLE(tr1, tr2) => f tr1 (f tr2 acc) + | SWITCH_I {switch,...} => sw f switch acc + | SWITCH_W {switch,...} => sw f switch acc + | SWITCH_S switch => sw f switch acc + | SWITCH_C switch => sw f switch acc + | SWITCH_E switch => sw f switch acc + | CON0 _ => acc + | CON1 (_,tr) => f tr acc + | DECON (_,tr) => f tr acc + | EXCON (_,NONE) => acc + | EXCON (_,SOME(_,tr)) => f tr acc + | DEEXCON (_,tr) => f tr acc + | RECORD (_,trs) => foldl (uncurry f) acc trs + | SELECT (_,tr) => f tr acc + | DEREF tr => f tr acc + | REF (_,tr) => f tr acc + | DROP tr => f tr acc + | ASSIGN (tr1,tr2) => f tr1 (f tr2 acc) + | EQUAL (_,tr1,tr2) => f tr1 (f tr2 acc) + | CCALL (_,trs) => foldl (uncurry f) acc trs + | BLOCKF64 (_,trs) => foldl (uncurry f) acc trs + | SCRATCHMEM _ => acc + | EXPORT (_,tr) => f tr acc + | RESET_REGIONS (_, tr) => f tr acc + | FRAME _ => acc + | _ => acc + in f tr nil + end + (*****************************) (* *) (* Pretty printing *) diff --git a/src/Compiler/reml.mlb b/src/Compiler/reml.mlb new file mode 100644 index 000000000..56ae021d9 --- /dev/null +++ b/src/Compiler/reml.mlb @@ -0,0 +1,45 @@ +local + prebackend.mlb + basis Regions = bas regions.mlb end + open BasLib (* Compiler *) Regions +in + (* Native Backend *) + + Backend/LINE_STMT.sml + Backend/REG_ALLOC.sml + Backend/FETCH_AND_FLUSH.sml + Backend/CALC_OFFSET.sml + Backend/SUBST_AND_SIMPLIFY.sml + local open Tools + in + local open CompilerObjects + in Backend/LineStmt.sml + local open Pickle in Backend/RegAlloc.sml end + Backend/FetchAndFlush.sml + local open Edlib in Backend/CalcOffset.sml end + Backend/SubstAndSimplify.sml + Backend/NativeCompile.sml + end + end + + (* X86 Backend *) + Backend/CODE_GEN.sml + Backend/X64/INSTS_X64.sml + ../Kitlib/kitlib.mlb + local open Tools + in + local open CompilerObjects + in local open Pickle in Backend/X64/InstsX64.sml end + Backend/X64/CodeGenUtilX64.sml + Backend/X64/CodeGenX64.sml + local open Pickle Basics Manager + in Backend/X64/ExecutionX64.sml + end + end + + local open Compiler + in ../Common/KitReML.sml + end + + end +end diff --git a/src/Makefile.in b/src/Makefile.in index a2ba9b9ec..6ed384293 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -48,6 +48,11 @@ smltojs: basics mlbmake mllex-yacc $(MLCOMP) -output smltojs Compiler/smltojs.mlb $(INSTALL) -p smltojs $(BINDIR) +.PHONY: reml +reml: mlkit_tools mlkit_runtime + $(MLCOMP) -output reml Compiler/reml.mlb + $(INSTALL) -p reml $(BINDIR) + .PHONY: mllex-yacc mllex-yacc: Parsing/Topdec.lex.sml Parsing/Topdec.grm.sml diff --git a/src/Manager/Manager.sml b/src/Manager/Manager.sml index eeecb2e0f..4dfd640c0 100644 --- a/src/Manager/Manager.sml +++ b/src/Manager/Manager.sml @@ -769,7 +769,7 @@ functor Manager(structure ManagerObjects : MANAGER_OBJECTS of Posix.Process.W_EXITED => (remove pid ; pid) | Posix.Process.W_EXITSTATUS n => (remove pid ; killrest (); raise IsolateFunExn (Word8.toInt n)) | Posix.Process.W_STOPPED s => (remove pid ; killrest (); failSig "W_STOPPED" s) - | Posix.Process.W_SIGNALED s => (remove pid ; killrest (); failSig "W_SIGNALED" s) + | Posix.Process.W_SIGNALED s => (remove pid ; killrest (); failSig "W_SIGNALED - wait" s) end handle OS.SysErr t => (killrest (); failSig "OS.SysErr" (Posix.Signal.fromWord 0w0)) fun isolate (f : 'a -> unit) (a:'a) : unit = @@ -781,14 +781,13 @@ functor Manager(structure ManagerObjects : MANAGER_OBJECTS Posix.Process.W_EXITED => () | Posix.Process.W_EXITSTATUS n => raise IsolateFunExn (Word8.toInt n) | Posix.Process.W_STOPPED s => failSig "W_STOPPED" s - | Posix.Process.W_SIGNALED s => failSig "W_SIGNALED" s) + | Posix.Process.W_SIGNALED s => failSig "W_SIGNALED - isolate" s) else raise Fail "isolate error 2" end | NONE => (f a before Posix.Process.exit 0w0 (* child *) handle e => (errSubProcess NONE e; Posix.Process.exit 0w1)) - end local diff --git a/src/Manager/ManagerObjects.sml b/src/Manager/ManagerObjects.sml index 1c950c962..48b9cf2b3 100644 --- a/src/Manager/ManagerObjects.sml +++ b/src/Manager/ManagerObjects.sml @@ -118,13 +118,6 @@ functor ManagerObjects( in if OS.Path.file p = filename then p else p ^ "." ^ filename end else -(* - let - val target_filename = OS.Path.base(OS.Path.file absprjid) ^ "-" ^ esc filename - val target_filename = pmdir() ^ target_filename - in OS.Path.mkAbsolute{path=target_filename, relativeTo=OS.FileSys.getDir()} - end -*) let val {dir,file} = OS.Path.splitDirFile filename val target_filename = OS.Path.base(OS.Path.file absprjid) ^ "-" ^ file val target_filename = mlbdir() ## target_filename @@ -179,9 +172,9 @@ functor ManagerObjects( end end - fun unsafe(tf,li) = Execution.unsafe_linkinfo li - fun exports(tf,li) = Execution.exports_of_linkinfo li - fun imports(tf,li) = Execution.imports_of_linkinfo li + fun unsafe (tf,li) = Execution.unsafe_linkinfo li + fun exports (tf,li) = Execution.exports_of_linkinfo li + fun imports (tf,li) = Execution.imports_of_linkinfo li fun dead_code_elim tfiles_with_linkinfos = let val _ = pr_debug_linking "[Link time dead code elimination begin...]\n" @@ -264,7 +257,7 @@ functor ManagerObjects( struct val empty = EMPTY_MODC val seq = SEQ_MODC - fun mk_modcode(t,l,f) = NOTEMITTED_MODC(t,l,f) + fun mk_modcode (t,l,f) = NOTEMITTED_MODC(t,l,f) fun exist EMPTY_MODC = true | exist (SEQ_MODC(mc1,mc2)) = exist mc1 andalso exist mc2 @@ -275,7 +268,7 @@ functor ManagerObjects( else (print ("File " ^ file ^ " not present\n"); res) end - fun emit(absprjid: absprjid, modc) = + fun emit (absprjid: absprjid, modc) = let fun em EMPTY_MODC = EMPTY_MODC | em (SEQ_MODC(modc1,modc2)) = SEQ_MODC(em modc1, em modc2) @@ -329,12 +322,6 @@ functor ManagerObjects( | EMPTY_MODC => 0 | EMITTED_MODC(tfile,_) => 1 | NOTEMITTED_MODC _ => 0 -(* - fun timeStampFileName absprjid = - let val base_absprjid = OS.Path.base(OS.Path.file(ModuleEnvironments.absprjid_to_string absprjid)) - in "PM/" ^ base_absprjid ^ ".timestamp" - end -*) fun list_minus (xs,nil) = xs | list_minus (x::xs,y::ys) = diff --git a/src/Manager/ManagerObjects0.sml b/src/Manager/ManagerObjects0.sml index fbe788e70..e8e646dc6 100644 --- a/src/Manager/ManagerObjects0.sml +++ b/src/Manager/ManagerObjects0.sml @@ -58,7 +58,7 @@ functor ManagerObjects0(structure Execution : EXECUTION) (PP.LEAF o SigId.pr_SigId) (TyName.Set.layoutSet {start="{",finish="}",sep=", "} (PP.LEAF o TyName.pr_TyName)) ise - fun layoutIntBasis(IB(ife,ise,ce,cb)) = + fun layoutIntBasis (IB(ife,ise,ce,cb)) = PP.NODE{start="IntBasis = [", finish="]", indent=1, childsep=PP.RIGHT ", ", children=[layoutIntFunEnv ife, layoutIntSigEnv ise, @@ -166,7 +166,7 @@ functor ManagerObjects0(structure Execution : EXECUTION) of SOME e => SigId.Map.add(sigid,e,acc) | NONE => die ("IntSigEnv.restrict: could not find sigid " ^ SigId.pr_SigId sigid)) SigId.Map.empty sigids) - fun enrich(ISE ise0, ISE ise) : bool = + fun enrich (ISE ise0, ISE ise) : bool = SigId.Map.Fold(fn ((sigid, T), b) => b andalso case SigId.Map.lookup ise0 sigid of SOME T0 => TyName.Set.eq T T0 @@ -299,7 +299,7 @@ functor ManagerObjects0(structure Execution : EXECUTION) in IB (ife',ise',ce',cb'') end - fun match(IB(ife1,ise1,ce1,cb1),IB(ife2,ise2,ce2,cb2)) = + fun match (IB(ife1,ise1,ce1,cb1),IB(ife2,ise2,ce2,cb2)) = let val _ = CompilerEnv.match(ce1,ce2) val cb1' = CompileBasis.match(cb1,cb2) in IB(ife1,ise1,ce1,cb1') @@ -314,13 +314,13 @@ functor ManagerObjects0(structure Execution : EXECUTION) fun CompilerEnv_enrichCEnv a = db_f "CompilerEnv" (CompilerEnv.enrichCEnv a) fun CompileBasis_enrich a = db_f "CompileBasis" (CompileBasis.enrich a) in - fun enrich(IB(ife0,ise0,ce0,cb0),IB(ife,ise,ce,cb)) = + fun enrich (IB(ife0,ise0,ce0,cb0),IB(ife,ise,ce,cb)) = IntFunEnv_enrich(ife0,ife) andalso IntSigEnv_enrich(ise0,ise) andalso CompilerEnv_enrichCEnv(ce0,ce) andalso CompileBasis_enrich(cb0,cb) end local - fun agree1(longstrid, (_,_,ce1,cb1), (_,_,ce2,cb2)) = + fun agree1 (longstrid, (_,_,ce1,cb1), (_,_,ce2,cb2)) = let val ce1 = CompilerEnv.lookup_longstrid ce1 longstrid val ce2 = CompilerEnv.lookup_longstrid ce2 longstrid in @@ -440,11 +440,6 @@ functor ManagerObjects0(structure Execution : EXECUTION) fun closure (B': Basis, B: Basis) : Basis = (* closure_B'(B) : the closure of B w.r.t. B' *) -(*was: - let val dom = domain B - in #1 (restrict(plus(B',B),dom)) - end -*) let val BASIS(infB',eB',oe',iB') = B' val BASIS(infB,eB,oe,iB) = B (* @@ -504,17 +499,17 @@ functor ManagerObjects0(structure Execution : EXECUTION) type Basis1 = opaq_env * IntBasis val pu_Basis1 = puSay "Basis1" (Pickle.pairGen(OpacityEnv.pu, IntBasis.pu)) - fun plusBasis1((oe,ib),(oe',ib')) = + fun plusBasis1 ((oe,ib),(oe',ib')) = (OpacityEnv.plus(oe,oe'), IntBasis.plus(ib,ib')) - fun initialBasis1() = (OpacityEnv.initial, - IntBasis.initial()) + fun initialBasis1 () = (OpacityEnv.initial, + IntBasis.initial()) fun matchBasis1 ((oe,iB), (oe0,iB0)) = let val _ = OpacityEnv.match(oe,oe0) val iB = IntBasis.match(iB,iB0) in (oe,iB) end - fun eqBasis1((oe1,iB1), (oe2,iB2)) = + fun eqBasis1 ((oe1,iB1), (oe2,iB2)) = db_f "OpacityEnv" (OpacityEnv.eq(oe1,oe2)) andalso db_f "IB_l" (IntBasis.enrich(iB1,iB2)) andalso db_f "IB_r" (IntBasis.enrich(iB2,iB1)) diff --git a/src/Parsing/LEX_UTILS.sml b/src/Parsing/LEX_UTILS.sml index b8c6c67d8..1de5b673a 100644 --- a/src/Parsing/LEX_UTILS.sml +++ b/src/Parsing/LEX_UTILS.sml @@ -43,6 +43,4 @@ signature LEX_UTILS = val parStackPop : LexArgument -> unit val parStackIsEmpty : LexArgument -> bool - val explicit_regions : bool ref (* if set, the lexer will support - * 'region' tokens *) - end; + end diff --git a/src/Parsing/LexUtils.sml b/src/Parsing/LexUtils.sml index 9f0c328f0..3d439af4f 100644 --- a/src/Parsing/LexUtils.sml +++ b/src/Parsing/LexUtils.sml @@ -153,11 +153,18 @@ functor LexUtils(Token: Topdec_TOKENS): LEX_UTILS = fun asString (LEX_ARGUMENT{stringChars, ...}) = concat(rev (!stringChars)) - val explicit_regions = ref false - val _ = Flags.add_bool_entry - {long="explicit_regions", short=SOME "er", neg=false, item=explicit_regions, - menu=["Control", "Explicit regions"], - desc="Support programming with explicit regions."} + val is_reml = + let val reml = ref false + in Flags.add_bool_entry + {long="reml", short=NONE, item=reml, + menu=["Control", "ReML"], neg=false, + desc="ReML is Standard ML with support for programming with \n\ + \explicit regions, explicit effects, and effect \n\ + \constraints. With ReML, atomic effects also include \n\ + \mutation effects. Whereas ReML include parallel \n\ + \thread support, ReML does not support integration \n\ + \with reference-tracing garbage collection."} + end (* Keyword detection (better done here than by the lexer). *) @@ -217,7 +224,7 @@ functor LexUtils(Token: Topdec_TOKENS): LEX_UTILS = | "#" => keyword HASH | "*" => keyword STAR (* Not actually reserved, but ... *) - | _ => if !explicit_regions then + | _ => if is_reml() then if text = "`" then keyword BACKQUOTE else if text = "##" then keyword HASHHASH else ID(text, p1, p2) diff --git a/src/Parsing/PARSE.sig b/src/Parsing/PARSE.sig index ab9c02d22..c858f6faf 100644 --- a/src/Parsing/PARSE.sig +++ b/src/Parsing/PARSE.sig @@ -28,10 +28,6 @@ signature PARSE = (EOF in the middle of a phrase is an error) *) - val explicit_regions : bool ref (* support parsing of explicit region - * annotations, such as 'region' - * declarations. *) - val begin: SourceReader -> State val parse: InfixBasis * State -> Result end diff --git a/src/Parsing/Parse.sml b/src/Parsing/Parse.sml index cfa551512..74fdbd21a 100644 --- a/src/Parsing/Parse.sml +++ b/src/Parsing/Parse.sml @@ -120,9 +120,7 @@ structure Parse: PARSE = STATE stream end - val explicit_regions = LexUtils.explicit_regions - - fun parse(ib, state) = + fun parse (ib, state) = (case parseStream state of PS_SUCCESS(topdec, state') => (case Infixing.resolve(ib, topdec) of diff --git a/src/Runtime/Posix.c b/src/Runtime/Posix.c index 7fe2e8550..6dbd937fc 100644 --- a/src/Runtime/Posix.c +++ b/src/Runtime/Posix.c @@ -1011,14 +1011,17 @@ int getlogin_r(char *buf, size_t bufsize); String REG_POLY_FUN_HDR(sml_getlogin, Region rs) { - String s; int r; - s = REG_POLY_CALL(allocStringC,rs, L_cuserid + 8); /* was 1 - hmm*/ - r = getlogin_r(&(s->data), L_cuserid); - if (r != 0) - { + char* buf = (char*) malloc(L_cuserid+1); + if (!buf) return NULL; + r = getlogin_r(buf, L_cuserid); + buf[L_cuserid] = '\0'; + if (r != 0) { + free(buf); return NULL; } + String s = REG_POLY_CALL(convertStringToML, rs, buf); + free(buf); return s; } diff --git a/test/explicit_regions/Makefile b/test/explicit_regions/Makefile index 55d09efeb..24045106b 100644 --- a/test/explicit_regions/Makefile +++ b/test/explicit_regions/Makefile @@ -1,5 +1,5 @@ -FLAGS=-no_gc -no_basislib --maximum_inline_size 0 -er -no_opt -MLKIT=../../bin/mlkit $(FLAGS) +FLAGS=-no_basislib --maximum_inline_size 0 -no_opt +REML=../../bin/reml $(FLAGS) SMLSOURCES=er*.sml param.sml rec.sml tup.sml call.sml call2.sml ty1.sml err_expty1.sml err_expty2.sml \ err_expty3.sml err_patty1.sml err_funty1.sml err_funty2.sml err_funty3.sml expty1.sml expty2.sml \ @@ -7,7 +7,7 @@ SMLSOURCES=er*.sml param.sml rec.sml tup.sml call.sml call2.sml ty1.sml err_expt .PHONY: all all: - ../../bin/kittester "$(MLKIT)" --logdirect all.tst + ../../bin/kittester "SML_LIB=../.. $(REML)" --logdirect all.tst all.sml: $(SMLSOURCES) echo '(* Testfiles *)' > $@ diff --git a/test/explicit_regions/all.tst b/test/explicit_regions/all.tst index 76b5c6daf..670755334 100644 --- a/test/explicit_regions/all.tst +++ b/test/explicit_regions/all.tst @@ -80,4 +80,8 @@ nomut-ok.sml (* Satisfiability of nomut constraint on funct nomut2-err.sml ccl ecte (* Violation of nomut constraint on function instantiation *) disputs.sml ccl ecte (* Violation of disjoint put-effects (##) - let rec *) -disputs2.sml ccl ecte (* Violation of disjoint put-effects (##) - fun *) \ No newline at end of file +disputs2.sml ccl ecte (* Violation of disjoint put-effects (##) - fun *) + +par.sml (* A sound implementation of par with constraint *) +par-no.sml ccl ecte (* But it needs to be satisfied *) +par-no2.sml ccl ecte (* The trivial definition of par is not ok *) \ No newline at end of file diff --git a/test/explicit_regions/disputs.sml.log.ok b/test/explicit_regions/disputs.sml.log.ok index 86d703ed2..6a2bc624d 100644 --- a/test/explicit_regions/disputs.sml.log.ok +++ b/test/explicit_regions/disputs.sml.log.ok @@ -3,7 +3,8 @@ disputs.sml, line 5, column 79: val rec par `[e1 e2] : (unit #e1 -> 'a) -> (unit #e2 -> 'b) -> ('a * 'b) while e1 ## e2 = ^^^^^^^^ -Instance `e1 -> e32 and `e2 -> e28. +Instance `e1_12 -> e32 +Instance `e2_10 -> e28 Put-constraint violation. The effect e28 contains the atomic effect put(r29), which also appears in the effect of e32 Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/disputs2.sml.log.ok b/test/explicit_regions/disputs2.sml.log.ok index d1cf97d73..1399bdd49 100644 --- a/test/explicit_regions/disputs2.sml.log.ok +++ b/test/explicit_regions/disputs2.sml.log.ok @@ -3,7 +3,8 @@ disputs2.sml, line 5, column 75: fun par `[e1 e2] (f: unit #e1 -> 'a) (g: unit #e2 -> 'b) : ('a * 'b) while e1 ## e2 = ^^^^^^^^ -Instance `e1 -> e28 and `e2 -> e24. +Instance `e1_12 -> e28 +Instance `e2_10 -> e24 Put-constraint violation. The effect e24 contains the atomic effect put(r31), which also appears in the effect of e28 Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/nomut-err.sml.log.ok b/test/explicit_regions/nomut-err.sml.log.ok index 20a1f5ec7..c0ec69416 100644 --- a/test/explicit_regions/nomut-err.sml.log.ok +++ b/test/explicit_regions/nomut-err.sml.log.ok @@ -4,6 +4,6 @@ nomut-err.sml, line 14, column 39: val rec g `e : (unit #e -> unit) while nomut e = ^^^^^^^ -Mutation constraint violation. The effect `e contains +Mutation constraint violation. The effect `e_44 contains the atomic effect mut(r6) Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/nomut2-err.sml.log.ok b/test/explicit_regions/nomut2-err.sml.log.ok index 0fdf8c32b..c003a15b4 100644 --- a/test/explicit_regions/nomut2-err.sml.log.ok +++ b/test/explicit_regions/nomut2-err.sml.log.ok @@ -7,5 +7,5 @@ nomut2-err.sml, line 28, column 91: ^^^^^^^^^ Instance `eee -> e88. Mutation constraint violation. The effect e88 contains -the atomic effect mut(r6) +the atomic effect e92, which has no nomut property Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/par-no.sml b/test/explicit_regions/par-no.sml new file mode 100644 index 000000000..ce27e12dd --- /dev/null +++ b/test/explicit_regions/par-no.sml @@ -0,0 +1,34 @@ +local + fun print (s:string) : unit = + prim("printStringML", s) + + fun alloc_unsafe (n:int) : 'a array = + prim ("word_table0", n) + + fun update_unsafe (a : 'a array, i : int, x : 'a) : unit = + prim ("word_update0", (a, i, x)) + + fun sub_unsafe (a : 'a array, i : int) : 'a = + prim ("word_sub0", (a, i)) + + fun sp__noinline `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + k (f()) + + fun get__noinline x = x +in + + fun spawn `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + sp__noinline f k + + fun get x = get__noinline x + + fun par `[e1 e2] (f: unit #e1 -> 'a, g: unit #e2 -> 'b) : 'a * 'b (* while e1 ## e2 *) = (* constraint needed *) + let val a1 : 'a array = alloc_unsafe 1 + val b1 : 'b array = alloc_unsafe 1 + in spawn (fn () => update_unsafe(b1,0,g())) (fn _ => (update_unsafe(a1,0,f()))) + ; (sub_unsafe(a1,0), sub_unsafe(b1,0)) + end + + val () = print "Done\n" + +end diff --git a/test/explicit_regions/par-no.sml.log.ok b/test/explicit_regions/par-no.sml.log.ok new file mode 100644 index 000000000..43dd14b57 --- /dev/null +++ b/test/explicit_regions/par-no.sml.log.ok @@ -0,0 +1,13 @@ +[reading source file: par-no.sml] +> val get : 'a->'a + val par : (unit-e1->'a) * (unit-e2->'b)->'a * 'b + val spawn : (unit-e1->'a)->('a-e2->'b)->'b +par-no.sml, line 14, column 79: + fun sp__noinline `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + ^^^^^^^^ +Instance `e1_60 -> e106 +Instance `e2_58 -> e102 +Instance `e1_44 -> `e1_60 +Instance `e2_42 -> `e2_58 +Put-constraint violation. Constraint not discharged by a satisfying constraint. +Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/par-no2.sml b/test/explicit_regions/par-no2.sml new file mode 100644 index 000000000..7de2b86c5 --- /dev/null +++ b/test/explicit_regions/par-no2.sml @@ -0,0 +1,32 @@ +local + fun print (s:string) : unit = + prim("printStringML", s) + + fun alloc_unsafe (n:int) : 'a array = + prim ("word_table0", n) + + fun update_unsafe (a : 'a array, i : int, x : 'a) : unit = + prim ("word_update0", (a, i, x)) + + fun sub_unsafe (a : 'a array, i : int) : 'a = + prim ("word_sub0", (a, i)) + + fun sp__noinline `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + k (f()) + + fun get__noinline x = x +in + + fun spawn `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + sp__noinline f k + + fun get x = get__noinline x + + (* The below is not ok as there is no guarantee that g also stores values in the pair-region... *) + + fun par `[e1 e2] (f: unit #e1 -> 'a, g: unit #e2 -> 'b) : 'a * 'b while e1 ## e2 = + spawn g (fn t => (f(), get t)) + + val () = print "Done\n" + +end diff --git a/test/explicit_regions/par-no2.sml.log.ok b/test/explicit_regions/par-no2.sml.log.ok new file mode 100644 index 000000000..e804172d5 --- /dev/null +++ b/test/explicit_regions/par-no2.sml.log.ok @@ -0,0 +1,14 @@ +[reading source file: par-no2.sml] +> val get : 'a->'a + val par : (unit-e1->'a) * (unit-e2->'b)->'a * 'b + val spawn : (unit-e1->'a)->('a-e2->'b)->'b +par-no2.sml, line 14, column 79: + fun sp__noinline `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + ^^^^^^^^ +Instance `e1_60 -> `e2_84 +Instance `e2_58 -> e92 +Instance `e1_44 -> `e1_60 +Instance `e2_42 -> `e2_58 +Put-constraint violation. The effect e92 contains +the atomic effect put(r125), which also appears in the effect of `e2_84 +Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/par.sml b/test/explicit_regions/par.sml new file mode 100644 index 000000000..1272dae07 --- /dev/null +++ b/test/explicit_regions/par.sml @@ -0,0 +1,34 @@ +local + fun print (s:string) : unit = + prim("printStringML", s) + + fun alloc_unsafe (n:int) : 'a array = + prim ("word_table0", n) + + fun update_unsafe (a : 'a array, i : int, x : 'a) : unit = + prim ("word_update0", (a, i, x)) + + fun sub_unsafe (a : 'a array, i : int) : 'a = + prim ("word_sub0", (a, i)) + + fun sp__noinline `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + k (f()) + + fun get__noinline x = x +in + + fun spawn `[e1 e2] (f: unit #e1 -> 'a) (k: 'a #e2 -> 'b) : 'b while e1 ## e2 = + sp__noinline f k + + fun get x = get__noinline x + + fun par `[e1 e2] (f: unit #e1 -> 'a, g: unit #e2 -> 'b) : 'a * 'b while e1 ## e2 = + let val a1 : 'a array = alloc_unsafe 1 + val b1 : 'b array = alloc_unsafe 1 + in spawn (fn () => update_unsafe(b1,0,g())) (fn _ => (update_unsafe(a1,0,f()))) + ; (sub_unsafe(a1,0), sub_unsafe(b1,0)) + end + + val () = print "Done\n" + +end diff --git a/test/explicit_regions/par.sml.out.ok b/test/explicit_regions/par.sml.out.ok new file mode 100644 index 000000000..a965a70ed --- /dev/null +++ b/test/explicit_regions/par.sml.out.ok @@ -0,0 +1 @@ +Done