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

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

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 204e945fc0c8b700388b30502709afcee1b8631b..6b1266ec8c41bd62410c3f68f443f1e18af10fa1 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -25,6 +25,7 @@
 
 open Printf
 
+module Pp = CicNotationPp
 module Pt = CicNotationPt
 module Env = CicNotationEnv
 module Util = CicNotationUtil
@@ -236,22 +237,34 @@ struct
     let magichecker map =
       List.fold_left
         (fun f (name, m) ->
+          prerr_endline ("compiling magichecker for " ^ name) ;
           let m_checker = compile_magic m in
           (fun env ->
             match m_checker (Env.lookup_term env name) env with
             | None -> None
-            | Some env' -> f env'))
-        (fun env -> Some env)
+            | Some env' ->
+               f env'))
+        (fun env ->
+            prerr_endline ("all magics processed ENV = " ^ Pp.pp_env env) ;       
+          Some env)
         map
     in
     let magichooser candidates =
       List.fold_left
         (fun f (pid, pl, checker) ->
+          List.iter (fun p -> prerr_endline ("P = " ^ Pp.pp_term p)) pl ;
           (fun matched_terms ->
             let env = env_of_matched pl matched_terms in
             match checker env with
             | None -> f matched_terms
-            | Some env -> Some (env, pid)))
+            | Some env ->
+               prerr_endline (String.concat " / " (List.map Pp.pp_term pl)) ;
+               prerr_endline ("magichoose found a match for " ^ Pp.pp_env env ^ " " ^ string_of_int pid) ;
+               let magic_map =
+                 try List.assoc pid magic_maps with Not_found -> assert false
+               in
+               let env' = Env.remove_names env (List.map fst magic_map) in
+               Some (env', pid)))
         (fun _ -> None)
         candidates
     in
@@ -265,44 +278,72 @@ struct
             pid, pl, magichecker magic_map)
           rows
       in
-      magichooser candidates
+       magichooser candidates
     in
     M.compiler rows' match_cb (fun _ -> None)
 
   and compile_magic = function
     | Pt.Fold (kind, p_base, names, p_rec) ->
         let p_rec_decls = Env.declarations_of_term p_rec in
+         (* LUCA: p_rec_decls should not contain "names" *)
         let acc_name = try List.hd names with Failure _ -> assert false in
-        let compiled = compiler [p_base, 0; p_rec, 1] in
-        (fun term env ->
-          let rec aux term =
-            match compiled term with
-            | None -> None
-            | Some (env', 0) -> Some (env', [])
-            | Some (env', 1) ->
-                begin
-                  let acc = Env.lookup_term env' acc_name in
-                  let env'' = Env.remove env' acc_name in
-                  match aux acc with
-                  | None -> None
-                  | Some (base_env, rec_envl) -> 
-                      Some (base_env, env'' :: rec_envl )
-                end
-            | _ -> assert false
-          in
-            match aux term with
-            | None -> None
-            | Some (base_env, rec_envl) ->
-                Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
+       let compiled_base = compiler [p_base, 0]
+       and compiled_rec = compiler [p_rec, 0] in
+         (fun term env ->
+            let aux_base term =
+              match compiled_base term with
+                | None -> None
+                | Some (env', _) -> Some (env', [])
+            in
+            let rec aux term =
+              match compiled_rec term with
+                | None -> aux_base term
+                | Some (env', _) ->
+                    begin
+                       let acc = Env.lookup_term env' acc_name in
+                       let env'' = Env.remove_name env' acc_name in
+                        match aux acc with
+                          | None -> aux_base term
+                          | Some (base_env, rec_envl) -> 
+                              Some (base_env, env'' :: rec_envl)
+                     end
+            in
+               match aux term with
+                | None -> None
+                | Some (base_env, rec_envl) ->
+                     Some (base_env @ Env.coalesce_env p_rec_decls rec_envl @ env)) (* @ env LUCA!!! *)
+
     | Pt.Default (p_some, p_none) ->  (* p_none can't bound names *)
         let p_some_decls = Env.declarations_of_term p_some in
         let none_env = List.map Env.opt_binding_of_name p_some_decls in
         let compiled = compiler [p_some, 0] in
         (fun term env ->
           match compiled term with
-          | None -> Some none_env
+          | None -> Some none_env (* LUCA: @ env ??? *)
           | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
           | _ -> assert false)
+
+    | Pt.If (guard, p) ->
+       prerr_endline ("guard = " ^ CicNotationPp.pp_term guard) ;
+       prerr_endline ("p = " ^ CicNotationPp.pp_term p) ;
+       let compiled_guard = compiler [guard, 0]
+       and compiled_p = compiler [p, 0] in
+         (fun term env ->
+            prerr_endline "GUARDIA?" ;
+            match compiled_guard term with
+              | None -> 
+                  prerr_endline "SONO CAZZI H2SO4" ;
+                  None
+              | Some _ ->
+                  begin
+                    prerr_endline "OKKKKKKKKKKKKKK" ;
+                    match compiled_p term with
+                      | None -> None
+                      | Some (env', _) ->
+                          prerr_endline "guardia ok" ;
+                          Some (env' @ env)
+                  end)
+
     | _ -> assert false
 end