- 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 premises, _ = Cl.split 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 = 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
- let rps, predicate = [List.nth tl 4], List.nth tl 2 in
- let e = Cn.mk_pattern rps predicate in
- List.rev script @ convert st t @
- [T.Rewrite (false, what, None, e, dtext); T.Branch (qs, "")]
- else if is_rewrite_left hd then
- let rps, predicate = [List.nth tl 4], List.nth tl 2 in
- let e = Cn.mk_pattern rps predicate in
- List.rev script @ convert st t @
- [T.Rewrite (true, what, None, e, 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)]
+ 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)
+ in
+ let synth = mk_synth I.S.empty decurry in
+ let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
+ let script = List.rev (mk_arg st hd) in
+ match rc with
+ | Some (i, j, uri, tyno) ->
+ let classes2, tl2, _, where = split2_last classes tl in
+ let script2 = List.rev (mk_arg st where) @ script in
+ let synth2 = I.S.add 1 synth in
+ let names = get_ind_names uri tyno in
+ let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
+ if List.length qs <> List.length names then
+ let qs = proc_bkd_proofs (next st) synth [] classes tl in
+ let hd = mk_exp_args hd tl classes synth in
+ script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+ else if is_rewrite_right hd then
+ script2 @ mk_rewrite st dtext where qs tl2 false what
+ else if is_rewrite_left hd then
+ script2 @ mk_rewrite st dtext where qs tl2 true what
+ else
+ let predicate = List.nth tl2 (parsno - i) in
+ let e = Cn.mk_pattern j predicate in
+ let using = Some hd in
+ (* convert_elim st what what e @ *) script2 @
+ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
+ | None ->
+ let qs = proc_bkd_proofs (next st) synth [] classes tl in
+ let hd = mk_exp_args hd tl classes synth in
+ script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_preamble st what script
+
+and proc_other st what =
+ let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
+ let script = [T.Note text] in
+ mk_preamble st what script
+
+and proc_proof st t =
+ let f st =
+ let xtypes, note = match get_inner_types st t with
+ | Some (it, et) -> Some (H.cic it, H.cic et),
+ (Printf.sprintf "\nInferred: %s\nExpected: %s"
+ (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et)))
+ | None -> None, "\nNo types"