diff options
| author | Thomas Bauereiss | 2018-02-01 17:57:36 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-01 18:01:20 +0000 |
| commit | a2d505a0e7e01efbfd24cacc6ea0f74918ba31f8 (patch) | |
| tree | 9be75ac5376ba02bc6fae67b49c3ef4742a780b0 /src | |
| parent | c7e8709e3de85d398ee9fa99317defd8c6a2756b (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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) |