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

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index d51e4bf02..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 " ")
-let builtin_symbol s = Ast.Literal (`Symbol s)
-let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
+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))
+    (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 >}
@@ -337,8 +337,8 @@ let set_compiled21 status f =
  status#set_content_pres_db
   { status#content_pres_db with compiled21 = Some f }
 
-let add_idrefs =
-  List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
+(* let add_idrefs =
+  List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) *)
 
 let instantiate21 idrefs env l1 =
   let rec subst_singleton pos env =
@@ -375,11 +375,27 @@ let instantiate21 idrefs env l1 =
         in
         [ value ]
     | Ast.Magic m -> subst_magic pos env m
-    | Ast.Literal l as t ->
-        let t = add_idrefs idrefs t in
-        (match l with
-        | `Keyword k -> [ add_keyword_attrs t ]
-        | _ -> [ t ])
+    | Ast.Literal (csym,l) as t ->
+       let enrich_literal l (_,uri,desc) =
+            let desc = Some desc in
+            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
@@ -393,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
@@ -470,17 +486,24 @@ 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); *)
     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 status 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')
   | _ ->
       (match get_compiled21 status term with
-      | None -> pp_ast0 status term (pp_ast1 status)
+      | None -> (* prerr_endline "### ramo 1"; *) 
+          pp_ast0 status term (pp_ast1 status)
       | Some (env, ctors, pid) ->
+          (* prerr_endline "### ramo 2";
+            prerr_endline ("### constructors:\n" ^ 
+           (String.concat "\n\n" (List.map (NotationPp.pp_term status) ctors)) ^
+           "\n\n### constructors end") *)
           let idrefs =
             List.flatten (List.map NotationUtil.get_idrefs ctors)
           in
@@ -491,7 +514,8 @@ let rec pp_ast1 status term =
           in
           instantiate21 idrefs (ast_env_of_env env) l1)
   in
-  prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term status res);
+  (* prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term
+   * status res);*)
   res
 
 let load_patterns21 status t =
@@ -548,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
@@ -579,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 =
@@ -611,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
@@ -619,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