Html optilambda view

.vscode/tasks.json

@@ -4,6 +4,22 @@
     // The -i option is necessary for launching GUI programs from tasks
     "version": "2.0.0",
     "tasks": [
+      {
+        "label": "OptiTrust: Run Extension Dev Host",
+        "type": "shell",
+        "command": "tools/vscode-optitrust/scripts/run_extension_dev_host.sh",
+        "options": {
+          "cwd": "${workspaceFolder}"
+        },
+        "problemMatcher": [],
+        "presentation": {
+          "clear": true,
+          "reveal": "always"
+        },
+        "runOptions": {
+          "runOn": "folderOpen"
+        }
+      },
       // Build using make (currently not using run_action.sh)
       {
         "label": "Build everything",

lib/framework/runtime/run.ml

@@ -2,6 +2,13 @@
 (*                                 Debug                                      *)
 (******************************************************************************)
 include Tools
+open Ast
+open Trm
+
+(** [absolute_path path] normalizes [path] against the current working directory. *)
+let absolute_path (path : string) : string =
+  let path = if Filename.is_relative path then Filename.concat (Unix.getcwd ()) path else path in
+  Filename.concat (Unix.realpath (Filename.dirname path)) (Filename.basename path)
 
 (** [set_exn_backtrace b]: based on [b] enable or disable backtracing in case an exception was thrown *)
 let set_exn_backtrace (b : bool) : unit =
@@ -42,18 +49,71 @@ let debug_inline_cpp = false
    source file and not those referring to the include path.
     *)
 let generate_source_with_inlined_header_cpp (basepath : string) (input_file : string) (inline : string list) (output_file : string) : unit =
-  (* FIXME: Inefficient because it performs one full pass for each inlined file. Moreover, order inside inline matters... *)
-  let s = ref (File.get_contents (Filename.concat basepath input_file)) in
-  let perform_inline finline =
-      let include_instr = "#include \"" ^ finline ^ "\"" in
-      if debug_inline_cpp then Tools.debug "Inlined %s" include_instr;
-      let contents = File.get_contents (Filename.concat basepath finline) in
-      s := Tools.string_subst include_instr contents !s;
-    in
-  List.iter perform_inline inline;
-  File.put_contents (Filename.concat basepath output_file) !s;
+  let output_path = Filename.concat basepath output_file in
+  let output_source_path = absolute_path output_path in
+  let quote_line_file filename = String.escaped filename in
+  let include_target line =
+    List.find_opt
+      (fun finline -> String.trim line = "#include \"" ^ finline ^ "\"")
+      inline
+  in
+  let rec expand_file ~(source_path : string) (read_path : string) : string =
+    File.get_lines read_path
+    |> List.mapi (fun i line ->
+        match include_target line with
+        | None -> line
+        | Some finline ->
+            if debug_inline_cpp then Tools.debug "Inlined #include \"%s\"" finline;
+            let included_path = absolute_path (Filename.concat basepath finline) in
+            Printf.sprintf "#line 1 \"%s\"\n%s\n#line %d \"%s\""
+              (quote_line_file included_path)
+              (expand_file ~source_path:included_path included_path)
+              (i + 2)
+              (quote_line_file source_path))
+    |> String.concat "\n"
+  in
+  let input_path = Filename.concat basepath input_file in
+  let contents = expand_file ~source_path:output_source_path input_path in
+  File.put_contents output_path contents;
   if debug_inline_cpp then Tools.debug "Generated %s" output_file
 
+(** [get_c_includes filename] returns the include directives visibly present in [filename]. *)
+let get_c_includes (filename : string) : string =
+  File.get_lines filename
+  |> List.filter (fun line -> String.starts_with ~prefix:"#include" (String.trim line))
+  |> String.concat "\n\n"
+
+(** [inline_parser basepath inline] parses an inlined C/C++ source and makes
+    declarations from explicitly inlined files behave as main-file code. *)
+let inline_parser (basepath : string) (inline : string list) : Trace.parser =
+  let inlined_paths =
+    List.map (fun filename -> absolute_path (Filename.concat basepath filename)) inline
+  in
+  let is_inlined_file filename =
+    let filename = absolute_path filename in
+    List.exists ((=) filename) inlined_paths
+  in
+  let flatten_inlined_includes (t : trm) : trm =
+    match t.desc with
+    | Trm_seq (instrs, result) ->
+      let instrs =
+        Mlist.to_list instrs
+        |> List.concat_map (fun instr ->
+          match trm_include_inv instr, instr.desc with
+          | Some filename, Trm_seq (included_instrs, None) when is_inlined_file filename ->
+            Mlist.to_list included_instrs
+          | _ ->
+            [instr])
+        |> Mlist.of_list
+      in
+      trm_alter ~desc:(Trm_seq (instrs, result)) t
+    | _ ->
+      t
+  in
+  fun filename ->
+    let header, ast = Trace.parse filename in
+    header, flatten_inlined_includes ast
+
 (** [get_program_basename ()]: returns the basename of the current binary program being used.
     It takes care to remove the leading './' and takes care to remove the "with_lines" suffix. *)
 let get_program_basename () : string =
@@ -112,7 +172,7 @@ let may_report_time (msg : string) (f : unit -> 'a) : 'a =
       This flag only has an effect if a [-exit_line] option was passed on the command line.
    - [~prefix:string] allows providing the basename for the output files produced
    *)
-let script ?(filename : string option) ~(extension : string) ?(check_exit_at_end : bool = true) ?(prefix : string option) ?(capture_show_in_batch = false) (f : unit -> unit) : unit =
+let script ?(filename : string option) ?(header : string option) ?(parser : Trace.parser option) ~(extension : string) ?(check_exit_at_end : bool = true) ?(prefix : string option) ?(capture_show_in_batch = false) (f : unit -> unit) : unit =
   Flags.process_cmdline_args ();
   Target.show_next_id_reset ();
 
@@ -149,7 +209,7 @@ let script ?(filename : string option) ~(extension : string) ?(check_exit_at_end
       try
         let trace_filename = prefix ^ "_trace.js" in
         if Sys.file_exists trace_filename then Sys.remove trace_filename;
-        Trace.init ~program:program_basename ~prefix filename;
+        Trace.init ?header ?parser ~program:program_basename ~prefix filename;
         if !Flags.check_validity || !Flags.recompute_resources_between_steps then
           Trace.step ~kind:Step_small ~tags:["pre-post-processing"] ~name:"Preprocessing contracts" (fun () ->
             Resources.fix_types_in_contracts ();
@@ -245,9 +305,9 @@ let script_cpp ?(filename : string option) ?(prepro : string list = []) ?(inline
     *)
 
     (* Handles on-the-fly inlining *)
-    let filename =
+    let filename, parser =
       match inline with
-      | [] -> filename
+      | [] -> filename, None
       | _ ->
         let program_basename = get_program_basename () in
         let basepath = Filename.dirname program_basename in
@@ -259,10 +319,10 @@ let script_cpp ?(filename : string option) ?(prepro : string list = []) ?(inline
         let basename = Filename.chop_extension filename in
         let inlinefilename = basename ^ "_inlined.cpp" in
         generate_source_with_inlined_header_cpp basepath filename inline inlinefilename;
-        Some inlinefilename
+        Some inlinefilename, Some (inline_parser basepath inline)
     in
 
-    script ?filename ~capture_show_in_batch ~extension:".cpp" ~check_exit_at_end ?prefix f)
+    script ?filename ?parser ~capture_show_in_batch ~extension:".cpp" ~check_exit_at_end ?prefix f)
 
 
 let stg_name (stg: int): string =

lib/framework/runtime/trace.ml

@@ -557,7 +557,7 @@ let output_prog (style:output_style) ?(beautify:bool=true) (ctx : context) (pref
   begin try
     begin match style.print with
     | Lang_OptiLambda optilambda_style ->
-      output_string out_prog (Optitrust_optilambda.Optilambda.trm_to_string ~style:optilambda_style ast)
+      output_string out_prog (Optitrust_optilambda.Optilambda.program_to_string ~style:optilambda_style ~header:ctx.header ast)
     | Lang_AST _ -> raise (TraceFailure "output_prog requires a Lang_C or Lang_OptiLambda printing mode, not a Lang_AST")
     | Lang_C cstyle ->
       (* Print the header, in particular the include directives *) (* LATER: include header directives into the AST representation *)
@@ -1333,16 +1333,18 @@ let invalidate () : unit =
 (** [get_initial_ast filename]: gets the initial ast before applying any trasformations
      [filename] - filename of the source code
      returns header and ast. *)
-let get_initial_ast (filename : string) : (string * trm) =
-  parse filename
+let get_initial_ast ?(parser : parser option) (filename : string) : (string * trm) =
+  match parser with
+  | None -> parse filename
+  | Some parser -> parser filename
 
 (** [init f]: initializes the trace with the contents of the file [f].
    This operation should be the first in a transformation script.
    The history is initialized with the initial AST.
    [~prefix:"foo"] allows to use a custom prefix for all output files,
    instead of the basename of [f].
    style is computed based on the global flags.   *)
-let init ~(prefix : string) ~(program : string) (filename : string) : unit =
+let init ?(header : string option) ?(parser : parser option) ~(prefix : string) ~(program : string) (filename : string) : unit =
   ast_just_before_first_call_to_restore_original := None; (* TEMPORARY HACK *)
   invalidate ();
   let basename = Filename.basename filename in
@@ -1374,7 +1376,8 @@ let init ~(prefix : string) ~(program : string) (filename : string) : unit =
 
   init_logs prefix;
 
-  let (header, cur_ast), stats_parse = Stats.measure_stats (fun () -> get_initial_ast filename) in
+  let ((parsed_header, cur_ast), stats_parse) = Stats.measure_stats (fun () -> get_initial_ast ?parser filename) in
+  let header = Option.value ~default:parsed_header header in
 
   let context = { extension; prefix; header } in
   the_trace.next_step_id <- 0;
@@ -1815,19 +1818,25 @@ let produce_diff_output_internal (step:step_tree) : unit =
     output_prog style ctx filename_prefix ast;
     Flags.verbose_info "Generated: %s" (output_filename style ctx filename_prefix);
     in
-  let output_optilambda_pair suffix representation =
-    let style = optilambda_style representation in
-    output_ast style (prefix ^ "_before" ^ suffix) ast_before;
-    output_ast style (prefix ^ "_after" ^ suffix) ast_after;
+  let diff_filename_prefix style side =
+    let suffix =
+      match style.Style.print with
+      | Lang_OptiLambda optilambda_style ->
+        begin match optilambda_style.representation with
+        | Optitrust_optilambda.Optilambda.Style.Surface -> ""
+        | Optitrust_optilambda.Optilambda.Style.Internal -> "_internal"
+        | Optitrust_optilambda.Optilambda.Style.FullyTypedInternal -> "_typed"
+        end
+      | Lang_AST _
+      | Lang_C _ -> ""
+      in
+    prefix ^ "_" ^ side ^ suffix
     in
-  (* Generate files. *)
-  output_ast style_before (prefix ^ "_before") ast_before;
-  output_ast style_after (prefix ^ "_after") ast_after;
-  output_optilambda_pair "" Optitrust_optilambda.Optilambda.Style.Surface;
-  List.iter
-    (fun (suffix, representation) -> output_optilambda_pair ("_" ^ suffix) representation)
-    optilambda_representations;
-  Flags.verbose_info "Writing ast and code into %s.js" prefix
+  (* Generate only the requested pair. Other OptiLambda representations are
+     generated lazily by the VS Code diff webview when the user switches syntax. *)
+  output_ast style_before (diff_filename_prefix style_before "before") ast_before;
+  output_ast style_after (diff_filename_prefix style_after "after") ast_after;
+  Flags.verbose_info "Generated diff files for %s" prefix
 
 (** [produce_trace_output step] is an auxiliary function for [produce_output_and_exit] *)
 let produce_trace_output (step:step_tree) : unit =

lib/optilambda/optilambda.ml

@@ -10,6 +10,8 @@ let default_style = Style.default
 
 let trm_to_doc = Printer.trm_to_doc
 let trm_to_string = Printer.trm_to_string
+let program_to_doc = Printer.program_to_doc
+let program_to_string = Printer.program_to_string
 let trm_to_html = Html.trm_to_html
 let typ_to_doc = Printer.typ_to_doc
 let typ_to_string = Printer.typ_to_string