Fixes

src/bin/stats.ml

@@ -110,6 +110,7 @@ let new_input st input_name input_size =
     end else
       st
   in
+  Tui.printf "new input : %s / size : %d@." input_name input_size;
   key, st
 
 let record_parsed st input counter loc =
@@ -131,6 +132,7 @@ let record_parsed st input counter loc =
           let typing = State.get typing_key st in
           Tui.Bar.add_to_process typing ~loc
         end;
+        Tui.printf "parsed(%s): %a@." (State.key_name input) Dolmen.Std.Loc.print_compact loc;
         st
     end
 

src/loop/state.ml

@@ -151,6 +151,7 @@ let set k v t =
 let update k f t =
   set k (f (get k t)) t
 
+let key_name { name; _ } = name
 
 (* Some common keys *)
 (* ************************************************************************* *)

src/loop/typer_intf.ml

@@ -116,7 +116,8 @@ module type Typer_Full = sig
   (** The typechecker needs to know whether we are checking models or not. *)
 
   val smtlib2_forced_logic : string option key
-  (** The typechecker needs to know whether we are checking models or not. *)
+  (** Force the typechecker to use the given logic (instead of using the one declared
+      in the `set-logic` statement). *)
 
   val init :
     ?ty_state:ty_state ->

src/model/loop.ml

@@ -6,18 +6,19 @@
 (* State *)
 (* ************************************************************************ *)
 
-type model = Model.t
+type typed_model = Model.t
+type parsed_model = Dolmen.Std.Statement.defs list
 type cst = Dolmen.Std.Expr.term_cst
 type term = Dolmen.Std.Expr.Term.t
 
-type answer =
-  | Sat of model
+type 'model answer =
+  | Sat of 'model
   | Unsat of Dolmen.Std.Loc.full
   | Error of Dolmen.Std.Loc.full
 
 type 'st answers =
   | Init
-  | Response_loaded of ('st -> 'st * answer option)
+  | Response_loaded of ('st -> 'st * parsed_model answer option)
 
 type 't located = {
   contents : 't;
