From 3cad2ad60f5f5f05ef94ba38590539939d3ccda0 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 30 Jan 2018 18:15:29 +0000
Subject: Split base definitions of Lem monads and further built-ins (e.g. loop
 combinators)

Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators.  These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
---
 src/pretty_print_lem.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/pretty_print_lem.ml')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 48825540..5d127f6d 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1495,15 +1495,15 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line =
         if !opt_sequential then
           concat [regstate_def; hardline;
             hardline;
-            string ("type MR 'a 'r = State.MR regstate 'a 'r " ^ exc_typ); hardline;
-            string ("type M 'a = State.M regstate 'a " ^ exc_typ); hardline;
+            string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline;
+            string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline;
             hardline;
             register_refs
           ]
         else
           concat [
-            string ("type MR 'a 'r = Prompt.MR 'a 'r " ^ exc_typ); hardline;
-            string ("type M 'a = Prompt.M 'a " ^ exc_typ); hardline
+            string ("type MR 'a 'r = Prompt_monad.MR 'a 'r " ^ exc_typ); hardline;
+            string ("type M 'a = Prompt_monad.M 'a " ^ exc_typ); hardline
           ]
         ]);
   (print defs_file)
-- 
cgit v1.2.3


From a2d505a0e7e01efbfd24cacc6ea0f74918ba31f8 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 1 Feb 2018 17:57:36 +0000
Subject: Comment out special casing of execute function in Lem pretty-printer

It assumes that execute is non-recursive, which is not the case for RISC-V with
compressed instructions.  Splitting execute into different auxiliary functions
for each clause is probably still useful, as Isabelle is likely to parse many
small functions faster than one big (potentially recursive) function, but this
splitting should be done in the rewriter instead of the pretty-printer, in
order to properly deal with recursion.
---
 src/pretty_print_lem.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/pretty_print_lem.ml')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 5d127f6d..42ba254e 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1210,7 +1210,8 @@ let doc_mutrec_lem = function
 let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
-  | FCL_aux (FCL_Funcl(id,_),_) :: _
+  (* TODO: Move splitting of execute function to the rewriter *)
+  (*| FCL_aux (FCL_Funcl(id,_),_) :: _
     when string_of_id id = "execute" (*|| string_of_id id = "initial_analysis"*) ->
     let (_,auxiliary_functions,clauses) =
       List.fold_left
@@ -1273,7 +1274,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
     auxiliary_functions ^^ hardline ^^ hardline ^^
     (prefix 2 1)
       ((separate space) [string "let" ^^ doc_rec_lem false r ^^ doc_id_lem id;equals;string "function"])
-      (clauses ^/^ string "end")
+      (clauses ^/^ string "end")*)
   | FCL_aux (FCL_Funcl(id,_),annot) :: _
     when not (Env.is_extern id (env_of_annot annot) "lem") ->
     string "let" ^^ (doc_rec_lem (List.length fcls > 1) r) ^^ (doc_fundef_rhs_lem fd)
-- 
cgit v1.2.3