interp: pretty printing of arrays

src/coq-tactic/why3tac.ml

@@ -1216,8 +1216,8 @@ let why3tac ?(timelimit=timelimit) s gl =
       | Valid -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"
       | Unknown s -> error ("Don't know: " ^ s)
-      | Failure s -> error ("Failure: " ^ s)
-      | Timeout -> error "Timeout"
+      | Call_provers.Failure s -> error ("Failure: " ^ s)
+      | Call_provers.Timeout -> error "Timeout"
       | OutOfMemory -> error "Out Of Memory"
       | HighFailure ->
           error ("Prover failure\n" ^ res.pr_output ^ "\n")

src/main.ml

@@ -601,17 +601,21 @@ let do_exec env fname cin exec =
               begin
                 match res with
                 | Mlw_interp.Normal _ ->
-                  printf "@\nresult: %a@\nstate: %a@]@." 
-                    Mlw_interp.print_result res
+                  printf "@\nresult: %a@\nstate: %a@]@."
+                    (Mlw_interp.print_result m.Mlw_module.mod_known
+                       m.Mlw_module.mod_theory.Theory.th_known st) res
                     Mlw_interp.print_state st
                 | Mlw_interp.Excep _ ->
-                  printf "@\nexceptional result: %a@\nstate: %a@]@." 
-                    Mlw_interp.print_result res
+                  printf "@\nexceptional result: %a@\nstate: %a@]@."
+                    (Mlw_interp.print_result m.Mlw_module.mod_known
+                       m.Mlw_module.mod_theory.Theory.th_known st) res
                     Mlw_interp.print_state st;
                   exit 1
-                | Mlw_interp.Irred _ | Mlw_interp.Fun _ -> 
+                | Mlw_interp.Irred _ | Mlw_interp.Fun _ ->
                   printf "@]@.";
-                  eprintf "Execution error: %a@." Mlw_interp.print_result res;
+                  eprintf "Execution error: %a@."
+                    (Mlw_interp.print_result m.Mlw_module.mod_known
+                       m.Mlw_module.mod_theory.Theory.th_known st) res;
                   exit 2
               end
             | _ ->

src/parser/typing.ml

@@ -281,7 +281,7 @@ let rec dpat uc env pat =
 and dpat_node loc uc env = function
   | PPpwild ->
       let ty = fresh_type_var loc in
-      env, Pwild, ty
+      env, Denv.Pwild, ty
   | PPpvar x ->
       let ty = fresh_type_var loc in
       let env = add_var x.id ty env in
@@ -303,7 +303,7 @@ and dpat_node loc uc env = function
             renv := env;
             e
         | None ->
-            { dp_node = Pwild; dp_ty = ty }
+            { dp_node = Denv.Pwild; dp_ty = ty }
       in
       let al = List.map2 get_val pjl tyl in
       !renv, Papp (cs, al), Opt.get ty

src/session/session.mli

@@ -469,8 +469,10 @@ val goal_task_or_recover: 'a env_session -> 'a goal -> Task.task
 (** {3 recursive} *)
 
 val goal_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key goal -> unit
