From da394cfc931139dbd3a688679dcbddf5ce2e846e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 16 Dec 2018 14:58:07 -0500 Subject: Specialize: stay clear of datatypes that are used polymorphically --- src/specialize.sml | 106 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 60 insertions(+), 46 deletions(-) (limited to 'src/specialize.sml') diff --git a/src/specialize.sml b/src/specialize.sml index 33545250..9dc2cf1b 100644 --- a/src/specialize.sml +++ b/src/specialize.sml @@ -44,6 +44,7 @@ end structure CM = BinaryMapFn(CK) structure IM = IntBinaryMap +structure IS = IntBinarySet type datatyp' = { name : int, @@ -61,7 +62,7 @@ type state = { count : int, datatypes : datatyp IM.map, constructors : int IM.map, - decls : (string * int * string list * (string * int * con option) list) list + decls : (string * int * string list * (string * int * con option) list) list } fun kind (k, st) = (k, st) @@ -72,6 +73,12 @@ val isOpen = U.Con.exists {kind = fn _ => false, CRel _ => true | _ => false} +fun findApp (c, args) = + case c of + CApp ((c', _), arg) => findApp (c', arg :: args) + | CNamed n => SOME (n, args) + | _ => NONE + fun considerSpecialization (st : state, n, args, dt : datatyp) = let val args = map ReduceLocal.reduceCon args @@ -132,31 +139,20 @@ fun considerSpecialization (st : state, n, args, dt : datatyp) = end and con (c, st : state) = - let - fun findApp (c, args) = - case c of - CApp ((c', _), arg) => findApp (c', arg :: args) - | CNamed n => SOME (n, args) - | _ => NONE - in - case findApp (c, []) of - SOME (n, args as (_ :: _)) => - if List.exists isOpen args then - (c, st) - else - (case IM.find (#datatypes st, n) of - NONE => (c, st) - | SOME dt => - if length args <> #params dt then - (c, st) - else - let - val (n, _, st) = considerSpecialization (st, n, args, dt) - in - (CNamed n, st) - end) - | _ => (c, st) - end + case findApp (c, []) of + SOME (n, args as ((_, loc) :: _)) => + (case IM.find (#datatypes st, n) of + NONE => (c, st) + | SOME dt => + if length args <> #params dt then + (c, st) + else + let + val (n, _, st) = considerSpecialization (st, n, args, dt) + in + (CNamed n, st) + end) + | _ => (c, st) and specCon st = U.Con.foldMap {kind = kind, con = con} st @@ -252,6 +248,21 @@ val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} fun specialize file = let + val fancyDatatypes = U.File.fold {kind = fn (_, fd) => fd, + exp = fn (_, fd) => fd, + decl = fn (_, fd) => fd, + con = fn (c, fd) => + case c of + CApp (c1, c2) => + if isOpen c2 then + case findApp (c, []) of + SOME (n, _) => IS.add (fd, n) + | NONE => fd + else + fd + | _ => fd} + IS.empty file + fun doDecl (d, st) = let (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) @@ -259,23 +270,26 @@ fun specialize file = in case #1 d of DDatatype dts => - ((case #decls st of - [] => [d] - | dts' => [(DDatatype (dts' @ dts), #2 d)]), - {count = #count st, - datatypes = foldl (fn ((x, n, xs, xnts), dts) => - IM.insert (dts, n, - {name = x, - params = length xs, - constructors = xnts, - specializations = CM.empty})) - (#datatypes st) dts, - constructors = foldl (fn ((x, n, xs, xnts), cs) => - foldl (fn ((_, n', _), constructors) => - IM.insert (constructors, n', n)) + if List.exists (fn (_, n, _, _) => IS.member (fancyDatatypes, n)) dts then + ([d], st) + else + ((case #decls st of + [] => [d] + | dts' => [(DDatatype (dts' @ dts), #2 d)]), + {count = #count st, + datatypes = foldl (fn ((x, n, xs, xnts), dts) => + IM.insert (dts, n, + {name = x, + params = length xs, + constructors = xnts, + specializations = CM.empty})) + (#datatypes st) dts, + constructors = foldl (fn ((x, n, xs, xnts), cs) => + foldl (fn ((_, n', _), constructors) => + IM.insert (constructors, n', n)) cs xnts) - (#constructors st) dts, - decls = []}) + (#constructors st) dts, + decls = []}) | _ => (case #decls st of [] => [d] @@ -287,10 +301,10 @@ fun specialize file = end val (ds, _) = ListUtil.foldlMapConcat doDecl - {count = U.File.maxName file + 1, - datatypes = IM.empty, - constructors = IM.empty, - decls = []} file + {count = U.File.maxName file + 1, + datatypes = IM.empty, + constructors = IM.empty, + decls = []} file in ds end -- cgit v1.2.3 From 7578916b630bd84ec3f8e7d97aaaa1cc7828e5ef Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 16 Dec 2018 16:45:37 -0500 Subject: Specialize: ignore recursive references in classifying polymorphic uses of datatypes --- src/compiler.sig | 1 + src/compiler.sml | 3 ++- src/core_util.sig | 6 ++++++ src/core_util.sml | 16 ++++++++++++++++ src/specialize.sml | 34 +++++++++++++++++++++++++++++++--- 5 files changed, 56 insertions(+), 4 deletions(-) (limited to 'src/specialize.sml') diff --git a/src/compiler.sig b/src/compiler.sig index 7922393d..09c913f8 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -164,6 +164,7 @@ signature COMPILER = sig val toUnpoly2 : (string, Core.file) transform val toShake4'' : (string, Core.file) transform val toEspecialize3 : (string, Core.file) transform + val toSpecialize3 : (string, Core.file) transform val toReduce2 : (string, Core.file) transform val toShake5 : (string, Core.file) transform val toMarshalcheck : (string, Core.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 271cf2f1..e7de4d82 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1390,8 +1390,9 @@ val toUnpoly2 = transform unpoly "unpoly2" o toShake4' val toSpecialize2 = transform specialize "specialize2" o toUnpoly2 val toShake4'' = transform shake "shake4'" o toSpecialize2 val toEspecialize3 = transform especialize "especialize3" o toShake4'' +val toSpecialize3 = transform specialize "specialize3" o toEspecialize3 -val toReduce2 = transform reduce "reduce2" o toEspecialize3 +val toReduce2 = transform reduce "reduce2" o toSpecialize3 val toShake5 = transform shake "shake5" o toReduce2 diff --git a/src/core_util.sig b/src/core_util.sig index 835577a3..8d295f1e 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -161,6 +161,12 @@ structure Decl : sig decl : (Core.decl', 'state, 'abort) Search.mapfolder} -> (Core.decl, 'state, 'abort) Search.mapfolder + val map : {kind : Core.kind' -> Core.kind', + con : Core.con' -> Core.con', + exp : Core.exp' -> Core.exp', + decl : Core.decl' -> Core.decl'} + -> Core.decl -> Core.decl + val fold : {kind : Core.kind' * 'state -> 'state, con : Core.con' * 'state -> 'state, exp : Core.exp' * 'state -> 'state, diff --git a/src/core_util.sml b/src/core_util.sml index 57ef16f7..d1d3d9c4 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -1029,6 +1029,22 @@ fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} = decl = fn () => fd, bind = fn ((), _) => ()} () +fun mapB {kind, con, exp, decl, bind} ctx d = + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), + con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), + exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), + decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()), + bind = bind} ctx d () of + S.Continue (d, ()) => d + | S.Return _ => raise Fail "CoreUtil.Decl.mapB: Impossible" + +fun map {kind, con, exp, decl} d = + mapB {kind = fn () => kind, + con = fn () => con, + exp = fn () => exp, + decl = fn () => decl, + bind = fn _ => ()} () d + fun fold {kind, con, exp, decl} s d = case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)), con = fn c => fn s => S.Continue (c, con (c, s)), diff --git a/src/specialize.sml b/src/specialize.sml index 9dc2cf1b..70e646e3 100644 --- a/src/specialize.sml +++ b/src/specialize.sml @@ -248,6 +248,27 @@ val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} fun specialize file = let + (*val () = CorePrint.debug := true + val () = print "SPECIALIZING\n"*) + + (* Let's run around a file, finding any polymorphic uses of a datatype. + * However, don't count polymorphism within a datatype's own definition! + * To that end, we run a silly transform on the file before traversing. *) + val file' = + map (fn d => + case #1 d of + DDatatype dts => + U.Decl.map {kind = fn x => x, + exp = fn x => x, + decl = fn x => x, + con = fn CNamed n => + if List.exists (fn (_, n', _, _) => n' = n) dts then + CUnit + else + CNamed n + | c => c} d + | _ => d) file + val fancyDatatypes = U.File.fold {kind = fn (_, fd) => fd, exp = fn (_, fd) => fd, decl = fn (_, fd) => fd, @@ -256,12 +277,18 @@ fun specialize file = CApp (c1, c2) => if isOpen c2 then case findApp (c, []) of - SOME (n, _) => IS.add (fd, n) + SOME (n, _) => + ((*Print.preface ("Disqualifier", + CorePrint.p_con CoreEnv.empty (c, ErrorMsg.dummySpan));*) + IS.add (fd, n)) | NONE => fd else fd | _ => fd} - IS.empty file + IS.empty file' + + (* Why did we find the polymorphism? + * It would be incoherent to specialize a datatype used polymorphically. *) fun doDecl (d, st) = let @@ -271,7 +298,8 @@ fun specialize file = case #1 d of DDatatype dts => if List.exists (fn (_, n, _, _) => IS.member (fancyDatatypes, n)) dts then - ([d], st) + ((*Print.preface ("Skipping", CorePrint.p_decl CoreEnv.empty d);*) + ([d], st)) else ((case #decls st of [] => [d] -- cgit v1.2.3