From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 3 Jul 2003 14:14:49 +0000 (+0000)
Subject: "backPointer" metadata enabled
X-Git-Tag: camera_ready~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=898d547264b7d445f6b4e67dbbda26acf7466150

"backPointer" metadata enabled
---

diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml
index 7550bcc9c..026e11b48 100644
--- a/helm/ocaml/mathql_interpreter/mQIProperty.ml
+++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml
@@ -140,7 +140,14 @@ let rec decolon s =
       String.sub s 0 i ^ "_" ^ decolon (String.sub s (succ i) (l - succ i))
    with Not_found -> s
 
-let conv = function
+let conv_bp = function
+   | []                  -> "h_occurrence" 
+   | [t]                 -> ""
+   | [_; "h:occurrence"] -> "source"
+   | [_; t]              -> decolon t
+   | _                   -> not_supported "conv_bp"
+
+let conv_gen = function
    | []             -> "source"
    | ["objectName"] -> "value" 
    | [t]            -> ""
@@ -149,6 +156,9 @@ let conv = function
 
 let exec_single h mc ct cfl el t =
    let table = match t with Some t -> decolon t | None -> "objectName" in
+   let table, conv = 
+      if table = "backPointer" then "refObj", conv_bp else table, conv_gen
+   in
    let first = conv mc in
    let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in
    let cons_true = mk_con ct in