-(* 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/.
- *)
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
exception IllFormedReference of string Lazy.t
| Def
| Fix of int * int (* fixno, recparamno *)
| CoFix of int
- | Ind of int
+ | Ind of bool * int (* inductive, indtyno *)
| Con of int * int (* indtyno, constrno *)
type reference = Ref of int * NUri.uri * spec
| "def" -> Ref (c (), u, Def)
| "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j))
| "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i))
- | "ind" -> let i = get1 s dot in Ref (c (), u, Ind (i))
+ | "ind" -> let b,i = get2 s dot in Ref (c (), u, Ind (b=1,i))
| "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j))
| _ -> raise Not_found
with Not_found -> raise (IllFormedReference (lazy s))
| Def -> s2 ^ ".def"
| Fix (i,j) -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
| CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
- | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")"
+ | Ind (b,i)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^")"
| Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
;;
let mk_constructor j = function
- | Ref (d, u, Ind i) ->
+ | Ref (d, u, Ind (_,i)) ->
reference_of_string (string_of_reference (Ref (d, u, Con (i,j))))
| _ -> assert false
;;
reference_of_string (string_of_reference (Ref (d, u, CoFix i)))
| _ -> assert false
;;
-
-let reference_of_ouri u indinfo =
- let u = NUri.nuri_of_ouri u in
- reference_of_string (string_of_reference (Ref (max_int,u,indinfo)))
-;;
-
-let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;;
-