Changeset 7195

Timestamp:

02/23/10 06:47:00 (7 months ago)

Author:

dbaelde

Message:

Add a notion of clock sub-occurrence and the corresponding occurs-check
in clock unification. This allows to detect bad situations like
add([s,cross(f,s)]) with "a dependency of a clock on itself".
By the way, I commit a preliminary support for clocks in cross().
Error messages are still shitty and super spacey ;)

Location:

trunk/liquidsoap/src

Files:

• clock.ml (modified) (1 diff)
• clock.mli (modified) (2 diffs)
• lang/lang.ml (modified) (1 diff)
• operators/cross.ml (modified) (4 diffs)
• source.ml (modified) (7 diffs)
• source.mli (modified) (1 diff)

trunk/liquidsoap/src/clock.ml

@@ -63 +63 @@
 
   val mutable outputs = []
-
   method attach s = outputs <- s::outputs
+
+  val mutable sub_clocks : Source.clock_variable list = []
+  method attach_clock c = sub_clocks <- c::sub_clocks
+  method sub_clocks = sub_clocks
 
   method end_tick =

trunk/liquidsoap/src/clock.mli

@@ -25 +25 @@
   method id : string
   method attach : Source.active_source -> unit
+  method attach_clock : Source.clock_variable -> unit
+  method sub_clocks : Source.clock_variable list
   method end_tick : unit
   method start : unit
@@ -37 +39 @@
 
 type clock_variable = Source.clock_variable
-val create_unknown : Source.active_source list -> clock_variable
-val create_known   : clock                     -> clock_variable
-val unify : clock_variable -> clock_variable -> bool
+val to_string      : clock_variable -> string
+val create_unknown : sources:(Source.active_source list) ->
+                     sub_clocks:(clock_variable list) ->
+                     clock_variable
+val create_known : clock -> clock_variable
+val unify : clock_variable -> clock_variable -> unit

trunk/liquidsoap/src/lang/lang.ml

@@ -626 +626 @@
           Printf.printf "ERROR: %s!\n" s ;
           exit 1
