Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 4f26dcf5

History | View | Annotate | Download (32.7 KB)

1 a2d97a3e ploc
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
12
(********************************************************************)
13 22fe1c93 ploc
14
(** Main typing module. Classic inference algorithm with destructive
15
    unification. *)
16
17
let debug fmt args = () (* Format.eprintf "%a"  *)
18
(* Though it shares similarities with the clock calculus module, no code
19
    is shared.  Simple environments, very limited identifier scoping, no
20
    identifier redefinition allowed. *)
21
22
open Utils
23
(* Yes, opening both modules is dirty as some type names will be
24
   overwritten, yet this makes notations far lighter.*)
25 8446bf03 ploc
open Lustre_types
26 22fe1c93 ploc
open Corelang
27 66359a5e ploc
(* open Types *)
28 22fe1c93 ploc
open Format
29
30 66359a5e ploc
31
module type EXPR_TYPE_HUB =
32
sig
33
  type type_expr 
34
  val import: Types.Main.type_expr -> type_expr
35
  val export: type_expr -> Types.Main.type_expr 
36
end
37
38
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =  
39
struct
40
41
  module TP = Type_predef.Make (T)
42
  include TP
43
    
44
let basic_coretype_type t =
45
  if is_real_type t then Tydec_real else
46
    if is_int_type t then Tydec_int else
47
      if is_bool_type t then Tydec_bool else
48
	assert false
49
50
51
52 22fe1c93 ploc
let pp_typing_env fmt env =
53
  Env.pp_env print_ty fmt env
54
55
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
56
    type [ty]. False otherwise. *)
57
let rec occurs tvar ty =
58
  let ty = repr ty in
59 66359a5e ploc
  match type_desc ty with
60 22fe1c93 ploc
  | Tvar -> ty=tvar
61
  | Tarrow (t1, t2) ->
62
      (occurs tvar t1) || (occurs tvar t2)
63
  | Ttuple tl ->
64 12af4908 xthirioux
     List.exists (occurs tvar) tl
65
  | Tstruct fl ->
66
     List.exists (fun (f, t) -> occurs tvar t) fl
67 22fe1c93 ploc
  | Tarray (_, t)
68
  | Tstatic (_, t)
69
  | Tclock t
70
  | Tlink t -> occurs tvar t
71 66359a5e ploc
  | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
72 22fe1c93 ploc
73
(** Promote monomorphic type variables to polymorphic type variables. *)
74
(* Generalize by side-effects *)
75
let rec generalize ty =
76 66359a5e ploc
  match type_desc ty with
77 22fe1c93 ploc
  | Tvar ->
78
      (* No scopes, always generalize *)
79
      ty.tdesc <- Tunivar
80
  | Tarrow (t1,t2) ->
81
      generalize t1; generalize t2
82 12af4908 xthirioux
  | Ttuple tl ->
83
     List.iter generalize tl
84
  | Tstruct fl ->
85
     List.iter (fun (f, t) -> generalize t) fl
86 22fe1c93 ploc
  | Tstatic (d, t)
87
  | Tarray (d, t) -> Dimension.generalize d; generalize t
88
  | Tclock t
89
  | Tlink t ->
90
      generalize t
91 66359a5e ploc
  | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
92 22fe1c93 ploc
93
(** Downgrade polymorphic type variables to monomorphic type variables *)
94
let rec instantiate inst_vars inst_dim_vars ty =
95
  let ty = repr ty in
96
  match ty.tdesc with
97 66359a5e ploc
  | Tenum _ | Tconst _ | Tvar | Tbasic _  -> ty
98 22fe1c93 ploc
  | Tarrow (t1,t2) ->
