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,ty) = CicUtil.lookup_subst n subst in
164 check_metasenv_consistency n subst metasenv context
167 (* trust or check ??? *)
168 CicSubstitution.lift_meta l ty, subst, metasenv
169 (* type_of_aux subst metasenv
170 context (CicSubstitution.lift_meta l term) *)
171 with CicUtil.Subst_not_found _ ->
172 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
174 check_metasenv_consistency n subst metasenv context
177 CicSubstitution.lift_meta l ty, subst, metasenv)
178 (* TASSI: CONSTRAINT *)
179 | C.Sort (C.Type t) ->
180 let t' = CicUniv.fresh() in
181 if not (CicUniv.add_gt t' t ) then
182 assert false (* t' is fresh! an error in CicUniv *)
184 C.Sort (C.Type t'),subst,metasenv
185 (* TASSI: CONSTRAINT *)
186 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
187 | C.Implicit _ -> raise (AssertFailure "21")
189 let _,subst',metasenv' =
190 type_of_aux subst metasenv context ty in
191 let inferredty,subst'',metasenv'' =
192 type_of_aux subst' metasenv' context te
195 let subst''',metasenv''' =
196 fo_unif_subst subst'' context metasenv'' inferredty ty
198 ty,subst''',metasenv'''
200 _ -> raise (RefineFailure "Cast"))
201 | C.Prod (name,s,t) ->
202 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
203 let sort2,subst'',metasenv'' =
204 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
206 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
207 | C.Lambda (n,s,t) ->
208 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
209 (match CicReduction.whd ~subst:subst' context sort1 with
213 raise (RefineFailure (sprintf
214 "Not well-typed lambda-abstraction: the source %s should be a type;
215 instead it is a term of type %s" (CicPp.ppterm s)
216 (CicPp.ppterm sort1)))
218 let type2,subst'',metasenv'' =
219 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
221 C.Prod (n,s,type2),subst'',metasenv''
223 (* only to check if s is well-typed *)
224 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
225 let inferredty,subst'',metasenv'' =
226 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
228 (* One-step LetIn reduction. Even faster than the previous solution.
229 Moreover the inferred type is closer to the expected one. *)
230 CicSubstitution.subst s inferredty,subst',metasenv'
231 | C.Appl (he::((_::_) as tl)) ->
232 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
233 let tlbody_and_type,subst'',metasenv'' =
235 (fun x (res,subst,metasenv) ->
236 let ty,subst',metasenv' =
237 type_of_aux subst metasenv context x
239 (x, ty)::res,subst',metasenv'
240 ) tl ([],subst',metasenv')
242 eat_prods subst'' metasenv'' context hetype tlbody_and_type
243 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
244 | C.Const (uri,exp_named_subst) ->
245 let subst',metasenv' =
246 check_exp_named_subst subst metasenv context exp_named_subst in
248 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
251 | C.MutInd (uri,i,exp_named_subst) ->
252 let subst',metasenv' =
253 check_exp_named_subst subst metasenv context exp_named_subst in
255 CicSubstitution.subst_vars exp_named_subst
256 (type_of_mutual_inductive_defs uri i)
259 | C.MutConstruct (uri,i,j,exp_named_subst) ->
260 let subst',metasenv' =
261 check_exp_named_subst subst metasenv context exp_named_subst in
263 CicSubstitution.subst_vars exp_named_subst
264 (type_of_mutual_inductive_constr uri i j)
267 | C.MutCase (uri, i, outtype, term, pl) ->
268 (* first, get the inductive type (and noparams) in the environment *)
269 let (_,b,arity,constructors), expl_params, no_left_params =
270 match CicEnvironment.get_cooked_obj ~trust:true uri with
271 C.InductiveDefinition (l,expl_params,parsno) ->
272 List.nth l i , expl_params, parsno
276 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
277 let rec count_prod t =
278 match CicReduction.whd ~subst context t with
279 C.Prod (_, _, t) -> 1 + (count_prod t)
281 let no_args = count_prod arity in
282 (* now, create a "generic" MutInd *)
283 let metasenv,left_args =
284 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
285 let metasenv,right_args =
286 let no_right_params = no_args - no_left_params in
287 if no_right_params < 0 then assert false
288 else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
289 let metasenv,exp_named_subst =
290 CicMkImplicit.fresh_subst metasenv subst context expl_params in
293 C.MutInd (uri,i,exp_named_subst)
295 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
297 (* check consistency with the actual type of term *)
298 let actual_type,subst,metasenv =
299 type_of_aux subst metasenv context term in
300 let _, subst, metasenv =
301 type_of_aux subst metasenv context expected_type
303 let actual_type = CicReduction.whd ~subst context actual_type in
305 fo_unif_subst subst context metasenv expected_type actual_type
307 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
308 let (_,outtypeinstances,subst,metasenv) =
310 (fun (j,outtypeinstances,subst,metasenv) p ->
312 if left_args = [] then
313 (C.MutConstruct (uri,i,j,exp_named_subst))
315 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
317 let actual_type,subst,metasenv =
318 type_of_aux subst metasenv context p in
319 let expected_type, subst, metasenv =
320 type_of_aux subst metasenv context constructor in
321 let outtypeinstance,subst,metasenv =
323 0 context metasenv subst
324 no_left_params actual_type constructor expected_type in
325 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
326 (1,[],subst,metasenv) pl in
327 (* we are left to check that the outype matches his instances.
328 The easy case is when the outype is specified, that amount
329 to a trivial check. Otherwise, we should guess a type from
333 let _, subst, metasenv =
334 type_of_aux subst metasenv context
335 (C.Appl ((outtype :: right_args) @ [term]))
337 let (subst,metasenv) =
339 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
343 CicSubstitution.lift constructor_args_no outtype
345 C.Appl (outtype'::args)
348 (* if appl is not well typed then the type_of below solves the
350 let (_, subst, metasenv) =
351 type_of_aux subst metasenv context appl
355 let prova1 = CicMetaSubst.whd subst context appl in
356 let prova2 = CicReduction.whd ~subst context appl in
357 if not (prova1 = prova2) then
359 prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
360 prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
363 (* CicMetaSubst.whd subst context appl *)
364 CicReduction.whd ~subst context appl
366 fo_unif_subst subst context metasenv instance instance')
367 (subst,metasenv) outtypeinstances in
368 CicReduction.whd ~subst
369 context (C.Appl(outtype::right_args@[term])),subst,metasenv
371 let subst,metasenv,types =
373 (fun (subst,metasenv,types) (n,_,ty,_) ->
374 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
375 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
376 ) (subst,metasenv,[]) fl
378 let len = List.length types in
379 let context' = types@context in
382 (fun (subst,metasenv) (name,x,ty,bo) ->
383 let ty_of_bo,subst,metasenv =
384 type_of_aux subst metasenv context' bo
386 fo_unif_subst subst context' metasenv
387 ty_of_bo (CicSubstitution.lift len ty)
388 ) (subst,metasenv) fl in
389 let (_,_,ty,_) = List.nth fl i in
392 let subst,metasenv,types =
394 (fun (subst,metasenv,types) (n,ty,_) ->
395 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
396 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
397 ) (subst,metasenv,[]) fl
399 let len = List.length types in
400 let context' = types@context in
403 (fun (subst,metasenv) (name,ty,bo) ->
404 let ty_of_bo,subst,metasenv =
405 type_of_aux subst metasenv context' bo
407 fo_unif_subst subst context' metasenv
408 ty_of_bo (CicSubstitution.lift len ty)
409 ) (subst,metasenv) fl in
411 let (_,ty,_) = List.nth fl i in
414 (* check_metasenv_consistency checks that the "canonical" context of a
415 metavariable is consitent - up to relocation via the relocation list l -
416 with the actual context *)
417 and check_metasenv_consistency
418 metano subst metasenv context canonical_context l
420 let module C = Cic in
421 let module R = CicReduction in
422 let module S = CicSubstitution in
423 let lifted_canonical_context =
427 | (Some (n,C.Decl t))::tl ->
428 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
429 | (Some (n,C.Def (t,None)))::tl ->
430 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
431 | None::tl -> None::(aux (i+1) tl)
432 | (Some (n,C.Def (t,Some ty)))::tl ->
434 C.Def ((S.lift_meta l (S.lift i t)),
435 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
437 aux 1 canonical_context
441 (fun (subst,metasenv) t ct ->
445 | Some t,Some (_,C.Def (ct,_)) ->
447 fo_unif_subst subst context metasenv t ct
448 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)))))
449 | Some t,Some (_,C.Decl ct) ->
450 let inferredty,subst',metasenv' =
451 type_of_aux subst metasenv context t
455 subst' context metasenv' inferredty ct
456 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)))))
458 raise (RefineFailure (sprintf
459 "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"
460 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
461 (CicMetaSubst.ppcontext subst canonical_context)))
462 ) (subst,metasenv) l lifted_canonical_context
464 Invalid_argument _ ->
468 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
469 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
470 (CicMetaSubst.ppcontext subst canonical_context)))
472 and check_exp_named_subst metasubst metasenv context =
473 let rec check_exp_named_subst_aux metasubst metasenv substs =
475 [] -> metasubst,metasenv
476 | ((uri,t) as subst)::tl ->
478 CicSubstitution.subst_vars substs (type_of_variable uri) in
479 (* CSC: why was this code here? it is wrong
480 (match CicEnvironment.get_cooked_obj ~trust:false uri with
481 Cic.Variable (_,Some bo,_,_) ->
484 "A variable with a body can not be explicit substituted")
485 | Cic.Variable (_,None,_,_) -> ()
489 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
492 let typeoft,metasubst',metasenv' =
493 type_of_aux metasubst metasenv context t
495 let metasubst'',metasenv'' =
497 fo_unif_subst metasubst' context metasenv' typeoft typeofvar
500 ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
501 " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
503 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
505 check_exp_named_subst_aux metasubst metasenv []
507 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
508 let module C = Cic in
509 let context_for_t2 = (Some (name,C.Decl s))::context in
510 let t1'' = CicReduction.whd ~subst context t1 in
511 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
512 match (t1'', t2'') with
513 (C.Sort s1, C.Sort s2)
514 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
515 C.Sort s2,subst,metasenv
516 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
517 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
518 let t' = CicUniv.fresh() in
519 if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
520 assert false ; (* not possible, error in CicUniv *)
521 C.Sort (C.Type t'),subst,metasenv
522 | (C.Sort _,C.Sort (C.Type t1)) ->
523 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
524 C.Sort (C.Type t1),subst,metasenv
525 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
526 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
527 (* TODO how can we force the meta to become a sort? If we don't we
528 * brake the invariant that refine produce only well typed terms *)
529 (* TODO if we check the non meta term and if it is a sort then we are
530 * likely to know the exact value of the result e.g. if the rhs is a
531 * Sort (Prop | Set | CProp) then the result is the rhs *)
533 CicMkImplicit.mk_implicit_sort metasenv subst in
534 let (subst, metasenv) =
535 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
539 raise (RefineFailure (sprintf
540 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
541 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
542 (CicPp.ppterm t2'')))
544 and eat_prods subst metasenv context hetype tlbody_and_type =
545 let rec mk_prod metasenv context =
548 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
550 CicMkImplicit.identity_relocation_list_for_metavariable context
552 metasenv,Cic.Meta (idx, irl)
554 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
556 CicMkImplicit.identity_relocation_list_for_metavariable context
558 let meta = Cic.Meta (idx,irl) in
560 (* The name must be fresh for context. *)
561 (* Nevertheless, argty is well-typed only in context. *)
562 (* Thus I generate a name (name_hint) in context and *)
563 (* then I generate a name --- using the hint name_hint *)
564 (* --- that is fresh in (context'@context). *)
566 (* Cic.Name "pippo" *)
567 FreshNamesGenerator.mk_fresh_name metasenv
568 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
569 (CicMetaSubst.apply_subst_context subst context)
571 (CicMetaSubst.apply_subst subst argty)
573 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
574 FreshNamesGenerator.mk_fresh_name
575 [] context name_hint (Cic.Sort Cic.Prop)
577 let metasenv,target =
578 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
580 metasenv,Cic.Prod (name,meta,target)
582 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
583 let (subst, metasenv) =
584 fo_unif_subst subst context metasenv hetype hetype'
586 let rec eat_prods metasenv subst context hetype =
588 [] -> metasenv,subst,hetype
589 | (hete, hety)::tl ->
593 fo_unif_subst subst context metasenv hety s
596 fo_unif_subst subst context metasenv hety s
598 prerr_endline("senza subst fallisce");
599 let hety = CicMetaSubst.apply_subst subst hety in
600 let s = CicMetaSubst.apply_subst subst s in
601 prerr_endline ("unifico = " ^(CicPp.ppterm hety));
602 prerr_endline ("con = " ^(CicPp.ppterm s));
603 fo_unif_subst subst context metasenv hety s *)
606 let t1 = CicMetaSubst.subst subst hete t in
607 let t2 = CicSubstitution.subst hete t in
608 prerr_endline ("con subst = " ^(CicPp.ppterm t1));
609 prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
610 prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
611 (CicMetaSubst.ppmetasenv metasenv subst));
612 prerr_endline("++++++++++subst prima di eat_prods:\n" ^
613 (CicMetaSubst.ppsubst subst));
615 eat_prods metasenv subst context
616 (* (CicMetaSubst.subst subst hete t) tl *)
617 (CicSubstitution.subst hete t) tl
621 let metasenv,subst,t =
622 eat_prods metasenv subst context hetype' tlbody_and_type
626 let rec aux context' args (resty,subst,metasenv) =
628 [] -> resty,subst,metasenv
634 | Some t -> Some (CicMetaSubst.lift subst 1 t)
636 let argty' = CicMetaSubst.lift subst (List.length args) argty in
638 (* The name must be fresh for (context'@context). *)
639 (* Nevertheless, argty is well-typed only in context. *)
640 (* Thus I generate a name (name_hint) in context and *)
641 (* then I generate a name --- using the hint name_hint *)
642 (* --- that is fresh in (context'@context). *)
644 FreshNamesGenerator.mk_fresh_name
645 (CicMetaSubst.apply_subst_metasenv subst metasenv)
646 (CicMetaSubst.apply_subst_context subst context)
648 (CicMetaSubst.apply_subst subst argty)
650 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
651 FreshNamesGenerator.mk_fresh_name
652 [] (context'@context) name_hint (Cic.Sort Cic.Prop)
654 let context'' = Some (name, Cic.Decl argty') :: context' in
655 let (metasenv, idx) =
656 CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
658 (Some (Cic.Rel 1))::args' @
659 (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
662 let newmeta = Cic.Meta (idx, irl) in
663 let prod = Cic.Prod (name, argty, newmeta) in
664 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
665 let (subst, metasenv) =
666 fo_unif_subst subst context metasenv resty prod
668 aux context'' (Some arg :: args)
669 (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
671 aux [] [] (hetype,subst,metasenv) tlbody_and_type
674 let ty,subst',metasenv' =
675 type_of_aux [] metasenv context t
677 let substituted_t = CicMetaSubst.apply_subst subst' t in
678 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
679 (* Andrea: ho rimesso qui l'applicazione della subst al
680 metasenv dopo che ho droppato l'invariante che il metsaenv
681 e' sempre istanziato *)
682 let substituted_metasenv =
683 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
685 (* substituted_t,substituted_ty,substituted_metasenv *)
686 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
688 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
690 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
691 let cleaned_metasenv =
693 (function (n,context,ty) ->
694 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
699 | Some (n, Cic.Decl t) ->
701 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
702 | Some (n, Cic.Def (bo,ty)) ->
703 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
708 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
710 Some (n, Cic.Def (bo',ty'))
714 ) substituted_metasenv
716 (cleaned_t,cleaned_ty,cleaned_metasenv)
722 let type_of_aux' metasenv context term =
725 type_of_aux' metasenv context term in
727 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
729 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
732 | RefineFailure msg as e ->
733 debug_print ("@@@ REFINE FAILED: " ^ msg);
735 | Uncertain msg as e ->
736 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);