From e8f55c2552def91dca21de02ad84543b79477bd8 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 14 Nov 2019 15:34:48 -0800
Subject: [PATCH] - tag_true and tag_false moved to lustre_types - real
constants are hidden in Real.ml{i} module
---
src/backends/Ada/ada_backend_common.ml | 5 +-
src/backends/C/c_backend_common.ml | 2 +-
src/backends/C/c_backend_src.ml | 2 +-
src/backends/Horn/horn_backend_printers.ml | 2 +-
src/corelang.ml | 57 +++++++++++++++++-----
src/corelang.mli | 11 ++---
src/lustre_types.ml | 4 +-
src/machine_code.ml | 7 ++-
src/machine_code_common.ml | 6 +--
src/main_lustre_compiler.ml | 4 +-
src/main_lustre_testgen.ml | 2 +-
src/main_lustre_verifier.ml | 6 +--
src/mutation.ml | 4 +-
src/parsers/lexerLustreSpec.mll | 4 +-
src/parsers/lexer_lustre.mll | 4 +-
src/parsers/parser_lustre.mly | 8 +--
src/plugins/salsa/machine_salsa_opt.ml | 6 +--
src/plugins/salsa/salsaDatatypes.ml | 4 +-
src/scheduling.ml | 2 +-
src/types.ml | 4 +-
src/typing.ml | 10 ++--
21 files changed, 93 insertions(+), 61 deletions(-)
diff --git a/src/backends/Ada/ada_backend_common.ml b/src/backends/Ada/ada_backend_common.ml
index 2f506272..34a4b64c 100644
--- a/src/backends/Ada/ada_backend_common.ml
+++ b/src/backends/Ada/ada_backend_common.ml
@@ -124,7 +124,7 @@ let pp_type fmt typ =
**)
let default_ada_cst cst_typ = match cst_typ with
| Types.Basic.Tint -> Const_int 0
- | Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
+ | Types.Basic.Treal -> Const_real Real.zero
| Types.Basic.Tbool -> Const_tag tag_false
| _ -> assert false
@@ -200,8 +200,7 @@ let pp_ada_tag fmt t =
let pp_ada_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real (c, e, s) ->
- fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
+ | Const_real r -> Real.pp_ada fmt r
| Const_tag t -> pp_ada_tag fmt t
| Const_string _ | Const_modeid _ ->
(Format.eprintf
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 45ad445f..2051a65b 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -226,7 +226,7 @@ let pp_c_tag fmt t =
let rec pp_c_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real (c,e,s)-> pp_print_string fmt s (* Format.fprintf fmt "%ie%i" c e*)
+ | Const_real r -> Real.pp fmt r
(* | Const_float r -> pp_print_float fmt r *)
| Const_tag t -> pp_c_tag fmt t
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 04b9d459..fcbf0772 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -130,7 +130,7 @@ let pp_suffix m fmt loop_vars =
let rec pp_c_const_suffix var_type fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real (_, _, s) -> pp_print_string fmt s
+ | Const_real r -> Real.pp fmt r
| Const_tag t -> pp_c_tag fmt t
| Const_array ca -> let var_type = Types.array_element_type var_type in
fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 2ed7093e..f10a9fd1 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -42,7 +42,7 @@ let pp_horn_tag fmt t =
let rec pp_horn_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real (_,_,s) -> pp_print_string fmt s
+ | Const_real r -> Real.pp fmt r
| Const_tag t -> pp_horn_tag fmt t
| _ -> assert false
diff --git a/src/corelang.ml b/src/corelang.ml
index abdb3075..1a9a8174 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -404,8 +404,6 @@ let rec coretype_equal ty1 ty2 =
| _ -> false
in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
-let tag_true = "true"
-let tag_false = "false"
let tag_default = "default"
let const_is_bool c =
@@ -579,17 +577,11 @@ let rec dimension_of_expr expr =
let sort_handlers hl =
List.sort (fun (t, _) (t', _) -> compare t t') hl
-let num_10 = Num.num_of_int 10
-
-let cst_real_to_num n i =
- Num.(n // (num_10 **/ (num_of_int i)))
-
+
let rec is_eq_const c1 c2 =
match c1, c2 with
- | Const_real (n1, i1, _), Const_real (n2, i2, _)
- -> let n1 = cst_real_to_num n1 i1 in
- let n2 = cst_real_to_num n2 i2 in
- Num.eq_num n1 n2
+ | Const_real r1, Const_real r2
+ -> Real.eq r1 r1
| Const_struct lcl1, Const_struct lcl2
-> List.length lcl1 = List.length lcl2
&& List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
@@ -1414,7 +1406,48 @@ let rec add_pre_expr vars e =
let mk_eq l e1 e2 =
mkpredef_call l "=" [e1; e2]
-
+
+
+let rec partial_eval e =
+ let pa = partial_eval in
+ let edesc =
+ match e.expr_desc with
+ | Expr_const _ -> e.expr_desc
+ | Expr_ident id -> e.expr_desc
+ | Expr_ite (g,t,e) -> (
+ let g, t, e = pa g, pa t, pa e in
+ match g.expr_desc with
+ | Expr_const (Const_tag tag) when (tag = tag_true) -> t.expr_desc
+ | Expr_const (Const_tag tag) when (tag = tag_false) -> e.expr_desc
+ | _ -> Expr_ite (g, t, e)
+ )
+ | Expr_tuple t ->
+ Expr_tuple (List.map pa t)
+ | Expr_arrow (e1, e2) ->
+ Expr_arrow (pa e1, pa e2)
+ | Expr_fby (e1, e2) ->
+ Expr_fby (pa e1, pa e2)
+ | Expr_pre e ->
+ Expr_pre (pa e)
+ | Expr_appl (op, args, opt) ->
+ let args = pa args in
+ if Basic_library.is_expr_internal_fun e then
+ Basic_library.partial_eval op args opt
+ else
+ Expr_appl (op, pa e, opt)
+ | Expr_array el ->
+ Expr_array (List.map pa el)
+ | Expr_access (e, d) ->
+ Expr_access (pa e, d)
+ | Expr_power (e, d) ->
+ Expr_power (pa e, d)
+ | Expr_when (e, id, l) ->
+ Expr_when (pa e, id, l)
+ | Expr_merge (id, gl) ->
+ Expr_merge(id, List.map (fun (l, e) -> l, pa e) gl)
+ in
+ { e with expr_desc = edesc }
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/corelang.mli b/src/corelang.mli
index 89f74aa3..93c9c22b 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -70,8 +70,6 @@ val is_clock_dec_type: type_dec_desc -> bool
val get_repr_type: type_dec_desc -> type_dec_desc
val is_user_type: type_dec_desc -> bool
val coretype_equal: type_dec_desc -> type_dec_desc -> bool
-val tag_true: label
-val tag_false: label
val tag_default: label
val tag_table: (label, top_decl) Hashtbl.t
val field_table: (label, top_decl) Hashtbl.t
@@ -190,9 +188,6 @@ val mk_fresh_var: (ident * var_decl list) -> Location.t -> Types.type_expr -> C
val find_eq: ident list -> eq list -> eq * eq list
-(* Extract a num to describe a real constant *)
-val cst_real_to_num: Num.num -> int -> Num.num
-
val get_expr_calls: top_decl list -> expr -> Utils.ISet.t
val eq_has_arrows: eq -> bool
@@ -202,6 +197,10 @@ val push_negations: ?neg:bool -> expr -> expr
val add_pre_expr: ident list -> expr -> expr
val mk_eq: Location.t -> expr -> expr -> expr
-(* Local Variables: *)
+
+(* Simple transformations: eg computation over constants *)
+val partial_eval: expr -> expr
+
+ (* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 7170eefa..1fe5fa5a 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -48,7 +48,7 @@ and clock_dec_desc =
type constant =
| Const_int of int
- | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
+ | Const_real of Real.t
| Const_array of constant list
| Const_tag of label
| Const_string of string (* used only for annotations *)
@@ -254,6 +254,8 @@ type spec_types =
| LocalContract of contract_desc
| TopContract of top_decl list
+let tag_true = "true"
+let tag_false = "false"
(* Local Variables: *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 1887b001..77254ba2 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -465,7 +465,6 @@ let translate_prog decls node_schs =
in
machines
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
+ (* Local Variables: *)
+ (* compile-command:"make -C .." *)
+ (* End: *)
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index ddf396e8..49254523 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -299,7 +299,7 @@ let type_of_value_appl f args =
let rec value_of_dimension m dim =
match dim.Dimension.dim_desc with
| Dimension.Dbool b ->
- mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool
+ mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool
| Dimension.Dint i ->
mk_val (Cst (Const_int i)) Type_predef.type_int
| Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v
@@ -315,8 +315,8 @@ let rec value_of_dimension m dim =
let rec dimension_of_value value =
match value.value_desc with
- | Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true
- | Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false
+ | Cst (Const_tag t) when t = tag_true -> Dimension.mkdim_bool Location.dummy_loc true
+ | Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool Location.dummy_loc false
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i
| Var v -> Dimension.mkdim_ident Location.dummy_loc v.var_id
| Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 9d33a54c..41e645a4 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -80,8 +80,8 @@ let rec compile dirname basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
- let machine_code =
- Compiler_stages.stage2 prog
+ let prog, machine_code =
+ Compiler_stages.stage2 params prog
in
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ " Machine_code_common.pp_machines machine_code);
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 7fe08dbd..52b8746c 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -76,7 +76,7 @@ let testgen_source dirname basename extension =
Options.output := "emf";
let params = Backends.get_normalization_params () in
let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
- let machine_code = Compiler_stages.stage2 prog_mcdc in
+ let prog_mcdc, machine_code = Compiler_stages.stage2 params prog_mcdc in
let source_emf = source_file ^ ".emf" in
let source_out = open_out source_emf in
let fmt = formatter_of_out_channel source_out in
diff --git a/src/main_lustre_verifier.ml b/src/main_lustre_verifier.ml
index e8ba2b75..391a2e6b 100644
--- a/src/main_lustre_verifier.ml
+++ b/src/main_lustre_verifier.ml
@@ -56,12 +56,12 @@ let rec verify dirname basename extension =
let module Verifier = (val verifier : VerifierType.S) in
decr Options.verbose_level;
+ let params = Verifier.get_normalization_params () in
(* Normalizing it *)
let prog, dependencies =
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
try
incr Options.verbose_level;
- let params = Verifier.get_normalization_params () in
decr Options.verbose_level;
Compiler_stages.stage1 params prog dirname basename extension
with Compiler_stages.StopPhase1 prog -> (
@@ -73,8 +73,8 @@ let rec verify dirname basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
- let machine_code =
- Compiler_stages.stage2 prog
+ let prog, machine_code =
+ Compiler_stages.stage2 params prog
in
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
diff --git a/src/mutation.ml b/src/mutation.ml
index 769e2379..4b19fca7 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -188,7 +188,7 @@ let rdm_mutate_real r =
let eshift = 10. ** (float_of_int shift) in
let i = Random.int (1 + bound * (int_of_float eshift)) in
let f = float_of_int i /. eshift in
- (Num.num_of_int i, shift, string_of_float f)
+ Real.create (string_of_int i) shift (string_of_float f)
else
r
@@ -224,7 +224,7 @@ let rdm_mutate_pre orig_expr =
let rdm_mutate_const_value c =
match c with
| Const_int i -> Const_int (rdm_mutate_int i)
- | Const_real (n, i, s) -> let (n', i', s') = rdm_mutate_real (n, i, s) in Const_real (n', i', s')
+ | Const_real r -> Const_real (rdm_mutate_real r)
| Const_array _
| Const_string _
| Const_modeid _
diff --git a/src/parsers/lexerLustreSpec.mll b/src/parsers/lexerLustreSpec.mll
index 18c911ee..564b1ae1 100644
--- a/src/parsers/lexerLustreSpec.mll
+++ b/src/parsers/lexerLustreSpec.mll
@@ -90,9 +90,9 @@ rule token = parse
| blank +
{token lexbuf}
| (('-'? ['0'-'9'] ['0'-'9']* as l) '.' (['0'-'9']* as r)) as s
- {REAL (Num.num_of_string (l^r), String.length r, s)}
+ {REAL (Real.create (l^r) (String.length r) s)}
| (('-'? ['0'-'9']+ as l) '.' (['0'-'9']+ as r) ('E'|'e') (('+'|'-') ['0'-'9'] ['0'-'9']* as exp)) as s
- {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp, s)}
+ {REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)}
| '-'? ['0'-'9']+
{INT (int_of_string (Lexing.lexeme lexbuf)) }
(* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index ad68e09b..24f13071 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -119,9 +119,9 @@ rule token = parse
| blank +
{token lexbuf}
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r) ('E'|'e') (('+'|'-')? ['0'-'9']+ as exp)) as s
- {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp , s)}
+ {REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)}
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s
- {REAL (Num.num_of_string (l^r), String.length r, s)}
+ {REAL (Real.create (l^r) (String.length r) s)}
| ['0'-'9']+
{INT (int_of_string (Lexing.lexeme lexbuf)) }
| "tel." {TEL}
diff --git a/src/parsers/parser_lustre.mly b/src/parsers/parser_lustre.mly
index 3f162e1d..a5caaa92 100644
--- a/src/parsers/parser_lustre.mly
+++ b/src/parsers/parser_lustre.mly
@@ -54,7 +54,7 @@ let rec fby expr n init =
%}
%token <int> INT
-%token <Num.num * int * string> REAL
+%token <Real.t> REAL
%token <string> STRING
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME
@@ -470,7 +470,7 @@ dim_list:
expr:
/* constants */
INT {mkexpr (Expr_const (Const_int $1))}
-| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
+| REAL {mkexpr (Expr_const (Const_real $1))}
| STRING {mkexpr (Expr_const (Const_string $1))}
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))}
@@ -606,11 +606,11 @@ signed_const_struct:
signed_const:
INT {Const_int $1}
-| REAL {let c,e,s =$1 in Const_real (c,e,s)}
+| REAL {Const_real $1}
/* | FLOAT {Const_float $1} */
| tag_ident {Const_tag $1}
| MINUS INT {Const_int (-1 * $2)}
-| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
+| MINUS REAL {Const_real (Real.uminus $2)}
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
| LCUR signed_const_struct RCUR { Const_struct $2 }
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
index e6ce5e28..f5e10639 100644
--- a/src/plugins/salsa/machine_salsa_opt.ml
+++ b/src/plugins/salsa/machine_salsa_opt.ml
@@ -778,9 +778,9 @@ let salsaStep constEnv m s =
match value.LT.eexpr_qfexpr.LT.expr_desc with
| LT.Expr_tuple [minv; maxv] -> (
let get_cst e = match e.LT.expr_desc with
- | LT.Expr_const (LT.Const_real (c,e,s)) ->
- (* calculer la valeur c * 10^e *)
- Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
+ | LT.Expr_const (LT.Const_real r) ->
+ (* calculer la valeur c * 10^e *)
+ Real.to_num r
| _ ->
Format.eprintf
"Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@."
diff --git a/src/plugins/salsa/salsaDatatypes.ml b/src/plugins/salsa/salsaDatatypes.ml
index 7b6591fa..fadbc74e 100644
--- a/src/plugins/salsa/salsaDatatypes.ml
+++ b/src/plugins/salsa/salsaDatatypes.ml
@@ -113,10 +113,10 @@ struct
*)
let inject cst = match cst with
| LT.Const_int(i) -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
- | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
+ | LT.Const_real r -> (* TODO: this is incorrect. We should rather
compute the error associated to the float *)
(* let f = float_of_string s in *)
- let n = Corelang.cst_real_to_num c e in
+ let n = Real.to_num r in
Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
(* let r = Salsa.Prelude.r_of_f_aux r in *)
diff --git a/src/scheduling.ml b/src/scheduling.ml
index d2a78206..1405eee5 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -260,7 +260,7 @@ let sort_equations_from_schedule eqs sch =
(Utils.fprintf_list ~sep:" ; " pp_eq_schedule) sch);
let split_eqs = Splitting.tuple_split_eq_list eqs in
(* Flatten schedule *)
- let sch = List.fold_right (fun vl res -> (List.map (fun v -> [v]) vl)@res) sch [] in
+ let sch = List.fold_right (fun vl res -> (List.map (fun v -> [v]) vl)@res) sch [] in
let eqs_rev, remainder =
List.fold_left
(fun (accu, node_eqs_remainder) vl ->
diff --git a/src/types.ml b/src/types.ml
index 7b20c903..69dd4cfc 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -169,8 +169,8 @@ and print_ty_param pp_basic fmt ty =
| Tbasic t -> pp_basic fmt t
| Tclock t ->
fprintf fmt "%a%s" print_ty t (if !Options.kind2_print then "" else " clock")
- | Tstatic (d, t) ->
- fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t
+ | Tstatic (d, t) -> print_ty fmt t
+ (* fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t *)
| Tconst t ->
fprintf fmt "%s" t
| Tarrow (ty1,ty2) ->
diff --git a/src/typing.ml b/src/typing.ml
index 8c4507e0..f80efb4d 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -259,8 +259,8 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
else (fun c -> None) in
begin
unif t1' t2';
- Dimension.eval Basic_library.eval_env eval_const e1;
- Dimension.eval Basic_library.eval_env eval_const e2;
+ Dimension.eval Basic_library.eval_dim_env eval_const e1;
+ Dimension.eval Basic_library.eval_dim_env eval_const e2;
Dimension.unify ~semi:semi e1 e2;
end
(* Special cases for machine_types. Rules to unify static types infered
@@ -359,7 +359,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
then dimension_of_expr arg
else Dimension.mkdim_var () in
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
- Dimension.eval Basic_library.eval_env eval_const d;
+ Dimension.eval Basic_library.eval_dim_env eval_const d;
let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
(match (* Types. *)get_static_value targ with
| None -> ()
@@ -477,7 +477,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
| Expr_power (e1, d) ->
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
- Dimension.eval Basic_library.eval_env eval_const d;
+ Dimension.eval Basic_library.eval_dim_env eval_const d;
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
let ty = (* Type_predef. *)type_array d ty_elt in
expr.expr_type <- Expr_type_hub.export ty;
@@ -637,7 +637,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let type_dim d =
begin
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
- Dimension.eval Basic_library.eval_env eval_const d;
+ Dimension.eval Basic_library.eval_dim_env eval_const d;
end in
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
--
GitLab