+++ /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 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-open Printf
-
-(** This module provides a functor to disambiguate the input **)
-(** given a set of user-interface call-backs **)
-
-module type Callbacks =
- sig
- val interactive_user_uri_choice :
- selection_mode:[`SINGLE | `MULTIPLE] ->
- ?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 list
- val input_or_locate_uri : title:string -> ?id:string -> unit -> 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
- HelmLogger.log (`Msg (`T "Locate query:"));
- MQueryUtil.text_of_query
- (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
- "" query;
- HelmLogger.log (`Msg (`T "Result:"));
- MQueryUtil.text_of_result (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
- let uris' =
- match uris with
- [] ->
- [UriManager.string_of_uri
- (C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
- | [uri] -> [uri]
- | _ ->
- C.interactive_user_uri_choice
- ~selection_mode:`MULTIPLE
- ~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
- HelmLogger.log (`Msg (`T (sprintf
- "Disambiguation phase started: up to %d cases will be tried"
- tests_no)));
- (* 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 metasenv',expr = mk_metasenv_and_expr resolve_id' in
-(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
- try
- let term,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
- in
- Ok (term,metasenv'')
- with
- CicRefine.Uncertain _ ->
-prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
- Uncertain
- | CicRefine.RefineFailure _ ->
-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
- (Printf.sprintf
- "+++++ ASSERTION FAILED: a refine operation should not modify the metasenv. Old metasenv:\n %s\n New metasenv:\n %s\n"
- (CicMetaSubst.ppmetasenv metasenv [])
- (CicMetaSubst.ppmetasenv newmetasenv [])) ;
- (* an assert would raise an exception that could be caught *)
- exit 1
- end
- ) resolve_ids ;
- let res =
- match resolve_ids with
- [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
- | [_] -> resolve_ids
- | _ ->
- 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 indexes = C.interactive_interpretation_choice choices in
- List.map (List.nth resolve_ids) indexes
- in
- List.map
- (fun (resolve_id',term,metasenv') ->
- (known_ids @ dom', resolve_id'), metasenv',term
- ) res
-end
-;;
-
-module EnvironmentP3 =
- struct
- type t = domain_and_interpretation
-
- let empty = ""
-
- let to_string (dom,resolve_id) =
- let string_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
- let uri' =
- match uri with
- CTP.ConUri uri -> UriManager.string_of_uri uri
- | CTP.VarUri uri -> UriManager.string_of_uri uri
- | CTP.IndTyUri (uri,tyno) ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
- | CTP.IndConUri (uri,tyno,consno) ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
- string_of_int consno
- in
- (* 4 = String.length "cic:" *)
- String.sub uri' 4 (String.length uri' - 4)
- in
- String.concat "\n"
- (List.map
- (function v ->
- let uri =
- match resolve_id v with
- None -> assert false
- | Some (CicTextualParser0.Uri uri) -> uri
- | Some (CicTextualParser0.Term _)
- | Some CicTextualParser0.Implicit -> assert false
- in
- "alias " ^
- (match v with
- CicTextualParser0.Id id -> id
- | CicTextualParser0.Symbol (descr,_) ->
- (* CSC: To be implemented *)
- assert false
- )^ " " ^ (string_of_cic_textual_parser_uri uri)
- ) dom)
-
- let of_string inputtext =
- let regexpr =
- let alfa = "[a-zA-Z_-]" in
- let digit = "[0-9]" in
- let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
- let blanks = "\( \|\t\|\n\)+" in
- let nonblanks = "[^ \t\n]+" in
- let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
- Str.regexp
- ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
- in
- let rec aux n =
- try
- let n' = Str.search_forward regexpr inputtext n in
- let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
- let uri =
- MQueryMisc.cic_textual_parser_uri_of_string
- ("cic:" ^ (Str.matched_group 5 inputtext))
- in
- let dom,resolve_id = aux (n' + 1) in
- if List.mem id dom then
- dom,resolve_id
- else
- id::dom,
- (function id' ->
- if id = id' then
- Some (CicTextualParser0.Uri uri)
- else resolve_id id')
- with
- Not_found -> ([],function _ -> None)
- in
- aux 0
- end
projects / helm.git / blobdiff