X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=93795f96ebb780eba031192d03ac15a16561a774;hb=fd648e40eb2c9c5b29cfa4408459511a74898d1d;hp=41c404392f429b2ac4a68debe6c5f9c36207a34c;hpb=616ca3a4330ac51127b0bd91644354ac888d1ce3;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 41c404392..93795f96e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -37,6 +37,15 @@ exception Try_again
 let debug = true
 let debug_print = if debug then prerr_endline else ignore
 
+(*
+  (** print benchmark information *)
+let benchmark = true
+let max_refinements = ref 0       (* benchmarking is not thread safe *)
+let actual_refinements = ref 0
+let domain_size = ref 0
+let choices_avg = ref 0.
+*)
+
 let descr_of_domain_item = function
  | Id s -> s
  | Symbol (s, _) -> s
@@ -48,7 +57,8 @@ type test_result =
   | Uncertain
 
 let refine metasenv context term =
-  let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
+(*   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
@@ -57,12 +67,14 @@ let refine metasenv context term =
     | CicRefine.Uncertain _ ->
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
-    | _ ->
+    | CicRefine.RefineFailure _ ->
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
-  snd (Environment.find item env) env num args
+  try
+    snd (Environment.find item env) env num args
+  with Not_found -> assert false
 
   (* TODO move it to Cic *)
 let find_in_environment name context =
@@ -75,13 +87,14 @@ let find_in_environment name context =
 
 let interpretate ~context ~env ast =
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-    | CicTextualParser2Ast.Appl terms ->
-        Cic.Appl (List.map (aux loc context) terms)
-    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
+    | CicAst.AttributedTerm (`Loc loc, term) ->
+        aux loc context term
+    | CicAst.AttributedTerm (_, term) -> aux loc context term
+    | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux loc context) args in
         resolve env (Symbol (symb, i)) ~args:cic_args ()
-    | CicTextualParser2Ast.Binder (binder_kind, (var, typ), body) ->
+    | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+    | CicAst.Binder (binder_kind, (var, typ), body) ->
         let cic_type = aux_option loc context typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
@@ -90,7 +103,7 @@ let interpretate ~context ~env ast =
         | `Exists ->
             resolve env (Symbol ("exists", 0))
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
-    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
+    | CicAst.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
         let cic_outtype = aux_option loc context outtype in
         let do_branch ((head, args), term) =
@@ -100,7 +113,7 @@ let interpretate ~context ~env ast =
                 let cic_body = do_branch' (name :: context) tl in
                 let typ =
                   match typ with
-                  | None -> Cic.Implicit
+                  | None -> Cic.Implicit (Some `Type)
                   | Some typ -> aux loc context typ
                 in
                 Cic.Lambda (name, typ, cic_body)
@@ -108,14 +121,27 @@ let interpretate ~context ~env ast =
           do_branch' context args
         in
         let (indtype_uri, indtype_no) =
-          match resolve env (Id indty_ident) () with
-          | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit -> raise Try_again
-          | _ -> raise DisambiguateChoices.Invalid_choice
+          match indty_ident with
+          | Some indty_ident ->
+              (match resolve env (Id indty_ident) () with
+              | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
+              | Cic.Implicit _ -> raise Try_again
+              | _ -> raise DisambiguateChoices.Invalid_choice)
+          | None ->
+              let fst_constructor =
+                match branches with
+                | ((head, _), _) :: _ -> head
+                | [] -> raise DisambiguateChoices.Invalid_choice
+              in
+              (match resolve env (Id fst_constructor) () with
+              | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
+                  (indtype_uri, indtype_no)
+              | Cic.Implicit _ -> raise Try_again
+              | _ -> raise DisambiguateChoices.Invalid_choice)
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
-    | CicTextualParser2Ast.LetIn ((name, typ), def, body) ->
+    | CicAst.LetIn ((name, typ), def, body) ->
         let cic_def = aux loc context def in
         let cic_def =
           match typ with
@@ -124,7 +150,7 @@ let interpretate ~context ~env ast =
         in
         let cic_body = aux loc (name :: context) body in
         Cic.LetIn (name, cic_def, cic_body)
-    | CicTextualParser2Ast.LetRec (kind, defs, body) ->
+    | CicAst.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
             context defs
@@ -164,49 +190,123 @@ 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
-    | CicTextualParser2Ast.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
+    | CicAst.Ident (name, subst) ->
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
-        with Not_found -> resolve env (Id name) ())
-    | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num ()
-    | CicTextualParser2Ast.Meta (index, subst) ->
+        with Not_found ->
+          let cic = resolve env (Id name) () in
+          let mk_subst uris =
+            let ids_to_uris =
+              List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
+            in
+            (match subst with
+            | Some subst ->
+                List.map
+                  (fun (s, term) ->
+                    (try
+                      List.assoc s ids_to_uris, aux loc context term
+                     with Not_found ->
+                       raise DisambiguateChoices.Invalid_choice))
+                  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
+                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
+                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
+                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
+                Cic.MutConstruct (uri, i, j, mk_subst uris)
+            | Cic.Meta _ | Cic.Implicit _ as t ->
+(*
+                prerr_endline (sprintf
+                  "Warning: %s must be instantiated with _[%s] but we do not enforce it"
+                  (CicPp.ppterm t)
+                  (String.concat "; "
+                    (List.map
+                      (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
+                      subst)));
+*)
+                t
+            | _ ->
+              raise DisambiguateChoices.Invalid_choice
+           with 
+             CicEnvironment.CircularDependency _ -> 
+               raise DisambiguateChoices.Invalid_choice))
+    | CicAst.Implicit -> Cic.Implicit None
+    | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
+    | CicAst.Meta (index, subst) ->
         let cic_subst =
           List.map
             (function None -> None | Some term -> Some (aux loc context term))
             subst
         in
         Cic.Meta (index, cic_subst)
-    | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop
-    | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set
-    | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type
-    | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
+    | CicAst.Sort `Set -> Cic.Sort Cic.Set
+    | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicAst.Symbol (symbol, instance) ->
+        resolve env (Symbol (symbol, instance)) ()
   and aux_option loc context = function
-    | None -> Cic.Implicit
+    | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
   in
   match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-  | _ -> assert false
+  | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+  | term -> aux (-1, -1) context term
 
 let domain_of_term ~context ast =
+    (* "aux" keeps domain in reverse order and doesn't care about duplicates.
+     * Domain item more in deep in the list will be processed first.
+     *)
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
-    | CicTextualParser2Ast.Appl terms ->
-        List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
-          Domain.empty terms
-    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
-        List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
-          (Domain.singleton (Symbol (symb, i))) args
-    | CicTextualParser2Ast.Binder (_, (var, typ), body) ->
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | CicAst.AttributedTerm (_, term) -> aux loc context term
+    | CicAst.Appl terms ->
+        List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
+    | CicAst.Binder (kind, (var, typ), body) ->
+        let kind_dom =
+          match kind with
+          | `Exists -> [ Symbol ("exists", 0) ]
+          | _ -> []
+        in
         let type_dom = aux_option loc context typ in
         let body_dom = aux loc (var :: context) body in
-        Domain.union type_dom body_dom
-    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
+        body_dom @ type_dom @ kind_dom
+    | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
         let do_branch ((head, args), term) =
@@ -216,27 +316,22 @@ let domain_of_term ~context ast =
                 (name :: cont,
                  (match typ with
                  | None -> dom
-                 | Some typ -> Domain.union dom (aux loc cont typ))))
-              (context, Domain.empty) args
+                 | Some typ -> aux loc cont typ @ dom)))
+              (context, []) args
           in
-          Domain.union (aux loc term_context term) args_domain
+          args_domain @ aux loc term_context term
         in
         let branches_dom =
-          List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
-            Domain.empty branches
+          List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
-        Domain.add (Id indty_ident)
-          (Domain.union outtype_dom (Domain.union term_dom branches_dom))
-    | CicTextualParser2Ast.LetIn ((var, typ), body, where) ->
+        branches_dom @ outtype_dom @ term_dom @
+        (match indty_ident with None -> [] | Some ident -> [ Id ident ])
+    | CicAst.LetIn ((var, typ), body, where) ->
         let body_dom = aux loc context body in
-        let type_dom = 
-          match typ with
-          | None -> Domain.empty
-          | Some typ -> aux loc context typ
-        in
+        let type_dom = aux_option loc context typ in
         let where_dom = aux loc (var :: context) where in
-        Domain.union (Domain.union body_dom where_dom) type_dom
-    | CicTextualParser2Ast.LetRec (kind, defs, where) ->
+        where_dom @ type_dom @ body_dom
+    | CicAst.LetRec (kind, defs, where) ->
         let context' =
           List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
             context defs
@@ -245,32 +340,77 @@ let domain_of_term ~context ast =
         let defs_dom =
           List.fold_left
             (fun dom ((_, typ), body, _) ->
-              Domain.union (aux loc context' body) (aux_option loc context typ))
-            Domain.empty defs
+              aux loc context' body @ aux_option loc context typ)
+            [] defs
         in
-        Domain.union where_dom defs_dom
-    | CicTextualParser2Ast.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
+        where_dom @ defs_dom
+    | CicAst.Ident (name, subst) ->
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
-              "Explicit substitutions not allowed here";
-          Domain.empty
-        with Not_found -> Domain.singleton (Id name))
-    | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)
-    | CicTextualParser2Ast.Meta (index, local_context) ->
-        List.fold_left
-          (fun dom term -> Domain.union dom (aux_option loc context term))
-            Domain.empty local_context
-    | CicTextualParser2Ast.Sort _ -> Domain.empty
+              "Explicit substitutions not allowed here"
+          else
+            []
+        with Not_found ->
+          (match subst with
+          | None -> [Id name]
+          | Some subst ->
+              List.fold_left
+                (fun dom (_, term) ->
+                  let dom' = aux loc context term in
+                  dom' @ dom)
+                [Id name] subst))
+    | CicAst.Implicit -> []
+    | CicAst.Num (num, i) -> [ Num i ]
+    | CicAst.Meta (index, local_context) ->
+        List.fold_left (fun dom term -> aux_option loc context term @ dom) []
+          local_context
+    | CicAst.Sort _ -> []
+    | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+
   and aux_option loc context = function
-    | None -> Domain.empty
+    | None -> []
     | Some t -> aux loc context t
   in
-  match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-  | _ -> assert false
+
+    (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
+  let rev_uniq =
+    let module SortedItem =
+      struct
+        type t = DisambiguateTypes.domain_item
+        let compare = Pervasives.compare
+      end
+    in
+    let module Set = Set.Make (SortedItem) in
+    fun l ->
+      let rev_l = List.rev l in
+      let (_, uniq_rev_l) =
+        List.fold_left
+          (fun (members, rev_l) elt ->
+            if Set.mem elt members then
+              (members, rev_l)
+            else
+              Set.add elt members, elt :: rev_l)
+          (Set.empty, []) rev_l
+      in
+      List.rev uniq_rev_l
+  in
+            
+  rev_uniq
+    (match ast with
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | term -> aux (-1, -1) context term)
+
+
+  (* dom1 \ dom2 *)
+let domain_diff dom1 dom2 =
+(* let domain_diff = Domain.diff *)
+  let is_in_dom2 =
+    List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
+      (fun _ -> false) dom2
+  in
+  List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 
 module Make (C: Callbacks) =
   struct
@@ -282,18 +422,11 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      C.output_html (`Msg (`T "Locate query:"));
-      MQueryUtil.text_of_query
-       (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
-       "" query; 
-      C.output_html (`Msg (`T "Result:"));
-      MQueryUtil.text_of_result
-        (fun s -> C.output_html (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->
            [UriManager.string_of_uri (C.input_or_locate_uri
-            ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+            ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
         | [uri] -> [uri]
         | _ ->
             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
@@ -316,10 +449,6 @@ module Make (C: Callbacks) =
 
     let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
     =
-      let current_dom = (* TODO temporary, remove ASAP *)
-        Environment.fold (fun item _ dom -> Domain.add item dom)
-          current_env Domain.empty
-      in
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
         List.map
@@ -329,7 +458,10 @@ module Make (C: Callbacks) =
       let term_dom = domain_of_term ~context:disambiguate_context term in
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain term_dom));
-      let todo_dom = Domain.diff term_dom current_dom in
+      let current_dom =
+        Environment.fold (fun item _ dom -> item :: dom) current_env []
+      in
+      let todo_dom = domain_diff term_dom current_dom in
       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
         let id_choices = Hashtbl.create 1023 in
@@ -349,80 +481,138 @@ module Make (C: Callbacks) =
         if choices = [] then raise (No_choices item);
         choices
       in
+
+(*
+      (* <benchmark> *)
+      let _ =
+        if benchmark then begin
+          let per_item_choices =
+            List.map
+              (fun dom_item ->
+                try
+                  let len = List.length (lookup_choices dom_item) in
+                  prerr_endline (sprintf "BENCHMARK %s: %d"
+                    (string_of_domain_item dom_item) len);
+                  len
+                with No_choices _ -> 0)
+              term_dom
+          in
+          max_refinements := List.fold_left ( * ) 1 per_item_choices;
+          actual_refinements := 0;
+          domain_size := List.length term_dom;
+          choices_avg :=
+            (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
+        end
+      in
+      (* </benchmark> *)
+*)
+
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
-      let test_env current_env todo_dom =
+      let test_env current_env todo_dom univ = 
         let filled_env =
-          Domain.fold
-            (fun item env ->
-              Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
-            todo_dom current_env
+          List.fold_left
+            (fun env item ->
+              Environment.add item
+                ("Implicit",
+                 (match item with
+                 | 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
-          refine metasenv context cic_term
+           let k = refine metasenv context cic_term in
+           let new_univ = CicUniv.get_working () in
+            (k , new_univ )
         with
-        | Try_again -> Uncertain
-        | DisambiguateChoices.Invalid_choice -> Ko
+        | Try_again -> Uncertain,univ 
+        | DisambiguateChoices.Invalid_choice -> Ko,univ 
       in
       (* (4) build all possible interpretations *)
-      let rec aux current_env todo_dom =
-        if Domain.is_empty todo_dom then
-          match test_env current_env Domain.empty with
-          | Ok (term, metasenv) -> [ current_env, term, metasenv ]
-          | Ko | Uncertain -> []
-        else
-          let item = Domain.choose todo_dom in
-          let remaining_dom = Domain.remove item todo_dom in
-          debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item));
-          let choices = lookup_choices item in
-          let rec filter = function
-            | [] -> []
-            | codomain_item :: tl ->
-                let new_env = Environment.add item codomain_item current_env in
-                (match test_env new_env remaining_dom with
-                | Ok (term, metasenv) ->
-                    (if Domain.is_empty remaining_dom then
-                      [ new_env, term, metasenv ]
-                    else
-                      aux new_env remaining_dom)
-                    @ filter tl
-                | Uncertain ->
-                    (if Domain.is_empty remaining_dom then
-                      []
-                    else
-                      aux new_env remaining_dom)
-                    @ filter tl
-                | Ko -> filter tl)
-          in
-          filter choices
-      in
-      let (choosed_env, choosed_term, choosed_metasenv) =
-        match aux current_env todo_dom with
-        | [] -> raise NoWellTypedInterpretation
-        | [ x ] ->
-            debug_print "UNA SOLA SCELTA";
-            x
-        | l ->
-            debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
-            let choices =
-              List.map
-                (fun (env, _, _) ->
-                  List.map
-                    (fun domain_item ->
-                      let description =
-                        fst (Environment.find domain_item env)
-                      in
-                      (descr_of_domain_item domain_item, description))
-                    (Domain.elements term_dom))
-                l
+      let rec aux current_env todo_dom base_univ =
+        match todo_dom with
+        | [] ->
+            (match test_env current_env [] base_univ with
+            | Ok (term, metasenv),new_univ -> 
+                               [ current_env, metasenv, term, new_univ ]
+            | Ko,_ | Uncertain,_ -> [])
+        | item :: remaining_dom ->
+            debug_print (sprintf "CHOOSED ITEM: %s"
+             (string_of_domain_item item));
+            let choices = lookup_choices item in
+            let rec filter univ = function 
+              | [] -> []
+              | codomain_item :: tl ->
+                  debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
+                  let new_env =
+                    Environment.add item codomain_item current_env
+                  in
+                  (match test_env new_env remaining_dom univ with
+                  | Ok (term, metasenv),new_univ ->
+                      (match remaining_dom with
+                      | [] -> [ new_env, metasenv, term, new_univ ]
+                      | _ -> aux new_env remaining_dom new_univ )@ 
+                        filter univ tl
+                  | Uncertain,new_univ ->
+                      (match remaining_dom with
+                      | [] -> []
+                      | _ -> aux new_env remaining_dom new_univ )@ 
+                        filter univ tl
+                  | Ko,_ -> filter univ tl)
             in
-            let choosed = C.interactive_interpretation_choice choices in
-            List.nth l choosed
+            filter base_univ choices 
       in
-      (choosed_env, choosed_metasenv, choosed_term)
-
+       let base_univ = CicUniv.get_working () 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 ]
+         | l ->
+             debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
+             let choices =
+               List.map
+                 (fun (env, _, _, _) ->
+                   List.map
+                     (fun domain_item ->
+                       let description =
+                         fst (Environment.find domain_item env)
+                       in
+                       (descr_of_domain_item domain_item, description))
+                     term_dom)
+                 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'
+        in
+(*
+        (if benchmark then
+          let res_size = List.length res in
+          prerr_endline (sprintf
+            ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
+            "BENCHMARK:   estimated %.2f")
+            !actual_refinements !max_refinements !domain_size res_size
+            !choices_avg
+            (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
+*)
+        res
+     with
+      CicEnvironment.CircularDependency s -> 
+        raise (Failure "e chi la becca sta CircularDependency?");
   end