From 4e89ae4ac9b001c0479d68d9f74fe81fca6ecd2d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 23 May 2011 10:49:02 +0000 Subject: [PATCH] ... --- .../content_pres/cicNotationParser.ml | 2 +- .../content_pres/cicNotationPres.ml | 61 ++++++++++++++++--- .../content_pres/termContentPres.ml | 6 +- .../ng_cic_content/interpretations.ml | 8 +-- matitaB/matita/applyTransformation.ml | 2 +- matitaB/matita/cicMathView.ml | 2 +- 6 files changed, 63 insertions(+), 18 deletions(-) diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index dc4534c84..82037a1d6 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -108,7 +108,7 @@ let add_symbol_to_grammar_explicit level2_ast_grammar ;Gramext.Stoken ("ATAGEND","")], (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc)) ]]]; - prerr_endline ("adding to grammar symbol " ^ s); +(* prerr_endline ("adding to grammar symbol " ^ s); *) (s,entry)::sym_table diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index 6bcec8edd..7f1470f76 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -87,8 +87,8 @@ let box_of spec attrs children = children in let attrs' = - (if spacing then RenderingAttrs.spacing_attributes `BoxML else []) - @ (if indent then RenderingAttrs.indent_attributes `BoxML else []) + (if spacing then [None, "spacing", "0.5em"] else []) + @ (if indent then [None, "indent", "0.5em"] else []) @ attrs in match kind with @@ -103,7 +103,17 @@ let render status ?(prec=(-1)) = | A.AttributedTerm _ -> aux_attributes [] "" prec t | A.Num (literal, _) -> Box.Text ([], literal) - | A.Symbol (literal, _) -> Box.Text ([], literal) + | A.Symbol (literal, Some (None,desc)) -> + let txt = "" ^ literal ^ "" in + Box.Text ([], to_unicode txt) + | A.Symbol (literal, Some (Some u,desc)) -> + let txt = + "" ^ literal ^ "" in + Box.Text ([], to_unicode txt) + | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal) + | A.Ident (literal, `Uri u) -> + let txt = "" ^ literal ^ "" in + Box.Text ([], to_unicode txt) | A.Ident (literal, _) -> Box.Text ([], to_unicode literal) | A.Meta(n, l) -> let local_context = @@ -194,17 +204,47 @@ let render status ?(prec=(-1)) = | A.InfRule (t1, t2, t3) -> assert false | A.Sqrt t -> assert false | A.Root (t1, t2) -> assert false - | A.Box (a, terms) -> - let children = List.map (aux prec) terms in - Box.H([],children) + | A.Box ((_,spacing,_) as kind, terms) -> + let children = + aux_children spacing prec + (NotationUtil.ungroup terms) + in + box_of kind attrs children | A.Mstyle (l,terms) -> assert false | A.Mpadded (l,terms) -> assert false | A.Maction alternatives -> toggle_action (List.map invoke_reinit alternatives) | A.Group terms -> assert false - | A.Break -> Box.Space [] + | A.Break -> Box.Space [] + and aux_children spacing prec terms = + let find_clusters = + let rec aux_list first clusters acc = + function + [] when acc = [] -> List.rev clusters + | [] -> aux_list first (List.rev acc :: clusters) [] [] + | (A.Layout A.Break) :: tl when acc = [] -> + aux_list first clusters [] tl + | (A.Layout A.Break) :: tl -> + aux_list first (List.rev acc :: clusters) [] tl + | [hd] -> + aux_list false clusters + (aux prec hd :: acc) [] + | hd :: tl -> + aux_list false clusters + (aux prec hd :: acc) tl + in + aux_list true [] [] + in + let boxify_pres = + function + [t] -> t + | tl -> box_of (A.H, spacing, false) [] tl + in + List.map boxify_pres (find_clusters terms) in - aux prec + (fun t -> + prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t)); + aux prec t) (* let render_to_boxml id_to_uri t = let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in @@ -221,14 +261,15 @@ let render_context_entry status name = function render status (TermContentPres.pp_ast status t)]) let render_context status context = - Box.V ([], + Box.V ([], + Box.Space [None, "width", "0.5em"]:: List.map (fun (name,entry) -> render_context_entry status (to_unicode name) entry) context) let render_sequent status (i,context,ty) = Box.V ([], - [render_context status context; + [render_context status (List.rev context); Box.Ink [None,"width","4cm"; None,"height","2px"]; render status (TermContentPres.pp_ast status ty)]) diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index 2b9bc650f..d51e4bf02 100644 --- a/matitaB/components/content_pres/termContentPres.ml +++ b/matitaB/components/content_pres/termContentPres.ml @@ -472,7 +472,8 @@ let rec pp_ast1 status term = let ast_env_of_env env = List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in -(* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *) + prerr_endline ("### pattern matching from 2 to 1 on term " ^ NotationPp.pp_term status term); + let res = match term with | Ast.AttributedTerm (attrs, term') -> Ast.AttributedTerm (attrs, pp_ast1 status term') @@ -489,6 +490,9 @@ let rec pp_ast1 status term = with Not_found -> assert false in instantiate21 idrefs (ast_env_of_env env) l1) + in + prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term status res); + res let load_patterns21 status t = set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t)) diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml index 226eecdfd..75f469430 100644 --- a/matitaB/components/ng_cic_content/interpretations.ml +++ b/matitaB/components/ng_cic_content/interpretations.ml @@ -89,7 +89,7 @@ let level_of_uri u = let find_level2_patterns32 status pid = IntMap.find pid status#interp_db.level2_patterns32 -let instantiate32 env symbol args = +let instantiate32 env symbol dsc args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = @@ -112,7 +112,7 @@ let instantiate32 env symbol args = in add_lambda t (n - count_lambda t) in - let head = Ast.Symbol (symbol, None) in + let head = Ast.Symbol (symbol, Some (None, dsc)) in if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) @@ -338,12 +338,12 @@ let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term = term ) env in - let _, symbol, args, _ = + let dsc, symbol, args, _ = try find_level2_patterns32 status pid with Not_found -> assert false in - instantiate32 env symbol args + instantiate32 env symbol dsc args ;; let nmap_context0 status ~metasenv ~subst context = diff --git a/matitaB/matita/applyTransformation.ml b/matitaB/matita/applyTransformation.ml index a911742b0..5db35244e 100644 --- a/matitaB/matita/applyTransformation.ml +++ b/matitaB/matita/applyTransformation.ml @@ -101,7 +101,7 @@ class status = method ppmetasenv ~subst metasenv = String.concat "\n" (List.map - (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 20 self + (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 50 self ~metasenv ~subst m) metasenv) (* method ppobj obj = diff --git a/matitaB/matita/cicMathView.ml b/matitaB/matita/cicMathView.ml index 9f1a00458..effa76001 100644 --- a/matitaB/matita/cicMathView.ml +++ b/matitaB/matita/cicMathView.ml @@ -637,7 +637,7 @@ object (self) let sequent = List.assoc metano metasenv in let txt = ApplyTransformation.ntxt_of_cic_sequent - ~map_unicode_to_tex:false 20 status ~metasenv ~subst (metano,sequent) + ~map_unicode_to_tex:false 50 status ~metasenv ~subst (metano,sequent) in (* MATITA 1.0 if BuildTimeConf.debug then begin let name = -- 2.39.2