The disambiguation now returns a list of interpretations.

[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 ca5f1449c961826f35516c629c59f23ec7402079..bc78f55eddc0888d80dba682c7b3a6edeeef27bf 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -491,7 +491,7 @@ module Make (C: Callbacks) =
         match todo_dom with
         | [] ->
             (match test_env current_env [] with
-            | Ok (term, metasenv) -> [ current_env, term, metasenv ]
+            | Ok (term, metasenv) -> [ current_env, metasenv, term ]
             | Ko | Uncertain -> [])
         | item :: remaining_dom ->
             debug_print (sprintf "CHOOSED ITEM: %s"
@@ -507,7 +507,7 @@ module Make (C: Callbacks) =
                   (match test_env new_env remaining_dom with
                   | Ok (term, metasenv) ->
                       (match remaining_dom with
-                      | [] -> [ new_env, term, metasenv ]
+                      | [] -> [ new_env, metasenv, term ]
                       | _ -> aux new_env remaining_dom) @ filter tl
                   | Uncertain ->
                       (match remaining_dom with
@@ -517,30 +517,27 @@ module Make (C: Callbacks) =
             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))
-                    term_dom)
-                l
-            in
-            let choosed = C.interactive_interpretation_choice choices in
-            List.nth l choosed
-      in
-      (choosed_env, choosed_metasenv, choosed_term)
+       match aux current_env todo_dom with
+       | [] -> raise NoWellTypedInterpretation
+       | [ _ ] as l ->
+           debug_print "UNA SOLA SCELTA";
+           l
+       | 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
+            List.map (List.nth l) choosed
 
   end