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 WrongArgumentNumber;;
42 let rec debug_aux t i =
44 let module U = UriManager in
45 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
48 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
49 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
52 let debug_print = prerr_endline
57 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
58 | (_,_) -> raise ListTooShort
61 let rec type_of_constant uri =
63 let module R = CicReduction in
64 let module U = UriManager in
65 match CicEnvironment.get_cooked_obj uri with
66 C.Constant (_,_,ty,_) -> ty
67 | C.CurrentProof (_,_,_,ty,_) -> ty
68 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
70 and type_of_variable uri =
72 let module R = CicReduction in
73 let module U = UriManager in
74 match CicEnvironment.get_cooked_obj uri with
75 C.Variable (_,_,ty,_) -> ty
76 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
78 and type_of_mutual_inductive_defs uri i =
80 let module R = CicReduction in
81 let module U = UriManager in
82 match CicEnvironment.get_cooked_obj uri with
83 C.InductiveDefinition (dl,_,_) ->
84 let (_,_,arity,_) = List.nth dl i in
86 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
88 and type_of_mutual_inductive_constr uri i j =
90 let module R = CicReduction in
91 let module U = UriManager in
92 match CicEnvironment.get_cooked_obj uri with
93 C.InductiveDefinition (dl,_,_) ->
94 let (_,_,_,cl) = List.nth dl i in
95 let (_,ty) = List.nth cl (j-1) in
97 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
99 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
101 (* the check_branch function checks if a branch of a case is refinable.
102 It returns a pair (outype_instance,args), a subst and a metasenv.
103 outype_instance is the expected result of applying the case outtype
105 The problem is that outype is in general unknown, and we should
106 try to synthesize it from the above information, that is in general
107 a second order unification problem. *)
109 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
110 let module C = Cic in
111 let module R = CicMetaSubst in
112 let module Un = CicUnification in
113 match R.whd metasenv subst context expectedtype with
115 (n,context,actualtype, [term]), subst, metasenv
116 | C.Appl (C.MutInd (_,_,_)::tl) ->
117 let (_,arguments) = split tl left_args_no in
118 (n,context,actualtype, arguments@[term]), subst, metasenv
119 | C.Prod (name,so,de) ->
120 (* we expect that the actual type of the branch has the due
122 (match R.whd metasenv subst context actualtype with
123 C.Prod (name',so',de') ->
124 let subst, metasenv =
125 Un.fo_unif_subst subst context metasenv so so' in
127 (match CicSubstitution.lift 1 term with
128 C.Appl l -> C.Appl (l@[C.Rel 1])
129 | t -> C.Appl [t ; C.Rel 1]) in
130 (* we should also check that the name variable is anonymous in
131 the actual type de' ?? *)
132 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
133 | _ -> raise WrongArgumentNumber)
134 | _ -> raise (NotRefinable "Prod or MutInd expected")
136 and type_of_aux' metasenv context t =
137 let rec type_of_aux subst metasenv context =
138 let module C = Cic in
139 let module S = CicSubstitution in
140 let module U = UriManager in
141 let module Un = CicUnification in
145 match List.nth context (n - 1) with
146 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
147 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
148 | Some (_,C.Def (bo,None)) ->
149 type_of_aux subst metasenv context (S.lift n bo)
150 | None -> raise RelToHiddenHypothesis
152 _ -> raise (NotRefinable "Not a close term")
154 | C.Var (uri,exp_named_subst) ->
156 let subst',metasenv' =
157 check_exp_named_subst subst metasenv context exp_named_subst in
159 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
164 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
165 let subst',metasenv' =
166 check_metasenv_consistency subst metasenv context canonical_context l
168 CicSubstitution.lift_meta l ty, subst', metasenv'
170 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
172 | C.Implicit -> raise (Impossible 21)
174 let _,subst',metasenv' =
175 type_of_aux subst metasenv context ty in
176 let inferredty,subst'',metasenv'' =
177 type_of_aux subst' metasenv' context ty
180 let subst''',metasenv''' =
181 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
183 ty,subst''',metasenv'''
185 _ -> raise (NotRefinable "Cast"))
186 | C.Prod (name,s,t) ->
187 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
188 let sort2,subst'',metasenv'' =
189 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
191 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
192 | C.Lambda (n,s,t) ->
193 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
194 let type2,subst'',metasenv'' =
195 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
197 let sort2,subst''',metasenv''' =
198 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
200 (* only to check if the product is well-typed *)
201 let _,subst'''',metasenv'''' =
202 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
204 C.Prod (n,s,type2),subst'''',metasenv''''
206 (* only to check if s is well-typed *)
207 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
208 let inferredty,subst'',metasenv'' =
209 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
211 (* One-step LetIn reduction. Even faster than the previous solution.
212 Moreover the inferred type is closer to the expected one. *)
213 CicSubstitution.subst s inferredty,subst',metasenv'
214 | C.Appl (he::tl) when List.length tl > 0 ->
215 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
216 let tlbody_and_type,subst'',metasenv'' =
218 (fun x (res,subst,metasenv) ->
219 let ty,subst',metasenv' =
220 type_of_aux subst metasenv context x
222 (x, ty)::res,subst',metasenv'
223 ) tl ([],subst',metasenv')
225 eat_prods subst'' metasenv'' context hetype tlbody_and_type
226 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
227 | C.Const (uri,exp_named_subst) ->
229 let subst',metasenv' =
230 check_exp_named_subst subst metasenv context exp_named_subst in
232 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
236 | C.MutInd (uri,i,exp_named_subst) ->
238 let subst',metasenv' =
239 check_exp_named_subst subst metasenv context exp_named_subst in
241 CicSubstitution.subst_vars exp_named_subst
242 (type_of_mutual_inductive_defs uri i)
246 | C.MutConstruct (uri,i,j,exp_named_subst) ->
247 let subst',metasenv' =
248 check_exp_named_subst subst metasenv context exp_named_subst in
250 CicSubstitution.subst_vars exp_named_subst
251 (type_of_mutual_inductive_constr uri i j)
254 | C.MutCase (uri, i, outtype, term, pl) ->
255 (* first, get the inductive type (and noparams) in the environment *)
256 let (_,b,arity,constructors), expl_params, no_left_params =
257 match CicEnvironment.get_cooked_obj ~trust:true uri with
258 C.InductiveDefinition (l,expl_params,parsno) ->
259 List.nth l i , expl_params, parsno
262 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
263 let rec count_prod t =
264 match CicMetaSubst.whd metasenv subst context t with
265 C.Prod (_, _, t) -> 1 + (count_prod t)
267 let no_args = count_prod arity in
268 (* now, create a "generic" MutInd *)
269 let metasenv,left_args =
270 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
271 let metasenv,right_args =
272 let no_right_params = no_args - no_left_params in
273 if no_right_params < 0 then assert false
274 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
275 let metasenv,exp_named_subst =
276 CicMkImplicit.fresh_subst metasenv context expl_params in
279 C.MutInd (uri,i,exp_named_subst)
281 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
283 (* check consistency with the actual type of term *)
284 let actual_type,subst,metasenv =
285 type_of_aux subst metasenv context term in
286 let _, subst, metasenv =
287 type_of_aux subst metasenv context expected_type
289 let actual_type = CicMetaSubst.whd metasenv subst context actual_type in
291 Un.fo_unif_subst subst context metasenv expected_type actual_type
293 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
294 let (_,outtypeinstances,subst,metasenv) =
296 (fun (j,outtypeinstances,subst,metasenv) p ->
298 if left_args = [] then
299 (C.MutConstruct (uri,i,j,exp_named_subst))
301 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
303 let actual_type,subst,metasenv =
304 type_of_aux subst metasenv context p in
305 let expected_type, subst, metasenv =
306 type_of_aux subst metasenv context constructor in
307 let outtypeinstance,subst,metasenv =
309 0 context metasenv subst
310 no_left_params actual_type constructor expected_type in
311 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
312 (1,[],subst,metasenv) pl in
313 (* we are left to check that the outype matches his instances.
314 The easy case is when the outype is specified, that amount
315 to a trivial check. Otherwise, we should guess a type from
318 let _, subst, metasenv =
319 type_of_aux subst metasenv context
320 (C.Appl ((outtype :: right_args) @ [term]))
322 let (subst,metasenv) =
324 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
328 CicSubstitution.lift constructor_args_no outtype
330 C.Appl (outtype'::args)
333 (* if appl is not well typed then the type_of below solves the
335 let (_, subst, metasenv) =
336 type_of_aux subst metasenv context appl
339 CicMetaSubst.whd metasenv subst context appl
341 Un.fo_unif_subst subst context metasenv instance instance')
342 (subst,metasenv) outtypeinstances in
343 CicMetaSubst.whd metasenv subst
344 context (C.Appl(outtype::right_args@[term])),subst,metasenv
346 | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
348 (* check_metasenv_consistency checks that the "canonical" context of a
349 metavariable is consitent - up to relocation via the relocation list l -
350 with the actual context *)
351 and check_metasenv_consistency subst metasenv context canonical_context l =
352 let module C = Cic in
353 let module R = CicReduction in
354 let module S = CicSubstitution in
355 let lifted_canonical_context =
359 | (Some (n,C.Decl t))::tl ->
360 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
361 | (Some (n,C.Def (t,None)))::tl ->
362 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
363 | None::tl -> None::(aux (i+1) tl)
364 | (Some (_,C.Def (_,Some _)))::_ -> assert false
366 aux 1 canonical_context
369 (fun (subst,metasenv) t ct ->
373 | Some t,Some (_,C.Def (ct,_)) ->
375 CicUnification.fo_unif_subst subst context metasenv t ct
376 with _ -> raise MetasenvInconsistency)
377 | Some t,Some (_,C.Decl ct) ->
378 let inferredty,subst',metasenv' =
379 type_of_aux subst metasenv context t
382 CicUnification.fo_unif_subst
383 subst' context metasenv' inferredty ct
384 with _ -> raise MetasenvInconsistency)
386 raise MetasenvInconsistency
387 ) (subst,metasenv) l lifted_canonical_context
389 and check_exp_named_subst metasubst metasenv context =
390 let rec check_exp_named_subst_aux metasubst metasenv substs =
392 [] -> metasubst,metasenv
393 | ((uri,t) as subst)::tl ->
395 CicSubstitution.subst_vars substs (type_of_variable uri) in
396 (match CicEnvironment.get_cooked_obj ~trust:false uri with
397 Cic.Variable (_,Some bo,_,_) ->
400 "A variable with a body can not be explicit substituted")
401 | Cic.Variable (_,None,_,_) -> ()
402 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
404 let typeoft,metasubst',metasenv' =
405 type_of_aux metasubst metasenv context t
408 let metasubst'',metasenv'' =
409 CicUnification.fo_unif_subst
410 metasubst' context metasenv' typeoft typeofvar
412 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
414 raise (NotRefinable "Wrong Explicit Named Substitution")
416 check_exp_named_subst_aux metasubst metasenv []
418 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
419 let module C = Cic in
420 (* ti could be a metavariable in the domain of the substitution *)
421 let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
422 let t1' = CicMetaSubst.apply_subst subst' t1 in
423 let t2' = CicMetaSubst.apply_subst subst' t2 in
424 let t1'' = CicMetaSubst.whd metasenv subst' context t1' in
426 CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2'
428 match (t1'', t2'') with
429 (C.Sort s1, C.Sort s2)
430 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
431 C.Sort s2,subst',metasenv'
432 | (C.Sort s1, C.Sort s2) ->
433 (*CSC manca la gestione degli universi!!! *)
434 C.Sort C.Type,subst',metasenv'
435 | (C.Meta _,_) | (_,C.Meta _) ->
436 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
438 CicMkImplicit.identity_relocation_list_for_metavariable context
440 C.Meta (idx, irl), subst, metasenv'
442 raise (NotRefinable (sprintf
443 "Two types were expected, found %s of type %s and %s of type %s"
444 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
445 (CicPp.ppterm t2'')))
447 and eat_prods subst metasenv context hetype =
449 [] -> hetype,subst,metasenv
450 | (hete, hety)::tl ->
451 (match (CicMetaSubst.whd metasenv subst context hetype) with
453 let subst',metasenv' =
454 CicUnification.fo_unif_subst subst context metasenv s hety
456 CicReduction.fdebug := -1 ;
457 eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
461 ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
462 | _ -> raise (NotRefinable "Appl: wrong Prod-type")
465 let ty,subst',metasenv' =
466 type_of_aux [] metasenv context t
468 let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in
469 (* we get rid of the metavariables that have been instantiated *)
472 (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
475 CicMetaSubst.apply_subst subst'' t,
476 CicMetaSubst.apply_subst subst'' ty,
481 let type_of_aux' metasenv context term =
483 let (t,ty,s,m) = type_of_aux' metasenv context term in
487 debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
490 debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
493 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
496 | CicUnification.AssertFailure msg as e ->
497 debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
500 | CicUnification.UnificationFailure msg as e ->
501 debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
508 debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
511 debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;