Commit 988f29da authored by Andrei Paskevich's avatar Andrei Paskevich

- minor bugfix in Pretty

- move redefinition of f_app higher in Term
  to make sure that ps_neq can never appear
- if a user "instantiates" a lemma as a goal on cloning, 
  the lemma just disappears (as it is alredy proved)
- catch Not_found in merge_namespace on cloning,
  due to local goals not being cloned
parent b54aec3f
......@@ -89,8 +89,8 @@ let print_ts fmt ts =
let print_ls fmt ls =
Hid.replace lhash ls.ls_name ls;
if ls.ls_constr then fprintf fmt "%s" (id_unique lprinter ls.ls_name)
else fprintf fmt "%s" (id_unique cprinter ls.ls_name)
if ls.ls_constr then fprintf fmt "%s" (id_unique cprinter ls.ls_name)
else fprintf fmt "%s" (id_unique lprinter ls.ls_name)
let print_pr fmt pr =
Hid.replace phash pr.pr_name pr;
......@@ -196,7 +196,7 @@ and print_tnode opl opr fmt t = match t.t_node with
print_term t1 (print_list newline print_tbranch) bl
| Teps fb ->
let v,f = f_open_bound fb in
fprintf fmt (protect_on opr "epsilon %a in@ %a")
fprintf fmt (protect_on opr "epsilon %a.@ %a")
print_vsty v print_opl_fmla f;
forget_var v
......
......@@ -461,6 +461,22 @@ let f_label l f = Hfmla.hashcons { f with f_label = l }
let f_label_add l f = Hfmla.hashcons { f with f_label = l :: f.f_label }
let f_label_copy { f_label = l } f = if l == [] then f else f_label l f
(* built-in symbols *)
let ps_equ =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix =") [v; v]
let ps_neq =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix <>") [v; v]
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]
let f_app p tl =
if p == ps_neq then f_not (f_app ps_equ tl) else f_app p tl
let f_app_unsafe = f_app
(* unsafe map with level *)
......@@ -829,22 +845,6 @@ let f_open_branch (pat, _, f) =
let vars, s, ns = pat_substs pat in
(pat_rename ns pat, vars, f_inst s 0 f)
(* built-in symbols *)
let ps_equ =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix =") [v; v]
let ps_neq =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix <>") [v; v]
let f_app p tl =
if p == ps_neq then f_not (f_app ps_equ tl) else f_app p tl
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]
(** Term library *)
module Termlib = struct
......
......@@ -694,10 +694,13 @@ module Context = struct
create_ind_decl (List.map add indl) :: acc
| Dprop (Pgoal, _) ->
acc
| Dprop (_, pr) ->
let k = if Spr.mem pr inst.inst_lemma then Plemma
else if Spr.mem pr inst.inst_goal then Pgoal
else Paxiom
| Dprop (Plemma, pr) when Spr.mem pr inst.inst_goal ->
acc
| Dprop (k, pr) ->
let k = match k with
| Paxiom when Spr.mem pr inst.inst_lemma -> Plemma
| Paxiom when Spr.mem pr inst.inst_goal -> Pgoal
| _ -> Paxiom
in
create_prop_decl k (cl_find_pr cl pr) :: acc
| Duse _ | Dclone _ ->
......@@ -884,7 +887,8 @@ module TheoryUC = struct
then Hpr.find cl.Context.pr_table pr else pr in
let f_ts n ts ns = add_ts true n (find_ts ts) ns in
let f_ls n ls ns = add_ls true n (find_ls ls) ns in
let f_pr n pr ns = add_pr true n (find_pr pr) ns in
let f_pr n pr ns = try add_pr true n (find_pr pr) ns
with Not_found -> ns (* goals are not cloned *) in
let rec f_ns n s = add_ns true n (merge_namespace empty_ns s)
and merge_namespace acc ns =
let acc = Mnm.fold f_ts ns.ns_ts acc in
......
......@@ -197,7 +197,7 @@ and print_tnode opl opr fmt t = match t.t_node with
print_term t1 (print_list newline print_tbranch) bl
| Teps fb ->
let v,f = f_open_bound fb in
fprintf fmt (protect_on opr "epsilon %a in@ %a")
fprintf fmt (protect_on opr "epsilon %a.@ %a")
print_vsty v print_opl_fmla f;
forget_var v
......
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