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
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
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)
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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:
- <!ELEMENT CurrentProof (Conjecture*,body)>
- <!ELEMENT Sequent %sequent;>
- <!ELEMENT Conjecture %sequent;>
- <!ELEMENT Decl %term;>
- <!ELEMENT Def %term;>
- <!ELEMENT Hidden EMPTY>
- <!ELEMENT Goal %term;>
-*)
-
-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 <tag_name,
- * attribute_list> *)
-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 <name, value> _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 "</%s>" 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. <arity>) *)
- push ctxt (Cic_term term)
- | "substitution" -> (* optional transparent elements (i.e. which _may_
- * contain a CIC) *)
- set_top ctxt (* replace <substitution> *)
- (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 <arg> 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 <instantiate> *)
- 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)
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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)
-;;
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-
-
+++ /dev/null
-(* 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)
-;;
+++ /dev/null
-(* 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
open Printf
module Ast = NotationPt
-module Obj = LibraryObjects
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
| 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:";
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 *)
let init lexicon_status =
initial_status lexicon_status
;;
-let pop () =
- LibraryObjects.pop ()
+let pop () = ()
;;
-let push () =
- LibraryObjects.push ()
+let push () = ()
;;
| 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, []
projects / helm.git / commitdiff