+(* unused
 val transf_iter_proof_attempt :
   ('key proof_attempt -> unit) -> 'key transf -> unit
+*)
 val theory_iter_proof_attempt :
   ('key proof_attempt -> unit) -> 'key theory -> unit
 val transf_iter_proof_attempt :
@@ -506,7 +508,9 @@ val iter_session :
 
 
 val goal_iter : ('key any -> unit) -> 'key goal -> unit
+(* unused
 val transf_iter : ('key any -> unit) -> 'key transf -> unit
+*)
 val theory_iter : ('key any -> unit) -> 'key theory -> unit
 val transf_iter : ('key any -> unit) -> 'key transf -> unit
 val metas_iter : ('key any -> unit) -> 'key metas -> unit

src/transform/inlining.ml

@@ -63,10 +63,12 @@ let fold in_goal notdeft notdeff notls d (env, task) =
           not (TermTF.t_select notdeft notdeff e
             || t_s_any Util.ffalse (ls_equal ls) e) in
         let env = if inline then Mls.add ls (vl,e) env else env in
-        let task = if inline && not in_goal then task else add_decl task d in
+        let task =
+          if inline && not in_goal then task else Task.add_decl task d
+        in
         env, task
     | _ ->
-        env, add_decl task d
+        env, Task.add_decl task d
 
 let fold in_goal notdeft notdeff notls task_hd (env, task) =
   match task_hd.task_decl.td_node with

src/why3bench/bench.ml

@@ -467,7 +467,7 @@ let empty_tool_res =
       match r with
         | Done (_,t) -> max acc t
         | InternalFailure _ -> acc ) 0. l
-  open Format
+
 (**
 answer output time
 

src/why3bench/db.ml

@@ -15,6 +15,8 @@ open Sqlite3
 
 type transaction_mode = | Deferred | Immediate | Exclusive
 
+let _ = Exclusive
+
 type handle = {
   raw_db : Sqlite3.db;
   mutable in_transaction: int;

src/whyml/mlw_interp.ml

@@ -33,9 +33,9 @@ type value =
 (*
   | Varray of Big_int.big_int * value * value Nummap.t
               (* length, default, elements *)
+*)
   | Vmap of value * value Nummap.t
               (* default, elements *)
-*)
   | Vbin of binop * value * value
   | Veq of value * value
   | Vnot of value
@@ -44,11 +44,10 @@ type value =
   | Veps of term_bound
   | Vcase of value * term_branch list
 
+let array_cons_ls = ref ps_equ
+
 let rec print_value fmt v =
   match v with
-  | Vapp(ls,vl) ->
-    fprintf fmt "@[%a(%a)@]"
-      Pretty.print_ls ls (Pp.print_list Pp.comma print_value) vl
   | Vnum n ->
     fprintf fmt "%s" (Big_int.string_of_big_int n)
   | Vbool b ->
@@ -56,9 +55,15 @@ let rec print_value fmt v =
   | Vvoid ->
     fprintf fmt "()"
   | Vreg reg -> Mlw_pretty.print_reg fmt reg
-(*
-  | Varray(len, def, m) ->
-    fprintf fmt "@[";
+  | Vmap(def,m) ->
+    fprintf fmt "@[[def=%a" print_value def;
+    Nummap.iter
+      (fun i v ->
+        fprintf fmt ",@ %s -> %a" (Big_int.string_of_big_int i) print_value v)
+      m;
+    fprintf fmt "]@]"
+  | Vapp(ls,[Vnum len;Vmap(def,m)]) when ls_equal ls !array_cons_ls ->
+    fprintf fmt "@[[";
     let i = ref Big_int.zero_big_int in
     while Big_int.lt_big_int !i len do
       let v =
@@ -71,7 +76,9 @@ let rec print_value fmt v =
       i := Big_int.succ_big_int !i
     done;
     fprintf fmt "]@]"
-*)
+  | Vapp(ls,vl) ->
+    fprintf fmt "@[%a(%a)@]"
+      Pretty.print_ls ls (Pp.print_list Pp.comma print_value) vl
   | Vbin(op,v1,v2) ->
     fprintf fmt "@[(%a %a@ %a)@]"
       print_value v1 (Pretty.print_binop ~asym:false) op print_value v2
@@ -225,18 +232,6 @@ let builtins = Hls.create 17
 
 let ls_minus = ref ps_equ (* temporary *)
 
-(*
-let term_of_big_int i =
-  if Big_int.sign_big_int i >= 0 then
-    let s = Big_int.string_of_big_int i in
-    t_const (Number.ConstInt (Number.int_const_dec s))
-  else
-    let i = Big_int.minus_big_int i in
-    let s = Big_int.string_of_big_int i in
-    let c = t_const (Number.ConstInt (Number.int_const_dec s)) in
-    t_app_infer !ls_minus [c]
-*)
-
 exception NotNum
 
 let big_int_of_const c =
@@ -249,16 +244,6 @@ let big_int_of_value v =
     | Vnum i -> i
     | _ -> assert false
 
-(*
-let rec big_int_of_term t =
-  match t.t_node with
-    | Tconst c -> big_int_of_const c
-    | Tapp(ls,[t1]) when ls_equal ls !ls_minus ->
-      let i = big_int_of_term t1 in
-      Big_int.minus_big_int i
-    | _ -> raise NotNum
-*)
-
 let eval_true _ls _l = Vbool true
 
 let eval_false _ls _l = Vbool false
@@ -294,20 +279,6 @@ let eval_int_rel op ls l =
   | _ -> Vapp(ls,l)
 
 
-(*
-let is_true t =
-  match t.t_node with
-    | Ttrue -> true
-    | Tapp(ls,[]) when ls_equal ls fs_bool_true -> true
-    | _ -> false
-
-let is_false t =
-  match t.t_node with
-    | Tfalse -> true
-    | Tapp(ls,[]) when ls_equal ls fs_bool_false -> true
-    | _ -> false
-*)
-
 let must_be_true b =
   if b then true else raise Undetermined
 
@@ -367,51 +338,64 @@ let ls_map_set = ref ps_equ
 
 let eval_map_const ls l =
   match l with
-(*
-    | [d] -> Vintmap(d,Nummap.empty)
-*)
+    | [d] -> Vmap(d,Nummap.empty)
     | _ -> Vapp(ls,l)
 
 let eval_map_get ls_get l =
   match l with
-    | [m;x] ->
+  | [m;x] ->
       (* eprintf "Looking for get:"; *)
-      let rec find m =
-        match m with
-          | Vapp(ls,[m';y;v]) when ls_equal ls !ls_map_set ->
-            begin try
-                    if value_equality x y then
-                      ((* Format.eprintf "ok!@.";*) v)
-                    else
-                      ((* Format.eprintf "recur...@.";*) find m' )
-              with Undetermined ->
-                (* Format.eprintf "failed.@."; *)
-                Vapp(ls_get,[m;x])
+    let rec find m =
+      match m with
+      | Vmap(def,m) ->
+        begin
+          match x with
+          | Vnum i ->
+            begin try Nummap.find i m
+              with Not_found -> def
             end
-          | Vapp(ls,[def]) when ls_equal ls !ls_map_const -> def
-          | _ -> Vapp(ls_get,[m;x])
-      in find m
-    | _ -> assert false
+          | _ -> assert false
+        end
+      | Vapp(ls,[m';y;v]) when ls_equal ls !ls_map_set ->
+        begin try
+                if value_equality x y then
+                  ((* Format.eprintf "ok!@.";*) v)
+                else
+                  ((* Format.eprintf "recur...@.";*) find m' )
+          with Undetermined ->
+              (* Format.eprintf "failed.@."; *)
+            Vapp(ls_get,[m;x])
+        end
+      | Vapp(ls,[def]) when ls_equal ls !ls_map_const -> def
+      | _ -> Vapp(ls_get,[m;x])
+    in find m
+  | _ -> assert false
 
 let eval_map_set ls_set l =
   match l with
-    | [m;x;v] ->
-      let rec compress m =
-        match m with
-          | Vapp(ls,[m';y;v']) when ls_equal ls !ls_map_set ->
-            begin try
-                    if value_equality x y then
-                      Vapp(ls_set,[m';x;v])
-                    else
-                      let c = compress m' in
-                      Vapp(ls_set,[c;y;v'])
-              with Undetermined ->
-                Vapp(ls_set,[m;x;v])
-            end
-          | _ ->
+  | [m;x;v] ->
+    let rec compress m =
+      match m with
+      | Vmap(def,m) ->
+        begin
+          match x with
+          | Vnum i -> Vmap(def,Nummap.add i v m)
+          | _ -> assert false
+        end
+      | Vapp(ls,[m';y;v']) when ls_equal ls !ls_map_set ->
+        begin try
+                if value_equality x y then
+                  Vapp(ls_set,[m';x;v])
+                else
+                  let c = compress m' in
+                  Vapp(ls_set,[c;y;v'])
+          with Undetermined ->
             Vapp(ls_set,[m;x;v])
-      in compress m
-    | _ -> assert false
+        end
+      | _ ->
+        Vapp(ls_set,[m;x;v])
+    in compress m
+  | _ -> assert false
 
 (* all builtin functions *)
 
@@ -548,19 +532,17 @@ type result =
 
 let builtin_progs = Hps.create 17
 
-let array_cons_ls = ref ps_equ
-
 let builtin_array_type kn its =
   let csl = Mlw_decl.find_constructors kn its in
   match csl with
     | [(pls,_)] -> array_cons_ls := pls.pl_ls
     | _ ->  assert false
 
-let exec_array_make env _spec s vty args =
+let exec_array_make env s vty args =
   match args with
     | [Vnum n;def] ->
 (**)
-      let m = Vapp(!ls_map_const,[def]) in
+      let m = Vmap(def,Nummap.empty) in
       let v = Vapp(!array_cons_ls,[Vnum n;m]) in
       let s',v' = to_program_value env s vty v in
 (**)
@@ -570,7 +552,7 @@ let exec_array_make env _spec s vty args =
       Normal v',s'
     | _ -> assert false
 
-let exec_array_get _env _spec s _vty args =
+let exec_array_get _env s _vty args =
   match args with
     | [t;Vnum i] ->
       begin
@@ -609,7 +591,7 @@ let exec_array_get _env _spec s _vty args =
       end
     | _ -> assert false
 
-let exec_array_length _env _spec s _vty args =
+let exec_array_length _env s _vty args =
   match args with
     | [t] ->
       begin
@@ -620,7 +602,7 @@ let exec_array_length _env _spec s _vty args =
       end
     | _ -> assert false
 
-let exec_array_set _env _spec s _vty args =
+let exec_array_set _env s _vty args =
   match args with
     | [t;i;v] ->
       begin
@@ -732,7 +714,7 @@ let rec to_logic_value env s v =
       with Not_found -> r
     in
     Mreg.find r' s
-  | Vnum _ | Vbool _ | Vvoid -> v
+  | Vnum _ | Vbool _ | Vvoid | Vmap _ -> v
   | Vbin(Tand,t1,t2) ->
     v_and (eval_rec t1) (eval_rec t2)
   | Vbin(Tor,t1,t2) ->
@@ -943,13 +925,29 @@ and p_expr fmt e =
     | Eassert (_, _) -> fprintf fmt "@[Eassert(_,@ _)@]"
     | Eabsurd -> fprintf fmt "@[Eabsurd@]"
 
-let print_result fmt r =
+let print_result mkm tkm s fmt r =
   match r with
     | Normal t ->
-      fprintf fmt "@[%a@]" print_value t
+      let env = {
+        mknown = mkm;
+        tknown = tkm;
+        regenv = Mreg.empty;
+        vsenv = Mvs.empty;
+      }
+      in
+      let v = to_logic_value env s t in
+      fprintf fmt "@[%a@]" print_value v
     | Excep(x,t) ->
+      let env = {
+        mknown = mkm;
+        tknown = tkm;
+        regenv = Mreg.empty;
+        vsenv = Mvs.empty;
+      }
+      in
+      let v = to_logic_value env s t in
       fprintf fmt "@[exception %s(@[%a@])@]"
-        x.xs_name.Ident.id_string print_value t
+        x.xs_name.Ident.id_string print_value v
     | Irred e ->
       fprintf fmt "@[Cannot execute expression@ @[%a@]@]"
         p_expr e
@@ -957,6 +955,7 @@ let print_result fmt r =
       fprintf fmt "@[Result is a function@]"
 
 
+
 (* evaluation of WhyML expressions *)
 
 
@@ -992,7 +991,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
         end
       | LetA _ -> Irred e, s
     end
-  | Eapp(e1,pvs,spec) ->
+  | Eapp(e1,pvs,_spec) ->
     begin match eval_expr env s e1 with
       | Fun(ps,args,n), s' ->
         if n > 1 then
@@ -1005,7 +1004,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
           in
           begin
             try
-              exec_app env s' ps (pvs::args) spec ity_result
+              exec_app env s' ps (pvs::args) (*spec*) ity_result
             with Exit -> Irred e, s
           end
       | _ -> Irred e, s
@@ -1153,7 +1152,7 @@ and exec_match env t s ebl =
   in
   iter ebl
 
-and exec_app env s ps args spec ity_result =
+and exec_app env s ps args (*spec*) ity_result =
   let args' = List.rev_map (fun pvs -> get_pvs env (*s*) pvs) args in
   let args_ty = List.rev_map (fun pvs -> pvs.pv_ity) args in
   let subst =
@@ -1190,7 +1189,7 @@ and exec_app env s ps args spec ity_result =
           ps.ps_name.Ident.id_string print_regenv env1.regenv
           print_state s;
 *)
-        let r,s' = f env1 spec s (VTvalue ity_result) args' in
+        let r,s' = f env1 (*spec*) s (VTvalue ity_result) args' in
 (*
         eprintf "@[Return from builtin function %s value %a in state:@\n%a@]@."
           ps.ps_name.Ident.id_string

src/whyml/mlw_interp.mli

@@ -23,8 +23,6 @@ type result = private
   | Irred of Mlw_expr.expr
   | Fun of Mlw_expr.psymbol * Mlw_ty.pvsymbol list * int
 
-val print_result: Format.formatter -> result -> unit
-
 type state
 
 val print_state: Format.formatter -> state -> unit
@@ -32,3 +30,6 @@ val print_state: Format.formatter -> state -> unit
 val eval_global_expr: Env.env ->
   Mlw_decl.known_map -> Decl.known_map -> Mlw_expr.expr -> result * state
 
+val print_result: Mlw_decl.known_map -> Decl.known_map -> state -> Format.formatter -> result -> unit
+
+

src/whyml/mlw_module.ml

@@ -495,7 +495,9 @@ let clone_export uc m inst =
         add_pdecl uc (create_val_decl (LetV npv))
     | PDval (LetA ps) ->
         let aty = conv_aty !mvs ps.ps_aty in
-        let nps = create_psymbol (id_clone ps.ps_name) ~ghost:ps.ps_ghost aty in
+        let nps =
+          Mlw_expr.create_psymbol (id_clone ps.ps_name) ~ghost:ps.ps_ghost aty
+        in
         Hid.add psh ps.ps_name (PS nps);
         add_pdecl uc (create_val_decl (LetA nps))
     | PDrec fdl ->
@@ -507,7 +509,7 @@ let clone_export uc m inst =
           (* we save all external pvsymbols to preserve the effects *)
           let spec = { aty.aty_spec with c_variant = vari } in
           let aty = vty_arrow ~spec aty.aty_args aty.aty_result in
-          let nps = create_psymbol id ~ghost:ps.ps_ghost aty in
+          let nps = Mlw_expr.create_psymbol id ~ghost:ps.ps_ghost aty in
           Hid.add psh ps.ps_name (PS nps);
           add_pdecl uc (create_val_decl (LetA nps)) in
         List.fold_left conv_fd uc fdl

src/whyml/mlw_module.mli

@@ -58,7 +58,7 @@ type modul = private {
   mod_theory: theory;			(* pure theory *)
   mod_decls : pdecl list;		(* module declarations *)
   mod_export: namespace;		(* exported namespace *)
-  mod_known : known_map;		(* known identifiers *)
+  mod_known : Mlw_decl.known_map;	(* known identifiers *)
   mod_local : Sid.t;			(* locally declared idents *)
   mod_used  : Sid.t;			(* used modules *)
 }
@@ -75,7 +75,7 @@ val close_namespace : module_uc -> bool -> module_uc
 
 val get_theory : module_uc -> theory_uc
 val get_namespace : module_uc -> namespace
-val get_known : module_uc -> known_map
+val get_known : module_uc -> Mlw_decl.known_map
 
 val restore_path : ident -> string list * string * string list
 (** [restore_path id] returns the triple (library path, module,

tests/test-eval.why

@@ -88,12 +88,17 @@ theory T
 
   use import map.Map
 
-  constant t : map int int = (const 0)[1<-42]
+  constant t0 : map int int = (const 42)
 
-  constant x0 : int = t[0]
-  constant x1 : int = t[1]
+  constant a0 : int = t0[0]
+  constant a1 : int = t0[1]
 
-  constant t2 : map int int = t[2<-37]
+  constant t1 : map int int = (const 0)[1<-42]
+
+  constant x0 : int = t1[0]
+  constant x1 : int = t1[1]
+
+  constant t2 : map int int = t1[2<-37]
 
   constant y0 : int = t2[0] (* should be 0 *)
   constant y1 : int = t2[1] (* should be 42 *)