Evaluate a logic constant in IDE

src/ide/gmain.ml

@@ -1571,18 +1571,125 @@ to the <b>selected goals</b>";
 (* Run  menu *)
 (*************)
 
-(*
 let run_menu = factory#add_submenu "_Run"
 let run_factory = new GMenu.factory run_menu ~accel_group
 
+let eval const result =
+  let msg =
+    match Str.split (Str.regexp "\\.") const with
+      | [f;m;i] ->
+        begin
+          let e = env_session () in
+          let files = e.S.files in
+          try
+            let fi = Mstr.find f files in
+            try
+              let th = Mstr.find m fi in
+              begin
+                try
+                  let ls = Theory.ns_find_ls th.Theory.th_export [i] in
+                  match Decl.find_logic_definition th.Theory.th_known ls with
+                    | None ->
+                      Pp.sprintf
+                        "Symbol '%s' has no definition in theory '%s.%s'" i f m
+                    | Some d ->
+                      let l,t = Decl.open_ls_defn d in
+                      match l with
+                        | [] ->
+                          let t =
+                            Mlw_interp.eval_global_term e.S.env
+                              th.Theory.th_known t
+                          in
+                          Pp.sprintf "@[<hov 2>%a@]" Pretty.print_term t
+                        | _ ->
+                          Pp.sprintf
+                            "Symbol '%s' is not a constant in theory '%s.%s'"
+                            i f m
+                with Not_found ->
+                  Pp.sprintf
+                    "Constant '%s' not found in theory '%s.%s'" i f m
+              end
+            with Not_found ->
+              Pp.sprintf "theory '%s.%s' not found" f m;
+          with Not_found ->
+            Pp.sprintf "@[<hov 2>file '%s' not found. Files are: [%a]@]" f
+              (Pp.print_list Pp.comma Pp.string)
+              (Mstr.keys files)
+        end
+      | _ ->
+        "must be of the form 'file.module.ident'";
+  in
+  result#source_buffer#set_text msg
+
+let constant_to_evaluate = ref ""
+
+let evaluate_window () =
+  let dialog = GWindow.dialog ~modal:true
+    ~title:"Why3: evaluate constant" ~icon:!Gconfig.why_icon ()
+  in
+  let vbox = dialog#vbox in
+  let frame =
+    GBin.frame ~label:"Evaluation" ~shadow_type:`ETCHED_OUT
+    ~packing:vbox#add ()
+  in
+  let vbox = GPack.vbox ~packing:frame#add () in
+  let text =
+    "Enter the constant to evaluate under the form <theory name>.<identifier>"
+  in
+  let _ = GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:vbox#add () in
+  let exec_entry =
+    GEdit.entry ~text:!constant_to_evaluate ~packing:vbox#add ()
+  in
+  let (_ : GtkSignal.id) =
+    exec_entry#connect#changed ~callback:
+      (fun () -> constant_to_evaluate := exec_entry#text)
+  in
+  let b = GButton.button ~label:"Run" ~packing:vbox#add () in
+
+  let text =
+    "Result:"
+  in
+  let _input = GMisc.label ~ypad:20 ~text ~xalign:0.0 ~packing:vbox#add () in
+(*
+  let _ = input#event#connect#key_press ~callback:
+    (fun k -> if GdkEvent.Key.keyval k = GdkKeysyms._Return then
+        eval !constant_to_evaluate view;
+      true)
+  in
+*)
+ let scroll =
+   GBin.scrolled_window
+     ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
+     ~shadow_type:`ETCHED_OUT ~packing:vbox#add ()
+ in
+ let view =
+   GSourceView2.source_view
+     ~editable:false
+     ~packing:scroll#add
+     ~height:100
+     ()
+ in
+  let (_ : GtkSignal.id) =
+    b#connect#clicked ~callback:(fun () -> eval !constant_to_evaluate view)
+  in
+  dialog#add_button "Close" `CLOSE ;
+  let _ = dialog#run () in
+  dialog#destroy ()
+
+let (_ : GMenu.image_menu_item) =
+  run_factory#add_image_item
+    ~label:"Evaluate a logic constant"
+    ~callback:evaluate_window
+    ()
+
 let function_to_execute = ref ""
 
 let execute_window () =
   let dialog = GWindow.dialog ~modal:true
-    ~title:"Why3: execute function" ~icon:!Gconfig.why_icon () 
+    ~title:"Why3: execute function" ~icon:!Gconfig.why_icon ()
   in
   let vbox = dialog#vbox in
-  let text = 
+  let text =
     "Enter the function to execute under the form <module name>.<function name>"
   in
   let _ = GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:vbox#add () in
@@ -1593,17 +1700,19 @@ let execute_window () =
     exec_entry#connect#changed ~callback:
       (fun () -> function_to_execute := exec_entry#text)
   in
-  dialog#add_button "Run" `CLOSE ;
+  dialog#add_button "Close" `CLOSE ;
   let ( _ : GWindow.Buttons.about) = dialog#run () in
   dialog#destroy ()
 
+(*
 let (_ : GMenu.image_menu_item) =
   run_factory#add_image_item
-    ~label:"Execute function"
+    ~label:"Execute a WhyML function"
     ~callback:execute_window
     ()
 *)
 
+
 (*************)
 (* Help menu *)
 (*************)

src/session/session.ml

@@ -227,6 +227,7 @@ type 'a env_session =
     { env : Env.env;
       mutable whyconf : Whyconf.config;
       loaded_provers : loaded_provers;
+      files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
       session : 'a session}
 
 let update_env_session_config e c = e.whyconf <- c
@@ -2086,19 +2087,28 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf =
     { session = new_session;
       env = env;
       whyconf = whyconf;
+      files = Mstr.empty;
       loaded_provers = PHprover.create 5;
     }
   in
   found_obsolete := false;
-  PHstr.iter (fun _ old_file ->
-    dprintf debug "[Load] file '%s'@\n" old_file.file_name;
-    let new_file,theories = add_file_return_theories
-      ~keygen new_env_session
-      ?format:old_file.file_format old_file.file_name
-    in
-    merge_file ~keygen ~theories
-      new_env_session ~allow_obsolete old_file new_file)
-    old_session.session_files;
+  let files = 
+    PHstr.fold (fun _ old_file acc ->
+      dprintf debug "[Load] file '%s'@\n" old_file.file_name;
+      let new_file,theories = add_file_return_theories
+        ~keygen new_env_session
+        ?format:old_file.file_format old_file.file_name
+      in
+      merge_file ~keygen ~theories
+        new_env_session ~allow_obsolete old_file new_file;
+      let fname = 
+        Filename.basename (Filename.chop_extension old_file.file_name) 
+      in
+      Mstr.add fname theories acc)
+      old_session.session_files
+      Mstr.empty
+  in
+  let new_env_session = { new_env_session with files = files } in
   dprintf debug "[Info] update_session: done@\n";
   let obsolete =
     if old_session.session_shape_version <> Termcode.current_shape_version

src/session/session.mli

@@ -202,6 +202,7 @@ type 'a env_session = private
     { env : Env.env;
       mutable whyconf : Whyconf.config;
       loaded_provers : loaded_provers;
+      files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
       session : 'a session}
 
 val update_env_session_config : 'a env_session -> Whyconf.config -> unit

src/whyml/mlw_interp.ml

@@ -401,7 +401,9 @@ let rec eval_term env s ty t =
     let v,t2 = t_open_bound tb in
     eval_term (bind_vs v u env) s ty t2
   | Tcase(t1,tbl) ->
+(*
     eprintf "found a match ... with ...@.";
+*)
     let u = eval_rec t1 in
     eval_match env s ty u tbl
   | Tquant _

tests/test-eval.why

@@ -103,4 +103,17 @@ theory T
   constant z1 : int = t3[1]
   constant z2 : int = t3[2]
 
-end
\ No newline at end of file
+end
+
+
+theory Records 
+
+  use import int.Int
+
+  type pt = { x : int ; y : int }
+
+  constant pt1 : pt = { x = 3 ; y = 4 }
+
+  constant t1 : int = pt1.x + pt1.y
+
+end