Mercurial > urweb
view src/termination.sml @ 1739:c414850f206f
Add support for -boot flag, which allows in-tree execution of Ur/Web
The boot flag rewrites most hardcoded paths to point to the build
directory, and also forces static compilation. This is convenient
for developing Ur/Web, or if you cannot 'sudo make install' Ur/Web.
The following changes were made:
* Header files were moved to include/urweb instead of include;
this lets FFI users point their C_INCLUDE_PATH at this directory
at write <urweb/urweb.h>. For internal Ur/Web executables,
we simply pass -I$PATH/include/urweb as normal.
* Differentiate between LIB and SRCLIB; SRCLIB is Ur and JavaScript
source files, while LIB is compiled products from libtool. For
in-tree compilation these live in different places.
* No longer reference Config for paths; instead use Settings; these
settings can be changed dynamically by Compiler.enableBoot ()
(TODO: add a disableBoot function.)
* config.h is now generated directly in include/urweb/config.h,
for consistency's sake (especially since it gets installed
along with the rest of the headers!)
* All of the autotools build products got updated.
* The linkStatic field in protocols now only contains the name of the
build product, and not the absolute path.
Future users have to be careful not to reference the Settings files
to early, lest they get an old version (this was the source of two
bugs during development of this patch.)
author | Edward Z. Yang <ezyang@mit.edu> |
---|---|
date | Wed, 02 May 2012 17:17:57 -0400 |
parents | 7f871c03e3a1 |
children |
line wrap: on
line source
(* Copyright (c) 2008, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: * * - Redistributions of source code must retain the above copyright notice, * this list of conditions and the following disclaimer. * - Redistributions in binary form must reproduce the above copyright notice, * this list of conditions and the following disclaimer in the documentation * and/or other materials provided with the distribution. * - The names of contributors may not be used to endorse or promote products * derived from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE * POSSIBILITY OF SUCH DAMAGE. *) structure Termination :> TERMINATION = struct open Elab structure E = ElabEnv structure IM = IntBinaryMap structure IS = IntBinarySet datatype pedigree = Func of int | Arg of int * int * con | Subarg of int * int * con | Rabble fun p2s p = case p of Func i => "Func" ^ Int.toString i | Arg (i, j, _) => "Arg" ^ Int.toString i ^ "," ^ Int.toString j | Subarg (i, j, _) => "Subarg" ^ Int.toString i ^ "," ^ Int.toString j | Rabble => "Rabble" fun declOk' env (d, loc) = case d of DValRec vis => let val nfns = length vis val fenv = ListUtil.foldli (fn (i, (_, j, _, _), fenv) => IM.insert (fenv, j, i)) IM.empty vis fun namesEq ((c1, _), (c2, _)) = case (c1, c2) of (CName s1, CName s2) => s1 = s2 | (CRel n1, CRel n2) => n1 = n2 | (CNamed n1, CNamed n2) => n1 = n2 | (CModProj n1, CModProj n2) => n1 = n2 | _ => false fun patCon pc = let fun unravel (t, _) = case t of TCFun (_, _, _, t) => unravel t | TFun (dom, _) => dom | _ => raise Fail "Termination: Unexpected constructor type" in case pc of PConVar i => let val (_, t) = E.lookupENamed env i in unravel t end | PConProj (m1, ms, x) => let val (str, sgn) = E.chaseMpath env (m1, ms) in case E.projectVal env {str = str, sgn = sgn, field = x} of NONE => raise Fail "Termination: Bad constructor projection" | SOME t => unravel t end end fun pat penv (p, (pt, _)) = let fun con (i, j, pc, pt') = pat penv (Subarg (i, j, patCon pc), pt') fun record (i, j, t, xps) = case t of (TRecord (CRecord (_, xts), _), _) => foldl (fn ((x, pt', _), penv) => let val p' = case List.find (fn (x', _) => namesEq ((CName x, ErrorMsg.dummySpan), x')) xts of NONE => Rabble | SOME (_, t) => Subarg (i, j, t) in pat penv (p', pt') end) penv xps | _ => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps in case (p, pt) of (_, PWild) => penv | (_, PVar _) => p :: penv | (_, PPrim _) => penv | (_, PCon (_, _, _, NONE)) => penv | (Arg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt') | (Subarg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt') | (_, PCon (_, _, _, SOME pt')) => pat penv (Rabble, pt') | (Arg (i, j, t), PRecord xps) => record (i, j, t, xps) | (Subarg (i, j, t), PRecord xps) => record (i, j, t, xps) | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps end fun exp parent (penv, calls) e = let val default = (Rabble, calls) fun apps () = let fun combiner calls e = case #1 e of EApp ((ECApp ( (ECApp ( (ECApp ( (ECApp ( (ECApp ( (ECApp ( (ECApp ( (ECApp ( (EModProj (m, [], "tag"), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), (ERecord xets, _)) => let val checkName = case E.lookupStrNamed env m of ("Basis", _) => (fn x : con => case #1 x of CName s => s = "Link" orelse s = "Action" | _ => false) | _ => (fn _ => false) val calls = foldl (fn ((x, e, _), calls) => if checkName x then calls else #2 (exp parent (penv, calls) e)) calls xets in (Rabble, [Rabble], calls) end | EApp (e1, e2) => let val (p1, ps, calls) = combiner calls e1 val (p2, calls) = exp parent (penv, calls) e2 val p = case p1 of Rabble => Rabble | Arg _ => Rabble | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran) | Subarg _ => Rabble | Func _ => Rabble in (p, ps @ [p2], calls) end | ECApp (e, _) => let val (p, ps, calls) = combiner calls e val p = case p of Rabble => Rabble | Arg _ => Rabble | Subarg (i, j, (TCFun (_, _, _, ran), _)) => Subarg (i, j, ran) | Subarg _ => Rabble | Func _ => Rabble in (p, ps, calls) end | EKApp (e, _) => combiner calls e | _ => let val (p, calls) = exp parent (penv, calls) e in (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; print (p2s p ^ "\n");*) (p, [p], calls) end val (p, ps, calls) = combiner calls e val calls = case ps of [] => raise Fail "Termination: Empty ps" | f :: ps => case f of Func i => (parent, i, ps) :: calls | _ => calls in (p, calls) end in case #1 e of EPrim _ => default | ERel n => (List.nth (penv, n), calls) | ENamed n => let val p = case IM.find (fenv, n) of NONE => Rabble | SOME n' => Func n' in (p, calls) end | EModProj _ => default | EApp _ => apps () | EAbs (_, _, _, e) => let val (_, calls) = exp parent (Rabble :: penv, calls) e in (Rabble, calls) end | ECApp _ => apps () | ECAbs (_, _, _, e) => let val (_, calls) = exp parent (penv, calls) e in (Rabble, calls) end | EKApp _ => apps () | EKAbs (_, e) => let val (_, calls) = exp parent (penv, calls) e in (Rabble, calls) end | ERecord xets => let val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets in (Rabble, calls) end | EField (e, x, _) => let val (p, calls) = exp parent (penv, calls) e val p = case p of Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) => (case List.find (fn (x', _) => namesEq (x, x')) xts of NONE => Rabble | SOME (_, t) => Subarg (i, j, t)) | _ => Rabble in (p, calls) end | ECut (e, _, _) => let val (_, calls) = exp parent (penv, calls) e in (Rabble, calls) end | ECutMulti (e, _, _) => let val (_, calls) = exp parent (penv, calls) e in (Rabble, calls) end | EConcat (e1, _, e2, _) => let val (_, calls) = exp parent (penv, calls) e1 val (_, calls) = exp parent (penv, calls) e2 in (Rabble, calls) end | ECase (e, pes, _) => let val (p, calls) = exp parent (penv, calls) e val calls = foldl (fn ((pt, e), calls) => let val penv = pat penv (p, pt) val (_, calls) = exp parent (penv, calls) e in calls end) calls pes in (Rabble, calls) end | EError => (Rabble, calls) | EUnif (ref (SOME e)) => exp parent (penv, calls) e | EUnif (ref NONE) => (Rabble, calls) | ELet (eds, e, _) => let fun extPenv ((ed, _), penv) = case ed of EDVal _ => Rabble :: penv | EDValRec vis => foldl (fn (_, penv) => Rabble :: penv) penv vis in exp parent (foldl extPenv penv eds, calls) e end end fun doVali (i, (_, f, _, e), calls) = let fun unravel (e, j, penv) = case #1 e of EAbs (_, t, _, e) => unravel (e, j + 1, Arg (i, j, t) :: penv) | ECAbs (_, _, _, e) => unravel (e, j, penv) | _ => (j, #2 (exp f (penv, calls) e)) in unravel (e, 0, []) end val (ns, calls) = ListUtil.foldliMap doVali [] vis fun isRecursive (from, to, _) = let fun search (at, soFar) = at = from orelse List.exists (fn (from', to', _) => from' = at andalso not (IS.member (soFar, to')) andalso search (to', IS.add (soFar, to'))) calls in search (to, IS.empty) end val calls = List.filter isRecursive calls fun search (ns, choices) = case ns of [] => let val choices = rev choices in List.all (fn (_, f, args) => let val recArg = List.nth (choices, f) fun isDatatype (t, _) = case t of CNamed _ => true | CModProj _ => true | CApp (t, _) => isDatatype t | _ => false in length args > recArg andalso case List.nth (args, recArg) of Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i) | _ => false end) calls end | n :: ns' => let fun search' i = i < n andalso (search (ns', i :: choices) orelse search' (i + 1)) in search' 0 end in if search (ns, []) then () else ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)" end | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds) | _ => () and declOk (d, env) = (declOk' env d; E.declBinds env d) fun check ds = ignore (foldl declOk E.empty ds) end