...

[helm.git] / matitaB / components / content_pres / termContentPres.ml

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 6846c30b5b9e608fe96af08fbb60b740ccf24b19..d51e4bf02ca392d08571431af6d41bdddcf8d4af 100644 (file)
--- 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) ->