-let mk_intros st script =
-try
- if st.intros = [] then script else
- let count = List.length st.intros in
- 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_atomic st dtext what =
- if T.is_atomic what then
- match what with
- | C.ARel (_, _, _, name) -> convert st ~name what, what
- | _ -> [], what
+let mk_arg st = function
+ | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
+ | _ -> []
+
+let mk_fwd_rewrite st dtext name tl direction t =
+ assert (List.length tl = 6);
+ let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
+ let e = Cn.mk_pattern 1 predicate in
+ match where with
+ | C.ARel (_, _, i, premise) as v ->
+ let where = Some (premise, name) in
+(* let _script = convert_elim st ~name:(premise, i) t v e in *)
+ let script = mk_arg st what @ mk_arg st v (* @ script *) in
+ let st = {st with context = Cn.clear st.context premise} in
+ st, T.Rewrite (direction, what, where, e, dtext) :: script
+ | _ -> assert false
+
+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