X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=1429826479f0cd5f87f6f715ca931eeab8e09aa9;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=dfb742810c6d2525cd255443ebf517e7031129fe;hpb=dbe67869a0f4842a21e6ee9f82e7ec938969a090;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index dfb742810..142982647 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -32,6 +32,18 @@ (* *) (***************************************************************************) +module P = Mpresentation +module B = Box + +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 = @@ -41,7 +53,7 @@ let rec split n l = let is_big_general countterm p = - let maxsize = Cexpr2pres.maxsize in + let maxsize = Ast2pres.maxsize in let module Con = Content in let rec countp current_size p = if current_size > maxsize then current_size @@ -105,6 +117,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 @@ -112,60 +126,69 @@ let is_big_general countterm p = (size > maxsize) ;; -let is_big = is_big_general (Cexpr2pres.countterm) +let is_big = is_big_general (Ast2pres.countterm) ;; -let make_row items concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - P.Mtable ([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])) +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_concl verb concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - P.Mtable ([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.Mtext([None,"mathcolor","Red"],verb); - P.Mspace([None,"width","0.1cm"]); - concl])) +let make_row ?(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 = + 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 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.Mi([],name)::row + (B.b_object (P.Mi ([], name)))::row + | Con.Lemma lemma -> + (B.b_object (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 (B.b_object (P.Mi([],"_")))::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.Mspace([None,"width","0.1cm"])::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;; + (B.b_object (P.Mi([],"_")))::row + in + 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 rec justification term2pres p = let module Con = Content in @@ -176,15 +199,14 @@ let rec justification term2pres p = (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 @@ -192,64 +214,82 @@ and proof2pres term2pres p = | `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 in + 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 -(* - 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 -> - let ac = - (match concl with - None -> P.Mtext([],"NO PROOF!!!") - | Some c -> c) in let action = - P.Maction([None,"actiontype","toggle"], - [(make_concl "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)])]) + 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 = - let module P = Mpresentation in - List.fold_right - (fun ce continuation -> - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[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 + (* 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 *) + match c with + [] -> continuation + | hd::tl -> + let continuation' = + List.fold_right + (fun ce continuation -> + let xref = get_xref ce 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 + 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 = let module Con = Content in - function + 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) @@ -257,69 +297,75 @@ 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.Mtext([],"("); - P.Mi ([],s); - P.Mtext([],")"); - 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) - | `Proof p -> proof2pres p + | `Proof p -> + proof2pres p | `Definition d -> (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([]," = "); + B.H ([], + [B.Text([],"Let "); + 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 P = Mpresentation in + let module Con = Content 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"], - [P.Mtr([],[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 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 = + and conclude2pres conclude indent omit_conclusion = + let module Con = Content in let module P = Mpresentation in - if indent then - P.indented (conclude_aux conclude) + let tconclude_body = + match conclude.Con.conclude_conclusion with + 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 = + if conclude.Con.conclude_method = "TD_Conversion" then + make_concl "that is equivalent to" concl + else make_concl "we conclude" concl in + B.V ([], [conclude_body; ann_concl]) + | _ -> conclude_aux conclude in + if indent then + B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], + [tconclude_body])) else - conclude_aux conclude + B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - 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 = Content in @@ -327,7 +373,7 @@ and proof2pres term2pres p = 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 @@ -335,46 +381,61 @@ 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 - let conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in - make_concl "that is equivalent to" conclusion + assert false else if conclude.Con.conclude_method = "Exact" then - let conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in let arg = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t - | _ -> assert false) in - make_row - [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion + | [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 -> + B.b_h [] [B.b_kw "Consider"; B.b_space; arg] + | Some c -> let conclusion = term2pres c in + make_row + [arg; B.b_space; B.Text([],"proves")] + conclusion + ) else if conclude.Con.conclude_method = "Intros+LetTac" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2pres p + | _ -> assert false) +(* 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([], - (make_concl "we proved *" conclusion))])]); + [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 + 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 @@ -387,89 +448,92 @@ and proof2pres term2pres p = let term2 = (match List.nth conclude.Con.conclude_args 5 with Con.Term t -> term2pres t - | _ -> assert false) in - 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" conclusion)])]) + | _ -> assert false) in + 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 - 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" concl in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [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"], - [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))))])]) in - match conclude.Con.conclude_conclusion with - None -> body - | Some t -> - 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"], - [P.Mtr ([],[P.Mtd ([],body)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) - - and args2pres l = - let module P = Mpresentation in - List.map - (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l + make_args_for_apply term2pres conclude.Con.conclude_args in + B.H([], + (B.b_kw "by"):: + B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")]) + else + B.V + ([], + [B.Text([],"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 " ^ string_of_int n) + B.Text ([],"aux " ^ n) | Con.Premise prem -> - P.Mtext ([],"premise") + B.Text ([],"premise") + | Con.Lemma lemma -> + B.Text ([],"lemma") | Con.Term t -> term2pres t | Con.ArgProof p -> proof2pres p | Con.ArgMethod s -> - P.Mtext ([],"method") + B.Text ([],"method") + and case conclude = + let module Con = Content in + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> B.Text([],"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.Text ([],"an aux???") + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> B.Text ([],"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.Text ([],"a proof???") + | Con.ArgMethod s -> + B.Text ([],"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.Text([],"No conclusion???") | Some t -> term2pres t) in 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 @@ -477,43 +541,36 @@ and proof2pres term2pres p = let arg = (match inductive_arg with Con.Aux n -> - P.Mtext ([],"an aux???") + B.Text ([],"an aux???") | Con.Premise prem -> (match prem.Con.premise_binder with - None -> P.Mtext ([],"the previous result") - | Some n -> P.Mi([],n)) + None -> B.Text ([],"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???") + B.Text ([],"a proof???") | Con.ArgMethod s -> - P.Mtext ([],"a method???")) in - (make_concl "we proceede by induction on" arg) in + B.Text ([],"a method???")) in + (make_concl "we proceed by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - let we_proved = - (make_concl "we proved" 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 - (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.Text([],"no name for case!!") + | Some n -> B.Object ([], P.Mi([],n))) in let indhyps,args = List.partition (function @@ -530,31 +587,28 @@ 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.Text([],"Case")::B.b_space::name::pattern_aux)@ + [B.b_space; + B.Text([],"->")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion!!!") + None -> B.Text([],"No conclusion!!!") | Some t -> term2pres t) in - let asubconcl = - P.Mtr([],[P.Mtd([], - 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 + B.indent (B.Text([],"by induction hypothesis we know:")) in let make_hyp = function `Hypothesis h -> @@ -562,134 +616,329 @@ and proof2pres term2pres p = (match h.Con.dec_name with None -> "no name" | Some s -> s) in - P.indented (P.Mrow ([], - [P.Mtext([],"("); - P.Mi ([],name); - P.Mtext([],")"); - 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 *) - let body = conclude2pres p.Con.proof_conclude true in + let body = conclude2pres p.Con.proof_conclude true false in let presacontext = - 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 + let acontext_id = + match p.Con.proof_apply_context with + [] -> p.Con.proof_conclude.Con.conclude_id + | {Con.proof_id = id}::_ -> id + in + B.Action([None,"type","toggle"], + [B.indent + (B.Text + ([None,"color","red" ; + Some "helm", "xref", acontext_id],"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 -> B.Text([],"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 -> [B.Text([],"Contradiction, hence")] + | Some n -> + [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")]) + | Con.Lemma lemma -> + [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"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 -> B.Text([],"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 -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))]) + | Con.Lemma lemma -> + [(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 -> + let get_name hyp = + (match hyp.Con.dec_name with + None -> "_" + | Some s -> s) in + let preshyp1 = + B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp1)); + B.Text([],")"); + B.skip; + term2pres hyp1.Con.dec_type]) in + let preshyp2 = + 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 + B.V + ([], + [B.H ([],arg@[B.skip; B.Text([],"we have")]); + preshyp1; + B.Text([],"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 -> B.Text([],"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 = + 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 = + 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 + B.V + ([], + [presdecl; + suchthat; + presacontext]); + | _ -> assert false in proof2pres p ;; 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 [] ":=" ; + 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 [] ":=" ; + proof2pres term2pres p]) + (List.rev context)) @ + [ B.b_text [] "|-" ; + 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_text [] + ("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_text [] 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_text [] (ind.Content.inductive_name ^ " of arity "); + 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 [] - (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])]]) - | _ -> 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_text [] ("Proof " ^ name) :: params2pres params); + B.b_text [] "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_text [] ("Definition " ^ name) :: params2pres params); + B.b_text [] "Type:"; + B.indent (term2pres ty)] @ + metasenv2pres term2pres metasenv @ + [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_text [] ("Axiom " ^ name) :: params2pres params); + B.b_text [] "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))) + (Cexpr2pres.cexpr2pres_charcount + (Content_expressions.acic2cexpr ids_to_inner_sorts p))) ;; +*) + +let content2pres ~ids_to_inner_sorts = + content2pres + (fun annterm -> + let (ast, ids_to_uris) as arg = + Acic2Ast.ast_of_acic ids_to_inner_sorts annterm + in + let astBox = Ast2pres.ast2astBox arg in + Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox) +