(* *)
(***************************************************************************)
+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 =
| _ -> 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")]
(make_concl "we proved 1" conclusion))])]);
| _ -> assert false)
*)
+ else if (conclude.Con.conclude_method = "Case") then
+ case conclude
else if (conclude.Con.conclude_method = "ByInduction") then
byinduction conclude
else if (conclude.Con.conclude_method = "Exists") then
| Con.ArgMethod s ->
P.Mtext ([],"method")
+ and case conclude =
+ let module P = Mpresentation in
+ let module Con = Content in
+ let proof_conclusion =
+ (match conclude.Con.conclude_conclusion with
+ None -> P.Mtext([],"No conclusion???")
+ | Some t -> term2pres t) in
+ let arg,args_for_cases =
+ (match conclude.Con.conclude_args with
+ Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
+ arg,tl
+ | _ -> assert false) in
+ let case_on =
+ let case_arg =
+ (match arg with
+ Con.Aux n ->
+ P.Mtext ([],"an aux???")
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> P.Mtext ([],"the previous result")
+ | Some n -> P.Mi([],n))
+ | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name)
+ | Con.Term t ->
+ term2pres t
+ | Con.ArgProof p ->
+ P.Mtext ([],"a proof???")
+ | Con.ArgMethod s ->
+ P.Mtext ([],"a method???")) in
+ (make_concl "we proceede by cases on" case_arg) in
+ let to_prove =
+ (make_concl "to prove" proof_conclusion) in
+ P.Mtable
+ ([None,"align","baseline 1"; None,"equalrows","false";
+ None,"columnalign","left"],
+ P.Mtr ([],[P.Mtd ([],case_on)])::
+ P.Mtr ([],[P.Mtd ([],to_prove)])::
+ (make_cases args_for_cases))
+
and byinduction conclude =
let module P = Mpresentation in
let module Con = Content in
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
;;
(Cexpr2pres.cexpr2pres_charcount
(Content_expressions.acic2cexpr ids_to_inner_sorts p)))
;;
+
projects / helm.git / blobdiff