(* *)
(***************************************************************************)
+let p_mtr a b = Mpresentation.Mtr(a,b)
+let p_mtd a b = Mpresentation.Mtd(a,b)
+let p_mtable a b = Mpresentation.Mtable(a,b)
+let p_mtext a b = Mpresentation.Mtext(a,b)
+let p_mi a b = Mpresentation.Mi(a,b)
+let p_mo a b = Mpresentation.Mo(a,b)
+let p_mrow a b = Mpresentation.Mrow(a,b)
+let p_mphantom a b = Mpresentation.Mphantom(a,b)
+
+
let rec split n l =
if n = 0 then [],l
else let l1,l2 =
| None ->
prerr_endline "NO NAME!!"; assert false)
| `Proof p ->
- (match p.Con.proof_name with
- Some "w" -> prerr_endline ("processing w");
- | _ -> ());
proof2pres p
| `Definition d ->
(match d.Con.def_name with
let module P = Mpresentation in
let tconclude_body =
match conclude.Con.conclude_conclusion with
- Some t when not omit_conclusion ->
+ Some t when
+ not omit_conclusion or
+ (* CSC: I ignore the omit_conclusion flag in this case. *)
+ (* CSC: Is this the correct behaviour? In the stylesheets *)
+ (* CSC: we simply generated nothing (i.e. the output type *)
+ (* CSC: of the function should become an option. *)
+ conclude.Con.conclude_method = "BU_Conversion" ->
let concl = (term2pres t) in
if conclude.Con.conclude_method = "BU_Conversion" then
make_concl "that is equivalent to" concl
| _ -> assert false) in
(match conclude.Con.conclude_conclusion with
None ->
- P.Mrow []
- [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+ p_mrow []
+ [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
| Some c -> let conclusion = term2pres c in
make_row
[arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
let module P = Mpresentation in
match obj with
`Def (K.Const,thesis,`Proof p) ->
- P.Mtable
+ p_mtable
[None,"align","baseline 1";
None,"equalrows","false";
None,"columnalign","left";
None,"helm:xref","id"]
- ([P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext []
+ ([p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext []
("UNFINISHED PROOF" ^ id ^"(" ^
String.concat " ; " (List.map UriManager.string_of_uri params)^
")")])] ;
- P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext [] "THESIS:"])] ;
- P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mphantom []
- (P.Mtext [] "__") ;
+ p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext [] "THESIS:"])] ;
+ p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mphantom []
+ (p_mtext [] "__") ;
term2pres thesis])]] @
(match metasenv with
None -> []
| Some metasenv' ->
- [P.Mtr []
- [P.Mtd []
+ [p_mtr []
+ [p_mtd []
(* Conjectures are in their own table to make *)
(* diffing the DOM trees easier. *)
- (P.Mtable
+ (p_mtable
[None,"align","baseline 1";
None,"equalrows","false";
None,"columnalign","left"]
- ((P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext [] "CONJECTURES:"])])::
+ ((p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext [] "CONJECTURES:"])])::
List.map
(function
(id,n,context,ty) ->
- P.Mtr []
- [P.Mtd []
- (P.Mrow [Some "helm", "xref", id]
+ p_mtr []
+ [p_mtd []
+ (p_mrow [Some "helm", "xref", id]
(List.map
(function
None ->
- P.Mrow []
- [ P.Mi [] "_" ;
- P.Mo [] ":?" ;
- P.Mi [] "_"]
+ p_mrow []
+ [ p_mi [] "_" ;
+ p_mo [] ":?" ;
+ p_mi [] "_"]
| Some (`Declaration d)
| Some (`Hypothesis d) ->
let
{ K.dec_name = dec_name ;
K.dec_type = ty } = d
in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match dec_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":" ;
+ p_mo [] ":" ;
term2pres ty]
| Some (`Definition d) ->
let
{ K.def_name = def_name ;
K.def_term = bo } = d
in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match def_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":=" ;
+ p_mo [] ":=" ;
term2pres bo]
| Some (`Proof p) ->
let proof_name = p.K.proof_name in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match proof_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":=" ;
+ p_mo [] ":=" ;
proof2pres term2pres p]
) (List.rev context) @
- [ P.Mo [] "|-" ] @
- [ P.Mi [] (string_of_int n) ;
- P.Mo [] ":" ;
+ [ p_mo [] "|-" ] @
+ [ p_mi [] (string_of_int n) ;
+ p_mo [] ":" ;
term2pres ty ]
))
]
) metasenv'
))]]
) @
- [P.Mtr []
- [P.Mtd []
- (P.Mrow []
+ [p_mtr []
+ [p_mtd []
+ (p_mrow []
[proof2pres term2pres p])]])
| _ -> raise ToDo
;;