-exception Fail of string;;
-
-(*CSC: generatore di nomi? Chiedere il nome? *)
-let fresh_name =
- let next_fresh_index = ref 0
-in
- function () ->
- incr next_fresh_index ;
- "fresh_name" ^ string_of_int !next_fresh_index
-;;
-
-(* lambda_abstract newmeta ty *)
-(* returns a triple [bo],[context],[ty'] where *)
-(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
-(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *)
-(* So, lambda_abstract is the core of the implementation of *)
-(* the Intros tactic. *)
-let lambda_abstract newmeta ty =
- let module C = Cic in
- let rec collect_context =
- function
- C.Cast (te,_) -> collect_context te
- | C.Prod (n,s,t) ->
- let (ctx,ty,bo) = collect_context t in
- let n' =
- match n with
- C.Name _ -> n
-(*CSC: generatore di nomi? Chiedere il nome? *)
- | 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
- bo,(List.rev revcontext),ty'
-;;
-
-let intros () =
- let module C = Cic 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)) -> metano,context,ty
- in
- let newmeta = new_meta () in
- let (bo',newcontext,ty') = lambda_abstract newmeta ty in
- let context'' = newcontext @ 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 context (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.")
-;;
-
-(*CSC: The call to the Intros tactic is embedded inside the code of the *)
-(*CSC: Elim tactic. Do we already need tacticals? *)
-(* Auxiliary function for apply: given a type (a backbone), it returns its *)
-(* head, a META environment in which there is new a META for each hypothesis,*)
-(* a list of arguments for the new applications and the indexes of the first *)
-(* and last new METAs introduced. The nth argument in the list of arguments *)
-(* is the nth new META lambda-abstracted as much as possible. Hence, this *)
-(* functions already provides the behaviour of Intros on the new goals. *)
-let new_metasenv_for_apply_intros 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 newargument,newcontext,ty' = lambda_abstract newmeta s in
- let (res,newmetasenv,arguments,lastmeta) =
- aux (newmeta + 1) (S.subst newargument t)
- in
- res,(newmeta,ty')::newmetasenv,newargument::arguments,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,arguments,lastmeta) = aux newmeta ty in
- res,newmetasenv,arguments,newmeta,lastmeta
-;;
-
-(* Auxiliary function for apply: given a type (a backbone), it returns its *)
-(* head, a META environment in which there is new a META for each hypothesis,*)
-(* a list of arguments for the new applications and the indexes of the first *)
-(* and last new METAs introduced. The nth argument in the list of arguments *)
-(* is just the nth new META. *)
-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 newargument = C.Meta newmeta in
- let (res,newmetasenv,arguments,lastmeta) =
- aux (newmeta + 1) (S.subst newargument t)
- in
- res,(newmeta,s)::newmetasenv,newargument::arguments,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,arguments,lastmeta) = aux newmeta ty in
- res,newmetasenv,arguments,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,arguments,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 arguments in
- Cic.Appl (term::arguments')
- in
- 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 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_intros 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,arguments,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
-(*CSC: Code to be used for Apply *)
- C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
- | C.Meta emeta -> emeta,[]
-(*CSC: Code to be used for ApplyIntros
- C.Appl (he::fargs) ->
- let rec find_head =
- function
- C.Meta emeta -> emeta
- | C.Lambda (_,_,t) -> find_head t
- | C.LetIn (_,_,t) -> find_head t
- | _ ->raise NotTheRightEliminatorShape
- in
- find_head he,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 arguments 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 reduction_tactic reduction_function term =
- let curi,metasenv,pbo,pty =
- match !proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) -> metano,context,ty
- in
- let ciccontext = cic_context_of_named_context context in
- let term' = reduction_function ciccontext term in
- (* We don't know if [term] is a subterm of [ty] or a subterm of *)
- (* the type of one metavariable. So we replace it everywhere. *)
- (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
- (*CSC: che si guadagni nulla in fatto di efficienza. *)
- let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
- let ty' = replace ty in
- let context' =
- List.map
- (function
- Definition (n,t) -> Definition (n,replace t)
- | Declaration (n,t) -> Declaration (n,replace t)
- ) context
- in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context',ty'))
-;;
-
-let reduction_tactic_in_scratch reduction_function ty term =