99
      {ty with tdesc =
100
       Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
101
  | Ttuple tlist ->
102
      {ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
103 12af4908 xthirioux
  | Tstruct flist ->
104
      {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
105 22fe1c93 ploc
  | Tclock t ->
106
	{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
107
  | Tstatic (d, t) ->
108
	{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
109
  | Tarray (d, t) ->
110
	{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
111
  | Tlink t ->
112
	(* should not happen *)
113
	{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
114
  | Tunivar ->
115
      try
116
        List.assoc ty.tid !inst_vars
117
      with Not_found ->
118
        let var = new_var () in
119
	inst_vars := (ty.tid, var)::!inst_vars;
120
	var
121
122
(* [type_coretype cty] types the type declaration [cty] *)
123
let rec type_coretype type_dim cty =
124
  match (*get_repr_type*) cty with
125
  | Tydec_any -> new_var ()
126 66359a5e ploc
  | Tydec_int -> type_int
127
  | Tydec_real -> (* Type_predef. *)type_real
128 04a63d25 xthirioux
  (* | Tydec_float -> Type_predef.type_real *)
129 66359a5e ploc
  | Tydec_bool -> (* Type_predef. *)type_bool
130
  | Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty)
131
  | Tydec_const c -> (* Type_predef. *)type_const c
132
  | Tydec_enum tl -> (* Type_predef. *)type_enum tl
133
  | Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
134 22fe1c93 ploc
  | Tydec_array (d, ty) ->
135
    begin
136 ec433d69 xthirioux
      let d = Dimension.copy (ref []) d in
137 22fe1c93 ploc
      type_dim d;
138 66359a5e ploc
      (* Type_predef. *)type_array d (type_coretype type_dim ty)
139 22fe1c93 ploc
    end
140
141 21485807 xthirioux
(* [coretype_type] is the reciprocal of [type_typecore] *)
142 22fe1c93 ploc
let rec coretype_type ty =
143
 match (repr ty).tdesc with
144
 | Tvar           -> Tydec_any
145 66359a5e ploc
 | Tbasic _       -> basic_coretype_type ty
146 22fe1c93 ploc
 | Tconst c       -> Tydec_const c
147
 | Tclock t       -> Tydec_clock (coretype_type t)
148
 | Tenum tl       -> Tydec_enum tl
149 12af4908 xthirioux
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
150 22fe1c93 ploc
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
151
 | Tstatic (_, t) -> coretype_type t
152
 | _         -> assert false
153
154 ef34b4ae xthirioux
let get_coretype_definition tname =
155 22fe1c93 ploc
  try
156 ef34b4ae xthirioux
    let top = Hashtbl.find type_table (Tydec_const tname) in
157
    match top.top_decl_desc with
158
    | TypeDef tdef -> tdef.tydef_desc
159
    | _ -> assert false
160 22fe1c93 ploc
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
161
162 ef34b4ae xthirioux
let get_type_definition tname =
163
    type_coretype (fun d -> ()) (get_coretype_definition tname)
164
165 695d6f2f xthirioux
(* Equality on ground types only *)
166
(* Should be used between local variables which must have a ground type *)
167
let rec eq_ground t1 t2 =
168 28c58de1 xthirioux
  let t1 = repr t1 in
169
  let t2 = repr t2 in
170
  t1==t2 ||
171 695d6f2f xthirioux
  match t1.tdesc, t2.tdesc with
172 66359a5e ploc
  | Tbasic t1, Tbasic t2 when t1 == t2 -> true
173 695d6f2f xthirioux
  | Tenum tl, Tenum tl' when tl == tl' -> true
174
  | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
175
  | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
176
  | (Tconst t, _) ->
177
    let def_t = get_type_definition t in
178
    eq_ground def_t t2
179
  | (_, Tconst t)  ->
180
    let def_t = get_type_definition t in
181
    eq_ground t1 def_t
182
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
183 6afa892a xthirioux
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
184 695d6f2f xthirioux
  | Tstatic (e1, t1'), Tstatic (e2, t2')
185
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
186
  | _ -> false
187
188 6afa892a xthirioux
(** [unify t1 t2] unifies types [t1] and [t2]
189
    using standard destructive unification.
190
    Raises [Unify (t1,t2)] if the types are not unifiable.
191
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
192
    so in case of unification error: expected type [t1], got type [t2].
193
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
194
    If [semi] unification is required,
195
    [t1] should furthermore be an instance of [t2]
196
    and constants are handled differently.*)
197
let unify ?(sub=false) ?(semi=false) t1 t2 =
198
  let rec unif t1 t2 =
199
    let t1 = repr t1 in
200
    let t2 = repr t2 in
201 8a183477 xthirioux
    if t1==t2 then
202 6afa892a xthirioux
      ()
203
    else
204
      match t1.tdesc,t2.tdesc with
205
      (* strictly subtyping cases first *)
206
      | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
207
	unif t1 t2
208
      | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
209
	unif t1 t2
210
      (* This case is not mandatory but will keep "older" types *)
211
      | Tvar, Tvar ->
212 22fe1c93 ploc
        if t1.tid < t2.tid then
213
          t2.tdesc <- Tlink t1
214
        else
215
          t1.tdesc <- Tlink t2
216 6afa892a xthirioux
      | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
217 22fe1c93 ploc
        t1.tdesc <- Tlink t2
218 6afa892a xthirioux
      | _, Tvar when (not (occurs t2 t1)) ->
219 7a47b44f xthirioux
        t2.tdesc <- Tlink t1
220 6afa892a xthirioux
      | Tarrow (t1,t2), Tarrow (t1',t2') ->
221
	begin
222
          unif t2 t2';
223
	  unif t1' t1
224
	end
225
      | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
226
	List.iter2 unif tl tl'
227
      | Ttuple [t1]        , _                  -> unif t1 t2
228
      | _                  , Ttuple [t2]        -> unif t1 t2
229
      | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
230
	List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
231
      | Tclock _, Tstatic _
232
      | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
233
      | Tclock t1', Tclock t2' -> unif t1' t2'
234 66359a5e ploc
      | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
235 6afa892a xthirioux
      | Tunivar, _ | _, Tunivar -> ()
236
      | (Tconst t, _) ->
237
	let def_t = get_type_definition t in
238
	unif def_t t2
239
      | (_, Tconst t)  ->
240
	let def_t = get_type_definition t in
241
	unif t1 def_t
242
      | Tenum tl, Tenum tl' when tl == tl' -> ()
243
      | Tstatic (e1, t1'), Tstatic (e2, t2')
244
      | Tarray (e1, t1'), Tarray (e2, t2') ->
245
	let eval_const =
246
	  if semi
247
	  then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
248
	  else (fun c -> None) in
249
	begin
250
	  unif t1' t2';
251
	  Dimension.eval Basic_library.eval_env eval_const e1;
252
	  Dimension.eval Basic_library.eval_env eval_const e2;
253
	  Dimension.unify ~semi:semi e1 e2;
254
	end
255 66359a5e ploc
      (* Special cases for machine_types. Rules to unify static types infered
256
      	 for numerical constants with non static ones for variables with
257
      	 possible machine types *)
258
      | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
259 6afa892a xthirioux
      | _,_ -> raise (Unify (t1, t2))
260
  in unif t1 t2
261 7a47b44f xthirioux
262 12af4908 xthirioux
(* Expected type ty1, got type ty2 *)
263 6afa892a xthirioux
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
264 7291cb80 xthirioux
  try
265 6afa892a xthirioux
    unify ~sub:sub ~semi:semi ty1 ty2
266 7291cb80 xthirioux
  with
267
  | Unify _ ->
268
    raise (Error (loc, Type_clash (ty1,ty2)))
269
  | Dimension.Unify _ ->
270
    raise (Error (loc, Type_clash (ty1,ty2)))
271
272 66359a5e ploc
let rec type_struct_const_field ?(is_annot=false) loc (label, c) =
273 12af4908 xthirioux
  if Hashtbl.mem field_table label
274 ef34b4ae xthirioux
  then let tydef = Hashtbl.find field_table label in
275
       let tydec = (typedef_of_top tydef).tydef_desc in 
276 12af4908 xthirioux
       let tydec_struct = get_struct_type_fields tydec in
277
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
278
       begin
279 66359a5e ploc
	 try_unify ty_label (type_const ~is_annot loc c) loc;
280 12af4908 xthirioux
	 type_coretype (fun d -> ()) tydec
281
       end
282
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
283
284 66359a5e ploc
and type_const ?(is_annot=false) loc c = 
285 22fe1c93 ploc
  match c with
286 66359a5e ploc
  | Const_int _     -> (* Type_predef. *)type_int
287
  | Const_real _    -> (* Type_predef. *)type_real
288 04a63d25 xthirioux
  (* | Const_float _   -> Type_predef.type_real *)
289 12af4908 xthirioux
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
290 22fe1c93 ploc
		      let ty = new_var () in
291 66359a5e ploc
		      List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
292
		      (* Type_predef. *)type_array d ty
293 12af4908 xthirioux
  | Const_tag t     ->
294 22fe1c93 ploc
    if Hashtbl.mem tag_table t
295 ef34b4ae xthirioux
    then 
296
      let tydef = typedef_of_top (Hashtbl.find tag_table t) in
297
      let tydec =
298
	if is_user_type tydef.tydef_desc
299
	then Tydec_const tydef.tydef_id
300
	else tydef.tydef_desc in
301
      type_coretype (fun d -> ()) tydec
302 22fe1c93 ploc
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
303 12af4908 xthirioux
  | Const_struct fl ->
304
    let ty_struct = new_var () in
305
    begin
306 21485807 xthirioux
      let used =
307
	List.fold_left
308
	  (fun acc (l, c) ->
309
	    if List.mem l acc
310
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
311 66359a5e ploc
	    else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)
312 21485807 xthirioux
	  [] fl in
313
      try
314
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
315
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
316
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
317
	let undef = List.find (fun l -> not (List.mem l used)) total
318
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
319
      with Not_found -> 
320
	ty_struct
321 12af4908 xthirioux
    end
322 66359a5e ploc
  | Const_string _ -> if is_annot then (* Type_predef. *)type_string else  assert false (* string should only appear in annotations *)
323 22fe1c93 ploc
324
(* The following typing functions take as parameter an environment [env]
325
   and whether the element being typed is expected to be constant [const]. 
326
   [env] is a pair composed of:
327
  - a map from ident to type, associating to each ident, i.e. 
328
    variables, constants and (imported) nodes, its type including whether
329
    it is constant or not. This latter information helps in checking constant 
330
    propagation policy in Lustre.
331
  - a vdecl list, in order to modify types of declared variables that are
332
    later discovered to be clocks during the typing process.
333
*)
334
let check_constant loc const_expected const_real =
335
  if const_expected && not const_real
336
  then raise (Error (loc, Not_a_constant))
337
338 a38c681e xthirioux
let rec type_add_const env const arg targ =
339 ec433d69 xthirioux
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
340 a38c681e xthirioux
  if const
341
  then let d =
342
	 if is_dimension_type targ
343
	 then dimension_of_expr arg
344
	 else Dimension.mkdim_var () in
345 66359a5e ploc
       let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
346 a38c681e xthirioux
       Dimension.eval Basic_library.eval_env eval_const d;
347 66359a5e ploc
       let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
348
       (match (* Types. *)get_static_value targ with
349 a38c681e xthirioux
       | None    -> ()
350
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
351
       real_static_type
352
  else targ
353 22fe1c93 ploc
354
(* emulates a subtyping relation between types t and (d : t),
355 4a840259 xthirioux
   used during node applications and assignments *)
356 22fe1c93 ploc
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
357
  let loc = real_arg.expr_loc in
358 66359a5e ploc
  let const = const || ((* Types. *)get_static_value formal_type <> None) in
359 a38c681e xthirioux
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
360 52cfee34 xthirioux
  (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
361 6afa892a xthirioux
  try_unify ~sub:sub formal_type real_type loc
362 52cfee34 xthirioux
363 22fe1c93 ploc
(* typing an application implies:
364
   - checking that const formal parameters match real const (maybe symbolic) arguments
365
   - checking type adequation between formal and real arguments
366 b616fe7a xthirioux
   An application may embed an homomorphic/internal function, in which case we need to split
367
   it in many calls
368 22fe1c93 ploc
*)
369
and type_appl env in_main loc const f args =
370 a38c681e xthirioux
  let targs = List.map (type_expr env in_main const) args in
371 04a63d25 xthirioux
  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
372 b616fe7a xthirioux
  then
373
    try
374 a38c681e xthirioux
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
375 66359a5e ploc
      (* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
376
    with 
377 b616fe7a xthirioux
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
378 66359a5e ploc
	
379
  else (
380 a38c681e xthirioux
    type_dependent_call env in_main loc const f (List.combine args targs)
381 66359a5e ploc
  )
382 b616fe7a xthirioux
383 a38c681e xthirioux
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
384
and type_dependent_call env in_main loc const f targs =
385 66359a5e ploc
(* Format.eprintf "Typing.type_dependent_call %s@." f; *)
386 719f9992 xthirioux
  let tins, touts = new_var (), new_var () in
387 66359a5e ploc
  (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
388
  let tfun = (* Type_predef. *)type_arrow tins touts in
389
  (* Format.eprintf "fun=%a@." print_ty tfun; *)
390 719f9992 xthirioux
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
391 66359a5e ploc
  (* Format.eprintf "type subtyping@."; *)
392 22fe1c93 ploc
  let tins = type_list_of_type tins in
393 a38c681e xthirioux
  if List.length targs <> List.length tins then
394
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
395 54ae8ac7 ploc
  else
396 a38c681e xthirioux
    begin
397 66359a5e ploc
      List.iter2 (
398
	fun (a,t) ti ->
399
	  let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
400
	  (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
401
	  try_unify ~sub:true ti t' a.expr_loc;
402
	  (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
403
	    
404
      )
405
	targs
406
	tins;
407 53206908 xthirioux
      touts
408 a38c681e xthirioux
    end
409
410
(* type a simple call without dependent types 
411
   but possible homomorphic extension.
412
   [targs] is here a list of arguments' types. *)
413
and type_simple_call env in_main loc const f targs =
414
  let tins, touts = new_var (), new_var () in
415 66359a5e ploc
  let tfun = (* Type_predef. *)type_arrow tins touts in
416 a38c681e xthirioux
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
417
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
418
  try_unify ~sub:true tins (type_of_type_list targs) loc;
419 22fe1c93 ploc
  touts
420
421
(** [type_expr env in_main expr] types expression [expr] in environment
422
    [env], expecting it to be [const] or not. *)
423 66359a5e ploc
and type_expr ?(is_annot=false) env in_main const expr =
424 b616fe7a xthirioux
  let resulting_ty = 
425 22fe1c93 ploc
  match expr.expr_desc with
426
  | Expr_const c ->
427 66359a5e ploc
    let ty = type_const ~is_annot expr.expr_loc c in
428
    let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in
429
    expr.expr_type <- Expr_type_hub.export ty;
430 22fe1c93 ploc
    ty
431
  | Expr_ident v ->
432
    let tyv =
433
      try
434
        Env.lookup_value (fst env) v
435
      with Not_found ->
436 66359a5e ploc
	Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;
437 22fe1c93 ploc
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
438
    in
439
    let ty = instantiate (ref []) (ref []) tyv in
440
    let ty' =
441
      if const
442 66359a5e ploc
      then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())
443 22fe1c93 ploc
      else new_var () in
444
    try_unify ty ty' expr.expr_loc;
445 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export ty;
446 22fe1c93 ploc
    ty 
447
  | Expr_array elist ->
448 a38c681e xthirioux
    let ty_elt = new_var () in
449
    List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
450 22fe1c93 ploc
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
451 66359a5e ploc
    let ty = (* Type_predef. *)type_array d ty_elt in
452
    expr.expr_type <- Expr_type_hub.export ty;
453 22fe1c93 ploc
    ty
454
  | Expr_access (e1, d) ->
455 66359a5e ploc
    type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;
456 22fe1c93 ploc
    let ty_elt = new_var () in
457
    let d = Dimension.mkdim_var () in
458 66359a5e ploc
    type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt);
459
    expr.expr_type <- Expr_type_hub.export ty_elt;
460 22fe1c93 ploc
    ty_elt
461
  | Expr_power (e1, d) ->
462 66359a5e ploc
    let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
463
    type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
464 22fe1c93 ploc
    Dimension.eval Basic_library.eval_env eval_const d;
465 a38c681e xthirioux
    let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
466 66359a5e ploc
    let ty = (* Type_predef. *)type_array d ty_elt in
467
    expr.expr_type <- Expr_type_hub.export ty;
468 22fe1c93 ploc
    ty
469
  | Expr_tuple elist ->
470 66359a5e ploc
    let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in
471
    expr.expr_type <- Expr_type_hub.export ty;
472 22fe1c93 ploc
    ty
473
  | Expr_ite (c, t, e) ->
474 66359a5e ploc
    type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;
475 a38c681e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
476 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export ty;
477 22fe1c93 ploc
    ty
478
  | Expr_appl (id, args, r) ->
479 5c1184ad ploc
    (* application of non internal function is not legal in a constant
480
       expression *)
481 22fe1c93 ploc
    (match r with
482
    | None        -> ()
483 54d032f5 xthirioux
    | Some c -> 
484
      check_constant expr.expr_loc const false;	
485 66359a5e ploc
      type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);
486 d7b73fed xthirioux
    let args_list = expr_list_of_expr args in
487 66359a5e ploc
    let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in
488
    args.expr_type <- Expr_type_hub.export targs;
489 d7b73fed xthirioux
    let touts = type_appl env in_main expr.expr_loc const id args_list in
490 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export touts;
491 22fe1c93 ploc
    touts
492
  | Expr_fby (e1,e2)
493
  | Expr_arrow (e1,e2) ->
494
    (* fby/arrow is not legal in a constant expression *)
495
    check_constant expr.expr_loc const false;
496 a38c681e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
497 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export ty;
498 22fe1c93 ploc
    ty
499
  | Expr_pre e ->
500
    (* pre is not legal in a constant expression *)
501
    check_constant expr.expr_loc const false;
502 a38c681e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
503 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export ty;
504 22fe1c93 ploc
    ty
505
  | Expr_when (e1,c,l) ->
506
    (* when is not legal in a constant expression *)
507
    check_constant expr.expr_loc const false;
508 66359a5e ploc
    let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in
509 22fe1c93 ploc
    let expr_c = expr_of_ident c expr.expr_loc in
510
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
511 a38c681e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
512 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export ty;
513 22fe1c93 ploc
    ty
514
  | Expr_merge (c,hl) ->
515
    (* merge is not legal in a constant expression *)
516
    check_constant expr.expr_loc const false;
517
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
518
    let expr_c = expr_of_ident c expr.expr_loc in
519 66359a5e ploc
    let typ_l = (* Type_predef. *)type_clock typ_in in
520 22fe1c93 ploc
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
521 66359a5e ploc
    expr.expr_type <- Expr_type_hub.export typ_out;
522 22fe1c93 ploc
    typ_out
523 b616fe7a xthirioux
  in 
524 66359a5e ploc
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
525 b616fe7a xthirioux
  resulting_ty
526 22fe1c93 ploc
527 66359a5e ploc
and type_branches ?(is_annot=false) env in_main loc const hl =
528 22fe1c93 ploc
  let typ_in = new_var () in
529
  let typ_out = new_var () in
530
  try
531
    let used_labels =
532
      List.fold_left (fun accu (t, h) ->
533 66359a5e ploc
	unify typ_in (type_const ~is_annot loc (Const_tag t));
534 22fe1c93 ploc
	type_subtyping_arg env in_main const h typ_out;
535
	if List.mem t accu
536
	then raise (Error (loc, Already_bound t))
537
	else t :: accu) [] hl in
538
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
539
    if List.sort compare used_labels <> List.sort compare type_labels
540
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
541
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
542
    else (typ_in, typ_out)
543
  with Unify (t1, t2) ->
544
    raise (Error (loc, Type_clash (t1,t2)))
545 a38c681e xthirioux
546 22fe1c93 ploc
(** [type_eq env eq] types equation [eq] in environment [env] *)
547
let type_eq env in_main undefined_vars eq =
548 ec433d69 xthirioux
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
549 22fe1c93 ploc
  (* Check undefined variables, type lhs *)
550
  let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
551
  let ty_lhs = type_expr env in_main false expr_lhs in
552
  (* Check multiple variable definitions *)
553
  let define_var id uvars =
554 ec433d69 xthirioux
    if ISet.mem id uvars
555
    then ISet.remove id uvars
556
    else raise (Error (eq.eq_loc, Already_defined id))
557 22fe1c93 ploc
  in
558 6afa892a xthirioux
  (* check assignment of declared constant, assignment of clock *)
559
  let ty_lhs =
560
    type_of_type_list
561
      (List.map2 (fun ty id ->
562
	if get_static_value ty <> None
563
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
564
	match get_clock_base_type ty with
565
	| None -> ty
566
	| Some ty -> ty)
567
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
568 22fe1c93 ploc
  let undefined_vars =
569
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
570
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
571
     to a (always non-constant) lhs variable *)
572 11242500 xthirioux
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
573 22fe1c93 ploc
  undefined_vars
574
575
576
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
577
   in environment [env] *)
578
let type_coreclock env ck id loc =
579
  match ck.ck_dec_desc with
580 45f0f48d xthirioux
  | Ckdec_any -> ()
581 22fe1c93 ploc
  | Ckdec_bool cl ->
582
      let dummy_id_expr = expr_of_ident id loc in
583
      let when_expr =
584
        List.fold_left
585
          (fun expr (x, l) ->
586
                {expr_tag = new_tag ();
587
                 expr_desc= Expr_when (expr,x,l);
588 66359a5e ploc
                 expr_type = Types.Main.new_var ();
589 22fe1c93 ploc
                 expr_clock = Clocks.new_var true;
590
                 expr_delay = Delay.new_var ();
591
                 expr_loc=loc;
592
		 expr_annot = None})
593
          dummy_id_expr cl
594
      in
595
      ignore (type_expr env false false when_expr)
596
597
let rec check_type_declaration loc cty =
598
 match cty with
599
 | Tydec_clock ty
600
 | Tydec_array (_, ty) -> check_type_declaration loc ty
601
 | Tydec_const tname   ->
602 3c3414c5 ploc
    (* Format.eprintf "TABLE: %a@." print_type_table (); *)
603
    if not (Hashtbl.mem type_table cty)
604
    then raise (Error (loc, Unbound_type tname));
605 22fe1c93 ploc
 | _                   -> ()
606
607
let type_var_decl vd_env env vdecl =
608 ec433d69 xthirioux
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
609 22fe1c93 ploc
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
610 66359a5e ploc
  let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
611 22fe1c93 ploc
  let type_dim d =
612
    begin
613 66359a5e ploc
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
614 22fe1c93 ploc
      Dimension.eval Basic_library.eval_env eval_const d;
615
    end in
616
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
617 ec433d69 xthirioux
618
  let ty_static =
619 22fe1c93 ploc
    if vdecl.var_dec_const
620 66359a5e ploc
    then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
621 22fe1c93 ploc
    else ty in
622 ec433d69 xthirioux
  (match vdecl.var_dec_value with
623
  | None   -> ()
624
  | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
625 66359a5e ploc
  try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
626 ec433d69 xthirioux
  let new_env = Env.add_value env vdecl.var_id ty_static in
627 22fe1c93 ploc
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
628 ec433d69 xthirioux
(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
629 22fe1c93 ploc
  new_env
630
631
let type_var_decl_list vd_env env l =
632
  List.fold_left (type_var_decl vd_env) env l
633
634
let type_of_vlist vars =
635 66359a5e ploc
  let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
636 22fe1c93 ploc
  type_of_type_list tyl
637
638
let add_vdecl vd_env vdecl =
639
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
640
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
641
 else vdecl::vd_env
642
643
let check_vd_env vd_env =
644
  ignore (List.fold_left add_vdecl [] vd_env)
645
646
(** [type_node env nd loc] types node [nd] in environment env. The
647
    location is used for error reports. *)
648
let type_node env nd loc =
649
  let is_main = nd.node_id = !Options.main_node in
650
  let vd_env_ol = nd.node_outputs@nd.node_locals in
651
  let vd_env =  nd.node_inputs@vd_env_ol in
652
  check_vd_env vd_env;
653
  let init_env = env in
654
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
655
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
656
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
657
  let new_env = Env.overwrite env delta_env in
658
  let undefined_vars_init =
659
    List.fold_left
660 ec433d69 xthirioux
      (fun uvs v -> ISet.add v.var_id uvs)
661
      ISet.empty vd_env_ol in
662 22fe1c93 ploc
  let undefined_vars =
663 333e3a25 ploc
    let eqs, auts = get_node_eqs nd in
664
    (* TODO XXX: il faut typer les handlers de l'automate *)
665
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
666 22fe1c93 ploc
  in
667 af5af1e8 ploc
  (* Typing asserts *)
668
  List.iter (fun assert_ ->
669
    let assert_expr =  assert_.assert_expr in
670 66359a5e ploc
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
671 af5af1e8 ploc
  )  nd.node_asserts;
672 66359a5e ploc
  (* Typing annots *)
673
  List.iter (fun annot ->
674
    List.iter (fun (_, eexpr) -> ignore (type_expr ~is_annot:true (new_env, vd_env) false false eexpr.eexpr_qfexpr)) annot.annots
675
  ) nd.node_annot;
676 af5af1e8 ploc
  
677 22fe1c93 ploc
  (* check that table is empty *)
678 ec433d69 xthirioux
  let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
679
  let undefined_vars = ISet.diff undefined_vars local_consts in
680
  if (not (ISet.is_empty undefined_vars)) then
681 22fe1c93 ploc
    raise (Error (loc, Undefined_var undefined_vars));
682
  let ty_ins = type_of_vlist nd.node_inputs in
683
  let ty_outs = type_of_vlist nd.node_outputs in
684
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
685
  generalize ty_node;
686
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
687 66359a5e ploc
  nd.node_type <- Expr_type_hub.export ty_node;
688 22fe1c93 ploc
  Env.add_value env nd.node_id ty_node
689
690
let type_imported_node env nd loc =
691
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
692
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
693
  check_vd_env vd_env;
694
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
695
  let ty_ins = type_of_vlist nd.nodei_inputs in
696
  let ty_outs = type_of_vlist nd.nodei_outputs in
697
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
698
  generalize ty_node;
699
(*
700
  if (is_polymorphic ty_node) then
701
    raise (Error (loc, Poly_imported_node nd.nodei_id));
702
*)
703
  let new_env = Env.add_value env nd.nodei_id ty_node in
704 66359a5e ploc
  nd.nodei_type <- Expr_type_hub.export ty_node;
705 22fe1c93 ploc
  new_env
706
707 ef34b4ae xthirioux
let type_top_const env cdecl =
708
  let ty = type_const cdecl.const_loc cdecl.const_value in
709
  let d =
710
    if is_dimension_type ty
711
    then dimension_of_const cdecl.const_loc cdecl.const_value
712
    else Dimension.mkdim_var () in
713 66359a5e ploc
  let ty = (* Type_predef. *)type_static d ty in
714 ef34b4ae xthirioux
  let new_env = Env.add_value env cdecl.const_id ty in
715 66359a5e ploc
  cdecl.const_type <- Expr_type_hub.export ty;
716 ef34b4ae xthirioux
  new_env
717
718 22fe1c93 ploc
let type_top_consts env clist =
719 ef34b4ae xthirioux
  List.fold_left type_top_const env clist
720
721
let rec type_top_decl env decl =
722 22fe1c93 ploc
  match decl.top_decl_desc with
723 e2380d4d ploc
  | Node nd -> (
724 53206908 xthirioux
    try
725
      type_node env nd decl.top_decl_loc
726
    with Error (loc, err) as exc -> (
727
      if !Options.global_inline then
728
	Format.eprintf "Type error: failing node@.%a@.@?"
729
	  Printers.pp_node nd
730
      ;
731
      raise exc)
732 e2380d4d ploc
  )
733 22fe1c93 ploc
  | ImportedNode nd ->
734 53206908 xthirioux
    type_imported_node env nd decl.top_decl_loc
735 ef34b4ae xthirioux
  | Const c ->
736 53206908 xthirioux
    type_top_const env c
737 ef34b4ae xthirioux
  | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
738 5c1184ad ploc
  | Open _  -> env
739 22fe1c93 ploc
740 d7b73fed xthirioux
let get_type_of_call decl =
741
  match decl.top_decl_desc with
742
  | Node nd         ->
743 66359a5e ploc
    let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
744 d7b73fed xthirioux
    type_list_of_type in_typ, type_list_of_type out_typ
745
  | ImportedNode nd ->
746 66359a5e ploc
    let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
747 d7b73fed xthirioux
    type_list_of_type in_typ, type_list_of_type out_typ
748
  | _               -> assert false
749
750 22fe1c93 ploc
let type_prog env decls =
751
try
752 5c1184ad ploc
  List.fold_left type_top_decl env decls
753 22fe1c93 ploc
with Failure _ as exc -> raise exc
754
755
(* Once the Lustre program is fully typed,
756
   we must get back to the original description of dimensions,
757
   with constant parameters, instead of unifiable internal variables. *)
758
759
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
760
   i.e. replacing unifiable second_order variables with the original static parameters.
761
   Once restored in this formulation, dimensions may be meaningfully printed.
762
*)
763
let uneval_vdecl_generics vdecl =
764
 if vdecl.var_dec_const
765
 then
766 66359a5e ploc
   match get_static_value (Expr_type_hub.import vdecl.var_type) with
767
   | None   -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
768 22fe1c93 ploc
   | Some d -> Dimension.uneval vdecl.var_id d
769
770
let uneval_node_generics vdecls =
771
  List.iter uneval_vdecl_generics vdecls
772
773
let uneval_top_generics decl =
774
  match decl.top_decl_desc with
775
  | Node nd ->
776
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
777
  | ImportedNode nd ->
778
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
779 ef34b4ae xthirioux
  | Const _
780
  | TypeDef _
781 5c1184ad ploc
  | Open _  -> ()
782 22fe1c93 ploc
783
let uneval_prog_generics prog =
784
 List.iter uneval_top_generics prog
785 5c1184ad ploc
786 ef34b4ae xthirioux
let rec get_imported_symbol decls id =
787 96f5fe18 xthirioux
  match decls with
788
  | [] -> assert false
789
  | decl::q ->
790
     (match decl.top_decl_desc with
791 ef34b4ae xthirioux
      | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
792
      | Const c when id = c.const_id && decl.top_decl_itf -> decl
793
      | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
794
      | _ -> get_imported_symbol q id)
795 96f5fe18 xthirioux
796 8f1c7e91 xthirioux
let check_env_compat header declared computed = 
797
  uneval_prog_generics header;
798 ef34b4ae xthirioux
  Env.iter declared (fun k decl_type_k ->
799
    let loc = (get_imported_symbol header k).top_decl_loc in 
800
    let computed_t =
801
      instantiate (ref []) (ref []) 
802
	(try Env.lookup_value computed k
803
	 with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
804 7291cb80 xthirioux
    (*Types.print_ty Format.std_formatter decl_type_k;
805 ef34b4ae xthirioux
      Types.print_ty Format.std_formatter computed_t;*)
806
    try_unify ~sub:true ~semi:true decl_type_k computed_t loc
807
  )
808
809 b1655a21 xthirioux
let check_typedef_top decl =
810 ef34b4ae xthirioux
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
811 6efbcb73 xthirioux
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
812 ef34b4ae xthirioux
(*Format.eprintf "%a" Corelang.print_type_table ();*)
813 b1655a21 xthirioux
  match decl.top_decl_desc with
814 ef34b4ae xthirioux
  | TypeDef ty ->
815
     let owner = decl.top_decl_owner in
816
     let itf = decl.top_decl_itf in
817
     let decl' =
818
       try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
819
       with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
820
     let owner' = decl'.top_decl_owner in
821 6efbcb73 xthirioux
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
822 ef34b4ae xthirioux
     let itf' = decl'.top_decl_itf in
823
     (match decl'.top_decl_desc with
824
     | Const _ | Node _ | ImportedNode _ -> assert false
825
     | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
826
     | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
827 b1655a21 xthirioux
  | _  -> ()
828
829
let check_typedef_compat header =
830
  List.iter check_typedef_top header
831 66359a5e ploc
end
832 5c1184ad ploc
833 66359a5e ploc
include  Make(Types.Main) (struct
834
  type type_expr  = Types.Main.type_expr
835
  let import x = x
836
  let export x = x
837
end)
838 22fe1c93 ploc
(* Local Variables: *)
839
(* compile-command:"make -C .." *)
840
(* End: *)