(* *)
(***************************************************************************)
+(* $Id$ *)
+
let mpres_document pres_box =
Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let arg_spec =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MatitaGtkMisc
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let debug = false ;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let rec to_string =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception PopupClosed
open Printf
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MatitaGeneratedGui
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
type thingsToInitilaize =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
(** Functions "imported" from Http_getter_misc *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let main () =
match Filename.basename Sys.argv.(0) with
| "matitadep" | "matitadep.opt" -> Matitadep.main ()
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module UM = UriManager
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module GA = GrafiteAst
module U = UriManager
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module MK = MatitamakeLib ;;
let main () =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let logger = fun mark ->
match mark with
| `Error -> HLog.error
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let _ =
let _ = Topdirs.dir_quit in
Toploop.loop Format.std_formatter;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module Ast = CicNotationPt
module Util = CicNotationUtil
(* *)
(**************************************************************************)
+(* $Id$ *)
+
let object_prefix = "obj:";;
let declaration_prefix = "decl:";;
let definition_prefix = "def:";;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module Ast = CicNotationPt
type value =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
(** CIC Notation Parse Tree *)
type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module Ast = CicNotationPt
let visit_ast ?(special_k = fun _ -> assert false) k =
(* *)
(**************************************************************************)
+(* $Id$ *)
+
type id = string;;
type joint_recursion_kind =
[ `Recursive of int list
(* *)
(***************************************************************************)
+(* $Id$ *)
+
exception TO_DO;;
let proof2cic deannotate p =
(* *)
(***************************************************************************)
+(* $Id$ *)
+
exception ContentPpInternalError;;
exception NotEnoughElements;;
exception TO_DO
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
(* *)
(*****************************************************************************)
+(* $Id$ *)
+
(* STUFF TO MANAGE IDENTIFIERS *)
type id = string (* the abstract type of the (annotated) node identifiers *)
type 'term explicit_named_substitution = (UriManager.uri * 'term) list
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
(* *)
(*****************************************************************************)
+(* $Id$ *)
+
(*****************************************************************************)
(** switch implementation **)
(*****************************************************************************)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
exception Meta_not_found of int
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* converts annotated terms into cic terms (forgetting ids and names) *)
let rec deannotate_term =
let module C = Cic in
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module DiscriminationTreeIndexing =
functor (A:Set.S) ->
struct
+(* Copyright (C) 2005, 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/.
+ *)
+
+(* $Id$ *)
+
(** {2 Auxiliary functions} *)
let uri = UriManager.uri_of_string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
(**** TABLES ****)
let default_eq_URIs =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* path indexing implementation *)
(* position of the subterm, subterm (Appl are not stored...) *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let _ =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let rec unshare =
let module C = Cic in
function
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
(*CSC codice cut & paste da cicPp e xmlcommand *)
exception NotImplemented;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
let string_of_sort = function
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception Impossible of int;;
exception NotWellTyped of string;;
exception WrongUriToConstant of string;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception ReferenceToNonVariable;;
let prerr_endline _ = ();;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open DisambiguateTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open DisambiguateTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
(*
type term = CicNotationPt.term
type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let _ =
DisambiguateChoices.add_num_choice
("natural number",
(* *)
(*****************************************************************************)
+(* $Id$ *)
(* ************************************************************************** *
CicEnvironment SETTINGS (trust and clean_tmp)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
type msg =
[ `Start_type_checking of UriManager.uri
| `Type_checking_completed of UriManager.uri
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let rec letin_nf =
let module C = Cic in
function
(* *)
(*****************************************************************************)
+(* $Id$ *)
+
exception CicPpInternalError;;
exception NotEnoughElements;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO unify exceptions *)
exception CicReductionInternalError;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception CannotSubstInMeta;;
exception RelToHiddenHypothesis;;
exception ReferenceToVariable;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
* ...") *)
(* *)
(*****************************************************************************)
+(* $Id$ *)
+
module C = Cic
module H = UriManager.UriHashtbl
let eq = UriManager.eq
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug_print = fun _ -> ()
let rec higher_name arity =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
(* PROFILING *)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* identity_relocation_list_for_metavariable i canonical_context *)
(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
(* where n = List.length [canonical_context] *)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
exception RefineFailure of string Lazy.t;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
exception UnificationFailure of string Lazy.t;;
(* *)
(*************************************************************************)
+(* $Id$ *)
+
type
'expr box =
Text of attr * string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module Pres = Mpresentation
(** {2 Pretty printing from BoxML to strings} *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
exception Error of int * int * string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
module Ast = CicNotationPt
module Mpres = Mpresentation
(* *)
(***************************************************************************)
+(* $Id$ *)
+
module P = Mpresentation
module B = Box
module Con = Content
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
(* *)
(**************************************************************************)
+(* $Id$ *)
+
type 'a mpres =
Mi of attr * string
| Mn of attr * string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type xml_attribute = string option * string * string
type markup = [ `MathML | `BoxML ]
(* *)
(***************************************************************************)
+(* $Id$ *)
+
let p_mtr a b = Mpresentation.Mtr(a,b)
let p_mtd a b = Mpresentation.Mtd(a,b)
let p_mtable a b = Mpresentation.Mtable(a,b)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let _ =
let level = ref "2@" in
let ic = ref stdin in
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
(** PROFILING *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
type log_tag = [ `Debug | `Error | `Message | `Warning ]
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception Corrupt_file of string
exception Format_mismatch of string
exception Version_mismatch of string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
type pattern_kind = Variable | Constructor
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open Http_getter_common
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Http_getter_types;;
open Printf;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf;;
let version = "0.4.0"
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open Http_getter_types
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let log_level = ref 1
let get_log_level () = !log_level
let set_log_level l = log_level := l
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let file_scheme_prefix = "file://"
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open Http_getter_misc
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception Bad_request of string
exception Unresolvable_URI of string
exception Invalid_URI of string
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Http_getter_types
let send cmd =
+(* $Id$ *)
let _ = Helm_registry.load_from "foo.conf.xml"
let fname = Http_getter.getxml ~format:`Normal ~patch_dtd:true Sys.argv.(1) in
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type direction = [ `LeftToRight | `RightToLeft ]
type loc = Token.flocation
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open GrafiteAst
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type ast_command = Cic.obj GrafiteAst.command
type moo = ast_command list
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception Drop
exception IncludedFileNotCompiled of string (* file name *)
(* the integer is expected to be the goal the user is currently seeing *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let is_empty buri =
List.for_all
(function
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let add_obj ~basedir uri obj status =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception Option_error of string * string
exception Statement_error of string
exception Command_error of string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let load_notation ~include_paths fname =
let ic = open_in fname in
let lexbuf = Ulexing.from_utf8_channel ic in
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception UnableToInclude of string
(* statements meaningful for matitadep *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception BaseUriNotSetYet
let singleton = function
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
exception Ambiguous_input
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Gramext
let tex_of_unicode s =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let _ =
let ic = ref stdin in
let usage = "test_coarse_parser [ file ]" in
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let _ = Helm_registry.load_from "test_parser.conf.xml"
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_types;;
open Printf;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_common;;
open Printf;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_misc;;
open Hbugs_types;;
open Printf;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_common;;
open Hbugs_types;;
open Printf;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_types;;
open Printf;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let _ = Random.self_init ()
let id_length = 32
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_types;;
open Printf;;
open Pxp_document;;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf;;
let rec hashtbl_remove_all tbl key =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_types;;
open Printf;;
+(* $Id$ *)
open Hbugs_types;;
open Printf;;
(* *)
(******************************************************************************)
+(* $Id$ *)
+
let domImpl = Gdome.domImplementation ()
let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let document_of_xml (domImplementation : Gdome.domImplementation) strm =
let module G = Gdome in
let module X = Xml in
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
type dbd = Mysql.dbd option
type result = Mysql.result option
type error_code = Mysql.error_code
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open LexiconAst
type notation_id =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open DisambiguateTypes
let alias_of_domain_and_codomain_items domain_item (dsc,_) =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type direction = [ `LeftToRight | `RightToLeft ]
type loc = Token.flocation
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open LexiconAst
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception IncludedFileNotCompiled of string (* file name *)
exception MetadataNotFound of string (* file name *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type lexicon = LexiconAst.command list
let format_name = "lexicon"
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let alias_diff ~from status =
let module Map = DisambiguateTypes.Environment in
Map.fold
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
exception Elim_failure of string Lazy.t
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let rec_ty uri leftno =
let rec_ty = Cic.MutInd (uri,0,[]) in
if leftno = 0 then rec_ty else
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
exception EqCarrNotImplemented of string Lazy.t
exception EqCarrOnNonMetaClosed
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf;;
type coercion_search_result =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let debug = false
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf ;;
let instance =
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let obj_file_of_baseuri ~basedir ~baseuri =
let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
path ^ ".moo"
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
exception Checksum_failure of string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception AlreadyDefined of UriManager.uri
let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
(* output data structures ***************************************************)
type path = string list (* the name of an attribute *)
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
exception NotAnInductiveDefinition
let get_constraints = function
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
module T = MQGTypes
let text_of_entries out entries =
(* *)
(******************************************************************************)
+(* $Id$ *)
+
module T = MQGTypes
module U = MQGUtil
* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
*)
+(* $Id$ *)
+
(* low level types *********************************************************)
type uri = string
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
module T = MQGTypes
(* low level functions *****************************************************)
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
module M = MathQL
module T = MQGTypes
module U = MQGUtil
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
type connection = MySQL_C of HMysql.dbd
| Postgres_C of Postgres.connection
| No_C
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
module U = MQueryUtil
type pg_map = (MathQL.path * (bool * string * string option)) list
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
let init () =
let module HR = Helm_registry in
let host =
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
let init () =
let connection_string =
Helm_registry.get "mathql_interpreter.postgresql_connection_string"
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
module M = MathQL
module C = MQIConn
module U = MQIUtil
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
type 'a con = MathQL.pattern * 'a * MathQL.value
type 'a con_true = 'a con list
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
(* boolean constants *******************************************************)
let mql_false = []
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
(* contexts *****************************************************************)
type svar_context = (MathQL.svar * MathQL.resource_set) list
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
(* text linearization and parsing *******************************************)
let rec txt_list out f s = function
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MetadataTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open MetadataTypes
open Printf
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MetadataTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MetadataTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let position_prefix = "http://www.cs.unibo.it/helm/schemas/schema-helm#"
(* let position_prefix = "" *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf;;
type tbl = [ `RefObj| `RefSort| `RefRel| `ObjectName| `Hits| `Count]
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module type EqualityIndex =
sig
module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module Index = Equality_indexing.DT (* discrimination tree based indexing *)
(*
module Index = Equality_indexing.DT (* path tree based indexing *)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Utils;;
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module Trivial_disambiguate:
sig
exception Ambiguous_term of string Lazy.t
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Inference;;
open Utils;;
+(* $Id$ *)
+
open Path_indexing
(*
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug = true;;
let debug_print s = if debug then prerr_endline (Lazy.force s);;
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let debug = false
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf;;
Helm_registry.load_from Sys.argv.(1);
Helm_registry.iter ~interpolate:false (fun k v -> printf "%s = %s\n" k v);
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let debug = false
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug_print = fun _ -> ()
let rec injection_tac ~term =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module C = Cic
module P = PrimitiveTactics
module T = Tacticals
* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
+
+(* $Id$ *)
let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(******************** THE FOURIER TACTIC ***********************)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
module PEH = ProofEngineHelpers
module U = CicUniv
(* *)
(*********************************************************************)
+(* $Id$ *)
(* the file contains an hash table of objects of the library
equivalent to some object in the standard subset; it is
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception History_failure
class ['a] history size =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let fake_constructor_tac ~n (proof, goal) =
let module C = Cic in
let module R = CicReduction in
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
exception NotAnInductiveTypeToEliminate
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let nonvar uri = not (UriManager.uri_is_var uri)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let absurd_tac ~term =
let absurd_tac ~term status =
let (proof, goal) = status in
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineHelpers
open ProofEngineTypes
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception Bad_pattern of string Lazy.t
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
(* *)
(******************************************************************************)
+(* $Id$ *)
(* The code of this module is derived from the code of CicReduction *)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineTypes
let clearbody ~hyp =
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineTypes
(* Note: this code is almost identical to change_tac and
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open CicReduction
open PrimitiveTactics
open ProofEngineTypes
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let default_history_size = 20
exception No_goal_left
(* *)
(*****************************************************************************)
+(* $Id$ *)
+
module MQI = MQueryInterpreter
module MQIC = MQIConn
module I = MQueryInterpreter
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* open CicReduction
open ProofEngineTypes
open UriManager *)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let debug = true
let debug_print s = if debug then prerr_endline (Lazy.force s)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(*
* "cic:/a/b/c.con" => ("cic:/a/b/c.con", id )
* "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let debug = false
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
+(* $Id$ *)
+
prerr_endline <:unicode<lambda>>
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception Macro_not_found of string
exception Utf8_not_found of string
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
(* fwd_simpl ****************************************************************)
let rec filter_map_n f n = function
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let nonvar uri = not (UriManager.uri_is_var uri)
+(* $Id$ *)
(* Parsing test:
* - XmlPushParser version *)
(* *)
(******************************************************************************)
+(* $Id$ *)
+
(* the type token for XML cdata, empty elements and not-empty elements *)
(* Usage: *)
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let gzip_bufsize = 10240
type callbacks = {
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let mathmlns = "http://www.w3.org/1998/Math/MathML";;
let xmldiffns = "http://helm.cs.unibo.it/XmlDiff";;
let helmns = "http://www.cs.unibo.it/helm";;
projects / helm.git / commitdiff