From: Ferruccio Guidi Date: Wed, 14 Apr 2004 13:56:14 +0000 (+0000) Subject: HELM dependent Mathql-1.4 library X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=refs%2Fheads%2Fmathql_1_4;p=helm.git HELM dependent Mathql-1.4 library --- diff --git a/helm/ocaml/tactics/mQueryHELM.ml b/helm/ocaml/tactics/mQueryHELM.ml new file mode 100644 index 000000000..565678e2c --- /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 index 000000000..5a20bcf52 --- /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 + *) + +val init : unit + +exception TermError of MathQL.result