From c3b7b4c8697a146a3d734b5333d655a25a642cb9 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Oct 2010 11:03:27 +0000 Subject: [PATCH] - most of cic/ removed --- matita/components/cic/.depend | 28 +- matita/components/cic/.depend.opt | 28 +- matita/components/cic/Makefile | 8 - matita/components/cic/cicInspect.ml | 147 ---- matita/components/cic/cicInspect.mli | 38 - matita/components/cic/cicParser.ml | 805 ------------------ matita/components/cic/cicParser.mli | 47 - matita/components/cic/cic_indexable.ml | 81 -- matita/components/cic/cic_indexable.mli | 29 - matita/components/cic/deannotate.ml | 225 ----- matita/components/cic/deannotate.mli | 40 - matita/components/cic/helmLibraryObjects.ml | 230 ----- matita/components/cic/helmLibraryObjects.mli | 182 ---- matita/components/cic/libraryObjects.ml | 227 ----- matita/components/cic/libraryObjects.mli | 70 -- matita/components/cic/path_indexing.ml | 227 ----- matita/components/cic/path_indexing.mli | 42 - matita/components/cic/unshare.ml | 214 ----- matita/components/cic/unshare.mli | 27 - matita/components/content/interpretations.ml | 1 - matita/components/grafite/grafiteMarshal.ml | 8 - .../grafite_engine/grafiteEngine.ml | 3 - .../components/grafite_engine/grafiteSync.ml | 6 +- .../ng_cic_content/ncic2astMatcher.ml | 2 - 24 files changed, 6 insertions(+), 2709 deletions(-) delete mode 100644 matita/components/cic/cicInspect.ml delete mode 100644 matita/components/cic/cicInspect.mli delete mode 100644 matita/components/cic/cicParser.ml delete mode 100644 matita/components/cic/cicParser.mli delete mode 100644 matita/components/cic/cic_indexable.ml delete mode 100644 matita/components/cic/cic_indexable.mli delete mode 100644 matita/components/cic/deannotate.ml delete mode 100644 matita/components/cic/deannotate.mli delete mode 100644 matita/components/cic/helmLibraryObjects.ml delete mode 100644 matita/components/cic/helmLibraryObjects.mli delete mode 100644 matita/components/cic/libraryObjects.ml delete mode 100644 matita/components/cic/libraryObjects.mli delete mode 100644 matita/components/cic/path_indexing.ml delete mode 100644 matita/components/cic/path_indexing.mli delete mode 100644 matita/components/cic/unshare.ml delete mode 100644 matita/components/cic/unshare.mli diff --git a/matita/components/cic/.depend b/matita/components/cic/.depend index b7f80297d..cabb8d5d1 100644 --- a/matita/components/cic/.depend +++ b/matita/components/cic/.depend @@ -1,35 +1,11 @@ cicUniv.cmi: -unshare.cmi: cic.cmo -deannotate.cmi: cic.cmo -cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo -helmLibraryObjects.cmi: cic.cmo -libraryObjects.cmi: -cic_indexable.cmi: cic.cmo -path_indexing.cmi: cic.cmo -cicInspect.cmi: cic.cmo cicPp.cmi: cic.cmo cic.cmo: cicUniv.cmi cic.cmx: cicUniv.cmx cicUniv.cmo: cicUniv.cmi cicUniv.cmx: cicUniv.cmi -unshare.cmo: cicUniv.cmi cic.cmo unshare.cmi -unshare.cmx: cicUniv.cmx cic.cmx unshare.cmi -deannotate.cmo: unshare.cmi cic.cmo deannotate.cmi -deannotate.cmx: unshare.cmx cic.cmx deannotate.cmi -cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicParser.cmi -cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi -helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi -helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi -libraryObjects.cmo: libraryObjects.cmi -libraryObjects.cmx: libraryObjects.cmi -cic_indexable.cmo: cicUtil.cmi cic.cmo cic_indexable.cmi -cic_indexable.cmx: cicUtil.cmx cic.cmx cic_indexable.cmi -path_indexing.cmo: cic.cmo path_indexing.cmi -path_indexing.cmx: cic.cmx path_indexing.cmi -cicInspect.cmo: cic.cmo cicInspect.cmi -cicInspect.cmx: cic.cmx cicInspect.cmi -cicPp.cmo: cicUtil.cmi cicUniv.cmi cic.cmo cicPp.cmi -cicPp.cmx: cicUtil.cmx cicUniv.cmx cic.cmx cicPp.cmi +cicPp.cmo: cic.cmo cicPp.cmi +cicPp.cmx: cic.cmx cicPp.cmi diff --git a/matita/components/cic/.depend.opt b/matita/components/cic/.depend.opt index 7306b25a5..296da325d 100644 --- a/matita/components/cic/.depend.opt +++ b/matita/components/cic/.depend.opt @@ -1,35 +1,11 @@ cicUniv.cmi: -unshare.cmi: cic.cmx -deannotate.cmi: cic.cmx -cicParser.cmi: cic.cmx cicUtil.cmi: cic.cmx -helmLibraryObjects.cmi: cic.cmx -libraryObjects.cmi: -cic_indexable.cmi: cic.cmx -path_indexing.cmi: cic.cmx -cicInspect.cmi: cic.cmx cicPp.cmi: cic.cmx cic.cmo: cicUniv.cmi cic.cmx: cicUniv.cmx cicUniv.cmo: cicUniv.cmi cicUniv.cmx: cicUniv.cmi -unshare.cmo: cicUniv.cmi cic.cmx unshare.cmi -unshare.cmx: cicUniv.cmx cic.cmx unshare.cmi -deannotate.cmo: unshare.cmi cic.cmx deannotate.cmi -deannotate.cmx: unshare.cmx cic.cmx deannotate.cmi -cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmx cicParser.cmi -cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi cicUtil.cmo: cicUniv.cmi cic.cmx cicUtil.cmi cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi -helmLibraryObjects.cmo: cic.cmx helmLibraryObjects.cmi -helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi -libraryObjects.cmo: libraryObjects.cmi -libraryObjects.cmx: libraryObjects.cmi -cic_indexable.cmo: cicUtil.cmi cic.cmx cic_indexable.cmi -cic_indexable.cmx: cicUtil.cmx cic.cmx cic_indexable.cmi -path_indexing.cmo: cic.cmx path_indexing.cmi -path_indexing.cmx: cic.cmx path_indexing.cmi -cicInspect.cmo: cic.cmx cicInspect.cmi -cicInspect.cmx: cic.cmx cicInspect.cmi -cicPp.cmo: cicUtil.cmi cicUniv.cmi cic.cmx cicPp.cmi -cicPp.cmx: cicUtil.cmx cicUniv.cmx cic.cmx cicPp.cmi +cicPp.cmo: cic.cmx cicPp.cmi +cicPp.cmx: cic.cmx cicPp.cmi diff --git a/matita/components/cic/Makefile b/matita/components/cic/Makefile index 2ffea3e4d..297d41d20 100644 --- a/matita/components/cic/Makefile +++ b/matita/components/cic/Makefile @@ -3,15 +3,7 @@ PREDICATES = INTERFACE_FILES = \ cicUniv.mli \ - unshare.mli \ - deannotate.mli \ - cicParser.mli \ cicUtil.mli \ - helmLibraryObjects.mli \ - libraryObjects.mli \ - cic_indexable.mli \ - path_indexing.mli \ - cicInspect.mli \ cicPp.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/cic/cicInspect.ml b/matita/components/cic/cicInspect.ml deleted file mode 100644 index 7186fb1f1..000000000 --- a/matita/components/cic/cicInspect.ml +++ /dev/null @@ -1,147 +0,0 @@ -(* Copyright (C) 2003-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/. - *) - -module UM = UriManager -module C = Cic - -module Int = struct - type t = int - let compare = compare -end -module S = Set.Make (Int) - -let overlaps s1 s2 = - let predicate x = S.mem x s1 in - S.exists predicate s2 - -let get_rels_from_premise h t = - let rec aux d g = function - | C.Sort _ - | C.Implicit _ -> g - | C.Rel i -> - if i < d then g else fun a -> g (S.add (i - d + h + 1) a) - | C.Appl ss -> List.fold_left (aux d) g ss - | C.Const (_, ss) - | C.MutInd (_, _, ss) - | C.MutConstruct (_, _, _, ss) - | C.Var (_, ss) -> - let map g (_, t) = aux d g t in - List.fold_left map g ss - | C.Meta (_, ss) -> - let map g = function - | None -> g - | Some t -> aux d g t - in - List.fold_left map g ss - | C.Cast (t1, t2) -> aux d (aux d g t2) t1 - | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 - | C.LetIn (_, t1, ty, t2) -> - aux d (aux d (aux (succ d) g t2) ty) t1 - | C.MutCase (_, _, t1, t2, ss) -> - aux d (aux d (List.fold_left (aux d) g ss) t2) t1 - | C.Fix (_, ss) -> - let k = List.length ss in - let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in - List.fold_left map g ss - | C.CoFix (_, ss) -> - let k = List.length ss in - let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in - List.fold_left map g ss - in - let g a = a in - aux 1 g t S.empty - -let get_mutinds_of_uri u t = - let rec aux g = function - | C.Sort _ - | C.Implicit _ - | C.Rel _ -> g - | C.Appl ss -> List.fold_left aux g ss - | C.Const (_, ss) - | C.MutConstruct (_, _, _, ss) - | C.Var (_, ss) -> - let map g (_, t) = aux g t in - List.fold_left map g ss - | C.MutInd (uri, tyno, ss) -> - let map g (_, t) = aux g t in - let g = List.fold_left map g ss in - if UM.eq u uri then fun a -> g (S.add tyno a) else g - | C.Meta (_, ss) -> - let map g = function - | None -> g - | Some t -> aux g t - in - List.fold_left map g ss - | C.Cast (t1, t2) -> aux (aux g t2) t1 - | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux (aux g t2) t1 - | C.LetIn (_, t1, ty, t2) -> aux (aux (aux g t2) ty) t1 - | C.MutCase (_, _, t1, t2, ss) -> - aux (aux (List.fold_left aux g ss) t2) t1 - | C.Fix (_, ss) -> - let map g (_, _, t1, t2) = aux (aux g t2) t1 in - List.fold_left map g ss - | C.CoFix (_, ss) -> - let map g (_, t1, t2) = aux (aux g t2) t1 in - List.fold_left map g ss - in - let g a = a in - aux g t S.empty - -let count_nodes ~meta n t = - let offset = if meta then 1 else 0 in - let rec aux n = function - | C.Implicit _ -> offset + n - | C.Sort _ - | C.Rel _ -> succ n - | C.Appl ts -> - List.fold_left aux (List.length ts - 1 + n) ts - | C.Const (_, ss) - | C.MutConstruct (_, _, _, ss) - | C.MutInd (_, _, ss) - | C.Var (_, ss) -> - let map n (_, t) = aux n t in - List.fold_left map (succ n) ss - | C.Meta (_, ss) -> - let map n = function - | None -> n - | Some t -> aux n t - in - List.fold_left map (n + offset) ss - | C.Cast (t1, t2) -> aux (aux (offset + n) t2) t1 - | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1 - | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (offset + n) t2) ty) t1 - | C.MutCase (_, _, t1, t2, ss) -> - aux (aux (List.fold_left aux (offset + 1 + n) ss) t2) t1 - | C.Fix (_, ss) -> - let map n (_, _, t1, t2) = aux (aux n t2) t1 in - List.fold_left map (2 + n) ss - | C.CoFix (_, ss) -> - let map n (_, t1, t2) = aux (aux n t2) t1 in - List.fold_left map (2 + n) ss -in -aux n t diff --git a/matita/components/cic/cicInspect.mli b/matita/components/cic/cicInspect.mli deleted file mode 100644 index a5b79b36d..000000000 --- a/matita/components/cic/cicInspect.mli +++ /dev/null @@ -1,38 +0,0 @@ -(* Copyright (C) 2003-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/. - *) - -module S: Set.S with type elt = int - -val overlaps: S.t -> S.t -> bool - -val get_rels_from_premise: int -> Cic.term -> S.t - -val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t - -(* count_nodes n t returns n + the number of nodes in t *) -(* implicits, metas and casts are counted if ~meta:true *) -(* if ~meta:false, complies with *) -(* F.Guidi: Procedural representation of CIC Proof Terms. Last version *) -val count_nodes: meta:bool -> int -> Cic.term -> int diff --git a/matita/components/cic/cicParser.ml b/matita/components/cic/cicParser.ml deleted file mode 100644 index 3962323a1..000000000 --- a/matita/components/cic/cicParser.ml +++ /dev/null @@ -1,805 +0,0 @@ -(* Copyright (C) 2004-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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) - -open Printf - -(* ZACK TODO element from the DTD still to be handled: - - - - - - - -*) - -exception Getter_failure of string * string -exception Parser_failure of string - -type stack_entry = - | Arg of string * Cic.annterm (* relative uri, term *) - (* constants' body and types resides in differne files, thus we can't simple - * keep constants in Cic_obj stack entries *) - | Cic_attributes of Cic.attribute list - | Cic_constant_body of string * string * UriManager.uri list * Cic.annterm - * Cic.attribute list - (* id, for, params, body, object attributes *) - | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm - * Cic.attribute list - (* id, name, params, type, object attributes *) - | Cic_term of Cic.annterm (* term *) - | Cic_obj of Cic.annobj (* object *) - | Cofix_fun of Cic.id * string * Cic.annterm * Cic.annterm - (* id, name, type, body *) - | Constructor of string * Cic.annterm (* name, type *) - | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) - | Def of Cic.id * Cic.name * Cic.annterm * Cic.annterm (* id, binder, source, type *) - | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm - (* id, name, ind. index, type, body *) - | Inductive_type of string * string * bool * Cic.annterm * - (string * Cic.annterm) list (* id, name, inductive, arity, constructors *) - | Meta_subst of Cic.annterm option - | Obj_class of Cic.object_class - | Obj_flavour of Cic.object_flavour - | Obj_field of string (* field name *) - | Obj_generated - | Tag of string * (string * string) list (* tag name, attributes *) - (* ZACK TODO add file position to tag stack entry so that when attribute - * errors occur, the position of their _start_tag_ could be printed - * instead of the current position (usually the end tag) *) - -type ctxt = { - mutable stack: stack_entry list; - mutable xml_parser: XmlPushParser.xml_parser option; - mutable filename: string; - uri: UriManager.uri; -} - -let string_of_stack ctxt = - "[" ^ (String.concat "; " - (List.map - (function - | Arg (reluri, _) -> sprintf "Arg %s" reluri - | Cic_attributes _ -> "Cic_attributes" - | Cic_constant_body (id, name, _, _, _) -> - sprintf "Cic_constant_body %s (id=%s)" name id - | Cic_constant_type (id, name, _, _, _) -> - sprintf "Cic_constant_type %s (id=%s)" name id - | Cic_term _ -> "Cic_term" - | Cic_obj _ -> "Cic_obj" - | Constructor (name, _) -> "Constructor " ^ name - | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id - | Decl (id, _, _) -> sprintf "Decl (id=%s)" id - | Def (id, _, _, _) -> sprintf "Def (id=%s)" id - | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id - | Inductive_type (id, name, _, _, _) -> - sprintf "Inductive_type %s (id=%s)" name id - | Meta_subst _ -> "Meta_subst" - | Obj_class _ -> "Obj_class" - | Obj_flavour _ -> "Obj_flavour" - | Obj_field name -> "Obj_field " ^ name - | Obj_generated -> "Obj_generated" - | Tag (tag, _) -> "Tag " ^ tag) - ctxt.stack)) ^ "]" - -let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2 -let sort_attrs = List.sort compare_attrs - -let new_parser_context uri = { - stack = []; - xml_parser = None; - filename = "-"; - uri = uri; -} - -let get_parser ctxt = - match ctxt.xml_parser with - | Some p -> p - | None -> assert false - -(** {2 Error handling} *) - -let parse_error ctxt msg = - let (line, col) = XmlPushParser.get_position (get_parser ctxt) in - raise (Parser_failure (sprintf "[%s: line %d, column %d] %s" - ctxt.filename line col msg)) - -let attribute_error ctxt tag = - parse_error ctxt ("wrong attribute set for " ^ tag) - -(** {2 Parsing context management} *) - -let pop ctxt = -(* debug_print (lazy "pop");*) - match ctxt.stack with - | hd :: tl -> (ctxt.stack <- tl) - | _ -> assert false - -let push ctxt v = -(* debug_print (lazy "push");*) - ctxt.stack <- v :: ctxt.stack - -let set_top ctxt v = -(* debug_print (lazy "set_top");*) - match ctxt.stack with - | _ :: tl -> (ctxt.stack <- v :: tl) - | _ -> assert false - - (** pop the last tag from the open tags stack returning a pair *) -let pop_tag ctxt = - match ctxt.stack with - | Tag (tag, attrs) :: tl -> - ctxt.stack <- tl; - (tag, attrs) - | _ -> parse_error ctxt "unexpected extra content" - - (** pop the last tag from the open tags stack returning its attributes. - * Attributes are returned as a list of pair _sorted_ by - * attribute name *) -let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt)) - -let pop_cics ctxt = - let rec aux acc stack = - match stack with - | Cic_term t :: tl -> aux (t :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_class_modifiers ctxt = - let rec aux acc stack = - match stack with - | (Cic_term (Cic.ASort _) as m) :: tl - | (Obj_field _ as m) :: tl -> - aux (m :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_meta_substs ctxt = - let rec aux acc stack = - match stack with - | Meta_subst t :: tl -> aux (t :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_fix_funs ctxt = - let rec aux acc stack = - match stack with - | Fix_fun (id, name, index, typ, body) :: tl -> - aux ((id, name, index, typ, body) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_cofix_funs ctxt = - let rec aux acc stack = - match stack with - | Cofix_fun (id, name, typ, body) :: tl -> - aux ((id, name, typ, body) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_constructors ctxt = - let rec aux acc stack = - match stack with - | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - values - -let pop_inductive_types ctxt = - let rec aux acc stack = - match stack with - | Inductive_type (id, name, ind, arity, ctors) :: tl -> - aux ((id, name, ind, arity, ctors) :: acc) tl - | tl -> acc, tl - in - let values, new_stack = aux [] ctxt.stack in - if values = [] then - parse_error ctxt "no \"InductiveType\" element found"; - ctxt.stack <- new_stack; - values - - (** travels the stack (without popping) for the first term subject of explicit - * named substitution and return its URI *) -let find_base_uri ctxt = - let rec aux = function - | Cic_term (Cic.AConst (_, uri, _)) :: _ - | Cic_term (Cic.AMutInd (_, uri, _, _)) :: _ - | Cic_term (Cic.AMutConstruct (_, uri, _, _, _)) :: _ - | Cic_term (Cic.AVar (_, uri, _)) :: _ -> - uri - | Arg _ :: tl -> aux tl - | _ -> parse_error ctxt "no \"arg\" element found" - in - UriManager.buri_of_uri (aux ctxt.stack) - - (** backwardly eats the stack building an explicit named substitution from Arg - * stack entries *) -let pop_subst ctxt base_uri = - let rec aux acc stack = - match stack with - | Arg (rel_uri, term) :: tl -> - let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in - aux ((uri, term) :: acc) tl - | tl -> acc, tl - in - let subst, new_stack = aux [] ctxt.stack in - if subst = [] then - parse_error ctxt "no \"arg\" element found"; - ctxt.stack <- new_stack; - subst - -let pop_cic ctxt = - match ctxt.stack with - | Cic_term t :: tl -> - ctxt.stack <- tl; - t - | _ -> parse_error ctxt "no cic term found" - -let pop_obj_attributes ctxt = - match ctxt.stack with - | Cic_attributes attributes :: tl -> - ctxt.stack <- tl; - attributes - | _ -> [] - -(** {2 Auxiliary functions} *) - -let uri_of_string = UriManager.uri_of_string - -let uri_list_of_string = - let space_RE = Str.regexp " " in - fun s -> - List.map uri_of_string (Str.split space_RE s) - -let impredicative_set = ref true;; - -let sort_of_string ctxt = function - | "Prop" -> Cic.Prop - (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY - * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION - * IS FIXED *) - | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ()) - | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) - | "Set" when !impredicative_set -> Cic.Set - | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) - | s -> - let len = String.length s in - let sort_len, mk_sort = - if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x - else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x - else parse_error ctxt "sort expected" - in - let s = String.sub s sort_len (len - sort_len) in - let i = String.index s ':' in - let id = int_of_string (String.sub s 0 i) in - let suri = String.sub s (i+1) (len - sort_len - i - 1) in - let uri = UriManager.uri_of_string suri in - try mk_sort (CicUniv.fresh ~uri ~id ()) - with - | Failure "int_of_string" - | Invalid_argument _ -> parse_error ctxt "sort expected" - -let patch_subst ctxt subst = function - | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst) - | Cic.AMutInd (id, uri, typeno, _) -> - Cic.AMutInd (id, uri, typeno, subst) - | Cic.AMutConstruct (id, uri, typeno, consno, _) -> - Cic.AMutConstruct (id, uri, typeno, consno, subst) - | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst) - | _ -> - parse_error ctxt - ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^ - " instantiated") - - (** backwardly eats the stack seeking for the first open tag carrying - * "helm:exception" attributes. If found return Some of a pair containing - * exception name and argument. Return None otherwise *) -let find_helm_exception ctxt = - let rec aux = function - | [] -> None - | Tag (_, attrs) :: tl -> - (try - let exn = List.assoc "helm:exception" attrs in - let arg = - try List.assoc "helm:exception_arg" attrs with Not_found -> "" - in - Some (exn, arg) - with Not_found -> aux tl) - | _ :: tl -> aux tl - in - aux ctxt.stack - -(** {2 Push parser callbacks} - * each callback needs to be instantiated to a parsing context *) - -let start_element ctxt tag attrs = -(* debug_print (lazy (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs))));*) - push ctxt (Tag (tag, attrs)) - -let end_element ctxt tag = -(* debug_print (lazy (sprintf "" tag));*) -(* debug_print (lazy (string_of_stack ctxt));*) - let attribute_error () = attribute_error ctxt tag in - let parse_error = parse_error ctxt in - let sort_of_string = sort_of_string ctxt in - match tag with - | "REL" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["binder", binder; "id", id; "idref", idref; "value", value] - | ["binder", binder; "id", id; "idref", idref; "sort", _; - "value", value] -> - Cic.ARel (id, idref, int_of_string value, binder) - | _ -> attribute_error ())) - | "VAR" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "uri", uri] - | ["id", id; "sort", _; "uri", uri] -> - Cic.AVar (id, uri_of_string uri, []) - | _ -> attribute_error ())) - | "CONST" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "uri", uri] - | ["id", id; "sort", _; "uri", uri] -> - Cic.AConst (id, uri_of_string uri, []) - | _ -> attribute_error ())) - | "SORT" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort) - | _ -> attribute_error ())) - | "APPLY" -> - let args = pop_cics ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id ] - | ["id", id; "sort", _] -> Cic.AAppl (id, args) - | _ -> attribute_error ())) - | "decl" -> - let source = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["binder", binder; "id", id ] - | ["binder", binder; "id", id; "type", _] -> - Decl (id, Cic.Name binder, source) - | ["id", id] - | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source) - | _ -> attribute_error ()) - | "def" -> (* same as "decl" above *) - let ty,source = - (*CSC: hack to parse Coq files where the LetIn is not typed *) - let ty = pop_cic ctxt in - try - let source = pop_cic ctxt in - ty,source - with - Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty - in - push ctxt - (match pop_tag_attrs ctxt with - | ["binder", binder; "id", id] - | ["binder", binder; "id", id; "sort", _] -> - Def (id, Cic.Name binder, source, ty) - | ["id", id] - | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty) - | _ -> attribute_error ()) - | "arity" (* transparent elements (i.e. which contain a CIC) *) - | "body" - | "inductiveTerm" - | "pattern" - | "patternsType" - | "target" - | "term" - | "type" -> - let term = pop_cic ctxt in - pop ctxt; (* pops start tag matching current end tag (e.g. ) *) - push ctxt (Cic_term term) - | "substitution" -> (* optional transparent elements (i.e. which _may_ - * contain a CIC) *) - set_top ctxt (* replace *) - (match ctxt.stack with - | Cic_term term :: tl -> - ctxt.stack <- tl; - (Meta_subst (Some term)) - | _ -> Meta_subst None) - | "PROD" -> - let target = pop_cic ctxt in - let rec add_decl target = function - | Decl (id, binder, source) :: tl -> - add_decl (Cic.AProd (id, binder, source, target)) tl - | tl -> - ctxt.stack <- tl; - target - in - let term = add_decl target ctxt.stack in - (match pop_tag_attrs ctxt with - [] - | ["type", _] -> () - | _ -> attribute_error ()); - push ctxt (Cic_term term) - | "LAMBDA" -> - let target = pop_cic ctxt in - let rec add_decl target = function - | Decl (id, binder, source) :: tl -> - add_decl (Cic.ALambda (id, binder, source, target)) tl - | tl -> - ctxt.stack <- tl; - target - in - let term = add_decl target ctxt.stack in - (match pop_tag_attrs ctxt with - [] - | ["sort", _] -> () - | _ -> attribute_error ()); - push ctxt (Cic_term term) - | "LETIN" -> - let target = pop_cic ctxt in - let rec add_def target = function - | Def (id, binder, source, ty) :: tl -> - add_def (Cic.ALetIn (id, binder, source, ty, target)) tl - | tl -> - ctxt.stack <- tl; - target - in - let term = add_def target ctxt.stack in - (match pop_tag_attrs ctxt with - [] - | ["sort", _] -> () - | _ -> attribute_error ()); - push ctxt (Cic_term term) - | "CAST" -> - let typ = pop_cic ctxt in - let term = pop_cic ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - ["id", id] - | ["id", id; "sort", _] -> Cic.ACast (id, term, typ) - | _ -> attribute_error ())); - | "IMPLICIT" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id] -> Cic.AImplicit (id, None) - | ["annotation", annotation; "id", id] -> - let implicit_annotation = - match annotation with - | "closed" -> `Closed - | "hole" -> `Hole - | "type" -> `Type - | _ -> parse_error "invalid value for \"annotation\" attribute" - in - Cic.AImplicit (id, Some implicit_annotation) - | _ -> attribute_error ())) - | "META" -> - let meta_substs = pop_meta_substs ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "no", no] - | ["id", id; "no", no; "sort", _] -> - Cic.AMeta (id, int_of_string no, meta_substs) - | _ -> attribute_error ())); - | "MUTIND" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noType", noType; "uri", uri] -> - Cic.AMutInd (id, uri_of_string uri, int_of_string noType, []) - | _ -> attribute_error ())); - | "MUTCONSTRUCT" -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri] - | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _; - "uri", uri] -> - Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType, - int_of_string noConstr, []) - | _ -> attribute_error ())); - | "FixFunction" -> - let body = pop_cic ctxt in - let typ = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "name", name; "recIndex", recIndex] -> - Fix_fun (id, name, int_of_string recIndex, typ, body) - | _ -> attribute_error ()) - | "CofixFunction" -> - let body = pop_cic ctxt in - let typ = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "name", name] -> - Cofix_fun (id, name, typ, body) - | _ -> attribute_error ()) - | "FIX" -> - let fix_funs = pop_fix_funs ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noFun", noFun] - | ["id", id; "noFun", noFun; "sort", _] -> - Cic.AFix (id, int_of_string noFun, fix_funs) - | _ -> attribute_error ())) - | "COFIX" -> - let cofix_funs = pop_cofix_funs ctxt in - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noFun", noFun] - | ["id", id; "noFun", noFun; "sort", _] -> - Cic.ACoFix (id, int_of_string noFun, cofix_funs) - | _ -> attribute_error ())) - | "MUTCASE" -> - (match pop_cics ctxt with - | patternsType :: inductiveTerm :: patterns -> - push ctxt (Cic_term - (match pop_tag_attrs ctxt with - | ["id", id; "noType", noType; "uriType", uriType] - | ["id", id; "noType", noType; "sort", _; "uriType", uriType] -> - Cic.AMutCase (id, uri_of_string uriType, int_of_string noType, - patternsType, inductiveTerm, patterns) - | _ -> attribute_error ())) - | _ -> parse_error "invalid \"MUTCASE\" content") - | "Constructor" -> - let typ = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["name", name] -> Constructor (name, typ) - | _ -> attribute_error ()) - | "InductiveType" -> - let constructors = pop_constructors ctxt in - let arity = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "inductive", inductive; "name", name] -> - Inductive_type (id, name, bool_of_string inductive, arity, - constructors) - | _ -> attribute_error ()) - | "InductiveDefinition" -> - let inductive_types = pop_inductive_types ctxt in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt (Cic_obj - (match pop_tag_attrs ctxt with - | ["id", id; "noParams", noParams; "params", params] -> - Cic.AInductiveDefinition (id, inductive_types, - uri_list_of_string params, int_of_string noParams, obj_attributes) - | _ -> attribute_error ())) - | "ConstantType" -> - let typ = pop_cic ctxt in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["id", id; "name", name; "params", params] -> - Cic_constant_type (id, name, uri_list_of_string params, typ, - obj_attributes) - | _ -> attribute_error ()) - | "ConstantBody" -> - let body = pop_cic ctxt in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["for", for_; "id", id; "params", params] -> - Cic_constant_body (id, for_, uri_list_of_string params, body, - obj_attributes) - | _ -> attribute_error ()) - | "Variable" -> - let typ = pop_cic ctxt in - let body = - match pop_cics ctxt with - | [] -> None - | [t] -> Some t - | _ -> parse_error "wrong content for \"Variable\"" - in - let obj_attributes = pop_obj_attributes ctxt in - push ctxt (Cic_obj - (match pop_tag_attrs ctxt with - | ["id", id; "name", name; "params", params] -> - Cic.AVariable (id, name, body, typ, uri_list_of_string params, - obj_attributes) - | _ -> attribute_error ())) - | "arg" -> - let term = pop_cic ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["relUri", relUri] -> Arg (relUri, term) - | _ -> attribute_error ()) - | "instantiate" -> - (* explicit named substitution handling: when the end tag of an element - * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it - * is stored on the stack with no substitutions (i.e. []). When the end - * tag of an "instantiate" element is found we patch the term currently - * on the stack with the substitution built from "instantiate" children - *) - (* XXX inefficiency here: first travels the elements in order to - * find the baseUri, then in order to build the explicit named subst *) - let base_uri = find_base_uri ctxt in - let subst = pop_subst ctxt base_uri in - let term = pop_cic ctxt in - (* comment from CicParser3.ml: - * CSC: the "id" optional attribute should be parsed and reflected in - * Cic.annterm and id = string_of_xml_attr (n#attribute "id") *) - (* replace *) - set_top ctxt (Cic_term (patch_subst ctxt subst term)) - | "attributes" -> - let rec aux acc = function (* retrieve object attributes *) - | Obj_class c :: tl -> aux (`Class c :: acc) tl - | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl - | Obj_generated :: tl -> aux (`Generated :: acc) tl - | tl -> acc, tl - in - let obj_attrs, new_stack = aux [] ctxt.stack in - ctxt.stack <- new_stack; - set_top ctxt (Cic_attributes obj_attrs) - | "generated" -> set_top ctxt Obj_generated - | "field" -> - push ctxt - (match pop_tag_attrs ctxt with - | ["name", name] -> Obj_field name - | _ -> attribute_error ()) - | "flavour" -> - push ctxt - (match pop_tag_attrs ctxt with - | [ "value", "definition"] -> Obj_flavour `Definition - | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition - | [ "value", "fact"] -> Obj_flavour `Fact - | [ "value", "lemma"] -> Obj_flavour `Lemma - | [ "value", "remark"] -> Obj_flavour `Remark - | [ "value", "theorem"] -> Obj_flavour `Theorem - | [ "value", "variant"] -> Obj_flavour `Variant - | [ "value", "axiom"] -> Obj_flavour `Axiom - | _ -> attribute_error ()) - | "class" -> - let class_modifiers = pop_class_modifiers ctxt in - push ctxt - (match pop_tag_attrs ctxt with - | ["value", "elim"] -> - (match class_modifiers with - | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort) - | _ -> - parse_error - "unexpected extra content for \"elim\" object class") - | ["value", "record"] -> - let fields = - List.map - (function - | Obj_field name -> - (match Str.split (Str.regexp " ") name with - | [name] -> name, false, 0 - | [name;"coercion"] -> name,true,0 - | [name;"coercion"; n] -> - let n = - try int_of_string n - with Failure _ -> - parse_error "int expected after \"coercion\"" - in - name,true,n - | _ -> - parse_error - "wrong \"field\"'s name attribute") - | _ -> - parse_error - "unexpected extra content for \"record\" object class") - class_modifiers - in - Obj_class (`Record fields) - | ["value", "projection"] -> Obj_class `Projection - | ["value", "inversion"] -> Obj_class `InversionPrinciple - | _ -> attribute_error ()) - | tag -> - match find_helm_exception ctxt with - | Some (exn, arg) -> raise (Getter_failure (exn, arg)) - | None -> parse_error (sprintf "unknown element \"%s\"" tag) - -(** {2 Parser internals} *) - -let has_gz_suffix fname = - try - let idx = String.rindex fname '.' in - let suffix = String.sub fname idx (String.length fname - idx) in - suffix = ".gz" - with Not_found -> false - -let parse uri filename = - let ctxt = new_parser_context uri in - ctxt.filename <- filename; - let module P = XmlPushParser in - let callbacks = { - P.default_callbacks with - P.start_element = Some (start_element ctxt); - P.end_element = Some (end_element ctxt); - } in - let xml_parser = P.create_parser callbacks in - ctxt.xml_parser <- Some xml_parser; - try - (try - let xml_source = - if has_gz_suffix filename then `Gzip_file filename - else `File filename - in - P.parse xml_parser xml_source - with exn -> - ctxt.xml_parser <- None; - (* ZACK: the above "<- None" is vital for garbage collection. Without it - * we keep in memory a circular structure parser -> callbacks -> ctxt -> - * parser. I don't know if the ocaml garbage collector is supposed to - * collect such structures, but for sure the expat bindings will (orribly) - * leak when used in conjunction with such structures *) - raise exn); - ctxt.xml_parser <- None; (* ZACK: same comment as above *) -(* debug_print (lazy (string_of_stack stack));*) - (* assert (List.length ctxt.stack = 1) *) - List.hd ctxt.stack - with - | Failure "int_of_string" -> parse_error ctxt "integer number expected" - | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected" - | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg) - | Sys.Break - | Parser_failure _ - | Getter_failure _ as exn -> - raise exn - | exn -> - raise (Parser_failure ("CicParser: uncaught exception: " ^ Printexc.to_string exn)) - -(** {2 API implementation} *) - -let annobj_of_xml uri filename filenamebody = - match filenamebody with - | None -> - (match parse uri filename with - | Cic_constant_type (id, name, params, typ, obj_attributes) -> - Cic.AConstant (id, None, name, None, typ, params, obj_attributes) - | Cic_obj obj -> obj - | _ -> raise (Parser_failure ("no object found in " ^ filename))) - | Some filenamebody -> - (match parse uri filename, parse uri filenamebody with - | Cic_constant_type (type_id, name, params, typ, obj_attributes), - Cic_constant_body (body_id, _, _, body, _) -> - Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,obj_attributes) - | _ -> - raise (Parser_failure (sprintf "no constant found in %s, %s" - filename filenamebody))) - -let obj_of_xml uri filename filenamebody = - Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody) diff --git a/matita/components/cic/cicParser.mli b/matita/components/cic/cicParser.mli deleted file mode 100644 index d874293a1..000000000 --- a/matita/components/cic/cicParser.mli +++ /dev/null @@ -1,47 +0,0 @@ -(* Copyright (C) 2000-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/. - *) - - (** raised for exception received by the getter (i.e. embedded in the source - * XML document). Arguments are values of "helm:exception" and - * "helm:exception_arg" attributes *) -exception Getter_failure of string * string - - (** generic parser failure *) -exception Parser_failure of string - - (* given the filename of an xml file of a cic object, it returns - * its internal annotated representation. In the case of constants (whose - * type is splitted from the body), a second xml file (for the body) must be - * provided. - * Both files are assumed to be gzipped. *) -val annobj_of_xml: UriManager.uri -> string -> string option -> Cic.annobj - - (* given the filename of an xml file of a cic object, it returns its internal - * logical representation. In the case of constants (whose type is splitted - * from the body), a second xml file (for the body) must be provided. - * Both files are assumed to be gzipped. *) -val obj_of_xml : UriManager.uri -> string -> string option -> Cic.obj - -val impredicative_set : bool ref diff --git a/matita/components/cic/cic_indexable.ml b/matita/components/cic/cic_indexable.ml deleted file mode 100644 index 7e98b8c5e..000000000 --- a/matita/components/cic/cic_indexable.ml +++ /dev/null @@ -1,81 +0,0 @@ -(* 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: discrimination_tree.ml 8991 2008-09-19 12:47:23Z tassi $ *) - -module CicIndexable : Discrimination_tree.Indexable -with type input = Cic.term and type constant_name = UriManager.uri -= struct - - type input = Cic.term - type constant_name = UriManager.uri - open Discrimination_tree - - let ppelem = function - | Constant (uri,arity) -> - "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")" - | Bound (i,arity) -> - "("^string_of_int i ^ "," ^ string_of_int arity^")" - | Variable -> "?" - | Proposition -> "Prop" - | Datatype -> "Type" - | Dead -> "Dead" - ;; - - let path_string_of = - let rec aux arity = function - | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable] - | Cic.Appl (Cic.Lambda _ :: _) -> - [Variable] (* maybe we should b-reduce *) - | Cic.Appl [] -> assert false - | Cic.Appl (hd::tl) -> - aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) - | Cic.Cast (t,_) -> aux arity t - | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable] - (* I think we should CicSubstitution.subst Implicit t *) - | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *) - | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable] - | Cic.Rel i -> [Bound (i, arity)] - | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition] - | Cic.Sort _ -> assert (arity=0); [Datatype] - | Cic.Const _ | Cic.Var _ - | Cic.MutInd _ | Cic.MutConstruct _ as t -> - [Constant (CicUtil.uri_of_term t, arity)] - | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead] - in - aux 0 - ;; - - let compare e1 e2 = - match e1,e2 with - | Constant (u1,a1),Constant (u2,a2) -> - let x = UriManager.compare u1 u2 in - if x = 0 then Pervasives.compare a1 a2 else x - | e1,e2 -> Pervasives.compare e1 e2 - ;; - - let string_of_path l = String.concat "." (List.map ppelem l) ;; -end - diff --git a/matita/components/cic/cic_indexable.mli b/matita/components/cic/cic_indexable.mli deleted file mode 100644 index fc1f73fbb..000000000 --- a/matita/components/cic/cic_indexable.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* 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/. - *) - - -module CicIndexable : Discrimination_tree.Indexable -with type input = Cic.term and type constant_name = UriManager.uri - diff --git a/matita/components/cic/deannotate.ml b/matita/components/cic/deannotate.ml deleted file mode 100644 index c560af569..000000000 --- a/matita/components/cic/deannotate.ml +++ /dev/null @@ -1,225 +0,0 @@ -(* 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/. - *) - -(* $Id$ *) - -(* converts annotated terms into cic terms (forgetting ids and names) *) -let rec deannotate_term = - let module C = Cic in - function - C.ARel (_,_,n,_) -> C.Rel n - | C.AVar (_,uri,exp_named_subst) -> - let deann_exp_named_subst = - List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst - in - C.Var (uri, deann_exp_named_subst) - | C.AMeta (_,n, l) -> - let l' = - List.map - (function - None -> None - | Some at -> Some (deannotate_term at) - ) l - in - C.Meta (n, l') - | C.ASort (_,s) -> C.Sort s - | C.AImplicit (_, annotation) -> C.Implicit annotation - | C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) - | C.AProd (_,name,so,ta) -> - C.Prod (name, deannotate_term so, deannotate_term ta) - | C.ALambda (_,name,so,ta) -> - C.Lambda (name, deannotate_term so, deannotate_term ta) - | C.ALetIn (_,name,so,ty,ta) -> - C.LetIn (name, deannotate_term so, deannotate_term ty, deannotate_term ta) - | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l) - | C.AConst (_,uri,exp_named_subst) -> - let deann_exp_named_subst = - List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst - in - C.Const (uri, deann_exp_named_subst) - | C.AMutInd (_,uri,i,exp_named_subst) -> - let deann_exp_named_subst = - List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst - in - C.MutInd (uri,i,deann_exp_named_subst) - | C.AMutConstruct (_,uri,i,j,exp_named_subst) -> - let deann_exp_named_subst = - List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst - in - C.MutConstruct (uri,i,j,deann_exp_named_subst) - | C.AMutCase (_,uri,i,outtype,te,pl) -> - C.MutCase (uri,i,deannotate_term outtype, - deannotate_term te, List.map deannotate_term pl) - | C.AFix (_,funno,ifl) -> - C.Fix (funno, List.map deannotate_inductiveFun ifl) - | C.ACoFix (_,funno,ifl) -> - C.CoFix (funno, List.map deannotate_coinductiveFun ifl) - -and deannotate_inductiveFun (_,name,index,ty,bo) = - (name, index, deannotate_term ty, deannotate_term bo) - -and deannotate_coinductiveFun (_,name,ty,bo) = - (name, deannotate_term ty, deannotate_term bo) -;; - -let deannotate_inductiveType (_, name, isinductive, arity, cons) = - (name, isinductive, deannotate_term arity, - List.map (fun (id,ty) -> (id,deannotate_term ty)) cons) -;; - -let deannotate_conjectures = - let module C = Cic in - List.map - (function - (_,id,acontext,con) -> - let context = - List.map - (function - | _,Some (n,(C.ADef (ate,aty))) -> - Some(n,(C.Def(deannotate_term ate,deannotate_term aty))) - | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at))) - | _,None -> None) - acontext - in - (id,context,deannotate_term con)) -;; - -let type_of_aux' = ref (fun _ _ -> assert false);; -let lift = ref (fun _ _ -> assert false);; - -let rec compute_letin_type context te = - let module C = Cic in - match te with - C.Rel _ - | C.Sort _ -> te - | C.Implicit _ -> assert false - | C.Meta (n,l) -> - C.Meta (n, - List.map - (fun x -> - match x with - None -> None - | Some x -> Some (compute_letin_type context x)) l) - | C.Cast (te,ty) -> - C.Cast - (compute_letin_type context te, - compute_letin_type context ty) - | C.Prod (name,so,dest) -> - let so = compute_letin_type context so in - C.Prod (name, so, - compute_letin_type ((Some (name,(C.Decl so)))::context) dest) - | C.Lambda (name,so,dest) -> - let so = compute_letin_type context so in - C.Lambda (name, so, - compute_letin_type ((Some (name,(C.Decl so)))::context) dest) - | C.LetIn (name,so,C.Implicit _,dest) -> - let so = compute_letin_type context so in - let ty = Unshare.unshare ~fresh_univs:true (!type_of_aux' context so) in - C.LetIn (name, so, ty, - compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest) - | C.LetIn (name,so,ty,dest) -> - let so = compute_letin_type context so in - let ty = compute_letin_type context ty in - C.LetIn (name, so, ty, - compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest) - | C.Appl l -> - C.Appl (List.map (fun x -> compute_letin_type context x) l) - | C.Var (uri,exp_named_subst) -> - C.Var (uri, - List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) - | C.Const (uri,exp_named_subst) -> - C.Const (uri, - List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) - | C.MutInd (uri,i,exp_named_subst) -> - C.MutInd (uri,i, - List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - C.MutConstruct (uri,i,j, - List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) - | C.MutCase (uri,i,out,te,pl) -> - C.MutCase (uri,i, - compute_letin_type context out, - compute_letin_type context te, - List.map (fun x -> compute_letin_type context x) pl) - | C.Fix (fno,fl) -> - let fl = - List.map - (function (name,recno,ty,bo) -> - name,recno,compute_letin_type context ty, bo) fl in - let tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (!lift len ty)))::types, - len+1) - ) ([],0) fl - in - C.Fix (fno, - List.map - (fun (name,recno,ty,bo) -> - name, recno, ty, compute_letin_type (tys @ context) bo - ) fl) - | C.CoFix (fno,fl) -> - let fl = - List.map - (function (name,ty,bo) -> - name, compute_letin_type context ty, bo) fl in - let tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (!lift len ty)))::types, - len+1) - ) ([],0) fl - in - C.CoFix (fno, - List.map - (fun (name,ty,bo) -> - name, ty, compute_letin_type (tys @ context) bo - ) fl) -;; - -let deannotate_obj = - let deannotate_term t = - compute_letin_type [] (deannotate_term t) - in - let module C = Cic in - function - C.AConstant (_, _, id, bo, ty, params, attrs) -> - C.Constant (id, - (match bo with None -> None | Some bo -> Some (deannotate_term bo)), - deannotate_term ty, params, attrs) - | C.AVariable (_, name, bo, ty, params, attrs) -> - C.Variable (name, - (match bo with None -> None | Some bo -> Some (deannotate_term bo)), - deannotate_term ty, params, attrs) - | C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) -> - C.CurrentProof ( - name, - deannotate_conjectures conjs, - deannotate_term bo,deannotate_term ty, params, attrs - ) - | C.AInductiveDefinition (_, tys, params, parno, attrs) -> - C.InductiveDefinition (List.map deannotate_inductiveType tys, - params, parno, attrs) -;; diff --git a/matita/components/cic/deannotate.mli b/matita/components/cic/deannotate.mli deleted file mode 100644 index f4fdd2d5d..000000000 --- a/matita/components/cic/deannotate.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* 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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(******************************************************************************) - -val type_of_aux' : (Cic.context -> Cic.term -> Cic.term) ref -val lift : (int -> Cic.term -> Cic.term) ref - -val deannotate_term : Cic.annterm -> Cic.term -val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv -val deannotate_obj : Cic.annobj -> Cic.obj diff --git a/matita/components/cic/helmLibraryObjects.ml b/matita/components/cic/helmLibraryObjects.ml deleted file mode 100644 index 3038582ab..000000000 --- a/matita/components/cic/helmLibraryObjects.ml +++ /dev/null @@ -1,230 +0,0 @@ -(* 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 - -let const ?(subst = []) uri = Cic.Const (uri, subst) -let var ?(subst = []) uri = Cic.Var (uri, subst) -let mutconstruct ?(subst = []) uri typeno consno = - Cic.MutConstruct (uri, typeno, consno, subst) -let mutind ?(subst = []) uri typeno = Cic.MutInd (uri, typeno, subst) - -let indtyuri_of_uri uri = - let index_sharp = String.index uri '#' in - let index_num = index_sharp + 3 in - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1) - -let indconuri_of_uri uri = - let index_sharp = String.index uri '#' in - let index_div = String.rindex uri '/' in - let index_con = index_div + 1 in - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string - (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1, - int_of_string - (String.sub uri index_con (String.length uri - index_con))) - -(** {2 Helm's objects shorthands} *) - -module Logic = - struct - let eq_SURI = "cic:/Coq/Init/Logic/eq.ind" - let eq_URI = uri eq_SURI - let eq_XURI = eq_SURI ^ "#xpointer(1/1)" - let eq_ind_URI = uri "cic:/Coq/Init/Logic/eq_ind.con" - let eq_ind_r_URI = uri "cic:/Coq/Init/Logic/eq_ind_r.con" - let true_URI = uri "cic:/Coq/Init/Logic/True.ind" - let false_URI = uri "cic:/Coq/Init/Logic/False.ind" - let false_ind_URI = uri "cic:/Coq/Init/Logic/False_ind.con" - let ex_SURI = "cic:/Coq/Init/Logic/ex.ind" - let ex_URI = uri ex_SURI - let ex_XURI = ex_SURI ^ "#xpointer(1/1)" - let ex_ind_URI = uri "cic:/Coq/Init/Logic/ex_ind.con" - let and_SURI = "cic:/Coq/Init/Logic/and.ind" - let and_URI = uri and_SURI - let and_XURI = and_SURI ^ "#xpointer(1/1)" - let and_ind_URI = uri "cic:/Coq/Init/Logic/and_ind.con" - let or_SURI = "cic:/Coq/Init/Logic/or.ind" - let or_URI = uri or_SURI - let or_XURI = or_SURI ^ "#xpointer(1/1)" - let not_SURI = "cic:/Coq/Init/Logic/not.con" - let not_URI = uri not_SURI - let iff_SURI = "cic:/Coq/Init/Logic/iff.con" - let iff_URI = uri "cic:/Coq/Init/Logic/iff.con" - let sym_eq_URI = uri "cic:/Coq/Init/Logic/sym_eq.con" - let trans_eq_URI = uri "cic:/Coq/Init/Logic/trans_eq.con" - let absurd_URI = uri "cic:/Coq/Init/Logic/absurd.con" - end - -module Datatypes = - struct - let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind" - let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind" - - let trueb = mutconstruct bool_URI 0 1 - let falseb = mutconstruct bool_URI 0 2 - let zero = mutconstruct nat_URI 0 1 - let succ = mutconstruct nat_URI 0 2 - end - -module Reals = - struct - let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con" - let rplus_SURI = "cic:/Coq/Reals/Rdefinitions/Rplus.con" - let rplus_URI = uri rplus_SURI - let rminus_SURI = "cic:/Coq/Reals/Rdefinitions/Rminus.con" - let rminus_URI = uri rminus_SURI - let rmult_SURI = "cic:/Coq/Reals/Rdefinitions/Rmult.con" - let rmult_URI = uri rmult_SURI - let rdiv_SURI = "cic:/Coq/Reals/Rdefinitions/Rdiv.con" - let rdiv_URI = uri rdiv_SURI - let ropp_SURI = "cic:/Coq/Reals/Rdefinitions/Ropp.con" - let ropp_URI = uri ropp_SURI - let rinv_SURI = "cic:/Coq/Reals/Rdefinitions/Rinv.con" - let rinv_URI = uri rinv_SURI - let r0_SURI = "cic:/Coq/Reals/Rdefinitions/R0.con" - let r0_URI = uri r0_SURI - let r1_SURI = "cic:/Coq/Reals/Rdefinitions/R1.con" - let r1_URI = uri r1_SURI - let rle_SURI = "cic:/Coq/Reals/Rdefinitions/Rle.con" - let rle_URI = uri rle_SURI - let rge_SURI = "cic:/Coq/Reals/Rdefinitions/Rge.con" - let rge_URI = uri rge_SURI - let rlt_SURI = "cic:/Coq/Reals/Rdefinitions/Rlt.con" - let rlt_URI = uri rlt_SURI - let rgt_SURI = "cic:/Coq/Reals/Rdefinitions/Rgt.con" - let rgt_URI = uri rgt_SURI - let rtheory_URI = uri "cic:/Coq/Reals/RIneq/RTheory.con" - let rinv_r1_URI = uri "cic:/Coq/Reals/RIneq/Rinv_1.con" - let pow_URI = uri "cic:/Coq/Reals/Rfunctions/pow.con" - - let r = const r_URI - let rplus = const rplus_URI - let rmult = const rmult_URI - let ropp = const ropp_URI - let r0 = const r0_URI - let r1 = const r1_URI - let rtheory = const rtheory_URI - end - -module Peano = - struct - let plus_SURI = "cic:/Coq/Init/Peano/plus.con" - let plus_URI = uri plus_SURI - let minus_SURI = "cic:/Coq/Init/Peano/minus.con" - let minus_URI = uri minus_SURI - let mult_SURI = "cic:/Coq/Init/Peano/mult.con" - let mult_URI = uri mult_SURI - let pred_URI = uri "cic:/Coq/Init/Peano/pred.con" - let le_SURI = "cic:/Coq/Init/Peano/le.ind" - let le_URI = uri le_SURI - let le_XURI = le_SURI ^ "#xpointer(1/1)" - let ge_SURI = "cic:/Coq/Init/Peano/ge.con" - let ge_URI = uri ge_SURI - let lt_SURI = "cic:/Coq/Init/Peano/lt.con" - let lt_URI = uri lt_SURI - let gt_SURI = "cic:/Coq/Init/Peano/gt.con" - let gt_URI = uri gt_SURI - - let plus = const plus_URI - let mult = const mult_URI - let pred = const pred_URI - end - -module BinPos = - struct - let positive_SURI = "cic:/Coq/NArith/BinPos/positive.ind" - let positive_URI = uri positive_SURI - let xI = mutconstruct positive_URI 0 1 - let xO = mutconstruct positive_URI 0 2 - let xH = mutconstruct positive_URI 0 3 - let pplus_SURI = "cic:/Coq/NArith/BinPos/Pplus.con" - let pplus_URI = uri pplus_SURI - let pplus = const pplus_URI - let pminus_SURI = "cic:/Coq/NArith/BinPos/Pminus.con" - let pminus_URI = uri pminus_SURI - let pminus = const pminus_URI - let pmult_SURI = "cic:/Coq/NArith/BinPos/Pmult.con" - let pmult_URI = uri pmult_SURI - let pmult = const pmult_URI - end - -module BinInt = - struct - let zmult_URI = uri "cic:/Coq/ZArith/BinInt/Zmult.con" - let zmult = const zmult_URI - let zplus_SURI = "cic:/Coq/ZArith/BinInt/Zplus.con" - let zplus_URI = uri zplus_SURI - let zplus = const zplus_URI - let zminus_SURI = "cic:/Coq/ZArith/BinInt/Zminus.con" - let zminus_URI = uri zminus_SURI - let zminus = const zminus_URI - let z_SURI = "cic:/Coq/ZArith/BinInt/Z.ind" - let z_URI = uri z_SURI - let z0 = mutconstruct z_URI 0 1 - let zpos = mutconstruct z_URI 0 2 - let zneg = mutconstruct z_URI 0 3 - let zopp_SURI = "cic:/Coq/ZArith/BinInt/Zopp.con" - let zopp_URI = uri zopp_SURI - let zopp = const zopp_URI - let zpower_URI = uri "cic:/Coq/ZArith/Zpower/Zpower.con" - end - -(** {2 Helpers for creating common terms} - * (e.g. numbers)} *) - -exception NegativeInteger - -let build_nat n = - if n < 0 then raise NegativeInteger; - let rec aux = function - | 0 -> Datatypes.zero - | n -> Cic.Appl [ Datatypes.succ; (aux (n - 1)) ] - in - aux n - -let build_real n = - if n < 0 then raise NegativeInteger; - let rec aux = function - | 0 -> Reals.r0 - | 1 -> Reals.r1 (* to avoid trailing "+ 0" *) - | n -> Cic.Appl [ Reals.rplus; Reals.r1; (aux (n - 1)) ] - in - aux n - -let build_bin_pos n = - if n < 1 then raise NegativeInteger; - let rec aux = function - | 1 -> BinPos.xH - | n when n mod 2 = 0 -> Cic.Appl [ BinPos.xO; aux (n / 2) ] - | n -> Cic.Appl [ BinPos.xI; aux (n / 2) ] - in - aux n - diff --git a/matita/components/cic/helmLibraryObjects.mli b/matita/components/cic/helmLibraryObjects.mli deleted file mode 100644 index 677879899..000000000 --- a/matita/components/cic/helmLibraryObjects.mli +++ /dev/null @@ -1,182 +0,0 @@ -(* Copyright (C) 2004, 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://helm.cs.unibo.it/ - *) - -module Logic : - sig - val absurd_URI : UriManager.uri - val and_ind_URI : UriManager.uri - val and_URI : UriManager.uri - val eq_ind_r_URI : UriManager.uri - val eq_ind_URI : UriManager.uri - val eq_URI : UriManager.uri - val ex_ind_URI : UriManager.uri - val ex_URI : UriManager.uri - val false_ind_URI : UriManager.uri - val false_URI : UriManager.uri - val iff_URI : UriManager.uri - val not_URI : UriManager.uri - val or_URI : UriManager.uri - val sym_eq_URI : UriManager.uri - val trans_eq_URI : UriManager.uri - val true_URI : UriManager.uri - - val and_SURI : string - val eq_SURI : string - val ex_SURI : string - val iff_SURI : string - val not_SURI : string - val or_SURI : string - - val and_XURI : string - val eq_XURI : string - val ex_XURI : string - val or_XURI : string - end - -module Datatypes : - sig - val bool_URI : UriManager.uri - val nat_URI : UriManager.uri - - val trueb : Cic.term - val falseb : Cic.term - val zero : Cic.term - val succ : Cic.term - end - -module Reals : - sig - val pow_URI : UriManager.uri - val r0_URI : UriManager.uri - val r1_URI : UriManager.uri - val rdiv_URI : UriManager.uri - val rge_URI : UriManager.uri - val rgt_URI : UriManager.uri - val rinv_r1_URI : UriManager.uri - val rinv_URI : UriManager.uri - val rle_URI : UriManager.uri - val rlt_URI : UriManager.uri - val rminus_URI : UriManager.uri - val rmult_URI : UriManager.uri - val ropp_URI : UriManager.uri - val rplus_URI : UriManager.uri - val rtheory_URI : UriManager.uri - val r_URI : UriManager.uri - - val r0_SURI : string - val r1_SURI : string - val rdiv_SURI : string - val rge_SURI : string - val rgt_SURI : string - val rinv_SURI : string - val rle_SURI : string - val rlt_SURI : string - val rminus_SURI : string - val rmult_SURI : string - val ropp_SURI : string - val rplus_SURI : string - - val r0 : Cic.term - val r1 : Cic.term - val r : Cic.term - val rmult : Cic.term - val ropp : Cic.term - val rplus : Cic.term - val rtheory : Cic.term - end - -module Peano : - sig - val ge_URI : UriManager.uri - val gt_URI : UriManager.uri - val le_URI : UriManager.uri - val lt_URI : UriManager.uri - val minus_URI : UriManager.uri - val mult_URI : UriManager.uri - val plus_URI : UriManager.uri - val pred_URI : UriManager.uri - - val ge_SURI : string - val gt_SURI : string - val le_SURI : string - val lt_SURI : string - val minus_SURI : string - val mult_SURI : string - val plus_SURI : string - - val le_XURI : string - - val mult : Cic.term - val plus : Cic.term - val pred : Cic.term - end - -module BinPos : - sig - val pminus_URI : UriManager.uri - val pmult_URI : UriManager.uri - val positive_URI : UriManager.uri - val pplus_URI : UriManager.uri - - val pminus_SURI : string - val pmult_SURI : string - val positive_SURI : string - val pplus_SURI : string - - val pminus : Cic.term - val pmult : Cic.term - val pplus : Cic.term - val xH : Cic.term - val xI : Cic.term - val xO : Cic.term - end - -module BinInt : - sig - val zminus_URI : UriManager.uri - val zmult_URI : UriManager.uri - val zopp_URI : UriManager.uri - val zplus_URI : UriManager.uri - val zpower_URI : UriManager.uri - val z_URI : UriManager.uri - - val zminus_SURI : string - val zopp_SURI : string - val zplus_SURI : string - val z_SURI : string - - val z0 : Cic.term - val zminus : Cic.term - val zmult : Cic.term - val zneg : Cic.term - val zopp : Cic.term - val zplus : Cic.term - val zpos : Cic.term - end - -val build_bin_pos : int -> Cic.term -val build_nat : int -> Cic.term -val build_real : int -> Cic.term - diff --git a/matita/components/cic/libraryObjects.ml b/matita/components/cic/libraryObjects.ml deleted file mode 100644 index c523a60de..000000000 --- a/matita/components/cic/libraryObjects.ml +++ /dev/null @@ -1,227 +0,0 @@ -(* 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -(**** TABLES ****) - -let default_eq_URIs = [] -let default_true_URIs = [] -let default_false_URIs = [] -let default_absurd_URIs = [] -let default_nat_URIs = [] - -(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *) -let eq_URIs_ref = ref default_eq_URIs;; - -let true_URIs_ref = ref default_true_URIs -let false_URIs_ref = ref default_false_URIs -let absurd_URIs_ref = ref default_absurd_URIs -let nat_URIs_ref = ref default_nat_URIs - - -(**** SET_DEFAULT ****) - -exception NotRecognized of string;; - -(* insert an element in front of the list, removing from the list all the - previous elements with the same key associated *) -let insert_unique e extract l = - let uri = extract e in - let l' = - List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l - in - e :: l' - -let set_default what l = - match what,l with - "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI; - eq_ind_r_URI;eq_rec_URI;eq_rec_r_URI;eq_rect_URI; - eq_rect_r_URI;eq_f_URI;eq_f_sym_URI] -> - eq_URIs_ref := - insert_unique - (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI, - eq_ind_r_URI,eq_rec_URI,eq_rec_r_URI,eq_rect_URI, - eq_rect_r_URI,eq_f_URI,eq_f_sym_URI) - (fun x,_,_,_,_,_,_,_,_,_,_ -> x) !eq_URIs_ref - | "true",[true_URI] -> - true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref - | "false",[false_URI] -> - false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref - | "absurd",[absurd_URI] -> - absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref - | "natural numbers",[nat_URI] -> - nat_URIs_ref := insert_unique nat_URI (fun x -> x) !nat_URIs_ref - | _,l -> - raise - (NotRecognized (what^" with "^string_of_int(List.length l)^" params")) -;; - -let reset_defaults () = - eq_URIs_ref := default_eq_URIs; - true_URIs_ref := default_true_URIs; - false_URIs_ref := default_false_URIs; - absurd_URIs_ref := default_absurd_URIs; - nat_URIs_ref := default_nat_URIs -;; - -let stack = ref [];; - -let push () = - stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref, - !nat_URIs_ref - )::!stack; - reset_defaults () -;; - -let pop () = - match !stack with - | [] -> raise (Failure "Unable to POP in libraryObjects.ml") - | (eq,t,f,a,n)::tl -> - stack := tl; - eq_URIs_ref := eq; - true_URIs_ref := t; - false_URIs_ref := f; - absurd_URIs_ref := a; - nat_URIs_ref := n -;; - -(**** LOOKUP FUNCTIONS ****) -let eq_URI () = - try let eq,_,_,_,_,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq - with Failure "hd" -> None - -let is_eq_URI uri = - List.exists (fun (eq,_,_,_,_,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref - -let is_eq_refl_URI uri = - let urieq = UriManager.strip_xpointer uri in - is_eq_URI urieq && - not (UriManager.eq urieq uri) -;; - -let is_eq_ind_URI uri = - List.exists (fun (_,_,_,eq_ind,_,_,_,_,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref -let is_eq_ind_r_URI uri = - List.exists (fun (_,_,_,_,eq_ind_r,_,_,_,_,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref -let is_eq_rec_URI uri = - List.exists (fun (_,_,_,_,_,eq_rec,_,_,_,_,_) -> UriManager.eq eq_rec uri) !eq_URIs_ref -let is_eq_rec_r_URI uri = - List.exists (fun (_,_,_,_,_,_,eq_rec_r,_,_,_,_) -> UriManager.eq eq_rec_r uri) !eq_URIs_ref -let is_eq_rect_URI uri = - List.exists (fun (_,_,_,_,_,_,_,eq_rect,_,_,_) -> UriManager.eq eq_rect uri) !eq_URIs_ref -let is_eq_rect_r_URI uri = - List.exists (fun (_,_,_,_,_,_,_,_,eq_rect_r,_,_) -> UriManager.eq eq_rect_r uri) !eq_URIs_ref -let is_trans_eq_URI uri = - List.exists (fun (_,_,trans_eq,_,_,_,_,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref -let is_sym_eq_URI uri = - List.exists (fun (_,sym_eq,_,_,_,_,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref -let is_eq_f_URI uri = - List.exists (fun (_,_,_,_,_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref -let is_eq_f_sym_URI uri = - List.exists (fun (_,_,_,_,_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref - -let in_eq_URIs uri = - is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri || - is_eq_ind_r_URI uri || is_eq_rec_URI uri || is_eq_rec_r_URI uri || - is_eq_rect_URI uri || is_eq_rect_r_URI uri || - is_trans_eq_URI uri || is_sym_eq_URI uri || is_eq_f_URI uri || - is_eq_f_sym_URI uri - - - -let eq_refl_URI ~eq:uri = - let uri = UriManager.strip_xpointer uri in - UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)") - -let sym_eq_URI ~eq:uri = - try - let _,x,_,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let trans_eq_URI ~eq:uri = - try - let _,_,x,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_ind_URI ~eq:uri = - try - let _,_,_,x,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_ind_r_URI ~eq:uri = - try - let _,_,_,_,x,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_rec_URI ~eq:uri = - try - let _,_,_,_,_,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_rec_r_URI ~eq:uri = - try - let _,_,_,_,_,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_rect_URI ~eq:uri = - try - let _,_,_,_,_,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_rect_r_URI ~eq:uri = - try - let _,_,_,_,_,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_f_URI ~eq:uri = - try - let _,_,_,_,_,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - -let eq_f_sym_URI ~eq:uri = - try - let _,_,_,_,_,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) - - -let eq_URI_of_eq_f_URI eq_f_URI = - try - let x,_,_,_,_,_,_,_,_,_,_ = - List.find (fun _,_,_,_,_,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref - in x - with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI)) - -let true_URI () = - try Some (List.hd !true_URIs_ref) with Failure "hd" -> None -let false_URI () = - try Some (List.hd !false_URIs_ref) with Failure "hd" -> None -let absurd_URI () = - try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None - -let nat_URI () = - try Some (List.hd !nat_URIs_ref) with Failure "hd" -> None -let is_nat_URI uri = - List.exists (fun nat -> UriManager.eq nat uri) !nat_URIs_ref diff --git a/matita/components/cic/libraryObjects.mli b/matita/components/cic/libraryObjects.mli deleted file mode 100644 index 248893002..000000000 --- a/matita/components/cic/libraryObjects.mli +++ /dev/null @@ -1,70 +0,0 @@ -(* 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://helm.cs.unibo.it/ - *) - -val set_default : string -> UriManager.uri list -> unit - -val reset_defaults : unit -> unit -val push: unit -> unit -val pop: unit -> unit - -val eq_URI : unit -> UriManager.uri option - -val is_eq_URI : UriManager.uri -> bool -val is_eq_refl_URI : UriManager.uri -> bool -val is_eq_ind_URI : UriManager.uri -> bool -val is_eq_ind_r_URI : UriManager.uri -> bool -val is_eq_rec_URI : UriManager.uri -> bool -val is_eq_rec_r_URI : UriManager.uri -> bool -val is_eq_rect_URI : UriManager.uri -> bool -val is_eq_rect_r_URI : UriManager.uri -> bool -val is_trans_eq_URI : UriManager.uri -> bool -val is_sym_eq_URI : UriManager.uri -> bool -val is_eq_f_URI : UriManager.uri -> bool -val is_eq_f_sym_URI : UriManager.uri -> bool -val in_eq_URIs : UriManager.uri -> bool - -val eq_URI_of_eq_f_URI : UriManager.uri -> UriManager.uri - -exception NotRecognized of string;; - -val eq_refl_URI : eq:UriManager.uri -> UriManager.uri -val eq_ind_URI : eq:UriManager.uri -> UriManager.uri -val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri -val eq_rec_URI : eq:UriManager.uri -> UriManager.uri -val eq_rec_r_URI : eq:UriManager.uri -> UriManager.uri -val eq_rect_URI : eq:UriManager.uri -> UriManager.uri -val eq_rect_r_URI : eq:UriManager.uri -> UriManager.uri -val trans_eq_URI : eq:UriManager.uri -> UriManager.uri -val sym_eq_URI : eq:UriManager.uri -> UriManager.uri -val eq_f_URI : eq:UriManager.uri -> UriManager.uri -val eq_f_sym_URI : eq:UriManager.uri -> UriManager.uri - - -val false_URI : unit -> UriManager.uri option -val true_URI : unit -> UriManager.uri option -val absurd_URI : unit -> UriManager.uri option - -val nat_URI : unit -> UriManager.uri option -val is_nat_URI : UriManager.uri -> bool diff --git a/matita/components/cic/path_indexing.ml b/matita/components/cic/path_indexing.ml deleted file mode 100644 index c0e4bb2be..000000000 --- a/matita/components/cic/path_indexing.ml +++ /dev/null @@ -1,227 +0,0 @@ -(* 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$ *) - -(* path indexing implementation *) - -(* position of the subterm, subterm (Appl are not stored...) *) - -module PathIndexing = - functor(A:Set.S) -> - struct - -type path_string_elem = Index of int | Term of Cic.term;; -type path_string = path_string_elem list;; - - -let rec path_strings_of_term index = - let module C = Cic in function - | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ] - | C.Appl (hd::tl) -> - let p = if index > 0 then [Index index; Term hd] else [Term hd] in - let _, res = - List.fold_left - (fun (i, r) t -> - let rr = path_strings_of_term i t in - (i+1, r @ (List.map (fun ps -> p @ ps) rr))) - (1, []) tl - in - res - | term -> [ [Index index; Term term] ] -;; - -(* -let string_of_path_string ps = - String.concat "." - (List.map - (fun e -> - let s = - match e with - | Index i -> "Index " ^ (string_of_int i) - | Term t -> "Term " ^ (CicPp.ppterm t) - in - "(" ^ s ^ ")") - ps) -;; -*) - -module OrderedPathStringElement = struct - type t = path_string_elem - - let compare t1 t2 = - match t1, t2 with - | Index i, Index j -> Pervasives.compare i j - | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2 - | Index _, Term _ -> -1 - | Term _, Index _ -> 1 -end - -module PSMap = Map.Make(OrderedPathStringElement);; - -module PSTrie = Trie.Make(PSMap);; - -type t = A.t PSTrie.t -type key = Cic.term -let empty = PSTrie.empty -let arities = Hashtbl.create 0 - -let index trie term info = - let ps = path_strings_of_term 0 term in - List.fold_left - (fun trie ps -> - let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in - let trie = PSTrie.add ps (A.add info ps_set) trie in - trie) trie ps - -let remove_index trie term info= - let ps = path_strings_of_term 0 term in - List.fold_left - (fun trie ps -> - try - let ps_set = A.remove info (PSTrie.find ps trie) in - if A.is_empty ps_set then - PSTrie.remove ps trie - else - PSTrie.add ps ps_set trie - with Not_found -> trie) trie ps -;; - -let in_index trie term test = - let ps = path_strings_of_term 0 term in - let ok ps = - try - let set = PSTrie.find ps trie in - A.exists test set - with Not_found -> - false - in - List.exists ok ps -;; - - -let head_of_term = function - | Cic.Appl (hd::tl) -> hd - | term -> term -;; - - -let subterm_at_pos index term = - if index = 0 then - term - else - match term with - | Cic.Appl l -> - (try List.nth l index with Failure _ -> raise Not_found) - | _ -> raise Not_found -;; - - -let rec retrieve_generalizations trie term = - match trie with - | PSTrie.Node (value, map) -> - let res = - match term with - | Cic.Meta _ -> A.empty - | term -> - let hd_term = head_of_term term in - try - let n = PSMap.find (Term hd_term) map in - match n with - | PSTrie.Node (Some s, _) -> s - | PSTrie.Node (None, m) -> - let l = - PSMap.fold - (fun k v res -> - match k with - | Index i -> - let t = subterm_at_pos i term in - let s = retrieve_generalizations v t in - s::res - | _ -> res) - m [] - in - match l with - | hd::tl -> - List.fold_left (fun r s -> A.inter r s) hd tl - | _ -> A.empty - with Not_found -> - A.empty - in - try - let n = PSMap.find (Term (Cic.Implicit None)) map in - match n with - | PSTrie.Node (Some s, _) -> A.union res s - | _ -> res - with Not_found -> - res -;; - - -let rec retrieve_unifiables trie term = - match trie with - | PSTrie.Node (value, map) -> - let res = - match term with - | Cic.Meta _ -> - PSTrie.fold - (fun ps v res -> A.union res v) - (PSTrie.Node (None, map)) - A.empty - | _ -> - let hd_term = head_of_term term in - try - let n = PSMap.find (Term hd_term) map in - match n with - | PSTrie.Node (Some v, _) -> v - | PSTrie.Node (None, m) -> - let l = - PSMap.fold - (fun k v res -> - match k with - | Index i -> - let t = subterm_at_pos i term in - let s = retrieve_unifiables v t in - s::res - | _ -> res) - m [] - in - match l with - | hd::tl -> - List.fold_left (fun r s -> A.inter r s) hd tl - | _ -> A.empty - with Not_found -> - A.empty - in - try - let n = PSMap.find (Term (Cic.Implicit None)) map in - match n with - | PSTrie.Node (Some s, _) -> A.union res s - | _ -> res - with Not_found -> - res -;; - -end diff --git a/matita/components/cic/path_indexing.mli b/matita/components/cic/path_indexing.mli deleted file mode 100644 index 899901618..000000000 --- a/matita/components/cic/path_indexing.mli +++ /dev/null @@ -1,42 +0,0 @@ -(* 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/. - *) - -module PathIndexing : - functor (A : Set.S) -> - sig - val arities : (Cic.term, int) Hashtbl.t - - type key = Cic.term - type t - - val empty : t - val index : t -> key -> A.elt -> t - val remove_index : t -> key -> A.elt -> t - val in_index : t -> key -> (A.elt -> bool) -> bool - val retrieve_generalizations : t -> key -> A.t - val retrieve_unifiables : t -> key -> A.t - end - - diff --git a/matita/components/cic/unshare.ml b/matita/components/cic/unshare.ml deleted file mode 100644 index 405e1d586..000000000 --- a/matita/components/cic/unshare.ml +++ /dev/null @@ -1,214 +0,0 @@ -(* 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/. - *) - -(* $Id$ *) - -let unshare ?(fresh_univs=false) t = - let module C = Cic in - let rec unshare = - function - C.Rel m -> C.Rel m - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i,l) -> - let l' = - List.map - (function - None -> None - | Some t -> Some (unshare t) - ) l - in - C.Meta(i,l') - | C.Sort s when not fresh_univs -> C.Sort s - | C.Sort (C.Type _) -> C.Sort (C.Type (CicUniv.fresh ())) - | C.Sort s -> C.Sort s - | C.Implicit info -> C.Implicit info - | C.Cast (te,ty) -> C.Cast (unshare te, unshare ty) - | C.Prod (n,s,t) -> C.Prod (n, unshare s, unshare t) - | C.Lambda (n,s,t) -> C.Lambda (n, unshare s, unshare t) - | C.LetIn (n,s,ty,t) -> - C.LetIn (n, unshare s, unshare ty, unshare t) - | C.Appl l -> C.Appl (List.map unshare l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst - in - C.MutInd (uri,tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst - in - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, unshare outty, unshare t, - List.map unshare pl) - | C.Fix (i, fl) -> - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, unshare ty, unshare bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, unshare ty, unshare bo)) - fl - in - C.CoFix (i, liftedfl) - in - unshare t -;; - -let sharing_map f l = - let unchanged = ref true in - let rec aux b = function - | [] as t -> unchanged := b; t - | he::tl -> - let he1 = f he in - he1 :: aux (b && he1 == he) tl - in - let l1 = aux true l in - if !unchanged then l else l1 -;; - -let fresh_univs t = - let module C = Cic in - let rec unshare = - function - | C.Sort (C.Type u) when not (CicUniv.is_anon u) -> C.Sort (C.Type (CicUniv.fresh ())) - | C.Sort _ | C.Implicit _ | C.Var _ | C.Rel _ as t -> t - | C.Meta (i,l) as orig -> - let l' = sharing_map - (function None -> None | Some t -> Some (unshare t)) l - in - if l == l' then orig else C.Meta(i,l') - | C.Cast (te,ty) as orig -> - let te' = unshare te in - let ty' = unshare ty in - if te' == te && ty' == ty then orig else C.Cast(te', ty') - | C.Prod (n,s,t) as orig -> - let s' = unshare s in - let t' = unshare t in - if s' == s && t' == t then orig else C.Prod(n,s',t') - | C.Lambda (n,s,t) as orig -> - let s' = unshare s in - let t' = unshare t in - if s' == s && t' == t then orig else C.Lambda(n,s',t') - | C.LetIn (n,s,ty,t) as orig -> - let s' = unshare s in - let t' = unshare t in - let ty' = unshare ty in - if t' == t && ty' == ty && s' == s then orig else C.LetIn (n, s', ty', t') - | C.Appl l as orig -> - let l' = sharing_map unshare l in - if l == l' then orig else C.Appl l' - | C.Const (uri,exp_named_subst) as orig -> - let exp_named_subst' = - sharing_map - (fun (uri,t as orig) -> - let t' = unshare t in - if t == t' then orig else (uri,t')) - exp_named_subst - in - if exp_named_subst' == exp_named_subst then orig - else C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) as orig -> - let exp_named_subst' = - sharing_map - (fun (uri,t as orig) -> - let t' = unshare t in - if t == t' then orig else (uri,t')) - exp_named_subst - in - if exp_named_subst' == exp_named_subst then orig - else C.MutInd (uri,tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) as orig -> - let exp_named_subst' = - sharing_map - (fun (uri,t as orig) -> - let t' = unshare t in - if t == t' then orig else (uri,t')) - exp_named_subst - in - if exp_named_subst' == exp_named_subst then orig - else C.MutConstruct (uri,tyno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) as orig -> - let t' = unshare t in - let pl' = sharing_map unshare pl in - let outty' = unshare outty in - if t' == t && pl' == pl && outty' == outty then orig - else C.MutCase (sp, i, outty', t', pl') - | C.Fix (i, fl) as orig -> - let fl' = - sharing_map - (fun (name, i, ty, bo as orig) -> - let ty' = unshare ty in - let bo' = unshare bo in - if ty' == ty && bo' == bo then orig else name,i,ty',bo') - fl - in - if fl' == fl then orig else C.Fix (i, fl') - | C.CoFix (i, fl) as orig -> - let fl' = - sharing_map - (fun (name, ty, bo as orig) -> - let ty' = unshare ty in - let bo' = unshare bo in - if ty' == ty && bo' == bo then orig else name,ty',bo') - fl - in - if fl' == fl then orig else C.CoFix (i, fl') - in - unshare t -;; - -let fresh_types = - let module C = Cic in - let unshare = fresh_univs in - function - | C.Constant (name,te,ty,exp,att) -> - C.Constant (name,HExtlib.map_option unshare te, - unshare ty,exp,att) - | C.CurrentProof _ -> assert false - | C.Variable _ -> assert false - | C.InductiveDefinition (itl,u,i,att) -> - C.InductiveDefinition - (List.map - (fun (name,b,t,cl) -> - name,b,unshare t, - List.map - (fun (name,t) -> name, unshare t) - cl) - itl,u,i,att) -;; diff --git a/matita/components/cic/unshare.mli b/matita/components/cic/unshare.mli deleted file mode 100644 index 0dffb532e..000000000 --- a/matita/components/cic/unshare.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* 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/. - *) - -val unshare : ?fresh_univs:bool -> Cic.term -> Cic.term -val fresh_types: Cic.obj -> Cic.obj diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml index c7bfa5768..1f16df421 100644 --- a/matita/components/content/interpretations.ml +++ b/matita/components/content/interpretations.ml @@ -28,7 +28,6 @@ open Printf module Ast = NotationPt -module Obj = LibraryObjects let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () diff --git a/matita/components/grafite/grafiteMarshal.ml b/matita/components/grafite/grafiteMarshal.ml index d666f62b6..15e4f5217 100644 --- a/matita/components/grafite/grafiteMarshal.ml +++ b/matita/components/grafite/grafiteMarshal.ml @@ -44,14 +44,6 @@ let rehash_cmd_uris = | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in GrafiteAst.Default (loc, name, uris) - | GrafiteAst.PreferCoercion (loc, uri) -> - GrafiteAst.PreferCoercion (loc, CicUtil.rehash_term uri) - | GrafiteAst.Coercion (loc, uri, close, arity, saturations) -> - GrafiteAst.Coercion (loc, CicUtil.rehash_term uri, close, arity, saturations) - | GrafiteAst.Index (loc, key, uri) -> - GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri) - | GrafiteAst.Select (loc, uri) -> - GrafiteAst.Select (loc, rehash_uri uri) | GrafiteAst.Include _ as cmd -> cmd | cmd -> prerr_endline "Found a command not expected in a .moo:"; diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index d428bad22..6ebeb2842 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -653,9 +653,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,cmd = disambiguate_command status (text,prefix_len,cmd) in let status,uris = match cmd with - | GrafiteAst.Default (loc, what, uris) as cmd -> - LibraryObjects.set_default what uris; - GrafiteTypes.add_moo_content [cmd] status,`New [] | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Include (loc, mode, new_or_old, baseuri) -> (* Old Include command is not recursive; new one is *) diff --git a/matita/components/grafite_engine/grafiteSync.ml b/matita/components/grafite_engine/grafiteSync.ml index 60c366a0e..9302cbf89 100644 --- a/matita/components/grafite_engine/grafiteSync.ml +++ b/matita/components/grafite_engine/grafiteSync.ml @@ -74,11 +74,9 @@ let time_travel ~present ?(past=initial_status present present#baseuri) () = let init lexicon_status = initial_status lexicon_status ;; -let pop () = - LibraryObjects.pop () +let pop () = () ;; -let push () = - LibraryObjects.push () +let push () = () ;; diff --git a/matita/components/ng_cic_content/ncic2astMatcher.ml b/matita/components/ng_cic_content/ncic2astMatcher.ml index 2ae782bdb..5acb8eb13 100644 --- a/matita/components/ng_cic_content/ncic2astMatcher.ml +++ b/matita/components/ng_cic_content/ncic2astMatcher.ml @@ -40,8 +40,6 @@ struct | NRef of NReference.reference | Appl of cic_mask_t list - let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) - let mask_of_cic = function | NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl | NCic.Const nref -> NRef nref, [] -- 2.39.2