]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_unification/cicMkImplicit.ml
incomplete proof completed
[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.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://cs.unibo.it/helm/.
24  *)
25
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 rec aux =
32    function
33       (_,[]) -> []
34     | (n,None::tl) -> None::(aux ((n+1),tl))
35     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
36   in
37    aux (start,canonical_context)
38
39 (* Returns the first meta whose number is above the *)
40 (* number of the higher meta.                       *)
41 let new_meta metasenv subst =
42   let rec aux =
43    function
44       None, [] -> 1
45     | Some n, [] -> n
46     | None, n::tl -> aux (Some n,tl)
47     | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
48   in
49   let indexes = 
50     (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst)
51   in
52   1 + aux (None, indexes)
53
54 (* let apply_subst_context = CicMetaSubst.apply_subst_context;; *)
55 (* questa o la precedente sembrano essere equivalenti come tempi *)
56 let apply_subst_context _ context = context ;;
57
58 let mk_implicit metasenv subst context =
59   let newmeta = new_meta metasenv subst in
60   let newuniv = CicUniv.fresh () in
61   let irl = identity_relocation_list_for_metavariable context in
62     (* in the following mk_* functions we apply substitution to canonical
63     * context since we have the invariant that the metasenv has already been
64     * instantiated with subst *)
65   let context = apply_subst_context subst context in
66   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
67     (* TASSI: ?? *)
68     newmeta + 1, context, Cic.Meta (newmeta, []);
69     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
70    newmeta + 2)
71
72 let mk_implicit_type metasenv subst context =
73   let newmeta = new_meta metasenv subst in
74   let newuniv = CicUniv.fresh () in
75   let context = apply_subst_context subst context in
76   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
77     (* TASSI: ?? *)
78     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
79    newmeta + 1)
80
81 let mk_implicit_sort metasenv subst =
82   let newmeta = new_meta metasenv subst in
83   let newuniv = CicUniv.fresh () in
84   ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta)
85   (* TASSI: ?? *)
86
87 let n_fresh_metas metasenv subst context n = 
88   if n = 0 then metasenv, []
89   else 
90     let irl = identity_relocation_list_for_metavariable context in
91     let context = apply_subst_context subst context in
92     let newmeta = new_meta metasenv subst in
93     let newuniv = CicUniv.fresh () in
94     let rec aux newmeta n = 
95       if n = 0 then metasenv, [] 
96       else
97         let metasenv', l = aux (newmeta + 3) (n-1) in 
98         (* TASSI: ?? *)
99         (newmeta, context, Cic.Sort (Cic.Type newuniv))::
100         (newmeta + 1, context, Cic.Meta (newmeta, irl))::
101         (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
102         Cic.Meta(newmeta+2,irl)::l in
103     aux newmeta n
104       
105 let fresh_subst metasenv subst context uris = 
106   let irl = identity_relocation_list_for_metavariable context in
107   let context = apply_subst_context subst context in
108   let newmeta = new_meta metasenv subst in
109   let newuniv = CicUniv.fresh () in
110   let rec aux newmeta = function
111       [] -> metasenv, [] 
112     | uri::tl ->
113        let metasenv', l = aux (newmeta + 3) tl in 
114          (* TASSI: ?? *)
115          (newmeta, context, Cic.Sort (Cic.Type newuniv))::
116          (newmeta + 1, context, Cic.Meta (newmeta, irl))::
117          (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
118           (uri,Cic.Meta(newmeta+2,irl))::l in
119     aux newmeta uris
120
121 let expand_implicits metasenv subst context term =
122   let rec aux metasenv context = function
123     | (Cic.Rel _) as t -> metasenv, t
124     | (Cic.Sort _) as t -> metasenv, t
125     | Cic.Const (uri, subst) ->
126         let metasenv', subst' = do_subst metasenv context subst in
127         metasenv', Cic.Const (uri, subst')
128     | Cic.Var (uri, subst) ->
129         let metasenv', subst' = do_subst metasenv context subst in
130         metasenv', Cic.Var (uri, subst')
131     | Cic.MutInd (uri, i, subst) ->
132         let metasenv', subst' = do_subst metasenv context subst in
133         metasenv', Cic.MutInd (uri, i, subst')
134     | Cic.MutConstruct (uri, i, j, subst) ->
135         let metasenv', subst' = do_subst metasenv context subst in
136         metasenv', Cic.MutConstruct (uri, i, j, subst')
137     | Cic.Meta (n,l) -> 
138         let metasenv', l' = do_local_context metasenv context l in
139         metasenv', Cic.Meta (n, l')
140     | Cic.Implicit (Some `Type) ->
141         let (metasenv', idx) = mk_implicit_type metasenv subst context in
142         let irl = identity_relocation_list_for_metavariable context in
143         metasenv', Cic.Meta (idx, irl)
144     | Cic.Implicit (Some `Closed) ->
145         let (metasenv', idx) = mk_implicit metasenv subst [] in
146         metasenv', Cic.Meta (idx, [])
147     | Cic.Implicit None ->
148         let (metasenv', idx) = mk_implicit metasenv subst context in
149         let irl = identity_relocation_list_for_metavariable context in
150         metasenv', Cic.Meta (idx, irl)
151     | Cic.Implicit _ -> assert false
152     | Cic.Cast (te, ty) ->
153         let metasenv', ty' = aux metasenv context ty in
154         let metasenv'', te' = aux metasenv' context te in
155         metasenv'', Cic.Cast (te', ty')
156     | Cic.Prod (name, s, t) ->
157         let metasenv', s' = aux metasenv context s in
158         let metasenv'', t' =
159           aux metasenv' (Some (name, Cic.Decl s') :: context) t
160         in
161         metasenv'', Cic.Prod (name, s', t')
162     | Cic.Lambda (name, s, t) ->
163         let metasenv', s' = aux metasenv context s in
164         let metasenv'', t' =
165           aux metasenv' (Some (name, Cic.Decl s') :: context) t
166         in
167         metasenv'', Cic.Lambda (name, s', t')
168     | Cic.LetIn (name, s, t) ->
169         let metasenv', s' = aux metasenv context s in
170         let metasenv'', t' =
171           aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
172         in
173         metasenv'', Cic.LetIn (name, s', t')
174     | Cic.Appl l when List.length l > 1 ->
175         let metasenv', l' =
176           List.fold_right
177             (fun term (metasenv, terms) ->
178               let new_metasenv, term = aux metasenv context term in
179               new_metasenv, term :: terms)
180             l (metasenv, [])
181         in
182         metasenv', Cic.Appl l'
183     | Cic.Appl _ -> assert false
184     | Cic.MutCase (uri, i, outtype, term, patterns) ->
185         let metasenv', l' =
186           List.fold_right
187             (fun term (metasenv, terms) ->
188               let new_metasenv, term = aux metasenv context term in
189               new_metasenv, term :: terms)
190             (outtype :: term :: patterns) (metasenv, [])
191         in
192         let outtype', term', patterns' =
193           match l' with
194           | outtype' :: term' :: patterns' -> outtype', term', patterns'
195           | _ -> assert false
196         in
197         metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
198     | Cic.Fix (i, funs) ->
199         let metasenv', types =
200           List.fold_right
201             (fun (name, _, typ, _) (metasenv, types) ->
202               let new_metasenv, new_type = aux metasenv context typ in
203               (new_metasenv, (name, new_type) :: types))
204             funs (metasenv, [])
205         in
206         let context' =
207           (List.rev_map
208             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
209             types)
210           @ context
211         in
212         let metasenv'', bodies =
213           List.fold_right
214             (fun (_, _, _, body) (metasenv, bodies) ->
215               let new_metasenv, new_body = aux metasenv context' body in
216               (new_metasenv, new_body :: bodies))
217             funs (metasenv', [])
218         in
219         let rec combine = function
220           | ((name, index, _, _) :: funs_tl),
221             ((_, typ) :: typ_tl),
222             (body :: body_tl) ->
223               (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
224           | [], [], [] -> []
225           | _ -> assert false
226         in
227         let funs' = combine (funs, types, bodies) in
228         metasenv'', Cic.Fix (i, funs')
229     | Cic.CoFix (i, funs) ->
230         let metasenv', types =
231           List.fold_right
232             (fun (name, typ, _) (metasenv, types) ->
233               let new_metasenv, new_type = aux metasenv context typ in
234               (new_metasenv, (name, new_type) :: types))
235             funs (metasenv, [])
236         in
237         let context' =
238           (List.rev_map
239             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
240             types)
241           @ context
242         in
243         let metasenv'', bodies =
244           List.fold_right
245             (fun (_, _, body) (metasenv, bodies) ->
246               let new_metasenv, new_body = aux metasenv context' body in
247               (new_metasenv, new_body :: bodies))
248             funs (metasenv', [])
249         in
250         let rec combine = function
251           | ((name, _, _) :: funs_tl),
252             ((_, typ) :: typ_tl),
253             (body :: body_tl) ->
254               (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
255           | [], [], [] -> []
256           | _ -> assert false
257         in
258         let funs' = combine (funs, types, bodies) in
259         metasenv'', Cic.CoFix (i, funs')
260   and do_subst metasenv context subst =
261     List.fold_right
262       (fun (uri, term) (metasenv, substs) ->
263         let metasenv', term' = aux metasenv context term in
264         (metasenv', (uri, term') :: substs))
265       subst (metasenv, [])
266   and do_local_context metasenv context local_context =
267     List.fold_right
268       (fun term (metasenv, local_context) ->
269         let metasenv', term' =
270           match term with
271           | None -> metasenv, None
272           | Some term ->
273               let metasenv', term' = aux metasenv context term in
274               metasenv', Some term'
275         in
276         metasenv', term' :: local_context)
277       local_context (metasenv, [])
278   in
279   aux metasenv context term
280