1 (* Copyright (C) 2000, 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/.
26 exception NotImplemented;;
28 let fresh_id ids_to_terms ids_to_father_ids =
31 let res = "i" ^ string_of_int !id in
33 Hashtbl.add ids_to_father_ids res father ;
34 Hashtbl.add ids_to_terms res t ;
38 exception NotEnoughElements;;
39 exception NameExpected;;
41 (*CSC: cut&paste da cicPp.ml *)
42 (* get_nth l n returns the nth element of the list l if it exists or *)
43 (* raises NotEnoughElements if l has less than n elements *)
47 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
48 | (_,_) -> raise NotEnoughElements
51 let acic_of_cic_env env t =
53 let ids_to_terms = Hashtbl.create 503 in
54 let ids_to_father_ids = Hashtbl.create 503 in
55 let fresh_id' = fresh_id ids_to_terms ids_to_father_ids in
56 let rec aux father bs tt =
57 let fresh_id'' = fresh_id' father tt in
58 let aux' = aux (Some fresh_id'') in
62 match get_nth bs n with
64 | _ -> raise NameExpected
66 C.ARel (fresh_id'', n, id)
67 | C.Var uri -> C.AVar (fresh_id'', uri)
68 | C.Meta n -> C.AMeta (fresh_id'', n)
69 | C.Sort s -> C.ASort (fresh_id'', s)
70 | C.Implicit -> C.AImplicit (fresh_id'')
72 C.ACast (fresh_id'', aux' bs v, aux' bs t)
74 C.AProd (fresh_id'', n, aux' bs s, aux' (n::bs) t)
76 C.ALambda (fresh_id'',n, aux' bs s, aux' (n::bs) t)
78 C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t)
79 | C.Appl l -> C.AAppl (fresh_id'', List.map (aux' bs) l)
80 | C.Const (uri,cn) -> C.AConst (fresh_id'', uri, cn)
81 | C.Abst _ -> raise NotImplemented
82 | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno)
83 | C.MutConstruct (uri,cn,tyno,consno) ->
84 C.AMutConstruct (fresh_id'', uri, cn, tyno, consno)
85 | C.MutCase (uri, cn, tyno, outty, term, patterns) ->
86 C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
87 aux' bs term, List.map (aux' bs) patterns)
88 | C.Fix (funno, funs) ->
89 let names = List.map (fun (name,_,_,_) -> C.Name name) funs in
90 C.AFix (fresh_id'', funno,
92 (fun (name, indidx, ty, bo) ->
93 (name, indidx, aux' bs ty, aux' (names@bs) bo)
96 | C.CoFix (funno, funs) ->
97 let names = List.map (fun (name,_,_) -> C.Name name) funs in
98 C.ACoFix (fresh_id'', funno,
100 (fun (name, ty, bo) ->
101 (name, aux' bs ty, aux' (names@bs) bo)
105 aux None env t, ids_to_terms, ids_to_father_ids
108 let acic_of_cic = acic_of_cic_env [];;