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 b5366af898dee5b67296527806844ece09eeeef7..abccb46264d2053927ded64beec8bb60169eefd5 100644 (file)
--- a/helm/ocaml/mathql/mQueryTLexer.mll
+++ b/helm/ocaml/mathql/mQueryTLexer.mll
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
 { 

diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly
index 707b7dd6c22a54e43b169d3c9a07a058aca13918..313636c80d13327489bf4c8ade0da24f500496ef 100644 (file)
--- a/helm/ocaml/mathql/mQueryTParser.mly
+++ b/helm/ocaml/mathql/mQueryTParser.mly
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  */
 
-/*
+/*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  */ 
 
 %{

diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml
index 2de8179327db4825a7cb6636122f0c41f23748f4..e4a29ffcfaa2c1392611e92de950c2ebd99c2ef1 100644 (file)
--- a/helm/ocaml/mathql/mQueryUtil.ml
+++ b/helm/ocaml/mathql/mQueryUtil.ml
@@ -23,8 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*
- *) 
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 (* text linearization and parsing *******************************************)
 

diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli
index 53d612e822ae60fd0fb5ba7aa6983dcd9657ee6d..69aaebd774cce29633faafb4e52f966288d35569 100644 (file)
--- 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 <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 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 191090c4f2a89d4645f8771876b9831dda4ff603..7e82fe5474a1919e49bfa08e25fa00c45dda5b69 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
 
 (* output data structures ***************************************************)
 

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index 24720d0aab4c9a4051168f7cd6218147a393ed90..2d529c9e8aa32f9f23659bebafcc418706bc5378 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 9229290e86511633095facbd8fb1f65979c096f1..6081cd02802819a92a06ca3520ff5a156717adeb 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 977638dba90adbb4d3dbd4008a5d25cc60b5f92a..d10f5d659bf69b6ce2902455abba4ce090806482 100644 (file)
--- 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 <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 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 5b214b73364741d3dace7e1750cd612736d89e15..c16d12bc14878fcda89d456352f61b0e4c8a929f 100644 (file)
--- 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 <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 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 805f1064da2517efbe5a5a962f1ef7cf2844f614..f628183632cdc536ffc69c2c0bcf6e081d9d77b0 100644 (file)
--- a/helm/ocaml/mathql_generator/mQueryLevels2.mli
+++ b/helm/ocaml/mathql_generator/mQueryLevels2.mli
@@ -27,9 +27,10 @@
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
 (*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 02/12/2002                                 *)
 (*                                                                            *)
+(*                            Missing description                             *)
 (*                                                                            *)
 (******************************************************************************)
 

diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml
index 1de6663e4a36369deaf5737d2e4b22eabca276bc..a51242bef323373ca38be15b6efdda5c4d0d338b 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 7eff1b4b45fef8a558cd6e8e941d73a6d1f8af53..405e405d15041d649230c40326d3d6593def9049 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 b19a51c83bbb0ccfde390b50ae485df1e8a3a0ed..7c4abcbf62b5beb1496c28b91afbda11b1275e14 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 d6b9d3f33f6eab69bfa54eeeda8d2bde2437bd4e..8acd2a2fd97d039710e31f27dafbaaaeb63c7081 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 b07fdd5519343f4a68a270714ccfdfd4ab20e187..7550bcc9c025fc97335a0df518a1fd9b5a173e93 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 7c2bc95f8e5bd9f4e94d4bc45c4e410a99aadabe..1084cc94aaddb1665275ec20465c479534590981 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 open MathQL
 open MQIConn
 

diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml
index 4d74ef1202973a3f871a9f28852f86b0ba9add89..fef3252ac2635188aca39b04ca76669a9689eb1c 100644 (file)
--- 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 <fguidi@cs.unibo.it>                   *)
-(*                                 06/01/2003                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 (* boolean constants  *******************************************************)
 

diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli
index 217ba8c01ed3171010886215932c3e450e0ff958..c294832c8e02b1b0a050ccc02b99612d2e150c09 100644 (file)
--- 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 <fguidi@cs.unibo.it>                   *)
-(*                                 06/01/2003                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 val mql_true      : MathQL.value
 

diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
index 5816a99bc10ae7def653c5558e1faa7a8b9d5f9c..58fb7b87e734545491f893046333a50a85265bf0 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 (* 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 481c5c31542fc29c01ad24e4a6dca9cb6a6a258c..9d7081fffedf8b3fcfc6a6c905eb63091ff2eb86 100644 (file)
--- 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 <fguidi@cs.unibo.it>
+ *)
+
 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 aa842b4b3a031f57283c8d96c792b1138664dd06..cb6f92a219bdb78a0e00dc4396617e12659fd85a 100644 (file)
--- 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 <sacerdot@cs.unibo.it>               *)
+(*                                 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 da69710285e34f38ec601446d2ee7ef1760e2bab..7e69bccf6874f74de08b06dd1444c69668bf32cd 100644 (file)
--- 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 <fguidi@cs.unibo.it>                   *)
-(*                                 23/05/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 { 
    open MQGTopParser

diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly
index e36dd5435c6b4c1e3adba2b6c83dedb1afff2e6a..cf2280dadd8f827ddf98a140f44f639c98d5032b 100644 (file)
--- 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 <string> 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 9e1dcde0d99dba624ffc4225169dc9ca33d55915..0ef1ca981f4f86377d3aac9141b5d773e18a8def 100644 (file)
--- 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
       | []           -> ()