X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=da20856d2694a5152b8561d5b5a56751356d92fe;hb=ab06d9617b863a42a49f9a407694a9605f500b98;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..da20856d2 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 @@ -105,6 +105,8 @@ let is_big_general countterm p = (match prem.Con.premise_binder with Some s -> current_size + (String.length s) | None -> current_size + 7) + | Con.Lemma lemma -> + current_size + (String.length lemma.Con.lemma_name) | Con.Term t -> countterm current_size t | Con.ArgProof p -> countp current_size p | Con.ArgMethod s -> (maxsize + 1)) in @@ -115,35 +117,45 @@ let is_big_general countterm p = let is_big = is_big_general (Cexpr2pres.countterm) ;; -let make_row items concl = +let get_xref = + let module Con = Content in + function + `Declaration d + | `Hypothesis d -> d.Con.dec_id + | `Proof p -> p.Con.proof_id + | `Definition d -> d.Con.def_id + | `Joint jo -> jo.Con.joint_id +;; + +let make_row ?(attrs=[]) items concl = let module P = Mpresentation in (match concl with P.Mtable _ -> (* big! *) - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]); P.Mtr ([],[P.Mtd ([],P.indented concl)])]) | _ -> (* small *) - P.Mrow([],items@[P.Mspace([None,"width","0.1cm"]);concl])) + P.Mrow(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl])) ;; -let make_concl verb concl = +let make_concl ?(attrs=[]) verb concl = let module P = Mpresentation in (match concl with P.Mtable _ -> (* big! *) - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]); P.Mtr ([],[P.Mtd ([],P.indented concl)])]) | _ -> (* small *) - P.Mrow([], + P.Mrow(attrs, [P.Mtext([None,"mathcolor","Red"],verb); P.Mspace([None,"width","0.1cm"]); 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 @@ -153,14 +165,16 @@ let make_args_for_apply term2pres args = (match prem.Con.premise_binder with None -> "previous" | Some s -> s) in - P.Mi([],name)::row + P.smallskip::P.Mi([],name)::row + | Con.Lemma lemma -> + P.smallskip::P.Mi([],lemma.Con.lemma_name)::row | Con.Term t -> if is_first then (term2pres t)::row - else P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row + else P.smallskip::P.Mi([],"_")::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row) in + P.smallskip::P.Mi([],"_")::row) in match args with hd::tl -> make_arg_for_apply true hd @@ -168,7 +182,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 +197,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 = @@ -201,12 +215,6 @@ and proof2pres term2pres p = let presacontext = acontext2pres p.Con.proof_apply_context presconclude indent in context2pres p.Con.proof_context presacontext in -(* - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], - (context2pres_old p.Con.proof_context)@ - (acontext2pres_old p.Con.proof_apply_context indent)@ - [conclude2pres_old p.Con.proof_conclude indent]) in *) match p.Con.proof_name with None -> body | Some name -> @@ -215,31 +223,30 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO PROOF!!!") | Some c -> c) in let action = - P.Maction([None,"actiontype","toggle"], + P.Maction([None,"actiontype","toggle" ; + None,"selection","1"], [(make_concl "proof of" ac); body]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], + None,"columnalign","left";Some "helm", "xref", p.Con.proof_id], [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); P.Mtr ([],[P.Mtd ([], P.indented action)])]) and context2pres c continuation = + (* we generate a subtable for each context element, for selection + purposes *) let module P = Mpresentation in List.fold_right (fun ce continuation -> + let xref = get_xref ce in P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd ([],ce2pres ce)]); + None,"columnalign","left"; Some "helm", "xref", xref ], + [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]); P.Mtr([],[P.Mtd ([], continuation)])])) c continuation - and context2pres_old c = - let module P = Mpresentation in - List.map - (function ce -> P.Mtr ([], [P.Mtd ([], ce2pres ce)])) c - 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 @@ -283,6 +290,7 @@ and proof2pres term2pres p = P.Mtext ([],"jointdef") and acontext2pres ac continuation indent = + let module Con = Content in let module P = Mpresentation in List.fold_right (fun p continuation -> @@ -292,20 +300,10 @@ and proof2pres term2pres p = else proof2pres p in P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd ([],hd)]); + None,"columnalign","left"; Some "helm","xref",p.Con.proof_id], + [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]); P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation - and acontext2pres_old ac indent = - let module P = Mpresentation in - List.map - (function p -> - if indent then - P.Mtr ([], [P.Mtd ([], P.indented (proof2pres p))]) - else - P.Mtr ([], - [P.Mtd ([], proof2pres p)])) ac - and conclude2pres conclude indent = let module P = Mpresentation in if indent then @@ -313,16 +311,8 @@ and proof2pres term2pres p = else conclude_aux conclude - and conclude2pres_old conclude indent = - let module P = Mpresentation in - if indent then - P.Mtr ([], [P.Mtd ([], P.indented (conclude_aux conclude))]) - else - P.Mtr ([], - [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 = @@ -338,7 +328,7 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO SYNTH!!!") | Some c -> (term2pres c)) in P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id], [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]); P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]); P.Mtr([],[P.Mtd([],proof2pres subproof)])]) @@ -347,7 +337,9 @@ and proof2pres term2pres p = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"NO Conclusion!!!") | Some c -> term2pres c) in - make_concl "that is equivalent to" conclusion + make_concl + ~attrs:[Some "helm", "xref", conclude.Con.conclude_id] + "that is equivalent to" conclusion else if conclude.Con.conclude_method = "Exact" then let conclusion = (match conclude.Con.conclude_conclusion with @@ -357,7 +349,7 @@ and proof2pres term2pres p = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t | _ -> assert false) in - make_row + make_row ~attrs:[Some "helm", "xref", conclude.Con.conclude_id] [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion else if conclude.Con.conclude_method = "Intros+LetTac" then let conclusion = @@ -368,7 +360,8 @@ and proof2pres term2pres p = [Con.ArgProof p] -> P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], + None,"columnalign","left"; + Some "helm", "xref", conclude.Con.conclude_id], [P.Mtr([],[P.Mtd([],proof2pres p)]); P.Mtr([],[P.Mtd([], (make_concl "we proved *" conclusion))])]); @@ -393,7 +386,8 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO Conclusion!!!") | Some c -> term2pres c) in P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; - None,"columnalign","left"], + None,"columnalign","left"; + Some "helm", "xref", conclude.Con.conclude_id], [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ P.Mtext([None,"mathcolor","Red"],"rewrite"); P.Mspace([None,"width","0.1cm"]);term1; @@ -415,12 +409,13 @@ and proof2pres term2pres p = let concl = (term2pres t) in let ann_concl = make_concl "we proved" concl in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], + None,"columnalign","left"; + Some "helm", "xref", conclude.Con.conclude_id], [P.Mtr ([],[P.Mtd ([],by)]); P.Mtr ([],[P.Mtd ([],ann_concl)])]) else let body = P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id], [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); P.Mtr ([], [P.Mtd ([], @@ -446,12 +441,14 @@ 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) + P.Mtext ([],"aux " ^ n) | Con.Premise prem -> P.Mtext ([],"premise") + | Con.Lemma lemma -> + P.Mtext ([],"lemma") | Con.Term t -> term2pres t | Con.ArgProof p -> @@ -461,7 +458,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???") @@ -469,7 +466,7 @@ and proof2pres term2pres p = let inductive_arg,args_for_cases = (match conclude.Con.conclude_args with Con.Aux(n)::_::tl -> - let l1,l2 = split n tl in + let l1,l2 = split (int_of_string n) tl in let last_pos = (List.length l2)-1 in List.nth l2 last_pos,l1 | _ -> assert false) in @@ -482,6 +479,7 @@ and proof2pres term2pres p = (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 -> @@ -507,7 +505,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 = @@ -547,7 +545,7 @@ and proof2pres term2pres p = | Some t -> term2pres t) in let asubconcl = P.Mtr([],[P.Mtd([], - make_concl "the thesis becomes" subconcl)]) in + P.indented (make_concl "the thesis becomes" subconcl))]) in let induction_hypothesis = (match indhyps with [] -> [] @@ -578,7 +576,9 @@ and proof2pres term2pres p = acontext2pres_old p.Con.proof_apply_context true in *) let body = conclude2pres p.Con.proof_conclude true in let presacontext = - acontext2pres p.Con.proof_apply_context body true in + P.Maction([None,"actiontype","toggle" ; None,"selection","1"], + [P.indented (P.Mtext([None,"mathcolor","Red"],"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@ @@ -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,83 @@ 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 [] + (* Conjectures are in their own table to make *) + (* diffing the DOM trees easier. *) + (P.Mtable + [None,"align","baseline 1"; + None,"equalrows","false"; + None,"columnalign","left"] + ((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 ;;