pdecl: fixed val predicate

parent b19660c9
......@@ -354,9 +354,19 @@ let rec t_insert hd t = match t.t_node with
| _ when hd.t_ty = None -> t_iff_simp hd t
| _ -> t_equ_simp hd t
let rec t_subst_fmla v t f = t_label_copy f (match f.t_node with
| Tapp (ps, [{t_node = Tvar u}; t1])
when ls_equal ps ps_equ && vs_equal v u && t_v_occurs v t1 = 0 ->
t_iff_simp t (t_equ_simp t1 t_bool_true)
| Tvar u when vs_equal u v -> t_if t t_bool_true t_bool_false
| _ -> t_map (t_subst_fmla v t) f)
let create_let_decl ld =
let conv_post t q =
let v,f = open_post q in t_subst_single v t f in
let v,f = open_post q in
match t.t_ty with
| Some _ -> t_subst_single v t f
| None -> t_subst_fmla v t f in
let conv_post t ql = List.map (conv_post t) ql in
let cty_axiom id cty f =
(* the absence of aliases in checked in add_pdecl *)
......
......@@ -319,7 +319,7 @@ let unit_module =
let td = create_alias_decl (id_fresh "unit") [] ity_unit in
let pd = create_type_decl [td] in
let uc = add_pdecl uc pd in
let th = List.fold_left add_decl uc.muc_theory pd.pd_pure in
let th = List.fold_left (add_decl ~warn:false) uc.muc_theory pd.pd_pure in
close_module { uc with muc_theory = th }
let create_module env ?(path=[]) n =
......@@ -339,7 +339,7 @@ let add_pdecl ~vc uc d =
| None -> uc) ids uc in
ignore vc; (* TODO *)
let uc = add_pdecl uc d in
let th = List.fold_left add_decl uc.muc_theory d.pd_pure in
let th = List.fold_left (add_decl ~warn:true) uc.muc_theory d.pd_pure in
{ uc with muc_theory = th }
(** {2 Cloning} *)
......
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