-and mk_proof st t =
-try
- match t with
- | 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 w 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, H.cic w), [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_const 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))
+ 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 rec mk_synth a n =
+ if n < 0 then a else mk_synth (I.S.add n a) (pred n)