[r2002-10-15 21:01:00 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-15 21:01:35+00:00

Makefile

@@ -8,10 +8,12 @@ TYPES  = types/recursive.cmo types/sortedList.cmo \
          types/strings.cmo types/types.cmo \
          types/patterns.cmo 
 
-DIRS = parser typing types
+DRIVER = driver/cduce.cmo
+
+DIRS = parser typing types driver
 
 OBJECTS = $(TYPES) $(PARSER) $(TYPING)
-DEPEND = parser/*.ml parser/*.mli typing/*.ml typing/*.mli types/*.ml types/*.mli
+DEPEND = parser/*.ml parser/*.mli typing/*.ml typing/*.mli types/*.ml types/*.mli driver/*.mli driver/*.ml
 INCLUDES = -I +camlp4 -I parser -I types -I typing
 
 SYNTAX_PARSER = -pp 'camlp4o pa_extend.cmo'
@@ -19,6 +21,9 @@ SYNTAX_PARSER = -pp 'camlp4o pa_extend.cmo'
 all.cma: $(OBJECTS)
 	ocamlc -o all.cma -I +camlp4 gramlib.cma -a $(OBJECTS)
 
+cduce: all.cma $(DRIVER)
+	ocamlc -o cduce all.cma $(DRIVER)
+
 compute_depend:
 	@echo "Computing dependencies ..."
 	ocamldep $(INCLUDES) $(SYNTAX_PARSER) $(DEPEND) > depend
@@ -30,7 +35,9 @@ clean:
 	(cd parser; rm -f *.cmi *.cmo *.cma *~)
 	(cd types; rm -f *.cmi *.cmo *.cma *~)
 	(cd typing; rm -f *.cmi *.cmo *.cma *~)
+	(cd driver; rm -f *.cmi *.cmo *.cma *~)
 	rm -f *.cmi *.cmo *.cma *~
+	rm -f cduce
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx
 

depend

-parser/ast.cmo: types/patterns.cmi types/types.cmi 
-parser/ast.cmx: types/patterns.cmx types/types.cmx 
+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 parser/location.cmi types/types.cmi \
@@ -47,3 +47,5 @@ types/patterns.cmi: types/sortedList.cmi types/sortedMap.cmi types/types.cmi
 types/sortedMap.cmi: types/sortedList.cmi 
 types/syntax.cmi: types/patterns.cmi types/types.cmi 
 types/types.cmi: types/sortedMap.cmi types/strings.cmi 
+driver/cduce.cmo: parser/parser.cmi typing/typer.cmi types/types.cmi 
+driver/cduce.cmx: parser/parser.cmx typing/typer.cmx types/types.cmx 

driver/cduce.ml

+open Location
+
+let input = Stream.of_channel stdin
+let ppf = Format.std_formatter
+let prog () = 
+  try Parser.prog input
+  with
+    | Stdpp.Exc_located (loc, e) -> 
+        raise (Location (loc, e))
+
+let rec print_exn ppf = function
+  | Location ((i,j), exn) ->
+      Format.fprintf ppf "Error at chars %i-%i@\n" i j;
+      print_exn ppf exn
+  | Typer.Constraint (s,t,msg) ->
+      Format.fprintf ppf "%s@\n" msg;
+      Format.fprintf ppf "%a is not a subtype of %a@\n" 
+	Types.Print.print_descr s 
+	Types.Print.print_descr t;
+      Format.fprintf ppf "as shown by %a@\n" 
+	Types.Print.print_sample (Types.Sample.get (Types.diff s t))
+  | exn ->
+      Format.fprintf ppf "%s@\n" (Printexc.to_string exn)
+
+let phrase ph =
+  match ph.descr with
+    | Ast.EvalStatement e ->
+	let (fv,e) = Typer.expr e in
+	let t = Typer.compute_type Typer.Env.empty e in
+	Format.fprintf ppf "%a@\n" Types.Print.print_descr t;
+    | _ -> assert false
+
+let () = 
+  try List.iter phrase (prog ())
+  with exn -> print_exn ppf exn
+	

parser/parser.ml

 open Location
 open Ast
 
-module P = struct
-
   let gram    = Grammar.create (Plexer.make ())
+  let prog    = Grammar.Entry.create gram "prog"
   let expr    = Grammar.Entry.create gram "expression"
   let pat     = Grammar.Entry.create gram "type/pattern expression"
   let regexp  = Grammar.Entry.create gram "type/pattern regexp"
@@ -22,7 +21,12 @@ module P = struct
     | [] -> assert false
 	
   EXTEND
-  GLOBAL: expr pat regexp const;
+  GLOBAL: prog expr pat regexp const;
+
+  prog: [
+    [ l = LIST0 [ e = expr -> mk loc (EvalStatement e) ] SEP ";;";
+       "EOF"  -> l ]
+  ];
 
   expr: [
     "top" RIGHTA
@@ -173,8 +177,12 @@ module P = struct
     ];
 END
 
-end
+let pat = Grammar.Entry.parse pat
+let expr = Grammar.Entry.parse expr
+let prog = Grammar.Entry.parse prog
 
-let pat_or_typ s = Grammar.Entry.parse P.pat (Stream.of_string s)
+module From_string = struct
+  let pat s = pat (Stream.of_string s)
+  let expr s = expr (Stream.of_string s)
+end
 
-let expr s =  Grammar.Entry.parse P.expr (Stream.of_string s)

parser/parser.mli

-val pat_or_typ : string -> Ast.ppat
-val expr : string -> Ast.pexpr
+val expr : char Stream.t -> Ast.pexpr
+val pat : char Stream.t -> Ast.ppat
+val prog : char Stream.t -> Ast.pmodule_item list
+
+module From_string : sig
+  val pat  : string -> Ast.ppat
+  val expr : string -> Ast.pexpr
+end

types/types.ml

@@ -340,21 +340,24 @@ and sample_rec_times_aux memo (left,right) =
 and sample_rec_arrow c =
   find sample_rec_arrow_aux c
 
-and sample_rec_arrow_aux (left,right) =
-  let single_right (s1,s2) =
-    let rec aux accu1 accu2 = function
-      | (t1,t2)::left ->
-          let accu1' = diff_t accu1 t1 in
-          if non_empty accu1' then aux accu1 accu2 left;
-          let accu2' = cap_t accu2 t2 in
-          if non_empty accu2' then aux accu1 accu2 left
-      | [] -> raise NotEmpty
-    in
-    let accu1 = descr s1 in
-    (is_empty accu1) ||
-    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
+and check_empty_simple_arrow_line left (s1,s2) = 
+  let rec aux accu1 accu2 = function
+    | (t1,t2)::left ->
+        let accu1' = diff_t accu1 t1 in
+        if non_empty accu1' then aux accu1 accu2 left;
+        let accu2' = cap_t accu2 t2 in
+        if non_empty accu2' then aux accu1 accu2 left
+    | [] -> raise NotEmpty
   in
-  if List.exists single_right right then raise Not_found
+  let accu1 = descr s1 in
+  (is_empty accu1) ||
+  (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
+
+and check_empty_arrow_line left right = 
+  List.exists (check_empty_simple_arrow_line left) right
+
+and sample_rec_arrow_aux (left,right) =
+  if (check_empty_arrow_line left right) then raise Not_found
   else Fun left
 
 
@@ -366,6 +369,7 @@ and sample_rec_record_aux memo fields =
   List.fold_left aux [] fields
 
 let get x = sample_rec Assumptions.empty x
+
 end
 
 
@@ -547,9 +551,42 @@ let rec rec_normalize d =
 let normalize n =
   internalize (rec_normalize (descr n))
 
-
-let apply t1 t2 = 
-  failwith "apply: not yet implemented"
+let apply_simple result left t = 
+  let ok = ref false in
+  let rec aux result accu1 accu2 = function
+    | (t1,s1)::left ->
+        let result = 
+	  let accu1 = diff_t accu1 t1 in
+          if non_empty accu1 then aux result accu1 accu2 left
+          else (ok := true; result) in
+        let result =
+	  let accu2 = cap_t accu2 s1 in
+          aux result accu1 accu2 left in
+	result
+    | [] -> 
+        if subtype accu2 result 
+	then result
+	else cup result accu2
+  in
+  let result = aux result t any left in
+  if !ok then result else raise Not_found
+
+let apply t1 t2 =
+  if is_empty t2 
+  then empty
+  else
+    if non_empty {t1 with arrow = []} 
+    then raise Not_found
+    else
+      List.fold_left
+	(fun accu (left,right) ->
+	   if Sample.check_empty_arrow_line left right 
+	   then accu 
+	   else
+	     apply_simple accu left t2
+	)
+	empty
+	t1.arrow
   
 
 module Print =
@@ -643,6 +680,39 @@ struct
     Format.fprintf ppf "@[%a" print_descr d;
     end_print ppf
  
+  let rec print_sep f sep ppf = function
+    | [] -> ()
+    | [x] -> f ppf x
+    | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
+
+
+  let rec print_sample ppf = function
+    | Sample.Int i -> Format.fprintf ppf "%i" i
+    | Sample.Atom a -> Format.fprintf ppf "`%s" (atom_name a)
+    | Sample.String s -> Format.fprintf ppf "%S" s
+    | Sample.Pair (x1,x2) -> 
+	Format.fprintf ppf "(%a,%a)" 
+        print_sample x1
+        print_sample x2
+    | Sample.Record r ->
+	Format.fprintf ppf "{ %a }"
+	  (print_sep 
+	     (fun ppf (l,x) -> 
+		Format.fprintf ppf "%s = %a"
+		(label_name l)
+		print_sample x
+	     )
+	     " ; "
+	  ) r
+    | Sample.Fun iface ->
+	Format.fprintf ppf "(fun ( %a ) x -> ...)"
+	  (print_sep
+	     (fun ppf (t1,t2) ->
+		Format.fprintf ppf "%a -> %a; "
+		print t1 print t2
+	     )
+	     " ; "
+	  ) iface
 end
 
 (*

types/types.mli

@@ -132,6 +132,7 @@ module Print :
 sig
   val print : Format.formatter -> node -> unit
   val print_descr: Format.formatter -> descr -> unit
+  val print_sample : Format.formatter -> Sample.t -> unit
 end
 
 val check: descr -> unit