Added a unit type. Tunit.

This commit is contained in:
Léonard Gérard 2010-11-23 17:10:11 +01:00
parent ed2642f847
commit 9998d7ea39
11 changed files with 39 additions and 20 deletions

View File

@ -28,6 +28,8 @@ and link =
exception Unify exception Unify
let invalid_clock = Cprod []
let index = ref 0 let index = ref 0
@ -53,18 +55,8 @@ let rec occur_check index ck =
| Con (ck, _, _) -> occur_check index ck | Con (ck, _, _) -> occur_check index ck
| _ -> raise Unify | _ -> raise Unify
(** unify ck *)
let rec unify t1 t2 = let rec unify_ck ck1 ck2 =
if t1 == t2
then ()
else
(match (t1, t2) with
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod ct_list1, Cprod ct_list2) ->
(try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify)
| _ -> raise Unify)
and unify_ck ck1 ck2 =
let ck1 = ck_repr ck1 in let ck1 = ck_repr ck1 in
let ck2 = ck_repr ck2 in let ck2 = ck_repr ck2 in
if ck1 == ck2 if ck1 == ck2
@ -82,22 +74,27 @@ and unify_ck ck1 ck2 =
unify_ck ck1 ck2 unify_ck ck1 ck2
| _ -> raise Unify) | _ -> raise Unify)
(** unify ct *)
let rec unify t1 t2 = let rec unify t1 t2 =
if t1 == t2 then () else
match (t1, t2) with match (t1, t2) with
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2 | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list | (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
| _ -> raise Unify | _ -> raise Unify
and unify_list t1_list t2_list = and unify_list t1_list t2_list =
try List.iter2 unify t1_list t2_list with | _ -> raise Unify try List.iter2 unify t1_list t2_list
with _ -> raise Unify
let rec skeleton ck = function let rec skeleton ck = function
| Tprod ty_list -> | Tprod ty_list ->
(match ty_list with (match ty_list with
| [] -> Format.eprintf "Warning, an exp with void type@."; Ck ck | [] ->
Format.eprintf "Internal error, an exp with invalid type@.";
assert false;
| _ -> Cprod (List.map (skeleton ck) ty_list)) | _ -> Cprod (List.map (skeleton ck) ty_list))
| Tarray _ | Tid _ -> Ck ck | Tarray _ | Tid _ | Tunit -> Ck ck
(* TODO here it implicitely says that the base clock is Cbase (* TODO here it implicitely says that the base clock is Cbase
and that all tuple is on Cbase *) and that all tuple is on Cbase *)

View File

@ -102,3 +102,5 @@ and type_compare ty1 ty2 = match ty1, ty2 with
if cr <> 0 then cr else static_exp_compare se1 se2 if cr <> 0 then cr else static_exp_compare se1 se2
| (Tprod _ | Tid _), _ -> 1 | (Tprod _ | Tid _), _ -> 1
| (Tarray _), _ -> -1 | (Tarray _), _ -> -1
| Tunit, Tunit -> 0
| Tunit, _ -> -1

View File

@ -59,6 +59,7 @@ and ty funs acc t = match t with
let t, acc = ty_it funs acc t in let t, acc = ty_it funs acc t in
let se, acc = static_exp_it funs acc se in let se, acc = static_exp_it funs acc se in
Tarray (t, se), acc Tarray (t, se), acc
| Tunit -> t, acc
(* (*
and ct_it funs acc c = try funs.ct funs acc c with Fallback -> ct funs acc t and ct_it funs acc c = try funs.ct funs acc c with Fallback -> ct funs acc t
and ct funs acc c = match c with and ct funs acc c = match c with

View File

@ -48,6 +48,7 @@ and print_type ff = function
| Tid id -> print_qualname ff id | Tid id -> print_qualname ff id
| Tarray (ty, n) -> | Tarray (ty, n) ->
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_static_exp n fprintf ff "@[<hov2>%a^%a@]" print_type ty print_static_exp n
| Tunit -> fprintf ff "()"
let print_field ff field = let print_field ff field =
fprintf ff "@[%a: %a@]" print_qualname field.f_name print_type field.f_type fprintf ff "@[%a: %a@]" print_qualname field.f_name print_type field.f_type

View File

@ -262,6 +262,7 @@ let rec unalias_type t = match t with
with Not_found -> raise (Undefined_type ty_name)) with Not_found -> raise (Undefined_type ty_name))
| Tarray (ty, n) -> Tarray(unalias_type ty, n) | Tarray (ty, n) -> Tarray(unalias_type ty, n)
| Tprod ty_list -> Tprod (List.map unalias_type ty_list) | Tprod ty_list -> Tprod (List.map unalias_type ty_list)
| Tunit -> Tunit
(** Return the current module as a [module_object] *) (** Return the current module as a [module_object] *)

View File

@ -26,7 +26,11 @@ and static_exp_desc =
| Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *) | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *)
| Sop of fun_name * static_exp list (** defined ops for now in pervasives *) | Sop of fun_name * static_exp list (** defined ops for now in pervasives *)
and ty = | Tprod of ty list | Tid of type_name | Tarray of ty * static_exp and ty =
| Tprod of ty list
| Tid of type_name
| Tarray of ty * static_exp
| Tunit
let invalid_type = Tprod [] let invalid_type = Tprod []

