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 Lazy.t;;
29 exception Uncertain of string Lazy.t;;
30 exception AssertFailure of string Lazy.t;;
32 let debug_print = fun _ -> ()
34 let profiler = HExtlib.profile "CicRefine.fo_unif"
36 let fo_unif_subst subst context metasenv t1 t2 ugraph =
39 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
40 in profiler.HExtlib.profile foo ()
42 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
43 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
49 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
50 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
53 let exp_impl metasenv subst context term =
54 let rec aux metasenv context = function
55 | (Cic.Rel _) as t -> metasenv, t
56 | (Cic.Sort _) as t -> metasenv, t
57 | Cic.Const (uri, subst) ->
58 let metasenv', subst' = do_subst metasenv context subst in
59 metasenv', Cic.Const (uri, subst')
60 | Cic.Var (uri, subst) ->
61 let metasenv', subst' = do_subst metasenv context subst in
62 metasenv', Cic.Var (uri, subst')
63 | Cic.MutInd (uri, i, subst) ->
64 let metasenv', subst' = do_subst metasenv context subst in
65 metasenv', Cic.MutInd (uri, i, subst')
66 | Cic.MutConstruct (uri, i, j, subst) ->
67 let metasenv', subst' = do_subst metasenv context subst in
68 metasenv', Cic.MutConstruct (uri, i, j, subst')
70 let metasenv', l' = do_local_context metasenv context l in
71 metasenv', Cic.Meta (n, l')
72 | Cic.Implicit (Some `Type) ->
73 let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
74 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
75 metasenv', Cic.Meta (idx, irl)
76 | Cic.Implicit (Some `Closed) ->
77 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
78 metasenv', Cic.Meta (idx, [])
79 | Cic.Implicit None ->
80 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
81 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
82 metasenv', Cic.Meta (idx, irl)
83 | Cic.Implicit _ -> assert false
84 | Cic.Cast (te, ty) ->
85 let metasenv', ty' = aux metasenv context ty in
86 let metasenv'', te' = aux metasenv' context te in
87 metasenv'', Cic.Cast (te', ty')
88 | Cic.Prod (name, s, t) ->
89 let metasenv', s' = aux metasenv context s in
90 metasenv', Cic.Prod (name, s', t)
91 | Cic.Lambda (name, s, t) ->
92 let metasenv', s' = aux metasenv context s in
93 metasenv', Cic.Lambda (name, s', t)
94 | Cic.LetIn (name, s, t) ->
95 let metasenv', s' = aux metasenv context s in
96 metasenv', Cic.LetIn (name, s', t)
97 | Cic.Appl l when List.length l > 1 ->
100 (fun term (metasenv, terms) ->
101 let new_metasenv, term = aux metasenv context term in
102 new_metasenv, term :: terms)
105 metasenv', Cic.Appl l'
106 | Cic.Appl _ -> assert false
107 | Cic.MutCase (uri, i, outtype, term, patterns) ->
110 (fun term (metasenv, terms) ->
111 let new_metasenv, term = aux metasenv context term in
112 new_metasenv, term :: terms)
113 (outtype :: term :: patterns) (metasenv, [])
115 let outtype', term', patterns' =
117 | outtype' :: term' :: patterns' -> outtype', term', patterns'
120 metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
121 | Cic.Fix (i, funs) ->
122 let metasenv', types =
124 (fun (name, _, typ, _) (metasenv, types) ->
125 let new_metasenv, new_type = aux metasenv context typ in
126 (new_metasenv, (name, new_type) :: types))
129 let rec combine = function
130 | ((name, index, _, body) :: funs_tl),
131 ((_, typ) :: typ_tl) ->
132 (name, index, typ, body) :: combine (funs_tl, typ_tl)
136 let funs' = combine (funs, types) in
137 metasenv', Cic.Fix (i, funs')
138 | Cic.CoFix (i, funs) ->
139 let metasenv', types =
141 (fun (name, typ, _) (metasenv, types) ->
142 let new_metasenv, new_type = aux metasenv context typ in
143 (new_metasenv, (name, new_type) :: types))
146 let rec combine = function
147 | ((name, _, body) :: funs_tl),
148 ((_, typ) :: typ_tl) ->
149 (name, typ, body) :: combine (funs_tl, typ_tl)
153 let funs' = combine (funs, types) in
154 metasenv', Cic.CoFix (i, funs')
155 and do_subst metasenv context subst =
157 (fun (uri, term) (metasenv, substs) ->
158 let metasenv', term' = aux metasenv context term in
159 (metasenv', (uri, term') :: substs))
161 and do_local_context metasenv context local_context =
163 (fun term (metasenv, local_context) ->
164 let metasenv', term' =
166 | None -> metasenv, None
168 let metasenv', term' = aux metasenv context term in
169 metasenv', Some term'
171 metasenv', term' :: local_context)
172 local_context (metasenv, [])
174 aux metasenv context term
177 let rec type_of_constant uri ugraph =
178 let module C = Cic in
179 let module R = CicReduction in
180 let module U = UriManager in
181 let _ = CicTypeChecker.typecheck uri in
184 CicEnvironment.get_cooked_obj ugraph uri
185 with Not_found -> assert false
188 C.Constant (_,_,ty,_,_) -> ty,u
189 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
192 (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
194 and type_of_variable uri ugraph =
195 let module C = Cic in
196 let module R = CicReduction in
197 let module U = UriManager in
198 let _ = CicTypeChecker.typecheck uri in
201 CicEnvironment.get_cooked_obj ugraph uri
202 with Not_found -> assert false
205 C.Variable (_,_,ty,_,_) -> ty,u
209 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
211 and type_of_mutual_inductive_defs uri i ugraph =
212 let module C = Cic in
213 let module R = CicReduction in
214 let module U = UriManager in
215 let _ = CicTypeChecker.typecheck uri in
218 CicEnvironment.get_cooked_obj ugraph uri
219 with Not_found -> assert false
222 C.InductiveDefinition (dl,_,_,_) ->
223 let (_,_,arity,_) = List.nth dl i in
228 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
230 and type_of_mutual_inductive_constr uri i j ugraph =
231 let module C = Cic in
232 let module R = CicReduction in
233 let module U = UriManager in
234 let _ = CicTypeChecker.typecheck uri in
237 CicEnvironment.get_cooked_obj ugraph uri
238 with Not_found -> assert false
241 C.InductiveDefinition (dl,_,_,_) ->
242 let (_,_,_,cl) = List.nth dl i in
243 let (_,ty) = List.nth cl (j-1) in
249 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
252 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
254 (* the check_branch function checks if a branch of a case is refinable.
255 It returns a pair (outype_instance,args), a subst and a metasenv.
256 outype_instance is the expected result of applying the case outtype
258 The problem is that outype is in general unknown, and we should
259 try to synthesize it from the above information, that is in general
260 a second order unification problem. *)
262 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
263 let module C = Cic in
264 (* let module R = CicMetaSubst in *)
265 let module R = CicReduction in
266 match R.whd ~subst context expectedtype with
268 (n,context,actualtype, [term]), subst, metasenv, ugraph
269 | C.Appl (C.MutInd (_,_,_)::tl) ->
270 let (_,arguments) = split tl left_args_no in
271 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
272 | C.Prod (name,so,de) ->
273 (* we expect that the actual type of the branch has the due
275 (match R.whd ~subst context actualtype with
276 C.Prod (name',so',de') ->
277 let subst, metasenv, ugraph1 =
278 fo_unif_subst subst context metasenv so so' ugraph in
280 (match CicSubstitution.lift 1 term with
281 C.Appl l -> C.Appl (l@[C.Rel 1])
282 | t -> C.Appl [t ; C.Rel 1]) in
283 (* we should also check that the name variable is anonymous in
284 the actual type de' ?? *)
286 ((Some (name,(C.Decl so)))::context)
287 metasenv subst left_args_no de' term' de ugraph1
288 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
289 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
291 and type_of_aux' metasenv context t ugraph =
292 let metasenv, t = exp_impl metasenv [] context t in
293 let rec type_of_aux subst metasenv context t ugraph =
294 let module C = Cic in
295 let module S = CicSubstitution in
296 let module U = UriManager in
297 (* this stops on binders, so we have to call it every time *)
302 match List.nth context (n - 1) with
303 Some (_,C.Decl ty) ->
304 t,S.lift n ty,subst,metasenv, ugraph
305 | Some (_,C.Def (_,Some ty)) ->
306 t,S.lift n ty,subst,metasenv, ugraph
307 | Some (_,C.Def (bo,None)) ->
309 (* if it is in the context it must be already well-typed*)
310 CicTypeChecker.type_of_aux' ~subst metasenv context
313 t,ty,subst,metasenv,ugraph
314 | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
316 _ -> raise (RefineFailure (lazy "Not a close term")))
317 | C.Var (uri,exp_named_subst) ->
318 let exp_named_subst',subst',metasenv',ugraph1 =
319 check_exp_named_subst
320 subst metasenv context exp_named_subst ugraph
322 let ty_uri,ugraph1 = type_of_variable uri ugraph in
324 CicSubstitution.subst_vars exp_named_subst' ty_uri
326 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
329 let (canonical_context, term,ty) =
330 CicUtil.lookup_subst n subst
332 let l',subst',metasenv',ugraph1 =
333 check_metasenv_consistency n subst metasenv context
334 canonical_context l ugraph
336 (* trust or check ??? *)
337 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
338 subst', metasenv', ugraph1
339 (* type_of_aux subst metasenv
340 context (CicSubstitution.subst_meta l term) *)
341 with CicUtil.Subst_not_found _ ->
342 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
343 let l',subst',metasenv', ugraph1 =
344 check_metasenv_consistency n subst metasenv context
345 canonical_context l ugraph
347 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
348 subst', metasenv',ugraph1)
349 | C.Sort (C.Type tno) ->
350 let tno' = CicUniv.fresh() in
351 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
352 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
354 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
355 | C.Implicit _ -> raise (AssertFailure (lazy "21"))
357 let ty',_,subst',metasenv',ugraph1 =
358 type_of_aux subst metasenv context ty ugraph
360 let te',inferredty,subst'',metasenv'',ugraph2 =
361 type_of_aux subst' metasenv' context te ugraph1
363 let subst''',metasenv''',ugraph3 =
364 fo_unif_subst subst'' context metasenv''
365 inferredty ty' ugraph2
367 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
368 | C.Prod (name,s,t) ->
369 let carr t subst context = CicMetaSubst.apply_subst subst t in
371 in_source tgt_sort t type_to_coerce subst ctx metasenv uragph
373 let coercion_src = carr type_to_coerce subst ctx in
374 match coercion_src with
376 t,type_to_coerce,subst,metasenv,ugraph
378 | Cic.Meta _ as meta when not in_source ->
379 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
380 let subst, metasenv, ugraph =
382 subst ctx metasenv meta coercion_tgt ugraph
384 t, Cic.Sort tgt_sort, subst, metasenv, ugraph
386 | Cic.Meta _ as meta ->
387 t, meta, subst, metasenv, ugraph
388 | Cic.Cast _ as cast ->
389 t, cast, subst, metasenv, ugraph
391 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
392 let search = CoercGraph.look_for_coercion in
393 let boh = search coercion_src coercion_tgt in
395 | CoercGraph.NoCoercion ->
396 raise (RefineFailure (lazy "no coercion"))
397 | CoercGraph.NotHandled _ ->
398 raise (RefineFailure (lazy "not a sort in PI"))
399 | CoercGraph.NotMetaClosed ->
400 raise (Uncertain (lazy "Coercions on metas 1"))
401 | CoercGraph.SomeCoercion c ->
402 Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
404 let s',sort1,subst',metasenv',ugraph1 =
405 type_of_aux subst metasenv context s ugraph
407 let s',sort1,subst', metasenv',ugraph1 =
408 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
409 s' sort1 subst' context metasenv' ugraph1
411 let context_for_t = ((Some (name,(C.Decl s')))::context) in
412 let metasenv',t = exp_impl metasenv' subst' context_for_t t in
413 let t',sort2,subst'',metasenv'',ugraph2 =
414 type_of_aux subst' metasenv'
415 context_for_t t ugraph1
417 let t',sort2,subst'',metasenv'',ugraph2 =
418 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
419 t' sort2 subst'' context_for_t metasenv'' ugraph2
421 let sop,subst''',metasenv''',ugraph3 =
422 sort_of_prod subst'' metasenv''
423 context (name,s') (sort1,sort2) ugraph2
425 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
426 | C.Lambda (n,s,t) ->
428 let s',sort1,subst',metasenv',ugraph1 =
429 type_of_aux subst metasenv context s ugraph
431 (match CicReduction.whd ~subst:subst' context sort1 with
435 raise (RefineFailure (lazy (sprintf
436 "Not well-typed lambda-abstraction: the source %s should be a type;
437 instead it is a term of type %s" (CicPp.ppterm s)
438 (CicPp.ppterm sort1))))
440 let context_for_t = ((Some (n,(C.Decl s')))::context) in
441 let metasenv',t = exp_impl metasenv' subst' context_for_t t in
442 let t',type2,subst'',metasenv'',ugraph2 =
443 type_of_aux subst' metasenv'
444 context_for_t t ugraph1
446 C.Lambda (n,s',t'),C.Prod (n,s',type2),
447 subst'',metasenv'',ugraph2
449 (* only to check if s is well-typed *)
450 let s',ty,subst',metasenv',ugraph1 =
451 type_of_aux subst metasenv context s ugraph
453 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
454 let metasenv',t = exp_impl metasenv' subst' context_for_t t in
456 let t',inferredty,subst'',metasenv'',ugraph2 =
457 type_of_aux subst' metasenv'
458 context_for_t t ugraph1
460 (* One-step LetIn reduction.
461 * Even faster than the previous solution.
462 * Moreover the inferred type is closer to the expected one.
464 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
465 subst'',metasenv'',ugraph2
466 | C.Appl (he::((_::_) as tl)) ->
467 let he',hetype,subst',metasenv',ugraph1 =
468 type_of_aux subst metasenv context he ugraph
470 let tlbody_and_type,subst'',metasenv'',ugraph2 =
472 (fun x (res,subst,metasenv,ugraph) ->
473 let x',ty,subst',metasenv',ugraph1 =
474 type_of_aux subst metasenv context x ugraph
476 (x', ty)::res,subst',metasenv',ugraph1
477 ) tl ([],subst',metasenv',ugraph1)
479 let tl',applty,subst''',metasenv''',ugraph3 =
480 eat_prods true subst'' metasenv'' context
481 hetype tlbody_and_type ugraph2
483 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
484 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
485 | C.Const (uri,exp_named_subst) ->
486 let exp_named_subst',subst',metasenv',ugraph1 =
487 check_exp_named_subst subst metasenv context
488 exp_named_subst ugraph in
489 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
491 CicSubstitution.subst_vars exp_named_subst' ty_uri
493 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
494 | C.MutInd (uri,i,exp_named_subst) ->
495 let exp_named_subst',subst',metasenv',ugraph1 =
496 check_exp_named_subst subst metasenv context
497 exp_named_subst ugraph
499 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
501 CicSubstitution.subst_vars exp_named_subst' ty_uri in
502 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
503 | C.MutConstruct (uri,i,j,exp_named_subst) ->
504 let exp_named_subst',subst',metasenv',ugraph1 =
505 check_exp_named_subst subst metasenv context
506 exp_named_subst ugraph
509 type_of_mutual_inductive_constr uri i j ugraph1
512 CicSubstitution.subst_vars exp_named_subst' ty_uri
514 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
516 | C.MutCase (uri, i, outtype, term, pl) ->
517 (* first, get the inductive type (and noparams)
518 * in the environment *)
519 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
520 let _ = CicTypeChecker.typecheck uri in
521 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
523 C.InductiveDefinition (l,expl_params,parsno,_) ->
524 List.nth l i , expl_params, parsno, u
528 (lazy ("Unkown mutual inductive definition " ^
529 U.string_of_uri uri)))
531 let rec count_prod t =
532 match CicReduction.whd ~subst context t with
533 C.Prod (_, _, t) -> 1 + (count_prod t)
536 let no_args = count_prod arity in
537 (* now, create a "generic" MutInd *)
538 let metasenv,left_args =
539 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
541 let metasenv,right_args =
542 let no_right_params = no_args - no_left_params in
543 if no_right_params < 0 then assert false
544 else CicMkImplicit.n_fresh_metas
545 metasenv subst context no_right_params
547 let metasenv,exp_named_subst =
548 CicMkImplicit.fresh_subst metasenv subst context expl_params in
551 C.MutInd (uri,i,exp_named_subst)
554 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
556 (* check consistency with the actual type of term *)
557 let term',actual_type,subst,metasenv,ugraph1 =
558 type_of_aux subst metasenv context term ugraph in
559 let expected_type',_, subst, metasenv,ugraph2 =
560 type_of_aux subst metasenv context expected_type ugraph1
562 let actual_type = CicReduction.whd ~subst context actual_type in
563 let subst,metasenv,ugraph3 =
564 fo_unif_subst subst context metasenv
565 expected_type' actual_type ugraph2
567 let rec instantiate_prod t =
571 match CicReduction.whd ~subst context t with
573 instantiate_prod (CicSubstitution.subst he t') tl
576 let arity_instantiated_with_left_args =
577 instantiate_prod arity left_args in
578 (* TODO: check if the sort elimination
579 * is allowed: [(I q1 ... qr)|B] *)
580 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
582 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
584 if left_args = [] then
585 (C.MutConstruct (uri,i,j,exp_named_subst))
588 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
590 let p',actual_type,subst,metasenv,ugraph1 =
591 type_of_aux subst metasenv context p ugraph
593 let constructor',expected_type, subst, metasenv,ugraph2 =
594 type_of_aux subst metasenv context constructor ugraph1
596 let outtypeinstance,subst,metasenv,ugraph3 =
597 check_branch 0 context metasenv subst no_left_params
598 actual_type constructor' expected_type ugraph2
601 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
602 ([],1,[],subst,metasenv,ugraph3) pl
605 (* we are left to check that the outype matches his instances.
606 The easy case is when the outype is specified, that amount
607 to a trivial check. Otherwise, we should guess a type from
613 (let candidate,ugraph5,metasenv,subst =
614 let exp_name_subst, metasenv =
616 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
618 let uris = CicUtil.params_of_obj o in
620 fun uri (acc,metasenv) ->
621 let metasenv',new_meta =
622 CicMkImplicit.mk_implicit metasenv subst context
625 CicMkImplicit.identity_relocation_list_for_metavariable
628 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
632 match left_args,right_args with
633 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
635 let rec mk_right_args =
638 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
640 let right_args_no = List.length right_args in
641 let lifted_left_args =
642 List.map (CicSubstitution.lift right_args_no) left_args
644 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
645 (lifted_left_args @ mk_right_args right_args_no))
648 FreshNamesGenerator.mk_fresh_name ~subst metasenv
649 context Cic.Anonymous ~typ:ty
651 match outtypeinstances with
653 let extended_context =
654 let rec add_right_args =
656 Cic.Prod (name,ty,t) ->
657 Some (name,Cic.Decl ty)::(add_right_args t)
660 (Some (fresh_name,Cic.Decl ty))::
662 (add_right_args arity_instantiated_with_left_args))@
665 let metasenv,new_meta =
666 CicMkImplicit.mk_implicit metasenv subst extended_context
669 CicMkImplicit.identity_relocation_list_for_metavariable
672 let rec add_lambdas b =
674 Cic.Prod (name,ty,t) ->
675 Cic.Lambda (name,ty,(add_lambdas b t))
676 | _ -> Cic.Lambda (fresh_name, ty, b)
679 add_lambdas (Cic.Meta (new_meta,irl))
680 arity_instantiated_with_left_args
682 (Some candidate),ugraph4,metasenv,subst
683 | (constructor_args_no,_,instance,_)::tl ->
685 let instance',subst,metasenv =
686 CicMetaSubst.delift_rels subst metasenv
687 constructor_args_no instance
689 let candidate,ugraph,metasenv,subst =
691 fun (candidate_oty,ugraph,metasenv,subst)
692 (constructor_args_no,_,instance,_) ->
693 match candidate_oty with
694 | None -> None,ugraph,metasenv,subst
697 let instance',subst,metasenv =
698 CicMetaSubst.delift_rels subst metasenv
699 constructor_args_no instance
701 let subst,metasenv,ugraph =
702 fo_unif_subst subst context metasenv
705 candidate_oty,ugraph,metasenv,subst
707 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
708 | CicUnification.UnificationFailure _
709 | CicUnification.Uncertain _ ->
710 None,ugraph,metasenv,subst
711 ) (Some instance',ugraph4,metasenv,subst) tl
714 | None -> None, ugraph,metasenv,subst
716 let rec add_lambdas n b =
718 Cic.Prod (name,ty,t) ->
719 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
721 Cic.Lambda (fresh_name, ty,
722 CicSubstitution.lift (n + 1) t)
725 (add_lambdas 0 t arity_instantiated_with_left_args),
726 ugraph,metasenv,subst
727 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
728 None,ugraph4,metasenv,subst
731 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
733 let subst,metasenv,ugraph =
734 fo_unif_subst subst context metasenv
735 candidate outtype ugraph5
737 C.MutCase (uri, i, outtype, term', pl'),
738 CicReduction.head_beta_reduce
739 (CicMetaSubst.apply_subst subst
740 (Cic.Appl (outtype::right_args@[term']))),
741 subst,metasenv,ugraph)
742 | _ -> (* easy case *)
743 let outtype,outtypety, subst, metasenv,ugraph4 =
744 type_of_aux subst metasenv context outtype ugraph4
746 let tlbody_and_type,subst,metasenv,ugraph4 =
748 (fun x (res,subst,metasenv,ugraph) ->
749 let x',ty,subst',metasenv',ugraph1 =
750 type_of_aux subst metasenv context x ugraph
752 (x', ty)::res,subst',metasenv',ugraph1
753 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
755 let _,_,subst,metasenv,ugraph4 =
756 eat_prods false subst metasenv context
757 outtypety tlbody_and_type ugraph4
759 let _,_, subst, metasenv,ugraph5 =
760 type_of_aux subst metasenv context
761 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
763 let (subst,metasenv,ugraph6) =
765 (fun (subst,metasenv,ugraph)
766 (constructor_args_no,context,instance,args) ->
770 CicSubstitution.lift constructor_args_no outtype
772 C.Appl (outtype'::args)
774 CicReduction.whd ~subst context appl
776 fo_unif_subst subst context metasenv
777 instance instance' ugraph)
778 (subst,metasenv,ugraph5) outtypeinstances
780 C.MutCase (uri, i, outtype, term', pl'),
781 CicReduction.head_beta_reduce
782 (CicMetaSubst.apply_subst subst
783 (C.Appl(outtype::right_args@[term]))),
784 subst,metasenv,ugraph6)
786 let fl_ty',subst,metasenv,types,ugraph1 =
788 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
789 let ty',_,subst',metasenv',ugraph1 =
790 type_of_aux subst metasenv context ty ugraph
792 fl @ [ty'],subst',metasenv',
793 Some (C.Name n,(C.Decl ty')) :: types, ugraph
794 ) ([],subst,metasenv,[],ugraph) fl
796 let len = List.length types in
797 let context' = types@context in
798 let fl_bo',subst,metasenv,ugraph2 =
800 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
801 let metasenv, bo = exp_impl metasenv subst context' bo in
802 let bo',ty_of_bo,subst,metasenv,ugraph1 =
803 type_of_aux subst metasenv context' bo ugraph
805 let subst',metasenv',ugraph' =
806 fo_unif_subst subst context' metasenv
807 ty_of_bo (CicSubstitution.lift len ty) ugraph1
809 fl @ [bo'] , subst',metasenv',ugraph'
810 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
812 let ty = List.nth fl_ty' i in
813 (* now we have the new ty in fl_ty', the new bo in fl_bo',
814 * and we want the new fl with bo' and ty' injected in the right
817 let rec map3 f l1 l2 l3 =
820 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
823 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
826 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
828 let fl_ty',subst,metasenv,types,ugraph1 =
830 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
831 let ty',_,subst',metasenv',ugraph1 =
832 type_of_aux subst metasenv context ty ugraph
834 fl @ [ty'],subst',metasenv',
835 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
836 ) ([],subst,metasenv,[],ugraph) fl
838 let len = List.length types in
839 let context' = types@context in
840 let fl_bo',subst,metasenv,ugraph2 =
842 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
843 let metasenv, bo = exp_impl metasenv subst context' bo in
844 let bo',ty_of_bo,subst,metasenv,ugraph1 =
845 type_of_aux subst metasenv context' bo ugraph
847 let subst',metasenv',ugraph' =
848 fo_unif_subst subst context' metasenv
849 ty_of_bo (CicSubstitution.lift len ty) ugraph1
851 fl @ [bo'],subst',metasenv',ugraph'
852 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
854 let ty = List.nth fl_ty' i in
855 (* now we have the new ty in fl_ty', the new bo in fl_bo',
856 * and we want the new fl with bo' and ty' injected in the right
859 let rec map3 f l1 l2 l3 =
862 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
865 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
868 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
870 (* check_metasenv_consistency checks that the "canonical" context of a
871 metavariable is consitent - up to relocation via the relocation list l -
872 with the actual context *)
873 and check_metasenv_consistency
874 metano subst metasenv context canonical_context l ugraph
876 let module C = Cic in
877 let module R = CicReduction in
878 let module S = CicSubstitution in
879 let lifted_canonical_context =
883 | (Some (n,C.Decl t))::tl ->
884 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
885 | (Some (n,C.Def (t,None)))::tl ->
886 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
887 | None::tl -> None::(aux (i+1) tl)
888 | (Some (n,C.Def (t,Some ty)))::tl ->
890 C.Def ((S.subst_meta l (S.lift i t)),
891 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
893 aux 1 canonical_context
897 (fun (l,subst,metasenv,ugraph) t ct ->
900 l @ [None],subst,metasenv,ugraph
901 | Some t,Some (_,C.Def (ct,_)) ->
902 let subst',metasenv',ugraph' =
904 fo_unif_subst subst context metasenv t ct ugraph
905 with e -> raise (RefineFailure (lazy (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 -> Lazy.force msg | _ -> (Printexc.to_string e))))))
907 l @ [Some t],subst',metasenv',ugraph'
908 | Some t,Some (_,C.Decl ct) ->
909 let t',inferredty,subst',metasenv',ugraph1 =
910 type_of_aux subst metasenv context t ugraph
912 let subst'',metasenv'',ugraph2 =
915 subst' context metasenv' inferredty ct ugraph1
916 with e -> raise (RefineFailure (lazy (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 -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
918 l @ [Some t'], subst'',metasenv'',ugraph2
920 raise (RefineFailure (lazy (sprintf "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" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
922 Invalid_argument _ ->
926 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
927 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
928 (CicMetaSubst.ppcontext subst canonical_context))))
930 and check_exp_named_subst metasubst metasenv context tl ugraph =
931 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
933 [] -> [],metasubst,metasenv,ugraph
934 | ((uri,t) as subst)::tl ->
935 let ty_uri,ugraph1 = type_of_variable uri ugraph in
937 CicSubstitution.subst_vars substs ty_uri in
938 (* CSC: why was this code here? it is wrong
939 (match CicEnvironment.get_cooked_obj ~trust:false uri with
940 Cic.Variable (_,Some bo,_,_) ->
943 "A variable with a body can not be explicit substituted"))
944 | Cic.Variable (_,None,_,_) -> ()
948 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
951 let t',typeoft,metasubst',metasenv',ugraph2 =
952 type_of_aux metasubst metasenv context t ugraph1
954 let metasubst'',metasenv'',ugraph3 =
957 metasubst' context metasenv' typeoft typeofvar ugraph2
959 raise (RefineFailure (lazy
960 ("Wrong Explicit Named Substitution: " ^
961 CicMetaSubst.ppterm metasubst' typeoft ^
962 " not unifiable with " ^
963 CicMetaSubst.ppterm metasubst' typeofvar)))
965 (* FIXME: no mere tail recursive! *)
966 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
967 check_exp_named_subst_aux
968 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
970 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
972 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
975 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
976 let module C = Cic in
977 let context_for_t2 = (Some (name,C.Decl s))::context in
978 let t1'' = CicReduction.whd ~subst context t1 in
979 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
980 match (t1'', t2'') with
981 (C.Sort s1, C.Sort s2)
982 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
983 (* different than Coq manual!!! *)
984 C.Sort s2,subst,metasenv,ugraph
985 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
986 let t' = CicUniv.fresh() in
987 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
988 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
989 C.Sort (C.Type t'),subst,metasenv,ugraph2
990 | (C.Sort _,C.Sort (C.Type t1)) ->
991 C.Sort (C.Type t1),subst,metasenv,ugraph
992 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
993 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
994 (* TODO how can we force the meta to become a sort? If we don't we
995 * brake the invariant that refine produce only well typed terms *)
996 (* TODO if we check the non meta term and if it is a sort then we
997 * are likely to know the exact value of the result e.g. if the rhs
998 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1000 CicMkImplicit.mk_implicit_sort metasenv subst in
1001 let (subst, metasenv,ugraph1) =
1002 fo_unif_subst subst context_for_t2 metasenv
1003 (C.Meta (idx,[])) t2'' ugraph
1005 t2'',subst,metasenv,ugraph1
1011 ("Two sorts were expected, found %s " ^^
1012 "(that reduces to %s) and %s (that reduces to %s)")
1013 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1014 (CicPp.ppterm t2''))))
1017 allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1019 let rec mk_prod metasenv context =
1022 let (metasenv, idx) =
1023 CicMkImplicit.mk_implicit_type metasenv subst context
1026 CicMkImplicit.identity_relocation_list_for_metavariable context
1028 metasenv,Cic.Meta (idx, irl)
1030 let (metasenv, idx) =
1031 CicMkImplicit.mk_implicit_type metasenv subst context
1034 CicMkImplicit.identity_relocation_list_for_metavariable context
1036 let meta = Cic.Meta (idx,irl) in
1038 (* The name must be fresh for context. *)
1039 (* Nevertheless, argty is well-typed only in context. *)
1040 (* Thus I generate a name (name_hint) in context and *)
1041 (* then I generate a name --- using the hint name_hint *)
1042 (* --- that is fresh in (context'@context). *)
1044 (* Cic.Name "pippo" *)
1045 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1046 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1047 (CicMetaSubst.apply_subst_context subst context)
1049 ~typ:(CicMetaSubst.apply_subst subst argty)
1051 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1052 FreshNamesGenerator.mk_fresh_name ~subst
1053 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
1055 let metasenv,target =
1056 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
1058 metasenv,Cic.Prod (name,meta,target)
1060 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1061 let (subst, metasenv,ugraph1) =
1063 fo_unif_subst subst context metasenv hetype hetype' ugraph
1065 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1066 (CicPp.ppterm hetype)
1067 (CicPp.ppterm hetype')
1068 (CicMetaSubst.ppmetasenv [] metasenv)
1069 (CicMetaSubst.ppsubst subst)));
1073 let rec eat_prods metasenv subst context hetype ugraph =
1075 | [] -> [],metasenv,subst,hetype,ugraph
1076 | (hete, hety)::tl ->
1079 let arg,subst,metasenv,ugraph1 =
1081 let subst,metasenv,ugraph1 =
1082 fo_unif_subst subst context metasenv hety s ugraph
1084 hete,subst,metasenv,ugraph1
1085 with exn when allow_coercions ->
1086 (* we search a coercion from hety to s *)
1088 let carr t subst context =
1089 CicMetaSubst.apply_subst subst t
1091 let c_hety = carr hety subst context in
1092 let c_s = carr s subst context in
1093 CoercGraph.look_for_coercion c_hety c_s
1096 | CoercGraph.NoCoercion
1097 | CoercGraph.NotHandled _ -> raise exn
1098 | CoercGraph.NotMetaClosed ->
1099 raise (Uncertain (lazy "Coercions on meta"))
1100 | CoercGraph.SomeCoercion c ->
1101 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
1103 let coerced_args,metasenv',subst',t',ugraph2 =
1104 eat_prods metasenv subst context
1105 (* (CicMetaSubst.subst subst hete t) tl *)
1106 (CicSubstitution.subst hete t) ugraph1 tl
1108 arg::coerced_args,metasenv',subst',t',ugraph2
1112 let coerced_args,metasenv,subst,t,ugraph2 =
1113 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1115 coerced_args,t,subst,metasenv,ugraph2
1118 (* eat prods ends here! *)
1120 let t',ty,subst',metasenv',ugraph1 =
1121 type_of_aux [] metasenv context t ugraph
1123 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1124 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1125 (* Andrea: ho rimesso qui l'applicazione della subst al
1126 metasenv dopo che ho droppato l'invariante che il metsaenv
1127 e' sempre istanziato *)
1128 let substituted_metasenv =
1129 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1131 (* substituted_t,substituted_ty,substituted_metasenv *)
1132 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1134 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1136 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1137 let cleaned_metasenv =
1139 (function (n,context,ty) ->
1140 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1145 | Some (n, Cic.Decl t) ->
1147 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1148 | Some (n, Cic.Def (bo,ty)) ->
1149 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1154 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1156 Some (n, Cic.Def (bo',ty'))
1160 ) substituted_metasenv
1162 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1165 let type_of_aux' metasenv context term ugraph =
1167 type_of_aux' metasenv context term ugraph
1169 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1171 let undebrujin uri typesno tys t =
1174 (fun (name,_,_,_) (i,t) ->
1175 (* here the explicit_named_substituion is assumed to be *)
1177 let t' = Cic.MutInd (uri,i,[]) in
1178 let t = CicSubstitution.subst t' t in
1180 ) tys (typesno - 1,t))
1182 let map_first_n n start f g l =
1183 let rec aux acc k l =
1186 | [] -> raise (Invalid_argument "map_first_n")
1187 | hd :: tl -> f hd k (aux acc (k+1) tl)
1193 (*CSC: this is a very rough approximation; to be finished *)
1194 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1195 let number_of_types = List.length tys in
1196 let subst,metasenv,ugraph,tys =
1198 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1199 let subst,metasenv,ugraph,cl =
1201 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1202 let rec aux ctx k subst = function
1203 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1204 let subst,metasenv,ugraph,tl =
1206 (subst,metasenv,ugraph,[])
1207 (fun t n (subst,metasenv,ugraph,acc) ->
1208 let subst,metasenv,ugraph =
1210 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1212 subst,metasenv,ugraph,(t::acc))
1213 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1216 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1217 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1218 subst,metasenv,ugraph,t
1219 | Cic.Prod (name,s,t) ->
1220 let ctx = (Some (name,Cic.Decl s))::ctx in
1221 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1222 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1226 (lazy "not well formed constructor type"))
1228 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1229 subst,metasenv,ugraph,(name,ty) :: acc)
1230 cl (subst,metasenv,ugraph,[])
1232 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1233 tys ([],metasenv,ugraph,[])
1235 let substituted_tys =
1237 (fun (name,ind,arity,cl) ->
1239 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1241 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1244 metasenv,ugraph,substituted_tys
1246 let typecheck metasenv uri obj =
1247 let ugraph = CicUniv.empty_ugraph in
1249 Cic.Constant (name,Some bo,ty,args,attrs) ->
1250 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1251 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1252 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1253 let bo' = CicMetaSubst.apply_subst subst bo' in
1254 let ty' = CicMetaSubst.apply_subst subst ty' in
1255 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1256 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1257 | Cic.Constant (name,None,ty,args,attrs) ->
1258 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1259 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1260 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1261 assert (metasenv' = metasenv);
1262 (* Here we do not check the metasenv for correctness *)
1263 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1264 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1268 (* instead of raising Uncertain, let's hope that the meta will become
1271 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1273 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1274 let bo' = CicMetaSubst.apply_subst subst bo' in
1275 let ty' = CicMetaSubst.apply_subst subst ty' in
1276 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1277 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1278 | Cic.Variable _ -> assert false (* not implemented *)
1279 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1280 (*CSC: this code is greately simplified and many many checks are missing *)
1281 (*CSC: e.g. the constructors are not required to build their own types, *)
1282 (*CSC: the arities are not required to have as type a sort, etc. *)
1283 let uri = match uri with Some uri -> uri | None -> assert false in
1284 let typesno = List.length tys in
1285 (* first phase: we fix only the types *)
1286 let metasenv,ugraph,tys =
1288 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1289 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1290 metasenv,ugraph,(name,b,ty',cl)::res
1291 ) tys (metasenv,ugraph,[]) in
1293 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1294 (* second phase: we fix only the constructors *)
1295 let metasenv,ugraph,tys =
1297 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1298 let metasenv,ugraph,cl' =
1300 (fun (name,ty) (metasenv,ugraph,res) ->
1301 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1302 let ty',_,metasenv,ugraph =
1303 type_of_aux' metasenv con_context ty ugraph in
1304 let ty' = undebrujin uri typesno tys ty' in
1305 metasenv,ugraph,(name,ty')::res
1306 ) cl (metasenv,ugraph,[])
1308 metasenv,ugraph,(name,b,ty,cl')::res
1309 ) tys (metasenv,ugraph,[]) in
1310 (* third phase: we check the positivity condition *)
1311 let metasenv,ugraph,tys =
1312 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1314 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1317 let type_of_aux' metasenv context term =
1320 type_of_aux' metasenv context term in
1322 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1324 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1327 | RefineFailure msg as e ->
1328 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1330 | Uncertain msg as e ->
1331 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1335 let profiler2 = HExtlib.profile "CicRefine"
1337 let type_of_aux' metasenv context term ugraph =
1338 profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
1340 let typecheck metasenv uri obj =
1341 profiler2.HExtlib.profile (typecheck metasenv uri) obj