- | C.ARel (_, _, _, binder) -> rewrite binder
- | _ ->
- assert (get_inner_sort st where = `Prop);
- let pred, old = List.nth tl 2, List.nth tl 1 in
- let pred_name = defined_premise in
- let pred_text = "extracted" in
- let p1 = T.LetIn (pred_name, pred, pred_text) in
- let cut_name = assumed_premise in
- let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
- let cut_text = "" in
- let p2 = T.Cut (cut_name, cut_type, cut_text) in
- let qs = [rewrite cut_name; mk_proof (next st) where] in
- [T.Branch (qs, ""); p2; p1]
-
-and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
- if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
- if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
- let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
- begin match get_inner_types st v with
- | Some (ity, _) when M.bkd st.context ty ->
- let qs = [[T.Id ""]; mk_proof (next st) v] in
- [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | _ ->
- let (classes, rc) as h = Cl.classify st.context ty in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- [T.LetIn (name, v, dtext ^ text)]
- end
- | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
- begin match Cn.mk_ind st.context id uri tyno outty arg cases with
- | None -> [T.LetIn (name, v, dtext)]
- | Some v -> mk_fwd_proof st dtext name v
- end
- | v ->
- [T.LetIn (name, v, dtext)]
-
-and mk_proof st = function
- | C.ALambda (_, name, v, t) as what ->
- let entry = Some (name, C.Decl (cic v)) in
- let intro = get_intro name t in
- let ety = match get_inner_types st what with
- | Some (_, ety) -> Some ety
- | None -> None
+ | C.ARel (_, _, i, premise) as v ->
+ let where = Some (premise, name) in
+(* let _script = convert_elim st ~name:(premise, i) t v e in *)
+ let script = mk_arg st what @ mk_arg st v (* @ script *) in
+ let st = {st with context = Cn.clear st.context premise} in
+ st, T.Rewrite (direction, what, where, e, dtext) :: script
+ | _ -> assert false
+
+let mk_rewrite st dtext where qs tl direction t =
+ assert (List.length tl = 5);
+ let predicate = List.nth tl 2 in
+ let e = Cn.mk_pattern 1 predicate in
+ let script = [] (* convert_elim st t t e *) in
+ script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
+
+let rec proc_lambda st name v t =
+ let dno = DTI.does_not_occur 1 (H.cic t) in
+ let dno = dno && match get_inner_types st t with
+ | None -> true
+ | Some (it, et) ->
+ DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
+ in
+ let name = match dno, name with
+ | true, _ -> C.Anonymous
+ | false, C.Anonymous -> H.mk_fresh_name st.context used_premise
+ | false, name -> name
+ in
+ let entry = Some (name, C.Decl (H.cic v)) in
+ let intro = get_intro name in
+ proc_proof (add st entry intro) t
+
+and proc_letin st what name v t =
+ let intro = get_intro name in
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let st, hyp, rqv = match get_inner_types st v with
+ | Some (ity, _) ->
+ let st, rqv = match v with
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
+ mk_fwd_rewrite st dtext intro tl true v
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl ->
+ mk_fwd_rewrite st dtext intro tl false v
+ | v ->
+ let qs = [proc_proof (next st) v; [T.Id ""]] in
+ st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+ in
+ st, C.Decl (H.cic ity), rqv
+ | None ->
+ st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)]
+ in
+ let entry = Some (name, hyp) in
+ let qt = proc_proof (next (add st entry intro)) t in
+ List.rev_append rqv qt
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_intros st what script
+
+and proc_rel st what =
+ let _, dtext = test_depth st in
+ let text = "assumption" in
+ let script = [T.Apply (what, dtext ^ text)] in
+ mk_intros st what script
+
+and proc_mutconstruct st what =
+ let _, dtext = test_depth st in
+ let script = [T.Apply (what, dtext)] in
+ mk_intros st what script
+
+and proc_appl st what hd tl =
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let ty = get_type "TC2" st hd in
+ let classes, rc = Cl.classify st.context ty in
+ let goal_arity = match get_inner_types st what with
+ | None -> 0
+ | Some (ity, _) -> snd (PEH.split_with_whd (st.context, H.cic ity))