Merge remote-tracking branch 'origin/master' into pancake_divmul

compiler/bootstrap/translation/from_pancake32ProgScript.sml

@@ -664,6 +664,12 @@ QED
 
 val _ = conv_Prog_ind  |> update_precondition;
 
+val res  = translate $ spec32 conv_Fun_def;
+
+val res = translate $ spec32 conv_FunList_def;
+
+val res = translate $ spec32 parse_funs_to_ast_def;
+
 val res = translate $ spec32 parse_to_ast_def;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);

compiler/bootstrap/translation/from_pancake64ProgScript.sml

@@ -668,6 +668,12 @@ QED
 
 val _ = conv_Prog_ind  |> update_precondition;
 
+val res  = translate $ spec64 conv_Fun_def;
+
+val res = translate $ spec64 conv_FunList_def;
+
+val res = translate $ spec64 parse_funs_to_ast_def;
+
 val res = translate $ spec64 parse_to_ast_def;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);

compiler/compilerScript.sml

@@ -277,11 +277,11 @@ val compile_def = Define`
 Definition compile_pancake_def:
   compile_pancake c input =
   let _ = empty_ffi (strlit "finished: start up") in
-  case panPtreeConversion$parse_to_ast input of
+  case panPtreeConversion$parse_funs_to_ast input of
   | NONE => Failure (ParseError (strlit "Failed pancake parsing"))
-  | SOME prog =>
+  | SOME funs =>
       let _ = empty_ffi (strlit "finished: lexing and parsing") in
-      case pan_to_target$compile_prog c [strlit "main", [], prog] of
+      case pan_to_target$compile_prog c funs of
       | NONE => (Failure AssembleError)
       | SOME (bytes,data,c) => (Success (bytes,data,c))
 End

pancake/parser/panConcreteExamplesScript.sml

@@ -1,5 +1,6 @@
 (**
  * Pancake concrete syntax examples
+ * 9th May 2023: Updated with function declarations
  *)
 open HolKernel Parse boolLib bossLib stringLib numLib intLib;
 open preamble panPtreeConversionTheory;
@@ -36,105 +37,137 @@ fun parse_pancake q =
   let
     val code = quote_to_strings q |> String.concatWith "\n" |> fromMLstring
   in
-    EVAL “parse_to_ast ^code”
+    EVAL “parse_funs_to_ast ^code”
   end
 
 val check_success = assert $ optionSyntax.is_some o rhs o concl
 
 (** Examples can be written using quoted strings and passed to the ML
     function parse_pancake. *)
 
-(** Pancake programs consist of a sequence of blocks of statements. *)
+(** Pancake programs consist of a sequence of function declarations. *)
+
+(** The body of each function consists of a sequence of blocks. *)
 
 (** Blocks: Declarations, Conditionals (If-Then-Else), Loops (While) *)
 
 (** Conditionals: An if-block without an alternative. The bodies of the
     conditional are Pancake programs (in this case a single assignment
     statement). NB: Statements end with a semi-colon, blocks do not. *)
-val ex1 = ‘if 2 >= 1 { x = 2; }’;
+val ex1 = ‘
+  fun cond() {
+    if 2 >= 1 { x = 2; }
+  }’;
 
 val treeEx1 = check_success $ parse_pancake ex1;
 
 (** We also have a selection of boolean operators and we can call
     functions. A struct value encloses expressions within chevrons
     (‘<>’). *)
-val ex2 = ‘if b & (a ^ c) & d {
-             foo(1, <2, 3>);
-           } else {
-             goo(4, 5, 6);
-           }’;
+val ex2 = ‘
+  fun main() {
+    if b & (a ^ c) & d {
+      foo(1, <2, 3>);
+    } else {
+      goo(4, 5, 6);
+    }
+  }’;
 
 val treeEx2 = check_success $ parse_pancake ex2;
 
 (** We also have a selection of boolean operators and
     a ‘return’ statement. *)
-(** FIXME: Add ‘true’ and ‘false’ to EBaseNT *)
-val ex3 = ‘if b & (a ^ c) & d { return true; } else { return false; }’;
+val ex3 = ‘
+  fun boolfun() {
+    if b & (a ^ c) & d { return true; }
+    else { return false; }
+  }’;
 
 val treeEx3 = check_success $ parse_pancake ex3;
 
 (** Loops: standard looping construct. *)
 
-val ex4 = ‘while b | c {
-             if x >= 5 {
-               break;
-             } else {
-               strb y, 8; // store byte
-               #foo(x,y,k,z); // ffi function call with pointer args
-               x = x + 1;
-               y = x + 1;
-             }
-           }’;
+val ex4 = ‘
+  fun loopy() {
+    while b | c {
+      if x >= 5 {
+        break;
+      } else {
+        strb y, 8; // store byte
+        #foo(x,y,k,z); // ffi function call with pointer args
+        x = x + 1;
+        y = x + 1;
+      }
+    }
+  }’;
 
 val treeEx4 = check_success $ parse_pancake ex4;
 
 (** Declarations: intended semantics is the variable scope extends as
     far left as possible. *)
 
-val ex5 = ‘var b = 5;
-           b = b + 1;
-           if b >= 5 {
-             raise Err 5;
-           }’;
+val ex5 = ‘
+  fun foo () {
+    var b = 5;
+    b = b + 1;
+    if b >= 5 {
+      raise Err 5;
+    }
+  }’;
 
 val treeEx5 = check_success $ parse_pancake ex5;
 
 (** Scope can be indicated with curly brackets *)
 
-val ex6 = ‘{var b = 5;
-            b = b + 1;};
-           if b >= 5 {
-             raise Err 5;
-           }’;
+val ex6 = ‘
+  fun foo () {
+    {var b = 5;
+     b = b + 1;};
+     if b >= 5 {
+       raise Err 5;
+     }
+  }’;
 
 val treeEx6 = check_success $ parse_pancake ex6;
 
 (* Load data of a fixed shape. The below example loads a triple where
    the first two components are single words, and the third is a tuple
    of words.
  *)
-val ex7 = ‘x = lds {1,1,2} y;’;
+val ex7 = ‘
+  fun loader() {
+    x = lds {1,1,2} y;
+  }’;
 
 val treeEx7 = check_success $ parse_pancake ex7;
 
 (* These can be nested arbitrarily deep *)
-val ex7_and_a_half = ‘x = lds {3,1,{1,{2,1}}} y;’;
+val ex7_and_a_half = ‘
+  fun loader() {
+    x = lds {3,1,{1,{2,1}}} y;
+  }’;
 
 val treeEx7_and_a_half = check_success $ parse_pancake ex7_and_a_half;
 
 (* Note that {1} and 1 are distinct shapes *)
-val ex7_and_three_quarters = ‘x = lds {1,{1}} y;’;
+val ex7_and_three_quarters = ‘
+  fun loader() {
+    x = lds {1,{1}} y;
+  }’;
 
 val treeEx7_and_three_quarters = check_success $ parse_pancake ex7_and_three_quarters;
 
 (* Comparison operators. Only two of these exist in the concrete syntax,
    so the parser may rotate them. This shouldn't matter since expressions
    are pure.
  *)
-val ex8 = ‘x = a < b;
-           x = b > a;
-           x =  b >= a;
-           x = a <= b;’;
+val ex8 = ‘
+  fun cmps () {
+    x = a < b;
+    x = b > a;
+    x =  b >= a;
+    x = a <= b;
+  }’;
 
 val treeEx8 = check_success $ parse_pancake ex8;
 
@@ -153,18 +186,40 @@ val treeEx8_and_a_half = check_success $ parse_pancake ex8_and_a_half;
 
 (** Small test modelled after the minimal working example. *)
 val ex10 = ‘
- var a = @base;
- var b = 8;
- var c = @base + 16;
- var d = 1;
- #out_morefun(a,b,c,d);
- str @base, ic;
- return 0;’;
+ fun testfun() {
+   var a = @base;
+   var b = 8;
+   var c = @base + 16;
+   var d = 1;
+   #out_morefun(a,b,c,d);
+   str @base, ic;
+   return 0;
+ }’;
 
 val treeEx10 = check_success $ parse_pancake ex10;
 
+(** Multiple functions. *)
+
+val ex_much_fun = ‘
+  fun loader() {
+    x = lds {1,{1}} y;
+  }
+
+  fun loader() {
+    x = lds {1,{1}} y;
+  }
+
+  fun cmps () {
+    x = a < b;
+    x = b > a;
+    x =  b >= a;
+    x = a <= b;
+  }’;
+
+val treeExMuchFun = check_success $ parse_pancake ex_much_fun;
+
 (** We can assign boolean expressions to variables. *)
-val exN = ‘x = b & a ^ c & d;’;
+val exN = ‘fun blah() { x = b & a ^ c & d; }’;
 
 val treeExN = check_success $ parse_pancake exN;
 

pancake/parser/panLexerScript.sml

@@ -19,7 +19,7 @@ val _ = new_theory "panLexer";
 Datatype:
   keyword = SkipK | StoreK | StoreBK | IfK | ElseK | WhileK
   | BrK | ContK | RaiseK | RetK | TicK | VarK | WithK | HandleK
-  | LdsK | LdbK | BaseK | InK | TrueK | FalseK
+  | LdsK | LdbK | BaseK | InK | FunK | TrueK | FalseK
 End
 
 Datatype:
@@ -112,6 +112,7 @@ Definition get_keyword_def:
   if s = "@base" then (KeywordT BaseK) else
   if s = "true" then (KeywordT TrueK) else
   if s = "false" then (KeywordT FalseK) else
+  if s = "fun" then (KeywordT FunK) else
   if isPREFIX "@" s ∨ s = "" then LexErrorT else
   IdentT s
 End

pancake/parser/panPEGScript.sml

@@ -14,11 +14,12 @@ open ASCIInumbersLib combinTheory;
 val _ = new_theory "panPEG";
 
 Datatype:
-  pancakeNT = ProgNT | BlockNT | StmtNT | ExpNT
+  pancakeNT = FunListNT | FunNT | ProgNT | BlockNT | StmtNT | ExpNT
             | DecNT | AssignNT | StoreNT | StoreByteNT
             | IfNT | WhileNT | CallNT | RetNT | HandleNT
             | ExtCallNT | RaiseNT | ReturnNT
             | ArgListNT
+            | ParamListNT
             | EXorNT | EAndNT | EEqNT | ECmpNT
             | EShiftNT | EAddNT | EMulNT
             | EBaseNT
@@ -104,12 +105,28 @@ End
 
 Definition pancake_peg_def[nocompute]:
   pancake_peg = <|
-    start := mknt ProgNT;
+    start := mknt FunListNT;
     anyEOF := "Didn't expect an EOF";
     tokFALSE := "Failed to see expected token";
     tokEOF := "Failed to see expected token; saw EOF instead";
     notFAIL := "Not combinator failed";
     rules := FEMPTY |++ [
+        (INL FunListNT, seql [rpt (mknt FunNT) FLAT] (mksubtree FunListNT));
+        (INL FunNT, seql [consume_kw FunK;
+                          keep_ident;
+                          consume_tok LParT;
+                          try (mknt ParamListNT);
+                          consume_tok RParT;
+                          consume_tok LCurT;
+                          mknt ProgNT;
+                          consume_tok RCurT]
+                          (mksubtree FunNT));
+        (INL ParamListNT, seql [mknt ShapeNT; keep_ident;
+                                rpt (seql [consume_tok CommaT;
+                                           mknt ShapeNT;
+                                           keep_ident] I)
+                                           FLAT]
+                               (mksubtree ParamListNT));
         (INL ProgNT, rpt (choicel [mknt BlockNT;
                                    seql [mknt StmtNT;
                                          consume_tok SemiT] I])
@@ -308,9 +325,16 @@ val test1 = time EVAL
 val prog =
   “pancake_lex "var x = 0 { var y = <1,2,3> { x = x + y.1; } }"”
 
+Definition parse_statement_def:
+  parse_statement s =
+    case peg_exec pancake_peg (mknt ProgNT) s [] NONE [] done failed of
+    | Result (Success [] [e] _) => SOME e
+    | _ => NONE
+End
+
 Definition parse_def:
   parse s =
-    case peg_exec pancake_peg (mknt ProgNT) s [] NONE [] done failed of
+    case peg_exec pancake_peg (mknt FunListNT) s [] NONE [] done failed of
     | Result (Success [] [e] _) => SOME e
     | _ => NONE
 End
@@ -477,7 +501,9 @@ val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT”
                 “HandleNT”, “RetNT”, “CallNT”,
                 “WhileNT”, “IfNT”, “StoreByteNT”,
                 “StoreNT”, “AssignNT”, “DecNT”,
-                “StmtNT”, “BlockNT”];
+                “StmtNT”, “BlockNT”, “ParamListNT”, “FunNT”];
+
+(*  “FunNT”, “FunListNT” *)
 
 (** All non-terminals except the top-level
   * program nonterminal always consume input. *)
@@ -501,7 +527,7 @@ end;
   * well-formed. *)
 val pancake_wfpeg_thm = save_thm(
   "pancake_wfpeg_thm",
-  LIST_CONJ (List.foldl wfnt [] (topo_nts @ [“ProgNT”])))
+  LIST_CONJ (List.foldl wfnt [] (topo_nts @ [“ProgNT”, “FunListNT”])))
 
 val subexprs_mknt = Q.prove(
   ‘subexprs (mknt n) = {mknt n}’,