diff --git a/examples/bts/138.mlw b/examples/bts/138.mlw index fd962cfa32724e9ac733aed77cfbbc321eb569ca..db43286293526df67b281063ab47a4dba4267d42 100644 --- a/examples/bts/138.mlw +++ b/examples/bts/138.mlw @@ -1,27 +1,17 @@ -module Test +module Test use int.Int type a = < range 22 46 > - + let f (b : a) = requires {a'int b = 42} ensures {a'int result = a'int b} (42:a) - -end - -module Test2 - use int.Int - let f (b : int) = - requires {b = 42} - ensures {result = b} - 42 - end module Test1 - clone Test2 as T (* Replace with Test does not work *) - -end \ No newline at end of file + clone Test as T (* Replace with Test does not work *) + +end diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index d00a5c925a73777e6cda6508a132ea59b0b43f9b..75d928f7b19c210256757ffc53fbe62f051c84a3 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -755,7 +755,7 @@ let clone_ppat cl sm pp mask = let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with | Evar v -> e_var (sm_find_pv sm v) - | Econst c -> e_const c e.e_ity + | Econst c -> e_const c (clone_ity cl e.e_ity) | Eexec (c,_) -> e_exec (clone_cexp cl sm c) | Eassign asl -> let conv (r,f,v) = @@ -1015,10 +1015,20 @@ let clone_pdecl inst cl uc d = match d.pd_node with let add_e spv e = Spv.union spv e.e_effect.eff_reads in let add_d spv d = List.fold_left add_e spv d.itd_witness in freeze_foreign cl (List.fold_left add_d Spv.empty tdl); - let tdl, vcl = clone_type_decl inst cl tdl uc.muc_known in - if tdl = [] then List.fold_left add_vc uc vcl else - let add uc d = add_pdecl ~warn:false ~vc:false uc d in - List.fold_left add uc (create_type_decl tdl) + let ndl, vcl = clone_type_decl inst cl tdl uc.muc_known in + let uc = List.fold_left add_vc uc vcl in + let dl = if ndl <> [] then create_type_decl ndl else [] in + let save_special_ls d d' = match d.d_node, d'.d_node with + | Dparam ls, Dparam ls' | Dlogic [ls,_], Dlogic [ls',_] -> + cl.ls_table <- Mls.add ls ls' cl.ls_table; + | Dtype _, Dtype _ -> () + | _ -> assert false in + begin match tdl, dl with + | [{itd_its = {its_def = (Range _|Float _)}}], [d'] -> + List.iter2 save_special_ls d.pd_pure d'.pd_pure + | _ -> () end; + let add uc d = add_pdecl ~warn:false ~vc:false uc d in + List.fold_left add uc dl | PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs -> (* refine only [val] symbols *) let cty = match c.c_node with (* cty for [val constant] is not c.c_cty *)