Commit 9ec870c8 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix typing of constants in programs, and also the issue with double cast

parent e196d727
......@@ -832,8 +832,6 @@ let check_literal c ty =
| _ -> raise (InvalidLiteralType ty) in
match c with
| Number.ConstInt c when not (ts_equal ts ts_int) ->
Format.eprintf "check literal %a of type %s@."
Number.print_integer_constant c ts.ts_name.id_string;
begin match ts.ts_def with
| Range ir -> Number.check_range c ir
| _ -> raise (InvalidLiteralType ty)
......
......@@ -541,10 +541,7 @@ let rec raw_of_expr prop e = match e.e_node with
effect-hiding construction, Etry, is forbidden. *)
| Eassign _ | Ewhile _ | Efor _ | Eassert _ -> assert false
| Evar v -> t_var v.pv_vs
| Econst (Number.ConstInt _ as c)->
t_const c ty_int
| Econst (Number.ConstReal _ as c)->
t_const c ty_real
| Econst c -> t_const c (ty_of_ity e.e_ity)
| Epure t -> t
| Eghost e -> pure_of_expr prop e
| Eexec (_,{cty_post = []}) -> raise Exit
......
......@@ -439,10 +439,8 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
let k = match e.e_node with
| Evar v ->
Klet (res, t_lab (t_var v.pv_vs), t_true)
| Econst (Number.ConstInt _ as c)->
Klet (res, t_lab (t_const c ty_int), t_true)
| Econst (Number.ConstReal _ as c)->
Klet (res, t_lab (t_const c ty_real), t_true)
| Econst c ->
Klet (res, t_lab (t_const c (ty_of_ity e.e_ity)), t_true)
| Eexec (ce, ({cty_pre = pre; cty_oldies = oldies} as cty)) ->
(* [ VC(ce) (if ce is a lambda executed in-place)
| STOP pre
......
......@@ -366,13 +366,13 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
DTuloc (dterm tuc gvars at denv e1, uloc)
| Ptree.Tnamed (Lstr lab, e1) ->
DTlabel (dterm tuc gvars at denv e1, Slab.singleton lab)
| Ptree.Tcast (e1, ty) ->
(* FIXME: accepts and silently ignores double casts: ((0:ty1):ty2) *)
let e1 = dterm tuc gvars at denv e1 in
let ty = ty_of_pty tuc ty in
match e1.dt_node with
| DTconst (c,_) -> DTconst (c, ty)
| _ -> DTcast (e1, ty))
| Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) ->
let ty = ty_of_pty tuc pty in
DTconst (c, ty)
| Ptree.Tcast (e1, pty) ->
let d1 = dterm tuc gvars at denv e1 in
let ty = ty_of_pty tuc pty in
DTcast (d1, ty))
(** typing program expressions *)
......@@ -586,7 +586,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| None -> qualid_app loc q el)
| _ -> qualid_app loc q el
in
Dexpr.dexpr ~loc (match desc with
Dexpr.dexpr ~loc begin match desc with
| Ptree.Eident q ->
qualid_app loc q []
| Ptree.Eidapp (q, el) ->
......@@ -747,13 +747,14 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
DEuloc (dexpr muc denv e1, uloc)
| Ptree.Enamed (Lstr lab, e1) ->
DElabel (dexpr muc denv e1, Slab.singleton lab)
| Ptree.Ecast (e1, pty) ->
let e1 = dexpr muc denv e1 in
| Ptree.Ecast ({expr_desc = Ptree.Econst c},pty) ->
let ity = ity_of_pty muc pty in
DEconst (c, dity_of_ity ity)
| Ptree.Ecast (e1,pty) ->
let d1 = dexpr muc denv e1 in
let ity = ity_of_pty muc pty in
let dity = dity_of_ity ity in
match e1.de_node with
| DEconst (c, _) -> DEconst (c, dity)
| _ -> DEcast (e1, ity))
DEcast (d1, ity)
end
and drec_defn muc denv fdl =
let prep (id, gh, kind, bl, pty, msk, sp, e) =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment