- mk_intros st script
- | C.ARel _ as what ->
- let _, dtext = test_depth st in
- let text = "assumption" in
- let script = [T.Apply (what, dtext ^ text)] in
- mk_intros st script
- | C.AMutConstruct _ as what ->
- let _, dtext = test_depth st in
- let script = [T.Apply (what, dtext)] in
- mk_intros st script
- | C.AAppl (_, hd :: tl) as t ->
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
- let (classes, rc) as h = Cl.classify st.context ty in
- let decurry = List.length classes - List.length tl in
- if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
- if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
- let synth = Cl.S.singleton 0 in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- match rc with
- | Some (i, j) when i > 1 && i <= List.length classes ->
- let classes, tl, _, what = split2_last classes tl in
- let script, what = mk_atomic st dtext what in
- let synth = Cl.S.add 1 synth in
- let qs = mk_bkd_proofs (next st) synth classes tl in
- if is_rewrite_right hd then
- List.rev script @ convert st t @
- [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
- else if is_rewrite_left hd then
- List.rev script @ convert st t @
- [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
- else
- let using = Some hd in
- List.rev script @ convert st t @
- [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
- | _ ->
- let qs = mk_bkd_proofs (next st) synth classes tl in
- let script, hd = mk_atomic st dtext hd in
- List.rev script @ convert st t @
- [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
- else
- [T.Apply (t, dtext)]