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 Impossible of int;;
29 exception NotRefinable of string;;
30 exception Uncertain of string;;
31 exception WrongUriToConstant of string;;
32 exception WrongUriToVariable of string;;
33 exception ListTooShort;;
34 exception WrongUriToMutualInductiveDefinitions of string;;
35 exception RelToHiddenHypothesis;;
36 exception MetasenvInconsistency;;
37 exception MutCaseFixAndCofixRefineNotImplemented;;
38 exception FreeMetaFound of int;;
39 exception WrongArgumentNumber;;
43 let rec debug_aux t i =
45 let module U = UriManager in
46 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
49 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
50 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
53 let debug_print = prerr_endline
58 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
59 | (_,_) -> raise ListTooShort
62 let rec type_of_constant uri =
64 let module R = CicReduction in
65 let module U = UriManager in
66 match CicEnvironment.get_cooked_obj uri with
67 C.Constant (_,_,ty,_) -> ty
68 | C.CurrentProof (_,_,_,ty,_) -> ty
69 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
71 and type_of_variable uri =
73 let module R = CicReduction in
74 let module U = UriManager in
75 match CicEnvironment.get_cooked_obj uri with
76 C.Variable (_,_,ty,_) -> ty
77 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
79 and type_of_mutual_inductive_defs uri i =
81 let module R = CicReduction in
82 let module U = UriManager in
83 match CicEnvironment.get_cooked_obj uri with
84 C.InductiveDefinition (dl,_,_) ->
85 let (_,_,arity,_) = List.nth dl i in
87 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
89 and type_of_mutual_inductive_constr uri i j =
91 let module R = CicReduction in
92 let module U = UriManager in
93 match CicEnvironment.get_cooked_obj uri with
94 C.InductiveDefinition (dl,_,_) ->
95 let (_,_,_,cl) = List.nth dl i in
96 let (_,ty) = List.nth cl (j-1) in
98 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
100 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
102 (* the check_branch function checks if a branch of a case is refinable.
103 It returns a pair (outype_instance,args), a subst and a metasenv.
104 outype_instance is the expected result of applying the case outtype
106 The problem is that outype is in general unknown, and we should
107 try to synthesize it from the above information, that is in general
108 a second order unification problem. *)
110 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
111 let module C = Cic in
112 let module R = CicMetaSubst in
113 let module Un = CicUnification in
114 match R.whd subst context expectedtype with
116 (n,context,actualtype, [term]), subst, metasenv
117 | C.Appl (C.MutInd (_,_,_)::tl) ->
118 let (_,arguments) = split tl left_args_no in
119 (n,context,actualtype, arguments@[term]), subst, metasenv
120 | C.Prod (name,so,de) ->
121 (* we expect that the actual type of the branch has the due
123 (match R.whd subst context actualtype with
124 C.Prod (name',so',de') ->
125 let subst, metasenv =
126 Un.fo_unif_subst subst context metasenv so so' in
128 (match CicSubstitution.lift 1 term with
129 C.Appl l -> C.Appl (l@[C.Rel 1])
130 | t -> C.Appl [t ; C.Rel 1]) in
131 (* we should also check that the name variable is anonymous in
132 the actual type de' ?? *)
133 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
134 | _ -> raise WrongArgumentNumber)
135 | _ -> raise (NotRefinable "Prod or MutInd expected")
137 and type_of_aux' metasenv context t =
138 let rec type_of_aux subst metasenv context =
139 let module C = Cic in
140 let module S = CicSubstitution in
141 let module U = UriManager in
142 let module Un = CicUnification in
146 match List.nth context (n - 1) with
147 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
148 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
149 | Some (_,C.Def (bo,None)) ->
150 type_of_aux subst metasenv context (S.lift n bo)
151 | None -> raise RelToHiddenHypothesis
153 _ -> raise (NotRefinable "Not a close term")
155 | C.Var (uri,exp_named_subst) ->
157 let subst',metasenv' =
158 check_exp_named_subst subst metasenv context exp_named_subst in
160 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
165 let (_,canonical_context,ty) =
167 List.find (function (m,_,_) -> n = m) metasenv
169 Not_found -> raise (FreeMetaFound n)
171 let subst',metasenv' =
172 check_metasenv_consistency subst metasenv context canonical_context l
174 CicSubstitution.lift_meta l ty, subst', metasenv'
176 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
178 | C.Implicit -> raise (Impossible 21)
180 let _,subst',metasenv' =
181 type_of_aux subst metasenv context ty in
182 let inferredty,subst'',metasenv'' =
183 type_of_aux subst' metasenv' context ty
186 let subst''',metasenv''' =
187 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
189 ty,subst''',metasenv'''
191 _ -> raise (NotRefinable "Cast"))
192 | C.Prod (name,s,t) ->
193 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
194 let sort2,subst'',metasenv'' =
195 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
197 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
198 | C.Lambda (n,s,t) ->
199 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
200 let type2,subst'',metasenv'' =
201 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
203 let sort2,subst''',metasenv''' =
204 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
206 (* only to check if the product is well-typed *)
207 let _,subst'''',metasenv'''' =
208 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
210 C.Prod (n,s,type2),subst'''',metasenv''''
212 (* only to check if s is well-typed *)
213 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
214 let inferredty,subst'',metasenv'' =
215 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
217 (* One-step LetIn reduction. Even faster than the previous solution.
218 Moreover the inferred type is closer to the expected one. *)
219 CicSubstitution.subst s inferredty,subst',metasenv'
220 | C.Appl (he::tl) when List.length tl > 0 ->
221 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
222 let tlbody_and_type,subst'',metasenv'' =
224 (fun x (res,subst,metasenv) ->
225 let ty,subst',metasenv' =
226 type_of_aux subst metasenv context x
228 (x, ty)::res,subst',metasenv'
229 ) tl ([],subst',metasenv')
231 eat_prods subst'' metasenv'' context hetype tlbody_and_type
232 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
233 | C.Const (uri,exp_named_subst) ->
235 let subst',metasenv' =
236 check_exp_named_subst subst metasenv context exp_named_subst in
238 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
242 | C.MutInd (uri,i,exp_named_subst) ->
244 let subst',metasenv' =
245 check_exp_named_subst subst metasenv context exp_named_subst in
247 CicSubstitution.subst_vars exp_named_subst
248 (type_of_mutual_inductive_defs uri i)
252 | C.MutConstruct (uri,i,j,exp_named_subst) ->
253 let subst',metasenv' =
254 check_exp_named_subst subst metasenv context exp_named_subst in
256 CicSubstitution.subst_vars exp_named_subst
257 (type_of_mutual_inductive_constr uri i j)
260 | C.MutCase (uri, i, outtype, term, pl) ->
261 (* first, get the inductive type (and noparams) in the environment *)
262 let (_,b,arity,constructors), expl_params, no_left_params =
263 match CicEnvironment.get_cooked_obj ~trust:true uri with
264 C.InductiveDefinition (l,expl_params,parsno) ->
265 List.nth l i , expl_params, parsno
268 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
269 let rec count_prod t =
270 match CicMetaSubst.whd subst context t with
271 C.Prod (_, _, t) -> 1 + (count_prod t)
273 let no_args = count_prod arity in
274 (* now, create a "generic" MutInd *)
275 let metasenv,left_args =
276 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
277 let metasenv,right_args =
278 let no_right_params = no_args - no_left_params in
279 if no_right_params < 0 then assert false
280 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
281 let metasenv,exp_named_subst =
282 CicMkImplicit.fresh_subst metasenv context expl_params in
285 C.MutInd (uri,i,exp_named_subst)
287 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
289 (* check consistency with the actual type of term *)
290 let actual_type,subst,metasenv =
291 type_of_aux subst metasenv context term in
292 let _, subst, metasenv =
293 type_of_aux subst metasenv context expected_type
295 let actual_type = CicMetaSubst.whd subst context actual_type in
297 Un.fo_unif_subst subst context metasenv expected_type actual_type
299 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
300 let (_,outtypeinstances,subst,metasenv) =
302 (fun (j,outtypeinstances,subst,metasenv) p ->
304 if left_args = [] then
305 (C.MutConstruct (uri,i,j,exp_named_subst))
307 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
309 let actual_type,subst,metasenv =
310 type_of_aux subst metasenv context p in
311 let expected_type, subst, metasenv =
312 type_of_aux subst metasenv context constructor in
313 let outtypeinstance,subst,metasenv =
315 0 context metasenv subst
316 no_left_params actual_type constructor expected_type in
317 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
318 (1,[],subst,metasenv) pl in
319 (* we are left to check that the outype matches his instances.
320 The easy case is when the outype is specified, that amount
321 to a trivial check. Otherwise, we should guess a type from
324 let _, subst, metasenv =
325 type_of_aux subst metasenv context
326 (C.Appl ((outtype :: right_args) @ [term]))
328 let (subst,metasenv) =
330 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
334 CicSubstitution.lift constructor_args_no outtype
336 C.Appl (outtype'::args)
339 (* if appl is not well typed then the type_of below solves the
341 let (_, subst, metasenv) =
342 type_of_aux subst metasenv context appl
345 CicMetaSubst.whd subst context appl
347 Un.fo_unif_subst subst context metasenv instance instance')
348 (subst,metasenv) outtypeinstances in
349 CicMetaSubst.whd subst
350 context (C.Appl(outtype::right_args@[term])),subst,metasenv
352 | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
354 (* check_metasenv_consistency checks that the "canonical" context of a
355 metavariable is consitent - up to relocation via the relocation list l -
356 with the actual context *)
357 and check_metasenv_consistency subst metasenv context canonical_context l =
358 let module C = Cic in
359 let module R = CicReduction in
360 let module S = CicSubstitution in
361 let lifted_canonical_context =
365 | (Some (n,C.Decl t))::tl ->
366 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
367 | (Some (n,C.Def (t,None)))::tl ->
368 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
369 | None::tl -> None::(aux (i+1) tl)
370 | (Some (_,C.Def (_,Some _)))::_ -> assert false
372 aux 1 canonical_context
375 (fun (subst,metasenv) t ct ->
379 | Some t,Some (_,C.Def (ct,_)) ->
381 CicUnification.fo_unif_subst subst context metasenv t ct
382 with _ -> raise MetasenvInconsistency)
383 | Some t,Some (_,C.Decl ct) ->
384 let inferredty,subst',metasenv' =
385 type_of_aux subst metasenv context t
388 CicUnification.fo_unif_subst
389 subst' context metasenv' inferredty ct
390 with _ -> raise MetasenvInconsistency)
392 raise MetasenvInconsistency
393 ) (subst,metasenv) l lifted_canonical_context
395 and check_exp_named_subst metasubst metasenv context =
396 let rec check_exp_named_subst_aux metasubst metasenv substs =
398 [] -> metasubst,metasenv
399 | ((uri,t) as subst)::tl ->
401 CicSubstitution.subst_vars substs (type_of_variable uri) in
402 (match CicEnvironment.get_cooked_obj ~trust:false uri with
403 Cic.Variable (_,Some bo,_,_) ->
406 "A variable with a body can not be explicit substituted")
407 | Cic.Variable (_,None,_,_) -> ()
408 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
410 let typeoft,metasubst',metasenv' =
411 type_of_aux metasubst metasenv context t
414 let metasubst'',metasenv'' =
415 CicUnification.fo_unif_subst
416 metasubst' context metasenv' typeoft typeofvar
418 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
420 raise (NotRefinable "Wrong Explicit Named Substitution")
422 check_exp_named_subst_aux metasubst metasenv []
424 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
425 let module C = Cic in
426 (* ti could be a metavariable in the domain of the substitution *)
427 let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
428 let t1' = CicMetaSubst.apply_subst subst' t1 in
429 let t2' = CicMetaSubst.apply_subst subst' t2 in
430 let t1'' = CicMetaSubst.whd subst' context t1' in
431 let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in
432 match (t1'', t2'') with
433 (C.Sort s1, C.Sort s2)
434 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
435 C.Sort s2,subst',metasenv'
436 | (C.Sort s1, C.Sort s2) ->
437 (*CSC manca la gestione degli universi!!! *)
438 C.Sort C.Type,subst',metasenv'
439 | (C.Meta _,_) | (_,C.Meta _) ->
440 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
442 CicMkImplicit.identity_relocation_list_for_metavariable context
444 C.Meta (idx, irl), subst, metasenv'
446 raise (NotRefinable (sprintf
447 "Two types were expected, found %s of type %s and %s of type %s"
448 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
449 (CicPp.ppterm t2'')))
451 and eat_prods subst metasenv context hetype =
453 [] -> hetype,subst,metasenv
454 | (hete, hety)::tl ->
455 (match (CicMetaSubst.whd subst context hetype) with
457 let subst',metasenv' =
458 CicUnification.fo_unif_subst subst context metasenv s hety
460 CicReduction.fdebug := -1 ;
461 eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
465 ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
466 | _ -> raise (NotRefinable "Appl: wrong Prod-type")
469 let ty,subst',metasenv' =
470 type_of_aux [] metasenv context t
472 let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in
473 (* we get rid of the metavariables that have been instantiated *)
476 (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
479 CicMetaSubst.apply_subst subst'' t,
480 CicMetaSubst.apply_subst subst'' ty,
485 let type_of_aux' metasenv context term =
487 let (t,ty,s,m) = type_of_aux' metasenv context term in
491 debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
494 debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
497 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
500 | CicUnification.AssertFailure msg as e ->
501 debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
504 | CicUnification.UnificationFailure msg as e ->
505 debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
512 debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
515 debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;