X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=a10d0a8bddd92068e77fb4bd598e092a8876c2c1;hb=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;hp=b9809335cf491d493c683dd81f69fe842398ac42;hpb=172e33ea0aabf7ef066e73fbe577061955327693;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index b9809335c..a10d0a8bd 100644
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -25,9 +25,9 @@
 
 open Printf
 
-module Pp = CicNotationPp
-module Pt = CicNotationPt
+module Ast = CicNotationPt
 module Env = CicNotationEnv
+module Pp = CicNotationPp
 module Util = CicNotationUtil
 
 type pattern_id = int
@@ -193,14 +193,14 @@ module Matcher21 =
 struct
   module Pattern21 =
   struct
-    type pattern_t = Pt.term
-    type term_t = Pt.term
+    type pattern_t = Ast.term
+    type term_t = Ast.term
     let rec classify = function
-      | Pt.AttributedTerm (_, t) -> classify t
-      | Pt.Variable _ -> Variable
-      | Pt.Magic _
-      | Pt.Layout _
-      | Pt.Literal _ as t -> assert false
+      | Ast.AttributedTerm (_, t) -> classify t
+      | Ast.Variable _ -> Variable
+      | Ast.Magic _
+      | Ast.Layout _
+      | Ast.Literal _ as t -> assert false
       | _ -> Constructor
     let tag_of_pattern = CicNotationTag.get_tag
     let tag_of_term = CicNotationTag.get_tag
@@ -213,14 +213,14 @@ struct
     let add_magic m =
       let name = Util.fresh_name () in
       magic_map := (name, m) :: !magic_map;
-      Pt.Variable (Pt.TermVar name)
+      Ast.Variable (Ast.TermVar name)
     in
     let rec aux = function
-      | Pt.AttributedTerm (_, t) -> assert false
-      | Pt.Literal _
-      | Pt.Layout _ -> assert false
-      | Pt.Variable v -> Pt.Variable v
-      | Pt.Magic m -> add_magic m
+      | Ast.AttributedTerm (_, t) -> assert false
+      | Ast.Literal _
+      | Ast.Layout _ -> assert false
+      | Ast.Variable v -> Ast.Variable v
+      | Ast.Magic m -> add_magic m
       | t -> Util.visit_ast aux t
     in
     let term' = aux term in
@@ -230,11 +230,11 @@ struct
     List.map2
       (fun p t ->
         match p, t with
-          Pt.Variable (Pt.TermVar name), _ ->
+          Ast.Variable (Ast.TermVar name), _ ->
             name, (Env.TermType, Env.TermValue t)
-        | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) ->
+        | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
             name, (Env.NumType, Env.NumValue s)
-        | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) ->
+        | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
             name, (Env.StringType, Env.StringValue s)
         | _ -> assert false)
       pl tl
@@ -291,7 +291,7 @@ struct
     M.compiler rows' match_cb (fun _ -> None)
 
   and compile_magic = function
-    | Pt.Fold (kind, p_base, names, p_rec) ->
+    | Ast.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
@@ -321,7 +321,7 @@ struct
 		 | 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 *)
+    | Ast.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
@@ -331,7 +331,7 @@ struct
           | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
           | _ -> assert false)
 
-    | Pt.If (p_test, p_true, p_false) ->
+    | Ast.If (p_test, p_true, p_false) ->
 	let compiled_test = compiler [p_test, 0]
 	and compiled_true = compiler [p_true, 0]
 	and compiled_false = compiler [p_false, 0] in
@@ -345,7 +345,7 @@ struct
 		 | None -> None
 		 | Some (env', _) -> Some (env' @ env))
 
-    | Pt.Fail -> (fun _ _ -> None)
+    | Ast.Fail -> (fun _ _ -> None)
 
     | _ -> assert false
 end
@@ -374,23 +374,23 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Pt.UriPattern uri -> Uri uri, []
-      | Pt.ImplicitPattern
-      | Pt.VarPattern _ -> Blob, []
-      | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
+      | Ast.UriPattern uri -> Uri uri, []
+      | Ast.ImplicitPattern
+      | Ast.VarPattern _ -> Blob, []
+      | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 
     let tag_of_pattern p =
       let mask, pl = mask_of_appl_pattern p in
       Hashtbl.hash mask, pl
 
-    type pattern_t = Pt.cic_appl_pattern
+    type pattern_t = Ast.cic_appl_pattern
     type term_t = Cic.annterm
 
     let classify = function
-      | Pt.ImplicitPattern
-      | Pt.VarPattern _ -> Variable
-      | Pt.UriPattern _
-      | Pt.ApplPattern _ -> Constructor
+      | Ast.ImplicitPattern
+      | Ast.VarPattern _ -> Variable
+      | Ast.UriPattern _
+      | Ast.ApplPattern _ -> Constructor
   end
 
   module M = Matcher (Pattern32)
@@ -403,8 +403,8 @@ struct
           List.map2
             (fun p t ->
               match p with
-              | Pt.ImplicitPattern -> Util.fresh_name (), t
-              | Pt.VarPattern name -> name, t
+              | Ast.ImplicitPattern -> Util.fresh_name (), t
+              | Ast.VarPattern name -> name, t
               | _ -> assert false)
             pl matched_terms
         in