components/acic_procedural/proceduralHelpers.ml

   1 (* Copyright (C) 2003-2005, 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://cs.unibo.it/helm/.
  24  *)
  25
  26 module C    = Cic
  27 module Rf   = CicRefine
  28 module Un   = CicUniv
  29 module Pp   = CicPp
  30 module TC   = CicTypeChecker
  31 module PEH  = ProofEngineHelpers
  32 module E    = CicEnvironment
  33 module UM   = UriManager
  34
  35 (* fresh name generator *****************************************************)
  36
  37 let split name =
  38    let rec aux i =
  39       if i <= 0 then assert false else
  40       let c = name.[pred i] in
  41       if c >= '0' && c <= '9' then aux (pred i)
  42       else Str.string_before name i, Str.string_after name i
  43    in
  44    let before, after = aux (String.length name) in
  45    let i = if after = "" then -1 else int_of_string after in
  46    before, i
  47
  48 let join (s, i) =
  49    C.Name (if i < 0 then s else s ^ string_of_int i)
  50
  51 let mk_fresh_name context (name, k) =
  52    let rec aux i = function
  53       | []                            -> name, i
  54       | Some (C.Name s, _) :: entries ->
  55          let m, j = split s in
  56          if m = name && j >= i then aux (succ j) entries else aux i entries
  57       | _ :: entries                  -> aux i entries
  58    in
  59    join (aux k context)
  60
  61 let mk_fresh_name context = function
  62    | C.Anonymous -> C.Anonymous
  63    | C.Name s    -> mk_fresh_name context (split s)
  64
  65 (* helper functions *********************************************************)
  66
  67 let rec list_map_cps g map = function
  68    | []       -> g []
  69    | hd :: tl ->
  70       let h hd =
  71          let g tl = g (hd :: tl) in
  72          list_map_cps g map tl
  73       in
  74       map h hd
  75
  76 let identity x = x
  77
  78 let compose f g x = f (g x)
  79
  80 let fst3 (x, _, _) = x
  81
  82 let refine c t =
  83    try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
  84    with e ->
  85       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
  86       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
  87       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
  88       raise e
  89
  90 let get_type c t =
  91    try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
  92    with e ->
  93       Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
  94       Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
  95       raise e
  96
  97 let get_tail c t =
  98    match PEH.split_with_whd (c, t) with
  99       | (_, hd) :: _, _ -> hd
 100       | _               -> assert false
 101
 102 let is_proof c t =
 103    match get_tail c (get_type c (get_type c t)) with
 104       | C.Sort C.Prop -> true
 105       | C.Sort _      -> false
 106       | _             -> assert false
 107
 108 let is_unsafe h (c, t) = true
 109
 110 let is_not_atomic = function
 111    | C.Sort _
 112    | C.Rel _
 113    | C.Const _
 114    | C.Var _
 115    | C.MutInd _
 116    | C.MutConstruct _ -> false
 117    | _                -> true
 118
 119 let get_ind_type uri tyno =
 120    match E.get_obj Un.empty_ugraph uri with
 121       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
 122       | _                                           -> assert false
 123
 124 let get_default_eliminator context uri tyno ty =
 125    let _, (name, _, _, _) = get_ind_type uri tyno in
 126    let ext = match get_tail context (get_type context ty) with
 127       | C.Sort C.Prop     -> "_ind"
 128       | C.Sort C.Set      -> "_rec"
 129       | C.Sort C.CProp    -> "_rec"
 130       | C.Sort (C.Type _) -> "_rect"
 131       | t                 ->
 132          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
 133          assert false
 134    in
 135    let buri = UM.buri_of_uri uri in
 136    let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
 137    C.Const (uri, [])
 138
 139 let get_ind_parameters c t =
 140    let ty = get_type c t in
 141    let ps = match get_tail c ty with
 142       | C.MutInd _                  -> []
 143       | C.Appl (C.MutInd _ :: args) -> args
 144       | _                           -> assert false
 145    in
 146    let disp = match get_tail c (get_type c ty) with
 147       | C.Sort C.Prop -> 0
 148       | C.Sort _      -> 1
 149       | _             -> assert false
 150    in
 151    ps, disp