X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=4ea6e5ac3e4dd3ee47655f62a2ac1ed05254dc8f;hb=0d6f5efcf10a888bfccc769f2c58d998c411da47;hp=6e72042e83c6a34901de94fe5607e6f41ecc9088;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 6e72042e8..4ea6e5ac3 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -19,8 +19,8 @@ open UriManager
 module Ast = CicNotationPt
 module NRef = NReference 
 
+let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
-(* let debug_print s = prerr_endline (Lazy.force s);; *)
 
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
@@ -34,7 +34,7 @@ let rec mk_rels howmany from =
 ;;
 
 let refine_term 
- metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
+ metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl=
   assert (uri=None);
   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" 
     (NCicPp.ppterm ~metasenv ~subst ~context term)));
@@ -46,12 +46,9 @@ let refine_term
         (*assert false*) HExtlib.dummy_floc
     in
     let metasenv, subst, term, _ = 
-      NCicRefiner.typeof
-        (NCicUnifHint.db ())
-        ~look_for_coercion:(
-          if use_coercions then 
-           NCicCoercion.look_for_coercion coercion_db
-          else (fun _ _ _ _ _ -> []))
+      NCicRefiner.typeof 
+        (rdb#set_coerc_db 
+          (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
         metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
@@ -67,7 +64,7 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~coercion_db metasenv subst context _uri 
+  ~rdb metasenv subst _context _uri 
   ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
@@ -75,17 +72,14 @@ let refine_obj
   let localise t = 
     try NCicUntrusted.NCicHash.find localization_tbl t
     with Not_found -> 
-      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
       (*assert false*)HExtlib.dummy_floc
   in
   try
     let obj =
       NCicRefiner.typeof_obj
-        (NCicUnifHint.db ())
-        ~look_for_coercion:(
-          if use_coercions then 
-           NCicCoercion.look_for_coercion coercion_db
-          else (fun _ _ _ _ _ -> []))
+        (rdb#set_coerc_db
+           (if use_coercions then rdb#coerc_db 
+            else NCicCoercion.empty_db))
         obj ~localise 
     in
       Disambiguate.Ok (obj, [], [], ())
@@ -124,6 +118,12 @@ let interpretate_term_and_interpretate_term_option
          NCicUntrusted.NCicHash.add localization_tbl res loc;
        res
     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
+    | CicNotationPt.Appl (CicNotationPt.Appl inner :: args) ->
+        aux ~localize loc context (CicNotationPt.Appl (inner @ args))
+    | CicNotationPt.Appl 
+        (CicNotationPt.AttributedTerm (att,(CicNotationPt.Appl inner))::args)->
+        aux ~localize loc context 
+          (CicNotationPt.AttributedTerm (att,CicNotationPt.Appl (inner @ args)))
     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux ~localize loc context) args in
         Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
@@ -321,7 +321,7 @@ let interpretate_term_and_interpretate_term_option
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
-           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
     | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
@@ -329,7 +329,8 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
-    | CicNotationPt.Implicit -> NCic.Implicit `Term
+    | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+    | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -342,15 +343,15 @@ let interpretate_term_and_interpretate_term_option
          NCic.Meta (index, (0, NCic.Ctx cic_subst))
     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+       [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
+       [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
+       [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -367,7 +368,8 @@ let interpretate_term_and_interpretate_term_option
         res
     | Some (CicNotationPt.AttributedTerm (_, term)) ->
         aux_option ~localize loc context annotation (Some term)
-    | Some CicNotationPt.Implicit -> NCic.Implicit annotation
+    | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation
+    | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | Some term -> aux ~localize loc context term
   in
    (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
@@ -482,7 +484,7 @@ let interpretate_obj
                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
                  defs
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour in
+             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
              NCic.Fixpoint (inductive,inductiveFuns,attrs)
          | bo -> 
              let bo = 
@@ -498,7 +500,7 @@ let interpretate_obj
        (fun (context,res) (name,t) ->
          let t =
           match t with
-             None -> CicNotationPt.Implicit
+             None -> CicNotationPt.Implicit `JustOne
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
@@ -512,13 +514,11 @@ let interpretate_obj
     let add_params =
      List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
     let leftno = List.length params in
+    let _,inductive,_,_ = try List.hd tyl with Failure _ -> assert false in
     let obj_context =
      snd (
       List.fold_left
        (fun (i,res) (name,_,_,_) ->
-         let _,inductive,_,_ =
-          (* ??? *)
-          try List.hd tyl with Failure _ -> assert false in
          let nref =
           NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
          in
@@ -548,7 +548,7 @@ let interpretate_obj
      let height = (* XXX calculate *) 0 in
      let attrs = `Provided, `Regular in
      uri, height, [], [], 
-     NCic.Inductive (true,leftno,tyl,attrs)
+     NCic.Inductive (inductive,leftno,tyl,attrs)
  | CicNotationPt.Record (params,name,ty,fields) ->
     let context,params =
      let context,res =
@@ -556,7 +556,7 @@ let interpretate_obj
        (fun (context,res) (name,t) ->
          let t =
           match t with
-             None -> CicNotationPt.Implicit
+             None -> CicNotationPt.Implicit `JustOne
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
@@ -607,7 +607,7 @@ let interpretate_obj
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
    ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~coercion_db ~lookup_in_library 
+   ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
@@ -621,7 +621,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
      ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
-     ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
+     ~refine_thing:(refine_term ~rdb) (text,prefix_len,term)
      ~mk_localization_tbl ~expty ~subst
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
@@ -629,7 +629,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
 
 let disambiguate_obj 
    ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~coercion_db ~lookup_in_library ~uri
+   ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
@@ -645,7 +645,7 @@ let disambiguate_obj
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
      ~interpretate_thing:(interpretate_obj ~mk_choice)
-     ~refine_thing:(refine_obj ~coercion_db) 
+     ~refine_thing:(refine_obj ~rdb) 
      (text,prefix_len,obj)
      ~mk_localization_tbl ~expty:None
    in