X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fdisambiguate.ml;h=afa47790ac3254173e4b2f708e8a2d570ba0d9f9;hb=69789d216abc552d2538089fd62b53af6f75b8b8;hp=c0e1818e1d18532c6fe480c6f00d05e81112b463;hpb=0b360e3e0202f27b62f1d3804315b665aca1a15a;p=helm.git diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index c0e1818e1..afa47790a 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -51,6 +51,12 @@ let get_last_query = module type Callbacks = sig + (* The following two functions are used to save/restore the metasenv *) + (* before/after the parsing. *) + (*CSC: This should be made functional sooner or later! *) + val get_metasenv : unit -> Cic.metasenv + val set_metasenv : Cic.metasenv -> unit + val output_html : string -> unit val interactive_user_uri_choice : selection_mode:[`SINGLE | `EXTENDED] -> @@ -64,7 +70,8 @@ module type Callbacks = ;; type domain_and_interpretation = - string list * (string -> CicTextualParser0.uri option) + CicTextualParser0.interpretation_domain_item list * + CicTextualParser0.interpretation ;; module Make(C:Callbacks) = @@ -110,6 +117,10 @@ module Make(C:Callbacks) = | Ko | Uncertain + type ambiguous_choices = + Uris of CicTextualParser0.uri list + | Symbols of (CicTextualParser0.interpretation -> Cic.term) list + let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris= let known_ids,resolve_id = id_to_uris in let dom' = @@ -122,13 +133,29 @@ module Make(C:Callbacks) = filter dom 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 + let list_of_uris = + List.map + (function + CicTextualParser0.Id id -> Uris (locate_one_id id) + | CicTextualParser0.Symbol (descr,choices) -> + (* CSC: Implementare la funzione di filtraggio manuale *) + (* CSC: corrispondente alla locate_one_id *) + Symbols (List.map snd choices) + ) dom' in let tests_no = - List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris + List.fold_left + (fun i uris -> + let len = + match uris with + Uris l -> List.length l + | Symbols l -> List.length l + in + i * len + ) 1 list_of_uris in if tests_no > 1 then C.output_html - ("

Disambiguation phase started: " ^ + ("

Disambiguation phase started: up to " ^ 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 *) @@ -137,25 +164,19 @@ module Make(C:Callbacks) = 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 + let resolve_id' = + 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 + let saved_status = C.get_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 ; + C.set_metasenv saved_status ; try let term,_,_,metasenv'' = CicRefine.type_of_aux' metasenv' context expr @@ -185,7 +206,7 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; let rec filter = function [] -> [] - | uri::uritl -> + | (uri : CicTextualParser0.interpretation_codomain_item)::uritl -> let resolve_id' = function id' -> if id = id' then Some uri else resolve_id id' in @@ -207,7 +228,14 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; filter uritl ) in - filter uris + (match uris with + Uris uris -> + filter + (List.map (function uri -> CicTextualParser0.Uri uri) uris) + | Symbols symbols -> + filter + (List.map + (function sym -> CicTextualParser0.Term sym) symbols)) | _,_ -> assert false in aux resolve_id dom' list_of_uris @@ -236,20 +264,27 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; (function (resolve,_,_) -> List.map (function id -> - id, + (match id with + CicTextualParser0.Id id -> id + | CicTextualParser0.Symbol (descr,_) -> descr + ), 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 ^ ")" + | Some (CicTextualParser0.Uri 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 ^ ")") + | Some (CicTextualParser0.Term term) -> + (* CSC: Implementare resa delle scelte *) + "To be implemented XXX01" + | Some CicTextualParser0.Implicit -> assert false ) dom ) resolve_ids in