diff --git a/examples/programs/course.mlw b/examples/programs/course.mlw new file mode 100644 index 0000000000000000000000000000000000000000..622edbede3013468536a5ad37169816bbe4fe3ff --- /dev/null +++ b/examples/programs/course.mlw @@ -0,0 +1,199 @@ + +{ + + (* 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 +} + +*) + + + + + + + + + + + diff --git a/share/images/deletefile32.png b/share/images/deletefile32.png new file mode 100644 index 0000000000000000000000000000000000000000..ef66efb30ad146feb5149f257e41489832d61e34 Binary files /dev/null and b/share/images/deletefile32.png differ diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 3b4d4ddf8b401b818a7a57a51a4c4690ead0648a..7fc904c3f6598fc15836775c496eaa94894a8975 100644 --- a/src/ide/gconfig.ml +++ b/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 () = diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index f5e7346960e68d8b734ef2accd3bf4a79e08d1bd..6956ce3c77cc4557918ca74fbc9c51ad8d92a9ef 100644 --- a/src/ide/gconfig.mli +++ b/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 diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 997087493d158503f12fb7e66773ae797ac3ff10..51af55e3db6850629b4677cc1d264e7ac9c77281 100644 --- a/src/ide/gmain.ml +++ b/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 ()