- let tests_no = List.length resolve_ids in
- if tests_no > 1 then
- output_html (outputhtml ())
- ("<h1>Disambiguation phase started: " ^
- string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
- (* now we select only the ones that generates well-typed terms *)
- let resolve_ids' =
- let rec filter =
- function
- [] -> []
- | resolve::tl ->
- let metasenv',expr = mk_metasenv_and_expr resolve in
- try
-(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
- let term,_,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
- in
- (* If metasen <> metasenv'' is a normal condition, we should *)
- (* be prepared to apply the returned substitution to the *)
- (* whole current proof. *)
- if metasenv <> metasenv'' then
- begin
- prerr_endline
- ("+++++ ASSERTION FAILED: " ^
- "a refine operation should not modify the metasenv") ;
- (* an assert would raise an exception that could be caught *)
- exit 1
- end ;
- (resolve,term,metasenv'')::(filter tl)
- with
- CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
- (try
- let term = CicTypeChecker.type_of_aux' metasenv' context expr in
- (resolve,term,metasenv')::(filter tl)
- with _ -> filter tl
- )
- | _ -> filter tl
- in
- filter resolve_ids
+ List.iter
+ (function (resolve,term,newmetasenv) ->
+ (* If metasen <> newmetasenv is a normal condition, we should *)
+ (* be prepared to apply the returned substitution to the *)
+ (* whole current proof. *)
+ if metasenv <> newmetasenv then
+ begin
+ prerr_endline
+ ("+++++ ASSERTION FAILED: " ^
+ "a refine operation should not modify the metasenv") ;
+ (* an assert would raise an exception that could be caught *)
+ exit 1
+ end
+ ) resolve_ids ;
+ let resolve_id',term,metasenv' =
+ match resolve_ids with
+ [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+ | [resolve_id] -> resolve_id
+ | _ ->
+ let choices =
+ List.map
+ (function (resolve,_,_) ->
+ List.map
+ (function id ->
+ id,
+ match resolve id with
+ None -> assert false
+ | Some uri ->
+ match uri with
+ CicTextualParser0.ConUri uri
+ | CicTextualParser0.VarUri uri ->
+ UriManager.string_of_uri uri
+ | CicTextualParser0.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ ")"
+ | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
+ ) dom
+ ) resolve_ids
+ in
+ let index = interactive_interpretation_choice choices in
+ List.nth resolve_ids index