First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / components / ng_cic_content / interpretations.ml

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index ee4bb9437ca5a5002f3f2587768b29a03ac2e239..5f41a1fe56ec8b56c52b9d2abf6fb99be852598b 100644 (file)
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -122,15 +122,15 @@ let instantiate32 idrefs env symbol args =
         let rec add_lambda t n =
           if n > 0 then
             let name = NotationUtil.fresh_name () in
-            Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
-              Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
+            Ast.Binder (`Lambda, (Ast.Ident (name, `Ambiguous), None),
+              Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, `Ambiguous)])
           else
             t
         in
         add_lambda t (n - count_lambda t)
   in
   let head =
-    let symbol = Ast.Symbol (symbol, 0) in
+    let symbol = Ast.Symbol (symbol, None) in
     add_idrefs idrefs symbol
   in
   if args = [] then head
@@ -236,10 +236,11 @@ let nast_of_cic0 status
        (try 
          let name,_ = List.nth context (n-1) in
          let name = if name = "_" then "__"^string_of_int n else name in
-          idref (Ast.Ident (name,None))
+          idref (Ast.Ident (name,`Ambiguous))
         with Failure "nth" | Invalid_argument "List.nth" -> 
-         idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None)))
-    | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, None))
+         idref (Ast.Ident ("-" ^ string_of_int (n - List.length
+         context),`Ambiguous)))
+    | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, `Ambiguous))
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
          k ~context (NCicSubstitution.subst_meta status lc t)
@@ -262,15 +263,15 @@ let nast_of_cic0 status
     | NCic.Prod (n,s,t) ->
         let n = if n.[0] = '_' then "_" else n in
         let binder_kind = `Forall in
-         idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)),
+         idref (Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)),
           k ~context:((n,NCic.Decl s)::context) t))
     | NCic.Lambda (n,s,t) ->
-        idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)),
+        idref (Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)),
          k ~context:((n,NCic.Decl s)::context) t))
     | NCic.LetIn (n,s,ty,NCic.Rel 1) ->
         idref (Ast.Cast (k ~context ty, k ~context s))
     | NCic.LetIn (n,s,ty,t) ->
-        idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context
+        idref (Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context
           ty, k ~context:((n,NCic.Decl s)::context) t))
     | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> 
        let _,_,t,_ = List.assoc n subst in
@@ -282,7 +283,7 @@ let nast_of_cic0 status
            | _ -> NCic.Appl (hd :: args)))
     | NCic.Appl args as t ->
        (match destroy_nat t with
-         | Some n -> idref (Ast.Num (string_of_int n, -1))
+         | Some n -> idref (Ast.Num (string_of_int n, None))
          | None ->
             let args =
              if not !hide_coercions then args
@@ -327,7 +328,7 @@ let nast_of_cic0 status
              eat_branch (pred n) ctx t pat 
           | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
               let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
-              (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs
+              (Ast.Ident (name,`Ambiguous), Some (k ~context:ctx s)) :: cv, rhs
           | _, _ -> [], k ~context:ctx pat
         in
         let j = ref 0 in
@@ -366,7 +367,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
            idref
             ~reference:
               (match term with NCic.Const nref -> nref | _ -> assert false)
-           (NotationPt.Ident ("dummy",None))
+           (NotationPt.Ident ("dummy",`Ambiguous))
           in
            match attrterm with
               Ast.AttributedTerm (`IdRef id, _) -> id