X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2Fdisambiguate.ml;fp=helm%2FgTopLevel%2Fdisambiguate.ml;h=0000000000000000000000000000000000000000;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hp=ce41208dd3ba2833f68b105376f56166a6300ae0;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml deleted file mode 100644 index ce41208dd..000000000 --- a/helm/gTopLevel/disambiguate.ml +++ /dev/null @@ -1,284 +0,0 @@ -(* 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 *) -(* 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 "

Locate Query: 

";
-     MQueryUtil.text_of_query C.output_html query ""; 
-     C.output_html "
Result:
";
-     MQueryUtil.text_of_result C.output_html result "
";
-     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
-        ("
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
-;;