- let qs = [[T.Id ""]; mk_proof (next st) v] in
- [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | _ ->
- [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)]
- in
- 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 = get_type "TC2" st hd in
- let (classes, rc) as h = Cl.classify st.context ty in
- let premises, _ = P.split st.context ty in
- assert (List.length classes - List.length tl = 0);
- let synth = I.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 && M.is_eliminator premises ->
- let classes, tl, _, what = split2_last classes tl in
- let script, what = mk_atomic st dtext what in
- let synth = I.S.add 1 synth in
- let qs = mk_bkd_proofs (next st) synth classes tl in
- if is_rewrite_right hd then
- mk_rewrite st dtext script t what qs tl false
- else if is_rewrite_left hd then
- mk_rewrite st dtext script t what qs tl true
- else
- let l = succ (List.length tl) in
- let predicate = List.nth tl (l - i) in
- let e = Cn.mk_pattern j predicate in
- let using = Some hd in
- List.rev script @ convert st t @
- [T.Elim (what, using, e, 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)]