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/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index 257d2440ba87b66c93e6863f660e715318bb0d35..681f3cd541312e8dff3e86e475cfe3e89aa0db7d 100644 (file)
--- a/components/acic_content/termAcicContent.ml
+++ b/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/components/acic_content/termAcicContent.mli b/components/acic_content/termAcicContent.mli
index 49358bfce00a8b546e71c787b1afc1c68fbaa4b6..def5b0a1bb9a6834d24d60d61cce87bcbad2072a 100644 (file)
--- a/components/acic_content/termAcicContent.mli
+++ b/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/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml
index 477697580fd4df83314ad345634a798b47870237..b9e89769472371c31b3a27e4ae8beedf1db53c49 100644 (file)
--- a/components/content_pres/content2pres.ml
+++ b/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/components/content_pres/sequent2pres.ml b/components/content_pres/sequent2pres.ml
index 2ae090bb01e1d2f0a0040c21fa7d162bdacde7c4..d9c3a325e808a7d531dddd37d2a9be124ff1a967 100644 (file)
--- a/components/content_pres/sequent2pres.ml
+++ b/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/components/content_pres/sequent2pres.mli b/components/content_pres/sequent2pres.mli
index 615c8e35f2cc5be590e0a0346db3c269b613d6d8..d6d9daa4005918fbe6892eb920679190e940492d 100644 (file)
--- a/components/content_pres/sequent2pres.mli
+++ b/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/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index fa5c77d7170928091cbd50a29917b9fc40ec883c..b5db34d17c8b852bdd2ca9988f10dd46feb4ed0b 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/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/matita/applyTransformation.ml b/matita/applyTransformation.ml
index 19a40960774ff0ad6a4c6bbc00d28e58bf692321..0309cf5930f757be60dcd3fb5aabb5a2e38f018d 100644 (file)
--- a/matita/applyTransformation.ml
+++ b/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/matita/applyTransformation.mli b/matita/applyTransformation.mli
index 7156d986706b90262b0480951a43b328a85ecb1c..788ef6810979f88531e7269cf0c64ad744627b85 100644 (file)
--- a/matita/applyTransformation.mli
+++ b/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/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 5c0bc953440814feedad53cfc395253fe35b49fc..f17d2f35673a85a4cd33fff658260224b68b205e 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/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