X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=487bceb871377cfb1964e94ad81cccf878e8d733;hb=37b52567b8aa1bf5807767d94b96594c0e640588;hp=4d8b132269ecd01cfac6abfb0ed8208bca2137a8;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 4d8b13226..487bceb87 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -19,16 +19,25 @@ 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 reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
 
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
   | _ -> assert false
 ;;
 
+let rec mk_rels howmany from =
+  match howmany with 
+  | 0 -> []
+  | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) 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)));
@@ -36,16 +45,13 @@ let refine_term
     let localise t = 
       try NCicUntrusted.NCicHash.find localization_tbl t
       with Not_found -> 
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-        assert false
+        prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+        (*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, ())
@@ -61,7 +67,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=[]);
@@ -69,17 +75,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, [], [], ())
@@ -118,6 +121,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)
@@ -306,22 +315,30 @@ let interpretate_term_and_interpretate_term_option
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
     | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
        assert (subst = None);
        (try
-         NCic.Rel (find_in_context name context)
+             NCic.Rel (find_in_context name context)
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
-           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
-    | CicNotationPt.Uri (name, subst) ->
+            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+    | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NRef.reference_of_string name)
+         NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
-    | CicNotationPt.Implicit -> NCic.Implicit `Term
+    | CicNotationPt.NRef nref -> NCic.Const nref
+    | CicNotationPt.NCic t -> 
+           let context = (* to make metas_of_term happy *)
+             List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
+           assert(NCicUntrusted.metas_of_term [] context t = []); t
+    | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+    | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
+    | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -334,13 +351,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/Type.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
+       [`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/CProp.univ"])
+       [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -357,7 +376,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),
@@ -399,7 +419,7 @@ let new_flavour_of_flavour = function
   | `MutualDefinition -> `Definition 
   | `Fact -> `Fact
   | `Lemma -> `Lemma
-  | `Remark -> `Corollary
+  | `Remark -> `Example
   | `Theorem -> `Theorem
   | `Variant -> `Corollary 
   | `Axiom -> `Fact
@@ -422,7 +442,7 @@ let interpretate_obj
    interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
  let uri = match uri with | None -> assert false | Some u -> u in
  match obj with
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) ->
      let ty' = 
        interpretate_term 
          ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty 
