X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=dfb742810c6d2525cd255443ebf517e7031129fe;hb=dbe67869a0f4842a21e6ee9f82e7ec938969a090;hp=c2d10e5199818b524612a44064e41496269dc01e;hpb=4a01e6197e070d3eff7a3fe02180597136d81eba;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index c2d10e519..dfb742810 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -42,7 +42,7 @@ let rec split n l = let is_big_general countterm p = let maxsize = Cexpr2pres.maxsize in - let module Con = Cic2content in + let module Con = Content in let rec countp current_size p = if current_size > maxsize then current_size else @@ -143,7 +143,7 @@ let make_concl verb concl = ;; let make_args_for_apply term2pres args = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in let rec make_arg_for_apply is_first arg row = (match arg with @@ -168,7 +168,7 @@ let make_args_for_apply term2pres args = | _ -> assert false;; let rec justification term2pres p = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or ((p.Con.proof_context = []) & @@ -183,7 +183,7 @@ let rec justification term2pres p = and proof2pres term2pres p = let rec proof2pres p = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in let indent = let is_decl e = @@ -239,7 +239,7 @@ and proof2pres term2pres p = and ce2pres = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function `Declaration d -> (match d.Con.dec_name with @@ -322,7 +322,7 @@ and proof2pres term2pres p = [P.Mtd ([], conclude_aux conclude)]) and conclude_aux conclude = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in if conclude.Con.conclude_method = "TD_Conversion" then let expected = @@ -446,7 +446,7 @@ and proof2pres term2pres p = and arg2pres = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function Con.Aux n -> P.Mtext ([],"aux " ^ string_of_int n) @@ -461,7 +461,7 @@ and proof2pres term2pres p = and byinduction conclude = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"No conclusion???") @@ -507,7 +507,7 @@ and proof2pres term2pres p = and make_case = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function Con.ArgProof p -> let name = @@ -591,20 +591,22 @@ proof2pres p exception ToDo;; let content2pres term2pres (id,params,metasenv,obj) = - let module Con = Cic2content 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 ;;