X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b39d35f070f68bce422c3ded19ecc7b729a9ed50;hb=18ad62cacbbb08decd4332b0bab449e640114fd7;hp=055630971ee5edd3f5ca29b1aea0260c12429c89;hpb=cbe0302d6b0d2bca6657fa7479a62d0004665612;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 055630971..b39d35f07 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -56,20 +56,25 @@ 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 _ ->
+          debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
+          Ko,ugraph
+      | CicUnification.UnificationFailure s -> 
+	 prerr_endline ("PASSADI QUI: " ^ s);
+	   raise ( CicUnification.UnificationFailure s )
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -190,15 +195,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
@@ -219,7 +235,8 @@ let interpretate ~context ~env ast =
             match cic with
             | Cic.Const (uri, []) ->
                 let uris =
-                  match CicEnvironment.get_obj uri with
+		  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Constant (_, _, _, uris) -> uris
                   | _ -> assert false
@@ -227,7 +244,8 @@ let interpretate ~context ~env ast =
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
                 let uris =
-                  match CicEnvironment.get_obj uri with
+		  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Variable (_, _, _, uris) -> uris
                   | _ -> assert false
@@ -235,7 +253,8 @@ let interpretate ~context ~env ast =
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                 let uris =
-                  match CicEnvironment.get_obj uri with
+		  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
                   | _ -> assert false
@@ -243,7 +262,8 @@ let interpretate ~context ~env ast =
                 Cic.MutInd (uri, i, mk_subst uris)
             | Cic.MutConstruct (uri, i, j, []) ->
                 let uris =
-                  match CicEnvironment.get_obj uri with
+		  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
                   | _ -> assert false
@@ -362,6 +382,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) ->
@@ -404,6 +425,7 @@ let domain_of_term ~context ast =
     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
     | term -> aux CicAst.dummy_floc context term)
 
+
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
@@ -446,7 +468,7 @@ module Make (C: Callbacks) =
         uris
 
     let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
-      ~aliases:current_env
+      ?(initial_ugraph = CicUniv.empty_ugraph)  ~aliases:current_env
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -508,28 +530,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 =
@@ -565,15 +585,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 =
@@ -589,15 +608,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