merge

examples/programs/course.mlw

+
+{
+
+  (* preliminaries *)
+
+  use array.Array as A
+
+  type array 'a = A.t int 'a
+
+  logic injective (n:int) (m:int) (a:array 'a) =
+    forall i j:int. n <= i <= m -> n <= j <= m ->
+       A.get a i = A.get a j -> i = j
+
+  type string
+
+  (* Capucine memory model *)
+
+  type pointer = int
+
+  type region 'a = A.t pointer 'a
+
+  type first_free_addr = int
+
+  logic valid (a:first_free_addr) (p:pointer) = p < a
+
+  logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
+     forall i:int. n <= i <= m -> valid a (A.get r i)
+
+}
+
+parameter alloc : ref first_free_addr
+
+parameter new_pointer : tt:unit ->
+  { }
+  pointer
+  writes alloc
+  { !alloc = old !alloc + 1 and result = old !alloc }
+
+(*
+record Student =
+  name: string;
+  mark: int
+  inv(this) { 0 <= this.mark <= 100 }
+end
+*)
+
+{
+
+  type student = (string, int)
+
+  logic invStudent (this:student) =
+     let (_,m) = this in 0 <= m <= 100
+
+}
+
+(*
+record Course =
+  group Rstud: Student;
+  students: array [Rstud]
+  count: int
+  sum: int
+  inv(this) {
+    count >= 0
+    and
+    injective(0, count-1, this.students)
+    and
+    this.sum = mark_sum(0,this.count-1,this.students)
+  }
+end
+*)
+
+{
+
+  type course = (region student, array pointer, int, int)
+
+  logic markSum (region student) int int (array pointer) : int
+
+  axiom MarkSumEmpty :
+    forall r:region student, i j:int, a : array pointer.
+      i > j -> markSum r i j a = 0
+
+  axiom MarkSumNonEmpty :
+    forall r:region student, i j:int, a : array pointer.
+      i <= j ->
+        let (_,mark) = A.get r (A.get a j) in
+        markSum r i j a = markSum r i (j-1) a  + mark
+
+(*
+  lemma MarkSumFootprint:
+  forall n:int. forall s1: array(Student [R1]).
+  forall s2: array(Student [R2]).
+  (forall i:int. [0] <= [i] and [i] < [n] ==>
+     [!(select(s1,i) : Student[R1]).mark] =
+       [!(select(s2,i) : Student[R2]).mark])
+  ==> [MarkSum(n, s1)] = [MarkSum(n,s2)]
+*)
+
+  lemma MarkSum_set_array_outside :
+     forall r:region student, i j k:int, a: array pointer, p:pointer.
+     not (i <= k <= j) ->
+     markSum r i j (A.set a k p) = markSum r i j a
+
+
+  lemma MarkSum_set_region_outside :
+     forall r:region student, i j:int, a: array pointer, p:pointer, s:student.
+     (forall k:int. i <= k <= j -> A.get a k <> p) ->
+     markSum (A.set r p s) i j a = markSum r i j a
+
+
+
+
+  logic invCourse (alloc:first_free_addr) (this:course) =
+     let (rStud,students,count,sum) = this in
+     count >= 0
+     and 
+     valid_array alloc 0 (count - 1) students
+     and
+     injective 0 (count - 1) students
+     and
+     sum = markSum rStud 0 (count-1) students
+
+}
+
+(*
+fun CreateCourse(R:[Course]): [R]
+  consumes R^e
+  produces R^c
+=
+  let c = new Course [R] in
+  c.count = 0;
+  c.sum = 0;
+  pack c;
+  c
+*)
+
+let createCourse (r: (ref (region course))) : pointer =
+  { }
+    let c = new_pointer () in
+    let (rStud,student,count,sum) = A.get !r c in
+    let newc = (rStud,student,0,0) in
+    r := A.set !r c newc;
+    assert { invCourse !alloc newc };
+    c
+  { valid !alloc result }
+
+(*
+fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
+  consumes R^c
+  produces R^c
+=
+  region S in
+  let s = new Student[S] in
+  s := (name, 0);
+  (adoptregion S as R.R_s);
+  assert [MarkSum(!(!c.students))] = [old(MarkSum(!(!c.students)))];
+  (focus !c.students) := add(!(!c.students), s);
+  c := (!c.students, !c.count + 1, !c.total, !c.4);
+  s
+*)
+
+let registerStudent
+    (r: (ref (region course))) (c:pointer) (name:string) : pointer =
+{ valid !alloc c and invCourse !alloc (A.get !r c) }
+  let s = new_pointer () in
+  let (rStud,student,count,sum) = A.get !r c in
+  let newstud = (name,0) in
+  let newc = (A.set rStud s newstud,A.set student count s,count+1,sum) in
+  r := A.set !r c newc;
+  assert { invCourse !alloc newc };
+  s
+{ valid !alloc result }
+
+(*
+
+fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit
+  consumes R^c
+  produces R^c
+{
+  unpack c  (* c.Rstud^G, R^o *)
+  let region Rs:Student
+  let s' = focus s as Rs (* Rs -o c.Rstud, Rs^c, R^o *)
+  unpack s' (* Rs -o c.Rstud, Rs^o, R^o *)
+  s'.mark <- mark;
+  pack s';
+  pack c
+}
+
+*)
+
+
+
+
+
+
+
+
+
+
+

src/ide/gconfig.ml

@@ -206,6 +206,7 @@ let iconname_file = "file32"
 let iconname_prover = "wizard32"
 let iconname_transf = "cutb32"
 let iconname_editor = "edit32"
+let iconname_remove = "deletefile32"
 
 let image_default = ref (image ~size:20 iconname_default)
 let image_scheduled = ref !image_default
@@ -222,6 +223,7 @@ let image_file = ref !image_default
 let image_prover = ref !image_default
 let image_transf = ref !image_default
 let image_editor = ref !image_default
+let image_remove = ref !image_default
 
 let resize_images size =
   image_default := image ~size iconname_default;
@@ -239,6 +241,7 @@ let resize_images size =
   image_prover := image ~size iconname_prover;
   image_transf := image ~size iconname_transf;
   image_editor := image ~size iconname_editor;
+  image_remove := image ~size iconname_remove;
   ()
 
 let () =

src/ide/gconfig.mli

@@ -66,6 +66,7 @@ val image_file : GdkPixbuf.pixbuf ref
 val image_prover : GdkPixbuf.pixbuf ref
 val image_transf : GdkPixbuf.pixbuf ref
 val image_editor : GdkPixbuf.pixbuf ref
+val image_remove : GdkPixbuf.pixbuf ref
 
 (* status icons *)
 val image_scheduled : GdkPixbuf.pixbuf ref

src/ide/gmain.ml

@@ -503,18 +503,25 @@ let task_checksum t =
 
 
 let info_window mt s =
+  let buttons = match mt with
+    | `INFO -> GWindow.Buttons.close
+    | `WARNING -> GWindow.Buttons.close
+    | `QUESTION -> GWindow.Buttons.ok_cancel
+    | `ERROR -> GWindow.Buttons.close
+  in
   let d = GWindow.message_dialog
     ~message:s
     ~message_type:mt
-    ~buttons:GWindow.Buttons.close
+    ~buttons
     ~title:"Why3 info or error"
     ~show:true ()
   in
+  let r = ref false in
   let (_ : GtkSignal.id) =
     d#connect#response
-      ~callback:(function `CLOSE | `DELETE_EVENT -> d#destroy ())
+      ~callback:(function x -> r := x = `OK; d#destroy ())
   in
-  ()
+  !r
 
 module Helpers = struct
 
@@ -1283,7 +1290,7 @@ let select_file () =
                   "@[Error while reading file@ '%s':@ %a@]" f
                   Exn_printer.exn_printer e;
 	        let msg = flush_str_formatter () in
-	        info_window `ERROR msg
+	        let (_:bool) = info_window `ERROR msg in ()
       end
   | `DELETE_EVENT | `CANCEL -> ()
   end ;
@@ -1291,7 +1298,7 @@ let select_file () =
 
 
 let not_implemented () =
-  info_window `INFO "This feature is not yet implemented, sorry"
+  let (_:bool) = info_window `INFO "This feature is not yet implemented, sorry" in ()
 
 (*************)
 (* File menu *)
@@ -1482,8 +1489,10 @@ let () =
              ()
          in
          let b = GButton.button ~packing:provers_box#add ~label:n () in
-         let i = GMisc.image ~pixbuf:(!image_prover) ()in
+(* prend de la place pour rien
+         let i = GMisc.image ~pixbuf:(!image_prover) () in
          let () = b#set_image i#coerce in
+*)
          let (_ : GtkSignal.id) =
            b#connect#pressed
              ~callback:(fun () -> prover_on_selected_goals p)
@@ -1788,7 +1797,9 @@ let edit_current_proof () =
     | [] -> ()
     | [r] -> edit_selected_row r
     | _ ->
-	info_window `INFO "Please select exactly one proof to edit"
+	let (_:bool) =
+          info_window `INFO "Please select exactly one proof to edit"
+        in ()
 
 
 let add_item_edit () =
@@ -1820,18 +1831,46 @@ let () =
     b#connect#pressed ~callback:not_implemented
   in ()
 
-(************)
-(* cleaning *)
-(************)
+(*************)
+(* removing  *)
+(*************)
+
+let confirm_remove_row r =
+  let row = filter_model#get_iter r in
+  match filter_model#get ~row ~column:Model.index_column with
+    | Model.Row_goal _g ->
+	let (_:bool) = info_window `ERROR "Cannot remove a goal" in ()
+    | Model.Row_theory _th ->
+	let (_:bool) = info_window `ERROR "Cannot remove a theory" in ()
+    | Model.Row_file _file ->
+	let (_:bool) = info_window `ERROR "Cannot remove a file" in ()
+    | Model.Row_proof_attempt _a ->
+	let (_:bool) = info_window `INFO "Proof attempt removal not implemented" in ()
+    | Model.Row_transformation _tr ->
+	let (_:bool) = info_window `INFO "Transformation removal not implemented" in ()
+(*
+  let b =
+    info_window `QUESTION
+      "Do you really want to remove the current selection?"
+  in
+  if b then remove_selection
+*)
+
+let confirm_remove_selection () =
+  match goals_view#selection#get_selected_rows with
+    | [] -> ()
+    | [r] -> confirm_remove_row r
+    | _ ->
+	let (_:bool) =
+          info_window `INFO "Please select exactly one item to remove"
+        in ()
 
 let () =
   let b = GButton.button ~packing:cleaning_box#add ~label:"Remove" () in
-(*
-  let i = GMisc.image ~pixbuf:(!image_replay) () in
+  let i = GMisc.image ~pixbuf:(!image_remove) () in
   let () = b#set_image i#coerce in
-*)
   let (_ : GtkSignal.id) =
-    b#connect#pressed ~callback:not_implemented
+    b#connect#pressed ~callback:confirm_remove_selection
   in ()