- P.Intros (Some count, List.rev st.intros, "") :: script
-
-let is_rewrite_right = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
- | _ -> false
-
-let is_rewrite_left = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
- | _ -> false
-
-let mk_premise = function
- | C.ARel (_, _, _, binder) -> binder
- | _ -> assert false
+ let p0 = T.Whd (count, "") in
+ let p1 = T.Intros (Some count, List.rev st.intros, "") in
+ match st.ety with
+ | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
+ | _ -> p1 :: script
+with Invalid_argument _ -> failwith "A2P.mk_intros"
+(*
+let rec mk_premise st dtext = function
+ | C.ARel (_, _, _, binder) -> [], binder
+ | where ->
+ let name = contracted_premise in
+ mk_fwd_proof st dtext name where, name
+*)
+let rec mk_fwd_rewrite st dtext name tl direction =
+ let what, where = List.nth tl 5, List.nth tl 3 in
+ let rewrite premise =
+ [T.Rewrite (direction, what, Some (premise, name), dtext)]
+ in
+ match where with
+ | 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]