- match xcno with
- | None -> tname
- | Some cno -> fst (List.nth cs (pred cno))
-with Invalid_argument _ -> failwith "A2P.get_ind_name"
-*)
-let get_inner_types st v =
-try
- let id = Ut.id_of_annterm v in
- try match Hashtbl.find st.types id with
- | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et)
- | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st)
- with Not_found -> None
-with Invalid_argument _ -> failwith "A2P.get_inner_types"
-(*
-let get_inner_sort st v =
-try
- let id = Ut.id_of_annterm v in
- try Hashtbl.find st.sorts id
- with Not_found -> `Type (CicUniv.fresh())
-with Invalid_argument _ -> failwith "A2P.get_sort"
-*)
-let get_type msg st bo =
-try
- let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in
- ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
-(* proof construction *******************************************************)
-
-let unused_premise = "UNUSED"
-
-let convert st ?name v =
- match get_inner_types st v with
- | None -> []
- | Some (st, et) ->
- let cst, cet = cic st, cic et in
- if PER.alpha_equivalence cst cet then [] else
- let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
- match name with
- | None -> [T.Change (st, et, None, e, "")]
- | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
-
-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 (_, _, _, name) as what -> convert st ~name 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
+ ""