The disambiguation now returns a list of interpretations.

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
 

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 0e05413b8d68c0aeaaad68e2c2b221e949f29f69..640549544c45c460c9724a7a72b0b13fabb5930b 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -37,8 +37,8 @@ module Make (C : Callbacks) :
       Cic.metasenv ->
       CicAst.term ->
       aliases:environment ->  (* previous interpretation status *)
-        environment *                   (* new interpretation status *)
-        Cic.metasenv *                  (* new metasenv *)
-        Cic.term                        (* disambiguated term *)
+        (environment *                   (* new interpretation status *)
+         Cic.metasenv *                  (* new metasenv *)
+         Cic.term) list                 (* disambiguated term *)
   end
 

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
index 92ca39f72571a9732867b51c098be7c2fc487c36..07d5abc067a63630b4a23b4affb47e9aae8fc944 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
@@ -28,7 +28,7 @@ module type Callbacks =
       ?enable_button_for_non_vars:bool ->
       title:string -> msg:string -> id:string -> string list -> string list
     val interactive_interpretation_choice :
-      (string * string) list list -> int
+      (string * string) list list -> int list
     val input_or_locate_uri : title:string -> UriManager.uri
   end
 

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index b6130080f170378411f307b6ce9dc98cc9bdaf86..523fe4b70838e7835d674480346dba9ea0da4428 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
@@ -46,7 +46,7 @@ module type Callbacks =
       ?enable_button_for_non_vars:bool ->
       title:string -> msg:string -> id:string -> string list -> string list
     val interactive_interpretation_choice :
-      (string * string) list list -> int
+      (string * string) list list -> int list
     val input_or_locate_uri : title:string -> UriManager.uri
   end