From: Ferruccio Guidi Date: Fri, 20 Jun 2003 15:23:55 +0000 (+0000) Subject: Author specification added in head comments; X-Git-Tag: V7_3_new_exportation_merged~5 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=931f10c61b4e3914474955a94a05cf43b5fa2bc0;p=helm.git Author specification added in head comments; MQueryGenerator.builtin ready to be used --- diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll index b5366af89..abccb4626 100644 --- a/helm/ocaml/mathql/mQueryTLexer.mll +++ b/helm/ocaml/mathql/mQueryTLexer.mll @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -(* +(* AUTOR: Ferruccio Guidi *) { diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 707b7dd6c..313636c80 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. */ -/* +/* AUTOR: Ferruccio Guidi */ %{ diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 2de817932..e4a29ffcf 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -23,8 +23,8 @@ * http://cs.unibo.it/helm/. *) -(* - *) +(* AUTOR: Ferruccio Guidi + *) (* text linearization and parsing *******************************************) diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli index 53d612e82..69aaebd77 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -23,16 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - +(* AUTOR: Ferruccio Guidi + *) val text_of_query : (string -> unit) -> MathQL.query -> string -> unit diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 191090c4f..7e82fe547 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -23,8 +23,8 @@ * http://www.cs.unibo.it/helm/. *) -(* - *) +(* AUTOR: Ferruccio Guidi + *) (* output data structures ***************************************************) diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 24720d0aa..2d529c9e8 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + type uri = string type position = string type depth = string @@ -36,6 +39,15 @@ type spec = MustObj of uri list * position list * depth list | OnlyRel of position list * depth list | Universe of position list +type builtin_t = MainHypothesis + | InHypothesis + | MainConclusion + | InConclusion + | InBody + | Set + | Prop + | Type + let text_of_builtin s = let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in if s = ns ^ "MainHypothesis" then "$MH" else @@ -43,9 +55,9 @@ let text_of_builtin s = if s = ns ^ "MainConclusion" then "$MC" else if s = ns ^ "InConclusion" then "$IC" else if s = ns ^ "InBody" then "$IB" else - if s = ns ^ "Set" then "$SET" else - if s = ns ^ "Prop" then "$PROP" else - if s = ns ^ "Type" then "$TYPE" else s + if s = "Set" then "$SET" else + if s = "Prop" then "$PROP" else + if s = "Type" then "$TYPE" else s let text_of_spec out l = let rec iter = function @@ -164,15 +176,14 @@ let compose cl = let builtin s = let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in match s with - | "MH" -> ns ^ "MainHypothesis" - | "IH" -> ns ^ "InHypothesis" - | "MC" -> ns ^ "MainConclusion" - | "IC" -> ns ^ "InConclusion" - | "IB" -> ns ^ "InBody" - | "SET" -> ns ^ "Set" - | "PROP" -> ns ^ "Prop" - | "TYPE" -> ns ^ "Type" - | _ -> raise (Failure "MQueryGenerator.builtin") + | MainHypothesis -> ns ^ "MainHypothesis" + | InHypothesis -> ns ^ "InHypothesis" + | MainConclusion -> ns ^ "MainConclusion" + | InConclusion -> ns ^ "InConclusion" + | InBody -> ns ^ "InBody" + | Set -> "Set" + | Prop -> "Prop" + | Type -> "Type" (* conversion functions from the old constraints ***************************) diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli index 9229290e8..6081cd028 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.mli +++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + type uri = string type position = string type depth = string @@ -36,11 +39,20 @@ type spec = MustObj of uri list * position list * depth list | OnlyRel of position list * depth list | Universe of position list +type builtin_t = MainHypothesis + | InHypothesis + | MainConclusion + | InConclusion + | InBody + | Set + | Prop + | Type + val locate : string -> MathQL.query val compose : spec list -> MathQL.query -val builtin : MathQL.vvar -> string +val builtin : builtin_t -> string (* interface for the old constraints ***************************************) diff --git a/helm/ocaml/mathql_generator/mQueryLevels.ml b/helm/ocaml/mathql_generator/mQueryLevels.ml index 977638dba..d10f5d659 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels.ml +++ b/helm/ocaml/mathql_generator/mQueryLevels.ml @@ -23,15 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) +(* AUTOR: Ferruccio Guidi + *) let levels_of_term metasenv context term = let module TC = CicTypeChecker in diff --git a/helm/ocaml/mathql_generator/mQueryLevels.mli b/helm/ocaml/mathql_generator/mQueryLevels.mli index 5b214b733..c16d12bc1 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels.mli +++ b/helm/ocaml/mathql_generator/mQueryLevels.mli @@ -23,14 +23,7 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) +(* AUTOR: Ferruccio Guidi + *) val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list) diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.mli b/helm/ocaml/mathql_generator/mQueryLevels2.mli index 805f1064d..f62818363 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels2.mli +++ b/helm/ocaml/mathql_generator/mQueryLevels2.mli @@ -27,9 +27,10 @@ (* *) (* PROJECT HELM *) (* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) +(* Claudio Sacerdoti Coen *) +(* 02/12/2002 *) (* *) +(* Missing description *) (* *) (******************************************************************************) diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index 1de6663e4..a51242bef 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + type flag = Postgres | Galax | Stat | Quiet | Warn | Log type handle = {log : string -> unit; (* logging function *) diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli index 7eff1b4b4..405e405d1 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ b/helm/ocaml/mathql_interpreter/mQIConn.mli @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + type flag = Postgres | Galax | Stat | Quiet | Warn | Log val string_of_flags : flag list -> string diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml index b19a51c83..7c4abcbf6 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.ml +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + let default_connection_string = "dbname=mowgli user=helm" diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.mli b/helm/ocaml/mathql_interpreter/mQIPostgres.mli index d6b9d3f33..8acd2a2fd 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.mli +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.mli @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + val init : unit -> Postgres.connection option val close : Postgres.connection option -> unit diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index b07fdd551..7550bcc9c 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -1,4 +1,3 @@ - (* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic @@ -24,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + module M = MathQL module P = MQIPostgres module C = MQIConn diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.mli b/helm/ocaml/mathql_interpreter/mQIProperty.mli index 7c2bc95f8..1084cc94a 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.mli +++ b/helm/ocaml/mathql_interpreter/mQIProperty.mli @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + open MathQL open MQIConn diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml index 4d74ef120..fef3252ac 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml @@ -23,16 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 06/01/2003 *) -(* *) -(* *) -(******************************************************************************) - +(* AUTOR: Ferruccio Guidi + *) (* boolean constants *******************************************************) diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli index 217ba8c01..c294832c8 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.mli +++ b/helm/ocaml/mathql_interpreter/mQIUtil.mli @@ -23,16 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 06/01/2003 *) -(* *) -(* *) -(******************************************************************************) - +(* AUTOR: Ferruccio Guidi + *) val mql_true : MathQL.value diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index 5816a99bc..58fb7b87e 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + (* contexts *****************************************************************) type svar_context = (MathQL.svar * MathQL.resource_set) list diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli b/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli index 481c5c315..9d7081fff 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli @@ -23,4 +23,7 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + val execute : MQIConn.handle -> MathQL.query -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.ml b/helm/ocaml/mathql_interpreter/mQueryMisc.ml index aa842b4b3..cb6f92a21 100644 --- a/helm/ocaml/mathql_interpreter/mQueryMisc.ml +++ b/helm/ocaml/mathql_interpreter/mQueryMisc.ml @@ -23,6 +23,16 @@ * http://cs.unibo.it/helm/. *) +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 15/01/2003 *) +(* *) +(* *) +(******************************************************************************) + exception IllFormedUri of string;; let string_of_cic_textual_parser_uri uri = diff --git a/helm/ocaml/mathql_test/mQGTopLexer.mll b/helm/ocaml/mathql_test/mQGTopLexer.mll index da6971028..7e69bccf6 100644 --- a/helm/ocaml/mathql_test/mQGTopLexer.mll +++ b/helm/ocaml/mathql_test/mQGTopLexer.mll @@ -23,15 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 23/05/2002 *) -(* *) -(* *) -(******************************************************************************) +(* AUTOR: Ferruccio Guidi + *) { open MQGTopParser diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly index e36dd5435..cf2280dad 100644 --- a/helm/ocaml/mathql_test/mQGTopParser.mly +++ b/helm/ocaml/mathql_test/mQGTopParser.mly @@ -30,7 +30,20 @@ let f (x, y, z) = x let s (x, y, z) = y let t (x, y, z) = z - + + let builtin s = + let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in + match s with + | "MH" -> ns ^ "MainHypothesis" + | "IH" -> ns ^ "InHypothesis" + | "MC" -> ns ^ "MainConclusion" + | "IC" -> ns ^ "InConclusion" + | "IB" -> ns ^ "InBody" + | "SET" -> "Set" + | "PROP" -> "Prop" + | "TYPE" -> "Type" + | _ -> raise Parsing.Parse_error + module G = MQueryGenerator %} %token ID @@ -75,8 +88,8 @@ | STR qstr { $1 ^ $2 } ; str: - | STR { $1 } - | DL ID { try G.builtin $2 with _ -> "" } + | STR { $1 } + | DL ID { builtin $2 } ; strs: | str CM strs { $1 :: $3 } diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml index 9e1dcde0d..0ef1ca981 100644 --- a/helm/ocaml/mathql_test/mqgtop.ml +++ b/helm/ocaml/mathql_test/mqgtop.ml @@ -157,8 +157,8 @@ let locate name = let mpattern n m l = let queries = ref [] in - let univ = Some [G.builtin "MH"; G.builtin "IH"; - G.builtin "MC"; G.builtin "IC"] in + let univ = Some [G.builtin G.MainHypothesis; G.builtin G.InHypothesis; + G.builtin G.MainConclusion; G.builtin G.InConclusion] in let handle = get_handle () in let rec pattern level = function | [] -> () @@ -194,10 +194,11 @@ let mpattern n m l = let mbackward n m l = let queries = ref [] in let torigth_restriction (u, b) = - let p = if b then G.builtin "MC" else G.builtin "IC" in + let p = if b then G.builtin G.MainConclusion + else G.builtin G.InConclusion in (u, p, None) in - let univ = Some [G.builtin "MC"; G.builtin "IC"] in + let univ = Some [G.builtin G.MainConclusion; G.builtin G.InConclusion] in let handle = get_handle () in let rec backward level = function | [] -> ()