From: Claudio Sacerdoti Coen 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