From: Claudio Sacerdoti Coen Date: Sun, 28 Oct 2007 21:56:23 +0000 (+0000) Subject: Pretty-printing of "match ... with" pattern syntax fixed. We need an X-Git-Tag: make_still_working~5929 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b02253b371aadbbb37226a685b9bd8777a64d175;p=helm.git Pretty-printing of "match ... with" pattern syntax fixed. We need an ~output_type flag since the semantics of patterns is slightly different from the semantics of terms (and maybe this was a very bad choice I made): match p return p with [ _ => p | ... | _ => p ] --- diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 257d2440b..681f3cd54 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -70,7 +70,7 @@ let constructor_of_inductive_type uri i j = let left_params_no_of_inductive_type uri = snd (get_types uri) -let ast_of_acic0 term_info acic k = +let ast_of_acic0 ~output_type term_info acic k = let k = k term_info in let id_to_uris = term_info.uri in let register_uri id uri = Hashtbl.add id_to_uris id uri in @@ -196,12 +196,21 @@ let ast_of_acic0 term_info acic k = List.map2 (fun (name, ty) pat -> incr j; - let (capture_variables, rhs) = eat_branch lpsno ty pat in - Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs + let name,(capture_variables,rhs) = + match output_type with + `Term -> name, eat_branch lpsno ty pat + | `Pattern -> "_", ([], k pat) + in + Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs ) constructors patterns with Invalid_argument _ -> assert false in - idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns)) + let indty = + match output_type with + `Pattern -> None + | `Term -> Some case_indty + in + idref id (Ast.Case (k te, indty, Some (k ty), patterns)) | Cic.AFix (id, no, funs) -> let defs = List.map @@ -323,11 +332,12 @@ let instantiate32 term_info idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let rec ast_of_acic1 term_info annterm = +let rec ast_of_acic1 ~output_type term_info annterm = let id_to_uris = term_info.uri in let register_uri id uri = Hashtbl.add id_to_uris id uri in match (get_compiled32 ()) annterm with - | None -> ast_of_acic0 term_info annterm ast_of_acic1 + | None -> + ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type) | Some (env, ctors, pid) -> let idrefs = List.map @@ -341,7 +351,8 @@ let rec ast_of_acic1 term_info annterm = ctors in let env' = - List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env + List.map + (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env in let _, symbol, args, _ = try @@ -357,11 +368,11 @@ let load_patterns32 t = in set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) -let ast_of_acic id_to_sort annterm = +let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic <- " ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in - let ast = ast_of_acic1 term_info annterm in + let ast = ast_of_acic1 ~output_type term_info annterm in debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri diff --git a/helm/software/components/acic_content/termAcicContent.mli b/helm/software/components/acic_content/termAcicContent.mli index 49358bfce..def5b0a1b 100644 --- a/helm/software/components/acic_content/termAcicContent.mli +++ b/helm/software/components/acic_content/termAcicContent.mli @@ -54,6 +54,7 @@ val set_active_interpretations: interpretation_id list -> unit (** {2 acic -> content} *) val ast_of_acic: + output_type:[`Pattern|`Term] -> (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) Cic.annterm -> (* acic *) CicNotationPt.term (* ast *) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 477697580..b9e897694 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -960,7 +960,7 @@ let content2pres content2pres ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) annterm -> let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm + TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres (CicNotationPres.render ids_to_uris ~prec diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml index 2ae090bb0..d9c3a325e 100644 --- a/helm/software/components/content_pres/sequent2pres.ml +++ b/helm/software/components/content_pres/sequent2pres.ml @@ -99,7 +99,7 @@ let sequent2pres ~ids_to_inner_sorts = sequent2pres (fun annterm -> let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm + TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres (CicNotationPres.render ids_to_uris diff --git a/helm/software/components/content_pres/sequent2pres.mli b/helm/software/components/content_pres/sequent2pres.mli index 615c8e35f..d6d9daa40 100644 --- a/helm/software/components/content_pres/sequent2pres.mli +++ b/helm/software/components/content_pres/sequent2pres.mli @@ -36,4 +36,3 @@ val sequent2pres : ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.conjecture -> CicNotationPres.boxml_markup - diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index fa5c77d71..b5db34d17 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -363,25 +363,25 @@ let pattern_of ?(equality=(==)) ~term terms = if b1||b2 then true,Cic.Cast (te, ty) else not_found - | Cic.Prod (name, s, t) -> + | Cic.Prod (_, s, t) -> let b1,s = aux s in let b2,t = aux t in if b1||b2 then - true, Cic.Prod (name, s, t) + true, Cic.Prod (Cic.Anonymous, s, t) else not_found - | Cic.Lambda (name, s, t) -> + | Cic.Lambda (_, s, t) -> let b1,s = aux s in let b2,t = aux t in if b1||b2 then - true, Cic.Lambda (name, s, t) + true, Cic.Lambda (Cic.Anonymous, s, t) else not_found - | Cic.LetIn (name, s, t) -> + | Cic.LetIn (_, s, t) -> let b1,s = aux s in let b2,t = aux t in if b1||b2 then - true, Cic.LetIn (name, s, t) + true, Cic.LetIn (Cic.Anonymous, s, t) else not_found | Cic.Appl terms -> diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 19a409607..0309cf593 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -48,8 +48,7 @@ let mml_of_cic_sequent metasenv sequent = in let content_sequent = Acic2content.map_sequent asequent in let pres_sequent = - (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) - in + Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in let xmlpres = mpres_document pres_sequent in (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres, unsh_sequent, @@ -86,20 +85,23 @@ let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent = BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size pres_sequent -let txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv sequent = +let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size + metasenv sequent = let _,(asequent,_,_,ids_to_inner_sorts,_) = Cic2acic.asequent_of_sequent metasenv sequent in let _,_,_,t = Acic2content.map_sequent asequent in - let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in + let t, ids_to_uris = + TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in let t = TermContentPres.pp_ast t in let t = CicNotationPres.render ids_to_uris t in BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size t let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = - let fake_sequent = (-1,context,t) in - txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv fake_sequent + let fake_sequent = (-1,context,t) in + txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size + metasenv fake_sequent ;; ignore ( @@ -148,14 +150,11 @@ let remove_closed_substs s = let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm - in + TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in let bobj = CicNotationPres.box_of_mpres ( CicNotationPres.render ~prec:90 ids_to_uris - (TermContentPres.pp_ast ast) - ) - in + (TermContentPres.pp_ast ast)) in let render = function _::x::_ -> x | _ -> assert false in let mpres = CicNotationPres.mpres_of_box bobj in let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 7156d9867..788ef6810 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -57,13 +57,12 @@ val mml_of_cic_object: val txt_of_cic_term: map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> - string + string val txt_of_cic_sequent: - map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> - string + map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> string val txt_of_cic_sequent_conclusion: - map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> - string + map_unicode_to_tex:bool -> output_type:[`Pattern | `Term] -> int -> + Cic.metasenv -> Cic.conjecture -> string (* columns, rendering style, name prefix, object *) val txt_of_cic_object: diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 5c0bc9534..f17d2f356 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -252,7 +252,7 @@ object (self) match self#get_term_by_id cic_info id with | SelTerm (t, father_hyp) -> let sequent = self#sequent_of_id ~paste_kind:`Pattern id in - let text = self#string_of_cic_sequent sequent in + let text = self#string_of_cic_sequent ~output_type:`Pattern sequent in (match father_hyp with | None -> None, [], Some text | Some hyp_name -> None, [ hyp_name, text ], None) @@ -264,7 +264,7 @@ object (self) match self#get_term_by_id cic_info id with | SelTerm (t, father_hyp) -> let sequent = self#sequent_of_id ~paste_kind:`Term id in - let text = self#string_of_cic_sequent sequent in + let text = self#string_of_cic_sequent ~output_type:`Term sequent in text | SelHyp (hyp_name, _ctxt) -> hyp_name @@ -442,24 +442,14 @@ object (self) | `Term -> self#tactic_text_of_node node else string_of_dom_node node - method private string_of_cic_sequent cic_sequent = + method private string_of_cic_sequent ~output_type cic_sequent = let script = MatitaScript.current () in let metasenv = if script#onGoingProof () then script#proofMetasenv else [] in - (* - let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = - Cic2acic.asequent_of_sequent metasenv cic_sequent in - let _, _, _, annterm = acic_sequent in - let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in - let pped_ast = TermContentPres.pp_ast ast in - let markup = CicNotationPres.render ids_to_uris pped_ast in - BoxPp.render_to_string text_width markup - *) let map_unicode_to_tex = Helm_registry.get_bool "matita.paste_unicode_as_tex" in ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex - text_width metasenv cic_sequent + ~output_type text_width metasenv cic_sequent method private pattern_of term context unsh_sequent = let context_len = List.length context in