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/.
26 exception Impossible of int;;
27 exception NotRefinable of string;;
28 exception Uncertain of string;;
29 exception WrongUriToConstant of string;;
30 exception WrongUriToVariable of string;;
31 exception ListTooShort;;
32 exception WrongUriToMutualInductiveDefinitions of string;;
33 exception RelToHiddenHypothesis;;
34 exception MetasenvInconsistency;;
35 exception MutCaseFixAndCofixRefineNotImplemented;;
36 exception FreeMetaFound of int;;
37 exception WrongArgumentNumber;;
41 let rec debug_aux t i =
43 let module U = UriManager in
44 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
47 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
48 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
51 let debug_print = prerr_endline
56 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
57 | (_,_) -> raise ListTooShort
60 let rec type_of_constant uri =
62 let module R = CicReduction in
63 let module U = UriManager in
64 match CicEnvironment.get_cooked_obj uri with
65 C.Constant (_,_,ty,_) -> ty
66 | C.CurrentProof (_,_,_,ty,_) -> ty
67 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
69 and type_of_variable uri =
71 let module R = CicReduction in
72 let module U = UriManager in
73 match CicEnvironment.get_cooked_obj uri with
74 C.Variable (_,_,ty,_) -> ty
75 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
77 and type_of_mutual_inductive_defs uri i =
79 let module R = CicReduction in
80 let module U = UriManager in
81 match CicEnvironment.get_cooked_obj uri with
82 C.InductiveDefinition (dl,_,_) ->
83 let (_,_,arity,_) = List.nth dl i in
85 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
87 and type_of_mutual_inductive_constr uri i j =
89 let module R = CicReduction in
90 let module U = UriManager in
91 match CicEnvironment.get_cooked_obj uri with
92 C.InductiveDefinition (dl,_,_) ->
93 let (_,_,_,cl) = List.nth dl i in
94 let (_,ty) = List.nth cl (j-1) in
96 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
98 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
100 (* the check_branch function checks if a branch of a case is refinable.
101 It returns a pair (outype_instance,args), a subst and a metasenv.
102 outype_instance is the expected result of applying the case outtype
104 The problem is that outype is in general unknown, and we should
105 try to synthesize it from the above information, that is in general
106 a second order unification problem. *)
108 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
109 let module C = Cic in
110 let module R = CicMetaSubst in
111 let module Un = CicUnification in
112 match R.whd subst context expectedtype with
114 (n,context,actualtype, [term]), subst, metasenv
115 | C.Appl (C.MutInd (_,_,_)::tl) ->
116 let (_,arguments) = split tl left_args_no in
117 (n,context,actualtype, arguments@[term]), subst, metasenv
118 | C.Prod (name,so,de) ->
119 (* we expect that the actual type of the branch has the due
121 (match R.whd subst context actualtype with
122 C.Prod (name',so',de') ->
123 let subst, metasenv =
124 Un.fo_unif_subst subst context metasenv so so' in
126 (match CicSubstitution.lift 1 term with
127 C.Appl l -> C.Appl (l@[C.Rel 1])
128 | t -> C.Appl [t ; C.Rel 1]) in
129 (* we should also check that the name variable is anonymous in
130 the actual type de' ?? *)
131 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
132 | _ -> raise WrongArgumentNumber)
133 | _ -> raise (NotRefinable "Prod or MutInd expected")
135 and type_of_aux' metasenv context t =
136 let rec type_of_aux subst metasenv context =
137 let module C = Cic in
138 let module S = CicSubstitution in
139 let module U = UriManager in
140 let module Un = CicUnification in
144 match List.nth context (n - 1) with
145 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
146 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
147 | Some (_,C.Def (bo,None)) ->
148 type_of_aux subst metasenv context (S.lift n bo)
149 | None -> raise RelToHiddenHypothesis
151 _ -> raise (NotRefinable "Not a close term")
153 | C.Var (uri,exp_named_subst) ->
155 let subst',metasenv' =
156 check_exp_named_subst subst metasenv context exp_named_subst in
158 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
163 let (_,canonical_context,ty) =
165 List.find (function (m,_,_) -> n = m) metasenv
167 Not_found -> raise (FreeMetaFound n)
169 let subst',metasenv' =
170 check_metasenv_consistency subst metasenv context canonical_context l
172 CicSubstitution.lift_meta l ty, subst', metasenv'
174 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
176 | C.Implicit -> raise (Impossible 21)
178 let _,subst',metasenv' =
179 type_of_aux subst metasenv context ty in
180 let inferredty,subst'',metasenv'' =
181 type_of_aux subst' metasenv' context ty
184 let subst''',metasenv''' =
185 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
187 ty,subst''',metasenv'''
189 _ -> raise (NotRefinable "Cast"))
190 | C.Prod (name,s,t) ->
191 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
192 let sort2,subst'',metasenv'' =
193 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
195 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
196 | C.Lambda (n,s,t) ->
197 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
198 let type2,subst'',metasenv'' =
199 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
201 let sort2,subst''',metasenv''' =
202 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
204 (* only to check if the product is well-typed *)
205 let _,subst'''',metasenv'''' =
206 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
208 C.Prod (n,s,type2),subst'''',metasenv''''
210 (* only to check if s is well-typed *)
211 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
212 let inferredty,subst'',metasenv'' =
213 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
215 (* One-step LetIn reduction. Even faster than the previous solution.
216 Moreover the inferred type is closer to the expected one. *)
217 CicSubstitution.subst s inferredty,subst',metasenv'
218 | C.Appl (he::tl) when List.length tl > 0 ->
219 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
220 let tlbody_and_type,subst'',metasenv'' =
222 (fun x (res,subst,metasenv) ->
223 let ty,subst',metasenv' =
224 type_of_aux subst metasenv context x
226 (x, ty)::res,subst',metasenv'
227 ) tl ([],subst',metasenv')
229 eat_prods subst'' metasenv'' context hetype tlbody_and_type
230 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
231 | C.Const (uri,exp_named_subst) ->
233 let subst',metasenv' =
234 check_exp_named_subst subst metasenv context exp_named_subst in
236 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
240 | C.MutInd (uri,i,exp_named_subst) ->
242 let subst',metasenv' =
243 check_exp_named_subst subst metasenv context exp_named_subst in
245 CicSubstitution.subst_vars exp_named_subst
246 (type_of_mutual_inductive_defs uri i)
250 | C.MutConstruct (uri,i,j,exp_named_subst) ->
251 let subst',metasenv' =
252 check_exp_named_subst subst metasenv context exp_named_subst in
254 CicSubstitution.subst_vars exp_named_subst
255 (type_of_mutual_inductive_constr uri i j)
258 | C.MutCase (uri, i, outtype, term, pl) ->
259 (* first, get the inductive type (and noparams) in the environment *)
260 let (_,b,arity,constructors), expl_params, no_left_params =
261 match CicEnvironment.get_cooked_obj ~trust:true uri with
262 C.InductiveDefinition (l,expl_params,parsno) ->
263 List.nth l i , expl_params, parsno
266 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
267 let rec count_prod t =
268 match CicMetaSubst.whd subst context t with
269 C.Prod (_, _, t) -> 1 + (count_prod t)
271 let no_args = count_prod arity in
272 (* now, create a "generic" MutInd *)
273 let metasenv,left_args =
274 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
275 let metasenv,right_args =
276 let no_right_params = no_args - no_left_params in
277 if no_right_params < 0 then assert false
278 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
279 let metasenv,exp_named_subst =
280 CicMkImplicit.fresh_subst metasenv context expl_params in
283 C.MutInd (uri,i,exp_named_subst)
285 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
287 (* check consistency with the actual type of term *)
288 let actual_type,subst,metasenv =
289 type_of_aux subst metasenv context term in
290 let _, subst, metasenv =
291 type_of_aux subst metasenv context expected_type
293 let actual_type = CicMetaSubst.whd subst context actual_type in
295 Un.fo_unif_subst subst context metasenv expected_type actual_type
297 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
298 let (_,outtypeinstances,subst,metasenv) =
300 (fun (j,outtypeinstances,subst,metasenv) p ->
302 if left_args = [] then
303 (C.MutConstruct (uri,i,j,exp_named_subst))
305 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
307 let actual_type,subst,metasenv =
308 type_of_aux subst metasenv context p in
309 let expected_type, subst, metasenv =
310 type_of_aux subst metasenv context constructor in
311 let outtypeinstance,subst,metasenv =
313 0 context metasenv subst
314 no_left_params actual_type constructor expected_type in
315 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
316 (1,[],subst,metasenv) pl in
317 (* we are left to check that the outype matches his instances.
318 The easy case is when the outype is specified, that amount
319 to a trivial check. Otherwise, we should guess a type from
322 let _, subst, metasenv =
323 type_of_aux subst metasenv context
324 (C.Appl ((outtype :: right_args) @ [term]))
326 let (subst,metasenv) =
328 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
332 CicSubstitution.lift constructor_args_no outtype
334 C.Appl (outtype'::args)
337 (* if appl is not well typed then the type_of below solves the
339 let (_, subst, metasenv) =
340 type_of_aux subst metasenv context appl
343 CicMetaSubst.whd subst context appl
345 Un.fo_unif_subst subst context metasenv instance instance')
346 (subst,metasenv) outtypeinstances in
347 CicMetaSubst.whd subst
348 context (C.Appl(outtype::right_args@[term])),subst,metasenv
350 | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
352 (* check_metasenv_consistency checks that the "canonical" context of a
353 metavariable is consitent - up to relocation via the relocation list l -
354 with the actual context *)
355 and check_metasenv_consistency subst metasenv context canonical_context l =
356 let module C = Cic in
357 let module R = CicReduction in
358 let module S = CicSubstitution in
359 let lifted_canonical_context =
363 | (Some (n,C.Decl t))::tl ->
364 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
365 | (Some (n,C.Def (t,None)))::tl ->
366 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
367 | None::tl -> None::(aux (i+1) tl)
368 | (Some (_,C.Def (_,Some _)))::_ -> assert false
370 aux 1 canonical_context
373 (fun (subst,metasenv) t ct ->
377 | Some t,Some (_,C.Def (ct,_)) ->
379 CicUnification.fo_unif_subst subst context metasenv t ct
380 with _ -> raise MetasenvInconsistency)
381 | Some t,Some (_,C.Decl ct) ->
382 let inferredty,subst',metasenv' =
383 type_of_aux subst metasenv context t
386 CicUnification.fo_unif_subst
387 subst' context metasenv' inferredty ct
388 with _ -> raise MetasenvInconsistency)
390 raise MetasenvInconsistency
391 ) (subst,metasenv) l lifted_canonical_context
393 and check_exp_named_subst metasubst metasenv context =
394 let rec check_exp_named_subst_aux metasubst metasenv substs =
396 [] -> metasubst,metasenv
397 | ((uri,t) as subst)::tl ->
399 CicSubstitution.subst_vars substs (type_of_variable uri) in
400 (match CicEnvironment.get_cooked_obj ~trust:false uri with
401 Cic.Variable (_,Some bo,_,_) ->
404 "A variable with a body can not be explicit substituted")
405 | Cic.Variable (_,None,_,_) -> ()
406 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
408 let typeoft,metasubst',metasenv' =
409 type_of_aux metasubst metasenv context t
412 let metasubst'',metasenv'' =
413 CicUnification.fo_unif_subst
414 metasubst' context metasenv' typeoft typeofvar
416 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
418 raise (NotRefinable "Wrong Explicit Named Substitution")
420 check_exp_named_subst_aux metasubst metasenv []
422 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
423 let module C = Cic in
424 (* ti could be a metavariable in the domain of the substitution *)
425 let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
426 let t1' = CicMetaSubst.apply_subst subst' t1 in
427 let t2' = CicMetaSubst.apply_subst subst' t2 in
428 let t1'' = CicMetaSubst.whd subst' context t1' in
429 let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in
430 match (t1'', t2'') with
431 (C.Sort s1, C.Sort s2)
432 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
433 C.Sort s2,subst',metasenv'
434 | (C.Sort s1, C.Sort s2) ->
435 (*CSC manca la gestione degli universi!!! *)
436 C.Sort C.Type,subst',metasenv'
437 | (C.Meta _,_) | (_,C.Meta _) ->
438 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
440 CicMkImplicit.identity_relocation_list_for_metavariable context
442 C.Meta (idx, irl), subst, metasenv'
446 ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
452 ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
454 and eat_prods subst metasenv context hetype =
456 [] -> hetype,subst,metasenv
457 | (hete, hety)::tl ->
458 (match (CicMetaSubst.whd subst context hetype) with
460 let subst',metasenv' =
461 CicUnification.fo_unif_subst subst context metasenv s hety
463 CicReduction.fdebug := -1 ;
464 eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
468 ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
469 | _ -> raise (NotRefinable "Appl: wrong Prod-type")
472 let ty,subst',metasenv' =
473 type_of_aux [] metasenv context t
475 let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in
476 (* we get rid of the metavariables that have been instantiated *)
479 (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
482 CicMetaSubst.apply_subst subst'' t,
483 CicMetaSubst.apply_subst subst'' ty,
488 let type_of_aux' metasenv context term =
490 let (t,ty,s,m) = type_of_aux' metasenv context term in
494 debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
497 debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
500 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
503 | CicUnification.AssertFailure msg as e ->
504 debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
507 | CicUnification.UnificationFailure msg as e ->
508 debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
515 debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
518 debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;