Good static Constructors names.

compiler/global/static.ml

@@ -18,18 +18,20 @@ open Names
 open Format
 
 type static_exp =
+  | Svar of name
   | Sint of int
   | Sfloat of float
   | Sbool of bool
+  | Sconstructor of
   | Sarray_power of static_exp * static_exp (** power : 0^n : [0,0,0,0,0,..] *)
   | Sarray of static_exp list (** [ e1, e2, e3 ] *)
-  | Svar of name
+  | Sop of longname * static_exp list (** defined ops for now in pervasives *)
-  | Sop of longname * static_exp list (** defined ops for now pervasives *)
+
 
 (** Constraints on size expressions. *)
 type size_constraint =
-  | Cequal of size_exp * size_exp (* e1 = e2*)
+  | Cequal of static_exp * static_exp (* e1 = e2*)
-  | Clequal of size_exp * size_exp (* e1 <= e2 *)
+  | Clequal of static_exp * static_exp (* e1 <= e2 *)
   | Cfalse
 
 (* unsatisfiable constraint *)
@@ -121,16 +123,16 @@ let rec solve const_env =
 let rec static_exp_subst m =
   function
     | Svar n -> (try List.assoc n m with | Not_found -> Svar n)
-    | Sop (op, e1, e2) -> Sop (op, size_exp_subst m e1, size_exp_subst m e2)
+    | Sop (op, e1, e2) -> Sop (op, static_exp_subst m e1, static_exp_subst m e2)
     | s -> s
 
 (** Substitutes variables in the constraint list with their value
     in the map (mapping vars to size exps). *)
 let instanciate_constr m constr =
   let replace_one m = function
-      | Cequal (e1, e2) -> Cequal (size_exp_subst m e1, size_exp_subst m e2)
+    | Cequal (e1, e2) -> Cequal (static_exp_subst m e1, static_exp_subst m e2)
-      | Clequal (e1, e2) -> Clequal (size_exp_subst m e1, size_exp_subst m e2)
+    | Clequal (e1, e2) -> Clequal (static_exp_subst m e1, static_exp_subst m e2)
-      | Cfalse -> Cfalse
+    | Cfalse -> Cfalse
   in List.map (replace_one m) constr
 
 let op_to_string =
@@ -138,7 +140,7 @@ let op_to_string =
 
 let rec print_static_exp ff =
   function
-    | Sconst i -> fprintf ff "%d" i
+    | SConst i -> fprintf ff "%d" i
     | Svar id -> fprintf ff "%s" id
     | Sop (op, e1, e2) ->
         fprintf ff "@[(%a %s %a)@]"
@@ -146,10 +148,10 @@ let rec print_static_exp ff =
 
 let print_size_constraint ff = function
   | Cequal (e1, e2) ->
-      fprintf ff "@[%a = %a@]" print_size_exp e1 print_size_exp e2
+      fprintf ff "@[%a = %a@]" print_static_exp e1 print_static_exp e2
   | Clequal (e1, e2) ->
-      fprintf ff "@[%a <= %a@]" print_size_exp e1 print_size_exp e2
+      fprintf ff "@[%a <= %a@]" print_static_exp e1 print_static_exp e2
-  | Cfalse -> fprintf ff "False"
+  | Cfalse -> fprintf ff "Cfalse"
 
 let psize_constraint oc c =
   let ff = formatter_of_out_channel oc

compiler/heptagon/analysis/typing.ml

@@ -628,9 +628,9 @@ and typing_array_op statefull h op e_list =
         let typed_idx2 = expect statefull h (Tid Initial.pint) idx2 in
         let typed_e, t1 = typing statefull h e in
         (*Create the expression to compute the size of the array *)
-        let e1 = SOp (SMinus, static_exp_of_exp idx2, static_exp_of_exp idx1) in
+        let e1 = Sop (SMinus, static_exp_of_exp idx2, static_exp_of_exp idx1) in
-        let e2 = SOp (SPlus, e1, SConst 1) in
+        let e2 = Sop (SPlus, e1, SConst 1) in
-        add_size_constr (LEqual (SConst 1, e2));
+        add_size_constr (Clequal (SConst 1, e2));
         Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
     | Econcat, [e1; e2] ->
         let typed_e1, t1 = typing statefull h e1 in
@@ -640,7 +640,7 @@ and typing_array_op statefull h op e_list =
         with
             TypingError(kind) -> message e1.e_loc kind
         end;
-        let n = SOp (SPlus, static_exp t1, static_exp t2) in
+        let n = Sop (SPlus, static_exp t1, static_exp t2) in
         Tarray (element_type t1, n), op, [typed_e1; typed_e2]
     | Eiterator (it, ({ op_name = f; op_params = params;
                         op_kind = k } as op_desc), reset),