X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=212c2cdc0ffb874d894a8f59cfbb7db38dee2742;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=8ff5a13f2a1094cb14c7bce5494a380f9002f3f2;hpb=1b67bd4dfa12ef25b8fa63884c71893b961db27d;p=helm.git

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 8ff5a13f2..212c2cdc0 100644
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -66,13 +66,13 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
-let space = Ast.Literal (`Symbol (" ", (None,None)))
-let builtin_symbol s = Ast.Literal (`Symbol (s,(None,None)))
-let keyword k = add_keyword_attrs (Ast.Literal (`Keyword (k,(None,None))))
+let space = Ast.Literal (None,`Symbol (" ", (None,None)))
+let builtin_symbol s = Ast.Literal (None,`Symbol (s,(None,None)))
+let keyword k = add_keyword_attrs (Ast.Literal (None,`Keyword (k,(None,None))))
 
 let number s =
   add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
-    (Ast.Literal (`Number (s,(None,None))))
+    (Ast.Literal (None,`Number (s,(None,None))))
 
 let ident i =
   add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
@@ -317,9 +317,9 @@ class type g_status =
     method content_pres_db: db
   end
  
-class virtual status =
+class virtual status uid =
  object
-   inherit NCic.status
+   inherit NCic.status uid
    val content_pres_db = initial_db  
    method content_pres_db = content_pres_db
    method set_content_pres_db v = {< content_pres_db = v >}
@@ -375,15 +375,27 @@ let instantiate21 idrefs env l1 =
         in
         [ value ]
     | Ast.Magic m -> subst_magic pos env m
-    | Ast.Literal l as t ->
-       (match idrefs with
-        | [] -> [t]
-        | desc::_ ->
+    | Ast.Literal (csym,l) as t ->
+       let enrich_literal l (_,uri,desc) =
             let desc = Some desc in
-            (match l with
-            | `Keyword (k,_) -> [ Ast.Literal (`Keyword (k,(None,desc))) ]
-            | `Symbol (s,_) -> [ Ast.Literal (`Symbol (s,(None,desc))) ]
-            | `Number (n,_) -> [ Ast.Literal (`Number (n,(None,desc))) ]))
+            match l with
+            | `Keyword (k,_) -> [ Ast.Literal (csym,`Keyword (k,(uri,desc))) ]
+            | `Symbol (s,_) -> [ Ast.Literal (csym,`Symbol (s,(uri,desc))) ]
+            | `Number (n,_) -> [ Ast.Literal (csym,`Number (n,(uri,desc))) ]
+       in
+       (match csym,idrefs with
+        | None, [] -> [t]
+        | None,disamb::_ -> enrich_literal l disamb
+        | Some cs,_ -> 
+             (try
+               let disamb = List.find (fun (cs',_,_) -> cs = cs') idrefs in
+               enrich_literal l disamb
+              with Not_found -> 
+                (* prerr_endline ("can't find idref for " ^ cs ^ ". Will now print idrefs");
+                List.iter 
+                  (fun (cs'',_,_) -> prerr_endline ("idref " ^ cs''))
+                  idrefs;*)
+                [t]))
     | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
     | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
   and subst_magic pos env = function
@@ -397,7 +409,7 @@ let instantiate21 idrefs env l1 =
         let sep =
           match sep_opt with
             | None -> []
-            | Some l -> [ Ast.Literal l; break; space ]
+            | Some l -> [ Ast.Literal (None,l); break; space ]
 	in
         let rec instantiate_list acc = function
           | [] -> List.rev acc
@@ -474,7 +486,7 @@ let rec pp_ast1 status term =
     | NotationEnv.DisambiguationValue _ as v -> v
   in
   let ast_env_of_env env =
-    prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env);
+    (* prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env); *)
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
 (* prerr_endline ("### pattern matching from 2 to 1 on term " ^
@@ -560,15 +572,17 @@ let unopt_names names env =
 
 let head_names names env =
   let rec aux acc = function
-    | (name, (ty, v)) :: tl when List.mem name names ->
+    | (name, (ty, v)) as x :: tl when List.mem name names ->
         (match ty, v with
         | Env.ListType ty, Env.ListValue (v :: _) ->
-            aux ((name, (ty, v)) :: acc) tl
+            aux ((name, (ty,v)):: acc) tl
         | Env.TermType _, Env.TermValue _  ->
-            aux ((name, (ty, v)) :: acc) tl
+            aux (x :: acc) tl
         | Env.OptType _, Env.OptValue _ ->
-            aux ((name, (ty, v)) :: acc) tl
+            aux (x :: acc) tl
         | _ -> assert false)
+    | (_,(_,Env.DisambiguationValue _)) as x :: tl -> 
+        aux (x::acc) tl
     | _ :: tl -> aux acc tl
       (* base pattern may contain only meta names, thus we trash all others *)
     | [] -> acc
@@ -591,7 +605,7 @@ let tail_names names env =
   in
   aux [] env
 
-let instantiate_level2 status env (loc,uri,desc) 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 =
@@ -623,7 +637,7 @@ let instantiate_level2 status env (loc,uri,desc) term =
     | Ast.Num _
     | Ast.Sort _
     | Ast.UserInput -> term
-    | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc)
+    | Ast.Symbol (s,_) -> aux_symbol s (List.map (fun (_,(_,x)) -> x) env)
 
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var
@@ -631,10 +645,33 @@ let instantiate_level2 status env (loc,uri,desc) 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_symbol s env =
+   (* XXX: it's totally unclear why the env we receive here is in reverse
+    * order (a diff with the previous revision shows no obvious reason).
+    * This one-line patch is needed so that the default symbol chosen for
+    * storing the interpretation is the leftmost, rather than the rightmost *)
+   let env = List.rev env in
+   try 
+     (let dv =
+      try List.find (function 
+        | Env.DisambiguationValue(Some s',_,_,_) when s = s' -> true
+        | _ -> false) env
+      with Not_found ->
+      List.find (function 
+        | Env.DisambiguationValue(None,_,_,_) -> true
+        | _ -> false) env
+      in
+      match dv with
+      | Env.DisambiguationValue(_,loc,uri,Some desc) -> 
+        Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
+      | Env.DisambiguationValue(_,loc,_,_) -> 
+        (* The important disambiguation info for symbols is the desc,
+         * if we don't have it, we won't use the uri either *)
+        Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
+      | _ -> assert false) (* vacuous *)
+   with Not_found -> 
+        (* Ast.AttributedTerm (`Loc Stdpp.dummy_loc, Ast.Symbol (s, None))*)
+        Ast.Symbol (s, None)
   and aux_opt env = function
     | Some term -> Some (aux env term)
     | None -> None