X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk%2Flablgtk_20000829-0.1.0%2Fdoc%2Flablgtk.mgp;fp=helm%2FDEVEL%2Flablgtk%2Flablgtk_20000829-0.1.0%2Fdoc%2Flablgtk.mgp;h=3eac793416f13dabde49350d7fa72f80ef4a6b3e;hb=2ee84a2a641938988703e329aef9fc3c5eb5aacf;hp=0000000000000000000000000000000000000000;hpb=34d83812af9b7064cc8f735c2a78169881140010;p=helm.git

diff --git a/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/doc/lablgtk.mgp b/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/doc/lablgtk.mgp
new file mode 100644
index 000000000..3eac79341
--- /dev/null
+++ b/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/doc/lablgtk.mgp
@@ -0,0 +1,558 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%deffont "code" xfont "itc avant garde gothic-demi-r", tfont "verdana.ttf"
+%deffont "code-bold" xfont "terminal-bold-r", tfont "verdanab.ttf"
+%deffont "sans" xfont "helvetica-medium-r", tfont "comic.ttf"
+%deffont "sans-bold" xfont "helvetica-bold-r", tfont "comicbd.ttf"
+%deffont "sansit" xfont "helvetica-medium-i", tfont "marlett.ttf"
+%deffont "title" xfont "times-medium-r", tfont "times.ttf"
+%deffont "title-bold" xfont "times-bold-r", tfont "timesbd.ttf"
+%default 1 right, size 2, fore "white", bgrad
+%default 1 vfont "goth", font "sans-bold", vgap 100
+%default 2 leftfill, size 8, vgap 60, prefix " ", font "sans"
+%default 3 size 4, bar "beige", vgap 10
+%default 4 size 5, fore "white", vgap 20, prefix " "
+%tab 1	size 5, vgap 40, prefix "  ", icon box "green" 50
+%tab 2	size 5, vgap 40, prefix "      ", icon arc "yellow" 50
+%tab 3	size 5, vgap 40, prefix "            ", icon arc "white" 40
+%tab com1	size 4, prefix "     "
+%tab com2	size 4, prefix "          "
+%tab com3	size 4, prefix "             "
+%tab txt	font "sans", size 5, fore "white", prefix " "
+%tab vspace	size 2
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+%nodefault
+%size 9, font "title-bold"
+%fore "beige", back "navyblue", vgap 20
+%center
+
+
+A Type System in Action:
+
+the LablGTK Interface
+
+
+%size 7, font "title"
+Jacques Garrigue
+Kyoto University
+%size 6, font "code"
+garrigue@kurims.kyoto-u.ac.jp
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+2
+Synopsis
+
+	Objective Label introduction
+%size 2
+
+	Why GTK+?
+	GTK+/LablGTK structure
+%size 2
+
+	Low Level
+		Type encoding with variants
+		Labeled parameters
+%size 2
+
+	High Level
+		Object-orientation
+		Optional arguments
+		Polymorphic methods
+%size 2
+
+	Conclusion
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+3
+Objective Label
+
+	Based on Objective Caml
+		ML syntax and type inference
+		Class-based object system
+
+	Several extensions
+		Labeled and optional parameters
+		Polymorphic variants
+		Polymorphic methods
+
+	Tools
+		Type-based browser
+		GUI and 3D graphics
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+4
+Labels and optionals
+
+%font "code", size 4, prefix "    ", fore "yellow"
+let rec map fun:f = function
+    [] -> []
+  | x :: l -> f x :: map fun:f l
+%fore "lightpink"
+val map : fun:('a -> 'b) -> 'a list -> 'b list
+
+%pause, fore "yellow", font "code"
+let f = map [1;2;3]
+%fore "lightpink"
+val f : fun:(int -> 'a) -> 'a list
+%fore "yellow"
+f fun:(fun x -> 2*x)
+%fore "lightpink"
+- : int list = [2; 3; 4]
+
+%pause, fore "yellow", font "code"
+let f x ?incr:y [< 1 >] = x + y
+%fore "lightpink"
+val f : int -> ?incr:int -> int
+%fore "yellow"
+f 1
+%fore "lightpink"
+- : int = 2
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+5
+Polymorphic variants
+
+
+%font "code", size 4, prefix "    ", fore "yellow"
+[`on; `off]
+%fore "lightpink"
+- : [> off on] list = [`on; `off]
+
+%pause, fore "yellow", font "code"
+`number 1;;
+%fore "lightpink"
+- : [> number(int)] = `number 1
+
+%pause, fore "yellow", font "code"
+let f = function `on -> 1 | `off -> 0 | `number n -> n
+%fore "lightpink"
+val f : [< number(int) off on] -> int
+
+%pause, fore "yellow", font "code"
+type t = [on off number(int)]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+6
+Polymorphic methods
+
+Not allowed in Objective Caml
+%size 2
+
+%font "code", size 4, prefix "    ", fore "yellow"
+class c = object method m x = x end
+%fore "red"
+Some type variables are unbound in this type:
+  class c : object method m : 'a -> 'a end
+The method m has type 'a -> 'a where 'a is unbound
+
+%pause, font "sans", size 5, prefix " ", fore "white"
+Need explicit annotation in O'Labl
+%size 2
+
+%font "code", size 4, prefix "    ", fore "yellow"
+class c = object
+    method m : 'a. 'a -> 'a = fun x -> x
+end
+%fore "lightpink"
+class c : object method m : 'a -> 'a end
+%fore "yellow"
+let o = new c
+%fore "lightpink"
+val o : c = <obj>
+%fore "yellow"
+o#m 1, o#m true
+%fore "lightpink"
+- : int * bool = 1, true
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+7
+Why GTK+ ?
+
+Why use the GIMP Tool Kit?
+%size 3
+
+	Widely used in free software
+
+	Easy to interface
+		Written in C (QT uses C++)
+		Memory management
+
+Drawbacks
+%size 3
+
+	Design lacks uniformity
+	Extensive use of dynamic typing
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+8
+GTK+ Structure
+
+Class hierarchy based on GtkObject
+%size 2
+
+	Single inheritance
+&com1 New widgets may redefine methods
+%size 2
+
+	Dynamically checked
+&com1 Casting necessay both up and down
+%size 2
+
+	Developper-side hierarchy
+&com1 Inheritance is not always meaningful to the user
+%size 2
+
+%size 5
+Signal-based callback mechanism
+%size 2
+
+	May use multiple callbacks
+%size 2
+
+	Signals are polymorphic
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+9
+LablGTK structure
+
+Typed at all levels
+
+	Low-level interface
+%size 2
+
+		C stub functions -- typechecked by C
+
+		ML type declarations -- ML abstract types
+
+	High-level interface
+%size 2
+
+		ML class wrappers -- ML concrete types
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+10
+Low Level Interface
+
+Goals
+
+	Strongly typed interface
+&com1 heavy use of advanced typing techniques
+
+	Very little ML code
+&com1 C-stubs and external declarations
+
+	Safe memory management
+&com1 have the library cooperate with the GC
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+11
+Low level encoding (I)
+
+
+How to represent widget subtyping in ML?
+
+	Example: buttons' hierarchy
+%size 2
+
+%font "code", size 5, prefix "      ", fore "yellow"
+GtkObject
+    GtkWidget
+        GtkContainer
+            GtkButton
+                GtkToggleButton
+                    GtkRadioButton
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+12
+Variants as set constraints
+
+
+Variants can be seen as sets of possible values:
+
+	[tag1 ... tagn] = {tag1,...,tagn}
+
+
+Polymorphic variants introduce constraints
+
+	α[> tag1 ... tagn] ⇔ α ⊃ {tag1,...,tagn}
+	α[< tag1 ... tagn] ⇔ α ⊂ {tag1,...,tagn}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+13
+Encoding hierarchies
+
+Define an abstract type
+&vspace
+%font "code", fore "yellow", size 5
+      type 'a obj
+
+&txt Use tags to represent properties
+&vspace
+%font "code", fore "yellow", size 5
+      type t = [class1 ... classn] obj
+
+&txt Functions check properties
+&vspace
+%font "code", fore "yellow", size 5
+      val f : [> class1 ... classn] obj -> ...
+&txt
+	Subsumes Haskell type classes
+&vspace
+	Allows multiple inheritance
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+14
+Low level encoding (II)
+
+Example: buttons' hierarchy
+%size 2
+
+%font "code", size 4, prefix "    ", fore "yellow"
+type 'a obj
+type widget = [widget] obj
+type container = [widget container] obj
+type button = [widget container button] obj
+type toggle_button = [widget ... togglebutton] obj
+type radio_button = [widget ... radiobutton] obj
+type state_type = [ NORMAL
+     ACTIVE PRELIGHT SELECTED INSENSITIVE ] 
+val set_state : [> widget] obj -> state_type -> unit
+val children : [> container] obj -> [widget] obj list
+val clicked : [> button] obj -> unit
+val set_group : [> radiobutton] obj -> group -> unit
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+15
+Alternate encoding
+
+Use only standard ML features
+%size 2
+
+%font "code", size 4, prefix "  ", fore "yellow", vgap 50
+type 'a obj
+type 'a widget
+...
+type 'a radio
+type state_type = NORMAL | ACTIVE | ... | INSENSITIVE
+val set_state : 'a widget obj -> state_type -> unit
+val children :
+    'a container widget obj -> unit widget obj list
+val clicked : 'a button container widget obj -> unit
+
+&txt Weaknesses
+	No multiple inheritance
+	Not very intuitive for the user
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+16
+Low level encoding (III)
+
+Use of labeled parameters
+%size 2
+
+%font "code", size 4, prefix "  ", fore "yellow", vgap 50
+val adjustment_new :
+    value:float -> lower:float -> upper:float ->
+    step_incr:float -> page_incr:float ->
+    page_size:float -> adjustment obj
+
+&txt Signals
+%size 2
+
+%font "code", size 4, prefix "  ", fore "yellow", vgap 50
+type ('a,'b) signal =
+    { name: string; marshaller: 'b -> GtkArgv.t -> unit }
+val connect : 'a obj -> sig:('a,'b) signal ->
+               callback:'b -> ?after:bool -> id
+val button_clicked : ([> button], unit -> unit) signal
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+17
+High-Level Interface
+
+Problems with GTK+
+%size 2
+
+	Name space is scattered
+&com1 One has to know in which superclass a function is defined
+	Developper oriented design
+&com1 There is no clear distinction between public and private definitions
+
+&txt LablGTK design
+%size 2
+
+	OCaml classes to reunify name space
+	Omit developper-oriented methods
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+18
+High-level classes
+
+%font "code", size 4, prefix "  ", fore "yellow"
+class button :
+%fore "lightgreen"
+  ?label:string ->
+%fore "lightpink"
+  ?border_width:int ->
+  ?width:int ->
+  ?height:int ->
+%fore "lightgray"
+  ?packing:(GButton.button -> unit) ->
+  ?show:bool ->
+%fore "yellow"
+  object
+%fore "lightgray"
+    method destroy : unit -> unit
+    method as_widget : Gtk.widget obj
+    method misc : GObj.widget_misc
+%fore "lightpink"
+    method add : #is_widget -> unit
+    method set_border_width : int -> unit
+%fore "lightgreen"
+    method clicked : unit -> unit
+    method connect : GButton.button_signals
+    method grab_default : unit -> unit
+%fore "yellow"
+  end
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+19
+High-level features
+
+	Objective Caml classes
+&com1 allow collecting methods from different modules
+
+	Use optionals in class constructors
+&com1 makes widget creation much easier
+
+	Polymorphic methods
+&com1 needed for container widgets
+%size 2
+
+%font "code", size 4, fore "yellow", vgap 50
+        method add : 'a. (#is_widget as 'a) -> unit
+
+%fore "white", font "sans"
+	Polymorphic variants
+&com1 for C-style enumeration types, avoid name-space dependancies
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+20
+Polymorphic methods (I)
+
+	Instance of first-class polymorphism
+%size 2
+
+		first-class polytypes cannot be inferred
+		they are propagated by the definition flow
+
+	Technically
+%size 2
+
+		use polymorphism to track available information
+		type system excludes derivations based on "guessed" information
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+21
+First class polymorphism
+
+%prefix "            "
+%image "formula.eps" 512x384
+%size 2
+
+%prefix " ", size 5, fore "lightblue"
+  (σ1 : σ : σ2) ⇔ σ1 = θ(ρ1(σ)) ∧ σ2 = θ(ρ2(σ))
+%fore "white"
+where θ instantiates free variables, and ρ1,ρ2 rename free labels of σ.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+22
+Polymorphic methods (II)
+
+Definitions
+%size 2
+
+%font "code", size 4, prefix "    ", fore "yellow", vgap 50
+type is_widget = < as_widget : widget obj >
+type #is_widget = < as_widget : widget obj; .. >
+type container =
+    < ... ; add : 'a. (#as_widget as 'a) -> unit; ... >
+
+%pause
+&txt Propagation
+%size 2
+
+%font "code", size 4, prefix "    ", fore "lightgreen", vgap 50
+fun (cont : container) -> cont#add widget
+
+%pause
+let button = new button in button#add widget
+
+%pause, fore "red"
+fun cont -> cont#add widget
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+23
+Programming example
+
+Hello World
+%size 2
+
+%font "code", size 4, prefix "    ", fore "yellow"
+open GMain
+
+let window =
+    new GWindow.window border_width: 10
+
+let button =
+    new GButton.button
+        label: "Hello World" packing: window#add
+
+let _ =
+  window#connect#destroy callback: Main.quit;
+  button#connect#clicked callback: window#destroy;
+  window#show ();
+  Main.main ()
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%page
+24
+Conclusion
+
+	Results
+%size 2
+
+		Could build a strongly typed interface
+
+		It is easier to use than the C API
+
+		Makes effective use of extensions to the type system
+
+	Comments
+%size 2
+
+		Still difficulties with the Caml object system 
+&com2 class recursion, method type refinement, etc...