+++ /dev/null
-(* Copyright (C) 2000-2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 06/01/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-(** This module provides a functor to disambiguate the input **)
-(** given a set of user-interface call-backs **)
-
-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] ->
- ?ok:string ->
- ?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
- val input_or_locate_uri : title:string -> UriManager.uri
- end
-;;
-
-type domain_and_interpretation =
- CicTextualParser0.interpretation_domain_item list *
- CicTextualParser0.interpretation
-;;
-
-module Make(C:Callbacks) =
- struct
-
- let locate_one_id mqi_handle id =
- let query = MQueryGenerator.locate id in
- let result = MQueryInterpreter.execute mqi_handle query in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- C.output_html "<h1>Locate Query: </h1><pre>";
- MQueryUtil.text_of_query C.output_html query "";
- C.output_html "<h1>Result:</h1>";
- MQueryUtil.text_of_result C.output_html result "<br>";
- let uris' =
- match uris with
- [] ->
- [UriManager.string_of_uri
- (C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
- | [uri] -> [uri]
- | _ ->
- C.interactive_user_uri_choice
- ~selection_mode:`EXTENDED
- ~ok:"Try every selection."
- ~enable_button_for_non_vars:true
- ~title:"Ambiguous input."
- ~msg:
- ("Ambiguous input \"" ^ id ^
- "\". Please, choose one or more interpretations:")
- ~id
- uris
- in
- List.map MQueryMisc.cic_textual_parser_uri_of_string uris'
-
-
- exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
-
- type test_result =
- Ok of Cic.term * Cic.metasenv
- | Ko
- | Uncertain
-
- type ambiguous_choices =
- Uris of CicTextualParser0.uri list
- | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
-
- let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
- let known_ids,resolve_id = id_to_uris in
- let dom' =
- let rec filter =
- function
- [] -> []
- | he::tl ->
- if List.mem he known_ids then filter tl else he::(filter tl)
- in
- filter dom
- in
- (* for each id in dom' we get the list of uris associated to it *)
- let list_of_uris =
- List.map
- (function
- CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle 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 ->
- 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
- ("<h1>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 *)
- let resolve_ids =
- (* 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' =
- 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 = 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 ;-(( *)
- C.set_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
- [],[] ->
- (match test resolve_id [] with
- Ok (term,metasenv) -> [resolve_id,term,metasenv]
- | Ko | Uncertain -> [])
- | id::idtl,uris::uristl ->
- let rec filter =
- function
- [] -> []
- | (uri : CicTextualParser0.interpretation_codomain_item)::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
- (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
- in
- 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 ->
- (match id with
- CicTextualParser0.Id id -> id
- | CicTextualParser0.Symbol (descr,_) -> descr
- ),
- match resolve id with
- None -> assert false
- | 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
- let index = C.interactive_interpretation_choice choices in
- List.nth resolve_ids index
- in
- (known_ids @ dom', resolve_id'), metasenv',term
-end
-;;
projects / helm.git / blobdiff