[r2002-10-10 09:11:23 by cvscast] Initial revision

Original author: cvscast
Date: 2002-10-10 09:11:23+00:00

Makefile

+PARSER = parser/location.cmo
+TYPES  = types/recursive.cmo types/sortedList.cmo types/sortedMap.cmo types/boolean.cmo types/intervals.cmo types/atoms.cmo types/strings.cmo types/types.cmo types/patterns.cmo types/syntax.cmo
+
+OBJECTS = $(PARSER) $(TYPES)
+
+all.cma: $(OBJECTS)
+	ocamlc -o all.cma -I +camlp4 gramlib.cma -a $(OBJECTS)
+
+depend:
+	ocamldep -pp 'camlp4o pa_extend.cmo' parser/*.ml* types/*.ml*
+
+
+clean:
+	(cd parser; rm -f *.cmi *.cmo *.cma *~)
+	(cd types; rm -f *.cmi *.cmo *.cma *~)
+	rm -f *.cmi *.cmo *.cma *~
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+
+.ml.cmo:
+	ocamlc -c -pp 'camlp4o pa_extend.cmo' -I +camlp4 $<
+
+.ml.cmx:
+	ocamlopt -c $<
+
+.mli.cmi:
+	ocamlc -c $<
+
+# FORTPATH = /users/formel8/frisch/solaris/fort/fort
+FORTPATH = /home/frisch/fort
+FORTBIN = $(FORTPATH)/fort
+FORTLIB = $(FORTPATH)
+
+test: all.cma
+	$(FORTBIN) -I $(FORTLIB) all.cma test_fort.ml
+
+atoms.cmo: sortedList.cmi atoms.cmi 
+atoms.cmx: sortedList.cmx atoms.cmi 
+boolean.cmo: recursive.cmi sortedList.cmi boolean.cmi 
+boolean.cmx: recursive.cmx sortedList.cmx boolean.cmi 
+intervals.cmo: intervals.cmi 
+intervals.cmx: intervals.cmi 
+patterns.cmo: sortedList.cmi sortedMap.cmi types.cmi patterns.cmi 
+patterns.cmx: sortedList.cmx sortedMap.cmx types.cmx patterns.cmi 
+recursive.cmo: recursive.cmi 
+recursive.cmx: recursive.cmi 
+sortedList.cmo: sortedList.cmi 
+sortedList.cmx: sortedList.cmi 
+sortedMap.cmo: sortedMap.cmi 
+sortedMap.cmx: sortedMap.cmi 
+location.cmo: location.cmi
+strings.cmo: boolean.cmi recursive.cmi sortedMap.cmi strings.cmi 
+strings.cmx: boolean.cmx recursive.cmx sortedMap.cmx strings.cmi 
+syntax.cmo: location.cmi patterns.cmi sortedList.cmi types.cmi syntax.cmi 
+syntax.cmx: location.cmi patterns.cmx sortedList.cmx types.cmx syntax.cmi 
+test_fort.cmo: strings.cmi types.cmi 
+test_fort.cmx: strings.cmx types.cmx 
+test_types.cmo: strings.cmi types.cmi 
+test_types.cmx: strings.cmx types.cmx 
+types.cmo: atoms.cmi boolean.cmi intervals.cmi recursive.cmi sortedList.cmi \
+    strings.cmi types.cmi 
+types.cmx: atoms.cmx boolean.cmx intervals.cmx recursive.cmx sortedList.cmx \
+    strings.cmx types.cmi 
+patterns.cmi: sortedList.cmi types.cmi 
+syntax.cmi: patterns.cmi types.cmi 
+types.cmi: atoms.cmi boolean.cmi intervals.cmi strings.cmi 

parser/ast.ml

+type expr = expr_descr located
+and  expr_descr = A | B of expr

parser/location.ml

+type loc = int * int
+exception Location of loc * exn
+
+let noloc = (-1,-1)

parser/location.mli

+type loc = int * int
+exception Location of loc * exn
+
+val noloc:loc

runtime/value.mli

+type t
+
+type descr =
+  | Pair of t * t
+  | Record of (Types.label * t) list
+  | Atom of Types.atom
+  | Integer of int
+  | String of string
+  | Fun of unit (* TODO ... *)
+
+val descr: t -> descr
+

tests/test_fort.ml

+open Types;;
+open Fort;;
+
+let recurs f =
+  let t = make () in
+  define t (f t);
+  internalize t
+
+let recurs' f = 
+  let t = make () in
+  define t (f t);
+  t
+
+let cons d =
+  let t = make () in
+  define t d;
+  internalize t
+
+let cons' d =
+  let t = make () in
+  define t d;
+  t
+
+let list t = recurs (fun s -> cup (times t s) (atom 0));;
+let square i j k l = times (cons (interval i j)) (cons (interval k l))
+let int_list i j = descr (list (cons (interval i j)))
+let int i = interval i i
+
+let (---) = diff;;
+let (=?) a b = expect_equal a b;;
+
+exception NoException
+let exn a x e = 
+  try ignore (a x); raise NoException
+  with 
+    | NoException -> fail "No exception"
+    | e' -> 
+	if e' <> e then fail 
+	  (Printf.sprintf "Wrong exception: '%s' instead of '%s'" 
+	     (Printexc.to_string e')
+	     (Printexc.to_string e)
+	  )
+
+let (??) a = expect_true a;;
+
+expect_pass "Unique representation"
+(fun () ->
+   let t1 = recurs (fun t -> times t t) in
+   let t2 = recurs (fun t -> times t1 t) in
+   let t3 = recurs (fun t -> arrow t t) in
+   let t4 = recurs (fun t -> times t (cons' (times t t))) in
+   let t5 = recurs (fun t -> cup (times t t) (times t t)) in
+   id t1 =? id t2;
+   id t1 =? id t4;
+   id t1 =? id t5;
+   ?? (id t3 <> id t2);
+);;
+
+expect_pass "Interval"
+(fun () ->
+   let t = int_list 1 2 --- int_list 1 1 in
+   Sample.get t =? Sample.Pair (Sample.Int 2, Sample.Atom 0);
+   Sample.get (interval 10 20) =? Sample.Int 10;
+);;
+
+expect_pass "Record"
+(fun () ->
+   let r l o i j = record l o (cons (interval i j)) in
+   Sample.get (r 1 false 100 200) =? Sample.Record [(1, Sample.Int 100 )];
+   Sample.get (r 1 true 100 200) =? Sample.Record [];
+   Sample.get (r 1 false 100 200 --- r 1 false 100 150) 
+       =? Sample.Record [(1, Sample.Int 151 )];
+   exn Sample.get (r 1 false 100 200 --- r 1 false 100 250) Not_found;
+);;
+
+
+expect_pass "Regular string expressions" 
+(fun () ->
+   let t = string (Strings.Star (Strings.Char 'a')) ---
+	   string Strings.Eps ---
+	   string (Strings.Char 'a')
+   in
+   is_empty t =? false;
+   Sample.get t =? Sample.String "aa";
+);;

tests/test_types.ml

+#load "all.cma";;
+open Types;;
+
+let recurs f =
+  let t = make () in
+  define t (f t);
+  internalize t
+
+let cons d =
+  let t = make () in
+  define t d;
+  internalize t
+  
+
+let list t = recurs (fun s -> cup (times t s) (atom 0));;
+let square i j k l = times (cons (interval i j)) (cons (interval k l))
+let int_list i j = descr (list (cons (interval i j)))
+
+let t1 = recurs (fun t -> times t t);;
+let t2 = recurs (fun t -> cup (times t t) (interval 1 2));;
+let t3 = recurs (fun t -> record 1 false t2);;
+let t4 = recurs (fun t -> arrow t t);;
+let t5 = recurs (fun t -> times t3 t4);;
+let t6 = cons 
+	   (
+	     diff 
+	      (square 1 2 1 2)
+	      (cup (square 1 2 1 1) (square 1 1 1 2))
+	   );;
+
+let t7 = cons (diff (int_list 1 2) (int_list 1 1));;
+
+Sample.get (descr t7);;
+
+(*
+
+open Syntax
+
+let v = new_var ();;
+let t = cons (Or (cons (Variable v), cons (Capture "x")));;
+global v t;;
+
+
+*)
+let t8 = cons (diff (diff 
+		 (string (`Star (`Char (65,65)))) 
+		 (string `Eps)
+		    )
+	       (string (`Char (65,65)))
+	      );;
+is_empty (descr t8);;
+Sample.get (descr t8);;
+
+
+let sample typ = 
+  let s = Syntax.parse typ in
+  let t = Syntax.make_type s in
+  Types.Sample.get (Types.descr t);;
+
+(* To fix: 
+let `Type t = Syntax.make (Syntax.parse "/ 'a'+ 'b'? 'c'+ /");;
+let `Type t = Syntax.make (Syntax.parse "/ 'a'+ 'b' /");;
+let `Type t = Syntax.make (Syntax.parse "/ 'a'+ 'b'? 'c'+ | 'd'+ /");;
+Sample.get t;;
+*)
+
+sample "'a where 'a = (`X,'a) | (`X,`Y)";;
+

types/IDEAS

+- Define a 'widening functions'  (types -> types) such two
+  equivalent types become physically equal

types/atoms.ml

+type 'a t = Finite of 'a list | Cofinite of 'a list
+
+let empty = Finite []
+let full = Cofinite []
+
+let atom x = Finite [x]
+
+let cup s t =
+  match (s,t) with
+    | (Finite s, Finite t) -> Finite (SortedList.cup s t)
+    | (Finite s, Cofinite t) -> Cofinite (SortedList.diff t s)
+    | (Cofinite s, Finite t) -> Cofinite (SortedList.diff s t)
+    | (Cofinite s, Cofinite t) -> Cofinite (SortedList.cap s t)
+
+let cap s t =
+  match (s,t) with
+    | (Finite s, Finite t) -> Finite (SortedList.cap s t)
+    | (Finite s, Cofinite t) -> Finite (SortedList.diff s t)
+    | (Cofinite s, Finite t) -> Finite (SortedList.diff t s)
+    | (Cofinite s, Cofinite t) -> Cofinite (SortedList.cup s t)
+
+let diff s t =
+  match (s,t) with
+    | (Finite s, Cofinite t) -> Finite (SortedList.cap s t)
+    | (Finite s, Finite t) -> Finite (SortedList.diff s t)
+    | (Cofinite s, Cofinite t) -> Finite (SortedList.diff t s)
+    | (Cofinite s, Finite t) -> Cofinite (SortedList.cup s t)
+	
+let contains x = function
+  | Finite s -> SortedList.mem s x
+  | Cofinite s -> not (SortedList.mem s x)
+
+let is_empty = function
+  | Finite [] -> true
+  | _ -> false
+      
+let sample except = function
+  | Finite (x :: _) -> x
+  | Cofinite l -> except l
+  | Finite [] -> raise Not_found
+
+
+let print any f = function
+  | Finite l -> List.map (fun x ppf -> f ppf x) l
+  | Cofinite [] ->
+      [ fun ppf -> Format.fprintf ppf "%s" any ]
+  | Cofinite [h] ->
+      [ fun ppf -> Format.fprintf ppf "@[%s - %a@]" any f h ]
+  | Cofinite (h::t) -> 
+      [ fun ppf -> 
+	  Format.fprintf ppf "@[%s - (" any;
+	  f ppf h;
+	  List.iter (fun x -> Format.fprintf ppf " |@ %a" f x) t;
+	  Format.fprintf ppf ")@]" ]
+
+      

types/atoms.mli

+type 'a t (* = Finite of 'a list | Cofinite of 'a list *)
+
+val empty : 'a t
+val full : 'a t
+
+val cup : 'a t -> 'a t -> 'a t
+val cap : 'a t -> 'a t -> 'a t
+val diff : 'a t -> 'a t -> 'a t
+val atom : 'a -> 'a t
+
+val contains : 'a -> 'a t -> bool
+val is_empty : 'a t -> bool
+val sample : ('a list -> 'a) -> 'a t -> 'a
+
+val print : string -> (Format.formatter -> 'a -> unit) -> 'a t -> 
+  (Format.formatter -> unit) list

types/boolean.ml

+type 'a t = ('a list * 'a list) list
+
+let empty = [ ]
+
+let full  = [ ([],[]) ]
+
+let atom x = [ ([x],[]) ]
+
+let may_remove (p1,n1) (p2,n2) =
+  (SortedList.subset p2 p1) && (SortedList.subset n2 n1)
+
+let cup t s = 
+  if t == s then t
+  else if (t == full) || (s == full) then full
+  else 
+    let s=
+      List.filter (fun (p,n) -> not (List.exists (may_remove (p,n)) t)) s in
+    let t=
+      List.filter (fun (p,n) -> not (List.exists (may_remove (p,n)) s)) t in 
+    SortedList.cup s t
+
+let rec fold2_aux f a x = function
+  | [] -> x
+  | h :: t -> fold2_aux f a (f x a h) t
+
+let rec fold2 f x l1 l2 =
+  match l1 with
+    | [] -> x
+    | h :: t -> fold2 f (fold2_aux f h x l2) t l2
+
+let cap s t =
+  if s == t then s
+  else if s == full then t
+  else if t == full then s
+  else if (s == empty) || (t == empty) then empty
+  else
+    let (lines1,common,lines2) = SortedList.split s t in
+    let lines =
+      fold2 
+        (fun lines (p1,n1) (p2,n2) ->
+           if (SortedList.disjoint p1 n2) && (SortedList.disjoint p2 n1) 
+           then (SortedList.cup p1 p2, SortedList.cup n1 n2) :: lines
+           else lines)
+        []
+        lines1
+	lines2
+    in
+    SortedList.cup common (SortedList.from_list lines)
+
+let diff c1 c2 =
+  if c2 == full then empty
+  else if (c1 == empty) || (c2 == empty) then c1
+  else
+    let c1 = SortedList.diff c1 c2 in
+    let line (p,n) =
+      let acc = List.fold_left (fun acc a -> ([], [a]) :: acc) [] p in
+      let acc = List.fold_left (fun acc a -> ([a], []) :: acc) acc n in
+      SortedList.from_list acc
+    in
+    List.fold_left (fun c1 l -> cap c1 (line l)) c1 c2
+
+
+let rec map f t =
+  let lines =
+    List.fold_left
+      (fun lines (p,n) ->
+	 let p = SortedList.map f p and n = SortedList.map f n in
+	 if (SortedList.disjoint p n) then (p,n) :: lines else lines)
+      []
+      t
+  in
+  SortedList.from_list lines
+
+
+  
+let equal_list e l1 l2 =
+  if List.length l1 <> List.length l2 then raise Recursive.NotEqual;
+  List.iter2 e l1 l2
+
+let equal_line e (p1,n1) (p2,n2) =
+  equal_list e p1 p2;
+  equal_list e n1 n2
+
+let equal e a b =
+  equal_list (equal_line e) a b
+
+
+let print any f =
+  List.map 
+    (function 
+	 (p1::p,n) -> 
+	   (fun ppf ->
+	      Format.fprintf ppf "@[%a" f p1;
+	      List.iter (fun x -> Format.fprintf ppf " &@ %a" f x) p;
+	      List.iter (fun x -> Format.fprintf ppf " -@ %a" f x) n;
+	      Format.fprintf ppf "@]";
+	   )
+       | ([],[]) -> 
+	   (fun ppf -> Format.fprintf ppf "%s" any)
+       | ([],[n]) ->
+	   (fun ppf -> Format.fprintf ppf "@[%s - %a@]" any f n)
+       | ([],n1::n) ->
+	   (fun ppf -> 
+              Format.fprintf ppf "@[%s" any;
+	      List.iter (fun x -> Format.fprintf ppf " -@ %a" f x) n;
+	      Format.fprintf ppf "@]";
+	   )
+    )
+
+let check b =
+  SortedList.check b;
+  List.iter 
+    (fun (p,n) -> 
+       SortedList.check p; 
+       SortedList.check n; 
+       assert (SortedList.disjoint p n)
+    )
+    b
+

types/boolean.mli

+(* Implementation of boolean combination in disjunctive normal form (dnf).
+   A dnf is a disjunction of lines, each line consisting of a 
+   conjunction of atoms and negations of atoms.
+
+   A line is coded as a pair (p,n) where p collects atoms and n
+   the negated atoms. p and n are disjoint and sorted lists without duplicates
+   (w.r.t Pervasives.compare).
+
+   A dnf is coded as a sorted list of lines without duplicated
+   (w.r.t Pervasives.compare).
+*)
+
+   
+
+type 'a t = ('a SortedList.t * 'a SortedList.t) SortedList.t
+
+val empty : 'a t
+val full  : 'a t
+val cup   : 'a t -> 'a t -> 'a t
+val cap   : 'a t -> 'a t -> 'a t
+val diff  : 'a t -> 'a t -> 'a t
+val atom  : 'a -> 'a t
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+
+
+val equal: ('a -> 'b -> unit) -> 'a t -> 'b t -> unit
+
+val print: string -> (Format.formatter -> 'a -> unit) -> 'a t ->
+  (Format.formatter -> unit) list
+
+
+val check: 'a t -> unit

types/intervals.ml

+type t = (int*int) list
+
+let empty = []
+let full = [min_int,max_int]
+let atom (a,b) =
+  if a<=b then [a,b] else empty
+
+let rec add l ((a,b) as i) = match l with
+  | [] -> 
+      [i]
+  | ((a1,_) :: _) as l when (a1<>min_int) && (b < (pred a1)) -> 
+      i::l
+  | ((a1,b1) as i' :: l') when (b1<>max_int) && (a > (succ b1)) -> 
+      i'::(add l' i)
+  | (a1,b1) :: l' -> 
+      add l' (min a a1, max b b1)
+
+let rec neg start l = match l with
+  | [] -> [start,max_int]
+  | (a,b) :: l' when a<>min_int -> 
+      if b = max_int then [start,pred a] else
+	(start, pred a) :: (neg (succ b) l')
+  | (_,b) :: l' ->
+      if b = max_int then [] else
+	(neg (succ b) l')
+
+let neg l = neg min_int l
+
+let cup i1 i2 =
+  List.fold_left add i1 i2
+
+let cap i1 i2 =
+  neg (cup (neg i1) (neg i2))
+
+let diff i1 i2 =
+  neg (cup (neg i1) i2)
+
+let is_empty i =
+  i = []  (* representation unique ! *)
+
+
+let contains n =
+  List.exists (fun (a,b) -> (n>=a) && (n<=b))
+
+let sample = function
+  | (i,j) :: _ -> i
+  | _ -> raise Not_found
+  
+
+let print =
+  List.map 
+    (fun (a,b) ->
+       if a = b 
+       then fun ppf -> Format.fprintf ppf "%i" a
+       else fun ppf -> Format.fprintf ppf "%i--%i" a b
+    )

types/intervals.mli

+(* Combinaisons booléennes d'intervalles d'entiers;
+
+   elle sont representées comme des réunions disjointes d'intervalles,
+   sous la forme de listes de couples (ai,bi) tq  ai<=bi,  (bi)+1<a(i+1)
+
+   Note: il y a representation unique
+*)
+
+type t = (int*int) list
+
+val empty : t
+val full  : t
+val cup   : t -> t -> t
+val cap   : t -> t -> t
+val diff  : t -> t -> t
+val atom  : int*int -> t
+
+
+val is_empty : t -> bool
+val contains : int -> t -> bool
+val sample : t -> int
+
+
+val print : t -> (Format.formatter -> unit) list

types/patterns.mli

+type capture = string
+type fv = capture SortedList.t
+
+exception IllFormedCup of fv * fv
+exception IllFormedCap of fv * fv
+
+
+(* Pattern algebra *)
+
+type descr
+type node
+
+val make: fv -> node
+val define: node -> descr -> unit
+
+val constr : Types.node -> descr
+val cup    : descr -> descr -> descr
+val cap    : descr -> descr -> descr
+
+val times  : node -> node -> descr 
+val record : Types.label -> node -> descr
+
+val capture : capture -> descr
+val constant: capture -> Types.const -> descr
+
+val id: node -> int
+val descr: node -> descr
+val fv : node -> fv
+
+(* Pattern matching: static semantics *)