helm/ocaml/tactics/mQueryHELM.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module M = MathQL
  27 module U = AvsUtil
  28 module L = MQILib
  29 module Misc = MQueryMisc
  30 module ER = ProofEngineReduction
  31
  32 let init = ()
  33
  34 (* external functions implementation  * * * * * * * * * * * * * * * * * * * *)
  35
  36 exception TermError of M.result
  37
  38 let uriref_of_avs r =
  39    match U.string_of_avs r with
  40       | Some s -> Misc.uriref_of_string s
  41       | None   -> raise (TermError r)
  42
  43 let body_of_set r =
  44    let b, _ = Misc.get_object (uriref_of_avs r) in b
  45
  46 let type_of_set r =
  47    let _, t = Misc.get_object (uriref_of_avs r) in t
  48
  49 (* BODY OF OBJECT ***********************************************************)
  50
  51 let helm_body_fun =
  52    let aux r =
  53       try U.avs_of_string (CicPp.ppterm (body_of_set r)) with _ -> U.val_false
  54    in
  55    L.fun_arity1 ["helm"; "body"] "" aux
  56
  57 let _ = L.fun_register ["helm"; "body"] helm_body_fun
  58
  59 (* TYPE OF OBJECT ***********************************************************)
  60
  61 let helm_type_fun =
  62    let aux r =
  63       try U.avs_of_string (CicPp.ppterm (type_of_set r)) with _ -> U.val_false
  64    in
  65    L.fun_arity1 ["helm"; "type"] "" aux
  66
  67 let _ = L.fun_register ["helm"; "type"] helm_type_fun
  68
  69 (* ALPHA CONVERTIBILITY OF BODIES *******************************************)
  70
  71 let helm_alpha_body_fun =
  72    let aux r1 r2 =
  73       try
  74          if ER.alpha_equivalence (body_of_set r1) (body_of_set r2)
  75          then U.val_true else U.val_false
  76       with _ -> U.val_false
  77    in
  78    L.fun_arity2 ["helm"; "alpha"; "body"] "" aux
  79
  80 let _ = L.fun_register ["helm"; "alpha"; "body"] helm_alpha_body_fun
  81
  82 (* ALPHA CONVERTIBILITY OF TYPES ********************************************)
  83
  84 let helm_alpha_type_fun =
  85    let aux r1 r2 =
  86       try
  87          if ER.alpha_equivalence (type_of_set r1) (type_of_set r2)
  88          then U.val_true else U.val_false
  89       with _ -> U.val_false
  90    in
  91    L.fun_arity2 ["helm"; "alpha"; "type"] "" aux
  92
  93 let _ = L.fun_register ["helm"; "alpha"; "type"] helm_alpha_type_fun
  94
  95 (* generator functions implementation * * * * * * * * * * * * * * * * * * * *)
  96
  97 (* STANDARD VARIABLES FOR METADATA ******************************************)
  98
  99 let helm_aliases_gen =
 100    let mk_let v s x = M.Let (Some v, M.Const [(s, [])], x) in
 101    let arity = L.Const 1 in
 102    let code _ = function
 103       | [x] ->
 104          let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
 105          let x = mk_let "SET" "Set" x in
 106          let x = mk_let "PROP" "Prop" x in
 107          let x = mk_let "TYPE" "Type" x in
 108          let x = mk_let "CPROP" "CProp" x in
 109          let x = mk_let "MH" (ns ^ "MainHypothesis") x in
 110          let x = mk_let "MC" (ns ^ "MainConclusion") x in
 111          let x = mk_let "IH" (ns ^ "InHypothesis") x in
 112          let x = mk_let "IC" (ns ^ "InConclusion") x in
 113                  mk_let "IB" (ns ^ "InBody") x
 114       | _   -> assert false
 115    in
 116    {L.arity = arity; L.code = code}
 117
 118 let _ = L.gen_register ["helm"; "aliases"] helm_aliases_gen