- let absts, args = aux 0 identity [] in
- match Cn.lift 1 n t with
- | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
- | t -> absts (C.AAppl ("", t :: args))
-
-let appl_expand n = function
- | C.AAppl (id, ts) ->
- let before, after = T.list_split (List.length ts + n) ts in
- C.AAppl ("", C.AAppl (id, before) :: after)
- | _ -> assert false
-
-let get_intro name t =
-try
-match name with
- | C.Anonymous -> unused_premise
- | C.Name s ->
- if DTI.does_not_occur 1 (cic t) then unused_premise else s
-with Invalid_argument _ -> failwith "A2P.get_intro"
-
-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
+ 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
+ if (Cn.does_not_occur e) then st, [] else
+ match where with
+ | C.ARel (_, _, i, premise) as w ->
+ let script name =
+ let where = Some (premise, name) in
+ let script = mk_arg st what @ mk_arg st w in
+ T.Rewrite (direction, what, where, e, dtext) :: script
+ in
+ if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
+ {st with context = Cn.clear st.context premise}, script name
+ else begin
+ assert (Ut.is_sober st.context (H.cic ity));
+ let ity = H.acic_bc st.context ity in
+ let br1 = [T.Id ""] in
+ let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
+ let text = "non linear rewrite" in
+ st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
+ end
+ | _ -> 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 = [T.Branch (qs, "")] in
+ if (Cn.does_not_occur e) then script else
+ T.Rewrite (direction, where, None, e, dtext) :: script
+
+let rec proc_lambda st what name v t =
+ let name = match name with
+ | C.Anonymous -> H.mk_fresh_name st.context anonymous_premise
+ | name -> name
+ in
+ let entry = Some (name, C.Decl (H.cic v)) in
+ let intro = get_intro name in
+ let script = proc_proof (add st entry) t in
+ let script = T.Intros (Some 1, [intro], "") :: script in
+ mk_preamble st what script
+
+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 t ity
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl ->
+ mk_fwd_rewrite st dtext intro tl false v t ity
+ | v ->
+ assert (Ut.is_sober st.context (H.cic ity));
+ let ity = H.acic_bc st.context ity in
+ let qs = [proc_proof (next st) v; [T.Id ""]] 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)) t in
+ List.rev_append rqv qt