- | C.ARel (_, _, _, binder) -> rewrite binder
- | _ ->
- assert (get_inner_sort st where = `Prop);
- let pred, old = List.nth tl 2, List.nth tl 1 in
- let pred_name = defined_premise in
- let pred_text = "extracted" in
- let p1 = T.LetIn (pred_name, pred, pred_text) in
- let cut_name = assumed_premise in
- let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
- let cut_text = "" in
- let p2 = T.Cut (cut_name, cut_type, cut_text) in
- let qs = [rewrite cut_name; mk_proof (next st) where] in
- [T.Branch (qs, ""); p2; p1]
-
-and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
- if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
- if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
- let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
- begin match get_inner_types st v with
- | Some (ity, _) when M.bkd st.context ty ->
- let qs = [[T.Id ""]; mk_proof (next st) v] in
- [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | _ ->
- let (classes, rc) as h = Cl.classify st.context ty in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- [T.LetIn (name, v, dtext ^ text)]
- end
- | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
- begin match Cn.mk_ind st.context id uri tyno outty arg cases with
- | None -> [T.LetIn (name, v, dtext)]
- | Some v -> mk_fwd_proof st dtext name v
- end
- | v ->
- [T.LetIn (name, v, dtext)]
-
-and mk_proof st = function
- | C.ALambda (_, name, v, t) as what ->
- let entry = Some (name, C.Decl (cic v)) in
- let intro = get_intro name t in
- let ety = match get_inner_types st what with
- | Some (_, ety) -> Some ety
- | None -> None
- in
- mk_proof (add st entry intro ety) 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 None)) t in
- List.rev_append (mk_fwd_proof st dtext intro v) q
- else
- [T.Apply (what, dtext)]
+ | C.ARel (_, _, _, premise) ->
+ let script = mk_arg st what in
+ let where = Some (premise, name) in
+ T.Rewrite (direction, what, where, e, dtext) :: script
+ | _ -> assert false
+
+let mk_rewrite st dtext what qs tl direction =
+ assert (List.length tl = 5);
+ let predicate = List.nth tl 2 in
+ let e = Cn.mk_pattern 1 predicate in
+ [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
+
+let rec proc_lambda st name v t =
+ let entry = Some (name, C.Decl (cic v)) in
+ let intro = get_intro name in
+ proc_proof (add st entry intro) t
+
+and proc_letin st what name v t =
+ let intro = get_intro name in
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let hyp, rqv = match get_inner_types st v with
+ | Some (ity, _) ->
+ let rqv = match v with
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
+ mk_fwd_rewrite st dtext intro tl true
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl ->
+ mk_fwd_rewrite st dtext intro tl false
+ | v ->
+ let qs = [[T.Id ""]; proc_proof (next st) v] in
+ [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+ in
+ C.Decl (cic ity), rqv
+ | None ->
+ C.Def (cic v, None), [T.LetIn (intro, v, dtext)]