- | C.Anonimous -> C.Name "fresh_name"
- in
- ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
- | C.LetIn (n,s,t) ->
- let (ctx,ty,bo) = collect_context t in
- ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
- | _ as t -> [], t, (C.Meta newmeta)
- in
- let revcontext',ty',bo' = collect_context ty in
- let context'' = (List.rev revcontext') @ context in
- refine_meta metano bo' [newmeta,ty'] ;
- goal := Some (newmeta,(context'',ty'))
-;;
-
-(* The term bo must be closed in the current context *)
-let exact bo =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let metasenv =
- match !proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) ->
- assert (ty = List.assoc metano metasenv) ;
- (* Invariant: context is the actual context of the meta in the proof *)
- metano,context,ty
- in
- let context = cic_context_of_named_context context in
- if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
- begin
- refine_meta metano bo [] ;
- goal := None
- end
- else
- raise (Fail "The type of the provided term is not the one expected.")
-;;
-
-(* Auxiliary function for apply: given a type (a backbone), it returns its *)
-(* head, a META environment in which there is a META for each hypothesis and *)
-(* the indexes of the first and last new METAs introduced. *)
-let new_metasenv_for_apply ty =
- let module C = Cic in
- let module S = CicSubstitution in
- let rec aux newmeta =
- function
- C.Cast (he,_) -> aux newmeta he
- | C.Prod (_,s,t) ->
- let (res,newmetasenv,lastmeta) =
- aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
- in
- res,(newmeta,s)::newmetasenv,lastmeta
- | t -> t,[],newmeta
- in
- let newmeta = new_meta () in
- (* WARNING: here we are using the invariant that above the most *)
- (* recente new_meta() there are no used metas. *)
- let (res,newmetasenv,lastmeta) = aux newmeta ty in
- res,newmetasenv,newmeta,lastmeta
-;;
-
-(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
-let classify_metas newmeta in_subst_domain apply_subst metasenv =
- List.fold_right
- (fun (i,ty) (old_uninst,new_uninst) ->
- if in_subst_domain i then
- old_uninst,new_uninst
- else
- let ty' = apply_subst ty in
- if i < newmeta then
- ((i,ty')::old_uninst),new_uninst
- else
- old_uninst,((i,ty')::new_uninst)
- ) metasenv ([],[])
-;;
-
-(* The term bo must be closed in the current context *)
-let apply term =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let metasenv =
- match !proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) ->
- assert (ty = List.assoc metano metasenv) ;
- (* Invariant: context is the actual context of the meta in the proof *)
- metano,context,ty
- in
- let ciccontext = cic_context_of_named_context context in
- let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
- (* newmeta is the lowest index of the new metas introduced *)
- let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in
- let newmetasenv = newmetas@metasenv in
- let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
- let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
- let apply_subst = CicUnification.apply_subst subst in
-(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
- let apply_subst_replacing t =
- List.fold_left
- (fun t (i,bo) ->
- ProofEngineReduction.replace
- ~what:(Cic.Meta i) ~with_what:bo ~where:t)
- t subst
- in
- let old_uninstantiatedmetas,new_uninstantiatedmetas =
- classify_metas newmeta in_subst_domain apply_subst newmetasenv
- in
- let bo' =
- if List.length newmetas = 0 then
- term
- else
- let arguments =
- List.map apply_subst
- (List.map (function (i,_) -> C.Meta i) newmetas)
- in
- Cic.Appl (term::arguments)
- in
- refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
- (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
-prerr_endline "QUI4" ; flush stderr ; (
- match new_uninstantiatedmetas with
- [] -> goal := None
- | (i,ty)::_ -> goal := Some (i,(context,ty))
-) ;
-List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas)
-; prerr_endline "FATTO" ; flush stderr ;
-List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ;
-prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b))
-; prerr_endline "FATTO2" ; flush stderr
-;;
-
-let eta_expand metasenv ciccontext t arg =
- let module T = CicTypeChecker in
- let module S = CicSubstitution in
- let module C = Cic in
- let rec aux n =
- function
- t' when t' = S.lift n arg -> C.Rel (1 + n)
- | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
- | C.Var _
- | C.Meta _
- | C.Sort _
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
- | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
- | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
- | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
- | C.Appl l -> C.Appl (List.map (aux n) l)
- | C.Const _ as t -> t
- | C.Abst _ -> assert false
- | C.MutInd _
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
- List.map (aux n) pl)
- | C.Fix (i,fl) ->
- let tylen = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let tylen = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
- fl
- in
- C.CoFix (i, substitutedfl)
- in
- let argty =
- T.type_of_aux' metasenv ciccontext arg
- in
- (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
-;;
-
-exception NotAnInductiveTypeToEliminate;;
-exception NotTheRightEliminatorShape;;
-exception NoHypothesesFound;;
-
-let elim term =
- let module T = CicTypeChecker in
- let module U = UriManager in
- let module R = CicReduction in
- let module C = Cic in
- let curi,metasenv =
- match !proof with
- None -> assert false
- | Some (curi,metasenv,_,_) -> curi,metasenv
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) ->
- assert (ty = List.assoc metano metasenv) ;
- (* Invariant: context is the actual context of the meta in the proof *)
- metano,context,ty
- in
- let ciccontext = cic_context_of_named_context context in
- let termty = T.type_of_aux' metasenv ciccontext term in
- let uri,cookingno,typeno,args =
- match termty with
- C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
- | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
- (uri,cookingno,typeno,args)
- | _ -> raise NotAnInductiveTypeToEliminate
- in
- let eliminator_uri =
- let buri = U.buri_of_uri uri in
- let name =
- match CicEnvironment.get_cooked_obj uri cookingno with
- C.InductiveDefinition (tys,_,_) ->
- let (name,_,_,_) = List.nth tys typeno in
- name
- | _ -> assert false
- in
- let ext =
- match T.type_of_aux' metasenv ciccontext ty with
- C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.Type -> "_rect"
- | _ -> assert false
- in
- U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
- in
- let eliminator_cookingno =
- UriManager.relative_depth curi eliminator_uri 0
- in
- let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
- let ety =
- T.type_of_aux' [] [] eliminator_ref
- in
- let (econclusion,newmetas,newmeta,lastmeta) =
- new_metasenv_for_apply ety
- in
- (* Here we assume that we have only one inductive hypothesis to *)
- (* eliminate and that it is the last hypothesis of the theorem. *)
- (* A better approach would be fingering the hypotheses in some *)
- (* way. *)
- let meta_of_corpse = Cic.Meta (lastmeta - 1) in
- let newmetasenv = newmetas @ metasenv in
-prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
-flush stderr ;
- let subst1 =
- CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
- in
- let ueconclusion = CicUnification.apply_subst subst1 econclusion in
-prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
-flush stderr ;
- (* The conclusion of our elimination principle is *)
- (* (?i farg1 ... fargn) *)
- (* The conclusion of our goal is ty. So, we can *)
- (* eta-expand ty w.r.t. farg1 .... fargn to get *)
- (* a new ty equal to (P farg1 ... fargn). Now *)
- (* ?i can be instantiated with P and we are ready *)
- (* to refine the term. *)
- let emeta, fargs =
- match ueconclusion with
- C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
- | _ -> raise NotTheRightEliminatorShape
- in
- let ty' = CicUnification.apply_subst subst1 ty in
- let eta_expanded_ty =
- List.fold_left (eta_expand metasenv ciccontext) ty' fargs
- in
-prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
- let subst2 =
-(*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
-da subst1!!!! Dovrei rimuoverle o sono innocue?*)
- CicUnification.fo_unif
- newmetasenv ciccontext ueconclusion eta_expanded_ty
- in
-prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
-prerr_endline "unwind"; flush stderr;
- let in_subst_domain i =
- let eq_to_i = function (j,_) -> i=j in
- List.exists eq_to_i subst1 ||
- List.exists eq_to_i subst2
- in
- (* When unwinding the META that corresponds to the elimination *)
- (* predicate (which is emeta), we must also perform one-step *)
- (* beta-reduction. *)
- let apply_subst t =
- let t' = CicUnification.apply_subst subst1 t in
- CicUnification.apply_subst_reducing
- subst2 (Some (emeta,List.length fargs)) t'
- in
-(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
- let apply_subst_replacing t =
- let t' =
- List.fold_left
- (fun t (i,bo) ->
- ProofEngineReduction.replace
- ~what:(Cic.Meta i) ~with_what:bo ~where:t)
- t subst1
- in
- List.fold_left
- (fun t (i,bo) ->
- ProofEngineReduction.replace
- ~what:(Cic.Meta i) ~with_what:bo ~where:t)
- t' subst2
- in
- let newmetasenv' =
- List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
- in
- let old_uninstantiatedmetas,new_uninstantiatedmetas =
- classify_metas newmeta in_subst_domain apply_subst newmetasenv
- in
- let arguments =
- List.map apply_subst
- (List.map (function (i,_) -> C.Meta i) newmetas)
- in
- let bo' = Cic.Appl (eliminator_ref::arguments) in
-prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
-List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
- refine_meta_with_brand_new_metasenv metano bo'
- apply_subst_replacing
- (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
- match new_uninstantiatedmetas with
- [] -> goal := None
- | (i,ty)::_ -> goal := Some (i,(context,ty))
-;;
-
-let elim_intros term =
- elim term ;
- intros ()
-;;