Put the scope-checker into the Pancake compiler

CakeML · Mar 19, 2024 · ca01320 · ca01320
1 parent 0d658da
commit ca01320
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 6 deletions.
diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml
@@ -24,6 +24,12 @@ val () = use_long_names := true;
 
 val spec32 = INST_TYPE[alpha|->``:32``]
 
+val res = translate $ spec32 panScopeTheory.scope_check_exp_def;
+val res = translate $ spec32 panScopeTheory.scope_check_prog_def;
+val res = translate $
+  INST_TYPE[beta|->``:32``] panScopeTheory.scope_check_funs_def;
+val res = translate $ INST_TYPE[beta|->``:32``] panScopeTheory.scope_check_def;
+
 val max_heap_limit_32_def = Define`
   max_heap_limit_32 c =
     ^(spec32 data_to_wordTheory.max_heap_limit_def

diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml
@@ -25,6 +25,12 @@ val () = use_long_names := true;
 
 val spec64 = INST_TYPE[alpha|->``:64``]
 
+val res = translate $ spec64 $ panScopeTheory.scope_check_exp_def;
+val res = translate $ spec64 $ panScopeTheory.scope_check_prog_def;
+val res = translate $
+  INST_TYPE[beta|->``:64``] panScopeTheory.scope_check_funs_def;
+val res = translate $ INST_TYPE[beta|->``:64``] panScopeTheory.scope_check_def;
+
 val max_heap_limit_64_def = Define`
                                   max_heap_limit_64 c =
 ^(spec64 data_to_wordTheory.max_heap_limit_def

diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml
@@ -18,7 +18,7 @@ open riscv_configTheory export_riscvTheory
 open mips_configTheory export_mipsTheory
 open arm7_configTheory export_arm7Theory
 open ag32_configTheory export_ag32Theory
-open panPtreeConversionTheory pan_to_targetTheory
+open panPtreeConversionTheory pan_to_targetTheory panScopeTheory
 
 val _ = new_theory"compiler";
 
@@ -171,6 +171,7 @@ Datatype:
                 | TypeError mlstring
                 | AssembleError
                 | ConfigError mlstring
+                | ScopeError mlstring mlstring
 End
 
 Definition find_next_newline_def:
@@ -277,10 +278,13 @@ Definition compile_pancake_def:
   case panPtreeConversion$parse_funs_to_ast input of
   | NONE => Failure (ParseError (strlit "Failed pancake parsing"))
   | SOME funs =>
-      let _ = empty_ffi (strlit "finished: lexing and parsing") in
-      case pan_to_target$compile_prog c funs of
-      | NONE => (Failure AssembleError)
-      | SOME (bytes,data,c) => (Success (bytes,data,c))
+      case scope_check funs of
+      | SOME (x, fname) => (Failure (ScopeError x fname))
+      | NONE =>
+          let _ = empty_ffi (strlit "finished: lexing and parsing") in
+          case pan_to_target$compile_prog c funs of
+          | NONE => (Failure AssembleError)
+          | SOME (bytes,data,c) => (Success (bytes,data,c))
 End
 
 (* The top-level compiler *)
@@ -294,7 +298,9 @@ 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 AssembleError = strlit "### ERROR: assembly error\n")`;
+  (error_to_str AssembleError = strlit "### ERROR: assembly error\n") /\
+  (error_to_str (ScopeError name fname) =
+    concat [strlit "### ERROR: scope error\n"; name; strlit " is not in scope in "; fname; strlit "\n"])`;
 
 val is_error_msg_def = Define `
   is_error_msg x = mlstring$isPrefix (strlit "###") x`;