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 ugraph =
36 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
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 ugraph =
51 let module R = CicReduction in
52 let module U = UriManager in
56 CicEnvironment.get_cooked_obj uri
57 with Not_found -> assert false
60 let obj,u= CicEnvironment.get_obj uri ugraph in
62 C.Constant (_,_,ty,_) -> ty,u
63 | C.CurrentProof (_,_,_,ty,_) -> ty,u
66 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
68 and type_of_variable uri ugraph =
70 let module R = CicReduction in
71 let module U = UriManager in
75 CicEnvironment.get_cooked_obj uri
76 with Not_found -> assert false
79 let obj,u = CicEnvironment.get_obj uri ugraph in
81 C.Variable (_,_,ty,_) -> ty,u
85 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
87 and type_of_mutual_inductive_defs uri i ugraph =
89 let module R = CicReduction in
90 let module U = UriManager in
94 CicEnvironment.get_cooked_obj uri
95 with Not_found -> assert false
98 let obj,u = CicEnvironment.get_obj uri ugraph in
100 C.InductiveDefinition (dl,_,_) ->
101 let (_,_,arity,_) = List.nth dl i in
106 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
108 and type_of_mutual_inductive_constr uri i j ugraph =
109 let module C = Cic in
110 let module R = CicReduction in
111 let module U = UriManager in
115 CicEnvironment.get_cooked_obj uri
116 with Not_found -> assert false
119 let obj,u = CicEnvironment.get_obj uri ugraph in
121 C.InductiveDefinition (dl,_,_) ->
122 let (_,_,_,cl) = List.nth dl i in
123 let (_,ty) = List.nth cl (j-1) in
128 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
131 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
133 (* the check_branch function checks if a branch of a case is refinable.
134 It returns a pair (outype_instance,args), a subst and a metasenv.
135 outype_instance is the expected result of applying the case outtype
137 The problem is that outype is in general unknown, and we should
138 try to synthesize it from the above information, that is in general
139 a second order unification problem. *)
141 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
142 let module C = Cic in
143 (* let module R = CicMetaSubst in *)
144 let module R = CicReduction in
145 match R.whd ~subst context expectedtype with
147 (n,context,actualtype, [term]), subst, metasenv, ugraph
148 | C.Appl (C.MutInd (_,_,_)::tl) ->
149 let (_,arguments) = split tl left_args_no in
150 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
151 | C.Prod (name,so,de) ->
152 (* we expect that the actual type of the branch has the due
154 (match R.whd ~subst context actualtype with
155 C.Prod (name',so',de') ->
156 let subst, metasenv, ugraph1 =
157 fo_unif_subst subst context metasenv so so' ugraph in
159 (match CicSubstitution.lift 1 term with
160 C.Appl l -> C.Appl (l@[C.Rel 1])
161 | t -> C.Appl [t ; C.Rel 1]) in
162 (* we should also check that the name variable is anonymous in
163 the actual type de' ?? *)
164 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1
165 | _ -> raise (AssertFailure "Wrong number of arguments"))
166 | _ -> raise (AssertFailure "Prod or MutInd expected")
168 and type_of_aux' metasenv context t ugraph =
169 let rec type_of_aux subst metasenv context t ugraph =
170 let module C = Cic in
171 let module S = CicSubstitution in
172 let module U = UriManager in
177 match List.nth context (n - 1) with
178 Some (_,C.Decl t) -> S.lift n t,subst,metasenv, ugraph
179 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv, ugraph
180 | Some (_,C.Def (bo,None)) ->
181 type_of_aux subst metasenv context (S.lift n bo) ugraph
182 | None -> raise (RefineFailure "Rel to hidden hypothesis")
184 _ -> raise (RefineFailure "Not a close term")
186 | C.Var (uri,exp_named_subst) ->
187 let subst',metasenv',ugraph1 =
188 check_exp_named_subst subst metasenv context exp_named_subst ugraph in
189 let ty_uri,ugraph1 = type_of_variable uri ugraph in
192 CicSubstitution.subst_vars exp_named_subst ty_uri
194 ty,subst',metasenv',ugraph1
197 let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
198 let subst,metasenv,ugraph1 =
199 check_metasenv_consistency n subst metasenv context
200 canonical_context l ugraph
202 (* trust or check ??? *)
203 CicSubstitution.lift_meta l ty, subst, metasenv, ugraph1
204 (* type_of_aux subst metasenv
205 context (CicSubstitution.lift_meta l term) *)
206 with CicUtil.Subst_not_found _ ->
207 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
208 let subst,metasenv, ugraph1 =
209 check_metasenv_consistency n subst metasenv context
210 canonical_context l ugraph
212 CicSubstitution.lift_meta l ty, subst, metasenv,ugraph1)
213 (* TASSI: CONSTRAINT *)
214 | C.Sort (C.Type t) ->
215 let t' = CicUniv.fresh() in
216 let ugraph1 = CicUniv.add_gt t' t ugraph in
217 (C.Sort (C.Type t')),subst,metasenv,ugraph1
218 (* TASSI: CONSTRAINT *)
219 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
220 | C.Implicit _ -> raise (AssertFailure "21")
222 let _,subst',metasenv',ugraph1 =
223 type_of_aux subst metasenv context ty ugraph in
224 let inferredty,subst'',metasenv'',ugraph2 =
225 type_of_aux subst' metasenv' context te ugraph1
228 let subst''',metasenv''',ugraph3 =
229 fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2
231 ty,subst''',metasenv''',ugraph3
233 _ -> raise (RefineFailure "Cast"))
234 | C.Prod (name,s,t) ->
235 let sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in
236 let sort2,subst'',metasenv'',ugraph2 =
237 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t ugraph1
239 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) ugraph2
240 | C.Lambda (n,s,t) ->
241 let sort1,subst',metasenv',ugraph1 =
242 type_of_aux subst metasenv context s ugraph
244 (match CicReduction.whd ~subst:subst' context sort1 with
248 raise (RefineFailure (sprintf
249 "Not well-typed lambda-abstraction: the source %s should be a type;
250 instead it is a term of type %s" (CicPp.ppterm s)
251 (CicPp.ppterm sort1)))
253 let type2,subst'',metasenv'',ugraph2 =
254 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t ugraph1
256 C.Prod (n,s,type2),subst'',metasenv'',ugraph2
258 (* only to check if s is well-typed *)
259 let ty,subst',metasenv',ugraph1 =
260 type_of_aux subst metasenv context s ugraph
262 let inferredty,subst'',metasenv'',ugraph2 =
263 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
265 (* One-step LetIn reduction. Even faster than the previous solution.
266 Moreover the inferred type is closer to the expected one. *)
267 CicSubstitution.subst s inferredty,subst',metasenv',ugraph2
268 | C.Appl (he::((_::_) as tl)) ->
269 let hetype,subst',metasenv',ugraph1 =
270 type_of_aux subst metasenv context he ugraph
272 let tlbody_and_type,subst'',metasenv'',ugraph2 =
274 (fun x (res,subst,metasenv,ugraph) ->
275 let ty,subst',metasenv',ugraph1 =
276 type_of_aux subst metasenv context x ugraph
278 (x, ty)::res,subst',metasenv',ugraph1
279 ) tl ([],subst',metasenv',ugraph1)
281 eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2
282 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
283 | C.Const (uri,exp_named_subst) ->
284 let subst',metasenv',ugraph1 =
285 check_exp_named_subst subst metasenv context exp_named_subst ugraph in
286 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
288 CicSubstitution.subst_vars exp_named_subst ty_uri
290 cty,subst',metasenv',ugraph2
291 | C.MutInd (uri,i,exp_named_subst) ->
292 let subst',metasenv',ugraph1 =
293 check_exp_named_subst subst metasenv context exp_named_subst ugraph
295 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
297 CicSubstitution.subst_vars exp_named_subst ty_uri in
298 cty,subst',metasenv',ugraph2
299 | C.MutConstruct (uri,i,j,exp_named_subst) ->
300 let subst',metasenv',ugraph1 =
301 check_exp_named_subst subst metasenv context exp_named_subst ugraph in
302 let ty_uri,ugraph2 = type_of_mutual_inductive_constr uri i j ugraph1 in
304 CicSubstitution.subst_vars exp_named_subst ty_uri in
305 cty,subst',metasenv',ugraph2
306 | C.MutCase (uri, i, outtype, term, pl) ->
307 (* first, get the inductive type (and noparams) in the environment *)
308 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
312 CicEnvironment.get_cooked_obj ~trust:true uri
313 with Not_found -> assert false
316 let obj,u = CicEnvironment.get_obj uri ugraph in
318 C.InductiveDefinition (l,expl_params,parsno) ->
319 List.nth l i , expl_params, parsno, u
323 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
324 let rec count_prod t =
325 match CicReduction.whd ~subst context t with
326 C.Prod (_, _, t) -> 1 + (count_prod t)
328 let no_args = count_prod arity in
329 (* now, create a "generic" MutInd *)
330 let metasenv,left_args =
331 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
332 let metasenv,right_args =
333 let no_right_params = no_args - no_left_params in
334 if no_right_params < 0 then assert false
335 else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
336 let metasenv,exp_named_subst =
337 CicMkImplicit.fresh_subst metasenv subst context expl_params in
340 C.MutInd (uri,i,exp_named_subst)
342 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
344 (* check consistency with the actual type of term *)
345 let actual_type,subst,metasenv,ugraph1 =
346 type_of_aux subst metasenv context term ugraph in
347 let _, subst, metasenv,ugraph2 =
348 type_of_aux subst metasenv context expected_type ugraph1
350 let actual_type = CicReduction.whd ~subst context actual_type in
351 let subst,metasenv,ugraph3 =
352 fo_unif_subst subst context metasenv expected_type actual_type ugraph2
354 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
355 let (_,outtypeinstances,subst,metasenv,ugraph4) =
357 (fun (j,outtypeinstances,subst,metasenv,ugraph) p ->
359 if left_args = [] then
360 (C.MutConstruct (uri,i,j,exp_named_subst))
362 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
364 let actual_type,subst,metasenv,ugraph1 =
365 type_of_aux subst metasenv context p ugraph in
366 let expected_type, subst, metasenv,ugraph2 =
367 type_of_aux subst metasenv context constructor ugraph1 in
368 let outtypeinstance,subst,metasenv,ugraph3 =
370 0 context metasenv subst
371 no_left_params actual_type constructor expected_type ugraph2 in
372 (j+1,outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
373 (1,[],subst,metasenv,ugraph3) pl in
374 (* we are left to check that the outype matches his instances.
375 The easy case is when the outype is specified, that amount
376 to a trivial check. Otherwise, we should guess a type from
380 let _, subst, metasenv,ugraph5 =
381 type_of_aux subst metasenv context
382 (C.Appl ((outtype :: right_args) @ [term])) ugraph4
384 let (subst,metasenv,ugraph6) =
386 (fun (subst,metasenv,ugraph) (constructor_args_no,context,instance,args) ->
390 CicSubstitution.lift constructor_args_no outtype
392 C.Appl (outtype'::args)
395 (* if appl is not well typed then the type_of below solves the
397 let (_, subst, metasenv,ugraph1) =
398 type_of_aux subst metasenv context appl ugraph
402 let prova1 = CicMetaSubst.whd subst context appl in
403 let prova2 = CicReduction.whd ~subst context appl in
404 if not (prova1 = prova2) then
406 prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
407 prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
410 (* CicMetaSubst.whd subst context appl *)
411 CicReduction.whd ~subst context appl
413 fo_unif_subst subst context metasenv instance instance' ugraph)
414 (subst,metasenv,ugraph5) outtypeinstances in
415 CicReduction.whd ~subst
416 context (C.Appl(outtype::right_args@[term])),subst,metasenv,ugraph6
418 let subst,metasenv,types,ugraph1 =
420 (fun (subst,metasenv,types,ugraph) (n,_,ty,_) ->
421 let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in
422 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph
423 ) (subst,metasenv,[],ugraph) fl
425 let len = List.length types in
426 let context' = types@context in
427 let subst,metasenv,ugraph2 =
429 (fun (subst,metasenv,ugraph) (name,x,ty,bo) ->
430 let ty_of_bo,subst,metasenv,ugraph1 =
431 type_of_aux subst metasenv context' bo ugraph
433 fo_unif_subst subst context' metasenv
434 ty_of_bo (CicSubstitution.lift len ty) ugraph1
435 ) (subst,metasenv,ugraph1) fl in
436 let (_,_,ty,_) = List.nth fl i in
437 ty,subst,metasenv,ugraph2
439 let subst,metasenv,types,ugraph1 =
441 (fun (subst,metasenv,types,ugraph) (n,ty,_) ->
442 let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in
443 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph1
444 ) (subst,metasenv,[],ugraph) fl
446 let len = List.length types in
447 let context' = types@context in
448 let subst,metasenv,ugraph2 =
450 (fun (subst,metasenv,ugraph) (name,ty,bo) ->
451 let ty_of_bo,subst,metasenv,ugraph1 =
452 type_of_aux subst metasenv context' bo ugraph
454 fo_unif_subst subst context' metasenv
455 ty_of_bo (CicSubstitution.lift len ty) ugraph1
456 ) (subst,metasenv,ugraph1) fl in
458 let (_,ty,_) = List.nth fl i in
459 ty,subst,metasenv,ugraph2
461 (* check_metasenv_consistency checks that the "canonical" context of a
462 metavariable is consitent - up to relocation via the relocation list l -
463 with the actual context *)
464 and check_metasenv_consistency
465 metano subst metasenv context canonical_context l ugraph
467 let module C = Cic in
468 let module R = CicReduction in
469 let module S = CicSubstitution in
470 let lifted_canonical_context =
474 | (Some (n,C.Decl t))::tl ->
475 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
476 | (Some (n,C.Def (t,None)))::tl ->
477 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
478 | None::tl -> None::(aux (i+1) tl)
479 | (Some (n,C.Def (t,Some ty)))::tl ->
481 C.Def ((S.lift_meta l (S.lift i t)),
482 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
484 aux 1 canonical_context
488 (fun (subst,metasenv,ugraph) t ct ->
491 subst,metasenv,ugraph
492 | Some t,Some (_,C.Def (ct,_)) ->
494 fo_unif_subst subst context metasenv t ct ugraph
495 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)))))
496 | Some t,Some (_,C.Decl ct) ->
497 let inferredty,subst',metasenv',ugraph1 =
498 type_of_aux subst metasenv context t ugraph
502 subst' context metasenv' inferredty ct ugraph1
503 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)))))
505 raise (RefineFailure (sprintf
506 "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"
507 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
508 (CicMetaSubst.ppcontext subst canonical_context)))
509 ) (subst,metasenv,ugraph) l lifted_canonical_context
511 Invalid_argument _ ->
515 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
516 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
517 (CicMetaSubst.ppcontext subst canonical_context)))
519 and check_exp_named_subst metasubst metasenv context tl ugraph =
520 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
522 [] -> metasubst,metasenv,ugraph
523 | ((uri,t) as subst)::tl ->
524 let ty_uri,ugraph1 = type_of_variable uri ugraph in
526 CicSubstitution.subst_vars substs ty_uri in
527 (* CSC: why was this code here? it is wrong
528 (match CicEnvironment.get_cooked_obj ~trust:false uri with
529 Cic.Variable (_,Some bo,_,_) ->
532 "A variable with a body can not be explicit substituted")
533 | Cic.Variable (_,None,_,_) -> ()
537 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
540 let typeoft,metasubst',metasenv',ugraph2 =
541 type_of_aux metasubst metasenv context t ugraph1
543 let metasubst'',metasenv'',ugraph3 =
545 fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2
548 ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
549 " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
551 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl ugraph3
553 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
556 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
557 let module C = Cic in
558 let context_for_t2 = (Some (name,C.Decl s))::context in
559 let t1'' = CicReduction.whd ~subst context t1 in
560 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
561 match (t1'', t2'') with
562 (C.Sort s1, C.Sort s2)
563 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
564 C.Sort s2,subst,metasenv,ugraph
565 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
566 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
567 let t' = CicUniv.fresh() in
568 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
569 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
570 C.Sort (C.Type t'),subst,metasenv,ugraph2
571 | (C.Sort _,C.Sort (C.Type t1)) ->
572 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
573 C.Sort (C.Type t1),subst,metasenv,ugraph
574 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
575 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
576 (* TODO how can we force the meta to become a sort? If we don't we
577 * brake the invariant that refine produce only well typed terms *)
578 (* TODO if we check the non meta term and if it is a sort then we are
579 * likely to know the exact value of the result e.g. if the rhs is a
580 * Sort (Prop | Set | CProp) then the result is the rhs *)
582 CicMkImplicit.mk_implicit_sort metasenv subst in
583 let (subst, metasenv,ugraph1) =
584 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
586 t2'',subst,metasenv,ugraph1
588 raise (RefineFailure (sprintf
589 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
590 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
591 (CicPp.ppterm t2'')))
593 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
594 let rec mk_prod metasenv context =
597 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
599 CicMkImplicit.identity_relocation_list_for_metavariable context
601 metasenv,Cic.Meta (idx, irl)
603 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
605 CicMkImplicit.identity_relocation_list_for_metavariable context
607 let meta = Cic.Meta (idx,irl) in
609 (* The name must be fresh for context. *)
610 (* Nevertheless, argty is well-typed only in context. *)
611 (* Thus I generate a name (name_hint) in context and *)
612 (* then I generate a name --- using the hint name_hint *)
613 (* --- that is fresh in (context'@context). *)
615 (* Cic.Name "pippo" *)
616 FreshNamesGenerator.mk_fresh_name ~subst metasenv
617 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
618 (CicMetaSubst.apply_subst_context subst context)
620 ~typ:(CicMetaSubst.apply_subst subst argty)
622 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
623 FreshNamesGenerator.mk_fresh_name ~subst
624 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
626 let metasenv,target =
627 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
629 metasenv,Cic.Prod (name,meta,target)
631 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
632 let (subst, metasenv,ugraph1) =
634 fo_unif_subst subst context metasenv hetype hetype' ugraph
636 prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
637 (CicPp.ppterm hetype)
638 (CicPp.ppterm hetype')
639 (CicMetaSubst.ppmetasenv metasenv [])
640 (CicMetaSubst.ppsubst subst));
644 let rec eat_prods metasenv subst context hetype ugraph =
646 [] -> metasenv,subst,hetype,ugraph
647 | (hete, hety)::tl ->
650 let subst,metasenv,ugraph1 =
652 fo_unif_subst subst context metasenv hety s ugraph
654 prerr_endline (Printf.sprintf "hety=%s\ns=%s\nmetasenv=%s"
655 (CicMetaSubst.ppterm subst hety)
656 (CicMetaSubst.ppterm subst s)
657 (CicMetaSubst.ppmetasenv metasenv subst));
662 fo_unif_subst subst context metasenv hety s
664 prerr_endline("senza subst fallisce");
665 let hety = CicMetaSubst.apply_subst subst hety in
666 let s = CicMetaSubst.apply_subst subst s in
667 prerr_endline ("unifico = " ^(CicPp.ppterm hety));
668 prerr_endline ("con = " ^(CicPp.ppterm s));
669 fo_unif_subst subst context metasenv hety s *)
672 let t1 = CicMetaSubst.subst subst hete t in
673 let t2 = CicSubstitution.subst hete t in
674 prerr_endline ("con subst = " ^(CicPp.ppterm t1));
675 prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
676 prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
677 (CicMetaSubst.ppmetasenv metasenv subst));
678 prerr_endline("++++++++++subst prima di eat_prods:\n" ^
679 (CicMetaSubst.ppsubst subst));
681 eat_prods metasenv subst context
682 (* (CicMetaSubst.subst subst hete t) tl *)
683 (CicSubstitution.subst hete t) ugraph1 tl
687 let metasenv,subst,t,ugraph2 =
688 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
690 t,subst,metasenv,ugraph2
691 (* eat prods ends here! *)
693 let ty,subst',metasenv',ugraph1 =
694 type_of_aux [] metasenv context t ugraph
696 let substituted_t = CicMetaSubst.apply_subst subst' t in
697 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
698 (* Andrea: ho rimesso qui l'applicazione della subst al
699 metasenv dopo che ho droppato l'invariante che il metsaenv
700 e' sempre istanziato *)
701 let substituted_metasenv =
702 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
704 (* substituted_t,substituted_ty,substituted_metasenv *)
705 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
707 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
709 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
710 let cleaned_metasenv =
712 (function (n,context,ty) ->
713 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
718 | Some (n, Cic.Decl t) ->
720 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
721 | Some (n, Cic.Def (bo,ty)) ->
722 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
727 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
729 Some (n, Cic.Def (bo',ty'))
733 ) substituted_metasenv
735 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
739 let type_of_aux' metasenv context term =
742 type_of_aux' metasenv context term in
744 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
746 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
749 | RefineFailure msg as e ->
750 debug_print ("@@@ REFINE FAILED: " ^ msg);
752 | Uncertain msg as e ->
753 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);