viewcvs.cgi/driver/cduce.ml

open Location
open Ident

let version = "0.0.9 (alpha)"

let quiet = ref false

let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty

let enter_global_value x v t =
  Eval.enter_global x v;
  typing_env := Typer.Env.add x t !typing_env

let rec is_abstraction = function
  | Ast.Abstraction _ -> true
  | Ast.LocatedExpr (_,e) -> is_abstraction e
  | _ -> false

let print_norm ppf d = 
  Location.protect ppf 
    (fun ppf -> Types.Print.print ppf ((*Types.normalize*) d))

let print_value ppf v =
  Location.protect ppf (fun ppf -> Value.print ppf v)

let dump_env ppf =
  Format.fprintf ppf "Global types:";
  Typer.dump_global_types ppf;
  Format.fprintf ppf ".@\n";
  Eval.Env.iter 
    (fun x v ->
       let t = Typer.Env.find x !typing_env in
       Format.fprintf ppf "@[|- %a : %a@ => %a@]@\n"
         U.print (Id.value x)
         print_norm t
         print_value v
    )
    !Eval.global_env
  

let rec print_exn ppf = function
  | Location (loc, exn) ->
      Format.fprintf ppf "Error %a:@\n" Location.print_loc loc;
      Format.fprintf ppf "%a" Location.html_hilight loc;
      print_exn ppf exn
  | Value.CDuceExn v ->
      Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@\n"
        print_value v
  | Eval.MultipleDeclaration v ->
      Format.fprintf ppf "Multiple declaration for global value %a@\n" 
        U.print (Id.value v)
  | Typer.WrongLabel (t,l) ->
      Format.fprintf ppf "Wrong record selection: the label %a@\n" 
        U.print (LabelPool.value l);
      Format.fprintf ppf "applied to an expression of type:@\n%a@\n"
        print_norm t
  | Typer.ShouldHave (t,msg) ->
      Format.fprintf ppf "This expression should have type:@\n%a@\n%s@\n" 
        print_norm t
        msg
  | Typer.ShouldHave2 (t1,msg,t2) ->
      Format.fprintf ppf "This expression should have type:@\n%a@\n%s %a@\n" 
        print_norm t1
        msg
        print_norm t2
  | Typer.Constraint (s,t,msg) ->
      Format.fprintf ppf "This expression should have type:@\n%a@\n" 
        print_norm t;
      Format.fprintf ppf "but its inferred type is:@\n%a@\n" 
        print_norm s;
      Format.fprintf ppf "which is not a subtype, as shown by the sample:@\n" ;
      Location.protect ppf
        (fun ppf ->
           Sample.print ppf (Sample.get (Types.diff s t)));
      Format.fprintf ppf "@\n%s@\n" msg
  | Typer.NonExhaustive t ->
      Format.fprintf ppf "This pattern matching is not exhaustive@\n";
      Format.fprintf ppf "Residual type:@\n%a@\n"
        print_norm t;
      Format.fprintf ppf "Sample:@\n%a@\n" 
        Sample.print (Sample.get t)
  | Typer.UnboundId x ->
      Format.fprintf ppf "Unbound identifier %a@\n" U.print (Id.value x)
  | Wlexer.Illegal_character c ->
      Format.fprintf ppf "Illegal character (%s)@\n" (Char.escaped c)
  | Wlexer.Unterminated_comment ->
      Format.fprintf ppf "Comment not terminated@\n"
  | Wlexer.Unterminated_string ->
      Format.fprintf ppf "String literal not terminated@\n"
  | Wlexer.Unterminated_string_in_comment ->
      Format.fprintf ppf "This comment contains an unterminated string literal@\n"
  | Parser.Error s | Stream.Error s -> 
      Format.fprintf ppf "Parsing error: %s@\n" s
  | Location.Generic s ->
      Format.fprintf ppf "%s@\n" s
  | exn ->
(*      raise exn *)
      Format.fprintf ppf "%s@\n" (Printexc.to_string exn)

