[r2002-10-19 20:52:17 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-19 20:52:18+00:00

Makefile

@@ -7,7 +7,8 @@ TYPES  = types/recursive.cmo types/sortedList.cmo \
          types/intervals.cmo types/chars.cmo types/atoms.cmo \
          types/types.cmo \
          types/patterns.cmo \
-	 types/sequence.cmo
+	 types/sequence.cmo \
+	 types/builtin.cmo
 
 DRIVER = driver/cduce.cmo
 

depend

@@ -2,10 +2,10 @@ parser/ast.cmo: parser/location.cmi types/patterns.cmi types/types.cmi
 parser/ast.cmx: parser/location.cmx types/patterns.cmx types/types.cmx 
 parser/location.cmo: parser/location.cmi 
 parser/location.cmx: parser/location.cmi 
-parser/parser.cmo: parser/ast.cmo types/chars.cmi parser/location.cmi \
-    types/types.cmi parser/parser.cmi 
-parser/parser.cmx: parser/ast.cmx types/chars.cmx parser/location.cmx \
-    types/types.cmx parser/parser.cmi 
+parser/parser.cmo: parser/ast.cmo types/atoms.cmi types/chars.cmi \
+    parser/location.cmi types/sequence.cmi types/types.cmi parser/parser.cmi 
+parser/parser.cmx: parser/ast.cmx types/atoms.cmx types/chars.cmx \
+    parser/location.cmx types/sequence.cmx types/types.cmx parser/parser.cmi 
 parser/parser.cmi: parser/ast.cmo 
 typing/typed.cmo: parser/location.cmi types/patterns.cmi types/types.cmi 
 typing/typed.cmx: parser/location.cmx types/patterns.cmx types/types.cmx 
@@ -20,6 +20,8 @@ types/atoms.cmo: types/sortedList.cmi types/atoms.cmi
 types/atoms.cmx: types/sortedList.cmx types/atoms.cmi 
 types/boolean.cmo: types/recursive.cmi types/sortedList.cmi types/boolean.cmi 
 types/boolean.cmx: types/recursive.cmx types/sortedList.cmx types/boolean.cmi 
+types/builtin.cmo: types/atoms.cmi types/chars.cmi types/types.cmi 
+types/builtin.cmx: types/atoms.cmx types/chars.cmx types/types.cmx 
 types/chars.cmo: types/chars.cmi 
 types/chars.cmx: types/chars.cmi 
 types/intervals.cmo: types/intervals.cmi 
@@ -30,8 +32,8 @@ types/patterns.cmx: types/sortedList.cmx types/sortedMap.cmx types/types.cmx \
     types/patterns.cmi 
 types/recursive.cmo: types/recursive.cmi 
 types/recursive.cmx: types/recursive.cmi 
-types/sequence.cmo: types/types.cmi types/sequence.cmi 
-types/sequence.cmx: types/types.cmx types/sequence.cmi 
+types/sequence.cmo: types/atoms.cmi types/types.cmi types/sequence.cmi 
+types/sequence.cmx: types/atoms.cmx types/types.cmx types/sequence.cmi 
 types/sortedList.cmo: types/sortedList.cmi 
 types/sortedList.cmx: types/sortedList.cmi 
 types/sortedMap.cmo: types/sortedMap.cmi 
@@ -53,8 +55,9 @@ types/patterns.cmi: types/sortedList.cmi types/sortedMap.cmi types/types.cmi
 types/sequence.cmi: types/types.cmi 
 types/sortedMap.cmi: types/sortedList.cmi 
 types/syntax.cmi: types/patterns.cmi types/types.cmi 
-types/types.cmi: types/chars.cmi types/intervals.cmi types/sortedMap.cmi 
-driver/cduce.cmo: parser/ast.cmo parser/location.cmi parser/parser.cmi \
-    typing/typer.cmi types/types.cmi 
-driver/cduce.cmx: parser/ast.cmx parser/location.cmx parser/parser.cmx \
-    typing/typer.cmx types/types.cmx 
+types/types.cmi: types/atoms.cmi types/chars.cmi types/intervals.cmi \
+    types/sortedMap.cmi 
+driver/cduce.cmo: parser/ast.cmo types/builtin.cmo parser/location.cmi \
+    parser/parser.cmi typing/typer.cmi types/types.cmi 
+driver/cduce.cmx: parser/ast.cmx types/builtin.cmx parser/location.cmx \
+    parser/parser.cmx typing/typer.cmx types/types.cmx 

driver/cduce.ml

 open Location
 
+let () =
+  List.iter 
+    (fun (n,t) -> Typer.register_global_types [n, mk noloc (Ast.Internal t)])
+    Builtin.types
+
 let input = Stream.of_channel stdin
 let ppf = Format.std_formatter
 let prog () = 

parser/ast.ml

@@ -15,6 +15,8 @@ and pmodule_item' =
 
 and pexpr = pexpr' located
 and pexpr' = 
+  (* For debugging the typer: an expression with prescribed type *)
+  | DebugTyper of ppat
     
   (* CDuce is a Lambda-calculus ... *)
   | Var of string

parser/parser.ml

@@ -8,8 +8,6 @@ open Ast
   let regexp  = Grammar.Entry.create gram "type/pattern regexp"
   let const   = Grammar.Entry.create gram "scalar constant"
  
-  let atom_nil = Types.mk_atom "nil"
-		   
   let rec multi_prod loc = function
     | [ x ] -> x
     | x :: l -> mk loc (Prod (x, multi_prod loc l))
@@ -20,6 +18,16 @@ open Ast
     | x :: l -> mk loc (Pair (x, tuple loc l))
     | [] -> assert false
 	
+  let char = mk noloc (Internal (Types.char Chars.any))
+  let string = Star (Elem char)
+
+  let cst_nil =  mk noloc (Cst (Types.Atom Sequence.nil_atom))
+
+  let seq_of_string s =
+    let rec aux accu i = if (i = 0) then accu else aux (s.[i-1]::accu) (i-1) in
+    aux [] (String.length s)
+
+
   EXTEND
   GLOBAL: prog expr pat regexp const;
 
@@ -59,17 +67,28 @@ open Ast
     | "no_appl" 
     [ c = const -> mk loc (Cst c)
     | "("; l = LIST1 expr SEP ","; ")" -> tuple loc l
-    | "[";  l = LIST0 expr LEVEL "no_appl"; "]" ->
-        tuple loc (l @ [mk noloc (Cst (Types.Atom atom_nil))])
-    | "[";  l = LIST0 expr LEVEL "no_appl"; ";"; e = expr; "]" ->
+    | "[";  l = LIST0 seq_elem; e = OPT [ ";"; e = expr -> e ]; "]" ->
+	let e = match e with Some e -> e | None -> cst_nil in
+	let l = List.flatten l in
         tuple loc (l @ [e])
     | "<"; t = expr_tag_spec; a = expr_attrib_spec; ">"; c = expr ->
 	tuple loc [t;a;c]
     | "{"; r = [ expr_record_spec | -> mk loc (RecordLitt []) ]; "}" -> r
+    | "!"; t = pat -> mk loc (DebugTyper t)
     | a = LIDENT -> mk loc (Var a)
     ]
 
   ];
+
+  seq_elem: [
+    [ x = STRING -> 
+	let s = seq_of_string (Token.eval_string x) in
+	List.map 
+	  (fun c -> mk loc (Cst (Types.Char (Chars.Unichar.from_char c))))
+	  s 
+    | e = expr LEVEL "no_appl" -> [e]
+    ]
+  ];
 	  
   let_binding: [
     [ "let"; p = pat; "="; e = expr -> (p,e)
@@ -106,6 +125,16 @@ open Ast
     | x = regexp; "?" -> Alt (x, Epsilon)
     | x = regexp; "??" -> Alt (Epsilon, x) ]
   | [ "("; x = regexp; ")" -> x
+    | UIDENT "String" -> string
+    | s = STRING ->
+	let s = seq_of_string (Token.eval_string s) in
+	List.fold_right
+	  (fun c accu -> 
+	     let c = Chars.Unichar.from_char c in
+	     let c = Chars.atom c in
+	     Seq (Elem (mk loc (Internal (Types.char c))), accu))
+	  s
+	  Epsilon
     | e = pat LEVEL "simple" -> Elem e
     ]
   ];
@@ -120,7 +149,6 @@ open Ast
       | x = pat; "-"; y = pat -> mk loc (Diff (x,y)) ]
     | 
       [ "{"; r = record_spec; "}" -> r
-      | UIDENT "Any" -> mk loc (Internal Types.any)
       | LIDENT "_" -> mk loc (Internal Types.any)
       | a = LIDENT -> mk loc (Capture a)
       | "("; a = LIDENT; ":="; c = const; ")" -> mk loc (Constant (a,c))
@@ -130,12 +158,12 @@ open Ast
 	  and j = Big_int.big_int_of_string j in
           mk loc (Internal (Types.interval i j))
       | i = char ; "--"; j = char ->
-          mk loc (Internal (Types.char_class i j))
+          mk loc (Internal (Types.char (Chars.char_class i j)))
       | c = const -> mk loc (Internal (Types.constant c))
       | "("; l = LIST1 pat SEP ","; ")" -> multi_prod loc l
       | "["; r = [ r = regexp -> r | -> Epsilon ];
              q = [ ";"; q = pat -> q 
-                 | -> mk noloc (Internal (Types.atom atom_nil)) ]; 
+                 | -> mk noloc (Internal (Sequence.nil_type)) ]; 
              "]" -> mk loc (Regexp (r,q))
       | "<"; t = tag_spec; a = attrib_spec; ">"; c = pat ->
           multi_prod loc [t;a;c]