@@ -34,7 +35,7 @@ type acc = {
 
 type internal =
   | Full_check of { acc : acc; }
-  | Fast_check of { answer : answer option; }
+  | Fast_check of { answer : (typed_model * parsed_model) answer option; }
 
 type 'st t = {
   internal : internal;
@@ -255,8 +256,10 @@ module Make
     in
     { contents; loc; file; }
 
-  let record_defs ~loc ~(file : _ file) st model typed_defs =
-    List.fold_left (fun (st, model) def ->
+  let record_defs st model (parsed_defs : Dolmen.Std.Statement.defs) typed_defs =
+    let file = State.get State.response_file st in
+    List.fold_left2 (fun (st, model) (parsed : Dolmen.Std.Statement.def) def ->
+        let loc = Dolmen.Std.Loc.{ file = file.loc; loc = parsed.loc; } in
         match def with
         | `Type_def _ ->
           (State.error ~file ~loc st type_def_in_model (), model)
@@ -275,34 +278,66 @@ module Make
               Value.print value;
           let model = Model.Cst.add cst value model in
           (st, model)
-      ) (st, model) typed_defs
+      ) (st, model) parsed_defs.contents typed_defs
 
-  let type_model ~file ~(loc : Dolmen.Std.Loc.full) ?attrs st l =
+  let is_id_declared (ty_state : Dolmen_loop.Typer.T.state) id =
+    match Dolmen_loop.Typer.T.find_global_st ty_state id with
+    | #Dolmen_loop.Typer.T.not_found -> false
+    | #Dolmen_loop.Typer.T.cst -> true
+
+  let are_defs_declared st (defs : Dolmen.Std.Statement.defs) =
+    let typer_state = State.get Typer.ty_state st in
+    let ty_state = Dolmen_loop.Typer.typer_state typer_state in
+    List.for_all (fun (def : Dolmen.Std.Statement.def) ->
+        is_id_declared ty_state def.id
+      ) defs.contents
+
+  let type_model_aux ~input ?attrs (st, model) parsed_defs =
+    if State.get State.debug st then
+      Format.eprintf "[model][parsed] @[<hov>%a@]@."
+        Dolmen.Std.Statement.(print_group print_def) parsed_defs;
+    let st, defs =
+      Typer.defs ~mode:`Use_declared_id st ~input ?attrs parsed_defs
+    in
+    (* Record inferred abstract values *)
+    let model =
+      List.fold_left (fun model c ->
+          let value = Value.abstract_cst c in
+          Model.Cst.add c value model
+        ) model (Typer.pop_inferred_model_constants st)
+    in
+    (* Record the explicit definitions *)
+    let st, model = record_defs st model parsed_defs defs in
+    st, model
+
+  let rec type_model_defined ~input ?attrs st model = function
+    | [] -> st, model, []
+    | (defs :: r) as l ->
+      if are_defs_declared st defs then
+        let st, model = type_model_aux ~input ?attrs (st, model) defs in
+        type_model_defined ~input ?attrs st model r
+      else
+        st, model, l
+
+  let type_model_full ?attrs st l =
+    let file = State.get State.response_file st in
     let input = `Response file in
     let st = Typer.push ~input st 1 in
     let st, model =
-      List.fold_left (fun (st, model) parsed_defs ->
-          if State.get State.debug st then
-            Format.eprintf "[model][parsed][%a] @[<hov>%a@]@."
-              Dolmen.Std.Loc.fmt_compact (Dolmen.Std.Loc.full_loc loc)
-              Dolmen.Std.Statement.(print_group print_def) parsed_defs;
-          let st, defs =
-            Typer.defs ~mode:`Use_declared_id st ~input ~loc:loc.loc ?attrs parsed_defs
-          in
-          (* Record inferred abstract values *)
-          let model =
-            List.fold_left (fun model c ->
-                let value = Value.abstract_cst c in
-                Model.Cst.add c value model
-              ) model (Typer.pop_inferred_model_constants st)
-          in
-          (* Record the explicit definitions *)
-          record_defs ~file ~loc st model defs
-        ) (st, Model.empty) l
+      List.fold_left (type_model_aux ~input ?attrs) (st, Model.empty) l
     in
     let st = Typer.pop st ~input 1 in
     st, model
 
+  let type_model_partial ?attrs st model parsed =
+    let file = State.get State.response_file st in
+    let input = `Response file in
+    let st = Typer.push ~input st 1 in
+    let st, model, parsed = type_model_defined ~input ?attrs st model parsed in
+    let st = Typer.pop st ~input 1 in
+    st, model, parsed
+
+
 
   (* Pipe function *)
   (* ************************************************************************ *)
@@ -323,10 +358,8 @@ module Make
           begin match answer.Dolmen.Std.Answer.descr with
             | Unsat -> st, Some (Unsat loc)
             | Error _ -> st, Some (Error loc)
-            | Sat None -> st, Some (Sat Model.empty)
-            | Sat Some model ->
-              let st, model = type_model ~loc ~file st model in
-              st, Some (Sat model)
+            | Sat None -> st, Some (Sat [])
+            | Sat Some model -> st, Some (Sat model)
           end
       in
       let st =
@@ -335,24 +368,28 @@ module Make
       in
       answers st
 
+  (* TODO: the file and loc parameters are the file and loc of the statement
+     in the original problem (and not the model file) that triggered
+     this module to read the model. Use multi-locs to better explain
+     that. *)
   let fast_check_answer ~file ~loc st t = function
     | Some _ as a -> st, a
     | None ->
       let st, answer = next_answer st in
-      let st =
+      let st, answer =
         match answer with
         | None ->
-          State.error ~file ~loc st missing_answer ()
-        | Some (Error loc) ->
+          State.error ~file ~loc st missing_answer (), None
+        | Some Error loc as a ->
           let file = State.get State.response_file st in
-          State.error ~file ~loc st error_in_response ()
-        | Some Unsat loc ->
+          State.error ~file ~loc st error_in_response (), a
+        | Some Unsat loc as a->
           let file = State.get State.response_file st in
-          State.warn ~file ~loc st cannot_check_proofs ()
-        | Some Sat _ ->
-          st
+          State.warn ~file ~loc st cannot_check_proofs (), a
+        | Some Sat parsed_model ->
+          st, Some (Sat (Model.empty, parsed_model))
       in
-      let t = { t with internal = Fast_check { answer = answer; } } in
+      let t = { t with internal = Fast_check { answer; } } in
       let st = State.set check_state t st in
       st, answer
 
@@ -362,9 +399,10 @@ module Make
     | Fast_check { answer } ->
       let st, answer = fast_check_answer ~file ~loc st t answer in
       begin match answer with
-        | Some Sat model ->
-          let st, model = fast st model in
-          let t = { t with internal = Fast_check { answer = Some (Sat model); } } in
+        | Some Sat (model, parsed) ->
+          let st, model, parsed = type_model_partial st model parsed in
+          let st, model = fast st parsed model in
+          let t = { t with internal = Fast_check { answer = Some (Sat (model, parsed)); } } in
           State.set check_state t st
         | _ -> st
       end
@@ -425,9 +463,9 @@ module Make
   let check_defs st ~file ~loc ~counter defs =
     let new_defs = pack_abstract_defs ~file ~loc defs in
     by_mode ~file ~loc st
-      ~fast:(fun st model ->
+      ~fast:(fun st parsed model ->
           let st, model = eval_def new_defs (st, model) in
-          let st = Stats.record_checked st counter loc.loc (`Set model) in
+          let st = Stats.record_checked st counter loc.loc (`Set (model, parsed)) in
           st, model
         )
       ~full:(fun st acc ->
@@ -439,9 +477,9 @@ module Make
   let check_hyps st ~file ~loc ~counter contents =
     let assertion = { file; loc; contents; } in
     by_mode ~file ~loc st
-      ~fast:(fun st model ->
+      ~fast:(fun st parsed model ->
           let st = eval_hyp model st assertion in
-          let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Set model) in
+          let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Set (model, parsed)) in
           st, model
         )
       ~full:(fun st acc ->
@@ -453,9 +491,9 @@ module Make
   let check_goal st ~file ~loc ~counter contents =
     let assertion = { file; loc; contents; } in
     by_mode ~file ~loc st
-      ~fast:(fun st model ->
+      ~fast:(fun st parsed model ->
           let st = eval_goal model st assertion in
-          let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Set model) in
+          let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Set (model, parsed)) in
           st, model
         )
       ~full:(fun st acc ->
@@ -467,9 +505,9 @@ module Make
   let check_clause st ~file ~loc ~counter contents =
     let assertion = { file; loc; contents; } in
     by_mode ~file ~loc st
-      ~fast:(fun st model ->
+      ~fast:(fun st parsed model ->
           let st = eval_clause model st assertion in
-          let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Set model) in
+          let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Set (model, parsed)) in
           st, model
         )
       ~full:(fun st acc ->
@@ -483,7 +521,7 @@ module Make
     let local_hyps = List.map (fun contents -> { file; loc = no_loc; contents; }) l in
     let st =
       by_mode ~file ~loc st
-        ~fast:(fun st model ->
+        ~fast:(fun st _parsed model ->
             let st = List.fold_left (eval_hyp model) st local_hyps in
             let st = Stats.record_checked st counter loc.loc (`Set Model.empty) in
             st, Model.empty
@@ -499,6 +537,7 @@ module Make
               let file = State.get State.response_file st in
               State.error ~file ~loc st error_in_response (), acc
             | st, Some Sat model ->
+              let st, model = type_model_full st model in
               let acc = { acc with hyps = local_hyps @ acc.hyps; } in
               let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Add local_hyps) in
               let st, model = List.fold_right eval_def acc.defs (st, model) in

