-
-let is_big_general countterm p =
- let maxsize = Ast2pres.maxsize in
- let module Con = Content in
- let rec countp current_size p =
- if current_size > maxsize then current_size
- else
- let c1 = (countcontext current_size p.Con.proof_context) in
- if c1 > maxsize then c1
- else
- let c2 = (countapplycontext c1 p.Con.proof_apply_context) in
- if c2 > maxsize then c2
- else
- countconclude c2 p.Con.proof_conclude
-
- and
- countcontext current_size c =
- List.fold_left countcontextitem current_size c
- and
- countcontextitem current_size e =
- if current_size > maxsize then maxsize
- else
- (match e with
- `Declaration d ->
- (match d.Con.dec_name with
- Some s -> current_size + 4 + (String.length s)
- | None -> prerr_endline "NO NAME!!"; assert false)
- | `Hypothesis h ->
- (match h.Con.dec_name with
- Some s -> current_size + 4 + (String.length s)
- | None -> prerr_endline "NO NAME!!"; assert false)
- | `Proof p -> countp current_size p
- | `Definition d ->
- (match d.Con.def_name with
- Some s ->
- let c1 = (current_size + 4 + (String.length s)) in
- (countterm c1 d.Con.def_term)
- | None ->
- prerr_endline "NO NAME!!"; assert false)
- | `Joint ho -> maxsize + 1) (* we assume is big *)
- and
- countapplycontext current_size ac =
- List.fold_left countp current_size ac
- and
- countconclude current_size co =
- if current_size > maxsize then current_size
- else
- let c1 = countargs current_size co.Con.conclude_args in
- if c1 > maxsize then c1
- else
- (match co.Con.conclude_conclusion with
- Some concl -> countterm c1 concl
- | None -> c1)
- and
- countargs current_size args =
- List.fold_left countarg current_size args
- and
- countarg current_size arg =
- if current_size > maxsize then current_size
- else
- (match arg with
- Con.Aux _ -> current_size
- | Con.Premise prem ->
- (match prem.Con.premise_binder with
- Some s -> current_size + (String.length s)
- | None -> current_size + 7)
- | Con.Lemma lemma ->
- current_size + (String.length lemma.Con.lemma_name)
- | Con.Term t -> countterm current_size t
- | Con.ArgProof p -> countp current_size p
- | Con.ArgMethod s -> (maxsize + 1)) in
- let size = (countp 0 p) in
- (size > maxsize)
-;;
-
-let is_big = is_big_general (Ast2pres.countterm)
-;;
-
-let get_xref =
- let module Con = Content in
- function
- `Declaration d
- | `Hypothesis d -> d.Con.dec_id
- | `Proof p -> p.Con.proof_id
- | `Definition d -> d.Con.def_id
- | `Joint jo -> jo.Con.joint_id
-;;
-
-let make_row ?(attrs=[]) items concl =
- match concl with
- B.V _ -> (* big! *)