helm/software/components/ng_disambiguation/nnumber_notation.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *)
  27
  28 let error msg =
  29    raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
  30
  31 let build_nat o s str =
  32    let n = int_of_string str in
  33    if n < 0 then error (str ^ " is not a valid natural number number") else
  34    let rec aux n = if n = 0 then o () else s (aux (pred n)) in
  35    aux n
  36
  37 let ninterp_natural_number num =
  38   (*
  39    let nat_URI = match Obj.nat_URI () with
  40       | Some uri -> uri
  41       | None     -> error "no default natural numbers"
  42    in
  43   *)
  44    let nat_URI = NUri.uri_of_string "cic:/matita/ng/arithmetics/nat/nat.ind" in
  45    let o () =
  46     NCic.Const
  47      (NReference.reference_of_spec nat_URI (NReference.Con (0,1,0))) in
  48    let s t =
  49     NCic.Appl
  50      [NCic.Const
  51       (NReference.reference_of_spec nat_URI (NReference.Con (0,2,0)));
  52       t] in
  53    build_nat o s num
  54
  55 let _ =
  56   DisambiguateChoices.nadd_num_choice
  57     ("nnatural number", `Num_interp ninterp_natural_number);
  58 ;;