From: Ferruccio Guidi Date: Tue, 9 Dec 2003 10:27:25 +0000 (+0000) Subject: while construction inserted X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a32bcc14672dae13e8bb725e54c819958dfdb677 while construction inserted --- diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend index 8acbe7bca..ff5132bcc 100644 --- a/helm/ocaml/mathql/.depend +++ b/helm/ocaml/mathql/.depend @@ -1,4 +1,2 @@ -mQueryMisc.cmo: mQueryMisc.cmi -mQueryMisc.cmx: mQueryMisc.cmi mQueryUtil.cmo: mQueryUtil.cmi mQueryUtil.cmx: mQueryUtil.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index f3030e882..a6a165f0a 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -1,10 +1,11 @@ PACKAGE = mathql -REQUIRES = helm-cic helm-cic_textual_parser +REQUIRES = + PREDICATES = -INTERFACE_FILES = mQueryMisc.mli mQueryUtil.mli +INTERFACE_FILES = mQueryUtil.mli -IMPLEMENTATION_FILES = mQueryMisc.ml mathQL.ml mQueryUtil.ml +IMPLEMENTATION_FILES = mathQL.ml mQueryUtil.ml EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml deleted file mode 100644 index fb32d8c24..000000000 --- a/helm/ocaml/mathql/mQueryMisc.ml +++ /dev/null @@ -1,120 +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 *) -(* Ferruccio Guidi *) -(* 15/01/2003 *) -(* *) -(* *) -(****************************************************************************) - -exception IllFormedUri of string;; - -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) -;; - -let cic_textual_parser_uri_of_string uri' = - try - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then - CicTextualParser0.ConUri (UriManager.uri_of_string uri') - else - if String.sub uri' (String.length uri' - 4) 4 = ".var" then - CicTextualParser0.VarUri (UriManager.uri_of_string uri') - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in - CicTextualParser0.IndTyUri (uri'',typeno) - with - UriManager.IllFormedUri _ - | CicTextualParser0.LexerFailure _ - | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in - CicTextualParser0.IndConUri (uri'',typeno,consno) - ) - with - UriManager.IllFormedUri _ - | CicTextualParser0.LexerFailure _ - | Invalid_argument _ -> - raise (IllFormedUri uri') -;; - -(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) -let wrong_xpointer_format_from_wrong_xpointer_format' uri = - try - let index_sharp = String.index uri '#' in - let index_rest = index_sharp + 10 in - let baseuri = String.sub uri 0 index_sharp in - let rest = - String.sub uri index_rest (String.length uri - index_rest - 1) - in - baseuri ^ "#" ^ rest - with Not_found -> uri -;; - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -(* conversion functions *****************************************************) - -type uriref = UriManager.uri * (int list) - -let string_of_uriref (uri, fi) = - let module UM = UriManager in - let str = UM.string_of_uri uri in - let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in - match fi with - | [] -> str - | [t] -> str ^ xp t ^ ")" - | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" diff --git a/helm/ocaml/mathql/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli deleted file mode 100644 index 6fb600dab..000000000 --- a/helm/ocaml/mathql/mQueryMisc.mli +++ /dev/null @@ -1,46 +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 *) -(* Ferruccio Guidi *) -(* 15/01/2003 *) -(* *) -(* *) -(****************************************************************************) - -exception IllFormedUri of string - -val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string -val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri -val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term -val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string - -type uriref = UriManager.uri * (int list) - -val string_of_uriref : uriref -> string diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 22d1f91e5..1051e2a7e 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -77,3 +77,29 @@ let rec add_assoc ap = function | [] -> [ap] | head :: tail when fst head = fst ap -> ap :: tail | head :: tail -> head :: add_assoc ap tail + +(* int of string ************************************************************) + +type t = End + | Space + | Figure of int + | Error + +let int_of_string s = + let l = String.length s in + let get_t i = + if i = l then End else + match s.[i] with + | ' ' | '\t' | '\r' | 'n' -> Space + | '0' .. '9' -> Figure (Char.code s.[i] - Char.code '0') + | _ -> Error + in + let rec aux i xv = match get_t i, xv with + | Error, _ + | End, None -> raise (Failure "int_of_string") + | End, Some v -> v + | Space, xv -> aux (succ i) xv + | Figure f, None -> aux (succ i) (Some f) + | Figure f, Some v -> aux (succ i) (Some (10 * v + f)) + in + aux 0 None diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli index fbfb3f793..635fb660f 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -43,3 +43,5 @@ val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list val flat_list : ('a -> unit) -> ('b -> unit) -> 'a -> 'b list -> unit val add_assoc : 'a * 'b -> ('a * 'b) list -> ('a * 'b) list + +val int_of_string : string -> int diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 884976fe5..8ba562ab2 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -80,11 +80,12 @@ type query = Const of result | Dot of avar * path | Ex of avar list * query | Select of avar * query * query - | Let of svar * query * query + | Let of svar option * query * query | Fun of path * path list * query list | Gen of path * query list | Add of bool * groups * query | For of gen * avar * query * query + | While of gen * query * query | Property of inverse * refine * path * main * istrue * isfalse list * exp_list * pattern * query