From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 2 Mar 2004 13:18:13 +0000 (+0000)
Subject: The disambiguation now returns a list of interpretations.
X-Git-Tag: v0_0_4~61
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dccf88890f1f9f8c8139f67aa7a26f8339b13502;p=helm.git

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 ca5f1449c..bc78f55ed 100644
--- 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 0e05413b8..640549544 100644
--- 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 92ca39f72..07d5abc06 100644
--- 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 b6130080f..523fe4b70 100644
--- 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