helm/ocaml/cic_disambiguation/disambiguate.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 open DisambiguateTypes
  29 open UriManager
  30
  31 exception No_choices of domain_item
  32 exception NoWellTypedInterpretation
  33
  34   (** raised when an environment is not enough informative to decide *)
  35 exception Try_again
  36
  37 let debug = false
  38 let debug_print = if debug then prerr_endline else ignore
  39
  40 (*
  41   (** print benchmark information *)
  42 let benchmark = true
  43 let max_refinements = ref 0       (* benchmarking is not thread safe *)
  44 let actual_refinements = ref 0
  45 let domain_size = ref 0
  46 let choices_avg = ref 0.
  47 *)
  48
  49 let descr_of_domain_item = function
  50  | Id s -> s
  51  | Symbol (s, _) -> s
  52  | Num i -> string_of_int i
  53
  54 type test_result =
  55   | Ok of Cic.term * Cic.metasenv
  56   | Ko
  57   | Uncertain
  58
  59 let refine metasenv context term ugraph =
  60 (*   if benchmark then incr actual_refinements; *)
  61   let metasenv, term =
  62     CicMkImplicit.expand_implicits metasenv [] context term in
  63     debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
  64     try
  65       let term', _, metasenv',ugraph1 =
  66         CicRefine.type_of_aux' metasenv context term ugraph in
  67         (Ok (term', metasenv')),ugraph1
  68     with
  69       | CicRefine.Uncertain _ ->
  70           debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
  71           Uncertain,ugraph
  72       | CicRefine.RefineFailure msg ->
  73           debug_print (
  74             (sprintf ("%%%%%% PRUNED!!!\n<<begin cause>>\n" ^^
  75               "%s\n<<end cause>>\n<<begin term>>\n%s\n<<end term>>")
  76               msg (CicPp.ppterm term)));
  77           Ko,ugraph
  78       | CicUnification.UnificationFailure s ->
  79          prerr_endline ("PASSADI QUI: " ^ s);
  80            raise ( CicUnification.UnificationFailure s )
  81
  82 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
  83   try
  84     snd (Environment.find item env) env num args
  85   with Not_found ->
  86     failwith ("Domain item not found: " ^
  87       (DisambiguateTypes.string_of_domain_item item))
  88
  89   (* TODO move it to Cic *)
  90 let find_in_environment name context =
  91   let rec aux acc = function
  92     | [] -> raise Not_found
  93     | Cic.Name hd :: tl when hd = name -> acc
  94     | _ :: tl ->  aux (acc + 1) tl
  95   in
  96   aux 1 context
  97
  98 let interpretate ~context ~env ast =
  99   let rec aux loc context = function
 100     | CicAst.AttributedTerm (`Loc loc, term) ->
 101         aux loc context term
 102     | CicAst.AttributedTerm (_, term) -> aux loc context term
 103     | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
 104         let cic_args = List.map (aux loc context) args in
 105         resolve env (Symbol (symb, i)) ~args:cic_args ()
 106     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
 107     | CicAst.Binder (binder_kind, (var, typ), body) ->
 108         let cic_type = aux_option loc context typ in
 109         let cic_body = aux loc (var :: context) body in
 110         (match binder_kind with
 111         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
 112         | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
 113         | `Exists ->
 114             resolve env (Symbol ("exists", 0))
 115               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
 116     | CicAst.Case (term, indty_ident, outtype, branches) ->
 117         let cic_term = aux loc context term in
 118         let cic_outtype = aux_option loc context outtype in
 119         let do_branch ((head, args), term) =
 120           let rec do_branch' context = function
 121             | [] -> aux loc context term
 122             | (name, typ) :: tl ->
 123                 let cic_body = do_branch' (name :: context) tl in
 124                 let typ =
 125                   match typ with
 126                   | None -> Cic.Implicit (Some `Type)
 127                   | Some typ -> aux loc context typ
 128                 in
 129                 Cic.Lambda (name, typ, cic_body)
 130           in
 131           do_branch' context args
 132         in
 133         let (indtype_uri, indtype_no) =
 134           match indty_ident with
 135           | Some indty_ident ->
 136               (match resolve env (Id indty_ident) () with
 137               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
 138               | Cic.Implicit _ -> raise Try_again
 139               | _ -> raise DisambiguateChoices.Invalid_choice)
 140           | None ->
 141               let fst_constructor =
 142                 match branches with
 143                 | ((head, _), _) :: _ -> head
 144                 | [] -> raise DisambiguateChoices.Invalid_choice
 145               in
 146               (match resolve env (Id fst_constructor) () with
 147               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
 148                   (indtype_uri, indtype_no)
 149               | Cic.Implicit _ -> raise Try_again
 150               | _ -> raise DisambiguateChoices.Invalid_choice)
 151         in
 152         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
 153           (List.map do_branch branches))
 154     | CicAst.LetIn ((name, typ), def, body) ->
 155         let cic_def = aux loc context def in
 156         let cic_def =
 157           match typ with
 158           | None -> cic_def
 159           | Some t -> Cic.Cast (cic_def, aux loc context t)
 160         in
 161         let cic_body = aux loc (name :: context) body in
 162         Cic.LetIn (name, cic_def, cic_body)
 163     | CicAst.LetRec (kind, defs, body) ->
 164         let context' =
 165           List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
 166             context defs
 167         in
 168         let cic_body = aux loc context' body in
 169         let inductiveFuns =
 170           List.map
 171             (fun ((name, typ), body, decr_idx) ->
 172               let cic_body = aux loc context' body in
 173               let cic_type = aux_option loc context typ in
 174               let name =
 175                 match name with
 176                 | Cic.Anonymous ->
 177                     CicTextualParser2.fail loc
 178                       "Recursive functions cannot be anonymous"
 179                 | Cic.Name name -> name
 180               in
 181               (name, decr_idx, cic_type, cic_body))
 182             defs
 183         in
 184         let counter = ref ~-1 in
 185         let build_term funs =
 186           (* this is the body of the fold_right function below. Rationale: Fix
 187            * and CoFix cases differs only in an additional index in the
 188            * inductiveFun list, see Cic.term *)
 189           match kind with
 190           | `Inductive ->
 191               (fun (var, _, _, _) cic ->
 192                 incr counter;
 193                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
 194           | `CoInductive ->
 195               let funs =
 196                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
 197               in
 198               (fun (var, _, _, _) cic ->
 199                 incr counter;
 200                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
 201         in
 202         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
 203     | CicAst.Ident (name, subst)
 204     | CicAst.Uri (name, subst) as ast ->
 205         let is_uri = function CicAst.Uri _ -> true | _ -> false in
 206         (try
 207           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
 208           let index = find_in_environment name context in
 209           if subst <> None then
 210             CicTextualParser2.fail loc
 211               "Explicit substitutions not allowed here";
 212           Cic.Rel index
 213         with Not_found ->
 214           let cic =
 215             if is_uri ast then  (* we have the URI, build the term out of it *)
 216               try
 217                 CicUtil.term_of_uri name
 218               with UriManager.IllFormedUri _ ->
 219                 CicTextualParser2.fail loc "Ill formed URI"
 220             else
 221               resolve env (Id name) ()
 222           in
 223           let mk_subst uris =
 224             let ids_to_uris =
 225               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
 226             in
 227             (match subst with
 228             | Some subst ->
 229                 List.map
 230                   (fun (s, term) ->
 231                     (try
 232                       List.assoc s ids_to_uris, aux loc context term
 233                      with Not_found ->
 234                        raise DisambiguateChoices.Invalid_choice))
 235                   subst
 236             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
 237           in
 238           (try
 239             match cic with
 240             | Cic.Const (uri, []) ->
 241                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 242                 let uris = CicUtil.params_of_obj o in
 243                 Cic.Const (uri, mk_subst uris)
 244             | Cic.Var (uri, []) ->
 245                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 246                 let uris = CicUtil.params_of_obj o in
 247                 Cic.Var (uri, mk_subst uris)
 248             | Cic.MutInd (uri, i, []) ->
 249                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 250                 let uris = CicUtil.params_of_obj o in
 251                 Cic.MutInd (uri, i, mk_subst uris)
 252             | Cic.MutConstruct (uri, i, j, []) ->
 253                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 254                 let uris = CicUtil.params_of_obj o in
 255                 Cic.MutConstruct (uri, i, j, mk_subst uris)
 256             | Cic.Meta _ | Cic.Implicit _ as t ->
 257 (*
 258                 prerr_endline (sprintf
 259                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
 260                   (CicPp.ppterm t)
 261                   (String.concat "; "
 262                     (List.map
 263                       (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
 264                       subst)));
 265 *)
 266                 t
 267             | _ ->
 268               raise DisambiguateChoices.Invalid_choice
 269            with
 270              CicEnvironment.CircularDependency _ ->
 271                raise DisambiguateChoices.Invalid_choice))
 272     | CicAst.Implicit -> Cic.Implicit None
 273     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
 274     | CicAst.Meta (index, subst) ->
 275         let cic_subst =
 276           List.map
 277             (function None -> None | Some term -> Some (aux loc context term))
 278             subst
 279         in
 280         Cic.Meta (index, cic_subst)
 281     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
 282     | CicAst.Sort `Set -> Cic.Sort Cic.Set
 283     | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
 284     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
 285     | CicAst.Symbol (symbol, instance) ->
 286         resolve env (Symbol (symbol, instance)) ()
 287     | CicAst.UserInput -> assert false
 288   and aux_option loc context = function
 289     | None -> Cic.Implicit (Some `Type)
 290     | Some term -> aux loc context term
 291   in
 292   match ast with
 293   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
 294   | term -> aux CicAst.dummy_floc context term
 295
 296 let domain_of_term ~context ast =
 297     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
 298      * Domain item more in deep in the list will be processed first.
 299      *)
 300   let rec aux loc context = function
 301     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
 302     | CicAst.AttributedTerm (_, term) -> aux loc context term
 303     | CicAst.Appl terms ->
 304         List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
 305     | CicAst.Binder (kind, (var, typ), body) ->
 306         let kind_dom =
 307           match kind with
 308           | `Exists -> [ Symbol ("exists", 0) ]
 309           | _ -> []
 310         in
 311         let type_dom = aux_option loc context typ in
 312         let body_dom = aux loc (var :: context) body in
 313         body_dom @ type_dom @ kind_dom
 314     | CicAst.Case (term, indty_ident, outtype, branches) ->
 315         let term_dom = aux loc context term in
 316         let outtype_dom = aux_option loc context outtype in
 317         let do_branch ((head, args), term) =
 318           let (term_context, args_domain) =
 319             List.fold_left
 320               (fun (cont, dom) (name, typ) ->
 321                 (name :: cont,
 322                  (match typ with
 323                  | None -> dom
 324                  | Some typ -> aux loc cont typ @ dom)))
 325               (context, []) args
 326           in
 327           args_domain @ aux loc term_context term
 328         in
 329         let branches_dom =
 330           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
 331         in
 332         branches_dom @ outtype_dom @ term_dom @
 333         (match indty_ident with None -> [] | Some ident -> [ Id ident ])
 334     | CicAst.LetIn ((var, typ), body, where) ->
 335         let body_dom = aux loc context body in
 336         let type_dom = aux_option loc context typ in
 337         let where_dom = aux loc (var :: context) where in
 338         where_dom @ type_dom @ body_dom
 339     | CicAst.LetRec (kind, defs, where) ->
 340         let context' =
 341           List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
 342             context defs
 343         in
 344         let where_dom = aux loc context' where in
 345         let defs_dom =
 346           List.fold_left
 347             (fun dom ((_, typ), body, _) ->
 348               aux loc context' body @ aux_option loc context typ)
 349             [] defs
 350         in
 351         where_dom @ defs_dom
 352     | CicAst.Ident (name, subst) ->
 353         (try
 354           let index = find_in_environment name context in
 355           if subst <> None then
 356             CicTextualParser2.fail loc
 357               "Explicit substitutions not allowed here"
 358           else
 359             []
 360         with Not_found ->
 361           (match subst with
 362           | None -> [Id name]
 363           | Some subst ->
 364               List.fold_left
 365                 (fun dom (_, term) ->
 366                   let dom' = aux loc context term in
 367                   dom' @ dom)
 368                 [Id name] subst))
 369     | CicAst.Uri _ -> []
 370     | CicAst.Implicit -> []
 371     | CicAst.Num (num, i) -> [ Num i ]
 372     | CicAst.Meta (index, local_context) ->
 373         List.fold_left (fun dom term -> aux_option loc context term @ dom) []
 374           local_context
 375     | CicAst.Sort _ -> []
 376     | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
 377     | CicAst.UserInput -> assert false
 378
 379   and aux_option loc context = function
 380     | None -> []
 381     | Some t -> aux loc context t
 382   in
 383
 384     (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
 385   let rev_uniq =
 386     let module SortedItem =
 387       struct
 388         type t = DisambiguateTypes.domain_item
 389         let compare = Pervasives.compare
 390       end
 391     in
 392     let module Set = Set.Make (SortedItem) in
 393     fun l ->
 394       let rev_l = List.rev l in
 395       let (_, uniq_rev_l) =
 396         List.fold_left
 397           (fun (members, rev_l) elt ->
 398             if Set.mem elt members then
 399               (members, rev_l)
 400             else
 401               Set.add elt members, elt :: rev_l)
 402           (Set.empty, []) rev_l
 403       in
 404       List.rev uniq_rev_l
 405   in
 406
 407   rev_uniq
 408     (match ast with
 409     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
 410     | term -> aux CicAst.dummy_floc context term)
 411
 412
 413   (* dom1 \ dom2 *)
 414 let domain_diff dom1 dom2 =
 415 (* let domain_diff = Domain.diff *)
 416   let is_in_dom2 =
 417     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
 418       (fun _ -> false) dom2
 419   in
 420   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 421
 422 module Make (C: Callbacks) =
 423   struct
 424     let choices_of_id ?owner dbd id =
 425       let uris = MetadataQuery.locate ?owner ~dbd id in
 426       let uris =
 427        match uris with
 428         | [] ->
 429            [UriManager.string_of_uri (C.input_or_locate_uri
 430             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
 431         | [uri] -> [uri]
 432         | _ ->
 433             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
 434              ~ok:"Try selected." ~enable_button_for_non_vars:true
 435              ~title:"Ambiguous input." ~id
 436              ~msg: ("Ambiguous input \"" ^ id ^
 437                 "\". Please, choose one or more interpretations:")
 438              uris
 439       in
 440       List.map
 441         (fun uri ->
 442           (uri,
 443            let term =
 444              try
 445                CicUtil.term_of_uri uri
 446              with exn ->
 447                prerr_endline uri;
 448                prerr_endline (Printexc.to_string exn);
 449                assert false
 450             in
 451            fun _ _ _ -> term))
 452         uris
 453
 454     let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
 455       ?(initial_ugraph = CicUniv.empty_ugraph) ?owner ~aliases:current_env
 456     =
 457       debug_print "NEW DISAMBIGUATE INPUT";
 458       let disambiguate_context =  (* cic context -> disambiguate context *)
 459         List.map
 460           (function None -> Cic.Anonymous | Some (name, _) -> name)
 461           context
 462       in
 463       let term_dom = domain_of_term ~context:disambiguate_context term in
 464       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
 465         (string_of_domain term_dom));
 466       let current_dom =
 467         Environment.fold (fun item _ dom -> item :: dom) current_env []
 468       in
 469       let todo_dom = domain_diff term_dom current_dom in
 470       (* (2) lookup function for any item (Id/Symbol/Num) *)
 471       let lookup_choices =
 472         let id_choices = Hashtbl.create 1023 in
 473         fun item ->
 474         let choices =
 475           match item with
 476           | Id id ->
 477               (try
 478                 Hashtbl.find id_choices id
 479               with Not_found ->
 480                 let choices = choices_of_id ?owner dbd id in
 481                 Hashtbl.add id_choices id choices;
 482                 choices)
 483           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
 484           | Num instance -> DisambiguateChoices.lookup_num_choices ()
 485         in
 486         if choices = [] then raise (No_choices item);
 487         choices
 488       in
 489
 490 (*
 491       (* <benchmark> *)
 492       let _ =
 493         if benchmark then begin
 494           let per_item_choices =
 495             List.map
 496               (fun dom_item ->
 497                 try
 498                   let len = List.length (lookup_choices dom_item) in
 499                   prerr_endline (sprintf "BENCHMARK %s: %d"
 500                     (string_of_domain_item dom_item) len);
 501                   len
 502                 with No_choices _ -> 0)
 503               term_dom
 504           in
 505           max_refinements := List.fold_left ( * ) 1 per_item_choices;
 506           actual_refinements := 0;
 507           domain_size := List.length term_dom;
 508           choices_avg :=
 509             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
 510         end
 511       in
 512       (* </benchmark> *)
 513 *)
 514
 515       (* (3) test an interpretation filling with meta uninterpreted identifiers
 516        *)
 517       let test_env current_env todo_dom ugraph =
 518         let filled_env =
 519           List.fold_left
 520             (fun env item ->
 521                Environment.add item
 522                ("Implicit",
 523                  (match item with
 524                     | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
 525                     | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
 526             current_env todo_dom
 527         in
 528         try
 529           let cic_term =
 530             interpretate ~context:disambiguate_context ~env:filled_env term
 531           in
 532           let k,ugraph1 = refine metasenv context cic_term ugraph in
 533             (k , ugraph1 )
 534         with
 535         | Try_again -> Uncertain,ugraph
 536         | DisambiguateChoices.Invalid_choice -> Ko,ugraph
 537       in
 538       (* (4) build all possible interpretations *)
 539       let rec aux current_env todo_dom base_univ =
 540         match todo_dom with
 541         | [] ->
 542             (match test_env current_env [] base_univ with
 543             | Ok (term, metasenv),new_univ ->
 544                                [ current_env, metasenv, term, new_univ ]
 545             | Ko,_ | Uncertain,_ -> [])
 546         | item :: remaining_dom ->
 547             debug_print (sprintf "CHOOSED ITEM: %s"
 548              (string_of_domain_item item));
 549             let choices = lookup_choices item in
 550             let rec filter univ = function
 551               | [] -> []
 552               | codomain_item :: tl ->
 553                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
 554                   let new_env =
 555                     Environment.add item codomain_item current_env
 556                   in
 557                   (match test_env new_env remaining_dom univ with
 558                   | Ok (term, metasenv),new_univ ->
 559                       (match remaining_dom with
 560                       | [] -> [ new_env, metasenv, term, new_univ ]
 561                       | _ -> aux new_env remaining_dom new_univ )@
 562                         filter univ tl
 563                   | Uncertain,new_univ ->
 564                       (match remaining_dom with
 565                       | [] -> []
 566                       | _ -> aux new_env remaining_dom new_univ )@
 567                         filter univ tl
 568                   | Ko,_ -> filter univ tl)
 569             in
 570             filter base_univ choices
 571       in
 572       let base_univ = initial_ugraph in
 573       try
 574         let res =
 575          match aux current_env todo_dom base_univ with
 576          | [] -> raise NoWellTypedInterpretation
 577          | [ e,me,t,u ] as l ->
 578              debug_print "UNA SOLA SCELTA";
 579              [ e,me,t,u]
 580          | l ->
 581              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
 582              let choices =
 583                List.map
 584                  (fun (env, _, _, _) ->
 585                    List.map
 586                      (fun domain_item ->
 587                        let description =
 588                          fst (Environment.find domain_item env)
 589                        in
 590                        (descr_of_domain_item domain_item, description))
 591                      term_dom)
 592                  l
 593              in
 594              let choosed = C.interactive_interpretation_choice choices in
 595              List.map (List.nth l) choosed
 596         in
 597 (*
 598         (if benchmark then
 599           let res_size = List.length res in
 600           prerr_endline (sprintf
 601             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
 602             "BENCHMARK:   estimated %.2f")
 603             !actual_refinements !max_refinements !domain_size res_size
 604             !choices_avg
 605             (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
 606 *)
 607         res
 608      with
 609       CicEnvironment.CircularDependency s ->
 610         failwith "Disambiguate: circular dependency"
 611   end
 612