* various bug fix related to the environment returned when a match

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index dac2b4c7348b64145a7001f52c908d89eacae13d..180a8c912f05484c451d856c30a3151586b71b58 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -265,6 +265,7 @@ let instantiate21 env (* precedence associativity *) l1 =
     | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
+         prerr_endline ("searching for " ^ name);
         let ty, value =
           try
             List.assoc name env
@@ -333,6 +334,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) -> 
@@ -346,16 +348,24 @@ let rec pp_ast1 term =
   match term with
   | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
   | _ ->
-      (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)))
+      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
+               prerr_endline ("IN " ^ CicNotationPp.pp_term term);
+               (* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *)
+               let res = Ast.AttributedTerm (`Level (precedence, associativity),
+                                             (instantiate21 (ast_env_of_env env) l1))
+               in
+                 prerr_endline "OUT";
+                 res
+      end
+  
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function