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=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=3eac793416f13dabde49350d7fa72f80ef4a6b3e;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;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
deleted file mode 100644
index 3eac79341..000000000
--- a/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/doc/lablgtk.mgp
+++ /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
-
-	α[> 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...