The disambiguation now returns the aliases diff. It used to return the

new aliases and a slow diff operation was performed later on.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b66e12d5e4c15909c2a7badc1d454666168086d2..e9ce2e81ca002ea8572bf46a0e1209279a53a62a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -638,7 +638,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     CicNotationPt.term ->
-    (environment *                   (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term*
      CicUniv.universe_graph) list *  (* disambiguated term *)
@@ -651,7 +651,7 @@ sig
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
-    (environment *                   (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
@@ -790,12 +790,12 @@ in refine_profiler.CicUtil.profile foo ()
         | Invalid_choice -> Ko, ugraph
       in
       (* (4) build all possible interpretations *)
-      let rec aux aliases todo_dom base_univ =
+      let rec aux aliases diff todo_dom base_univ =
         match todo_dom with
         | [] ->
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
-               [ aliases, metasenv, thing, new_univ ]
+               [ aliases, diff, metasenv, thing, new_univ ]
             | Ko,_ | Uncertain,_ -> [])
         | item :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
@@ -806,16 +806,17 @@ in refine_profiler.CicUtil.profile foo ()
               | codomain_item :: tl ->
                   debug_print (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ;
                   let new_env = Environment.add item codomain_item aliases in
+                  let new_diff = (item,codomain_item)::diff in
                   (match test_env new_env remaining_dom univ with
                   | Ok (thing, metasenv),new_univ ->
                       (match remaining_dom with
-                      | [] -> [ new_env, metasenv, thing, new_univ ]
-                      | _ -> aux new_env remaining_dom new_univ )@ 
+                      | [] -> [ new_env, new_diff, metasenv, thing, new_univ ]
+                      | _ -> aux new_env new_diff remaining_dom new_univ )@ 
                         filter univ tl
                   | Uncertain,new_univ ->
                       (match remaining_dom with
                       | [] -> []
-                      | _ -> aux new_env remaining_dom new_univ )@ 
+                      | _ -> aux new_env new_diff remaining_dom new_univ )@ 
                         filter univ tl
                   | Ko,_ -> filter univ tl)
             in
@@ -824,16 +825,16 @@ in refine_profiler.CicUtil.profile foo ()
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases todo_dom base_univ with
+         match aux aliases [] todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
-         | [ e,me,t,u ] ->
+         | [_,diff,metasenv,t,ugraph] ->
              debug_print (lazy "SINGLE INTERPRETATION");
-             [ e,me,t,u ], false
+             [diff,metasenv,t,ugraph], false
          | l ->
              debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
-                 (fun (env, _, _, _) ->
+                 (fun (env, _, _, _, _) ->
                    List.map
                      (fun domain_item ->
                        let description =
@@ -844,19 +845,10 @@ in refine_profiler.CicUtil.profile foo ()
                  l
              in
              let choosed = C.interactive_interpretation_choice choices in
-             (List.map (List.nth l) choosed), true
+             (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
+              true
         in
-(*
-        (if benchmark then
-          let res_size = List.length res in
-          debug_print (lazy (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
+         res
      with
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 87e09daef7705cf3f9331a6073d3ea5fe332f0c5..1c6d4bbe7d3e3002462b237a7b6b93aa36a5e736 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -46,7 +46,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     DisambiguateTypes.term ->
-    (DisambiguateTypes.environment * (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term *
      CicUniv.universe_graph) list *  (* disambiguated term *)
@@ -60,7 +60,7 @@ sig
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
-    (DisambiguateTypes.environment * (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
@@ -83,7 +83,7 @@ sig
     ?initial_ugraph:CicUniv.universe_graph -> 
     ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*)
     string ->
-    (DisambiguateTypes.environment * (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                 (* new metasenv *)
      Cic.term *
      CicUniv.universe_graph) list   (* disambiguated term *)