X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=c0cdc5c0f0f0c289cc07afd85c1127161b25d2d8;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=cfa061bfb2e442c93da5457d2fa7545ccf444edc;hpb=7fd0b9edc6be316b4ef43ca98a6b02f76dd1108e;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index cfa061bfb..c0cdc5c0f 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -32,6 +32,16 @@ (* *) (***************************************************************************) +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 = @@ -236,7 +246,8 @@ and proof2pres term2pres p = | Some ac -> P.Maction ([None,"actiontype","toggle" ; None,"selection","1"], - [(make_concl "proof of" ac); body]) + [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] + "proof of" ac); body]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], @@ -303,9 +314,6 @@ and proof2pres term2pres p = | 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 @@ -341,7 +349,13 @@ and proof2pres term2pres p = 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 @@ -396,8 +410,8 @@ and proof2pres term2pres p = | _ -> 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")] @@ -422,6 +436,8 @@ and proof2pres term2pres p = (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 @@ -493,6 +509,44 @@ and proof2pres term2pres p = | 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 @@ -611,8 +665,16 @@ and proof2pres term2pres p = acontext2pres_old p.Con.proof_apply_context true in *) let body = conclude2pres p.Con.proof_conclude true false in let presacontext = + let acontext_id = + match p.Con.proof_apply_context with + [] -> p.Con.proof_conclude.Con.conclude_id + | {Con.proof_id = id}::_ -> id + in P.Maction([None,"actiontype","toggle" ; None,"selection","1"], - [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof")); + [P.indented + (P.Mtext + ([None,"mathcolor","Red" ; + Some "helm", "xref", acontext_id],"Proof")) ; acontext2pres p.Con.proof_apply_context body true]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], @@ -765,103 +827,103 @@ let content2pres term2pres (id,params,metasenv,obj) = 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] - ) context @ - [ P.Mo [] "|-" ] @ - [ P.Mi [] (string_of_int n) ; - P.Mo [] ":" ; + ) (List.rev context) @ + [ 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 ;; @@ -872,3 +934,4 @@ let content2pres ~ids_to_inner_sorts = (Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr ids_to_inner_sorts p))) ;; +