Commit f2d60961 authored by Pietro Abate's avatar Pietro Abate
Browse files

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

Original author: cvscast
Date: 2002-10-15 21:01:35+00:00
parent d68414df
......@@ -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
......
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
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
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)
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
......@@ -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
(*
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment