- 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)]
+ 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 t ity
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl ->
+ mk_fwd_rewrite st dtext intro tl false v t ity
+ | v ->
+ assert (Ut.is_sober st.context (H.cic ity));
+ let ity = H.acic_bc st.context ity in
+ 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, H.cic w), [T.LetIn (intro, v, dtext)]
+ in
+ let entry = Some (name, hyp) in
+ let qt = proc_proof (next (add st entry)) t in
+ List.rev_append rqv qt
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_preamble 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_preamble st what script
+
+and proc_mutconstruct st what =
+ let _, dtext = test_depth st in
+ let script = [T.Apply (what, dtext)] in
+ mk_preamble st what script
+
+and proc_const st what =
+ let _, dtext = test_depth st in
+ let script = [T.Apply (what, dtext)] in
+ mk_preamble 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, goal = match get_inner_types st what with
+ | None -> 0, None
+ | Some (ity, ety) ->
+ snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ety)
+ in
+ let parsno, argsno = List.length classes, List.length tl in
+ let decurry = parsno - argsno in
+ let diff = goal_arity - decurry in
+ if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (H.cic hd)));
+ let classes = Cl.adjust st.context tl ?goal classes in
+ let rec mk_synth a n =
+ if n < 0 then a else mk_synth (I.S.add n a) (pred n)