@@ -164,15 +192,15 @@ open Ast
   const:
     [ 
       [ i = INT -> Types.Integer (Big_int.big_int_of_string i)
-(*      | x = STRING -> Types.String (Token.eval_string x) *)
-      | "`"; a = [LIDENT | UIDENT] -> Types.Atom (Types.mk_atom a) 
+      | "`"; a = [LIDENT | UIDENT] -> Types.Atom (Types.mk_atom a)
       | c = char -> Types.Char c ]
     ];
 
   tag_spec:
     [
-      [ a = [LIDENT | UIDENT] -> 
-	  mk loc (Internal (Types.atom (Types.mk_atom a))) ]
+      [ LIDENT "_" -> mk loc (Internal (Types.atom (Atoms.any))) ]
+    | [ a = [LIDENT | UIDENT] -> 
+	  mk loc (Internal (Types.atom (Atoms.atom (Types.mk_atom a)))) ]
     | [ t = pat -> t ]
     ];
 

types/atoms.ml

 type 'a t = Finite of 'a list | Cofinite of 'a list
 
 let empty = Finite []
-let full = Cofinite []
+let any   = Cofinite []
 
 let atom x = Finite [x]
 

types/atoms.mli

 type 'a t (* = Finite of 'a list | Cofinite of 'a list *)
 
 val empty : 'a t
-val full : 'a t
+val any   : 'a t
 
 val cup : 'a t -> 'a t -> 'a t
 val cap : 'a t -> 'a t -> 'a t

types/builtin.ml

+let types =
+  [ 
+    "Empty",   Types.empty;
+    "Any",     Types.any;
+    "Int",     Types.Int.any;
+    "Char",    Types.char Chars.any;
+    "Atom",    Types.atom Atoms.any
+  ];

types/chars.ml

@@ -31,7 +31,7 @@ let from_int c =
 let to_int c = c
 
 let empty = []
-let full = [0,max_char]
+let any = [0,max_char]
 
 let char_class a b = if a<=b then [a,b] else empty
 

types/chars.mli

@@ -10,7 +10,7 @@ end
 type t = (Unichar.t * Unichar.t) list
 
 val empty : t
-val full  : t
+val any   : t
 val cup   : t -> t -> t
 val cap   : t -> t -> t
 val diff  : t -> t -> t

types/sequence.ml

-let atom_nil = Types.mk_atom "nil"
-let type_nil = Types.atom atom_nil
+let nil_atom = Types.mk_atom "nil"
+let nil_type = Types.atom (Atoms.atom nil_atom)
 
 let decompose t =
