From: Claudio Sacerdoti Coen Date: Mon, 23 Dec 2002 21:36:52 +0000 (+0000) Subject: Ambiguous parsing improved: refining is now used to prune-out not-well-typed X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6e4f76ce06af1f10366bcc094a4be0df3ae8caa;p=helm.git Ambiguous parsing improved: refining is now used to prune-out not-well-typed choices as soon as the term can not be refined. Unfortunately the whole disambiguation is parsing-bound and not type-checking/refining bound. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index f81dffc85..d1b9b9964 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1315,6 +1315,11 @@ let locate_one_id id = exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;; exception AmbiguousInput;; +type test_result = + Ok of Cic.term * Cic.metasenv + | Ko + | Uncertain + let disambiguate_input context metasenv dom mk_metasenv_and_expr = let known_ids,resolve_id = !id_to_uris in let dom' = @@ -1328,98 +1333,141 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = in (* for each id in dom' we get the list of uris associated to it *) let list_of_uris = List.map locate_one_id dom' in - (* and now we compute the list of all possible assignments from id to uris *) + let tests_no = + List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris + in + if tests_no > 1 then + output_html (outputhtml ()) + ("

Disambiguation phase started: " ^ + string_of_int tests_no ^ " cases will be tried.") ; + (* and now we compute the list of all possible assignments from *) + (* id to uris that generate well-typed terms *) let resolve_ids = - let rec aux ids list_of_uris = + (* function to test if a partial interpretation is so far correct *) + let test resolve_id residual_dom = + (* We put implicits in place of every identifier that is not *) + (* resolved by resolve_id *) + let resolve_id'' = + let resolve_id' = + function id -> + match resolve_id id with + None -> None + | Some uri -> Some (CicTextualParser0.Uri uri) + in + List.fold_left + (fun f id -> + function id' -> + if id = id' then Some (CicTextualParser0.Implicit) else f id' + ) resolve_id' residual_dom + in + (* and we try to refine the term *) + let saved_status = !CicTextualParser0.metasenv in + let metasenv',expr = mk_metasenv_and_expr resolve_id'' in +(*CSC: Bug here: we do not try to typecheck also the metasenv' *) + (* The parser is imperative ==> we must restore the old status ;-(( *) + CicTextualParser0.metasenv := saved_status ; + try + let term,_,_,metasenv'' = + CicRefine.type_of_aux' metasenv' context expr + in + Ok (term,metasenv'') + with + CicRefine.MutCaseFixAndCofixRefineNotImplemented -> + (try + let term = CicTypeChecker.type_of_aux' metasenv' context expr in + Ok (term,metasenv') + with _ -> Ko + ) + | CicRefine.Uncertain _ -> +prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ; + Uncertain + | _ -> +prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; + Ko + in + let rec aux resolve_id ids list_of_uris = match ids,list_of_uris with - [],[] -> [resolve_id] + [],[] -> + (match test resolve_id [] with + Ok (term,metasenv) -> [resolve_id,term,metasenv] + | Ko | Uncertain -> []) | id::idtl,uris::uristl -> - let resolves = aux idtl uristl in - List.concat - (List.map - (function uri -> - List.map - (function f -> - function id' -> if id = id' then Some uri else f id' - ) resolves - ) uris - ) + let rec filter = + function + [] -> [] + | uri::uritl -> + let resolve_id' = + function id' -> if id = id' then Some uri else resolve_id id' + in + (match test resolve_id' idtl with + Ok (term,metasenv) -> + (* the next three ``if''s are used to avoid the base *) + (* case where the term would be refined a second time. *) + (if uristl = [] then + [resolve_id',term,metasenv] + else + (aux resolve_id' idtl uristl) + ) @ (filter uritl) + | Uncertain -> + (if uristl = [] then [] + else + (aux resolve_id' idtl uristl) + ) @ (filter uritl) + | Ko -> + filter uritl + ) + in + filter uris | _,_ -> assert false in - aux dom' list_of_uris + aux resolve_id dom' list_of_uris in - let tests_no = List.length resolve_ids in - if tests_no > 1 then - output_html (outputhtml ()) - ("

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 in - 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 - in - id_to_uris := known_ids @ dom', resolve_id' ; - metasenv',term + id_to_uris := known_ids @ dom', resolve_id' ; + metasenv',term ;; (* A WIDGET TO ENTER CIC TERMS *)