Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 055630971ee5edd3f5ca29b1aea0260c12429c89..c384dc59fdbfc3a096996789260c0c4b9aa6261b 100644 (file)
--- 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
@@ -219,7 +224,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 uri CicUniv.empty_ugraph in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Constant (_, _, _, uris) -> uris
                   | _ -> assert false
@@ -227,7 +233,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 uri CicUniv.empty_ugraph in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Variable (_, _, _, uris) -> uris
                   | _ -> assert false
@@ -235,7 +242,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 uri CicUniv.empty_ugraph in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
                   | _ -> assert false
@@ -243,7 +251,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 uri CicUniv.empty_ugraph in
+                  match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
                   | _ -> assert false
@@ -404,6 +413,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 +456,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 +518,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 +573,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 +596,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