X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;fp=helm%2FgTopLevel%2FproofEngine.ml;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=f33c69e35918cd64ef4a3b2527230a2490ab6609;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml deleted file mode 100644 index f33c69e35..000000000 --- a/helm/gTopLevel/proofEngine.ml +++ /dev/null @@ -1,1017 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -let proof = - ref (None : (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option) -;; -let goal = ref (None : int option);; - -(*CSC: commento vecchio *) -(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *) -(* This (heavy) function must be called when a tactic can instantiate old *) -(* metavariables (i.e. existential variables). It substitues the metasenv *) -(* of the proof with the result of removing [meta] from the domain of *) -(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *) -(* in the current proof. Finally it applies [apply_subst_replacing] to *) -(* current proof. *) -(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *) -(*CSC: ci ripasso sopra apply_subst!!! *) -(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *) -(*CSC: [newmetasenv]. *) -let subst_meta_and_metasenv_in_current_proof meta subst_in newmetasenv = - let (uri,bo,ty) = - match !proof with - None -> assert false - | Some (uri,_,bo,ty) -> uri,bo,ty - in - let bo' = subst_in bo in - let metasenv' = - List.fold_right - (fun metasenv_entry i -> - match metasenv_entry with - (m,canonical_context,ty) when m <> meta -> - let canonical_context' = - List.map - (function - None -> None - | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) - | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) - ) canonical_context - in - (m,canonical_context',subst_in ty)::i - | _ -> i - ) newmetasenv [] - in - proof := Some (uri,metasenv',bo',ty) ; - metasenv' -;; - -let subst_meta_in_current_proof meta term newmetasenv = - let (uri,metasenv,bo,ty) = - match !proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in - let subst_in = CicUnification.apply_subst [meta,term] in - let metasenv' = - newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) - in - let metasenv'' = - List.map - (function i,canonical_context,ty -> - let canonical_context' = - List.map - (function - Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) - | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s)) - | None -> None - ) canonical_context - in - i,canonical_context',(subst_in ty) - ) metasenv' - in - let bo' = subst_in bo in - proof := Some (uri,metasenv'',bo',ty) ; - metasenv'' -;; - -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -let new_meta () = - let metasenv = - match !proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let rec aux = - function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) - in - 1 + aux (None,metasenv) -;; - -(* metas_in_term term *) -(* Returns the ordered list of the metas that occur in [term]. *) -(* Duplicates are removed. The implementation is not very efficient. *) -let metas_in_term term = - let module C = Cic in - let rec aux = - function - C.Rel _ - | C.Var _ -> [] - | C.Meta (n,_) -> [n] - | C.Sort _ - | C.Implicit -> [] - | C.Cast (te,ty) -> (aux te) @ (aux ty) - | C.Prod (_,s,t) -> (aux s) @ (aux t) - | C.Lambda (_,s,t) -> (aux s) @ (aux t) - | C.LetIn (_,s,t) -> (aux s) @ (aux t) - | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l - | C.Const _ - | C.Abst _ - | C.MutInd _ - | C.MutConstruct _ -> [] - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - (aux outt) @ (aux t) @ - (List.fold_left (fun i t -> i @ (aux t)) [] pl) - | C.Fix (i,fl) -> - List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl - | C.CoFix (i,fl) -> - List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl - in - let metas = aux term in - let rec elim_duplicates = - function - [] -> [] - | he::tl -> - he::(elim_duplicates (List.filter (function el -> he <> el) tl)) - in - elim_duplicates metas -;; - -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list [1 ; ... ; n] *) -(* where n = List.length [canonical_context] *) -(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) -let identity_relocation_list_for_metavariable canonical_context = - let canonical_context_length = List.length canonical_context in - let rec aux = - function - (_,[]) -> [] - | (n,None::tl) -> None::(aux ((n+1),tl)) - | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) - in - aux (1,canonical_context) -;; - -(* perforate context term ty *) -(* replaces the term [term] in the proof with a new metavariable whose type *) -(* is [ty]. [context] must be the context of [term] in the whole proof. This *) -(* could be easily computed; so the only reasons to have it as an argument *) -(* are efficiency reasons. *) -let perforate context term ty = - let module C = Cic in - let newmeta = new_meta () in - match !proof with - None -> assert false - | Some (uri,metasenv,bo,gty) -> - (* We push the new meta at the end of the list for pretty-printing *) - (* purposes: in this way metas are ordered. *) - let metasenv' = metasenv@[newmeta,context,ty] in - let irl = identity_relocation_list_for_metavariable context in -(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*) - let bo' = - ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo - in - (* It may be possible that some metavariables occurred only in *) - (* the term we are perforating and they now occurs no more. We *) - (* get rid of them, collecting the really useful metavariables *) - (* in metasenv''. *) -(*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *) -(*CSC: di una metavariabile che compare in bo'!!!!!!! *) - let newmetas = metas_in_term bo' in - let metasenv'' = - List.filter (function (n,_,_) -> List.mem n newmetas) metasenv' - in - proof := Some (uri,metasenv'',bo',gty) ; - goal := Some newmeta -;; - -(************************************************************) -(* Some easy tactics. *) -(************************************************************) - -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 context newmeta ty = - let module C = Cic in - let rec collect_context context = - function - C.Cast (te,_) -> collect_context context te - | C.Prod (n,s,t) -> - let n' = - match n with - C.Name _ -> n -(*CSC: generatore di nomi? Chiedere il nome? *) - | C.Anonimous -> C.Name (fresh_name ()) - in - let (context',ty,bo) = - collect_context ((Some (n',(C.Decl s)))::context) t - in - (context',ty,C.Lambda(n',s,bo)) - | C.LetIn (n,s,t) -> - let (context',ty,bo) = - collect_context ((Some (n,(C.Def s)))::context) t - in - (context',ty,C.LetIn(n,s,bo)) - | _ as t -> - let irl = identity_relocation_list_for_metavariable context in - context, t, (C.Meta (newmeta,irl)) - in - collect_context context 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - let newmeta = new_meta () in - let (context',ty',bo') = lambda_abstract context newmeta ty in - let _ = subst_meta_in_current_proof metano bo' [newmeta,context',ty'] in - goal := Some newmeta -;; - -(* 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then - begin - let metasenv' = subst_meta_in_current_proof metano bo [] in - goal := - match metasenv' with - [] -> None - | (n,_,_)::_ -> Some n - 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 context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta = - function - C.Cast (he,_) -> aux newmeta he - | C.Prod (name,s,t) -> - let newcontext,ty',newargument = lambda_abstract context newmeta s in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - res,(newmeta,newcontext,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 context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta = - function - C.Cast (he,_) -> aux newmeta he - | C.Prod (name,s,t) -> - let irl = identity_relocation_list_for_metavariable context in - let newargument = C.Meta (newmeta,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - res,(newmeta,context,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 subst_in metasenv = - List.fold_right - (fun (i,canonical_context,ty) (old_uninst,new_uninst) -> - if in_subst_domain i then - old_uninst,new_uninst - else - let ty' = subst_in canonical_context ty in - let canonical_context' = - List.fold_right - (fun entry canonical_context' -> - let entry' = - match entry with - Some (n,Cic.Decl s) -> - Some (n,Cic.Decl (subst_in canonical_context' s)) - | Some (n,Cic.Def s) -> - Some (n,Cic.Def (subst_in canonical_context' s)) - | None -> None - in - entry'::canonical_context' - ) canonical_context [] - in - if i < newmeta then - ((i,canonical_context',ty')::old_uninst),new_uninst - else - old_uninst,((i,canonical_context',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 -> - List.find (function (m,_,_) -> m=metano) metasenv - in - let termty = CicTypeChecker.type_of_aux' metasenv context term in - (* newmeta is the lowest index of the new metas introduced *) - let (consthead,newmetas,arguments,newmeta,_) = - new_metasenv_for_apply context termty - in - let newmetasenv = newmetas@metasenv in - let subst,newmetasenv' = - CicUnification.fo_unif newmetasenv context consthead ty - in - let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in - let apply_subst = CicUnification.apply_subst subst in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - (* subst_in doesn't need the context. Hence the underscore. *) - let subst_in _ = CicUnification.apply_subst subst in - classify_metas newmeta in_subst_domain subst_in 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 - let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in - let newmetasenv''' = - let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in - subst_meta_and_metasenv_in_current_proof metano subst_in - newmetasenv'' - in - match newmetasenv''' with - [] -> goal := None - | (i,_,_)::_ -> goal := Some i -;; - -let eta_expand metasenv context 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 context arg - in - (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) -;; - -exception NotAnInductiveTypeToEliminate;; -exception NotTheRightEliminatorShape;; -exception NoHypothesesFound;; - -let elim_intros_simpl 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 -> - List.find (function (m,_,_) -> m=metano) metasenv - in - let termty = T.type_of_aux' metasenv context 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 context 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 context ety -*) - new_metasenv_for_apply_intros context 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 = - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas - in - let irl = - identity_relocation_list_for_metavariable canonical_context - in - Cic.Meta (lastmeta - 1, irl) - in - let newmetasenv = newmetas @ metasenv in - let subst1,newmetasenv' = - CicUnification.fo_unif newmetasenv context term meta_of_corpse - in - let ueconclusion = CicUnification.apply_subst subst1 econclusion in - (* 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 = -(*CSC: newmetasenv' era metasenv ??????????? *) - List.fold_left (eta_expand newmetasenv' context) ty' fargs - in - let subst2,newmetasenv'' = -(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite -da subst1!!!! Dovrei rimuoverle o sono innocue?*) - CicUnification.fo_unif - newmetasenv' context ueconclusion eta_expanded_ty - in - 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 -(*CSC: codice per l'elim - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. apply_subst doesn't need the context. Hence *) - (* the underscore. *) - 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: codice per l'elim_intros_simpl. Non effettua semplificazione. *) - let apply_subst context t = - let t' = CicUnification.apply_subst (subst1@subst2) t in - ProofEngineReduction.simpl context t' - in -(* *) - let old_uninstantiatedmetas,new_uninstantiatedmetas = - classify_metas newmeta in_subst_domain apply_subst - newmetasenv'' - in - let arguments' = List.map (apply_subst context) arguments in - let bo' = Cic.Appl (eliminator_ref::arguments') in - let newmetasenv''' = - new_uninstantiatedmetas@old_uninstantiatedmetas - in - let newmetasenv'''' = - (* When unwinding the META that corresponds to the *) - (* elimination predicate (which is emeta), we must *) - (* also perform one-step beta-reduction. *) - (* The only difference w.r.t. apply_subst is that *) - (* we also substitute metano with bo'. *) - (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) - (*CSC: no? *) -(*CSC: codice per l'elim - let apply_subst' t = - let t' = CicUnification.apply_subst subst1 t in - CicUnification.apply_subst_reducing - ((metano,bo')::subst2) - (Some (emeta,List.length fargs)) t' - in -*) -(*CSC: codice per l'elim_intros_simpl *) - let apply_subst' t = - CicUnification.apply_subst - ((metano,bo')::(subst1@subst2)) t - in -(* *) - subst_meta_and_metasenv_in_current_proof metano - apply_subst' newmetasenv''' - in - match newmetasenv'''' with - [] -> goal := None - | (i,_,_)::_ -> goal := Some i -;; - -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 -> List.find (function (m,_,_) -> m=metano) metasenv - 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: Il vero problema e' che non sapendo dove sia il term non *) - (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) - (*CSC: e' meglio prima cercare il termine e scoprirne il *) - (*CSC: contesto, poi ridurre e infine rimpiazzare. *) - let replace context where= -(*CSC: Per il momento se la riduzione fallisce significa solamente che *) -(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) -(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) - try - let term' = reduction_function context term in - ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' - ~where:where - with - _ -> where - in - let ty' = replace context ty in - let context' = - List.fold_right - (fun entry context -> - match entry with - Some (name,Cic.Def t) -> - (Some (name,Cic.Def (replace context t)))::context - | Some (name,Cic.Decl t) -> - (Some (name,Cic.Decl (replace context t)))::context - | None -> None::context - ) context [] - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some metano -;; - -(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) -let reduction_tactic_in_scratch reduction_function term ty = - let metasenv = - match !proof with - None -> [] - | Some (_,metasenv,_,_) -> metasenv - in - let metano,context,_ = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - let term' = reduction_function context term in - ProofEngineReduction.replace - ~equality:(==) ~what:term ~with_what:term' ~where:ty -;; - -let whd = reduction_tactic CicReduction.whd;; -let reduce = reduction_tactic ProofEngineReduction.reduce;; -let simpl = reduction_tactic ProofEngineReduction.simpl;; - -let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;; -let reduce_in_scratch = - reduction_tactic_in_scratch ProofEngineReduction.reduce;; -let simpl_in_scratch = - reduction_tactic_in_scratch ProofEngineReduction.simpl;; - -(* It is just the opposite of whd. The code should probably be merged. *) -let fold 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - let term' = CicReduction.whd context 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 - ~equality:(ProofEngineReduction.syntactic_equality) - ~what:term' ~with_what:term - in - let ty' = replace ty in - let context' = - List.map - (function - Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) - | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t)) - | None -> None - ) context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some metano -;; - -let cut term = - let module C = Cic in - 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - let newmeta1 = new_meta () in - let newmeta2 = newmeta1 + 1 in - let context_for_newmeta1 = - (Some (C.Name "dummy_for_cut",C.Decl term))::context in - let irl1 = - identity_relocation_list_for_metavariable context_for_newmeta1 in - let irl2 = identity_relocation_list_for_metavariable context in - let newmeta1ty = CicSubstitution.lift 1 ty in - let bo' = - C.Appl - [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; - C.Meta (newmeta2,irl2)] - in - let _ = - subst_meta_in_current_proof metano bo' - [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; - in - goal := Some newmeta1 -;; - -let letin term = - let module C = Cic in - 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - let _ = CicTypeChecker.type_of_aux' metasenv context term in - let newmeta = new_meta () in - let context_for_newmeta = - (Some (C.Name "dummy_for_letin",C.Def term))::context in - let irl = - identity_relocation_list_for_metavariable context_for_newmeta in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in - let _ = subst_meta_in_current_proof metano bo' [newmeta,context_for_newmeta,newmetaty] in - goal := Some newmeta -;; - -exception NotConvertible;; - -(*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *) -(*CSC: while [goal_input] can have a richer context (because of binders) *) -(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *) -(*CSC: Is that evident? Is that right? Or should it be changed? *) -let change ~goal_input ~input = - 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - (* are_convertible works only on well-typed terms *) - ignore (CicTypeChecker.type_of_aux' metasenv context input) ; - if CicReduction.are_convertible context goal_input input then - begin - let replace = - ProofEngineReduction.replace - ~equality:(==) ~what:goal_input ~with_what:input - in - let ty' = replace ty in - let context' = - List.map - (function - Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t)) - | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) - | None -> None - ) context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some metano - end - else - raise NotConvertible -;; - -let clearbody = - let module C = Cic in - function - None -> assert false - | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") - | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body -> - let curi,metasenv,pbo,pty = - match !proof with - None -> assert false - | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty - in - let metano,_,_ = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonimous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear_body -> - let cleared_entry = - let ty = - CicTypeChecker.type_of_aux' metasenv context term - in - Some (n_to_clear_body, Cic.Decl ty) - in - cleared_entry::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def t) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("The correctness of hypothesis " ^ - string_of_name n ^ - " relies on the body of " ^ - string_of_name n_to_clear_body) - ) - in - entry::context - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("The correctness of the goal relies on the body of " ^ - string_of_name n_to_clear_body)) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) -;; - -let clear hyp_to_clear = - let module C = Cic in - match hyp_to_clear with - None -> assert false - | Some (n_to_clear, _) -> - 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 -> List.find (function (m,_,_) -> m=metano) metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonimous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear -> None::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def t) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("Hypothesis " ^ - string_of_name n ^ - " uses hypothesis " ^ - string_of_name n_to_clear) - ) - in - entry::context - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("Hypothesis " ^ string_of_name n_to_clear ^ - " occurs in the goal")) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) -;;