Use model to simplify report

backend/cn/lib/explain.ml

@@ -4,6 +4,7 @@ module BT = BaseTypes
 module RE = Resources
 module RET = ResourceTypes
 module LC = LogicalConstraints
+module LAT = LogicalArgumentTypes
 module LS = LogicalSorts
 module SymSet = Set.Make (Sym)
 module SymMap = Map.Make (Sym)
@@ -88,6 +89,53 @@ let subterms_without_bound_variables bindings =
     ITSet.empty
 
 
+(** Simplify a constraint in the context of a model. *)
+let simp_constraint eval lct =
+  let eval_to_bool it =
+    match eval it with Some (IT (Const (Bool b1), _, _)) -> Some b1 | _ -> None
+  in
+  let is b it = match eval_to_bool it with Some b1 -> Bool.equal b b1 | _ -> false in
+  let rec go (IT (term, bt, loc)) =
+    let mk x = IT (x, bt, loc) in
+    let ands xs = IT.and_ xs loc in
+    let go1 t = ands (go t) in
+    match term with
+    | Const (Bool true) -> []
+    | Binop (Or, lhs, rhs) when is false lhs -> go rhs
+    | Binop (Or, lhs, rhs) when is false rhs -> go lhs
+    | Binop (And, lhs, rhs) -> List.append (go lhs) (go rhs)
+    | Binop (Implies, lhs, rhs) ->
+      (match eval_to_bool lhs with
+       | Some b -> if b then go rhs else []
+       | None -> [ mk (Binop (Implies, go1 lhs, go1 rhs)) ])
+    | ITE (cond, ifT, ifF) ->
+      (match eval_to_bool cond with
+       | Some b -> if b then go ifT else go ifF
+       | None -> [ mk (ITE (go1 cond, go1 ifT, go1 ifF)) ])
+    | _ -> [ mk term ]
+  in
+  match lct with LC.Forall _ -> [ lct ] | LC.T ct -> List.map (fun x -> LC.T x) (go ct)
+
+
+(** Simplify a resource clause in the context of a model. *)
+let rec simp_resource eval r =
+  match r with
+  | LAT.Constraint (ct, info, more) ->
+    let is_true =
+      match ct with
+      | LC.T ct ->
+        (match eval ct with Some (IT (Const (Bool b), _, _)) -> b | _ -> false)
+      | _ -> false
+    in
+    if is_true then
+      simp_resource eval more
+    else
+      LAT.Constraint (ct, info, simp_resource eval more)
+  | LAT.Define (x, i, more) -> LAT.Define (x, i, simp_resource eval more)
+  | LAT.Resource (x, i, more) -> LAT.Resource (x, i, simp_resource eval more)
+  | I i -> I i
+
+
 let state ctxt model_with_q extras =
   let where =
     let cur_colour = !Cerb_colour.do_colour in
@@ -181,7 +229,7 @@ let state ctxt model_with_q extras =
           | LC.T (IT (Representable _, _, _)) -> false
           | LC.T (IT (Good _, _, _)) -> false
           | _ -> true)
-        (LCSet.elements ctxt.constraints)
+        (List.concat_map (simp_constraint evaluate) (LCSet.elements ctxt.constraints))
     in
     (List.map LC.pp interesting, List.map LC.pp uninteresting)
   in
