1 (* Copyright (C) 2003-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 module TC = CicTypeChecker
31 module PEH = ProofEngineHelpers
32 module E = CicEnvironment
33 module UM = UriManager
36 (* fresh name generator *****************************************************)
40 if i <= 0 then assert false else
41 let c = name.[pred i] in
42 if c >= '0' && c <= '9' then aux (pred i)
43 else Str.string_before name i, Str.string_after name i
45 let before, after = aux (String.length name) in
46 let i = if after = "" then -1 else int_of_string after in
50 C.Name (if i < 0 then s else s ^ string_of_int i)
52 let mk_fresh_name context (name, k) =
53 let rec aux i = function
55 | Some (C.Name s, _) :: entries ->
57 if m = name && j >= i then aux (succ j) entries else aux i entries
58 | _ :: entries -> aux i entries
62 let mk_fresh_name context = function
63 | C.Anonymous -> C.Anonymous
64 | C.Name s -> mk_fresh_name context (split s)
66 (* helper functions *********************************************************)
68 let rec list_map_cps g map = function
72 let g tl = g (hd :: tl) in
79 let compose f g x = f (g x)
81 let fst3 (x, _, _) = x
84 try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
86 Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
87 Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
88 Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
92 try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
94 Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
95 Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
99 match PEH.split_with_whd (c, t) with
100 | (_, hd) :: _, _ -> hd
104 match get_tail c (get_type c (get_type c t)) with
105 | C.Sort C.Prop -> true
109 let is_unsafe h (c, t) = true
111 let is_not_atomic = function
117 | C.MutConstruct _ -> false
120 let is_atomic t = not (is_not_atomic t)
122 let get_ind_type uri tyno =
123 match E.get_obj Un.empty_ugraph uri with
124 | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
127 let get_default_eliminator context uri tyno ty =
128 let _, (name, _, _, _) = get_ind_type uri tyno in
129 let ext = match get_tail context (get_type context ty) with
130 | C.Sort C.Prop -> "_ind"
131 | C.Sort C.Set -> "_rec"
132 | C.Sort C.CProp -> "_rec"
133 | C.Sort (C.Type _) -> "_rect"
135 Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
138 let buri = UM.buri_of_uri uri in
139 let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
142 let get_ind_parameters c t =
143 let ty = get_type c t in
144 let ps = match get_tail c ty with
146 | C.Appl (C.MutInd _ :: args) -> args
149 let disp = match get_tail c (get_type c ty) with
156 let cic = D.deannotate_term