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/.
28 exception RefineFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
32 let debug_print = prerr_endline
34 let fo_unif_subst subst context metasenv t1 t2 =
36 CicUnification.fo_unif_subst subst context metasenv t1 t2
38 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
39 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
45 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
46 | (_,_) -> raise (AssertFailure "split: list too short")
49 let rec type_of_constant uri =
51 let module R = CicReduction in
52 let module U = UriManager in
53 match CicEnvironment.get_cooked_obj uri with
54 C.Constant (_,_,ty,_) -> ty
55 | C.CurrentProof (_,_,_,ty,_) -> ty
58 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
60 and type_of_variable uri =
62 let module R = CicReduction in
63 let module U = UriManager in
64 match CicEnvironment.get_cooked_obj uri with
65 C.Variable (_,_,ty,_) -> ty
69 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
71 and type_of_mutual_inductive_defs uri i =
73 let module R = CicReduction in
74 let module U = UriManager in
75 match CicEnvironment.get_cooked_obj uri with
76 C.InductiveDefinition (dl,_,_) ->
77 let (_,_,arity,_) = List.nth dl i in
82 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
84 and type_of_mutual_inductive_constr uri i j =
86 let module R = CicReduction in
87 let module U = UriManager in
88 match CicEnvironment.get_cooked_obj uri with
89 C.InductiveDefinition (dl,_,_) ->
90 let (_,_,_,cl) = List.nth dl i in
91 let (_,ty) = List.nth cl (j-1) in
96 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
98 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
100 (* the check_branch function checks if a branch of a case is refinable.
101 It returns a pair (outype_instance,args), a subst and a metasenv.
102 outype_instance is the expected result of applying the case outtype
104 The problem is that outype is in general unknown, and we should
105 try to synthesize it from the above information, that is in general
106 a second order unification problem. *)
108 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
109 let module C = Cic in
110 (* let module R = CicMetaSubst in *)
111 let module R = CicReduction in
112 match R.whd ~subst context expectedtype with
114 (n,context,actualtype, [term]), subst, metasenv
115 | C.Appl (C.MutInd (_,_,_)::tl) ->
116 let (_,arguments) = split tl left_args_no in
117 (n,context,actualtype, arguments@[term]), subst, metasenv
118 | C.Prod (name,so,de) ->
119 (* we expect that the actual type of the branch has the due
121 (match R.whd ~subst context actualtype with
122 C.Prod (name',so',de') ->
123 let subst, metasenv =
124 fo_unif_subst subst context metasenv so so' in
126 (match CicSubstitution.lift 1 term with
127 C.Appl l -> C.Appl (l@[C.Rel 1])
128 | t -> C.Appl [t ; C.Rel 1]) in
129 (* we should also check that the name variable is anonymous in
130 the actual type de' ?? *)
131 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
132 | _ -> raise (AssertFailure "Wrong number of arguments"))
133 | _ -> raise (AssertFailure "Prod or MutInd expected")
135 and type_of_aux' metasenv context t =
136 let rec type_of_aux subst metasenv context t =
137 let module C = Cic in
138 let module S = CicSubstitution in
139 let module U = UriManager in
144 match List.nth context (n - 1) with
145 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
146 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
147 | Some (_,C.Def (bo,None)) ->
148 type_of_aux subst metasenv context (S.lift n bo)
149 | None -> raise (RefineFailure "Rel to hidden hypothesis")
151 _ -> raise (RefineFailure "Not a close term")
153 | C.Var (uri,exp_named_subst) ->
154 let subst',metasenv' =
155 check_exp_named_subst subst metasenv context exp_named_subst in
157 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
162 let (canonical_context, term) = CicUtil.lookup_subst n subst in
164 check_metasenv_consistency n subst metasenv context
167 type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
168 with CicUtil.Subst_not_found _ ->
169 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
171 check_metasenv_consistency n subst metasenv context
174 CicSubstitution.lift_meta l ty, subst, metasenv)
175 (* TASSI: CONSTRAINT *)
176 | C.Sort (C.Type t) ->
177 let t' = CicUniv.fresh() in
178 if not (CicUniv.add_gt t' t ) then
179 assert false (* t' is fresh! an error in CicUniv *)
181 C.Sort (C.Type t'),subst,metasenv
182 (* TASSI: CONSTRAINT *)
183 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
184 | C.Implicit _ -> raise (AssertFailure "21")
186 let _,subst',metasenv' =
187 type_of_aux subst metasenv context ty in
188 let inferredty,subst'',metasenv'' =
189 type_of_aux subst' metasenv' context te
192 let subst''',metasenv''' =
193 fo_unif_subst subst'' context metasenv'' inferredty ty
195 ty,subst''',metasenv'''
197 _ -> raise (RefineFailure "Cast"))
198 | C.Prod (name,s,t) ->
199 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
200 let sort2,subst'',metasenv'' =
201 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
203 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
204 | C.Lambda (n,s,t) ->
205 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
206 (match CicReduction.whd ~subst:subst' context sort1 with
210 raise (RefineFailure (sprintf
211 "Not well-typed lambda-abstraction: the source %s should be a type;
212 instead it is a term of type %s" (CicPp.ppterm s)
213 (CicPp.ppterm sort1)))
215 let type2,subst'',metasenv'' =
216 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
218 C.Prod (n,s,type2),subst'',metasenv''
220 (* only to check if s is well-typed *)
221 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
222 let inferredty,subst'',metasenv'' =
223 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
225 (* One-step LetIn reduction. Even faster than the previous solution.
226 Moreover the inferred type is closer to the expected one. *)
227 CicSubstitution.subst s inferredty,subst',metasenv'
228 | C.Appl (he::((_::_) as tl)) ->
229 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
230 let tlbody_and_type,subst'',metasenv'' =
232 (fun x (res,subst,metasenv) ->
233 let ty,subst',metasenv' =
234 type_of_aux subst metasenv context x
236 (x, ty)::res,subst',metasenv'
237 ) tl ([],subst',metasenv')
239 eat_prods subst'' metasenv'' context hetype tlbody_and_type
240 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
241 | C.Const (uri,exp_named_subst) ->
242 let subst',metasenv' =
243 check_exp_named_subst subst metasenv context exp_named_subst in
245 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
248 | C.MutInd (uri,i,exp_named_subst) ->
249 let subst',metasenv' =
250 check_exp_named_subst subst metasenv context exp_named_subst in
252 CicSubstitution.subst_vars exp_named_subst
253 (type_of_mutual_inductive_defs uri i)
256 | C.MutConstruct (uri,i,j,exp_named_subst) ->
257 let subst',metasenv' =
258 check_exp_named_subst subst metasenv context exp_named_subst in
260 CicSubstitution.subst_vars exp_named_subst
261 (type_of_mutual_inductive_constr uri i j)
264 | C.MutCase (uri, i, outtype, term, pl) ->
265 (* first, get the inductive type (and noparams) in the environment *)
266 let (_,b,arity,constructors), expl_params, no_left_params =
267 match CicEnvironment.get_cooked_obj ~trust:true uri with
268 C.InductiveDefinition (l,expl_params,parsno) ->
269 List.nth l i , expl_params, parsno
273 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
274 let rec count_prod t =
275 match CicReduction.whd ~subst context t with
276 C.Prod (_, _, t) -> 1 + (count_prod t)
278 let no_args = count_prod arity in
279 (* now, create a "generic" MutInd *)
280 let metasenv,left_args =
281 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
282 let metasenv,right_args =
283 let no_right_params = no_args - no_left_params in
284 if no_right_params < 0 then assert false
285 else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
286 let metasenv,exp_named_subst =
287 CicMkImplicit.fresh_subst metasenv subst context expl_params in
290 C.MutInd (uri,i,exp_named_subst)
292 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
294 (* check consistency with the actual type of term *)
295 let actual_type,subst,metasenv =
296 type_of_aux subst metasenv context term in
297 let _, subst, metasenv =
298 type_of_aux subst metasenv context expected_type
300 let actual_type = CicReduction.whd ~subst context actual_type in
302 fo_unif_subst subst context metasenv expected_type actual_type
304 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
305 let (_,outtypeinstances,subst,metasenv) =
307 (fun (j,outtypeinstances,subst,metasenv) p ->
309 if left_args = [] then
310 (C.MutConstruct (uri,i,j,exp_named_subst))
312 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
314 let actual_type,subst,metasenv =
315 type_of_aux subst metasenv context p in
316 let expected_type, subst, metasenv =
317 type_of_aux subst metasenv context constructor in
318 let outtypeinstance,subst,metasenv =
320 0 context metasenv subst
321 no_left_params actual_type constructor expected_type in
322 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
323 (1,[],subst,metasenv) pl in
324 (* we are left to check that the outype matches his instances.
325 The easy case is when the outype is specified, that amount
326 to a trivial check. Otherwise, we should guess a type from
330 let _, subst, metasenv =
331 type_of_aux subst metasenv context
332 (C.Appl ((outtype :: right_args) @ [term]))
334 let (subst,metasenv) =
336 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
340 CicSubstitution.lift constructor_args_no outtype
342 C.Appl (outtype'::args)
345 (* if appl is not well typed then the type_of below solves the
347 let (_, subst, metasenv) =
348 type_of_aux subst metasenv context appl
352 let prova1 = CicMetaSubst.whd subst context appl in
353 let prova2 = CicReduction.whd ~subst context appl in
354 if not (prova1 = prova2) then
356 prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
357 prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
360 (* CicMetaSubst.whd subst context appl *)
361 CicReduction.whd ~subst context appl
363 fo_unif_subst subst context metasenv instance instance')
364 (subst,metasenv) outtypeinstances in
365 CicReduction.whd ~subst
366 context (C.Appl(outtype::right_args@[term])),subst,metasenv
368 let subst,metasenv,types =
370 (fun (subst,metasenv,types) (n,_,ty,_) ->
371 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
372 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
373 ) (subst,metasenv,[]) fl
375 let len = List.length types in
376 let context' = types@context in
379 (fun (subst,metasenv) (name,x,ty,bo) ->
380 let ty_of_bo,subst,metasenv =
381 type_of_aux subst metasenv context' bo
383 fo_unif_subst subst context' metasenv
384 ty_of_bo (CicSubstitution.lift len ty)
385 ) (subst,metasenv) fl in
386 let (_,_,ty,_) = List.nth fl i in
389 let subst,metasenv,types =
391 (fun (subst,metasenv,types) (n,ty,_) ->
392 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
393 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
394 ) (subst,metasenv,[]) fl
396 let len = List.length types in
397 let context' = types@context in
400 (fun (subst,metasenv) (name,ty,bo) ->
401 let ty_of_bo,subst,metasenv =
402 type_of_aux subst metasenv context' bo
404 fo_unif_subst subst context' metasenv
405 ty_of_bo (CicSubstitution.lift len ty)
406 ) (subst,metasenv) fl in
408 let (_,ty,_) = List.nth fl i in
411 (* check_metasenv_consistency checks that the "canonical" context of a
412 metavariable is consitent - up to relocation via the relocation list l -
413 with the actual context *)
414 and check_metasenv_consistency
415 metano subst metasenv context canonical_context l
417 let module C = Cic in
418 let module R = CicReduction in
419 let module S = CicSubstitution in
420 let lifted_canonical_context =
424 | (Some (n,C.Decl t))::tl ->
425 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
426 | (Some (n,C.Def (t,None)))::tl ->
427 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
428 | None::tl -> None::(aux (i+1) tl)
429 | (Some (n,C.Def (t,Some ty)))::tl ->
431 C.Def ((S.lift_meta l (S.lift i t)),
432 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
434 aux 1 canonical_context
438 (fun (subst,metasenv) t ct ->
442 | Some t,Some (_,C.Def (ct,_)) ->
444 fo_unif_subst subst context metasenv t ct
445 with e -> raise (RefineFailure (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 AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
446 | Some t,Some (_,C.Decl ct) ->
447 let inferredty,subst',metasenv' =
448 type_of_aux subst metasenv context t
452 subst' context metasenv' inferredty ct
453 with e -> raise (RefineFailure (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 AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
455 raise (RefineFailure (sprintf
456 "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"
457 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
458 (CicMetaSubst.ppcontext subst canonical_context)))
459 ) (subst,metasenv) l lifted_canonical_context
461 Invalid_argument _ ->
465 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
466 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
467 (CicMetaSubst.ppcontext subst canonical_context)))
469 and check_exp_named_subst metasubst metasenv context =
470 let rec check_exp_named_subst_aux metasubst metasenv substs =
472 [] -> metasubst,metasenv
473 | ((uri,t) as subst)::tl ->
475 CicSubstitution.subst_vars substs (type_of_variable uri) in
476 (* CSC: why was this code here? it is wrong
477 (match CicEnvironment.get_cooked_obj ~trust:false uri with
478 Cic.Variable (_,Some bo,_,_) ->
481 "A variable with a body can not be explicit substituted")
482 | Cic.Variable (_,None,_,_) -> ()
486 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
489 let typeoft,metasubst',metasenv' =
490 type_of_aux metasubst metasenv context t
492 let metasubst'',metasenv'' =
494 fo_unif_subst metasubst' context metasenv' typeoft typeofvar
497 ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
498 " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
500 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
502 check_exp_named_subst_aux metasubst metasenv []
504 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
505 let module C = Cic in
506 let context_for_t2 = (Some (name,C.Decl s))::context in
507 let t1'' = CicReduction.whd ~subst context t1 in
508 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
509 match (t1'', t2'') with
510 (C.Sort s1, C.Sort s2)
511 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
512 C.Sort s2,subst,metasenv
513 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
514 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
515 let t' = CicUniv.fresh() in
516 if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
517 assert false ; (* not possible, error in CicUniv *)
518 C.Sort (C.Type t'),subst,metasenv
519 | (C.Sort _,C.Sort (C.Type t1)) ->
520 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
521 C.Sort (C.Type t1),subst,metasenv
522 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
523 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
524 (* TODO how can we force the meta to become a sort? If we don't we
525 * brake the invariant that refine produce only well typed terms *)
526 (* TODO if we check the non meta term and if it is a sort then we are
527 * likely to know the exact value of the result e.g. if the rhs is a
528 * Sort (Prop | Set | CProp) then the result is the rhs *)
530 CicMkImplicit.mk_implicit_sort metasenv subst in
531 let (subst, metasenv) =
532 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
536 raise (RefineFailure (sprintf
537 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
538 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
539 (CicPp.ppterm t2'')))
541 and eat_prods subst metasenv context hetype tlbody_and_type =
542 let rec mk_prod metasenv context =
545 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
547 CicMkImplicit.identity_relocation_list_for_metavariable context
549 metasenv,Cic.Meta (idx, irl)
551 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
553 CicMkImplicit.identity_relocation_list_for_metavariable context
555 let meta = Cic.Meta (idx,irl) in
557 (* The name must be fresh for context. *)
558 (* Nevertheless, argty is well-typed only in context. *)
559 (* Thus I generate a name (name_hint) in context and *)
560 (* then I generate a name --- using the hint name_hint *)
561 (* --- that is fresh in (context'@context). *)
563 (* Cic.Name "pippo" *)
564 FreshNamesGenerator.mk_fresh_name metasenv
565 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
566 (CicMetaSubst.apply_subst_context subst context)
568 (CicMetaSubst.apply_subst subst argty)
570 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
571 FreshNamesGenerator.mk_fresh_name
572 [] context name_hint (Cic.Sort Cic.Prop)
574 let metasenv,target =
575 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
577 metasenv,Cic.Prod (name,meta,target)
579 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
580 let (subst, metasenv) =
581 fo_unif_subst subst context metasenv hetype hetype'
583 let rec eat_prods metasenv subst context hetype =
585 [] -> metasenv,subst,hetype
586 | (hete, hety)::tl ->
590 fo_unif_subst subst context metasenv hety s
593 fo_unif_subst subst context metasenv hety s
595 prerr_endline("senza subst fallisce");
596 let hety = CicMetaSubst.apply_subst subst hety in
597 let s = CicMetaSubst.apply_subst subst s in
598 prerr_endline ("unifico = " ^(CicPp.ppterm hety));
599 prerr_endline ("con = " ^(CicPp.ppterm s));
600 fo_unif_subst subst context metasenv hety s *)
603 let t1 = CicMetaSubst.subst subst hete t in
604 let t2 = CicSubstitution.subst hete t in
605 prerr_endline ("con subst = " ^(CicPp.ppterm t1));
606 prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
607 prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
608 (CicMetaSubst.ppmetasenv metasenv subst));
609 prerr_endline("++++++++++subst prima di eat_prods:\n" ^
610 (CicMetaSubst.ppsubst subst));
612 eat_prods metasenv subst context
613 (* (CicMetaSubst.subst subst hete t) tl *)
614 (CicSubstitution.subst hete t) tl
618 let metasenv,subst,t =
619 eat_prods metasenv subst context hetype' tlbody_and_type
623 let rec aux context' args (resty,subst,metasenv) =
625 [] -> resty,subst,metasenv
631 | Some t -> Some (CicMetaSubst.lift subst 1 t)
633 let argty' = CicMetaSubst.lift subst (List.length args) argty in
635 (* The name must be fresh for (context'@context). *)
636 (* Nevertheless, argty is well-typed only in context. *)
637 (* Thus I generate a name (name_hint) in context and *)
638 (* then I generate a name --- using the hint name_hint *)
639 (* --- that is fresh in (context'@context). *)
641 FreshNamesGenerator.mk_fresh_name
642 (CicMetaSubst.apply_subst_metasenv subst metasenv)
643 (CicMetaSubst.apply_subst_context subst context)
645 (CicMetaSubst.apply_subst subst argty)
647 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
648 FreshNamesGenerator.mk_fresh_name
649 [] (context'@context) name_hint (Cic.Sort Cic.Prop)
651 let context'' = Some (name, Cic.Decl argty') :: context' in
652 let (metasenv, idx) =
653 CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
655 (Some (Cic.Rel 1))::args' @
656 (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
659 let newmeta = Cic.Meta (idx, irl) in
660 let prod = Cic.Prod (name, argty, newmeta) in
661 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
662 let (subst, metasenv) =
663 fo_unif_subst subst context metasenv resty prod
665 aux context'' (Some arg :: args)
666 (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
668 aux [] [] (hetype,subst,metasenv) tlbody_and_type
671 let ty,subst',metasenv' =
672 type_of_aux [] metasenv context t
674 let substituted_t = CicMetaSubst.apply_subst subst' t in
675 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
676 (* Andrea: ho rimesso qui l'applicazione della subst al
677 metasenv dopo che ho droppato l'invariante che il metsaenv
678 e' sempre istanziato *)
679 let substituted_metasenv =
680 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
682 (* substituted_t,substituted_ty,substituted_metasenv *)
683 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
685 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
687 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
688 let cleaned_metasenv =
690 (function (n,context,ty) ->
691 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
696 | Some (n, Cic.Decl t) ->
698 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
699 | Some (n, Cic.Def (bo,ty)) ->
700 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
705 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
707 Some (n, Cic.Def (bo',ty'))
711 ) substituted_metasenv
713 (cleaned_t,cleaned_ty,cleaned_metasenv)
719 let type_of_aux' metasenv context term =
722 type_of_aux' metasenv context term in
724 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
726 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
729 | RefineFailure msg as e ->
730 debug_print ("@@@ REFINE FAILED: " ^ msg);
732 | Uncertain msg as e ->
733 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);