X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=9f4c41d2e709e608b5f7497d27692d6737736598;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=93795f96ebb780eba031192d03ac15a16561a774;hpb=da49d2dca60a85abe54e0e549b290fa28a8127ba;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 93795f96e..9f4c41d2e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -34,7 +34,7 @@ exception NoWellTypedInterpretation
   (** raised when an environment is not enough informative to decide *)
 exception Try_again
 
-let debug = true
+let debug = false
 let debug_print = if debug then prerr_endline else ignore
 
 (*
@@ -56,25 +56,33 @@ type test_result =
   | Ko
   | Uncertain
 
-let refine metasenv context term =
+let refine metasenv context term ugraph =
 (*   if benchmark then incr actual_refinements; *)
-  let metasenv, term = CicMkImplicit.expand_implicits metasenv [] context term in
-  debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
-  try
-    let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
-    Ok (term', metasenv')
-  with
-    | CicRefine.Uncertain _ ->
-        debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
-        Uncertain
-    | CicRefine.RefineFailure _ ->
-        debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
-        Ko
+  let metasenv, term = 
+    CicMkImplicit.expand_implicits metasenv [] context term in
+    debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
+    try
+      let term', _, metasenv',ugraph1 = 
+	CicRefine.type_of_aux' metasenv context term ugraph in
+	(Ok (term', metasenv')),ugraph1
+    with
+      | CicRefine.Uncertain _ ->
+          debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+          Uncertain,ugraph
+      | CicRefine.RefineFailure msg ->
+          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+            (CicPp.ppterm term) msg);
+          Ko,ugraph
+      | CicUnification.UnificationFailure s -> 
+	 prerr_endline ("PASSADI QUI: " ^ s);
+	   raise ( CicUnification.UnificationFailure s )
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try
     snd (Environment.find item env) env num args
-  with Not_found -> assert false
+  with Not_found -> 
+    failwith ("Domain item not found: " ^ 
+      (DisambiguateTypes.string_of_domain_item item))
 
   (* TODO move it to Cic *)
 let find_in_environment name context =
@@ -190,15 +198,26 @@ let interpretate ~context ~env ast =
                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
