From dbe67869a0f4842a21e6ee9f82e7ec938969a090 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Jul 2003 10:19:23 +0000 Subject: [PATCH] Rendering of current proofs completed. --- .../ocaml/cic_transformations/content2pres.ml | 85 ++++++++++++++++--- 1 file changed, 75 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 46585f14c..dfb742810 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -591,20 +591,22 @@ proof2pres p exception ToDo;; let content2pres term2pres (id,params,metasenv,obj) = - let module Con = Content in + let module K = Content in let module P = Mpresentation in match obj with - `Def (Con.Const,thesis,`Proof p) -> + `Def (K.Const,thesis,`Proof p) -> P.Mtable [None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; None,"helm:xref","id"] - [(*P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ params ^ ")")])] ; -*) + ([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 [] @@ -614,11 +616,74 @@ let content2pres term2pres (id,params,metasenv,obj) = (P.Mrow [] [P.Mphantom [] (P.Mtext [] "__") ; - term2pres thesis])] ; - P.Mtr [] + term2pres thesis])]] @ + (match metasenv with + None -> [] + | Some metasenv' -> + (P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mtext [] "CONJECTURES:"])]) :: + List.map + (function + (id,n,context,ty) -> + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + (List.map + (function + (_,None) -> + 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 [] + (match dec_name with + None -> "_" + | Some n -> n) ; + P.Mo [] ":" ; + term2pres ty] + | (_,Some (`Definition d)) -> + let + { K.def_name = def_name ; + K.def_term = bo } = d + in + P.Mrow [] + [ P.Mi [] + (match def_name with + None -> "_" + | Some n -> n) ; + P.Mo [] ":=" ; + term2pres bo] + | (_,Some (`Proof p)) -> + let proof_name = p.K.proof_name in + P.Mrow [] + [ P.Mi [] + (match proof_name with + None -> "_" + | Some n -> n) ; + P.Mo [] ":=" ; + proof2pres term2pres p] + ) context @ + [ P.Mo [] "|-" ] @ + [ P.Mi [] (string_of_int n) ; + P.Mo [] ":" ; + term2pres ty ] + )) + ] + ) metasenv' + ) @ + [P.Mtr [] [P.Mtd [] (P.Mrow [] - [proof2pres term2pres p])]] + [proof2pres term2pres p])]]) | _ -> raise ToDo ;; -- 2.39.2