+      | Source.Clock_conflict (a,b) ->
+          (* TODO better printing of clock errors: we don't have position
+           *   information, use the source's ID *)
+          Printf.printf
+            "An operator cannot belong to two clocks (%s, %s).\n"
+            a b ;
+          exit 1
+      | Source.Clock_loop (a,b) ->
+          Printf.printf
+            "Cannot unify two dependent clocks: %s, %s.\n"
+            a b ;
+          exit 1
       | e -> print_error "Unknown error" ; raise e
 

trunk/liquidsoap/src/operators/cross.ml

@@ -2 +2 @@
 
   Liquidsoap, a programmable stream generator.
-  Copyright 2003-2009 Savonet team
+  Copyright 2003-2010 Savonet team
 
   This program is free software; you can redistribute it and/or modify
@@ -43 +43 @@
   inherit operator ~name:"cross" kind [s] as super
 
-  method stype = s#stype (* This actually depends on [f]. *)
+  method stype = s#stype (* This should actually depend on [f]. *)
+
+  val my_clock = new Clock.clock "cross_clock"
+
+  method set_clock =
+    let my_clock = Clock.create_known my_clock in
+    (* The source must belong to our clock, since we need occasional
+     * control on its flow (to fold an end of track over a beginning). *)
+    Clock.unify my_clock s#clock ;
+    (* Our external clock should stricly contain the internal my_clock. *)
+    Clock.unify
+      self#clock
+      (Clock.create_unknown ~sources:[] ~sub_clocks:[my_clock])
 
   (* The played source will be [s] at first, but can become a combination of
@@ -52 +64 @@
   method private source_get ab =
     source#get ab ;
+    (* TODO it might be abusive to end the tick all the time,
+     *   maybe we didn't consume till the end of the current frame *)
+    my_clock#end_tick ;
+    (* TODO for now, we need to handle this (possibly passive) source
+     *   ourselves since the clock only takes care of the active guys *)
     source#after_output
 
-  val mutable activation = []
-
-  method private wake_up activator =
-    activation <- (self:>source)::activator ;
-    s#get_ready ~dynamic:true activation ;
+  method private wake_up _ =
+    s#get_ready ~dynamic:true [(self:>source)] ;
     source <- s ;
-    source#get_ready activation ;
-    Lang.iter_sources (fun s -> s#get_ready ~dynamic:true activation) f
+    source#get_ready [(self:>source)] ;
+    (* TODO when using f we'll have to force our clock on it *)
+    Lang.iter_sources (fun s -> s#get_ready ~dynamic:true [(self:>source)]) f
 
   method private sleep =
@@ -175 +190 @@
       in
         source#leave (self:>source) ;
-        s#get_ready activation ;
+        s#get_ready [(self:>source)] ;
         source <- s ;
         status <- `After inhibit

trunk/liquidsoap/src/source.ml

@@ -78 +78 @@
   * are forced to wallclock. *)
 
-class type ['a] proto_clock =
+class type ['a,'b] proto_clock =
 object
+
   method id : string
+
+  (** Attach an active source.
+    * For now this only works before #start, but in a near future
+    * dynamic attaching/detaching should be supported. *)
   method attach : 'a -> unit
+
+  (** Attach a sub_clock, get all subclocks, see below. *)
+  method attach_clock : 'b -> unit
+  method sub_clocks : 'b list
+
   method start : unit
   method stop : unit
+
 end
 
 (** {1 Clock variables}
-  * Used to infer what clock a source belongs to. *)
+  * Used to infer what clock a source belongs to.
+  * Each variable comes with
+  *   - a list of active sources belonging to the clock, unused during
+  *     inference/unification, but animated by the clock when running
+  *   - a list of sub-clocks, used during unification's occurs-check
+  *     to avoid cycles which would result in unsound behavior
+  *     e.g. add([s,cross(f,s)]).
+  * Clock constants are objects of type proto_clock, but need to also
+  * maintain the information attached to variables.
+  *
+  * The unification algorithm can be described as follows, ignoring
+  * the active source maintenance.
+  * X[Y1,Y2,..,Yn] denotes a variable or constant clock with the set Gamma
+  *    of subclocks,
+  *    from a first-order unification perspective it should be thought of
+  *    as a term X(Y1,Y2,..,Yn,...) where the second ... denotes a
+  *    row variable: we don't know if there are more parameters there
+  *    (more subclocks)
+  * We write X[Gamma] with Gamma list of clocks, and X[..Y..] when
+  * Y belongs to the subclocks of X, or the subclocks of the subclocks,
+  * etc.
+  * Unification rules are:
+  *   X[..Y..] = Y[..]    ---> ERROR (occurs-check)
+  *   c1[...]  = c2[...]  ---> ERROR (rigid-rigid)
+  *   X[Gamma] = Y[Delta] ---> X,Y:=Z[Gamma,Delta]
+  *      Here Gamma,Delta denotes an union. It is possible that two
+  *      distinct variables might become unified, in which case we'll
+  *      end up with two occurrences of the same subclock.
+  *)
 
 type 'a var =
   | Link of 'a link_t ref
-  | Known of 'a proto_clock
+  | Known of ('a,'a var) proto_clock
 and 'a link_t =
-  | Unknown of 'a list
+  | Unknown of 'a list * 'a var list
   | Same_as of 'a var
 
@@ -108 +147 @@
   Known c
 
-let create_unknown l =
-  let clock = Link (ref (Unknown l)) in
+let create_unknown ~sources ~sub_clocks =
+  let clock = Link (ref (Unknown (sources,sub_clocks))) in
     clocks := clock :: !clocks ;
     clock
@@ -119 +158 @@
 let rec variable_to_string = function
   | Link {contents=Same_as c} -> variable_to_string c
-  | Link ({contents=Unknown l} as r) ->
-      Printf.sprintf "?(%x:%d)" (Obj.magic r) (List.length l)
-  | Known c -> c#id
-
-exception Clock_conflict
+  | Link ({contents=Unknown (sources,clocks)} as r) ->
+      Printf.sprintf "?(%x:%d)[%s]"
+        (Obj.magic r)
+        (List.length sources)
+        (String.concat "," (List.map variable_to_string clocks))
+  | Known c ->
+      Printf.sprintf "%s[%s]"
+        c#id
+        (String.concat "," (List.map variable_to_string c#sub_clocks))
+
+(** Equality modulo dereferencing, does not identify two variables
+  * with the same sources and clocks. *)
+let var_eq a b =
+  let a = deref a in
+  let b = deref b in
+    match a, b with
+      | Link a, Link b -> a==b
+      | Known a, Known b -> a=b
+      | _,_ -> false
+
+exception Clock_conflict of string * string
+exception Clock_loop of string * string
+
+let rec sub_clocks = function
+  | Known c -> c#sub_clocks
+  | Link {contents = Unknown (_,sc)} -> sc
+  | Link {contents = Same_as x} -> sub_clocks x
+
+let occurs_check x y =
+  let rec aux = function
+    | [] -> ()
+    | []::tl -> aux tl
+    | (x'::clocks)::tl ->
+        if var_eq x x' then
+          raise (Clock_loop (variable_to_string x, variable_to_string y)) ;
+        aux (sub_clocks x' :: clocks :: tl)
+  in
+    aux [sub_clocks y]
+
+let occurs_check x y =
+  occurs_check x y ;
+  occurs_check y x
 
 let rec unify a b =
@@ -129 +205 @@
     | Link {contents=Same_as a}, _ -> unify a b
     | _, Link {contents=Same_as b} -> unify a b
-    | Known s, Known s' -> s = s'
-    | Link ({contents=Unknown la} as ra), Link ({contents=Unknown lb} as rb) ->
-        let merge = Link (ref (Unknown (la@lb))) in
+    | Known s, Known s' -> if s <> s' then
+        raise (Clock_conflict (variable_to_string a, variable_to_string b))
+    | Link ({contents=Unknown (sa,ca)} as ra),
+      Link ({contents=Unknown (sb,cb)} as rb) ->
+        (* TODO perhaps optimize ca@cb *)
+        occurs_check a b ;
+        let merge = Link (ref (Unknown (sa@sb,ca@cb))) in
           ra := Same_as merge ;
-          rb := Same_as merge ;
-          true
-    | Known c, Link ({contents=Unknown l} as r)
-    | Link ({contents=Unknown l} as r), Known c ->
-        List.iter c#attach l ;
-        r := Same_as (Known c) ;
-        true
+          rb := Same_as merge
+    | Known c, Link ({contents=Unknown (s,sc)} as r)
+    | Link ({contents=Unknown (s,sc)} as r), Known c ->
+        occurs_check (Known c) (Link r) ;
+        List.iter c#attach s ;
+        List.iter c#attach_clock sc ;
+        r := Same_as (Known c)
 
 let assign_clocks ~default =
@@ -219 +299 @@
    * changed anymore: a source lives in only one time flow. *)
 
-  val clock : active_source var = create_unknown []
+  val clock : active_source var = create_unknown ~sources:[] ~sub_clocks:[]
 
   method clock = clock
 
   method set_clock =
-    List.iter
-      (fun s ->
-         if not (unify self#clock s#clock) then
-           raise Clock_conflict)
-      sources
+    List.iter (fun s -> unify self#clock s#clock) sources
 
   (** Startup/shutdown.
@@ -439 +515 @@
     has_outputs := true ;
     ignore
-      (unify self#clock (create_unknown [(self:>active_source)])) ;
+      (unify
+         self#clock
+         (create_unknown ~sources:[(self:>active_source)] ~sub_clocks:[])) ;
     self#set_sources []
 
@@ -481 +559 @@
   method id : string
   method attach : active_source -> unit
+  method attach_clock : clock_variable -> unit
+  method sub_clocks : clock_variable list
   method start : unit
   method stop : unit

trunk/liquidsoap/src/source.mli

@@ -151 +151 @@
 val has_outputs : unit -> bool
 
+(** {1 Clocks} *)
+
 class type clock =
 object
   method id : string
   method attach : active_source -> unit
+
   method start : unit
   method stop : unit
+
+  method attach_clock : clock_variable -> unit
+  method sub_clocks : clock_variable list
 end
 
-exception Clock_conflict
+exception Clock_conflict of string*string
+exception Clock_loop of string*string
 
 module Clock_variables :
 sig
   val to_string : clock_variable -> string
-  val create_unknown : active_source list -> clock_variable
-  val create_known   : clock              -> clock_variable
-  val unify : clock_variable -> clock_variable -> bool
+  val create_unknown : sources:(active_source list) ->
+                       sub_clocks:(clock_variable list) ->
+                       clock_variable
+  val create_known : clock -> clock_variable
+  val unify : clock_variable -> clock_variable -> unit
   val get_clocks : default:clock -> clock list
 end