1 (* Copyright (C) 2004, 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 (* identity_relocation_list_for_metavariable i canonical_context *)
27 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
28 (* where n = List.length [canonical_context] *)
29 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
30 let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
31 let canonical_context_length = List.length canonical_context in
35 | (n,None::tl) -> None::(aux ((n+1),tl))
36 | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
38 aux (start,canonical_context)
40 (* Returns the first meta whose number is above the *)
41 (* number of the higher meta. *)
42 let new_meta metasenv =
47 | None,(n,_,_)::tl -> aux (Some n,tl)
48 | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
50 1 + aux (None,metasenv)
52 let mk_implicit metasenv context =
53 let newmeta = new_meta metasenv in
54 let newuniv = CicUniv.fresh () in
55 let irl = identity_relocation_list_for_metavariable context in
56 ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
58 newmeta + 1, context, Cic.Meta (newmeta, []);
59 newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
62 let mk_implicit_type metasenv context =
63 let newmeta = new_meta metasenv in
64 let newuniv = CicUniv.fresh () in
65 ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
67 newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
70 let mk_implicit_sort metasenv =
71 let newmeta = new_meta metasenv in
72 let newuniv = CicUniv.fresh () in
73 ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta)
76 let n_fresh_metas metasenv context n =
77 if n = 0 then metasenv, []
79 let irl = identity_relocation_list_for_metavariable context in
80 let newmeta = new_meta metasenv in
81 let newuniv = CicUniv.fresh () in
82 let rec aux newmeta n =
83 if n = 0 then metasenv, []
85 let metasenv', l = aux (newmeta + 3) (n-1) in
87 (newmeta, context, Cic.Sort (Cic.Type newuniv))::
88 (newmeta + 1, context, Cic.Meta (newmeta, irl))::
89 (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
90 Cic.Meta(newmeta+2,irl)::l in
93 let fresh_subst metasenv context uris =
94 let irl = identity_relocation_list_for_metavariable context in
95 let newmeta = new_meta metasenv in
96 let newuniv = CicUniv.fresh () in
97 let rec aux newmeta = function
100 let metasenv', l = aux (newmeta + 3) tl in
102 (newmeta, context, Cic.Sort (Cic.Type newuniv))::
103 (newmeta + 1, context, Cic.Meta (newmeta, irl))::
104 (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
105 (uri,Cic.Meta(newmeta+2,irl))::l in
108 let expand_implicits metasenv context term =
109 let rec aux metasenv context = function
110 | (Cic.Rel _) as t -> metasenv, t
111 | (Cic.Sort _) as t -> metasenv, t
112 | Cic.Const (uri, subst) ->
113 let metasenv', subst' = do_subst metasenv context subst in
114 metasenv', Cic.Const (uri, subst')
115 | Cic.Var (uri, subst) ->
116 let metasenv', subst' = do_subst metasenv context subst in
117 metasenv', Cic.Var (uri, subst')
118 | Cic.MutInd (uri, i, subst) ->
119 let metasenv', subst' = do_subst metasenv context subst in
120 metasenv', Cic.MutInd (uri, i, subst')
121 | Cic.MutConstruct (uri, i, j, subst) ->
122 let metasenv', subst' = do_subst metasenv context subst in
123 metasenv', Cic.MutConstruct (uri, i, j, subst')
125 let metasenv', l' = do_local_context metasenv context l in
126 metasenv', Cic.Meta (n, l')
127 | Cic.Implicit (Some `Type) ->
128 let (metasenv', idx) = mk_implicit_type metasenv context in
129 let irl = identity_relocation_list_for_metavariable context in
130 metasenv', Cic.Meta (idx, irl)
131 | Cic.Implicit (Some `Closed) ->
132 let (metasenv', idx) = mk_implicit metasenv [] in
133 metasenv', Cic.Meta (idx, [])
134 | Cic.Implicit None ->
135 let (metasenv', idx) = mk_implicit metasenv context in
136 let irl = identity_relocation_list_for_metavariable context in
137 metasenv', Cic.Meta (idx, irl)
138 | Cic.Cast (te, ty) ->
139 let metasenv', ty' = aux metasenv context ty in
140 let metasenv'', te' = aux metasenv' context te in
141 metasenv'', Cic.Cast (te', ty')
142 | Cic.Prod (name, s, t) ->
143 let metasenv', s' = aux metasenv context s in
145 aux metasenv' (Some (name, Cic.Decl s') :: context) t
147 metasenv'', Cic.Prod (name, s', t')
148 | Cic.Lambda (name, s, t) ->
149 let metasenv', s' = aux metasenv context s in
151 aux metasenv' (Some (name, Cic.Decl s') :: context) t
153 metasenv'', Cic.Lambda (name, s', t')
154 | Cic.LetIn (name, s, t) ->
155 let metasenv', s' = aux metasenv context s in
157 aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
159 metasenv'', Cic.LetIn (name, s', t')
160 | Cic.Appl l when List.length l > 1 ->
163 (fun term (metasenv, terms) ->
164 let new_metasenv, term = aux metasenv context term in
165 new_metasenv, term :: terms)
168 metasenv', Cic.Appl l'
169 | Cic.Appl _ -> assert false
170 | Cic.MutCase (uri, i, outtype, term, patterns) ->
173 (fun term (metasenv, terms) ->
174 let new_metasenv, term = aux metasenv context term in
175 new_metasenv, term :: terms)
176 (outtype :: term :: patterns) (metasenv, [])
178 let outtype', term', patterns' =
180 | outtype' :: term' :: patterns' -> outtype', term', patterns'
183 metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
184 | Cic.Fix (i, funs) ->
185 let metasenv', types =
187 (fun (name, _, typ, _) (metasenv, types) ->
188 let new_metasenv, new_type = aux metasenv context typ in
189 (new_metasenv, (name, new_type) :: types))
194 (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
198 let metasenv'', bodies =
200 (fun (_, _, _, body) (metasenv, bodies) ->
201 let new_metasenv, new_body = aux metasenv context' body in
202 (new_metasenv, new_body :: bodies))
205 let rec combine = function
206 | ((name, index, _, _) :: funs_tl),
207 ((_, typ) :: typ_tl),
209 (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
213 let funs' = combine (funs, types, bodies) in
214 metasenv'', Cic.Fix (i, funs')
215 | Cic.CoFix (i, funs) ->
216 let metasenv', types =
218 (fun (name, typ, _) (metasenv, types) ->
219 let new_metasenv, new_type = aux metasenv context typ in
220 (new_metasenv, (name, new_type) :: types))
225 (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
229 let metasenv'', bodies =
231 (fun (_, _, body) (metasenv, bodies) ->
232 let new_metasenv, new_body = aux metasenv context' body in
233 (new_metasenv, new_body :: bodies))
236 let rec combine = function
237 | ((name, _, _) :: funs_tl),
238 ((_, typ) :: typ_tl),
240 (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
244 let funs' = combine (funs, types, bodies) in
245 metasenv'', Cic.CoFix (i, funs')
246 and do_subst metasenv context subst =
248 (fun (uri, term) (metasenv, substs) ->
249 let metasenv', term' = aux metasenv context term in
250 (metasenv', (uri, term') :: substs))
252 and do_local_context metasenv context local_context =
254 (fun term (metasenv, local_context) ->
255 let metasenv', term' =
257 | None -> metasenv, None
259 let metasenv', term' = aux metasenv context term in
260 metasenv', Some term'
262 metasenv', term' :: local_context)
263 local_context (metasenv, [])
265 aux metasenv context term