X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateTypes.ml;h=b323f9231972b9dcda2368d2807af5e56f651738;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=522a08dc0adf4140ae77f6a5826f0bcb1df34b87;hpb=8004125685a99b6c0f2f95fd7f3fa09a4f5c9094;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 522a08dc0..b323f9231 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -1,8 +1,42 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +type term = CicNotationPt.term +type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic +type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical +type script_entry = + | Command of tactical + | Comment of CicNotationPt.location * string +type script = CicNotationPt.location * script_entry list type domain_item = - | Id of string (* literal *) - | Symbol of string * int (* literal, instance num *) - | Num of int (* instance num *) + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +exception Invalid_choice of string Lazy.t module OrderedDomain = struct @@ -10,8 +44,32 @@ module OrderedDomain = let compare = Pervasives.compare end -module Domain = Set.Make (OrderedDomain) -module Environment = Map.Make (OrderedDomain) +(* module Domain = Set.Make (OrderedDomain) *) +module Environment = +struct + module Environment' = Map.Make (OrderedDomain) + + include Environment' + + let cons k v env = + try + let current = find k env in + let dsc, _ = v in + add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env + with Not_found -> + add k [v] env + + let hd list_env = + try + map List.hd list_env + with Failure _ -> assert false + + let fold_flatten f env base = + fold + (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc) + env base + +end type codomain_item = string * (* description *) @@ -20,17 +78,32 @@ type codomain_item = and environment = codomain_item Environment.t +type multiple_environment = codomain_item list Environment.t + + +(** adds a (name,uri) list l to a disambiguation environment e **) +let multiple_env_of_list l e = + List.fold_left + (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e) + e l + +let env_of_list l e = + List.fold_left + (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) + e l + module type Callbacks = sig - val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit - val interactive_user_uri_choice : + 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 + title:string -> msg:string -> id:string -> UriManager.uri list -> + UriManager.uri list + val interactive_interpretation_choice: + (string * string) list list -> int list + val input_or_locate_uri: + title:string -> ?id:string -> unit -> UriManager.uri end let string_of_domain_item = function @@ -39,53 +112,15 @@ let string_of_domain_item = function | Num i -> Printf.sprintf "NUM(instance %d)" i let string_of_domain dom = - let buf = Buffer.create 1024 in - Domain.iter - (fun item -> Buffer.add_string buf (string_of_domain_item item ^ "; ")) - dom; - Buffer.contents buf + String.concat "; " (List.map string_of_domain_item dom) -module EnvironmentP3 = - struct - type t = environment - let empty = "" - - let to_string env = - Environment.fold - (fun i v s -> - match i with - | Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v) - | _ -> "") - env "" - - 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 = Id (Str.matched_group 2 inputtext) in - let uri = "cic:" ^ (Str.matched_group 5 inputtext) in - let resolve_id = aux (n' + 1) in - if Environment.mem id resolve_id then - resolve_id - else - let term = - HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) - in - (Environment.add id (uri, (fun _ _ _ -> term)) - resolve_id) - with - Not_found -> Environment.empty - in - aux 0 - end +let floc_of_loc (loc_begin, loc_end) = + let floc_begin = + { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; + Lexing.pos_cnum = loc_begin } + in + let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in + (floc_begin, floc_end) + +let dummy_floc = floc_of_loc (-1, -1)