HELM dependent Mathql-1.4 library

diff --git a/helm/ocaml/tactics/mQueryHELM.ml b/helm/ocaml/tactics/mQueryHELM.ml
new file mode 100644 (file)
index 0000000..565678e
--- /dev/null
+++ b/helm/ocaml/tactics/mQueryHELM.ml
@@ -0,0 +1,118 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module M = MathQL
+module U = AvsUtil
+module L = MQILib
+module Misc = MQueryMisc
+module ER = ProofEngineReduction
+
+let init = ()
+
+(* external functions implementation  * * * * * * * * * * * * * * * * * * * *)
+
+exception TermError of M.result
+
+let uriref_of_avs r =
+   match U.string_of_avs r with
+      | Some s -> Misc.uriref_of_string s
+      | None   -> raise (TermError r)
+
+let body_of_set r =
+   let b, _ = Misc.get_object (uriref_of_avs r) in b
+
+let type_of_set r = 
+   let _, t = Misc.get_object (uriref_of_avs r) in t
+
+(* BODY OF OBJECT ***********************************************************)
+
+let helm_body_fun =
+   let aux r = 
+      try U.avs_of_string (CicPp.ppterm (body_of_set r)) with _ -> U.val_false
+   in
+   L.fun_arity1 ["helm"; "body"] "" aux
+
+let _ = L.fun_register ["helm"; "body"] helm_body_fun
+
+(* TYPE OF OBJECT ***********************************************************)
+
+let helm_type_fun =
+   let aux r = 
+      try U.avs_of_string (CicPp.ppterm (type_of_set r)) with _ -> U.val_false
+   in
+   L.fun_arity1 ["helm"; "type"] "" aux
+
+let _ = L.fun_register ["helm"; "type"] helm_type_fun
+
+(* ALPHA CONVERTIBILITY OF BODIES *******************************************)
+
+let helm_alpha_body_fun = 
+   let aux r1 r2 = 
+      try 
+         if ER.alpha_equivalence (body_of_set r1) (body_of_set r2) 
+         then U.val_true else U.val_false
+      with _ -> U.val_false
+   in 
+   L.fun_arity2 ["helm"; "alpha"; "body"] "" aux 
+
+let _ = L.fun_register ["helm"; "alpha"; "body"] helm_alpha_body_fun
+
+(* ALPHA CONVERTIBILITY OF TYPES ********************************************)
+
+let helm_alpha_type_fun = 
+   let aux r1 r2 = 
+      try 
+         if ER.alpha_equivalence (type_of_set r1) (type_of_set r2) 
+         then U.val_true else U.val_false
+      with _ -> U.val_false
+   in 
+   L.fun_arity2 ["helm"; "alpha"; "type"] "" aux 
+
+let _ = L.fun_register ["helm"; "alpha"; "type"] helm_alpha_type_fun
+
+(* generator functions implementation * * * * * * * * * * * * * * * * * * * *)
+
+(* STANDARD VARIABLES FOR METADATA ******************************************)
+
+let helm_aliases_gen =
+   let mk_let v s x = M.Let (Some v, M.Const [(s, [])], x) in 
+   let arity = L.Const 1 in
+   let code _ = function
+      | [x] -> 
+         let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
+         let x = mk_let "SET" "Set" x in
+        let x = mk_let "PROP" "Prop" x in
+        let x = mk_let "TYPE" "Type" x in
+        let x = mk_let "CPROP" "CProp" x in
+        let x = mk_let "MH" (ns ^ "MainHypothesis") x in
+        let x = mk_let "MC" (ns ^ "MainConclusion") x in
+        let x = mk_let "IH" (ns ^ "InHypothesis") x in
+        let x = mk_let "IC" (ns ^ "InConclusion") x in
+                mk_let "IB" (ns ^ "InBody") x
+      | _   -> assert false
+   in
+   {L.arity = arity; L.code = code}
+
+let _ = L.gen_register ["helm"; "aliases"] helm_aliases_gen

diff --git a/helm/ocaml/tactics/mQueryHELM.mli b/helm/ocaml/tactics/mQueryHELM.mli
new file mode 100644 (file)
index 0000000..5a20bcf
--- /dev/null
+++ b/helm/ocaml/tactics/mQueryHELM.mli
@@ -0,0 +1,31 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val init : unit
+
+exception TermError of MathQL.result