@@ -431,14 +451,14 @@ let interpretate_obj
      uri, height, [], [], 
      (match bo,flavour with
       | None,`Axiom -> 
-          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
           NCic.Constant ([],name,None,ty',attrs)
       | Some _,`Axiom -> assert false
       | None,_ ->
-          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
       | Some bo,_ ->
-         match bo with
+        (match bo with
          | CicNotationPt.LetRec (kind, defs, _) ->
              let inductive = kind = `Inductive in
              let _,obj_context =
@@ -472,107 +492,130 @@ 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, pragma in
              NCic.Fixpoint (inductive,inductiveFuns,attrs)
          | bo -> 
              let bo = 
                interpretate_term 
                 ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
-             NCic.Constant ([],name,Some bo,ty',attrs))
-  | _ -> raise (MultiPassDisambiguator.DisambiguationError (0, []))
-(*
-  | CicNotationPt.Inductive (params,tyl) ->
-     let uri = match uri with Some uri -> uri | None -> assert false in
-     let context,params =
-      let context,res =
-       List.fold_left
-        (fun (context,res) (name,t) ->
-          let t =
-           match t with
-              None -> CicNotationPt.Implicit
-            | Some t -> t in
-          let name = CicNotationUtil.cic_name_of_name name in
-           name::context,(name, interpretate_term context env None false t)::res
-        ) ([],[]) params
-      in
-       context,List.rev res in
-     let add_params =
-      List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
-     let obj_context =
-      snd (
-       List.fold_left
-        (*here the explicit_named_substituion is assumed to be of length 0 *)
-        (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
-        (0,[]) tyl) in
-     let tyl =
-      List.map
-       (fun (name,b,ty,cl) ->
-         let ty' = add_params (interpretate_term context env None false ty) in
-         let cl' =
-          List.map
-           (fun (name,ty) ->
-             let ty' =
-              add_params
-               (interpretate_term ~obj_context ~context ~env ~uri:None
-                 ~is_path:false ty)
-             in
-              name,ty'
-           ) cl
+             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+             NCic.Constant ([],name,Some bo,ty',attrs)))
+ | CicNotationPt.Inductive (params,tyl) ->
+    let context,params =
+     let context,res =
+      List.fold_left
+       (fun (context,res) (name,t) ->
+         let t =
+          match t with
+             None -> CicNotationPt.Implicit `JustOne
+           | Some t -> t in
+         let name = cic_name_of_name name in
+         let t =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false t
          in
-          name,b,ty',cl'
-       ) tyl
+          (name,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
      in
-      Cic.InductiveDefinition (tyl,[],List.length params,[])
-  | CicNotationPt.Record (params,name,ty,fields) ->
-     let uri = match uri with Some uri -> uri | None -> assert false in
-     let context,params =
-      let context,res =
-       List.fold_left
-        (fun (context,res) (name,t) ->
-          let t =
-           match t with
-              None -> CicNotationPt.Implicit
-            | Some t -> t in
-          let name = CicNotationUtil.cic_name_of_name name in
-           name::context,(name, interpretate_term context env None false t)::res
-        ) ([],[]) params
-      in
-       context,List.rev res in
-     let add_params =
-      List.fold_right
-       (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
-     let ty' = add_params (interpretate_term context env None false ty) in
-     let fields' =
-      snd (
-       List.fold_left
-        (fun (context,res) (name,ty,_coercion,arity) ->
-          let context' = Cic.Name name :: context in
-           context',(name,interpretate_term context env None false ty)::res
-        ) (context,[]) fields) in
-     let concl =
-      (*here the explicit_named_substituion is assumed to be of length 0 *)
-      let mutind = Cic.MutInd (uri,0,[]) in
-      if params = [] then mutind
-      else
-       Cic.Appl
-        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
-     let con =
+      context,List.rev res in
+    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 t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
-       concl fields' in
-     let con' = add_params con in
-     let tyl = [name,true,ty',["mk_" ^ name,con']] in
-     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
-      Cic.InductiveDefinition
-       (tyl,[],List.length params,[`Class (`Record field_names)])
-*)
+       (fun (i,res) (name,_,_,_) ->
+         let nref =
+          NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+         in
+          i+1,(name,nref)::res)
+       (0,[]) tyl) in
+    let tyl =
+     List.map
+      (fun (name,_,ty,cl) ->
+        let ty' =
+         add_params
+         (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false ty) in
+        let cl' =
+         List.map
+          (fun (name,ty) ->
+            let ty' =
+             add_params
+              (interpretate_term ~obj_context ~context ~env ~uri:None
+                ~is_path:false ty) in
+            let relevance = [] in
+             relevance,name,ty'
+          ) cl in
+        let relevance = [] in
+         relevance,name,ty',cl'
+      ) tyl
+    in
+     let height = (* XXX calculate *) 0 in
+     let attrs = `Provided, `Regular in
+     uri, height, [], [], 
+     NCic.Inductive (inductive,leftno,tyl,attrs)
+ | CicNotationPt.Record (params,name,ty,fields) ->
+    let context,params =
+     let context,res =
+      List.fold_left
+       (fun (context,res) (name,t) ->
+         let t =
+          match t with
+             None -> CicNotationPt.Implicit `JustOne
+           | Some t -> t in
+         let name = cic_name_of_name name in
+         let t =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false t
+         in
+          (name,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
+     in
+      context,List.rev res in
+    let add_params =
+     List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
+    let leftno = List.length params in
+    let ty' =
+     add_params
+      (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+        ~is_path:false ty) in
+    let nref =
+     NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+    let obj_context = [name,nref] in
+    let fields' =
+     snd (
+      List.fold_left
+       (fun (context,res) (name,ty,_coercion,_arity) ->
+         let ty =
+          interpretate_term ~obj_context ~context ~env ~uri:None
+           ~is_path:false ty in
+         let context' = (name,NCic.Decl ty)::context in
+          context',(name,ty)::res
+       ) (context,[]) fields) in
+    let concl =
+     let mutind = NCic.Const nref in
+     if params = [] then mutind
+     else
+      NCic.Appl
+       (mutind::mk_rels (List.length params) (List.length fields)) in
+    let con =
+     List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in
+    let con' = add_params con in
+    let relevance = [] in
+    let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
+    let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
+     let height = (* XXX calculate *) 0 in
+     let attrs = `Provided, `Record field_names in
+     uri, height, [], [], 
+     NCic.Inductive (true,leftno,tyl,attrs)
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
-   ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~coercion_db ~lookup_in_library 
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
+   ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
@@ -580,21 +623,21 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
      ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~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
 ;;
 
 let disambiguate_obj 
-   ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~coercion_db ~lookup_in_library ~uri
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
+   ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
@@ -602,7 +645,7 @@ let disambiguate_obj
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_obj
      ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe 
      ~uri:(Some uri)
@@ -610,12 +653,13 @@ 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
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;
+(*
 let _ = 
 let mk_type n = 
   if n = 0 then
@@ -654,4 +698,5 @@ in
          NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
 
 ;;
+*)