src/standard/loc.ml

@@ -110,12 +110,12 @@ let first_byte c =
   start
 
 let last_byte c =
-  let start, offset = split_compact c in
-  start + offset (* +1 ? *)
+  let offset, length = split_compact c in
+  offset + length (* +1 ? *)
 
 let length_in_bytes c =
-  let _, offset = split_compact c in
-  offset + 1
+  let _, length = split_compact c in
+  length + 1
 
 
 (* File table *)

src/standard/loc.mli

@@ -106,3 +106,8 @@ val print_compact : Format.formatter -> t -> unit
 val file_name : file -> string
 (** Filename for a file *)
 
+
+val split_compact : t -> int * int
+
+val mk_compact : int -> int -> t
+

src/typecheck/intf.ml

@@ -501,11 +501,14 @@ module type Formulas = sig
   val find_global : env -> Dolmen.Std.Id.t -> [ cst | not_found ]
   (** Try and find the given id in the set of globally bound constants. *)
 
+  val find_global_st : state -> Dolmen.Std.Id.t -> [ cst | not_found ]
+  (** Try and find the given id in the set of globally bound constants. *)
+
   val find_builtin : env -> Dolmen.Std.Id.t -> [ builtin | not_found ]
   (** Try and find the given id in the set of bound builtin symbols. *)
 
   val find_bound : env -> Dolmen.Std.Id.t -> [ bound | not_found ]
-  (** Try and find a bound identifier in the env, whetehr it be locally bound
+  (** Try and find a bound identifier in the env, whether it be locally bound
       (such as bound variables), constants bound at top-level, or builtin
       symbols bound by the builtin theory. *)
 

src/typecheck/thf.ml

@@ -577,11 +577,14 @@ module Make
         | None -> `Not_found
       end
 
-  let find_global env id : [cst | not_found] =
-    match M.find_opt id env.st.csts with
+  let find_global_st st id : [ cst | not_found ] =
+    match M.find_opt id st.csts with
     | Some res -> (res :> [cst | not_found])
     | None -> `Not_found
 
+  let find_global env id : [cst | not_found] =
+    find_global_st env.st id
+
   let find_builtin env id : [builtin | not_found] =
     match env.builtins env (Id id) with
     | `Not_found -> `Not_found