-and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
- if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
- if is_fwd_rewrite_left hd tl 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) ->
- let entry = Some (name, C.Decl (cic v)) in
- let intro = get_intro name t in
- mk_proof (add st entry intro) t
- | C.ALetIn (_, name, v, t) as what ->
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let entry = Some (name, C.Def (cic v, None)) in
- let intro = get_intro name t in
- let q = mk_proof (next (add st entry intro)) t in
- List.rev_append (mk_fwd_proof st dtext intro v) q
- else
- [T.Apply (what, dtext)]
+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 -> false
+ | 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
+ let ity = H.acic_bc st.context ity 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))