let debug ppf = function
  | `Subtype (t1,t2) ->
      Format.fprintf ppf "[DEBUG:subtype]@\n";
      let t1 = Types.descr (Typer.typ t1)
      and t2 = Types.descr (Typer.typ t2) in
      Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2
        (Types.subtype t1 t2)
  | `Sample t ->
      Format.fprintf ppf "[DEBUG:sample]@\n";
      let t = Types.descr (Typer.typ t) in
      Location.protect ppf
        (fun ppf -> Sample.print ppf (Sample.get t));
      Format.fprintf ppf "@\n"
  | `Filter (t,p) -> 
      Format.fprintf ppf "[DEBUG:filter]@\n";
      let t = Typer.typ t
      and p = Typer.pat p in
      let f = Patterns.filter (Types.descr t) p in
      List.iter (fun (x,t) ->
                   Format.fprintf ppf " %a:%a@\n" U.print (Id.value x)
                     print_norm (Types.descr t)) f
  | `Accept p ->
      Format.fprintf ppf "[DEBUG:accept]@\n";
      let p = Typer.pat p in
      let t = Patterns.accept p in
      Format.fprintf ppf " %a@\n" Types.Print.print (Types.descr t)
  | `Compile (t,pl) ->
      Format.fprintf ppf "[DEBUG:compile]@\n";
      let t = Typer.typ t
      and pl = List.map Typer.pat pl in
      Patterns.Compile.debug_compile ppf t pl


let mk_builtin () =
  let bi = List.map (fun (n,t) -> [n, mknoloc (Ast.Internal t)]) 
             Builtin.types in
  List.iter Typer.register_global_types bi

let () = mk_builtin ()


let run ppf ppf_err input =
  let insert_type_bindings = 
    List.iter (fun (x,t) ->
                 typing_env := Typer.Env.add x t !typing_env;
                 if not !quiet then
                   Format.fprintf ppf "|- %a : %a@\n@." U.print (Id.value x) print_norm t) 
  in
  
  let type_decl decl =
    insert_type_bindings (Typer.type_let_decl !typing_env decl);
    Typer.report_unused_branches ()
  in

  let eval_decl decl =
    let bindings = Eval.eval_let_decl Eval.Env.empty decl in
    List.iter 
      (fun (x,v) ->
         Eval.enter_global x v;
         if not !quiet then
           Format.fprintf ppf "=> %a : @[%a@]@\n@." U.print (Id.value x) print_value v
      ) bindings
  in

  let phrase ph = 
    match ph.descr with
      | Ast.EvalStatement e ->
          let (fv,e) = Typer.expr e in
          let t = Typer.type_check !typing_env e Types.any true in
          Typer.report_unused_branches ();
          Location.dump_loc ppf e.Typed.exp_loc;
          if not !quiet then
            Format.fprintf ppf "|- %a@\n@." print_norm t;
          let v = Eval.eval Eval.Env.empty e in
          if not !quiet then
            Format.fprintf ppf "=> @[%a@]@\n@." print_value v
      | Ast.LetDecl (p,e) when is_abstraction e -> ()
      | Ast.LetDecl (p,e) ->
          let decl = Typer.let_decl p e in
          type_decl decl;
          Typer.report_unused_branches ();
          eval_decl decl
      | Ast.TypeDecl _ -> ()
      | Ast.Debug l -> debug ppf l
      | _ -> assert false
  in

  let do_fun_decls decls =
    let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in
    insert_type_bindings (Typer.type_rec_funs !typing_env decls);
    Typer.report_unused_branches ();
    List.iter eval_decl decls
  in
  let rec phrases funs = function
    | { descr = Ast.LetDecl (p,e) } :: phs when is_abstraction e -> 
        phrases ((p,e)::funs) phs
    | ph :: phs ->
        do_fun_decls funs;
        phrase ph;
        phrases [] phs
    | _ ->
        do_fun_decls funs
  in
  try 
    let p = 
      try Parser.prog input
      with
        | Stdpp.Exc_located (_, (Location _ as e)) -> raise e
        | Stdpp.Exc_located ((i,j), e) -> raise_loc i j e
    in
    let (type_decls,fun_decls) = 
      List.fold_left
        (fun ((typs,funs) as accu) ph -> match ph.descr with
           | Ast.TypeDecl (x,t) -> ((x,t) :: typs,funs)
           | Ast.LetDecl (p,e) when is_abstraction e -> 
               (typs, (p,e)::funs)
           | _ -> accu
        ) ([],[]) p in
    Typer.register_global_types type_decls;
    phrases [] p;
    true
  with 
    | (Failure _ | Not_found | Invalid_argument _) as e -> 
        raise e  (* To get ocamlrun stack trace *)
    | exn -> print_exn ppf_err exn; false
        

1	abate	10	open Location
2	abate	225	open Ident
3	abate	10
4	abate	370	let version = "0.0.9 (alpha)"
5	abate	368
6	abate	217	let quiet = ref false
7
8	abate	107	let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty
9
10	abate	368	let enter_global_value x v t =
11			Eval.enter_global x v;
12			typing_env := Typer.Env.add x t !typing_env
13
14	abate	332	let rec is_abstraction = function
15			\| Ast.Abstraction _ -> true
16			\| Ast.LocatedExpr (_,e) -> is_abstraction e
17			\| _ -> false
18
19	abate	29	let print_norm ppf d =
20	abate	92	Location.protect ppf
21	abate	367	(fun ppf -> Types.Print.print ppf ((Types.normalize) d))
22	abate	29
23	abate	92	let print_value ppf v =
24			Location.protect ppf (fun ppf -> Value.print ppf v)
25
26	abate	107	let dump_env ppf =
27	abate	278	Format.fprintf ppf "Global types:";
28			Typer.dump_global_types ppf;
29			Format.fprintf ppf ".@\n";
30	abate	107	Eval.Env.iter
31			(fun x v ->
32			let t = Typer.Env.find x !typing_env in
33	abate	374	Format.fprintf ppf "@[\|- %a : %a@ => %a@]@\n"
34			U.print (Id.value x)
35	abate	107	print_norm t
36			print_value v
37			)
38	abate	278	!Eval.global_env
39	abate	107
40
41	abate	10	let rec print_exn ppf = function
42	abate	66	\| Location (loc, exn) ->
43	abate	91	Format.fprintf ppf "Error %a:@\n" Location.print_loc loc;
44	abate	92	Format.fprintf ppf "%a" Location.html_hilight loc;
45	abate	91	print_exn ppf exn
46	abate	64	\| Value.CDuceExn v ->
47			Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@\n"
48	abate	92	print_value v
49	abate	368	\| Eval.MultipleDeclaration v ->
50	abate	374	Format.fprintf ppf "Multiple declaration for global value %a@\n"
51			U.print (Id.value v)
52	abate	26	\| Typer.WrongLabel (t,l) ->
53	abate	374	Format.fprintf ppf "Wrong record selection: the label %a@\n"
54			U.print (LabelPool.value l);
55	abate	364	Format.fprintf ppf "applied to an expression of type:@\n%a@\n"
56	abate	29	print_norm t
57	abate	19	\| Typer.ShouldHave (t,msg) ->
58	abate	364	Format.fprintf ppf "This expression should have type:@\n%a@\n%s@\n"
59	abate	29	print_norm t
60	abate	28	msg
61	abate	355	\| Typer.ShouldHave2 (t1,msg,t2) ->
62	abate	364	Format.fprintf ppf "This expression should have type:@\n%a@\n%s %a@\n"
63	abate	355	print_norm t1
64			msg
65			print_norm t2
66	abate	10	\| Typer.Constraint (s,t,msg) ->
67	abate	364	Format.fprintf ppf "This expression should have type:@\n%a@\n"
68	abate	29	print_norm t;
69	abate	412	Format.fprintf ppf "but its inferred type is:@\n%a@\n"
70	abate	29	print_norm s;
71	abate	410	Format.fprintf ppf "which is not a subtype, as shown by the sample:@\n" ;
72	abate	293	Location.protect ppf
73			(fun ppf ->
74	abate	407	Sample.print ppf (Sample.get (Types.diff s t)));
75	abate	293	Format.fprintf ppf "@\n%s@\n" msg
76	abate	17	\| Typer.NonExhaustive t ->
77			Format.fprintf ppf "This pattern matching is not exhaustive@\n";
78	abate	364	Format.fprintf ppf "Residual type:@\n%a@\n"
79	abate	29	print_norm t;
80	abate	407	Format.fprintf ppf "Sample:@\n%a@\n"
81			Sample.print (Sample.get t)
82	abate	36	\| Typer.UnboundId x ->
83	abate	374	Format.fprintf ppf "Unbound identifier %a@\n" U.print (Id.value x)
84	abate	81	\| Wlexer.Illegal_character c ->
85			Format.fprintf ppf "Illegal character (%s)@\n" (Char.escaped c)
86			\| Wlexer.Unterminated_comment ->
87			Format.fprintf ppf "Comment not terminated@\n"
88			\| Wlexer.Unterminated_string ->
89			Format.fprintf ppf "String literal not terminated@\n"
90			\| Wlexer.Unterminated_string_in_comment ->
91			Format.fprintf ppf "This comment contains an unterminated string literal@\n"
92	abate	90	\| Parser.Error s \| Stream.Error s ->
93	abate	81	Format.fprintf ppf "Parsing error: %s@\n" s
94	abate	91	\| Location.Generic s ->
95			Format.fprintf ppf "%s@\n" s
96	abate	10	\| exn ->
97	abate	403	(* raise exn *)
98	abate	10	Format.fprintf ppf "%s@\n" (Printexc.to_string exn)
99
100	abate	90	let debug ppf = function
101	abate	224	\| `Subtype (t1,t2) ->
102			Format.fprintf ppf "[DEBUG:subtype]@\n";
103	abate	277	let t1 = Types.descr (Typer.typ t1)
104			and t2 = Types.descr (Typer.typ t2) in
105	abate	224	Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2
106			(Types.subtype t1 t2)
107	abate	407	\| `Sample t ->
108			Format.fprintf ppf "[DEBUG:sample]@\n";
109			let t = Types.descr (Typer.typ t) in
110			Location.protect ppf
111			(fun ppf -> Sample.print ppf (Sample.get t));
112			Format.fprintf ppf "@\n"
113	abate	43	\| `Filter (t,p) ->
114			Format.fprintf ppf "[DEBUG:filter]@\n";
115	abate	277	let t = Typer.typ t
116			and p = Typer.pat p in
117	abate	43	let f = Patterns.filter (Types.descr t) p in
118			List.iter (fun (x,t) ->
119	abate	374	Format.fprintf ppf " %a:%a@\n" U.print (Id.value x)
120	abate	43	print_norm (Types.descr t)) f
121			\| `Accept p ->
122			Format.fprintf ppf "[DEBUG:accept]@\n";
123	abate	277	let p = Typer.pat p in
124	abate	43	let t = Patterns.accept p in
125	abate	367	Format.fprintf ppf " %a@\n" Types.Print.print (Types.descr t)
126	abate	43	\| `Compile (t,pl) ->
127			Format.fprintf ppf "[DEBUG:compile]@\n";
128	abate	277	let t = Typer.typ t
129			and pl = List.map Typer.pat pl in
130	abate	149	Patterns.Compile.debug_compile ppf t pl
131	abate	66
132
133	abate	107
134	abate	90	let mk_builtin () =
135	abate	249	let bi = List.map (fun (n,t) -> [n, mknoloc (Ast.Internal t)])
136	abate	107	Builtin.types in
137	abate	277	List.iter Typer.register_global_types bi
138	abate	66
139	abate	95	let () = mk_builtin ()
140
141
142	abate	124	let run ppf ppf_err input =
143	abate	90	let insert_type_bindings =
144			List.iter (fun (x,t) ->
145			typing_env := Typer.Env.add x t !typing_env;
146	abate	217	if not !quiet then
147	abate	374	Format.fprintf ppf "\|- %a : %a@\n@." U.print (Id.value x) print_norm t)
148	abate	90	in
149
150			let type_decl decl =
151	abate	314	insert_type_bindings (Typer.type_let_decl !typing_env decl);
152			Typer.report_unused_branches ()
153	abate	90	in
154	abate	10
155	abate	90	let eval_decl decl =
156	abate	107	let bindings = Eval.eval_let_decl Eval.Env.empty decl in
157	abate	90	List.iter
158			(fun (x,v) ->
159			Eval.enter_global x v;
160	abate	217	if not !quiet then
161	abate	374	Format.fprintf ppf "=> %a : @[%a@]@\n@." U.print (Id.value x) print_value v
162	abate	90	) bindings
163			in
164	abate	66
165	abate	126	let phrase ph =
166	abate	90	match ph.descr with
167			\| Ast.EvalStatement e ->
168	abate	277	let (fv,e) = Typer.expr e in
169	abate	90	let t = Typer.type_check !typing_env e Types.any true in
170	abate	314	Typer.report_unused_branches ();
171	abate	93	Location.dump_loc ppf e.Typed.exp_loc;
172	abate	217	if not !quiet then
173			Format.fprintf ppf "\|- %a@\n@." print_norm t;
174	abate	107	let v = Eval.eval Eval.Env.empty e in
175	abate	217	if not !quiet then
176			Format.fprintf ppf "=> @[%a@]@\n@." print_value v
177	abate	332	\| Ast.LetDecl (p,e) when is_abstraction e -> ()
178	abate	90	\| Ast.LetDecl (p,e) ->
179	abate	277	let decl = Typer.let_decl p e in
180	abate	90	type_decl decl;
181	abate	314	Typer.report_unused_branches ();
182	abate	90	eval_decl decl
183			\| Ast.TypeDecl _ -> ()
184			\| Ast.Debug l -> debug ppf l
185			\| _ -> assert false
186			in
187
188			let do_fun_decls decls =
189	abate	277	let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in
190	abate	315	insert_type_bindings (Typer.type_rec_funs !typing_env decls);
191	abate	314	Typer.report_unused_branches ();
192	abate	90	List.iter eval_decl decls
193			in
194	abate	126	let rec phrases funs = function
195	abate	332	\| { descr = Ast.LetDecl (p,e) } :: phs when is_abstraction e ->
196	abate	126	phrases ((p,e)::funs) phs
197			\| ph :: phs ->
198			do_fun_decls funs;
199			phrase ph;
200			phrases [] phs
201			\| _ ->
202			do_fun_decls funs
203			in
204	abate	13	try
205	abate	90	let p =
206			try Parser.prog input
207			with
208			\| Stdpp.Exc_located (_, (Location _ as e)) -> raise e
209	abate	249	\| Stdpp.Exc_located ((i,j), e) -> raise_loc i j e
210	abate	90	in
211	abate	66	let (type_decls,fun_decls) =
212	abate	13	List.fold_left
213	abate	66	(fun ((typs,funs) as accu) ph -> match ph.descr with
214			\| Ast.TypeDecl (x,t) -> ((x,t) :: typs,funs)
215	abate	332	\| Ast.LetDecl (p,e) when is_abstraction e ->
216	abate	66	(typs, (p,e)::funs)
217	abate	13	\| _ -> accu
218	abate	66	) ([],[]) p in
219	abate	277	Typer.register_global_types type_decls;
220	abate	126	phrases [] p;
221	abate	95	true
222	abate	28	with
223	abate	57	\| (Failure _ \| Not_found \| Invalid_argument _) as e ->
224	abate	90	raise e (* To get ocamlrun stack trace *)
225	abate	124	\| exn -> print_exn ppf_err exn; false
226	abate	10
227	abate	21