From 6a677a770c73855addbca7a7bdacd38676fb9b67 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 10 Jul 2017 00:08:18 -0500 Subject: [PATCH 1/2] Make parseArgs total by handling the case where there is an unrecognized argument --- src/flags.sml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/flags.sml b/src/flags.sml index df21c8f..2f12c21 100644 --- a/src/flags.sml +++ b/src/flags.sml @@ -12,7 +12,9 @@ structure Flags : FLAGS = struct fun parseArgs [] = () | parseArgs ("--latex"::rest) = (flgShouldGenLaTeX := true; parseArgs rest) - | parseArgs ("--steps"::rest) = parseArgs rest | parseArgs ("--out"::file::rest) = (flgOutFile := SOME file; parseArgs rest) + | parseArgs (arg::_) = + (print ("Unrecognized argument: " ^ arg ^ "\n"); + OS.Process.exit OS.Process.failure) end From fae6152d884e65a997e791c83deb44489a83175e Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 10 Jul 2017 00:10:15 -0500 Subject: [PATCH 2/2] Make breakdown total by throwing exception if impossible case happens --- src/ljt.sml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ljt.sml b/src/ljt.sml index d4a0c16..8237a7e 100644 --- a/src/ljt.sml +++ b/src/ljt.sml @@ -123,6 +123,7 @@ structure LJT = struct OneInf (DisjR2, breakdown (G || [] ===> B), goal)) end | breakdown (G || [] ===> C) = searchSync G C + | breakdown _ = raise Fail "breakdown case not supposed to happen" and searchSync G C = case getSome (eliminate C) (allCtxs G) of