]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/doc/lablgtk.mgp
This commit was manufactured by cvs2svn to create branch 'init'.
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / doc / lablgtk.mgp
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
deleted file mode 100644 (file)
index 3eac793..0000000
+++ /dev/null
@@ -1,558 +0,0 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%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
-
-       \e$B&A\e(B[> tag1 ... tagn] \e$B"N\e(B \e$B&A\e(B \e$B"?\e(B {tag1,...,tagn}
-       \e$B&A\e(B[< tag1 ... tagn] \e$B"N\e(B \e$B&A\e(B \e$B">\e(B {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"
-  (\e$B&R\e(B1 : \e$B&R\e(B : \e$B&R\e(B2) \e$B"N\e(B \e$B&R\e(B1 = \e$B&H\e(B(\e$B&Q\e(B1(\e$B&R\e(B)) \e$B"J\e(B \e$B&R\e(B2 = \e$B&H\e(B(\e$B&Q\e(B2(\e$B&R\e(B))
-%fore "white"
-where \e$B&H\e(B instantiates free variables, and \e$B&Q\e(B1,\e$B&Q\e(B2 rename free labels of \e$B&R\e(B.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%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...