]> matita.cs.unibo.it Git - helm.git/commitdiff
moved disambiguate module away
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 22 Jan 2004 16:19:22 +0000 (16:19 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 22 Jan 2004 16:19:22 +0000 (16:19 +0000)
helm/gTopLevel/disambiguate.ml [deleted file]
helm/gTopLevel/disambiguate.mli [deleted file]

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
deleted file mode 100644 (file)
index 07a0368..0000000
+++ /dev/null
@@ -1,288 +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 <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
-    (* 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 : ?append_NL:bool -> Ui_logger.html_msg -> unit
-    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
-    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 (`Msg (`T "Locate query:"));
-     MQueryUtil.text_of_query
-      (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
-      "" query; 
-     C.output_html (`Msg (`T "Result:"));
-     MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" 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:`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
-       C.output_html (`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 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
-;;
diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli
deleted file mode 100644 (file)
index 79e77df..0000000
+++ /dev/null
@@ -1,73 +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 <sacerdot@cs.unibo.it>               *)
-(*                                 15/01/2003                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-(** 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 : ?append_NL:bool -> Ui_logger.html_msg -> unit
-    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
-    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) :
-    sig
-      exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
-      val disambiguate_input :
-        MQIConn.handle -> 
-        Cic.context ->
-        Cic.metasenv ->
-        CicTextualParser0.interpretation_domain_item list ->
-        (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) ->
-        id_to_uris:domain_and_interpretation ->
-        domain_and_interpretation * Cic.metasenv * Cic.term
-    end