]> matita.cs.unibo.it Git - helm.git/commitdiff
"backPointer" metadata enabled
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 3 Jul 2003 14:14:49 +0000 (14:14 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 3 Jul 2003 14:14:49 +0000 (14:14 +0000)
helm/ocaml/mathql_interpreter/mQIProperty.ml

index 7550bcc9c025fc97335a0df518a1fd9b5a173e93..026e11b488b608831620785a245c70a7934b065c 100644 (file)
@@ -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