Skip to content
Permalink
Browse files

Merge pull request #693 from LawAbidingCactus/rename-compile-error

rename CompileError to AssembleError
  • Loading branch information...
xrchz committed Oct 9, 2019
2 parents b8b2069 + 7b35d2a commit c83d628203cffb295bb21893583d5281d59b5bc5
Showing with 5 additions and 5 deletions.
  1. +3 −3 compiler/compilerScript.sml
  2. +2 −2 compiler/proofs/compilerProofScript.sml
@@ -64,7 +64,7 @@ val _ = Datatype`
; only_print_sexp : bool
|>`;

val _ = Datatype`compile_error = ParseError | TypeError mlstring | CompileError | ConfigError mlstring`;
val _ = Datatype`compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring`;

val locs_to_string_def = Define `
(locs_to_string NONE = implode "unknown location") ∧
@@ -115,7 +115,7 @@ val compile_def = Define`
(Failure (TypeError (implode(print_sexp (listsexp (MAP decsexp full_prog))))),[])
else
case backend$compile_tap c.backend_config full_prog of
| (NONE, td) => (Failure CompileError, td)
| (NONE, td) => (Failure AssembleError, td)
| (SOME (bytes,c), td) => (Success (bytes,c), td)`;

(* The top-level compiler *)
@@ -128,7 +128,7 @@ val error_to_str_def = Define`
concat [strlit "### ERROR: type error\n"; s; strlit "\n"]
else s) /\
(error_to_str (ConfigError s) = concat [strlit "### ERROR: config error\n"; s; strlit "\n"]) /\
(error_to_str CompileError = strlit "### ERROR: compile error\n")`;
(error_to_str AssembleError = strlit "### ERROR: assembly error\n")`;

val is_error_msg_def = Define `
is_error_msg x = mlstring$isPrefix (strlit "###") x`;
@@ -143,7 +143,7 @@ Theorem compile_correct_gen:
case FST (compiler$compile cc prelude input) of
| Failure ParseError => semantics st prelude input = CannotParse
| Failure (TypeError e) => semantics st prelude input = IllTyped
| Failure CompileError => T (* see theorem about to_lab to avoid CompileError *)
| Failure AssembleError => T (* see theorem about to_lab to avoid AssembleError *)
| Failure (ConfigError e) => T (* configuration string is malformed *)
| Success (code,data,c) =>
∃behaviours.
@@ -209,7 +209,7 @@ Theorem compile_correct = Q.prove(`
case FST (compiler$compile cc prelude input) of
| Failure ParseError => semantics_init ffi prelude input = CannotParse
| Failure (TypeError e) => semantics_init ffi prelude input = IllTyped
| Failure CompileError => T (* see theorem about to_lab to avoid CompileError *)
| Failure AssembleError => T (* see theorem about to_lab to avoid AssembleError *)
| Failure (ConfigError e) => T (* configuration string is malformed *)
| Success (code,data,c) =>
∃behaviours.

0 comments on commit c83d628

Please sign in to comment.
You can’t perform that action at this time.