-    | CicAst.Ident (name, subst) ->
+    | CicAst.Ident (name, subst)
+    | CicAst.Uri (name, subst) as ast ->
+        let is_uri = function CicAst.Uri _ -> true | _ -> false in
         (try
+          if is_uri ast then raise Not_found;(* don't search the env for URIs *)
           let index = find_in_environment name context in
           if subst <> None then
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
         with Not_found ->
-          let cic = resolve env (Id name) () in
+          let cic =
+            if is_uri ast then  (* we have the URI, build the term out of it *)
+              try
+                CicUtil.term_of_uri name
+              with UriManager.IllFormedUri _ ->
+                CicTextualParser2.fail loc "Ill formed URI"
+            else
+              resolve env (Id name) ()
+          in
           let mk_subst uris =
             let ids_to_uris =
               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
@@ -214,40 +233,23 @@ let interpretate ~context ~env ast =
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in
-          (* the try is for CicTypeChecker.typecheck *)
           (try 
             match cic with
             | Cic.Const (uri, []) ->
-                let uris =
-                  match CicEnvironment.get_obj uri with
-                  (*match CicTypeChecker.typecheck uri with*)
-                  | Cic.Constant (_, _, _, uris) -> uris
-                  | _ -> assert false
-                in
+                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
-                let uris =
-                  match CicEnvironment.get_obj uri with
-                  (*match CicTypeChecker.typecheck uri with*)
-                  | Cic.Variable (_, _, _, uris) -> uris
-                  | _ -> assert false
-                in
+                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
-                let uris =
-                  match CicEnvironment.get_obj uri with
-                  (*match CicTypeChecker.typecheck uri with*)
-                  | Cic.InductiveDefinition (_, uris, _) -> uris
-                  | _ -> assert false
-                in
+                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let uris = CicUtil.params_of_obj o in
                 Cic.MutInd (uri, i, mk_subst uris)
             | Cic.MutConstruct (uri, i, j, []) ->
-                let uris =
-                  match CicEnvironment.get_obj uri with
-                  (*match CicTypeChecker.typecheck uri with*)
-                  | Cic.InductiveDefinition (_, uris, _) -> uris
-                  | _ -> assert false
-                in
+                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
 (*
@@ -280,13 +282,14 @@ let interpretate ~context ~env ast =
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
+    | CicAst.UserInput -> assert false
   and aux_option loc context = function
     | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
   in
   match ast with
   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-  | term -> aux (-1, -1) context term
+  | term -> aux CicAst.dummy_floc context term
 
 let domain_of_term ~context ast =
     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
@@ -361,6 +364,7 @@ let domain_of_term ~context ast =
                   let dom' = aux loc context term in
                   dom' @ dom)
                 [Id name] subst))
+    | CicAst.Uri _ -> []
     | CicAst.Implicit -> []
     | CicAst.Num (num, i) -> [ Num i ]
     | CicAst.Meta (index, local_context) ->
@@ -368,6 +372,7 @@ let domain_of_term ~context ast =
           local_context
     | CicAst.Sort _ -> []
     | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+    | CicAst.UserInput -> assert false
 
   and aux_option loc context = function
     | None -> []
@@ -400,7 +405,7 @@ let domain_of_term ~context ast =
   rev_uniq
     (match ast with
     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-    | term -> aux (-1, -1) context term)
+    | term -> aux CicAst.dummy_floc context term)
 
 
   (* dom1 \ dom2 *)
@@ -414,15 +419,9 @@ let domain_diff dom1 dom2 =
 
 module Make (C: Callbacks) =
   struct
-    let choices_of_id mqi_handle id =
-     let query  =  MQueryGenerator.locate id in
-     let result = MQueryInterpreter.execute mqi_handle query in
-     let uris =
-      List.map
-       (function uri,_ ->
-         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
-       ) result in
-      let uris' =
+    let choices_of_id dbd id =
+      let uris = MetadataQuery.locate ~dbd id in
+      let uris =
        match uris with
         | [] ->
            [UriManager.string_of_uri (C.input_or_locate_uri
@@ -441,13 +440,17 @@ module Make (C: Callbacks) =
           (uri,
            let term =
              try
-               HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
-             with _ -> assert false
+               CicUtil.term_of_uri uri
+             with exn ->
+               prerr_endline uri;
+               prerr_endline (Printexc.to_string exn);
+               assert false
             in
            fun _ _ _ -> term))
-        uris'
+        uris
 
-    let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
+    let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -472,7 +475,7 @@ module Make (C: Callbacks) =
               (try
                 Hashtbl.find id_choices id
               with Not_found ->
-                let choices = choices_of_id mqi_handle id in
+                let choices = choices_of_id dbd id in
                 Hashtbl.add id_choices id choices;
                 choices)
           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
@@ -509,28 +512,26 @@ module Make (C: Callbacks) =
 
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
-      let test_env current_env todo_dom univ = 
+      let test_env current_env todo_dom ugraph = 
         let filled_env =
           List.fold_left
             (fun env item ->
-              Environment.add item
-                ("Implicit",
+               Environment.add item
+               ("Implicit",
                  (match item with
-                 | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
-                 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
+                    | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
+                    | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
             current_env todo_dom 
         in
         try
-          CicUniv.set_working univ; 
           let cic_term =
             interpretate ~context:disambiguate_context ~env:filled_env term
           in
-           let k = refine metasenv context cic_term in
-           let new_univ = CicUniv.get_working () in
-            (k , new_univ )
+          let k,ugraph1 = refine metasenv context cic_term ugraph in
+            (k , ugraph1 )
         with
-        | Try_again -> Uncertain,univ 
-        | DisambiguateChoices.Invalid_choice -> Ko,univ 
+        | Try_again -> Uncertain,ugraph
+        | DisambiguateChoices.Invalid_choice -> Ko,ugraph
       in
       (* (4) build all possible interpretations *)
       let rec aux current_env todo_dom base_univ =
@@ -566,15 +567,14 @@ module Make (C: Callbacks) =
             in
             filter base_univ choices 
       in
-       let base_univ = CicUniv.get_working () in
+      let base_univ = initial_ugraph in
       try
         let res =
          match aux current_env todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
          | [ e,me,t,u ] as l ->
              debug_print "UNA SOLA SCELTA";
-             CicUniv.set_working u;
-             [ e,me,t ]
+             [ e,me,t,u]
          | l ->
              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
              let choices =
@@ -590,15 +590,7 @@ module Make (C: Callbacks) =
                  l
              in
              let choosed = C.interactive_interpretation_choice choices in
-             let l' = List.map (List.nth l) choosed in
-             match l' with
-               [] -> assert false
-             | [e,me,t,u] -> 
-                 CicUniv.set_working u;
-                 (*CicUniv.print_working_graph ();*)
-                 [e,me,t]
-             | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *)
-                 List.map (fun (e,me,t,u) -> (e,me,t)) l'
+             List.map (List.nth l) choosed
         in
 (*
         (if benchmark then
@@ -613,6 +605,6 @@ module Make (C: Callbacks) =
         res
      with
       CicEnvironment.CircularDependency s -> 
-        raise (Failure "e chi la becca sta CircularDependency?");
+        failwith "Disambiguate: circular dependency"
   end