X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=212c2cdc0ffb874d894a8f59cfbb7db38dee2742;hb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced;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..212c2cdc0 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))
@@ -66,16 +66,17 @@ 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))
+  add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
+    (Ast.Literal (None,`Number (s,(None,None))))
 
 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
@@ -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
@@ -467,18 +483,27 @@ 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 =
+    (* 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 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
@@ -488,6 +513,10 @@ 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))
@@ -543,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
@@ -574,7 +605,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 +630,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 (List.map (fun (_,(_,x)) -> x) env)
 
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var
@@ -619,6 +645,33 @@ let instantiate_level2 status env term =
     | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
 
     | _ -> assert false
+  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
@@ -636,14 +689,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) ->