- let args = List.rev_map2 map tl classes in
- let args = aux args in
- if args = [] then hd else C.AAppl ("", hd :: args)
-
-let convert st ?name v =
- match get_inner_types st v with
- | None -> []
- | Some (sty, ety) ->
- let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
- let csty, cety = cic sty, cic ety in
- if Ut.alpha_equivalence csty cety then [] else
- match name with
- | None -> [T.Change (sty, ety, None, e, "")]
- | Some (id, i) ->
- begin match get_entry st id with
- | C.Def _ -> [T.ClearBody (id, "")]
- | C.Decl w ->
- let w = S.lift i w in
- if Ut.alpha_equivalence csty w then []
- else
- [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w);
- T.Change (sty, ety, Some (id, id), e, "")]
- end
-
-let get_intro = function
- | C.Anonymous -> unused_premise
- | C.Name s -> s
-
-let mk_intros st script =
- if st.intros = [] then script else
- let count = List.length st.intros in
- T.Intros (Some count, List.rev st.intros, "") :: 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 =
- 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 (_, _, _, premise) ->
- let script = mk_arg st what in
- let where = Some (premise, name) in
- T.Rewrite (direction, what, where, e, dtext) :: script
- | _ -> assert false
-
-let mk_rewrite st dtext what qs tl direction =
- assert (List.length tl = 5);
- let predicate = List.nth tl 2 in
- let e = Cn.mk_pattern 1 predicate in
- [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
-
-let rec proc_lambda st name v t =
- let entry = Some (name, C.Decl (cic v)) in
- let intro = get_intro name in
- proc_proof (add st entry intro) t
-
-and proc_letin st what name v t =
- let intro = get_intro name in
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let hyp, rqv = match get_inner_types st v with
- | Some (ity, _) ->
- let rqv = match v with
- | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
- mk_fwd_rewrite st dtext intro tl true
- | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl ->
- mk_fwd_rewrite st dtext intro tl false
- | v ->
- let qs = [[T.Id ""]; proc_proof (next st) v] in
- [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 rec is_record = function
+ | [] -> None
+ | `Class (`Record fields) :: _ -> Some fields
+ | _ :: tl -> is_record tl
+
+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 =
+ if List.mem G.IPComments params then
+ Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ else
+ ""