- let clears st script =
- if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
- in
- intros st (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
- 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
- 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)]
- | _ -> 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 what name v t =
- let dno, ae = match get_inner_types st t with
- | None -> false, true
- | Some (sty, ety) ->
- let sty, ety = H.cic sty, H.cic ety in
- DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety,
- Ut.alpha_equivalence sty ety
- in
- let dno = dno && DTI.does_not_occur 1 (H.cic t) 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
- let st = (add st entry intro) in
- if ae then proc_proof st t else
- let script = proc_proof (clear st) t in
- mk_intros st t 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 ->
- 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)]
+ let flavour_map x y = match x, y with
+ | None, G.IPAs flavour -> Some flavour
+ | _ -> x
+ in
+ match List.fold_left flavour_map None params with
+ | Some fl -> fl
+ | None -> aux attrs
+
+let proc_obj ?(info="") proc_proof sorts params context = function
+ | C.AConstant (_, _, s, Some v, t, [], attrs) ->
+ begin match get_flavour sorts params context v attrs with
+ | flavour when List.mem flavour th_flavours ->
+ let ast = proc_proof v in
+ let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
+ let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"