X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=c605d41a97d2848eca8fd05c4575d8e8aa46d184;hb=b855d2cee134386df462125b5a395f0063c7a93e;hp=8f5d0c96e9ef749811d7370a33fc3be52984811c;hpb=c7d2d6da56d97250ee7ab619ee8c310d91fa912d;p=helm.git diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 8f5d0c96e..c605d41a9 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -1,83 +1,104 @@ -type binder_type = - Declaration - | Definition -;; - -type metasenv = (int * Cic.term) list;; - -type context = (binder_type * Cic.name * Cic.term) list;; - -type sequent = context * Cic.term;; +(* 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 * metasenv * Cic.term * Cic.term) option) + ref (None : (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option) ;; -(*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *) -(* Note: the sequent is redundant: it can be computed from the type of the *) -(* metavariable and its context in the proof. We keep it just for efficiency *) -(* because computing the context of a term may be quite expensive. *) -let goal = ref (None : (int * sequent) option);; - -exception NotImplemented - -(*CSC: Funzione che deve sparire!!! *) -let cic_context_of_context = - List.map - (function - Declaration,_,t -> t - | Definition,_,_ -> raise NotImplemented - ) +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 refine_meta meta term newmetasenv = +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 metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in - let rec aux = - let module C = Cic in - function - C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta meta' when meta=meta' -> term - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) - | C.Appl l -> C.Appl (List.map aux l) - | C.Const _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,aux outt, aux t, - List.map aux pl) - | C.Fix (i,fl) -> - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let substitutedfl = + 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 - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl + (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 - C.CoFix (i, substitutedfl) - in - let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in - let bo' = aux bo in - proof := Some (uri,metasenv'',bo',ty) + 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. *) +(* Returns the first meta whose number is above the *) +(* number of the higher meta. *) let new_meta () = let metasenv = match !proof with @@ -88,8 +109,8 @@ let new_meta () = 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) + | 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) ;; @@ -103,7 +124,7 @@ let metas_in_term term = function C.Rel _ | C.Var _ -> [] - | C.Meta n -> [n] + | C.Meta (n,_) -> [n] | C.Sort _ | C.Implicit -> [] | C.Cast (te,ty) -> (aux te) @ (aux ty) @@ -112,7 +133,6 @@ let metas_in_term term = | 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) -> @@ -133,6 +153,21 @@ let metas_in_term term = 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 *) @@ -146,19 +181,24 @@ let perforate context term ty = | 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,ty] in - let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in + 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' + List.filter (function (n,_,_) -> List.mem n newmetas) metasenv' in proof := Some (uri,metasenv'',bo',gty) ; - goal := Some (newmeta,(context,ty)) ; - newmeta + goal := Some newmeta ;; (************************************************************) @@ -167,6 +207,49 @@ let perforate context term ty = 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 @@ -175,33 +258,15 @@ let intros () = None -> assert false | Some (_,metasenv,_,_) -> metasenv in - let (metano,context,ty) = + let metano,context,ty = match !goal with None -> assert false - | Some (metano,(context,ty)) -> metano,context,ty + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in let newmeta = new_meta () 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 - let context'' = (List.rev revcontext') @ context in - refine_meta metano bo' [newmeta,ty'] ; - goal := Some (newmeta,(context'',ty')) + 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 *) @@ -213,94 +278,107 @@ let exact bo = None -> assert false | Some (_,metasenv,_,_) -> metasenv in - let (metano,context,ty) = + 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 + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - (*CSC: deve sparire! *) - let context = cic_context_of_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.") + 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.") ;; -let fix_andreas_meta mgu mgut = - let mgul = Array.to_list mgu in - let mgutl = Array.to_list mgut in - let applymetas_to_metas = - let newmeta = new_meta () in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - Array.init (List.length mgul) (function i -> newmeta + i) in - (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) - (* Here we assume that either a META has been instantiated with *) - (* a close term or with itself. *) - let uninstantiatedmetas = - List.fold_right2 - (fun bo ty newmetas -> - let module C = Cic in - match bo with - Cic.Meta i -> - let newmeta = applymetas_to_metas.(i) in - (*CSC: se ty contiene metas, queste hanno il numero errato!!! *) - let ty_with_newmetas = - (* Substitues (META n) with (META (applymetas_to_metas.(n))) *) - let rec aux = - function - C.Rel _ - | C.Var _ as t -> t - | C.Meta n -> C.Meta (applymetas_to_metas.(n)) - | C.Sort _ - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) - | C.Appl l -> C.Appl (List.map aux 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 outt, aux t, - List.map aux pl) - | C.Fix (i,fl) -> - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl - in - C.CoFix (i, substitutedfl) - in - aux ty - in - (newmeta,ty_with_newmetas)::newmetas - | _ -> newmetas - ) mgul mgutl [] +(*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 mgul' = - List.map - (function - Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i)) - | _ as t -> t - ) mgul - in - mgul',uninstantiatedmetas + 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 *) @@ -313,32 +391,47 @@ let apply term = None -> assert false | Some (_,metasenv,_,_) -> metasenv in - let (metano,context,ty) = + 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 + | Some metano -> + List.find (function (m,_,_) -> m=metano) metasenv in - (*CSC: deve sparire! *) - let ciccontext = cic_context_of_context context in - let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in - let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in - let bo' = - if List.length mgul' = 0 then - term - else - Cic.Appl (term::mgul') + 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 - refine_meta metano bo' uninstantiatedmetas ; - match uninstantiatedmetas with - (n,ty)::tl -> goal := Some (n,(context,ty)) - | [] -> goal := None + 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 ciccontext t arg = +let eta_expand metasenv context t arg = let module T = CicTypeChecker in let module S = CicSubstitution in let module C = Cic in @@ -356,7 +449,6 @@ let eta_expand metasenv ciccontext t arg = | 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) -> @@ -380,7 +472,7 @@ let eta_expand metasenv ciccontext t arg = C.CoFix (i, substitutedfl) in let argty = - T.type_of_aux' metasenv ciccontext arg + T.type_of_aux' metasenv context arg in (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) ;; @@ -389,7 +481,7 @@ exception NotAnInductiveTypeToEliminate;; exception NotTheRightEliminatorShape;; exception NoHypothesesFound;; -let elim term = +let elim_intros_simpl term = let module T = CicTypeChecker in let module U = UriManager in let module R = CicReduction in @@ -399,149 +491,166 @@ let elim term = None -> assert false | Some (curi,metasenv,_,_) -> curi,metasenv in - let (metano,context,ty) = + 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 + | Some metano -> + List.find (function (m,_,_) -> m=metano) metasenv in - (*CSC: deve sparire! *) - let ciccontext = cic_context_of_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 + 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_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") + let eliminator_cookingno = + UriManager.relative_depth curi eliminator_uri 0 in - let eliminator_cookingno = - UriManager.relative_depth curi eliminator_uri 0 + let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in + let ety = + T.type_of_aux' [] [] eliminator_ref in - let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in - let ety = - T.type_of_aux' [] [] eliminator_ref + let (econclusion,newmetas,arguments,newmeta,lastmeta) = +(* + new_metasenv_for_apply context ety +*) + new_metasenv_for_apply_intros context ety in - - let earity = CicUnification.get_arity ety in - let mgu = Array.init earity (fun i -> (C.Meta i)) in - let mgut = Array.make earity C.Implicit 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 hypothesis_to_eliminate,econclusion = - (* aux n h t *) - (* traverses the backbone [t] looking for the last hypothesis *) - (* and substituting Pi-abstractions with META declarations. *) - (* [h] is the last hypothesis met up to now. [n] is the next *) - (* unused META. *) - let rec aux n h = - function - C.Prod (_,s,t) -> - mgut.(n) <- s ; - aux (n+1) (Some s) (CicSubstitution.subst (C.Meta n) t) - | C.Cast (te,_) -> aux n h te - | t -> match h with - None -> raise NoHypothesesFound - | Some h' -> h',t - in - aux 0 None ety + (* 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 -prerr_endline ("HTOELIM: " ^ CicPp.ppterm hypothesis_to_eliminate) ; -prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ; -flush stderr ; - ignore (CicUnification.fo_unif_mgu 0 hypothesis_to_eliminate termty mgu) ; - ignore (CicUnification.fo_unif_mgu 0 term (C.Meta (earity - 1)) mgu) ; - let mgu = CicUnification.unwind mgu in -prerr_endline "Dopo l'unwind dell'mgu"; flush stderr ; - let mark = Array.make earity 1 in - let ueconclusion = - CicUnification.unwind_meta mgu mark econclusion + let irl = + identity_relocation_list_for_metavariable canonical_context 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 + 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 + | C.Meta (emeta,_) -> emeta,[] +(* *) + | _ -> 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 eta_expanded_ty = -(*CSC: metasenv e ?????????????*) - List.fold_left (eta_expand metasenv ciccontext) ty fargs + 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 -(*CSC: 0????????*) -prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ; - ignore (CicUnification.fo_unif_mgu 0 ueconclusion eta_expanded_ty mgu) ; -prerr_endline "Dopo la seconda unificazione" ; flush stdout ; - let mgu = CicUnification.unwind mgu in - print_endline "unwind"; flush stdout; - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. *) - let mgut = - let mark = Array.make (Array.length mgu) 1 in - Array.map - (CicUnification.unwind_meta_reducing mgu mark (Some emeta)) - mgut ; + 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 - print_endline "unwind_array"; flush stdout; - let mgu' = Array.copy mgu in - let mgut' = CicUnification.list_of_array mgut in - print_endline "list"; flush stdout; - Array.iteri - (fun i ty -> -prerr_endline ("META " ^ string_of_int i ^ ": " ^ CicPp.ppterm mgu'.(i) ^ - " == " ^ CicPp.ppterm ty) ; flush stderr ; - let ty' = - CicTypeChecker.type_of_aux' mgut' ciccontext mgu'.(i) - in - ignore (CicUnification.fo_unif_mgu 0 ty ty' mgu) - ) mgut ; - let mgu = CicUnification.unwind mgu in - let mgut = CicUnification.unwind_array mgu mgut in -prerr_endline "Dopo le unwind dell'mgut" ; flush stdout ; - let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in -prerr_endline "Dopo il fissaggio" ; flush stdout ; - let bo' = Cic.Appl (eliminator_ref::mgul') in -prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ; - refine_meta metano bo' uninstantiatedmetas ; -prerr_endline "dopo refine meta" ; flush stdout ; - match uninstantiatedmetas with - (n,ty)::tl -> goal := Some (n,(context,ty)) - | [] -> goal := None -;; - -let elim_intros term = - elim term ; - intros () +(*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 = @@ -550,43 +659,66 @@ let reduction_tactic reduction_function term = None -> assert false | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty in - let (metano,context,ty) = + let metano,context,ty = match !goal with None -> assert false - | Some (metano,(context,ty)) -> metano,context,ty + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - let term' = reduction_function 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 (bt,n,t) -> bt,n,replace t) context 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,ty') + (n,_,_) when n = metano -> (metano,context',ty') | _ as t -> t ) metasenv in proof := Some (curi,metasenv',pbo,pty) ; - goal := Some (metano,(context',ty')) + goal := Some metano ;; -let reduction_tactic_in_scratch reduction_function ty term = +(* 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 context = + let metano,context,_ = match !goal with - None -> [] - | Some (_,(context,_)) -> context + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - let term' = reduction_function term in - ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty + let term' = reduction_function context term in + ProofEngineReduction.replace + ~equality:(==) ~what:term ~with_what:term' ~where:ty ;; let whd = reduction_tactic CicReduction.whd;; @@ -606,28 +738,39 @@ let fold term = None -> assert false | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty in - let (metano,context,ty) = + let metano,context,ty = match !goal with None -> assert false - | Some (metano,(context,ty)) -> metano,context,ty + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - let term' = CicReduction.whd term 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 ~what:term' ~with_what:term in + let replace = + ProofEngineReduction.replace + ~equality:(ProofEngineReduction.syntactic_equality) + ~what:term' ~with_what:term + in let ty' = replace ty in - let context' = List.map (function (bt,n,t) -> bt,n,replace t) context 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,ty') + (n,_,_) when n = metano -> (metano,context',ty') | _ as t -> t ) metasenv in proof := Some (curi,metasenv',pbo,pty) ; - goal := Some (metano,(context',ty')) + goal := Some metano ;; let cut term = @@ -637,25 +780,53 @@ let cut term = None -> assert false | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty in - let (metano,context,ty) = + let metano,context,ty = match !goal with None -> assert false - | Some (metano,(context,ty)) -> metano,context,ty + | 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) ; - C.Meta newmeta2] + [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; + C.Meta (newmeta2,irl2)] in -prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ; - refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty]; - goal := - Some - (newmeta1,((Declaration, C.Name "dummy_for_cut", term)::context, - newmeta1ty)) + 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;; @@ -670,28 +841,176 @@ let change ~goal_input ~input = None -> assert false | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty in - let (metano,context,ty) = + let metano,context,ty = match !goal with None -> assert false - | Some (metano,(context,ty)) -> metano,context,ty + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - (*CSC: deve sparire! *) - let ciccontext = cic_context_of_context context in - (* are_convertible works only on well-typed terms *) - ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ; - if CicReduction.are_convertible goal_input input then - begin - let ty' = ProofEngineReduction.replace goal_input input ty 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')) - end + (* 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) +;;