- assert (Ut.is_sober st.context csty);
- assert (Ut.is_sober st.context cety);
- if Ut.alpha_equivalence csty cety then script else
- let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
- match name with
- | None -> T.Change (sty, ety, None, e, "") :: script
- | Some (id, i) ->
- begin match get_entry st id with
- | C.Def _ -> assert false (* T.ClearBody (id, "") :: script *)
- | C.Decl _ ->
- T.Change (ety, sty, Some (id, Some id), e, "") :: script
- end
-
-let convert st ?name v =
- match get_inner_types st v with
- | None ->
- if debug then [T.Note "NORMAL: NO INNER TYPES"] else []
- | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
-
-let convert_elim st ?name t v pattern =
- match t, get_inner_types st t, get_inner_types st v with
- | _, None, _
- | _, _, None -> [(* T.Note "ELIM: NO INNER TYPES"*)]
- | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
- let where = List.hd (List.rev tl) in
- let cty = Cn.elim_inferred_type
- st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
- in
- mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
- | _, Some _, Some _ -> assert false
-
-let get_intro = function
- | C.Anonymous -> None
- | C.Name s -> Some s
-
-let mk_preamble st what script =
- let clears st script =
- if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
- in
- clears st (convert st what @ script)
-
-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 v t ity =
- let compare premise = function
- | None -> true
- | Some s -> s = premise
- in
- 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 = convert_elim st ~name:(premise, i) v w e in *)
- let script name =
- let where = Some (premise, name) in
- let script = mk_arg st what @ mk_arg st w (* @ script *) 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
-(* let script = convert_elim st t t e in *)
- 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)]