6 type metasenv = (int * Cic.term) list;;
8 type context = (binder_type * Cic.name * Cic.term) list;;
10 type sequent = context * Cic.term;;
13 ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
15 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
16 (* Note: the sequent is redundant: it can be computed from the type of the *)
17 (* metavariable and its context in the proof. We keep it just for efficiency *)
18 (* because computing the context of a term may be quite expensive. *)
19 let goal = ref (None : (int * sequent) option);;
21 exception NotImplemented
23 (*CSC: Funzione che deve sparire!!! *)
24 let cic_context_of_context =
28 | Definition,_,_ -> raise NotImplemented
32 let refine_meta meta term newmetasenv =
33 let (uri,metasenv,bo,ty) =
36 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
38 let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
44 | C.Meta meta' when meta=meta' -> term
47 | C.Implicit as t -> t
48 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
49 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
50 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
51 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
52 | C.Appl l -> C.Appl (List.map aux l)
55 | C.MutInd _ as t -> t
56 | C.MutConstruct _ as t -> t
57 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
58 C.MutCase (sp,cookingsno,i,aux outt, aux t,
63 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
66 C.Fix (i, substitutedfl)
70 (fun (name,ty,bo) -> (name, aux ty, aux bo))
73 C.CoFix (i, substitutedfl)
75 let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in
77 proof := Some (uri,metasenv'',bo',ty)
80 (* Returns the first meta whose number is above the number of the higher meta. *)
85 | Some (_,metasenv,_,_) -> metasenv
91 | None,(n,_)::tl -> aux (Some n,tl)
92 | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
94 1 + aux (None,metasenv)
97 (* metas_in_term term *)
98 (* Returns the ordered list of the metas that occur in [term]. *)
99 (* Duplicates are removed. The implementation is not very efficient. *)
100 let metas_in_term term =
101 let module C = Cic in
109 | C.Cast (te,ty) -> (aux te) @ (aux ty)
110 | C.Prod (_,s,t) -> (aux s) @ (aux t)
111 | C.Lambda (_,s,t) -> (aux s) @ (aux t)
112 | C.LetIn (_,s,t) -> (aux s) @ (aux t)
113 | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
117 | C.MutConstruct _ -> []
118 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
119 (aux outt) @ (aux t) @
120 (List.fold_left (fun i t -> i @ (aux t)) [] pl)
122 List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
124 List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
126 let metas = aux term in
127 let rec elim_duplicates =
131 he::(elim_duplicates (List.filter (function el -> he <> el) tl))
133 elim_duplicates metas
136 (* perforate context term ty *)
137 (* replaces the term [term] in the proof with a new metavariable whose type *)
138 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
139 (* could be easily computed; so the only reasons to have it as an argument *)
140 (* are efficiency reasons. *)
141 let perforate context term ty =
142 let module C = Cic in
143 let newmeta = new_meta () in
146 | Some (uri,metasenv,bo,gty) ->
147 (* We push the new meta at the end of the list for pretty-printing *)
148 (* purposes: in this way metas are ordered. *)
149 let metasenv' = metasenv@[newmeta,ty] in
150 let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
151 (* It may be possible that some metavariables occurred only in *)
152 (* the term we are perforating and they now occurs no more. We *)
153 (* get rid of them, collecting the really useful metavariables *)
155 let newmetas = metas_in_term bo' in
157 List.filter (function (n,_) -> List.mem n newmetas) metasenv'
159 proof := Some (uri,metasenv'',bo',gty) ;
160 goal := Some (newmeta,(context,ty)) ;
164 (************************************************************)
165 (* Some easy tactics. *)
166 (************************************************************)
168 exception Fail of string;;
171 let module C = Cic in
172 let module R = CicReduction in
176 | Some (_,metasenv,_,_) -> metasenv
178 let (metano,context,ty) =
181 | Some (metano,(context,ty)) -> metano,context,ty
183 let newmeta = new_meta () in
184 let rec collect_context =
186 C.Cast (te,_) -> collect_context te
188 let (ctx,ty,bo) = collect_context t in
192 (*CSC: generatore di nomi? Chiedere il nome? *)
193 | C.Anonimous -> C.Name "fresh_name"
195 ((Declaration,n',s)::ctx,ty,C.Lambda(n',s,bo))
197 let (ctx,ty,bo) = collect_context t in
198 ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo))
199 | _ as t -> [], t, (C.Meta newmeta)
201 let revcontext',ty',bo' = collect_context ty in
202 let context'' = (List.rev revcontext') @ context in
203 refine_meta metano bo' [newmeta,ty'] ;
204 goal := Some (newmeta,(context'',ty'))
207 (* The term bo must be closed in the current context *)
209 let module T = CicTypeChecker in
210 let module R = CicReduction in
214 | Some (_,metasenv,_,_) -> metasenv
216 let (metano,context,ty) =
219 | Some (metano,(context,ty)) ->
220 assert (ty = List.assoc metano metasenv) ;
221 (* Invariant: context is the actual context of the meta in the proof *)
224 (*CSC: deve sparire! *)
225 let context = cic_context_of_context context in
226 if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
228 refine_meta metano bo [] ;
232 raise (Fail "The type of the provided term is not the one expected.")
235 let fix_andreas_meta mgu mgut =
236 let mgul = Array.to_list mgu in
237 let mgutl = Array.to_list mgut in
238 let applymetas_to_metas =
239 let newmeta = new_meta () in
240 (* WARNING: here we are using the invariant that above the most *)
241 (* recente new_meta() there are no used metas. *)
242 Array.init (List.length mgul) (function i -> newmeta + i) in
243 (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
244 (* Here we assume that either a META has been instantiated with *)
245 (* a close term or with itself. *)
246 let uninstantiatedmetas =
248 (fun bo ty newmetas ->
249 let module C = Cic in
252 let newmeta = applymetas_to_metas.(i) in
253 (*CSC: se ty contiene metas, queste hanno il numero errato!!! *)
254 let ty_with_newmetas =
255 (* Substitues (META n) with (META (applymetas_to_metas.(n))) *)
260 | C.Meta n -> C.Meta (applymetas_to_metas.(n))
262 | C.Implicit as t -> t
263 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
264 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
265 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
266 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
267 | C.Appl l -> C.Appl (List.map aux l)
268 | C.Const _ as t -> t
269 | C.Abst _ -> assert false
271 | C.MutConstruct _ as t -> t
272 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
273 C.MutCase (sp,cookingsno,i,aux outt, aux t,
278 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
281 C.Fix (i, substitutedfl)
285 (fun (name,ty,bo) -> (name, aux ty, aux bo))
288 C.CoFix (i, substitutedfl)
292 (newmeta,ty_with_newmetas)::newmetas
299 Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i))
303 mgul',uninstantiatedmetas
306 (* The term bo must be closed in the current context *)
308 let module T = CicTypeChecker in
309 let module R = CicReduction in
310 let module C = Cic in
314 | Some (_,metasenv,_,_) -> metasenv
316 let (metano,context,ty) =
319 | Some (metano,(context,ty)) ->
320 assert (ty = List.assoc metano metasenv) ;
321 (* Invariant: context is the actual context of the meta in the proof *)
324 (*CSC: deve sparire! *)
325 let ciccontext = cic_context_of_context context in
326 let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
327 let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in
329 if List.length mgul' = 0 then
332 Cic.Appl (term::mgul')
334 refine_meta metano bo' uninstantiatedmetas ;
335 match uninstantiatedmetas with
336 (n,ty)::tl -> goal := Some (n,(context,ty))
341 let eta_expand metasenv ciccontext t arg =
342 let module T = CicTypeChecker in
343 let module S = CicSubstitution in
344 let module C = Cic in
347 t' when t' = S.lift n arg -> C.Rel (1 + n)
348 | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
352 | C.Implicit as t -> t
353 | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
354 | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
355 | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
356 | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
357 | C.Appl l -> C.Appl (List.map (aux n) l)
358 | C.Const _ as t -> t
359 | C.Abst _ -> assert false
361 | C.MutConstruct _ as t -> t
362 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
363 C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
366 let tylen = List.length fl in
369 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
372 C.Fix (i, substitutedfl)
374 let tylen = List.length fl in
377 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
380 C.CoFix (i, substitutedfl)
383 T.type_of_aux' metasenv ciccontext arg
385 (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
388 exception NotAnInductiveTypeToEliminate;;
389 exception NotTheRightEliminatorShape;;
390 exception NoHypothesesFound;;
393 let module T = CicTypeChecker in
394 let module U = UriManager in
395 let module R = CicReduction in
396 let module C = Cic in
400 | Some (curi,metasenv,_,_) -> curi,metasenv
402 let (metano,context,ty) =
405 | Some (metano,(context,ty)) ->
406 assert (ty = List.assoc metano metasenv) ;
407 (* Invariant: context is the actual context of the meta in the proof *)
410 (*CSC: deve sparire! *)
411 let ciccontext = cic_context_of_context context in
412 let termty = T.type_of_aux' metasenv ciccontext term in
413 let uri,cookingno,typeno,args =
415 C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
416 | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
417 (uri,cookingno,typeno,args)
418 | _ -> raise NotAnInductiveTypeToEliminate
421 let buri = U.buri_of_uri uri in
423 match CicEnvironment.get_cooked_obj uri cookingno with
424 C.InductiveDefinition (tys,_,_) ->
425 let (name,_,_,_) = List.nth tys typeno in
430 match T.type_of_aux' metasenv ciccontext ty with
431 C.Sort C.Prop -> "_ind"
432 | C.Sort C.Set -> "_rec"
433 | C.Sort C.Type -> "_rect"
436 U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
438 let eliminator_cookingno =
439 UriManager.relative_depth curi eliminator_uri 0
441 let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
443 T.type_of_aux' [] [] eliminator_ref
446 let earity = CicUnification.get_arity ety in
447 let mgu = Array.init earity (fun i -> (C.Meta i)) in
448 let mgut = Array.make earity C.Implicit in
449 (* Here we assume that we have only one inductive hypothesis to *)
450 (* eliminate and that it is the last hypothesis of the theorem. *)
451 (* A better approach would be fingering the hypotheses in some *)
453 let hypothesis_to_eliminate,econclusion =
455 (* traverses the backbone [t] looking for the last hypothesis *)
456 (* and substituting Pi-abstractions with META declarations. *)
457 (* [h] is the last hypothesis met up to now. [n] is the next *)
463 aux (n+1) (Some s) (CicSubstitution.subst (C.Meta n) t)
464 | C.Cast (te,_) -> aux n h te
466 None -> raise NoHypothesesFound
471 prerr_endline ("HTOELIM: " ^ CicPp.ppterm hypothesis_to_eliminate) ;
472 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
474 ignore (CicUnification.fo_unif_mgu 0 hypothesis_to_eliminate termty mgu) ;
475 ignore (CicUnification.fo_unif_mgu 0 term (C.Meta (earity - 1)) mgu) ;
476 let mgu = CicUnification.unwind mgu in
477 prerr_endline "Dopo l'unwind dell'mgu"; flush stderr ;
478 let mark = Array.make earity 1 in
480 CicUnification.unwind_meta mgu mark econclusion
482 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
484 (* The conclusion of our elimination principle is *)
485 (* (?i farg1 ... fargn) *)
486 (* The conclusion of our goal is ty. So, we can *)
487 (* eta-expand ty w.r.t. farg1 .... fargn to get *)
488 (* a new ty equal to (P farg1 ... fargn). Now *)
489 (* ?i can be instantiated with P and we are ready *)
490 (* to refine the term. *)
492 match ueconclusion with
493 C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
494 | _ -> raise NotTheRightEliminatorShape
496 let eta_expanded_ty =
497 (*CSC: metasenv e ?????????????*)
498 List.fold_left (eta_expand metasenv ciccontext) ty fargs
501 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
502 ignore (CicUnification.fo_unif_mgu 0 ueconclusion eta_expanded_ty mgu) ;
503 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
504 let mgu = CicUnification.unwind mgu in
505 print_endline "unwind"; flush stdout;
506 (* When unwinding the META that corresponds to the elimination *)
507 (* predicate (which is emeta), we must also perform one-step *)
508 (* beta-reduction. *)
510 let mark = Array.make (Array.length mgu) 1 in
512 (CicUnification.unwind_meta_reducing mgu mark (Some emeta))
515 print_endline "unwind_array"; flush stdout;
516 let mgu' = Array.copy mgu in
517 let mgut' = CicUnification.list_of_array mgut in
518 print_endline "list"; flush stdout;
521 prerr_endline ("META " ^ string_of_int i ^ ": " ^ CicPp.ppterm mgu'.(i) ^
522 " == " ^ CicPp.ppterm ty) ; flush stderr ;
524 CicTypeChecker.type_of_aux' mgut' ciccontext mgu'.(i)
526 ignore (CicUnification.fo_unif_mgu 0 ty ty' mgu)
528 let mgu = CicUnification.unwind mgu in
529 let mgut = CicUnification.unwind_array mgu mgut in
530 prerr_endline "Dopo le unwind dell'mgut" ; flush stdout ;
531 let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in
532 prerr_endline "Dopo il fissaggio" ; flush stdout ;
533 let bo' = Cic.Appl (eliminator_ref::mgul') in
534 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
535 refine_meta metano bo' uninstantiatedmetas ;
536 prerr_endline "dopo refine meta" ; flush stdout ;
537 match uninstantiatedmetas with
538 (n,ty)::tl -> goal := Some (n,(context,ty))
542 let reduction_tactic reduction_function term =
543 let curi,metasenv,pbo,pty =
546 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
548 let (metano,context,ty) =
551 | Some (metano,(context,ty)) -> metano,context,ty
553 let term' = reduction_function term in
554 let ty' = ProofEngineReduction.replace term term' ty in
558 (n,_) when n = metano -> (metano,ty')
562 proof := Some (curi,metasenv',pbo,pty) ;
563 goal := Some (metano,(context,ty'))
566 let whd = reduction_tactic CicReduction.whd;;
567 let reduce = reduction_tactic ProofEngineReduction.reduce;;
569 let simpl = reduction_tactic ProofEngineReduction.simpl;;
573 let curi,metasenv,pbo,pty =
576 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
578 let (metano,context,ty) =
581 | Some (metano,(context,ty)) -> metano,context,ty
583 let term' = ProofEngineReduction.simpl term in
584 let ty' = ProofEngineReduction.replace term term' ty in
588 (n,_) when n = metano -> (metano,ty')
592 proof := Some (curi,metasenv',pbo,pty) ;
593 goal := Some (metano,(context,ty'))
596 (* It is just the opposite of whd. The code should probably be merged. *)
598 let curi,metasenv,pbo,pty =
601 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
603 let (metano,context,ty) =
606 | Some (metano,(context,ty)) -> metano,context,ty
608 let term' = CicReduction.whd term in
609 let ty' = ProofEngineReduction.replace term' term ty in
613 (n,_) when n = metano -> (metano,ty')
617 proof := Some (curi,metasenv',pbo,pty) ;
618 goal := Some (metano,(context,ty'))
622 let module C = Cic in
623 let curi,metasenv,pbo,pty =
626 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
628 let (metano,context,ty) =
631 | Some (metano,(context,ty)) -> metano,context,ty
633 let newmeta1 = new_meta () in
634 let newmeta2 = newmeta1 + 1 in
635 let newmeta1ty = CicSubstitution.lift 1 ty in
638 [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
641 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
642 refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
645 (newmeta1,((Declaration, C.Name "dummy_for_cut", term)::context,
649 exception NotConvertible;;
651 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
652 (*CSC: while [goal_input] can have a richer context (because of binders) *)
653 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
654 (*CSC: Is that evident? Is that right? Or should it be changed? *)
655 let change ~goal_input ~input =
656 let curi,metasenv,pbo,pty =
659 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
661 let (metano,context,ty) =
664 | Some (metano,(context,ty)) -> metano,context,ty
666 (*CSC: deve sparire! *)
667 let ciccontext = cic_context_of_context context in
668 (* are_convertible works only on well-typed terms *)
669 ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
670 if CicReduction.are_convertible goal_input input then
672 let ty' = ProofEngineReduction.replace goal_input input ty in
676 (n,_) when n = metano -> (metano,ty')
680 proof := Some (curi,metasenv',pbo,pty) ;
681 goal := Some (metano,(context,ty'))