module Ut = CicUtil
module E = CicEnvironment
module PEH = ProofEngineHelpers
-module PER = ProofEngineReduction
module Pp = CicPp
module Cl = ProceduralClassify
ty
with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
+let get_entry st id =
+ let rec aux = function
+ | [] -> assert false
+ | Some (C.Name name, e) :: _ when name = id -> e
+ | _ :: tl -> aux tl
+ in
+ aux st.context
+
(* proof construction *******************************************************)
let unused_premise = "UNUSED"
let convert st ?name v =
match get_inner_types st v with
- | None -> []
- | Some (st, et) ->
- let cst, cet = cic st, cic et in
- if PER.alpha_equivalence cst cet then [] else
+ | None -> []
+ | Some (sty, ety) ->
+ let csty, cety = cic sty, cic ety in
+ if Ut.alpha_equivalence csty cety then [] else
let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
match name with
- | None -> [T.Change (st, et, None, e, "")]
- | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
+ | None -> [T.Change (sty, ety, None, e, "")]
+ | Some id ->
+ begin match get_entry st id with
+ | C.Def _ -> [T.ClearBody (id, "")]
+ | C.Decl w ->
+ if Ut.alpha_equivalence csty w then []
+ else [T.Change (sty, ety, Some (id, id), e, "")]
+ end
let get_intro = function
| C.Anonymous -> unused_premise
T.Intros (Some count, List.rev st.intros, "") :: script
let mk_arg st = function
- | C.ARel (_, _, _, name) as what -> [] (* convert st ~name what *)
+ | C.ARel (_, _, _, name) as what -> convert st ~name what
| _ -> []
let mk_fwd_rewrite st dtext name tl direction =
let qs = [[T.Id ""]; proc_proof (next st) v] in
[T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
in
- C.Decl (get_type "TC1" st v), rqv
+ C.Decl (cic ity), rqv
| None ->
C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
in