X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=ee3e64bd5456d873e0af5f74ca00f2c6213ab5b9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=af3999a3963df8fd1aa714dce8ab6f86c2f394bc;hpb=caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index af3999a39..ee3e64bd5 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2003-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -32,6 +32,10 @@ (* *) (***************************************************************************) +module P = Mpresentation +module B = Box +module Con = Content + 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) @@ -41,132 +45,40 @@ 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 = split (n-1) (List.tl l) in (List.hd l)::l1,l2 -;; +let get_xref = 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 is_big_general countterm p = - let maxsize = Cexpr2pres.maxsize in - let module Con = Content in - let rec countp current_size p = - if current_size > maxsize then current_size - else - let c1 = (countcontext current_size p.Con.proof_context) in - if c1 > maxsize then c1 - else - let c2 = (countapplycontext c1 p.Con.proof_apply_context) in - if c2 > maxsize then c2 - else - countconclude c2 p.Con.proof_conclude - - and - countcontext current_size c = - List.fold_left countcontextitem current_size c - and - countcontextitem current_size e = - if current_size > maxsize then maxsize - else - (match e with - `Declaration d -> - (match d.Con.dec_name with - Some s -> current_size + 4 + (String.length s) - | None -> prerr_endline "NO NAME!!"; assert false) - | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> current_size + 4 + (String.length s) - | None -> prerr_endline "NO NAME!!"; assert false) - | `Proof p -> countp current_size p - | `Definition d -> - (match d.Con.def_name with - Some s -> - let c1 = (current_size + 4 + (String.length s)) in - (countterm c1 d.Con.def_term) - | None -> - prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> maxsize + 1) (* we assume is big *) - and - countapplycontext current_size ac = - List.fold_left countp current_size ac - and - countconclude current_size co = - if current_size > maxsize then current_size - else - let c1 = countargs current_size co.Con.conclude_args in - if c1 > maxsize then c1 - else - (match co.Con.conclude_conclusion with - Some concl -> countterm c1 concl - | None -> c1) - and - countargs current_size args = - List.fold_left countarg current_size args - and - countarg current_size arg = - if current_size > maxsize then current_size - else - (match arg with - Con.Aux _ -> current_size - | Con.Premise prem -> - (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 - let size = (countp 0 p) in - (size > maxsize) -;; - -let is_big = is_big_general (Cexpr2pres.countterm) -;; - -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 (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(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl])) -;; +let hv_attrs = + RenderingAttrs.spacing_attributes `BoxML + @ RenderingAttrs.indent_attributes `BoxML + +let make_row items concl = + B.b_hv hv_attrs (items @ [ concl ]) +(* match concl with + B.V _ -> |+ big! +| + B.b_v attrs [B.b_h [] items; B.b_indent concl] + | _ -> |+ small +| + B.b_h attrs (items@[B.b_space; concl]) *) let make_concl ?(attrs=[]) verb concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - 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(attrs, - [P.Mtext([None,"mathcolor","Red"],verb); - P.Mspace([None,"width","0.1cm"]); - concl])) -;; + B.b_hv (hv_attrs @ attrs) [ B.b_kw verb; concl ] +(* match concl with + B.V _ -> |+ big! +| + B.b_v attrs [ B.b_kw verb; B.b_indent concl] + | _ -> |+ small +| + B.b_h attrs [ B.b_kw verb; B.b_space; concl ] *) let make_args_for_apply term2pres args = - let module Con = Content in - let module P = Mpresentation in let make_arg_for_apply is_first arg row = let res = match arg with @@ -176,95 +88,90 @@ let make_args_for_apply term2pres args = (match prem.Con.premise_binder with None -> "previous" | Some s -> s) in - P.Mi([],name)::row + (B.b_object (P.Mi ([], name)))::row | Con.Lemma lemma -> - P.Mi([],lemma.Con.lemma_name)::row + let lemma_attrs = [ + Some "helm", "xref", lemma.Con.lemma_id; + Some "xlink", "href", lemma.Con.lemma_uri ] + in + (B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row | Con.Term t -> if is_first then (term2pres t)::row - else P.Mi([],"_")::row + else (B.b_object (P.Mi([],"_")))::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.Mi([],"_")::row + (B.b_object (P.Mi([],"_")))::row in - if is_first then res else P.smallskip::res + if is_first then res else B.skip::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 get_name = function + | Some s -> s + | None -> "_" + +let add_xref id = function + | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) + | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) let rec justification term2pres p = - let module Con = Content in - let module P = Mpresentation in if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or ((p.Con.proof_context = []) & (p.Con.proof_apply_context = []) & (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then let pres_args = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) + B.H([], + (B.b_kw "by")::B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")]) else proof2pres term2pres p and proof2pres term2pres p = let rec proof2pres p = - let module Con = Content in - let module P = Mpresentation in - let indent = - let is_decl e = - (match e with - `Declaration _ - | `Hypothesis _ -> true - | _ -> false) in - ((List.filter is_decl p.Con.proof_context) != []) in - let omit_conclusion = (not indent) && (p.Con.proof_context != []) in - let concl = - (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> None - | Some t -> Some (term2pres t)) in - let body = - let presconclude = - conclude2pres p.Con.proof_conclude indent omit_conclusion in - let presacontext = - acontext2pres p.Con.proof_apply_context presconclude indent in - context2pres p.Con.proof_context presacontext in - match p.Con.proof_name with - None -> body - | Some name -> - let action = - match concl with - None -> body -(* - P.Maction - ([None,"actiontype","toggle" ; None,"selection","1"], - [P.Mtext [] "proof" ; body]) -*) - | Some ac -> - P.Maction - ([None,"actiontype","toggle" ; None,"selection","1"], - [(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"], - [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); - P.Mtr ([],[P.Mtd ([], P.indented action)])]) -(* - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - 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)])]) *) + let indent = + let is_decl e = + (match e with + `Declaration _ + | `Hypothesis _ -> true + | _ -> false) in + ((List.filter is_decl p.Con.proof_context) != []) in + let omit_conclusion = (not indent) && (p.Con.proof_context != []) in + let concl = + (match p.Con.proof_conclude.Con.conclude_conclusion with + None -> None + | Some t -> Some (term2pres t)) in + let body = + let presconclude = + conclude2pres p.Con.proof_conclude indent omit_conclusion in + let presacontext = + acontext2pres p.Con.proof_apply_context presconclude indent in + context2pres p.Con.proof_context presacontext in + match p.Con.proof_name with + None -> body + | Some name -> + let action = + match concl with + None -> body + | Some ac -> + B.Action + ([None,"type","toggle"], + [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] + "proof of" ac); body]) + in + B.V ([], + [B.Text ([],"(" ^ name ^ ")"); + B.indent action]) and context2pres c continuation = (* we generate a subtable for each context element, for selection purposes The table generated by the head-element does not have an xref; the whole context-proof is already selectable *) - let module P = Mpresentation in match c with [] -> continuation | hd::tl -> @@ -272,30 +179,42 @@ and proof2pres term2pres p = List.fold_right (fun ce continuation -> let xref = get_xref ce in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; Some "helm", "xref", xref ], - [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]); - P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in + B.V([Some "helm", "xref", xref ], + [B.H([Some "helm", "xref", "ce_"^xref], + [ce2pres_in_proof_context_element ce]); + continuation])) tl continuation in let hd_xref= get_xref hd in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([Some "helm", "xref", "ce_"^hd_xref], - [P.Mtd ([],ce2pres hd)]); - P.Mtr([],[P.Mtd ([], continuation')])]) - - and ce2pres = - let module P = Mpresentation in - let module Con = Content in - function + B.V([], + [B.H([Some "helm", "xref", "ce_"^hd_xref], + [ce2pres_in_proof_context_element hd]); + continuation']) + + and ce2pres_in_joint_context_element = function + | `Inductive _ -> assert false (* TODO *) + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x + | (`Proof _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x + + and ce2pres_in_proof_context_element = function + | `Joint ho -> + B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs)) + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x + | (`Proof _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x + + and ce2pres = + function `Declaration d -> (match d.Con.dec_name with Some s -> let ty = term2pres d.Con.dec_type in - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"Assume"); - P.Mspace([None,"width","0.1cm"]); - P.Mi([],s); - P.Mtext([],":"); + B.H ([], + [(B.b_kw "Assume"); + B.b_space; + B.Object ([], P.Mi([],s)); + B.Text([],":"); ty]) | None -> prerr_endline "NO NAME!!"; assert false) @@ -303,13 +222,13 @@ and proof2pres term2pres p = (match h.Con.dec_name with Some s -> let ty = term2pres h.Con.dec_type in - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"Suppose"); - P.Mspace([None,"width","0.1cm"]); - P.Mo([],"("); - P.Mi ([],s); - P.Mo([],")"); - P.Mspace([None,"width","0.1cm"]); + B.H ([], + [(B.b_kw "Suppose"); + B.b_space; + B.Text([],"("); + B.Object ([], P.Mi ([],s)); + B.Text([],")"); + B.b_space; ty]) | None -> prerr_endline "NO NAME!!"; assert false) @@ -319,34 +238,27 @@ and proof2pres term2pres p = (match d.Con.def_name with Some s -> let term = term2pres d.Con.def_term in - P.Mrow ([], - [P.Mtext([],"Let "); - P.Mi([],s); - P.Mtext([]," = "); - term]) + B.H ([], + [ B.b_kw "Let"; B.b_space; + B.Object ([], P.Mi([],s)); + B.Text([]," = "); + term]) | None -> prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> - P.Mtext ([],"jointdef") and acontext2pres ac continuation indent = - let module Con = Content in - let module P = Mpresentation in List.fold_right (fun p continuation -> let hd = if indent then - P.indented (proof2pres p) + B.indent (proof2pres p) else proof2pres p in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - 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 + B.V([Some "helm","xref",p.Con.proof_id], + [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); + continuation])) ac continuation and conclude2pres conclude indent omit_conclusion = - let module Con = Content in - let module P = Mpresentation in let tconclude_body = match conclude.Con.conclude_conclusion with Some t when @@ -368,25 +280,19 @@ and proof2pres term2pres p = 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)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) + B.V ([], [conclude_body; ann_concl]) | _ -> conclude_aux conclude in if indent then - P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id], + B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], [tconclude_body])) else - P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - + B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) and conclude_aux conclude = - let module Con = Content in - let module P = Mpresentation in if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO EXPECTED!!!") + None -> B.Text([],"NO EXPECTED!!!") | Some c -> term2pres c) in let subproof = (match conclude.Con.conclude_args with @@ -394,27 +300,30 @@ and proof2pres term2pres p = | _ -> assert false) in let synth = (match subproof.Con.proof_conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO SYNTH!!!") + None -> B.Text([],"NO SYNTH!!!") | Some c -> (term2pres c)) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [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)])]) + B.V + ([], + [make_concl "we must prove" expected; + make_concl "or equivalently" synth; + proof2pres subproof]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false else if conclude.Con.conclude_method = "Exact" then let arg = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t - | _ -> assert false) in + | [Con.Premise p] -> + (match p.Con.premise_binder with + | None -> assert false; (* unnamed hypothesis ??? *) + | Some s -> B.Text([],s)) + | err -> assert false) in (match conclude.Con.conclude_conclusion with None -> - p_mrow [] - [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] + B.b_h [] [B.b_kw "Consider"; B.b_space; arg] | Some c -> let conclusion = term2pres c in make_row - [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] + [arg; B.b_space; B.b_kw "proves"] conclusion ) else if conclude.Con.conclude_method = "Intros+LetTac" then @@ -424,18 +333,20 @@ and proof2pres term2pres p = (* OLD CODE let conclusion = (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") + None -> B.Text([],"NO Conclusion!!!") | Some c -> term2pres c) in (match conclude.Con.conclude_args with [Con.ArgProof p] -> - P.Mtable + B.V ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr([],[P.Mtd([],proof2pres p)]); - P.Mtr([],[P.Mtd([], + [B.H([],[B.Object([],proof2pres p)]); + B.H([],[B.Object([], (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 @@ -457,62 +368,69 @@ and proof2pres term2pres p = (match List.nth conclude.Con.conclude_args 5 with Con.Term t -> term2pres t | _ -> assert false) 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)])]); + B.V ([], + [B.H ([],[ + (B.b_kw "rewrite"); + B.b_space; term1; + B.b_space; (B.b_kw "with"); + B.b_space; term2; + B.indent justif])]) else if conclude.Con.conclude_method = "Apply" then let pres_args = make_args_for_apply term2pres conclude.Con.conclude_args in - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by"):: - P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) + B.H([], + (B.b_kw "by"):: + B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")]) else - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); - P.Mtr ([], - [P.Mtd ([], - (P.indented - (P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - args2pres conclude.Con.conclude_args))))])]) - - and args2pres l = - let module P = Mpresentation in - List.map - (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l + B.V ([], [ + B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to"); + (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))]) + + and args2pres l = List.map arg2pres l and arg2pres = - let module P = Mpresentation in - let module Con = Content in function - Con.Aux 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 -> - proof2pres p - | Con.ArgMethod s -> - P.Mtext ([],"method") + Con.Aux n -> B.b_kw ("aux " ^ n) + | Con.Premise prem -> B.b_kw "premise" + | Con.Lemma lemma -> B.b_kw "lemma" + | Con.Term t -> term2pres t + | Con.ArgProof p -> proof2pres p + | Con.ArgMethod s -> B.b_kw "method" + and case conclude = + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> B.b_kw "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 -> B.b_kw "an aux???" + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> B.b_kw "the previous result" + | Some n -> B.Object ([], P.Mi([],n))) + | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) + | Con.Term t -> + term2pres t + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") + in + (make_concl "we proceed by cases on" case_arg) in + let to_prove = + (make_concl "to prove" proof_conclusion) in + B.V ([], case_on::to_prove::(make_cases args_for_cases)) + and byinduction 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???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let inductive_arg,args_for_cases = (match conclude.Con.conclude_args with @@ -524,43 +442,30 @@ and proof2pres term2pres p = let induction_on = let arg = (match inductive_arg with - Con.Aux n -> - P.Mtext ([],"an aux???") + Con.Aux n -> B.b_kw "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) + None -> B.b_kw "the previous result" + | Some n -> B.Object ([], P.Mi([],n))) + | Con.Lemma lemma -> B.Object ([], 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 induction on" arg) in + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") in + (make_concl "we proceed by induction on" 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 ([],induction_on)]):: - P.Mtr ([],[P.Mtd ([],to_prove)]):: - (make_cases args_for_cases)) - - and make_cases args_for_cases = - let module P = Mpresentation in - List.map - (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases + B.V ([], induction_on::to_prove:: (make_cases args_for_cases)) + + and make_cases l = List.map make_case l and make_case = - let module P = Mpresentation in - let module Con = Content in function Con.ArgProof p -> let name = (match p.Con.proof_name with - None -> P.Mtext([],"no name for case!!") - | Some n -> P.Mi([],n)) in + None -> B.b_kw "no name for case!!" + | Some n -> B.Object ([], P.Mi([],n))) in let indhyps,args = List.partition (function @@ -577,31 +482,27 @@ and proof2pres term2pres p = (match h.Con.dec_name with None -> "NO NAME???" | Some n ->n) in - [P.Mspace([None,"width","0.1cm"]); - P.Mi ([],name); - P.Mtext([],":"); + [B.b_space; + B.Object ([], P.Mi ([],name)); + B.Text([],":"); (term2pres h.Con.dec_type)] - | _ -> [P.Mtext ([],"???")]) in + | _ -> [B.Text ([],"???")]) in dec@p) args [] in let pattern = - P.Mtr ([],[P.Mtd ([],P.Mrow([], - P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@ - [P.Mspace([None,"width","0.1cm"]); - P.Mtext([],"->")]))]) in + B.H ([], + (B.b_kw "Case"::B.b_space::name::pattern_aux)@ + [B.b_space; + B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion!!!") + None -> B.b_kw "No conclusion!!!" | Some t -> term2pres t) in - let asubconcl = - P.Mtr([],[P.Mtd([], - P.indented (make_concl "the thesis becomes" subconcl))]) in + let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in let induction_hypothesis = (match indhyps with [] -> [] | _ -> - let text = - P.Mtr([],[P.Mtd([], P.indented - (P.Mtext([],"by induction hypothesis we know:")))]) in + let text = B.indent (B.b_kw "by induction hypothesis we know") in let make_hyp = function `Hypothesis h -> @@ -609,17 +510,14 @@ and proof2pres term2pres p = (match h.Con.dec_name with None -> "no name" | Some s -> s) in - P.indented (P.Mrow ([], - [P.Mo([],"("); - P.Mi ([],name); - P.Mo([],")"); - P.Mspace([None,"width","0.1cm"]); + B.indent (B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")"); + B.b_space; term2pres h.Con.dec_type])) | _ -> assert false in - let hyps = - List.map - (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)])) - indhyps in + let hyps = List.map make_hyp indhyps in text::hyps) in (* let acontext = acontext2pres_old p.Con.proof_apply_context true in *) @@ -630,24 +528,16 @@ and proof2pres term2pres p = [] -> 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" ; - 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)])]) + B.Action([None,"type","toggle"], + [ B.indent (add_xref acontext_id (B.b_kw "Proof")); + acontext2pres p.Con.proof_apply_context body true]) in + B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) | _ -> 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???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let case_arg = (match conclude.Con.conclude_args with @@ -661,21 +551,21 @@ and proof2pres term2pres p = Con.Aux n -> assert false | Con.Premise prem -> (match prem.Con.premise_binder with - None -> [P.Mtext([],"Contradiction, hence")] + None -> [B.b_kw "Contradiction, hence"] | Some n -> - [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")]) + [ B.Object ([],P.Mi([],n)); B.skip; + B.b_kw "is contradictory, hence"]) | Con.Lemma lemma -> - [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")] + [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; + B.b_kw "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???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let proof,case_arg = (match conclude.Con.conclude_args with @@ -690,9 +580,10 @@ and proof2pres term2pres p = | Con.Premise prem -> (match prem.Con.premise_binder with None -> [] - | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)]) + | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))]) | Con.Lemma lemma -> - [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)] + [(B.b_kw "by");B.skip; + B.Object([], P.Mi([],lemma.Con.lemma_name))] | _ -> assert false) in match proof.Con.proof_context with `Hypothesis hyp1::`Hypothesis hyp2::tl -> @@ -701,40 +592,36 @@ and proof2pres term2pres p = None -> "_" | Some s -> s) in let preshyp1 = - P.Mrow ([], - [P.Mtext([],"("); - P.Mi([],get_name hyp1); - P.Mtext([],")"); - P.smallskip; + B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp1)); + B.Text([],")"); + B.skip; term2pres hyp1.Con.dec_type]) in let preshyp2 = - P.Mrow ([], - [P.Mtext([],"("); - P.Mi([],get_name hyp2); - P.Mtext([],")"); - P.smallskip; + B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp2)); + B.Text([],")"); + B.skip; 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)])]); + B.V + ([], + [B.H ([],arg@[B.skip; B.b_kw "we have"]); + preshyp1; + B.b_kw "and"; + preshyp2; + 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???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let proof = (match conclude.Con.conclude_args with @@ -751,146 +638,186 @@ and proof2pres term2pres p = 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 + B.H ([], + [(B.b_kw "let"); + B.skip; + B.Object ([], P.Mi([],get_name decl)); + B.Text([],":"); 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; + B.H ([], + [(B.b_kw "such that"); + B.skip; + B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp)); + B.Text([],")"); + B.skip; 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 + B.V + ([], + [presdecl; + suchthat; + presacontext]); + | _ -> assert false + + in + proof2pres p -proof2pres p -;; +exception ToDo -exception ToDo;; +let counter = ref 0 + +let conjecture2pres term2pres (id, n, context, ty) = + (B.b_h [Some "helm", "xref", id] + (((List.map + (function + | None -> + B.b_h [] + [ B.b_object (p_mi [] "_") ; + B.b_object (p_mo [] ":?") ; + B.b_object (p_mi [] "_")] + | Some (`Declaration d) + | Some (`Hypothesis d) -> + let { Content.dec_name = + dec_name ; Content.dec_type = ty } = d + in + B.b_h [] + [ B.b_object + (p_mi [] + (match dec_name with + None -> "_" + | Some n -> n)); + B.b_text [] ":"; + term2pres ty ] + | Some (`Definition d) -> + let + { Content.def_name = def_name ; + Content.def_term = bo } = d + in + B.b_h [] + [ B.b_object (p_mi [] + (match def_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + term2pres bo] + | Some (`Proof p) -> + let proof_name = p.Content.proof_name in + B.b_h [] + [ B.b_object (p_mi [] + (match proof_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + proof2pres term2pres p]) + (List.rev context)) @ + [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); + B.b_object (p_mi [] (string_of_int n)) ; + B.b_text [] ":" ; + term2pres ty ]))) + +let metasenv2pres term2pres = function + | None -> [] + | Some metasenv' -> + (* Conjectures are in their own table to make *) + (* diffing the DOM trees easier. *) + [B.b_v [] + ((B.b_kw ("Conjectures:" ^ + (let _ = incr counter; in (string_of_int !counter)))) :: + (List.map (conjecture2pres term2pres) metasenv'))] + +let params2pres params = + let param2pres uri = + B.b_text [Some "xlink", "href", UriManager.string_of_uri uri] + (UriManager.name_of_uri uri) + in + let rec spatiate = function + | [] -> [] + | hd :: [] -> [hd] + | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl + in + match params with + | [] -> [] + | p -> + let params = spatiate (List.map param2pres p) in + [B.b_space; + B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])] + +let recursion_kind2pres params kind = + let kind = + match kind with + | `Recursive _ -> "Recursive definition" + | `CoRecursive -> "CoRecursive definition" + | `Inductive _ -> "Inductive definition" + | `CoInductive _ -> "CoInductive definition" + in + B.b_h [] (B.b_kw kind :: params2pres params) + +let inductive2pres term2pres ind = + let constructor2pres decl = + B.b_h [] [ + B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":"); + B.b_space; + term2pres decl.Content.dec_type + ] + in + B.b_v [] + (B.b_h [] [ + B.b_kw (ind.Content.inductive_name ^ " of arity"); + B.smallskip; + term2pres ind.Content.inductive_type ] + :: List.map constructor2pres ind.Content.inductive_constructors) + +let joint_def2pres term2pres def = + match def with + | `Inductive ind -> inductive2pres term2pres ind + | _ -> assert false (* ZACK or raise ToDo? *) let content2pres term2pres (id,params,metasenv,obj) = - let module K = Content in - let module P = Mpresentation in match obj with - `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 ^"(" ^ - 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 [] "__") ; - 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 [Some "helm", "xref", id] - (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] - ) (List.rev context) @ - [ p_mo [] "|-" ] @ - [ p_mi [] (string_of_int n) ; - p_mo [] ":" ; - term2pres ty ] - )) - ] - ) metasenv' - ))]] - ) @ - [p_mtr [] - [p_mtd [] - (p_mrow [] - [proof2pres term2pres p])]]) - | _ -> raise ToDo -;; + | `Def (Content.Const, thesis, `Proof p) -> + let name = get_name p.Content.proof_name in + B.b_v + [Some "helm","xref","id"] + ([ B.b_h [] (B.b_kw ("Proof " ^ name) :: params2pres params); + B.b_kw "Thesis:"; + B.indent (term2pres thesis) ] @ + metasenv2pres term2pres metasenv @ + [proof2pres term2pres p]) + | `Def (_, ty, `Definition body) -> + let name = get_name body.Content.def_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params); + B.b_kw "Type:"; + B.indent (term2pres ty)] @ + metasenv2pres term2pres metasenv @ + [B.b_kw "Body:"; term2pres body.Content.def_term]) + | `Decl (_, `Declaration decl) + | `Decl (_, `Hypothesis decl) -> + let name = get_name decl.Content.dec_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params); + B.b_kw "Type:"; + B.indent (term2pres decl.Content.dec_type)] @ + metasenv2pres term2pres metasenv) + | `Joint joint -> + B.b_v [] + (recursion_kind2pres params joint.Content.joint_kind + :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) + | _ -> raise ToDo let content2pres ~ids_to_inner_sorts = - content2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p))) -;; + content2pres + (fun annterm -> + let ast, ids_to_uris = + CicNotationRew.ast_of_acic ids_to_inner_sorts annterm + in + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris + (CicNotationRew.pp_ast ast))) +