X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=d51e4bf02ca392d08571431af6d41bdddcf8d4af;hb=4e89ae4ac9b001c0479d68d9f74fe81fca6ecd2d;hp=6846c30b5b9e608fe96af08fbb60b740ccf24b19;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index 6846c30b5..d51e4bf02 100644 --- a/matitaB/components/content_pres/termContentPres.ml +++ b/matitaB/components/content_pres/termContentPres.ml @@ -52,11 +52,11 @@ let rec remove_level_info = | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t) | t -> t -let add_xml_attrs attrs t = - if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) +let add_xml_attrs attrs t = t +(* if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) *) -let add_keyword_attrs = - add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) +let add_keyword_attrs t = t +(* add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) *) let box kind spacing indent content = Ast.Layout (Ast.Box ((kind, spacing, indent), content)) @@ -71,11 +71,12 @@ let builtin_symbol s = Ast.Literal (`Symbol s) let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) let number s = - add_xml_attrs (RenderingAttrs.number_attributes `MathML) + add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) () (Ast.Literal (`Number s)) let ident i = - add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None)) + add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) () + (Ast.Ident (i,`Ambiguous)) let ident_w_href href i = match href with @@ -85,13 +86,13 @@ let ident_w_href href i = add_xml_attrs [Some "xlink", "href", href] (ident i) let binder_symbol s = - add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML) + add_xml_attrs (* (RenderingAttrs.builtin_symbol_attributes `MathML) *) () (builtin_symbol s) let xml_of_sort x = - let to_string x = Ast.Ident (x, None) in + let to_string x = Ast.Ident (x, `Ambiguous) in let identify x = - add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x) + add_xml_attrs (* (RenderingAttrs.keyword_attributes `MathML) *) () (to_string x) in let lvl t = Ast.AttributedTerm (`Level 90,t) in match x with @@ -271,8 +272,7 @@ let pp_ast0 status t k = | Ast.Sort sort -> aux_sort sort | Ast.Num _ | Ast.Symbol _ - | Ast.Ident (_, None) | Ast.Ident (_, Some []) - | Ast.Uri (_, None) | Ast.Uri (_, Some []) + | Ast.Ident _ | Ast.Literal _ | Ast.UserInput as leaf -> leaf | t -> NotationUtil.visit_ast ~special_k k t @@ -467,11 +467,13 @@ let rec pp_ast1 status term = NotationEnv.OptValue (Some (pp_value v)) | NotationEnv.ListValue vl -> NotationEnv.ListValue (List.map pp_value vl) + | NotationEnv.DisambiguationValue _ as v -> v in 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') @@ -488,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)) @@ -574,7 +579,7 @@ let tail_names names env = in aux [] env -let instantiate_level2 status env term = +let instantiate_level2 status env (loc,uri,desc) term = (* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *) let fresh_env = ref [] in let lookup_fresh_name n = @@ -599,19 +604,14 @@ let instantiate_level2 status env term = | Ast.LetRec (kind, definitions, body) -> Ast.LetRec (kind, List.map (aux_definition env) definitions, aux env body) - | Ast.Uri (name, None) -> Ast.Uri (name, None) - | Ast.Uri (name, Some substs) -> - Ast.Uri (name, Some (aux_substs env substs)) - | Ast.Ident (name, Some substs) -> - Ast.Ident (name, Some (aux_substs env substs)) | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs) | Ast.Implicit _ | Ast.Ident _ | Ast.Num _ | Ast.Sort _ - | Ast.Symbol _ | Ast.UserInput -> term + | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc) | Ast.Magic magic -> aux_magic env magic | Ast.Variable var -> aux_variable env var @@ -619,6 +619,10 @@ let instantiate_level2 status env term = | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty) | _ -> assert false + and aux_symbol s loc = function + | _, None -> Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None)) + | uri, Some desc -> + Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc))) and aux_opt env = function | Some term -> Some (aux env term) | None -> None @@ -636,14 +640,14 @@ let instantiate_level2 status env term = List.map (fun (name, term) -> (name, aux env term)) substs and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs and aux_variable env = function - | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0) + | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, None) | Ast.IdentVar name -> (match Env.lookup_string env name with - Env.Ident x -> Ast.Ident (x, None) + Env.Ident x -> Ast.Ident (x, `Ambiguous) | Env.Var x -> Ast.Variable (Ast.IdentVar x)) | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> Ast.AttributedTerm (`Level l,Env.lookup_term env name) - | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None) + | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, `Ambiguous) | Ast.Ascription (term, name) -> assert false and aux_magic env = function | Ast.Default (some_pattern, none_pattern) ->