]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_unification/cicRefine.ml
rebuilt
[helm.git] / helm / ocaml / cic_unification / cicRefine.ml
1 (* Copyright (C) 2000, 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 open Printf
27
28 exception RefineFailure of string;;
29
30 exception Impossible of int;;
31 exception NotRefinable of string;;
32 exception Uncertain of string;;
33 exception WrongUriToConstant of string;;
34 exception WrongUriToVariable of string;;
35 exception ListTooShort;;
36 exception WrongUriToMutualInductiveDefinitions of string;;
37 exception RelToHiddenHypothesis;;
38 exception WrongArgumentNumber;;
39
40 let fdebug = ref 0;;
41 let debug t context =
42  let rec debug_aux t i =
43   let module C = Cic in
44   let module U = UriManager in
45    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
46  in
47   if !fdebug = 0 then
48    raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
49    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
50 ;;
51
52 let debug_print = prerr_endline
53
54 let rec split l n =
55  match (l,n) with
56     (l,0) -> ([], l)
57   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
58   | (_,_) -> raise ListTooShort
59 ;;
60
61 let rec type_of_constant uri =
62  let module C = Cic in
63  let module R = CicReduction in
64  let module U = UriManager in
65   match CicEnvironment.get_cooked_obj uri with
66      C.Constant (_,_,ty,_) -> ty
67    | C.CurrentProof (_,_,_,ty,_) -> ty
68    | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
69
70 and type_of_variable uri =
71  let module C = Cic in
72  let module R = CicReduction in
73  let module U = UriManager in
74   match CicEnvironment.get_cooked_obj uri with
75      C.Variable (_,_,ty,_) -> ty
76    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
77
78 and type_of_mutual_inductive_defs uri i =
79  let module C = Cic in
80  let module R = CicReduction in
81  let module U = UriManager in
82   match CicEnvironment.get_cooked_obj uri with
83      C.InductiveDefinition (dl,_,_) ->
84       let (_,_,arity,_) = List.nth dl i in
85        arity
86    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
87
88 and type_of_mutual_inductive_constr uri i j =
89  let module C = Cic in
90  let module R = CicReduction in
91  let module U = UriManager in
92   match CicEnvironment.get_cooked_obj uri with
93       C.InductiveDefinition (dl,_,_) ->
94        let (_,_,_,cl) = List.nth dl i in
95         let (_,ty) = List.nth cl (j-1) in
96          ty
97    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
98
99 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
100
101 (* the check_branch function checks if a branch of a case is refinable. 
102    It returns a pair (outype_instance,args), a subst and a metasenv.
103    outype_instance is the expected result of applying the case outtype 
104    to args. 
105    The problem is that outype is in general unknown, and we should
106    try to synthesize it from the above information, that is in general
107    a second order unification problem. *)
108  
109 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
110   let module C = Cic in
111   let module R = CicMetaSubst in
112   let module Un = CicUnification in 
113   match R.whd subst context expectedtype with
114      C.MutInd (_,_,_) ->
115        (n,context,actualtype, [term]), subst, metasenv
116    | C.Appl (C.MutInd (_,_,_)::tl) ->
117        let (_,arguments) = split tl left_args_no in
118        (n,context,actualtype, arguments@[term]), subst, metasenv
119    | C.Prod (name,so,de) ->
120       (* we expect that the actual type of the branch has the due 
121          number of Prod *)
122       (match R.whd subst context actualtype with
123            C.Prod (name',so',de') ->
124              let subst, metasenv = 
125                 Un.fo_unif_subst subst context metasenv so so' in
126              let term' =
127                (match CicSubstitution.lift 1 term with
128                    C.Appl l -> C.Appl (l@[C.Rel 1])
129                  | t -> C.Appl [t ; C.Rel 1]) in
130              (* we should also check that the name variable is anonymous in
131              the actual type de' ?? *)
132              check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de 
133          | _ -> raise WrongArgumentNumber)
134   | _ -> raise (NotRefinable "Prod or MutInd expected")
135
136 and type_of_aux' metasenv context t =
137  let rec type_of_aux subst metasenv context =
138   let module C = Cic in
139   let module S = CicSubstitution in
140   let module U = UriManager in
141   let module Un = CicUnification in
142    function
143       C.Rel n ->
144        (try
145          match List.nth context (n - 1) with
146             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
147           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
148           | Some (_,C.Def (bo,None)) ->
149              type_of_aux subst metasenv context (S.lift n bo)
150           | None -> raise RelToHiddenHypothesis
151         with
152          _ -> raise (NotRefinable "Not a close term")
153        )
154     | C.Var (uri,exp_named_subst) ->
155       incr fdebug ;
156       let subst',metasenv' =
157        check_exp_named_subst subst metasenv context exp_named_subst in
158       let ty =
159        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
160       in
161        decr fdebug ;
162        ty,subst',metasenv'
163     | C.Meta (n,l) -> 
164        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
165         let subst',metasenv' =
166          check_metasenv_consistency n subst metasenv context canonical_context l
167         in
168         CicSubstitution.lift_meta l ty, subst', metasenv'
169     | C.Sort s ->
170        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
171         subst,metasenv
172     | C.Implicit _ -> raise (Impossible 21)
173     | C.Cast (te,ty) ->
174        let _,subst',metasenv' =
175         type_of_aux subst metasenv context ty in
176        let inferredty,subst'',metasenv'' =
177         type_of_aux subst' metasenv' context te
178        in
179         (try
180           let subst''',metasenv''' =
181            Un.fo_unif_subst subst'' context metasenv'' inferredty ty
182           in
183            ty,subst''',metasenv'''
184          with
185           _ -> raise (NotRefinable "Cast"))
186     | C.Prod (name,s,t) ->
187        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
188        let sort2,subst'',metasenv'' =
189         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
190        in
191         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
192    | C.Lambda (n,s,t) ->
193        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
194        let type2,subst'',metasenv'' =
195         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
196        in
197         let sort2,subst''',metasenv''' =
198          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
199         in
200          (* only to check if the product is well-typed *)
201          let _,subst'''',metasenv'''' =
202           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
203          in
204           C.Prod (n,s,type2),subst'''',metasenv''''
205    | C.LetIn (n,s,t) ->
206       (* only to check if s is well-typed *)
207       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
208       let inferredty,subst'',metasenv'' =
209        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
210       in
211        (* One-step LetIn reduction. Even faster than the previous solution.
212           Moreover the inferred type is closer to the expected one. *)
213        CicSubstitution.subst s inferredty,subst',metasenv'
214    | C.Appl (he::tl) when List.length tl > 0 ->
215       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
216       let tlbody_and_type,subst'',metasenv'' =
217        List.fold_right
218         (fun x (res,subst,metasenv) ->
219           let ty,subst',metasenv' =
220            type_of_aux subst metasenv context x
221           in
222            (x, ty)::res,subst',metasenv'
223         ) tl ([],subst',metasenv')
224       in
225        eat_prods subst'' metasenv'' context hetype tlbody_and_type
226    | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
227    | C.Const (uri,exp_named_subst) ->
228       incr fdebug ;
229       let subst',metasenv' =
230        check_exp_named_subst subst metasenv context exp_named_subst in
231       let cty =
232        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
233       in
234        decr fdebug ;
235        cty,subst',metasenv'
236    | C.MutInd (uri,i,exp_named_subst) ->
237       incr fdebug ;
238       let subst',metasenv' =
239        check_exp_named_subst subst metasenv context exp_named_subst in
240       let cty =
241        CicSubstitution.subst_vars exp_named_subst
242         (type_of_mutual_inductive_defs uri i)
243       in
244        decr fdebug ;
245        cty,subst',metasenv'
246    | C.MutConstruct (uri,i,j,exp_named_subst) ->
247       let subst',metasenv' =
248        check_exp_named_subst subst metasenv context exp_named_subst in
249       let cty =
250        CicSubstitution.subst_vars exp_named_subst
251         (type_of_mutual_inductive_constr uri i j)
252       in
253        cty,subst',metasenv'
254    | C.MutCase (uri, i, outtype, term, pl) ->
255        (* first, get the inductive type (and noparams) in the environment  *)
256        let (_,b,arity,constructors), expl_params, no_left_params =
257          match CicEnvironment.get_cooked_obj ~trust:true uri with
258             C.InductiveDefinition (l,expl_params,parsno) -> 
259               List.nth l i , expl_params, parsno
260           | _ ->
261             raise
262              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
263        let rec count_prod t =
264          match CicMetaSubst.whd subst context t with
265              C.Prod (_, _, t) -> 1 + (count_prod t)
266            | _ -> 0 in 
267        let no_args = count_prod arity in
268        (* now, create a "generic" MutInd *)
269        let metasenv,left_args = 
270          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
271        let metasenv,right_args = 
272          let no_right_params = no_args - no_left_params in
273          if no_right_params < 0 then assert false
274          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
275        let metasenv,exp_named_subst = 
276          CicMkImplicit.fresh_subst metasenv context expl_params in
277        let expected_type = 
278          if no_args = 0 then 
279            C.MutInd (uri,i,exp_named_subst)
280          else
281            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
282        in
283        (* check consistency with the actual type of term *)
284        let actual_type,subst,metasenv = 
285          type_of_aux subst metasenv context term in
286        let _, subst, metasenv =
287          type_of_aux subst metasenv context expected_type
288        in
289        let actual_type = CicMetaSubst.whd subst context actual_type in
290        let subst,metasenv =
291          Un.fo_unif_subst subst context metasenv expected_type actual_type
292        in
293        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
294        let (_,outtypeinstances,subst,metasenv) =
295           List.fold_left
296            (fun (j,outtypeinstances,subst,metasenv) p ->
297              let constructor =
298               if left_args = [] then
299                (C.MutConstruct (uri,i,j,exp_named_subst))
300               else
301                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
302              in
303              let actual_type,subst,metasenv = 
304                type_of_aux subst metasenv context p in
305              let expected_type, subst, metasenv = 
306                type_of_aux subst metasenv context constructor in
307              let outtypeinstance,subst,metasenv =
308                check_branch 
309                 0 context metasenv subst 
310                 no_left_params actual_type constructor expected_type in
311              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
312             (1,[],subst,metasenv) pl in
313         (* we are left to check that the outype matches his instances.
314            The easy case is when the outype is specified, that amount
315            to a trivial check. Otherwise, we should guess a type from
316            its instances *)
317         (* easy case *)
318         let _, subst, metasenv =
319           type_of_aux subst metasenv context
320             (C.Appl ((outtype :: right_args) @ [term]))
321         in
322         let (subst,metasenv) = 
323           List.fold_left
324             (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
325               let instance' = 
326                 let appl =
327                   let outtype' =
328                     CicSubstitution.lift constructor_args_no outtype
329                   in
330                   C.Appl (outtype'::args)
331                 in
332 (*
333                 (* if appl is not well typed then the type_of below solves the
334                  * problem *)
335                 let (_, subst, metasenv) =
336                   type_of_aux subst metasenv context appl
337                 in
338 *)
339                 CicMetaSubst.whd subst context appl
340               in
341                Un.fo_unif_subst subst context metasenv instance instance')
342              (subst,metasenv) outtypeinstances in
343         CicMetaSubst.whd subst
344           context (C.Appl(outtype::right_args@[term])),subst,metasenv
345    | C.Fix (i,fl) ->
346       let subst,metasenv,types =
347        List.fold_left
348         (fun (subst,metasenv,types) (n,_,ty,_) ->
349           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
350            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
351         ) (subst,metasenv,[]) fl
352       in
353        let len = List.length types in
354        let context' = types@context in
355        let subst,metasenv =
356         List.fold_left
357          (fun (subst,metasenv) (name,x,ty,bo) ->
358            let ty_of_bo,subst,metasenv =
359             type_of_aux subst metasenv context' bo
360            in
361             Un.fo_unif_subst subst context' metasenv
362               ty_of_bo (CicMetaSubst.lift subst len ty)
363          ) (subst,metasenv) fl in
364         let (_,_,ty,_) = List.nth fl i in
365          ty,subst,metasenv
366    | C.CoFix (i,fl) ->
367       let subst,metasenv,types =
368        List.fold_left
369         (fun (subst,metasenv,types) (n,ty,_) ->
370           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
371            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
372         ) (subst,metasenv,[]) fl
373       in
374        let len = List.length types in
375        let context' = types@context in
376        let subst,metasenv =
377         List.fold_left
378          (fun (subst,metasenv) (name,ty,bo) ->
379            let ty_of_bo,subst,metasenv =
380             type_of_aux subst metasenv context' bo
381            in
382             Un.fo_unif_subst subst context' metasenv
383               ty_of_bo (CicMetaSubst.lift subst len ty)
384          ) (subst,metasenv) fl in
385       
386         let (_,ty,_) = List.nth fl i in
387          ty,subst,metasenv
388
389  (* check_metasenv_consistency checks that the "canonical" context of a
390  metavariable is consitent - up to relocation via the relocation list l -
391  with the actual context *)
392  and check_metasenv_consistency
393   metano subst metasenv context canonical_context l
394  =
395    let module C = Cic in
396    let module R = CicReduction in
397    let module S = CicSubstitution in
398     let lifted_canonical_context = 
399      let rec aux i =
400       function
401          [] -> []
402        | (Some (n,C.Decl t))::tl ->
403           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
404        | (Some (n,C.Def (t,None)))::tl ->
405           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
406        | None::tl -> None::(aux (i+1) tl)
407        | (Some (n,C.Def (t,Some ty)))::tl ->
408            (Some (n,
409             C.Def ((S.lift_meta l (S.lift i t)),
410               Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
411      in
412       aux 1 canonical_context
413     in
414      List.fold_left2 
415       (fun (subst,metasenv) t ct -> 
416         match (t,ct) with
417            _,None ->
418              subst,metasenv
419          | Some t,Some (_,C.Def (ct,_)) ->
420             (try
421               CicUnification.fo_unif_subst subst context metasenv t ct
422              with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
423          | Some t,Some (_,C.Decl ct) ->
424             let inferredty,subst',metasenv' =
425              type_of_aux subst metasenv context t
426             in
427              (try
428                CicUnification.fo_unif_subst
429                 subst' context metasenv' inferredty ct
430              with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
431          | None, Some _  ->
432              raise (NotRefinable (sprintf
433               "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
434               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
435               (CicMetaSubst.ppcontext subst canonical_context)))
436       ) (subst,metasenv) l lifted_canonical_context 
437
438  and check_exp_named_subst metasubst metasenv context =
439   let rec check_exp_named_subst_aux metasubst metasenv substs =
440    function
441       [] -> metasubst,metasenv
442     | ((uri,t) as subst)::tl ->
443        let typeofvar =
444         CicSubstitution.subst_vars substs (type_of_variable uri) in
445        (match CicEnvironment.get_cooked_obj ~trust:false uri with
446            Cic.Variable (_,Some bo,_,_) ->
447             raise
448              (NotRefinable
449                "A variable with a body can not be explicit substituted")
450          | Cic.Variable (_,None,_,_) -> ()
451          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
452        ) ;
453        let typeoft,metasubst',metasenv' =
454         type_of_aux metasubst metasenv context t
455        in
456         try
457          let metasubst'',metasenv'' =
458           CicUnification.fo_unif_subst
459            metasubst' context metasenv' typeoft typeofvar
460          in
461           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
462         with _ ->
463          raise (NotRefinable "Wrong Explicit Named Substitution")
464   in
465    check_exp_named_subst_aux metasubst metasenv []
466
467  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
468   let module C = Cic in
469     let t1'' = CicMetaSubst.whd subst context t1 in
470     let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
471     match (t1'', t2'') with
472        (C.Sort s1, C.Sort s2)
473          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
474           C.Sort s2,subst,metasenv
475      | (C.Sort s1, C.Sort s2) ->
476          (*CSC manca la gestione degli universi!!! *)
477          C.Sort C.Type,subst,metasenv
478      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
479      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
480          (* TODO how can we force the meta to become a sort? If we don't we
481           * brake the invariant that refine produce only well typed terms *)
482          (* TODO if we check the non meta term and if it is a sort then we are
483           * likely to know the exact value of the result e.g. if the rhs is a
484           * Sort (Prop | Set | CProp) then the result is the rhs *)
485          let (metasenv,idx) =
486           CicMkImplicit.mk_implicit metasenv [] in
487          let (subst, metasenv) =
488           CicUnification.fo_unif_subst subst context metasenv
489            (C.Meta (idx,[])) t2''
490          in
491           t2'',subst,metasenv
492      | (_,_) ->
493          raise (NotRefinable (sprintf
494           "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
495           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
496           (CicPp.ppterm t2'')))
497
498  and eat_prods subst metasenv context hetype tlbody_and_type =
499   let rec aux context' args (resty,subst,metasenv) =
500    function
501       [] -> resty,subst,metasenv
502     | (arg,argty)::tl ->
503        let args' =
504         List.map
505          (function
506              None -> assert false
507            | Some t -> Some (CicMetaSubst.lift subst 1 t)
508          ) args in
509        let argty' = CicMetaSubst.lift subst (List.length args) argty in
510        let name =
511         (* The name must be fresh for (context'@context).      *)
512         (* Nevertheless, argty is well-typed only in context.  *)
513         (* Thus I generate a name (name_hint) in context and   *)
514         (* then I generate a name --- using the hint name_hint *)
515         (* --- that is fresh in (context'@context).            *)
516         let name_hint =
517          FreshNamesGenerator.mk_fresh_name
518           (CicMetaSubst.apply_subst_metasenv subst metasenv)
519           (CicMetaSubst.apply_subst_context subst context)
520           Cic.Anonymous
521           (CicMetaSubst.apply_subst subst argty)
522         in
523          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
524          FreshNamesGenerator.mk_fresh_name
525           [] (context'@context) name_hint (Cic.Sort Cic.Prop)
526        in
527        let context'' = Some (name, Cic.Decl argty') :: context' in
528        let (metasenv, idx) =
529         CicMkImplicit.mk_implicit metasenv (context'' @ context) in
530        let irl =
531          (Some (Cic.Rel 1))::args' @
532           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
533             context)
534        in
535        let newmeta = Cic.Meta (idx, irl) in
536        let prod = Cic.Prod (name, argty, newmeta) in
537        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
538        let (subst, metasenv) =
539          CicUnification.fo_unif_subst subst context metasenv resty prod
540        in
541         aux context'' (Some arg :: args)
542          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
543   in
544    aux [] [] (hetype,subst,metasenv) tlbody_and_type
545
546  in
547   let ty,subst',metasenv' =
548    type_of_aux [] metasenv context t
549   in
550    let substituted_t = CicMetaSubst.apply_subst subst' t in
551    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
552    let substituted_metasenv =
553     CicMetaSubst.apply_subst_metasenv subst' metasenv'
554    in
555     let cleaned_t =
556      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
557     let cleaned_ty =
558      FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
559     let cleaned_metasenv =
560      List.map
561       (function (n,context,ty) ->
562         let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
563         let context' =
564          List.map
565           (function
566               None -> None
567             | Some (n, Cic.Decl t) ->
568                Some (n,
569                 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
570             | Some (n, Cic.Def (bo,ty)) ->
571                let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
572                let ty' =
573                 match ty with
574                    None -> None
575                  | Some ty ->
576                     Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
577                in
578                 Some (n, Cic.Def (bo',ty'))
579           ) context
580         in
581          (n,context',ty')
582       ) substituted_metasenv
583     in
584      (cleaned_t,cleaned_ty,cleaned_metasenv)
585
586 ;;
587
588 (* DEBUGGING ONLY *)
589 let type_of_aux' metasenv context term =
590  try
591   let (t,ty,m) = type_of_aux' metasenv context term in
592    debug_print
593     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
594 (*
595    debug_print
596     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
597 *)
598    (t,ty,m)
599  with
600  | CicUnification.AssertFailure msg as e ->
601      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
602      debug_print msg;
603      raise e
604  | CicUnification.UnificationFailure msg as e ->
605      debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
606      debug_print msg;
607      raise e
608  | e ->
609    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
610    raise e
611 ;;
612