clears_note: string;
case: int list;
skip_thm_and_qed : bool;
- skip_initial_lambdas : bool;
}
(* helpers ******************************************************************)
let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
note (Pp.ppterm csty) (Pp.ppterm cety)
in
+ assert (Ut.is_sober csty);
+ assert (Ut.is_sober cety);
if Ut.alpha_equivalence csty cety then [(* T.Note note *)] 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, ""(*note*))]
| Some (id, i) ->
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 -> true
+ | None -> false
| Some (it, et) ->
DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
in
mk_fwd_rewrite st dtext intro tl false v
| v ->
let qs = [proc_proof (next st) v; [T.Id ""]] in
- st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+ 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 ->
(Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et)))
| None -> None, "\nNo types"
in
- let context, clears =
- if st.skip_initial_lambdas then
- st.context, []
- else
- Cn.get_clears st.context (H.cic t) xtypes
- in
+ let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
let note = Pp.ppcontext st.context ^ note in
{st with context = context; clears = clears; clears_note = note; }
in
let ast = proc_proof st v in
let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
- let ast =
- if st.skip_initial_lambdas then
- match ast with
- | T.Intros _::tl -> tl
- | ast -> ast
- else ast
- in
if st.skip_thm_and_qed then ast
else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
| _ ->
(* interface functions ******************************************************)
let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-?(skip_thm_and_qed=false) ?(skip_initial_lambdas=false) prefix aobj =
+?(skip_thm_and_qed=false) prefix aobj =
let st = {
sorts = ids_to_inner_sorts;
types = ids_to_inner_types;
clears_note = "";
case = [];
skip_thm_and_qed = skip_thm_and_qed;
- skip_initial_lambdas = skip_initial_lambdas;
} in
HLog.debug "Procedural: level 2 transformation";
let steps = proc_obj st aobj in