X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=c0cdc5c0f0f0c289cc07afd85c1127161b25d2d8;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=1616c21c8273d0bf15b9fc4ba39948a3e328e8c4;hpb=60951dd6218b8436830723dc10d4aed7b6894855;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 1616c21c8..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 = @@ -157,29 +167,34 @@ let make_concl ?(attrs=[]) verb concl = let make_args_for_apply term2pres args = let module Con = Content in let module P = Mpresentation in - let rec make_arg_for_apply is_first arg row = - (match arg with + let make_arg_for_apply is_first arg row = + let res = + match arg with Con.Aux n -> assert false | Con.Premise prem -> let name = (match prem.Con.premise_binder with None -> "previous" | Some s -> s) in - P.smallskip::P.Mi([],name)::row + P.Mi([],name)::row | Con.Lemma lemma -> - P.smallskip::P.Mi([],lemma.Con.lemma_name)::row + P.Mi([],lemma.Con.lemma_name)::row | Con.Term t -> if is_first then (term2pres t)::row - else P.smallskip::P.Mi([],"_")::row + else P.Mi([],"_")::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.smallskip::P.Mi([],"_")::row) in - match args with - hd::tl -> - make_arg_for_apply true hd - (List.fold_right (make_arg_for_apply false) tl []) - | _ -> assert false;; + P.Mi([],"_")::row + in + if is_first then res else P.smallskip::res + in + match args with + hd::tl -> + make_arg_for_apply true hd + (List.fold_right (make_arg_for_apply false) tl []) + | _ -> assert false +;; let rec justification term2pres p = let module Con = Content in @@ -231,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"], @@ -290,14 +306,15 @@ and proof2pres term2pres p = P.Mrow ([], [P.Mtext([None,"mathcolor","Red"],"Suppose"); P.Mspace([None,"width","0.1cm"]); - P.Mtext([],"("); + P.Mo([],"("); P.Mi ([],s); - P.Mtext([],")"); + P.Mo([],")"); P.Mspace([None,"width","0.1cm"]); ty]) | None -> prerr_endline "NO NAME!!"; assert false) - | `Proof p -> proof2pres p + | `Proof p -> + proof2pres p | `Definition d -> (match d.Con.def_name with Some s -> @@ -332,13 +349,25 @@ 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 + else if conclude.Con.conclude_method = "FalseInd" then + (* false ind is in charge to add the conclusion *) + falseind conclude else let conclude_body = conclude_aux conclude in - let ann_concl = make_concl "we conclude" concl in + let ann_concl = + if conclude.Con.conclude_method = "TD_Conversion" then + make_concl "that is equivalent to" concl + else make_concl "we conclude" concl in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],conclude_body)]); @@ -381,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")] @@ -407,8 +436,16 @@ 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 + exists conclude + else if (conclude.Con.conclude_method = "AndInd") then + andind conclude + else if (conclude.Con.conclude_method = "FalseInd") then + falseind conclude else if (conclude.Con.conclude_method = "Rewrite") then let justif = (match (List.nth conclude.Con.conclude_args 6) with @@ -431,21 +468,6 @@ and proof2pres term2pres p = P.Mtext([None,"mathcolor","Red"],"with"); P.Mspace([None,"width","0.1cm"]);term2]))]); P.Mtr ([],[P.Mtd ([],P.indented justif)])]); -(* OLD CODE - let conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in - P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ - P.Mtext([None,"mathcolor","Red"],"rewrite"); - P.Mspace([None,"width","0.1cm"]);term1; - P.Mspace([None,"width","0.1cm"]); - P.Mtext([None,"mathcolor","Red"],"with"); - P.Mspace([None,"width","0.1cm"]);term2]))]); - P.Mtr ([],[P.Mtd ([],P.indented justif)]); - P.Mtr ([],[P.Mtd ([],make_concl "we proved 2" conclusion)])]) *) else if conclude.Con.conclude_method = "Apply" then let pres_args = make_args_for_apply term2pres conclude.Con.conclude_args in @@ -453,21 +475,6 @@ and proof2pres term2pres p = P.Mtext([None,"mathcolor","Red"],"by"):: P.Mspace([None,"width","0.1cm"]):: P.Mo([],"(")::pres_args@[P.Mo([],")")]) -(* OLD CODE - let by = - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) in - match conclude.Con.conclude_conclusion with - None -> P.Mrow([],[P.Mtext([],"QUA");by]) - | Some t -> - let concl = (term2pres t) in - let ann_concl = make_concl "we proved 3" concl in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; - Some "helm", "xref", conclude.Con.conclude_id], - [P.Mtr ([],[P.Mtd ([],by)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) *) else P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], @@ -479,16 +486,6 @@ and proof2pres term2pres p = ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], args2pres conclude.Con.conclude_args))))])]) -(* OLD CODE - match conclude.Con.conclude_conclusion with - None -> body - | Some t -> - let concl = (term2pres t) in - let ann_concl = make_concl "we proved 4" concl in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],body)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) *) and args2pres l = let module P = Mpresentation in @@ -512,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 @@ -551,16 +586,7 @@ and proof2pres term2pres p = P.Mtr ([],[P.Mtd ([],induction_on)]):: P.Mtr ([],[P.Mtd ([],to_prove)]):: (make_cases args_for_cases)) -(* OLD CODE - let we_proved = - (make_concl "we proved 5" proof_conclusion) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - P.Mtr ([],[P.Mtd ([],induction_on)]):: - P.Mtr ([],[P.Mtd ([],to_prove)]):: - (make_cases args_for_cases) @ - [P.Mtr ([],[P.Mtd ([],we_proved)])]) *) - + and make_cases args_for_cases = let module P = Mpresentation in List.map @@ -624,9 +650,9 @@ and proof2pres term2pres p = None -> "no name" | Some s -> s) in P.indented (P.Mrow ([], - [P.Mtext([],"("); + [P.Mo([],"("); P.Mi ([],name); - P.Mtext([],")"); + P.Mo([],")"); P.Mspace([None,"width","0.1cm"]); term2pres h.Con.dec_type])) | _ -> assert false in @@ -639,14 +665,157 @@ 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"], pattern::asubconcl::induction_hypothesis@ [P.Mtr([],[P.Mtd([],presacontext)])]) - | _ -> assert false in + | _ -> assert false + + and falseind 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 case_arg = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;case_arg] -> case_arg + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + let arg = + (match case_arg with + Con.Aux n -> assert false + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> [P.Mtext([],"Contradiction, hence")] + | Some n -> + [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")]) + | Con.Lemma lemma -> + [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")] + | _ -> assert false) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + make_row arg proof_conclusion + + and andind 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 proof,case_arg = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + let arg = + (match case_arg with + Con.Aux n -> assert false + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> [] + | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)]) + | Con.Lemma lemma -> + [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)] + | _ -> assert false) in + match proof.Con.proof_context with + `Hypothesis hyp1::`Hypothesis hyp2::tl -> + let get_name hyp = + (match hyp.Con.dec_name with + None -> "_" + | Some s -> s) in + let preshyp1 = + P.Mrow ([], + [P.Mtext([],"("); + P.Mi([],get_name hyp1); + P.Mtext([],")"); + P.smallskip; + term2pres hyp1.Con.dec_type]) in + let preshyp2 = + P.Mrow ([], + [P.Mtext([],"("); + P.Mi([],get_name hyp2); + P.Mtext([],")"); + P.smallskip; + term2pres hyp2.Con.dec_type]) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + let body = conclude2pres proof.Con.proof_conclude false true in + let presacontext = + acontext2pres proof.Con.proof_apply_context body false in + P.Mtable + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr ([],[P.Mtd ([], + P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]); + P.Mtr ([],[P.Mtd ([],preshyp1)]); + P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]); + P.Mtr ([],[P.Mtd ([],preshyp2)]); + P.Mtr ([],[P.Mtd ([],presacontext)])]); + | _ -> assert false + + and exists 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 proof = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;Con.ArgProof proof;_] -> proof + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + match proof.Con.proof_context with + `Declaration decl::`Hypothesis hyp::tl + | `Hypothesis decl::`Hypothesis hyp::tl -> + let get_name decl = + (match decl.Con.dec_name with + None -> "_" + | Some s -> s) in + let presdecl = + P.Mrow ([], + [P.Mtext([None,"mathcolor","Red"],"let"); + P.smallskip; + P.Mi([],get_name decl); + P.Mtext([],":"); term2pres decl.Con.dec_type]) in + let suchthat = + P.Mrow ([], + [P.Mtext([None,"mathcolor","Red"],"such that"); + P.smallskip; + P.Mtext([],"("); + P.Mi([],get_name hyp); + P.Mtext([],")"); + P.smallskip; + term2pres hyp.Con.dec_type]) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + let body = conclude2pres proof.Con.proof_conclude false true in + let presacontext = + acontext2pres proof.Con.proof_apply_context body false in + P.Mtable + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr ([],[P.Mtd ([],presdecl)]); + P.Mtr ([],[P.Mtd ([],suchthat)]); + P.Mtr ([],[P.Mtd ([],presacontext)])]); + | _ -> assert false in proof2pres p ;; @@ -658,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 [] "_"] - | (_,Some (`Declaration d)) - | (_,Some (`Hypothesis d)) -> + 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 [] + p_mrow [] + [ p_mi [] (match dec_name with None -> "_" | Some n -> n) ; - P.Mo [] ":" ; + p_mo [] ":" ; term2pres ty] - | (_,Some (`Definition d)) -> + | 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)) -> + | 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 ;; @@ -765,3 +934,4 @@ let content2pres ~ids_to_inner_sorts = (Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr ids_to_inner_sorts p))) ;; +