View File

@ -384,6 +384,7 @@ let rec check_type const_env = function
| Tid ty_name -> Tid ty_name | Tid ty_name -> Tid ty_name
| Tprod l -> | Tprod l ->
Tprod (List.map (check_type const_env) l) Tprod (List.map (check_type const_env) l)
| Tunit -> Tunit
and typing_static_exp const_env se = and typing_static_exp const_env se =
try try

View File

@ -398,7 +398,8 @@ let rec reconstruct input_type (env : PatEnv.t) =
| Evarpat ident, _ -> mk_var_dec ident ty :: var_list | Evarpat ident, _ -> mk_var_dec ident ty :: var_list
| Etuplepat pat_list, Tprod ty_list -> | Etuplepat pat_list, Tprod ty_list ->
List.fold_right2 mk_var_decs pat_list ty_list var_list List.fold_right2 mk_var_decs pat_list ty_list var_list
| Etuplepat _, (Tarray _ | Tid _) -> assert false (* ill-typed *) in | Etuplepat [], Tunit -> var_list
| Etuplepat _, (Tarray _ | Tid _ | Tunit) -> assert false (* ill-typed *) in
let add_to_lists pat (_, head, children) (eq_list, var_list) = let add_to_lists pat (_, head, children) (eq_list, var_list) =
(* Remember the encoding of resets given above. *) (* Remember the encoding of resets given above. *)

View File

@ -102,6 +102,7 @@ let rec ctype_of_otype oty =
| Tarray(ty, n) -> Cty_arr(int_of_static_exp n, | Tarray(ty, n) -> Cty_arr(int_of_static_exp n,
ctype_of_otype ty) ctype_of_otype ty)
| Tprod _ -> assert false | Tprod _ -> assert false
| Tunit -> assert false
let cvarlist_of_ovarlist vl = let cvarlist_of_ovarlist vl =
let cvar_of_ovar vd = let cvar_of_ovar vd =

View File

@ -84,7 +84,7 @@ let assert_node_res cd =
(* TODO: refactor into something more readable. *) (* TODO: refactor into something more readable. *)
let main_def_of_class_def cd = let main_def_of_class_def cd =
let format_for_type ty = match ty with let format_for_type ty = match ty with
| Tarray _ | Tprod _ -> assert false | Tarray _ | Tprod _ | Tunit -> assert false
| Types.Tid id when id = Initial.pfloat -> "%f" | Types.Tid id when id = Initial.pfloat -> "%f"
| Types.Tid id when id = Initial.pint -> "%d" | Types.Tid id when id = Initial.pint -> "%d"
| Types.Tid id when id = Initial.pbool -> "%d" | Types.Tid id when id = Initial.pbool -> "%d"
@ -93,7 +93,7 @@ let main_def_of_class_def cd =
(** Does reading type [ty] need a buffer? When it is the case, (** Does reading type [ty] need a buffer? When it is the case,
[need_buf_for_ty] also returns the type's name. *) [need_buf_for_ty] also returns the type's name. *)
let need_buf_for_ty ty = match ty with let need_buf_for_ty ty = match ty with
| Tarray _ | Tprod _ -> assert false | Tarray _ | Tprod _ | Tunit -> assert false
| Types.Tid id when id = Initial.pfloat -> None | Types.Tid id when id = Initial.pfloat -> None
| Types.Tid id when id = Initial.pint -> None | Types.Tid id when id = Initial.pint -> None
| Types.Tid id when id = Initial.pbool -> None | Types.Tid id when id = Initial.pbool -> None

10
todo.txt Normal file
View File

@ -0,0 +1,10 @@
Plus ou moins ordonné du plus urgent au moins urgent.
*- (LG) Faire la passe de transformation des switchs dans heptagon avant le reset et ainsi simplifier le reset.
*- (LG) Rajouter les annotations d'horloge dans le source (les mettres comme contrainte de sous typage en ck_base ?? voir avec lucy-n)
*- Compléter la passe "static.ml" pour gérer l'ensemble des opérateurs de pervasives
*- Optimiser le reset en utilisant un memcopy ?