-  (Types.Atom.has_atom t atom_nil,
+  (Types.Atom.has_atom t nil_atom,
    Types.Product.get t)
 
 (*
@@ -51,8 +51,8 @@ let mapping f t queue =
   
 
 let aux_concat = mapping (fun t v -> V.times (V.ty t) v)
-let aux_flatten t = mapping aux_concat t (V.ty type_nil)
-let aux_map f t = mapping (fun t v -> V.times (V.ty (f t)) v) t (V.ty type_nil)
+let aux_flatten t = mapping aux_concat t (V.ty nil_type)
+let aux_map f t = mapping (fun t v -> V.times (V.ty (f t)) v) t (V.ty nil_type)
 
 let solve x = Types.descr (V.solve x)
 
@@ -65,7 +65,7 @@ let recurs f =
   Types.define n (f n);
   Types.internalize n
 
-let star t = recurs (fun n -> Types.cup type_nil (Types.times t n ))
+let star t = recurs (fun n -> Types.cup nil_type (Types.times t n ))
 
 let any_node = star (Types.cons Types.any)
 let any = Types.descr any_node

types/sequence.mli

+val nil_type: Types.descr
+val nil_atom: Types.atom
 val any: Types.descr
 val seqseq: Types.descr
 

types/types.ml

@@ -32,21 +32,20 @@ module I = struct
     arrow = Boolean.full; 
     record= Boolean.full; 
     ints  = Intervals.any;
-    atoms = Atoms.full;
-    chars = Chars.full;
+    atoms = Atoms.any;
+    chars = Chars.any;
   }
 	       
   let interval i j = { empty with ints = Intervals.atom i j }
   let times x y = { empty with times = Boolean.atom (x,y) }
   let arrow x y = { empty with arrow = Boolean.atom (x,y) }
   let record label opt t = { empty with record = Boolean.atom (label,opt,t) }
-  let atom a = { empty with atoms = Atoms.atom a }
-  let char c = { empty with chars = Chars.atom c }
-  let char_class c1 c2 = { empty with chars = Chars.char_class c1 c2 }
+  let atom a = { empty with atoms = a }
+  let char c = { empty with chars = c }
   let constant = function
     | Integer i -> interval i i
-    | Atom a -> atom a
-    | Char c -> char c
+    | Atom a -> atom (Atoms.atom a)
+    | Char c -> char (Chars.atom c)
 
 		   
   let any_record = { empty with record = any.record }

types/types.mli

@@ -34,12 +34,11 @@ val any    : descr
 (** Constructors **)
 
 val interval : Big_int.big_int -> Big_int.big_int -> descr
-val atom     : atom -> descr
+val atom     : atom Atoms.t -> descr
 val times    : node -> node -> descr
 val arrow    : node -> node -> descr
 val record   : label -> bool -> node -> descr
-val char     : Chars.Unichar.t -> descr
-val char_class : Chars.Unichar.t -> Chars.Unichar.t -> descr
+val char     : Chars.t -> descr
 val constant : const -> descr
 
 (** Positive systems and least solutions **)

typing/typed.ml

@@ -19,6 +19,8 @@ type texpr  = { exp_loc : loc;
 		exp_descr : texpr';
 	      }
 and  texpr' = 
+  | DebugTyper of ttyp
+
   (* CDuce is a Lambda-calculus ... *)
   | Var of string
   | Apply of texpr * texpr

typing/typer.ml

@@ -296,6 +296,7 @@ module Fv = StringSet
 let rec expr { loc = loc; descr = d } = 
   let (fv,td) = 
     match d with
+      | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
       | Var s -> (Fv.singleton s, Typed.Var s)
       | Apply (e1,e2) -> 
 	  let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
@@ -380,6 +381,7 @@ let rec compute_type env e =
   d
 
 and compute_type' loc env = function
+  | DebugTyper t -> Types.descr t
   | Var s -> Env.find s env
   | Apply (e1,e2) ->
       let t1 = compute_type env e1 and t2 = compute_type env e2 in