Bugfix var local name

case_studies/dot_product/dot.ml

@@ -18,13 +18,7 @@ let part = 1 (* Choose which part you want to work on. *)
 let _ = if part = 1 then Run.script_cpp (fun () ->
   (* !! Function.elim_infix_ops ~indepth:true []; *)
   !! Loop.tile (int 32) ~index:"bi" ~bound:TileDivides [cFor "i"];
-
-  (* LATER: !! Variable.local_name ~var:"s" ~local_var:"t" [tSpanSeq [cForBody "bi"]]; *)
-  !! (
-    Sequence.intro ~mark:"t_scope" ~start:[tFirst; cForBody "bi"] ~stop:[tLast; cForBody "bi"] ();
-    Variable.local_name ~var:"s" ~local_var:"t" [cMark "t_scope"];
-    Sequence.elim [cMark "t_scope"];
-  );
+  !! Variable.local_name ~var:"s" ~local_var:"t" [tSpanSeq [cForBody "bi"]];
 
   (* DEPRECATED? !! Sequence_basic.insert (trm_let (new_var "d", typ_f32) (trm_get (trm_find_var "s" []))) [tFirst; cForBody "bi"]; *)
   !! (

doc/odoc_extra.css

@@ -23,6 +23,8 @@ body {
    /*border: 1px solid black;*/
    padding: 3px 5px 3px 5px;
    background: #FFFFA0;
+   color: #1a1a1a; /* anchor text dark: odoc's theme flips text to light in dark mode,
+                      which would be unreadable on the light-yellow background */
    font-weight: bold;
 }
 
@@ -83,3 +85,31 @@ body {
 .d2h-code-line del, .d2h-code-side-line del {
     background-color: inherit;
 }
+
+/* Dark-mode support.
+   odoc's stylesheet flips page text to a light color under
+   `prefers-color-scheme: dark` (see _doc/odoc.support/odoc.css), but the injected
+   example/diff blocks pin light backgrounds. Without the rules below you get
+   light-on-light (unreadable). odoc_extra.css is loaded after odoc.css and these
+   selectors are at least as specific, so they win without !important. */
+@media (prefers-color-scheme: dark) {
+
+  /* Example OCaml block: turn it into a proper dark code card instead of the
+     light-yellow highlight, keeping a faint yellow tint for identity. */
+  .code-unit-test {
+    background: #3a3a26;
+    color: #f5f1c0;
+  }
+
+  /* Diff block: diff2html hardcodes light pastel backgrounds for added/removed
+     lines that can't be re-tinted cleanly. Rather than override each one, we
+     force the whole diff into a light "island": a white table background (which
+     fills the transparent context-line cells) and dark inherited text (which
+     cascades to every cell while the changed lines keep their own pastels). */
+  .diff-unit-test .d2h-wrapper,
+  .diff-unit-test .d2h-file-wrapper,
+  .diff-unit-test .d2h-diff-table {
+    background: #ffffff;
+    color: #1a1a1a;
+  }
+}

lib/framework/flags.ml

@@ -21,6 +21,7 @@ let analyse_stats_details : bool ref = ref false
 (** [dump_ast_details]: flag to dump OptiTrust AST, both in the form of a '.ast' and '_enc.cpp' files. *)
 let dump_ast_details : bool ref = ref false
 
+(* TODO : deprecate once optilambda surface display works *)
 (** [pretty_matrix_notation]: flag to display matrix macros with syntactic sugar:
   MALLOC2(n, m, sizeof(T)) --> malloc(sizeof(T[n][m]))
   x[MINDEX2(n, m, i, j)] --> x[i;j]
@@ -124,16 +125,20 @@ let set_optilambda_repr repr =
    This allows for the propagation of the backtrace. *)
 let stop_on_first_resource_error = ref true
 
+(* TODO Yanni : reevaluate *)
 (** [resource_typing_enabled]: if false, never attempt typing resources and never introduce ghosts. *)
 let resource_typing_enabled = ref true
 
+(* TODO Yanni : reevaluate *)
 (** [check_validity]: perform validation of transformations *)
 let check_validity = ref false
 
+(* TODO Yanni : reevaluate *)
 (** [preserve_specs_only]: allow code transformation that preserve the specification without necessarily preserving the semantics
     TODO: update code which was also using check_validity for this purpose *)
 let preserve_specs_only = ref false
 
+(* TODO Yanni : reevaluate *)
 (** [disable_resource_typing ()] should be called when using OptiTrust without resources. *)
 let disable_resource_typing () =
   resource_typing_enabled := false;
@@ -145,6 +150,7 @@ let reparse_between_steps = ref false
 (** [recompute_resources_between_steps]: always recompute resources between two steps *)
 let recompute_resources_between_steps = ref false
 
+(* TODO Yanni : depreciate - should always be true *)
 (** [use_resources_with_models]: use resources of the form "p ~~> v" instead of "p ~> Cell". In the long term, this flag should disappear as we should be able to unify those two modes into one, using clever syntactic sugar and unification features. *)
 let use_resources_with_models = ref false
 
@@ -265,6 +271,7 @@ let string_to_steps_selector (s:string) : steps_selector =
   | "all" -> Steps_all
   | _ -> failwith "invalid step selector, should be one of 'none', 'script', 'important', 'effectful', 'all'"
 
+(* TODO : the trace would be smaller once we share terms in the trace *)
 (* Options to control which steps are exported in the trace.
    Be careful that a step not exported cannot be viewed even in step diff mode. *)
 let save_steps : steps_selector option ref = ref None

lib/framework/prelude.ml

@@ -7,72 +7,7 @@ include Contextualized_error
 include Mark
 include Target
 include Trm_pattern
-
-module Trm = struct
-  include Trm
-  (* short aliases *)
-  let var = trm_var
-  let struct_access = trm_struct_access
-  let array_access = trm_array_access
-  let get_stringreprid = trm_get_stringreprid
-
-  let pattern_var = trm_pattern_var
-end
-
-module ShowAt = Show.At
-
-let trm_seq_nobrace = Nobrace.trm_seq
-let trm_seq_nobrace_nomarks = Nobrace.trm_seq_nomarks
-
-type seq_component =
-  | Trm of trm
-  | TrmList of trm list
-  | TrmMlist of trm mlist
-  | Mark of mark
-  | MarkList of mark list
-  | SeqComponents of seq_component list
-
-let trm_seq_helper ?(annot : trm_annot option) ?(loc : location) ?(result: var option) ?(braces = true) (components: seq_component list) : trm =
-  let rec aux cs acc = List.fold_right (fun comp acc ->
-    match comp with
-    | Trm t -> Mlist.push_front t acc
-    | TrmList tl -> Mlist.merge (Mlist.of_list tl) acc
-    | TrmMlist tml -> Mlist.merge tml acc
-    | Mark "" -> acc
-    | Mark m -> Mlist.insert_mark_at 0 m acc
-    | MarkList ms -> Mlist.insert_marks_at 0 ms acc
-    | SeqComponents cs -> aux cs acc
-  ) cs acc in
-  let mlist = aux components (Mlist.empty ()) in
-  if braces then
-    trm_seq ?annot ?loc ?result mlist
-  else begin
-    assert (annot = None);
-    assert (loc = None);
-    trm_seq_nobrace ?result mlist
-  end
-
-let update_span_helper (span : Dir.span) (t_seq : trm) (f : trm mlist -> seq_component list) : trm =
-  let instrs, result = trm_inv ~error:"expected seq" trm_seq_inv t_seq in
-  if span.start >= span.stop then begin
-    t_seq
-  end else begin
-    let (span_instrs, instrs_after) = Mlist.split ~left_bias:false span.stop instrs in
-    let (instrs_before, span_instrs) = Mlist.split ~left_bias:true span.start span_instrs in
-    let new_span_components = f span_instrs in
-    trm_seq_helper ~annot:t_seq.annot ?result [
-      TrmMlist instrs_before;
-      SeqComponents new_span_components;
-      TrmMlist instrs_after;
-    ]
-  end
-
-let skip_includes (t : trm) : trm =
-  match trm_seq_inv t with
-  | Some (instrs, None) ->
-    let not_include = Mlist.filter (fun t -> not (trm_is_include t)) instrs in
-    trm_seq not_include
-  | _ -> failwith "skip_includes should be called on the root of the AST"
+include Seq_helper
 
 let rec find_var_filter_on (candidates : typ option varmap ref) (filter : var -> bool) (t : trm) : unit =
   let update_map v ty =
@@ -100,7 +35,7 @@ let find_var_filter ?(target : target = []) (filter : var -> bool) : var * typ o
   then find_var_filter_on candidates filter (skip_includes (Trace.ast ()))
   else List.iter (fun p ->
     find_var_filter_on candidates filter (Target.resolve_path p)
-  ) (resolve_target target);
+  ) (resolve_target_with_stringreprs_available target (Trace.ast ()));
   (* let candidates = Var_set.filter filter vars in *)
   match Var_map.cardinal !candidates with
   | 0 -> failwith "could not find variable in current AST variables" (* ": %s" (vars_to_string (Var_set.elements vars)) *)

lib/framework/runtime/trace.ml

@@ -1428,7 +1428,7 @@ let failure_expected (h : exn -> bool) (f : unit -> unit) : unit =
 let resource_error_expected (f: unit -> unit): unit =
   failure_expected (function
   | Resource_computation.ResourceError _ -> true
-  | _ -> false) f
+  | _ -> false) (fun () -> f (); recompute_resources ())
 
 (** [apply f]: applies the transformation [f] to the current AST,
    and updates the current ast with the result of that transformation.

lib/framework/seq_helper.ml

@@ -0,0 +1,78 @@
+include Optitrust_utils
+include Optitrust_ast
+include Ast
+include Trm
+include Typ
+include Contextualized_error
+include Mark
+(* include Target *)
+include Trm_pattern
+
+module Trm = struct
+  include Trm
+  (* short aliases *)
+  let var = trm_var
+  let struct_access = trm_struct_access
+  let array_access = trm_array_access
+  let get_stringreprid = trm_get_stringreprid
+
+  let pattern_var = trm_pattern_var
+end
+
+(* module Show.At = Show.At *)
+
+let debug_path = true
+
+let trm_seq_nobrace = Nobrace.trm_seq
+let trm_seq_nobrace_nomarks = Nobrace.trm_seq_nomarks
+
+type seq_component =
+  | Trm of trm
+  | TrmList of trm list
+  | TrmMlist of trm mlist
+  | Mark of mark
+  | MarkList of mark list
+  | SeqComponents of seq_component list
+
+let trm_seq_helper ?(annot : trm_annot option) ?(loc : location) ?(result: var option) ?(braces = true) (components: seq_component list) : trm =
+  let rec aux cs acc = List.fold_right (fun comp acc ->
+    match comp with
+    | Trm t -> Mlist.push_front t acc
+    | TrmList tl -> Mlist.merge (Mlist.of_list tl) acc
+    | TrmMlist tml -> Mlist.merge tml acc
+    | Mark "" -> acc
+    | Mark m -> Mlist.insert_mark_at 0 m acc
+    | MarkList ms -> Mlist.insert_marks_at 0 ms acc
+    | SeqComponents cs -> aux cs acc
+  ) cs acc in
+  let mlist = aux components (Mlist.empty ()) in
+  if braces then
+    trm_seq ?annot ?loc ?result mlist
+  else begin
+    assert (annot = None);
+    assert (loc = None);
+    trm_seq_nobrace ?result mlist
+  end
+
+let update_span_helper (span : Dir.span) (t_seq : trm) (f : trm mlist -> seq_component list) : trm =
+  let instrs, result = trm_inv ~error:"expected seq" trm_seq_inv t_seq in
+  if span.start > span.stop then begin
+    failwith "update_span_helper: This span is impossible [%n; %n]" span.start span.stop
+  end else begin
+    let (span_instrs, instrs_after) = Mlist.split ~left_bias:false span.stop instrs in
+    let (instrs_before, span_instrs) = Mlist.split ~left_bias:true span.start span_instrs in
+    let new_span_components = f span_instrs in
+    trm_seq_helper ~annot:t_seq.annot ?result [
+      TrmMlist instrs_before;
+      SeqComponents new_span_components;
+      TrmMlist instrs_after;
+    ]
+  end
+
+let skip_includes (t : trm) : trm =
+  match trm_seq_inv t with
+  | Some (instrs, None) ->
+    let not_include = Mlist.filter (fun t -> not (trm_is_include t)) instrs in
+    trm_seq not_include
+  | _ -> failwith "skip_includes should be called on the root of the AST"
+

lib/framework/show.ml

@@ -8,7 +8,7 @@ include Style
      Show.trm ~msg:"foo:" t
      Show.trm ~msg:"foo:" tg
      Show.trm ~msg:"foo:" (Target.resolve_path p)
-     ShowAt.trm ~msg:"foo:" (Target.of_path p)
+     Show.At.trm ~msg:"foo:" (Target.of_path p)
 *)
 
 
@@ -113,7 +113,7 @@ let trm_text ?(msg : string option) ?(only_desc : bool = false) (t : trm) : unit
 
 
 
-(* DEPRECATED: use ShowAt.trm []
+(* DEPRECATED: use Show.At.trm []
 let ast ?(style = Default) ?(msg : string = "") () : unit =
   trm ~style ~msg (**:(add_linebreak msg)*) (Trace.ast ())
 *)
@@ -179,9 +179,9 @@ module At = struct
 
   (* Operations *)
 
-(* DEPRECATED: use ShowAt.trm []
+(* DEPRECATED: use Show.At.trm []
   let ast ?(msg : string = "") (tg : Target.target) : unit =
-    if tg <> [] then fail None "ShowAt.ast: can only be called on the root, with argument []";
+    if tg <> [] then fail None "Show.At.ast: can only be called on the root, with argument []";
     ast ~msg ()
     *)
 
@@ -399,5 +399,5 @@ type style = {
 *)
 
 (* = Show.trm ~style msg (Target.resolve_path p) *)
-(* = ShowAt.trm ~style msg (Target.of_path p) *)
+(* = Show.At.trm ~style msg (Target.of_path p) *)
 (* let current_ast_at_path ?(style = Display) ?(msg : string = "") (p : Path.path) : *)

lib/framework/target/constr.ml

@@ -13,6 +13,8 @@ exception Resolve_target_failure of string
 (* TODO deprecate this after Target.iter is used everywhere *)
 let old_resolution = ref false
 
+let debug_marks = true
+
 (******************************************************************************)
 (*                        Data structure for targets                          *)
 (******************************************************************************)
@@ -826,9 +828,12 @@ let rec check_constraint ~(incontracts:bool) (c : constr) (t : trm) : bool =
 
   | Constr_prim (pred_ty, pred_prim), Trm_prim (ty1, p1) ->
     pred_ty ty1 && pred_prim p1
+
   | Constr_mark (pred, _m), _ ->
     if !old_resolution then begin
       let t_marks = trm_get_marks t in
+      if debug_marks then
+        begin Printf.printf "check_constraint: marks of term are [%s]" (String.concat "; " t_marks) end;
       begin match t.desc with
       | Trm_seq (tl, _) ->
         (List.exists pred t_marks) || (List.fold_left (fun acc x -> (List.exists pred x) || acc) false (Mlist.get_marks tl))

lib/framework/target/path.ml

@@ -5,6 +5,7 @@ open Typ
 open Contextualized_error
 open Mark
 open Tools
+open Seq_helper
 
 (***********************************************************************************)
 (*                               Auxiliary functions                               *)
@@ -57,7 +58,6 @@ let apply_on_path (transfo : trm -> trm) (t : trm) (dl : path) : trm =
         (* trm_fail t *)
         path_fail dl "apply_on_path: Dir_before should not remain at this stage; probably the transformation was not expecting a target-between (tBefore, tAfter, ...)"
       | Dir_span _, _ ->
-        (* trm_fail t *)
         path_fail dl "apply_on_path: Dir_span should not remain at this stage; probably the transformation was not expecting a target-span (tSpan)"
       | Dir_seq_nth n, Trm_seq (tl, result) ->
         { t with desc = Trm_seq (Mlist.update_nth n aux tl, result) }
@@ -241,7 +241,15 @@ let resolve_path_and_ctx (dl : path) (t : trm) : trm * (trm list) =
       let loc = t.loc in
       begin match d, t.desc with
       | Dir_before _, _ -> trm_fail t "aux_on_path_rec: Dir_before should not remain at this stage"
-      | Dir_span _, _ -> trm_fail t "aux_on_path_rec: Dir_span should not remain at this stage"
+      | Dir_span {start; stop}, Trm_seq (instrs, result) ->
+        if start > stop then begin
+          trm_fail t (Printf.sprintf "aux_on_path_rec: Dir_span has an impossible span [%n; %n]" start stop)
+        end else begin
+          let (span_instrs, _instrs_after) = Mlist.split ~left_bias:false stop instrs in
+          let (_instrs_before, span_instrs) = Mlist.split ~left_bias:true start span_instrs in
+          let t_seq = trm_seq ?result span_instrs in
+          aux t_seq
+        end
       | Dir_seq_nth n, Trm_seq (tl, result) ->
         let tl = Mlist.to_list tl in
         (* DEPRECATED:

lib/transfo/loop.ml

@@ -158,8 +158,8 @@ let%transfo hoist_alloc_loop_list
         (* Transfo_debug.path "p_nested" p_nested;
         Transfo_debug.path "p" p; *)
         Matrix_basic.simpl_access_of_access (target_of_path p);
-        (* ShowAt.trm ~msg:"t@p" (target_of_path p);
-        ShowAt.trm ~msg:"t@p" (target_of_path (p @ [Dir_arg_nth 1])); *)
+        (* Show.At.trm ~msg:"t@p" (target_of_path p);
+        Show.At.trm ~msg:"t@p" (target_of_path (p @ [Dir_arg_nth 1])); *)
         Matrix_basic.simpl_index_add (target_of_path (p @ [Dir_arg_nth 1]));
         Arith.(simpl_rec gather_rec (target_of_path (p @ [Dir_arg_nth 1])));
       ) [nbAny; cMark mark]