(* 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