@@ -233,6 +281,8 @@ let trace (ctxt, log) (model_with_q : Solver.model_with_q) (extras : state_extra
       (statef ctxt
        :: List.filter_map (function State ctxt -> Some (statef ctxt) | _ -> None) log)
   in
+  let model, _quantifier_counter_model = model_with_q in
+  let evaluate it = Solver.eval ctxt.global model it in
   let predicate_hints =
     match extras.request with
     | None -> []
@@ -242,7 +292,9 @@ let trace (ctxt, log) (model_with_q : Solver.model_with_q) (extras : state_extra
        | Owned _ -> []
        | PName pname ->
          let doc_clause (_name, c) =
-           { cond = IT.pp c.guard; clause = LogicalArgumentTypes.pp IT.pp c.packing_ft }
+           { cond = IT.pp c.guard;
+             clause = LogicalArgumentTypes.pp IT.pp (simp_resource evaluate c.packing_ft)
+           }
          in
          List.map doc_clause (relevant_predicate_clauses ctxt.global pname req))
   in

backend/cn/lib/explain.mli

@@ -0,0 +1,28 @@
+(** Manipulate a resource *)
+type action =
+  | Read of IndexTerms.t * IndexTerms.t
+  | Write of IndexTerms.t * IndexTerms.t
+  | Create of IndexTerms.t
+  | Kill of IndexTerms.t
+  | Call of Sym.t * IndexTerms.t list
+  | Return of IndexTerms.t
+
+(** Info about what happened *)
+type log_entry =
+  | Action of action * Locations.t (** We did this. *)
+  | State of Context.t (** Various things we know about. *)
+
+(** Steps we took to get here, most recent first *)
+type log = log_entry list
+
+(** Additional information about what went wrong. *)
+type state_extras =
+  { request : ResourceTypes.t option; (** Requested resource *)
+    unproven_constraint : LogicalConstraints.t option (** Unproven constraint *)
+  }
+
+(** No additional information *)
+val no_ex : state_extras
+
+(** Generate a report describing what went wrong. *)
+val trace : Context.t * log -> Solver.model_with_q -> state_extras -> Report.report

backend/cn/lib/report.ml

@@ -1,9 +1,3 @@
-type state_entry =
-  { loc_e : Pp.document option;
-    loc_v : Pp.document option;
-    state : Pp.document option
-  }
-
 type term_entry =
   { term : Pp.document;
     value : Pp.document

backend/cn/lib/report.mli

@@ -1,17 +1,13 @@
-type state_entry =
-  { loc_e : Pp.document option;
-    loc_v : Pp.document option;
-    state : Pp.document option
-  }
-
+(** Definition of something *)
 type term_entry =
-  { term : Pp.document;
-    value : Pp.document
+  { term : Pp.document; (** The term being evaluated *)
+    value : Pp.document (** Its value in the current context *)
   }
 
+(** A clause for a resource *)
 type predicate_clause_entry =
-  { cond : Pp.document;
-    clause : Pp.document
+  { cond : Pp.document; (** Guard on the resource *)
+    clause : Pp.document (** The actual resource *)
   }
 
 type resource_entry =
@@ -23,21 +19,36 @@ type where_report =
   { fnction : string option;
     section : string option;
     loc_cartesian : ((int * int) * (int * int)) option;
-    loc_head : string
+    (** Where in the source file we are *)
+    loc_head : string (** Name of what we are currently processing *)
   }
 
+(** Information about a specific state of the computation.
+    The resources, constraints, and terms are pairs because they classify
+    how relevant the thing might be:
+    the first component is "interesting", the second is not. *)
 type state_report =
-  { where : where_report;
-    resources : Pp.document list * Pp.document list;
-    constraints : Pp.document list * Pp.document list;
-    terms : term_entry list * term_entry list
+  { where : where_report; (** Location information *)
+    resources : Pp.document list * Pp.document list; (** Resources *)
+    constraints : Pp.document list * Pp.document list; (** Constraints *)
+    terms : term_entry list * term_entry list (** Term values *)
   }
 
+(** Parts of an HTML rendering of an error. *)
 type report =
-  { trace : state_report list;
-    requested : Pp.document option;
-    unproven : Pp.document option;
+  { trace : state_report list; (** The states we went through to get here *)
+    requested : Pp.document option; (** Resource that we failed to construct *)
+    unproven : Pp.document option; (** Fact we failed to prove *)
     predicate_hints : predicate_clause_entry list
+    (** Definitions of resource predicates related to the requested one. *)
   }
 
+(** Save a report to a file.
+    The first argument is the name of the file where the report should be saved.
+    It is also returned as the result of the function.
+
+    The second argument is the C source code for the report, which is used
+    to highlight locations.
+
+    The third argument is information about the various things that need to be saved. *)
 val make : string -> string Option.m -> report -> string