milestone in basic_2, λδ-2A reconstructed

[helm.git] / helm / software / components / ng_cic_content / ncic2astMatcher.ml

diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.ml b/helm/software/components/ng_cic_content/ncic2astMatcher.ml
index 099e0b26a2c8f2d1ffd30415830448b33348a7b8..2245e34295791f082d1e4a451b4c811aba52ba4d 100644 (file)
--- a/helm/software/components/ng_cic_content/ncic2astMatcher.ml
+++ b/helm/software/components/ng_cic_content/ncic2astMatcher.ml
@@ -28,20 +28,23 @@
 module Ast = CicNotationPt
 module Util = CicNotationUtil
 
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
 module Matcher32 =
 struct
   module Pattern32 =
   struct
     type cic_mask_t =
       Blob
-    | Uri of UriManager.uri
+    | NRef of NReference.reference
     | Appl of cic_mask_t list
 
     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
 
     let mask_of_cic = function
       | NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl
-      | NCic.Const nref -> Uri (NCic2OCic.ouri_of_reference nref), []
+      | NCic.Const nref -> NRef nref, []
       | _ -> Blob, []
 
     let tag_of_term t =
@@ -49,7 +52,8 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Ast.UriPattern uri -> Uri uri, []
+      | Ast.UriPattern uri -> NRef (!reference_of_oxuri uri), []
+      | Ast.NRefPattern nref -> NRef nref, []
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> Blob, []
       | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
@@ -70,6 +74,7 @@ struct
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> PatternMatcher.Variable
       | Ast.UriPattern _
+      | Ast.NRefPattern _
       | Ast.ApplPattern _ -> PatternMatcher.Constructor
   end