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" Env.empty

let enter_global_value x v t =
  Eval.enter_global x v;
  typing_env := 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";
  Env.iter 
    (fun x v ->
       let t = 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.Error s ->
      Format.fprintf ppf "%s@\n" s
  | Typer.Constraint (s,t) ->
      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"
  | 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 run ppf ppf_err input =
  let insert_type_bindings = 
    List.iter (fun (x,t) ->
                 typing_env := 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 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 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	421	let typing_env = State.ref "Cduce.typing_env" Env.empty
9	abate	107
10	abate	368	let enter_global_value x v t =
11			Eval.enter_global x v;
12	abate	421	typing_env := Env.add x t !typing_env
13	abate	368
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	421	Env.iter
31	abate	107	(fun x v ->
32	abate	421	let t = 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	421	\| Typer.Error s ->
67			Format.fprintf ppf "%s@\n" s
68			\| Typer.Constraint (s,t) ->
69	abate	364	Format.fprintf ppf "This expression should have type:@\n%a@\n"
70	abate	29	print_norm t;
71	abate	412	Format.fprintf ppf "but its inferred type is:@\n%a@\n"
72	abate	29	print_norm s;
73	abate	410	Format.fprintf ppf "which is not a subtype, as shown by the sample:@\n" ;
74	abate	293	Location.protect ppf
75			(fun ppf ->
76	abate	407	Sample.print ppf (Sample.get (Types.diff s t)));
77	abate	421	Format.fprintf ppf "@\n"
78	abate	17	\| Typer.NonExhaustive t ->
79			Format.fprintf ppf "This pattern matching is not exhaustive@\n";
80	abate	364	Format.fprintf ppf "Residual type:@\n%a@\n"
81	abate	29	print_norm t;
82	abate	407	Format.fprintf ppf "Sample:@\n%a@\n"
83			Sample.print (Sample.get t)
84	abate	36	\| Typer.UnboundId x ->
85	abate	374	Format.fprintf ppf "Unbound identifier %a@\n" U.print (Id.value x)
86	abate	81	\| Wlexer.Illegal_character c ->
87			Format.fprintf ppf "Illegal character (%s)@\n" (Char.escaped c)
88			\| Wlexer.Unterminated_comment ->
89			Format.fprintf ppf "Comment not terminated@\n"
90			\| Wlexer.Unterminated_string ->
91			Format.fprintf ppf "String literal not terminated@\n"
92			\| Wlexer.Unterminated_string_in_comment ->
93			Format.fprintf ppf "This comment contains an unterminated string literal@\n"
94	abate	90	\| Parser.Error s \| Stream.Error s ->
95	abate	81	Format.fprintf ppf "Parsing error: %s@\n" s
96	abate	91	\| Location.Generic s ->
97			Format.fprintf ppf "%s@\n" s
98	abate	10	\| exn ->
99	abate	403	(* raise exn *)
100	abate	10	Format.fprintf ppf "%s@\n" (Printexc.to_string exn)
101
102	abate	90	let debug ppf = function
103	abate	224	\| `Subtype (t1,t2) ->
104			Format.fprintf ppf "[DEBUG:subtype]@\n";
105	abate	277	let t1 = Types.descr (Typer.typ t1)
106			and t2 = Types.descr (Typer.typ t2) in
107	abate	224	Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2
108			(Types.subtype t1 t2)
109	abate	407	\| `Sample t ->
110			Format.fprintf ppf "[DEBUG:sample]@\n";
111			let t = Types.descr (Typer.typ t) in
112			Location.protect ppf
113			(fun ppf -> Sample.print ppf (Sample.get t));
114			Format.fprintf ppf "@\n"
115	abate	43	\| `Filter (t,p) ->
116			Format.fprintf ppf "[DEBUG:filter]@\n";
117	abate	277	let t = Typer.typ t
118			and p = Typer.pat p in
119	abate	43	let f = Patterns.filter (Types.descr t) p in
120			List.iter (fun (x,t) ->
121	abate	374	Format.fprintf ppf " %a:%a@\n" U.print (Id.value x)
122	abate	43	print_norm (Types.descr t)) f
123			\| `Accept p ->
124			Format.fprintf ppf "[DEBUG:accept]@\n";
125	abate	277	let p = Typer.pat p in
126	abate	43	let t = Patterns.accept p in
127	abate	367	Format.fprintf ppf " %a@\n" Types.Print.print (Types.descr t)
128	abate	43	\| `Compile (t,pl) ->
129			Format.fprintf ppf "[DEBUG:compile]@\n";
130	abate	277	let t = Typer.typ t
131			and pl = List.map Typer.pat pl in
132	abate	149	Patterns.Compile.debug_compile ppf t pl
133	abate	66
134
135	abate	107
136	abate	66
137	abate	95
138	abate	124	let run ppf ppf_err input =
139	abate	90	let insert_type_bindings =
140			List.iter (fun (x,t) ->
141	abate	421	typing_env := Env.add x t !typing_env;
142	abate	217	if not !quiet then
143	abate	374	Format.fprintf ppf "\|- %a : %a@\n@." U.print (Id.value x) print_norm t)
144	abate	90	in
145
146			let type_decl decl =
147	abate	314	insert_type_bindings (Typer.type_let_decl !typing_env decl);
148			Typer.report_unused_branches ()
149	abate	90	in
150	abate	10
151	abate	90	let eval_decl decl =
152	abate	421	let bindings = Eval.eval_let_decl Env.empty decl in
153	abate	90	List.iter
154			(fun (x,v) ->
155			Eval.enter_global x v;
156	abate	217	if not !quiet then
157	abate	374	Format.fprintf ppf "=> %a : @[%a@]@\n@." U.print (Id.value x) print_value v
158	abate	90	) bindings
159			in
160	abate	66
161	abate	126	let phrase ph =
162	abate	90	match ph.descr with
163			\| Ast.EvalStatement e ->
164	abate	277	let (fv,e) = Typer.expr e in
165	abate	90	let t = Typer.type_check !typing_env e Types.any true in
166	abate	314	Typer.report_unused_branches ();
167	abate	93	Location.dump_loc ppf e.Typed.exp_loc;
168	abate	217	if not !quiet then
169			Format.fprintf ppf "\|- %a@\n@." print_norm t;
170	abate	421	let v = Eval.eval Env.empty e in
171	abate	217	if not !quiet then
172			Format.fprintf ppf "=> @[%a@]@\n@." print_value v
173	abate	332	\| Ast.LetDecl (p,e) when is_abstraction e -> ()
174	abate	90	\| Ast.LetDecl (p,e) ->
175	abate	277	let decl = Typer.let_decl p e in
176	abate	90	type_decl decl;
177	abate	314	Typer.report_unused_branches ();
178	abate	90	eval_decl decl
179			\| Ast.TypeDecl _ -> ()
180			\| Ast.Debug l -> debug ppf l
181			\| _ -> assert false
182			in
183
184			let do_fun_decls decls =
185	abate	277	let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in
186	abate	315	insert_type_bindings (Typer.type_rec_funs !typing_env decls);
187	abate	314	Typer.report_unused_branches ();
188	abate	90	List.iter eval_decl decls
189			in
190	abate	126	let rec phrases funs = function
191	abate	332	\| { descr = Ast.LetDecl (p,e) } :: phs when is_abstraction e ->
192	abate	126	phrases ((p,e)::funs) phs
193			\| ph :: phs ->
194			do_fun_decls funs;
195			phrase ph;
196			phrases [] phs
197			\| _ ->
198			do_fun_decls funs
199			in
200	abate	13	try
201	abate	90	let p =
202			try Parser.prog input
203			with
204			\| Stdpp.Exc_located (_, (Location _ as e)) -> raise e
205	abate	249	\| Stdpp.Exc_located ((i,j), e) -> raise_loc i j e
206	abate	90	in
207	abate	66	let (type_decls,fun_decls) =
208	abate	13	List.fold_left
209	abate	66	(fun ((typs,funs) as accu) ph -> match ph.descr with
210			\| Ast.TypeDecl (x,t) -> ((x,t) :: typs,funs)
211	abate	332	\| Ast.LetDecl (p,e) when is_abstraction e ->
212	abate	66	(typs, (p,e)::funs)
213	abate	13	\| _ -> accu
214	abate	66	) ([],[]) p in
215	abate	277	Typer.register_global_types type_decls;
216	abate	126	phrases [] p;
217	abate	95	true
218	abate	28	with
219	abate	57	\| (Failure _ \| Not_found \| Invalid_argument _) as e ->
220	abate	90	raise e (* To get ocamlrun stack trace *)
221	abate	124	\| exn -> print_exn ppf_err exn; false
222	abate	10
223	abate	21