X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=207b26a233d139773815234a62843838e115020d;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=3af28fddde636d25a41d279d923a7ee8e334b010;hpb=d25c0d1fd0dee1036df6f3bbc62c75c55c3bd314;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 3af28fddd..207b26a23 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -82,6 +82,8 @@ let resolve_binder = function
   | `Exists -> "\\exists"
 
 let pp_ast0 t k =
+  let reset_href t = Ast.AttributedTerm (`Href [], t) in
+  let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in
   let rec aux = function
     | Ast.Appl ts ->
         Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
@@ -92,21 +94,22 @@ let pp_ast0 t k =
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             aux_ty ty;
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              Ast.Literal (`Symbol "\\to"); k body]))])))
+              builtin_symbol "\\to";
+              k body]))])))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              Ast.Literal (`Symbol (resolve_binder binder_kind));
+              builtin_symbol (resolve_binder binder_kind);
               k id;
-              Ast.Literal (`Symbol ":");
+              builtin_symbol ":";
               aux_ty ty ]));
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              Ast.Literal (`Symbol ".");
+              builtin_symbol ".";
               k body ]))])))
     | t -> CicNotationUtil.visit_ast ~special_k k t
   and aux_ty = function
-    | None -> Ast.Literal (`Symbol "?")
+    | None -> builtin_symbol "?"
     | Some ty -> k ty
   and special_k = function
     | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
@@ -115,7 +118,6 @@ let pp_ast0 t k =
   aux t
 
 let ast_of_acic0 term_info acic k =
-(*   prerr_endline "ast_of_acic0"; *)
   let k = k term_info in
   let register_uri id uri = Hashtbl.add term_info.uri id uri in
   let sort_of_id id =
@@ -321,7 +323,8 @@ let instantiate21 env (* precedence associativity *) l1 =
 	  end
     | _ -> assert false (* impossible *)
   and subst_layout env = function
-    | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+    | Ast.Box (kind, tl) ->
+        Ast.Box (kind, List.concat (List.map (subst env) tl))
     | l -> CicNotationUtil.visit_layout (subst_singleton env) l
   in
     subst_singleton env l1
@@ -330,6 +333,7 @@ let rec pp_ast1 term =
   let rec pp_value = function
     | CicNotationEnv.NumValue _ as v -> v
     | CicNotationEnv.StringValue _ as v -> v
+(*     | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
     | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
     | CicNotationEnv.OptValue None as v -> v
     | CicNotationEnv.OptValue (Some v) -> 
@@ -340,16 +344,21 @@ let rec pp_ast1 term =
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
-  match (get_compiled21 ()) term with
-  | None -> pp_ast0 term pp_ast1
-  | Some (env, pid) ->
-      let precedence, associativity, l1 =
-        try
-          Hashtbl.find level1_patterns21 pid
-        with Not_found -> assert false
-      in
-      Ast.AttributedTerm (`Level (precedence, associativity),
-        (instantiate21 (ast_env_of_env env) (* precedence associativity *) l1))
+  match term with
+  | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
+  | _ ->
+      begin
+	match (get_compiled21 ()) term with
+	  | None -> pp_ast0 term pp_ast1
+	  | Some (env, pid) ->
+              let precedence, associativity, l1 =
+		try
+		  Hashtbl.find level1_patterns21 pid
+		with Not_found -> assert false
+              in
+		Ast.AttributedTerm (`Level (precedence, associativity),
+				(instantiate21 (ast_env_of_env env) l1))
+      end
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
@@ -379,12 +388,15 @@ let rec ast_of_acic1 term_info annterm =
       let env' =
         List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
       in
-      let symbol, args =
+      let symbol, args, uris =
         try
           Hashtbl.find level2_patterns32 pid
         with Not_found -> assert false
       in
-      instantiate32 term_info env' symbol args
+      let ast = instantiate32 term_info env' symbol args in
+      match uris with
+      | [] -> ast
+      | _ -> Ast.AttributedTerm (`Href uris, ast)
 
 let load_patterns32 t =
   set_compiled32 (CicNotationMatcher.Matcher32.compiler t)
@@ -407,7 +419,8 @@ let fresh_id =
 
 let add_interpretation (symbol, args) appl_pattern =
   let id = fresh_id () in
-  Hashtbl.add level2_patterns32 id (symbol, args);
+  let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in
+  Hashtbl.add level2_patterns32 id (symbol, args, uris);
   pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
   load_patterns32 !pattern32_matrix;
   id