attempt: make location resolution slightly more powerful?

Signed-off-by: Sacha Ayoun <[email protected]>

GillianCore/engine/FOLogic/Reduction.ml

@@ -2416,74 +2416,51 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     string option =
   let max_fuel = 5 in
 
+  let loc_name = function
+    | Expr.ALoc loc | Lit (Loc loc) -> Some loc
+    | _ -> None
+  in
+
   let rec resolve_expr_to_location_aux
       (fuel : int)
       (tried : Expr.Set.t)
       (to_try : Expr.t list) : string option =
+    let open Syntaxes.Option in
+    let* () = if fuel <= 0 then None else Some () in
     let f = resolve_expr_to_location_aux (fuel - 1) in
-    match fuel = 0 with
-    | true -> None
-    | false -> (
-        match to_try with
-        | [] -> None
-        | e :: _rest -> (
-            match e with
-            | Lit (Loc loc) | ALoc loc -> Some loc
-            | _ -> (
-                let equal_e = get_equal_expressions pfs e in
-                let equal_e =
-                  equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e
-                in
-                let ores =
-                  List.find_opt
-                    (fun x ->
-                      match x with
-                      | Expr.ALoc _ | Lit (Loc _) -> true
-                      | _ -> false)
-                    equal_e
-                in
-                match ores with
-                | Some (ALoc loc) | Some (Lit (Loc loc)) -> Some loc
-                | _ -> (
-                    let lvars_e =
-                      List.map
-                        (fun x -> Expr.LVar x)
-                        (Containers.SS.elements (Expr.lvars e))
-                    in
-                    let found_subst =
-                      List.map
-                        (fun e -> (e, get_equal_expressions pfs e))
-                        lvars_e
-                    in
-                    let found_subst =
-                      List.filter_map
-                        (fun (e, es) ->
-                          match es with
-                          | [] -> None
-                          | es :: _ -> Some (e, es))
-                        found_subst
-                    in
-                    let subst_e =
-                      List.fold_left
-                        (fun (e : Expr.t) (e_to, e_with) ->
-                          Expr.subst_expr_for_expr ~to_subst:e_to
-                            ~subst_with:e_with e)
-                        e found_subst
-                    in
-                    let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
-                    match subst_e with
-                    | ALoc loc | Lit (Loc loc) -> Some loc
-                    | _ ->
-                        let new_tried = Expr.Set.add e tried in
-                        let new_to_try = equal_e @ [ subst_e ] in
-                        let new_to_try =
-                          List.filter
-                            (fun e -> not (Expr.Set.mem e new_tried))
-                            new_to_try
-                        in
-                        f new_tried new_to_try))))
+    let* e, rest =
+      match to_try with
+      | [] -> None
+      | e :: rest -> Some (e, rest)
+    in
+    (* If e is a loc name, we return it *)
+    let/ () = loc_name e in
+    let equal_e = get_equal_expressions pfs e in
+    let equal_e = equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e in
+    (* If we find a loc in there, we return it *)
+    let/ () = List.find_map loc_name equal_e in
+    let found_subst =
+      List.concat_map
+        (fun x ->
+          let e = Expr.LVar x in
+          List.map (fun es -> (e, es)) (get_equal_expressions pfs e))
+        (Containers.SS.elements (Expr.lvars e))
+    in
+    let subst_e =
+      List.fold_left
+        (fun (e : Expr.t) (e_to, e_with) ->
+          Expr.subst_expr_for_expr ~to_subst:e_to ~subst_with:e_with e)
+        e found_subst
+    in
+    let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
+    let/ () = loc_name subst_e in
+    let new_tried = Expr.Set.add e tried in
+    let new_to_try = rest @ equal_e @ [ subst_e ] in
+    let new_to_try =
+      List.filter (fun e -> not (Expr.Set.mem e new_tried)) new_to_try
+    in
+    f new_tried new_to_try
   in
-
   resolve_expr_to_location_aux max_fuel Expr.Set.empty [ e ]
 
 let rec reduce_formula_loop