From efdc3184ccd0738fe48aa0056fc444fba23329e8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 9 Dec 2003 10:30:03 +0000 Subject: [PATCH] update --- helm/ocaml/mathql_generator/.depend | 10 +- helm/ocaml/mathql_generator/Makefile | 5 +- .../ocaml/mathql_generator/cGSearchPattern.ml | 7 +- helm/ocaml/mathql_generator/mQGTypes.ml | 1 + helm/ocaml/mathql_generator/mQGUtil.ml | 28 +-- .../ocaml/mathql_generator/mQueryGenerator.ml | 2 +- helm/ocaml/mathql_generator/mQueryMisc.ml | 164 ++++++++++++++++++ helm/ocaml/mathql_generator/mQueryMisc.mli | 56 ++++++ 8 files changed, 251 insertions(+), 22 deletions(-) create mode 100644 helm/ocaml/mathql_generator/mQueryMisc.ml create mode 100644 helm/ocaml/mathql_generator/mQueryMisc.mli diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend index 820add841..0619b2c03 100644 --- a/helm/ocaml/mathql_generator/.depend +++ b/helm/ocaml/mathql_generator/.depend @@ -7,9 +7,11 @@ mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi mQueryGenerator.cmo: mQGTypes.cmo mQGUtil.cmi mQueryGenerator.cmi mQueryGenerator.cmx: mQGTypes.cmx mQGUtil.cmx mQueryGenerator.cmi -cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi -cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi +mQueryMisc.cmo: mQueryMisc.cmi +mQueryMisc.cmx: mQueryMisc.cmi +cGMatchConclusion.cmo: mQGTypes.cmo mQueryMisc.cmi cGMatchConclusion.cmi +cGMatchConclusion.cmx: mQGTypes.cmx mQueryMisc.cmx cGMatchConclusion.cmi cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi -cGLocateInductive.cmo: mQGTypes.cmo cGLocateInductive.cmi -cGLocateInductive.cmx: mQGTypes.cmx cGLocateInductive.cmi +cGLocateInductive.cmo: mQGTypes.cmo mQueryMisc.cmi cGLocateInductive.cmi +cGLocateInductive.cmx: mQGTypes.cmx mQueryMisc.cmx cGLocateInductive.cmi diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index a72f17ab2..529b3a88b 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -1,10 +1,11 @@ PACKAGE = mathql_generator -REQUIRES = helm-cic helm-cic_proof_checking helm-mathql +REQUIRES = helm-cic helm-cic_textual_parser helm-cic_proof_checking \ + helm-mathql helm-mathql_interpreter PREDICATES = -INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ +INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli mQueryMisc.mli \ cGMatchConclusion.mli cGSearchPattern.mli \ cGLocateInductive.mli diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index 77f3b488c..65c955cca 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -93,9 +93,10 @@ let get_constraints term = | Branch _ -> let s' = match s with - Cic.Prop -> T.Prop - | Cic.Set -> T.Set - | Cic.Type -> T.Type + Cic.Prop -> T.Prop + | Cic.Set -> T.Set + | Cic.CProp -> T.CProp + | Cic.Type -> T.Type in [],[],[!!kind,s'] | _ -> [],[],[]) diff --git a/helm/ocaml/mathql_generator/mQGTypes.ml b/helm/ocaml/mathql_generator/mQGTypes.ml index 2dacfe14c..79c102250 100644 --- a/helm/ocaml/mathql_generator/mQGTypes.ml +++ b/helm/ocaml/mathql_generator/mQGTypes.ml @@ -39,6 +39,7 @@ type depth = int type sort = Set | Prop | Type + | CProp type spec = MustObj of uri list * position list * depth list | MustSort of sort list * position list * depth list diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml index 36dd0653c..b9ff4bb15 100644 --- a/helm/ocaml/mathql_generator/mQGUtil.ml +++ b/helm/ocaml/mathql_generator/mQGUtil.ml @@ -40,9 +40,10 @@ let string_of_position p = | T.InBody -> ns ^ "InBody" let string_of_sort = function - | T.Set -> "Set" - | T.Prop -> "Prop" - | T.Type -> "Type" + | T.Set -> "Set" + | T.Prop -> "Prop" + | T.Type -> "Type" + | T.CProp -> "CProp" let string_of_depth = string_of_int @@ -54,9 +55,10 @@ let mathql_of_position = function | T.InBody -> "$IB" let mathql_of_sort = function - | T.Set -> "$SET" - | T.Prop -> "$PROP" - | T.Type -> "$TYPE" + | T.Set -> "$SET" + | T.Prop -> "$PROP" + | T.Type -> "$TYPE" + | T.CProp -> "$CPROP" let mathql_of_depth = string_of_int @@ -92,9 +94,10 @@ let position_of_mathql = function | _ -> raise Parsing.Parse_error let sort_of_mathql = function - | "$SET" -> T.Set - | "$PROP" -> T.Prop - | "$TYPE" -> T.Type + | "$SET" -> T.Set + | "$PROP" -> T.Prop + | "$TYPE" -> T.Type + | "$CPROP" -> T.CProp | _ -> raise Parsing.Parse_error let depth_of_mathql s = @@ -120,9 +123,10 @@ let text_of_depth pos no_depth_text = match pos with | _ -> no_depth_text let text_of_sort = function - | T.Set -> "Set" - | T.Prop -> "Prop" - | T.Type -> "Type" + | T.Set -> "Set" + | T.Prop -> "Prop" + | T.Type -> "Type" + | T.CProp -> "CProp" let is_main_position = function | `MainHypothesis _ diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 811546956..e56a744cd 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -149,7 +149,7 @@ let compose cl = let letin_query = if ! letin = [] then fun x -> x else - let f (vvar, msval) x = M.Let (vvar, msval, x) in + let f (vvar, msval) x = M.Let (Some vvar, msval, x) in iter f (fun x y z -> x (y z)) ! letin in stat (letin_query (select_query must_query)) diff --git a/helm/ocaml/mathql_generator/mQueryMisc.ml b/helm/ocaml/mathql_generator/mQueryMisc.ml new file mode 100644 index 000000000..044b1cfe7 --- /dev/null +++ b/helm/ocaml/mathql_generator/mQueryMisc.ml @@ -0,0 +1,164 @@ +(* 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 ^ ")" + +let uriref_of_string str = + try + let i0 = String.index str '#' in + let u = UriManager.uri_of_string (String.sub str 0 i0) in + let i2 = pred (String.length str) in + let i0 = i0 + 12 in + try + let i1 = String.index_from str i0 '/' in + u, [pred (int_of_string (String.sub str i0 (i1 - i0))); + int_of_string (String.sub str (succ i1) (i2 - succ i1))] + with Not_found -> + u, [pred (int_of_string (String.sub str i0 (i2 - i0)))] + with Not_found -> UriManager.uri_of_string str, [] + +(* object inspection ********************************************************) + +exception CurrentProof + +exception InductiveDefinition + +exception IllFormedFragment + +let get_object (u, fi) = + let nth l i = + try List.nth l i with Failure "nth" -> raise IllFormedFragment + in + match (CicEnvironment.get_obj u) with + | Cic.Constant (_, Some t, ty, _) -> t, ty + | Cic.Constant (_, None, ty, _) -> Cic.Const (u, []), ty + | Cic.Variable (_, Some t, ty, _) -> t, ty + | Cic.Variable (_, None, ty, _) -> Cic.Var (u, []), ty + | Cic.CurrentProof (_, me, t, ty, _) -> raise CurrentProof + | Cic.InductiveDefinition (tl, _, _) -> + match fi with + | [] -> raise InductiveDefinition + | [i] -> + let _, _, ty, _ = nth tl i in + Cic.MutInd (u, i, []), ty + | [i; j] -> + let _, _, _, cl = nth tl i in + let _, ty = nth cl (pred j) in + Cic.MutConstruct (u, i, j, []), ty + | _ -> raise IllFormedFragment diff --git a/helm/ocaml/mathql_generator/mQueryMisc.mli b/helm/ocaml/mathql_generator/mQueryMisc.mli new file mode 100644 index 000000000..e225ded9c --- /dev/null +++ b/helm/ocaml/mathql_generator/mQueryMisc.mli @@ -0,0 +1,56 @@ +(* 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 + +val uriref_of_string : string -> uriref + +exception CurrentProof + +exception InductiveDefinition + +exception IllFormedFragment + +val get_object : uriref -> Cic.term * Cic.term -- 2.39.2