From e5f4d8fa36a154bbc0a555eefa5ccc0bdb29afb0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Jan 2005 10:31:25 +0000 Subject: [PATCH] rendering fixes: - does not assert false for a missing idref on a symbol (which is not available when rendering ast coming from parsing) - fixed pattern matching rendering --- .../applyTransformation.ml | 47 +---- helm/ocaml/cic_transformations/ast2pres.ml | 51 ++---- .../ocaml/cic_transformations/content2pres.ml | 173 ++++++++++-------- 3 files changed, 131 insertions(+), 140 deletions(-) diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index e1b36ea5c..6eff8d17b 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -48,45 +48,18 @@ let mml_of_cic_sequent metasenv sequent = let pres_sequent = (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in let xmlpres = mpres_document pres_sequent in - (* Xml.pp_to_outchan xmlpres stdout ; *) - try - Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) - with - e -> - prerr_endline ("LUCA: eccezione in document_of_xml " ^ (Printexc.to_string e)) ; - raise e + Xml2Gdome.document_of_xml Misc.domImpl xmlpres, + (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;; let mml_of_cic_object ~explode_all uri acic - ids_to_inner_sorts ids_to_inner_types = - match acic with - Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> - let time1 = Sys.time () in - let content = - Cic2content.annobj2content - ~ids_to_inner_sorts ~ids_to_inner_types acic in - (* ContentPp.print_obj content; *) - let pres = Content2pres.content2pres ~ids_to_inner_sorts content in - let time2 = Sys.time () in - (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) - let xmlpres = mpres_document pres in - let time25 = Sys.time () in - (* alternative: printing to file - prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); - Xml.pp xmlpres (Some "tmp"); - let time3 = Sys.time () in - prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); - end alternative *) - (try - Xml2Gdome.document_of_xml Misc.domImpl xmlpres - with (GdomeInit.DOMException (_,s)) as e -> - prerr_endline s; raise e) - | _ -> assert false + ids_to_inner_sorts ids_to_inner_types += + let content = + Cic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types acic + in + let pres = Content2pres.content2pres ~ids_to_inner_sorts content in + let xmlpres = mpres_document pres in + Xml2Gdome.document_of_xml Misc.domImpl xmlpres ;; -(* -let _ = - Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount -;; -*) - diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index 0eba3757f..c82f0fb8a 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -138,6 +138,12 @@ let append_tail ~tail box = | [] -> box | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail)) +let rec find_symbol idref = function + | A.AttributedTerm (`Loc _, t) -> find_symbol None t + | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t + | A.Symbol (name, _) -> `Symbol (name, idref) + | _ -> `None + let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) (t, ids_to_uris) = @@ -165,19 +171,10 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t | A.Appl [] -> assert false | A.Appl ((hd::tl) as l) -> - let rec find_symbol idref = function - | A.AttributedTerm (`Loc _, t) -> find_symbol None t - | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t - | A.Symbol (name, _) -> - (match idref with - | None -> assert false - | Some idref -> `Symbol (name, idref)) - | _ -> `None - in let aattr = make_attributes [Some "helm","xref"] [xref] in (match find_symbol None hd with | `Symbol (name, sxref) -> - let sattr = make_std_attributes (Some sxref) in + let sattr = make_std_attributes sxref in (try (let f = Hashtbl.find symbol_table_charcount name in f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr) @@ -230,14 +227,15 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) Box.smallskip; Box.Text([],map_tex unicode "Rightarrow"); Box.smallskip; - Box.Object([],rhs)]) in - let plbox = match pl with - [] -> Box.Text([],"[]") + append_tail ~tail (Box.Object([],rhs))]) in + let plbox = + match pl with + [] -> append_tail ~tail (Box.Text([],"[]")) | r::tl -> Box.V([], (make_rule ~tail:[] "[" r) :: (make_args - (fun ~tail pat -> make_rule ~tail:[] "|" pat) + (fun ~tail pat -> make_rule ~tail "|" pat) ~tail:("]" :: tail) tl)) in @@ -245,7 +243,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) match ty with | Some ty -> [ Box.H([],[Box.Text([],"["); - ast2box ~tail ty; + ast2box ~tail:[] ty; Box.Text([],"]")]) ] | None -> [] in @@ -253,7 +251,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) Box.V(make_attributes [Some "helm","xref"] [xref], ty_box @ [Box.Text([],"match"); - Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg])); + Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg])); Box.Text([],"with"); Box.indent plbox]) else @@ -262,7 +260,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) [Box.H(make_attributes [Some "helm","xref"] [xref], [Box.Text([],"match"); Box.smallskip; - ast2box ~tail arg; + ast2box ~tail:[] arg; Box.smallskip; Box.Text([],"with")]); Box.indent plbox]) @@ -273,8 +271,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) let definitions = let rec make_defs let_txt = function [] -> [] - | [(var,s,_)] -> - make_def let_txt var s "in" + | [(var,s,_)] -> make_def let_txt var s "in" | (var,s,_)::tl -> (make_def let_txt var s "")@(make_defs "and" tl) in make_defs "let rec" vars in @@ -474,20 +471,10 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = | A.UserInput -> P.Mtext([], "") | A.Appl [] -> assert false | A.Appl ((hd::tl) as l) -> - let rec find_symbol idref = function - | A.AttributedTerm (`Loc _, t) -> find_symbol None t - | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t - | A.Symbol (name, _) -> - (match idref with - | None -> assert false - | Some idref -> `Symbol (name, idref)) - | term -> - `None - in let aattr = make_attributes [Some "helm","xref"] [xref] in (match find_symbol None hd with | `Symbol (name, sxref) -> - let sattr = make_std_attributes (Some sxref) in + let sattr = make_std_attributes sxref in (try (let f = Hashtbl.find symbol_table name in f tl ~priority ~assoc ~ids_to_uris aattr sattr) @@ -551,7 +538,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = let lhs = P.Mtext([], constr) :: (List.concat - (List.map (fun var -> P.smallskip :: make_capture_variable var) + (List.map + (fun var -> P.smallskip :: make_capture_variable var) vars)) in lhs @ @@ -697,4 +685,5 @@ let _ = (** fill symbol_table *) add_binary_op "times" 70 (`Ascii "*"); add_binary_op "minus" 60 (`Ascii "-"); add_binary_op "div" 60 (`Ascii "/"); + add_binary_op "cast" 80 (`Ascii ":"); diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 1301d1017..29da14591 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -758,80 +758,109 @@ proof2pres p exception ToDo;; -let aaa = ref 0 +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 get_name = function + | Some s -> s + | None -> "_" + +let pp_params = function + | [] -> "" + | params -> + " (" ^ + String.concat " ; " (List.map UriManager.string_of_uri params) ^ + ")" let content2pres term2pres (id,params,metasenv,obj) = - let module K = Content in - match obj with - `Def (K.Const,thesis,`Proof p) -> - B.b_v - [None,"helm:xref","id"] - ([B.b_text [] ("UNFINISHED PROOF " ^ id ^"(" ^ String.concat " ; " (List.map UriManager.string_of_uri params)^ ")") ; - B.b_text [] "THESIS:" ; - B.indent (term2pres thesis)] @ - (match metasenv with - 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 aaa; in (string_of_int !aaa)))):: - (List.map - (function - (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 - { K.dec_name = dec_name ; - K.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 - { K.def_name = def_name ; - K.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.K.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 ]) - )) - ) metasenv')) - )::[proof2pres term2pres p] - ) - ) - | _ -> raise ToDo + match obj with + | `Def (Content.Const, thesis, `Proof p) -> + let name = get_name p.Content.proof_name in + B.b_v + [None,"helm:xref","id"] + ([ B.b_text [] ("Proof " ^ name ^ pp_params 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 + [None,"helm:xref","id"] + ([B.b_text [] ("Definition " ^ name ^ pp_params 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 + [None,"helm:xref","id"] + ([B.b_text [] ("Axiom " ^ name ^ pp_params params); + B.b_text [] "Type:"; + B.indent (term2pres decl.Content.dec_type)] @ + metasenv2pres term2pres metasenv) + | _ -> raise ToDo ;; (* -- 2.39.2