X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=0cfd8f07cfe620ed9e2fe58438b6c7d97744b5c6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8f5d0c96e9ef749811d7370a33fc3be52984811c;hpb=c7d2d6da56d97250ee7ab619ee8c310d91fa912d;p=helm.git diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 8f5d0c96e..0cfd8f07c 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -1,97 +1,78 @@ -type binder_type = - Declaration - | Definition -;; +(* 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/. + *) -type metasenv = (int * Cic.term) list;; +open ProofEngineHelpers +open ProofEngineTypes -type context = (binder_type * Cic.name * Cic.term) list;; + (* proof assistant status *) -type sequent = context * Cic.term;; +let proof = ref (None : proof option) +let goal = ref (None : goal option) -let proof = - ref (None : (UriManager.uri * 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 get_proof () = !proof;; +let set_proof p = proof := p;; -let refine_meta meta term newmetasenv = - let (uri,metasenv,bo,ty) = - match !proof with +let get_current_status_as_xml () = + match get_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 = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl + | Some (uri, metasenv, bo, ty) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let currentproof = + (*CSC: Wrong: [] is just plainly wrong *) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]) + in + let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = + Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof + in + let xml, bodyxml = + match + Cic2Xml.print_object uri ~ids_to_inner_sorts + ~ask_dtd_to_the_getter:true acurrentproof + with + xml,Some bodyxml -> xml,bodyxml + | _,None -> assert false 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) + (xml, bodyxml) ;; -(* 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) +let apply_tactic ~tactic = + let module PET = ProofEngineTypes in + match get_proof (),!goal with + | None,_ + | _,None -> assert false + | Some proof', Some goal' -> + let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in + set_proof (Some newproof); + goal := + (match newgoals, newproof with + goal::_, _ -> Some goal + | [], (_,(goal,_,_)::_,_,_) -> + (* the tactic left no open goal ; let's choose the first open goal *) + (*CSC: here we could implement and use a proof-tree like notion... *) + Some goal + | _, _ -> None) ;; (* metas_in_term term *) @@ -101,26 +82,26 @@ let metas_in_term term = let module C = Cic in let rec aux = function - C.Rel _ - | C.Var _ -> [] - | C.Meta n -> [n] + C.Rel _ -> [] + | C.Meta (n,_) -> [n] | C.Sort _ - | C.Implicit -> [] + | 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) -> + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_left (fun i (_,t) -> i @ (aux t)) [] exp_named_subst + | C.MutCase (_,_,outt,t,pl) -> (aux outt) @ (aux t) @ (List.fold_left (fun i t -> i @ (aux t)) [] pl) - | C.Fix (i,fl) -> + | C.Fix (_,fl) -> List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl - | C.CoFix (i,fl) -> + | C.CoFix (_,fl) -> List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl in let metas = aux term in @@ -131,7 +112,6 @@ let metas_in_term term = he::(elim_duplicates (List.filter (function el -> he <> el) tl)) in elim_duplicates metas -;; (* perforate context term ty *) (* replaces the term [term] in the proof with a new metavariable whose type *) @@ -140,558 +120,149 @@ let metas_in_term term = (* 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) -> + match get_proof () with + None -> assert false + | Some (uri,metasenv,bo,gty as proof') -> + let newmeta = new_meta_of_proof proof' in (* 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 = + CicMkImplicit.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 -;; + set_proof (Some (uri,metasenv'',bo',gty)) ; + goal := Some newmeta + (************************************************************) (* Some easy tactics. *) (************************************************************) -exception Fail of string;; - -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 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')) +(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) +let reduction_tactic_in_scratch reduction_function terms ty = + let metasenv = + match get_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 terms' = List.map (reduction_function context) terms in + ProofEngineReduction.replace + ~equality:(==) ~what:terms ~with_what:terms' ~where: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 - (*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.") -;; +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 -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 [] - in - let mgul' = - List.map - (function - Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i)) - | _ as t -> t - ) mgul - in - mgul',uninstantiatedmetas -;; +(************************************************************) +(* Tactics defined elsewhere *) +(************************************************************) -(* 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 - (*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') - in - refine_meta metano bo' uninstantiatedmetas ; - match uninstantiatedmetas with - (n,ty)::tl -> goal := Some (n,(context,ty)) - | [] -> goal := None -;; + (* primitive tactics *) +let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term) +let intros ?mk_fresh_name_callback () = + apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ()) +let cut ?mk_fresh_name_callback term = + apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback ~term) +let letin ?mk_fresh_name_callback term = + apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback ~term) +let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) +let elim_intros_simpl term = + apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) +let change ~goal_input:what ~input:with_what = + apply_tactic (PrimitiveTactics.change_tac ~what ~with_what) -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]) -;; + (* structural tactics *) -exception NotAnInductiveTypeToEliminate;; -exception NotTheRightEliminatorShape;; -exception NoHypothesesFound;; +let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp) +let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) -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 - (*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 - 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 + (* reduction tactics *) - 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 - 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 - 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 eta_expanded_ty = -(*CSC: metasenv e ?????????????*) - List.fold_left (eta_expand metasenv ciccontext) ty fargs - 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 ; - 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 whd terms = + apply_tactic + (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms)) +let reduce terms = + apply_tactic + (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms)) +let simpl terms = + apply_tactic + (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms)) -let elim_intros term = - elim term ; - intros () -;; +let fold_whd term = + apply_tactic + (ReductionTactics.fold_tac ~reduction:CicReduction.whd + ~also_in_hypotheses:true ~term) +let fold_reduce term = + apply_tactic + (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce + ~also_in_hypotheses:true ~term) +let fold_simpl term = + apply_tactic + (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl + ~also_in_hypotheses:true ~term) -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 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 - 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')) -;; + (* other tactics *) -let reduction_tactic_in_scratch reduction_function ty term = - let metasenv = - match !proof with - None -> [] - | Some (_,metasenv,_,_) -> metasenv - in - let context = - match !goal with - None -> [] - | Some (_,(context,_)) -> context - in - let term' = reduction_function term in - ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty -;; +let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term) +let ring () = apply_tactic Ring.ring_tac +let fourier () = apply_tactic FourierR.fourier_tac -let whd = reduction_tactic CicReduction.whd;; -let reduce = reduction_tactic ProofEngineReduction.reduce;; -let simpl = reduction_tactic ProofEngineReduction.simpl;; +(* let auto ~dbd () = apply_tactic (AutoTactic.auto_tac ~dbd) *) +let auto ~dbd () = apply_tactic (AutoTactic.auto_tac_new ~dbd) -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,(context,ty)) -> metano,context,ty - in - let term' = CicReduction.whd 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 - 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 rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term) +let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term) +let replace ~goal_input:what ~input:with_what = + apply_tactic (EqualityTactics.replace_tac ~what ~with_what) -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,(context,ty)) -> metano,context,ty - in - let newmeta1 = new_meta () in - let newmeta2 = newmeta1 + 1 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] - 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 reflexivity () = apply_tactic EqualityTactics.reflexivity_tac +let symmetry () = apply_tactic EqualityTactics.symmetry_tac +let transitivity term = apply_tactic (EqualityTactics.transitivity_tac ~term) -exception NotConvertible;; +let exists () = apply_tactic IntroductionTactics.exists_tac +let split () = apply_tactic IntroductionTactics.split_tac +let left () = apply_tactic IntroductionTactics.left_tac +let right () = apply_tactic IntroductionTactics.right_tac + +let assumption () = apply_tactic VariousTactics.assumption_tac + +let generalize ?mk_fresh_name_callback terms = + apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms) + +let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) +let contradiction () = apply_tactic NegationTactics.contradiction_tac + +let decompose ~uris_choice_callback term = + apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term) + +let injection term = apply_tactic (DiscriminationTactics.injection_tac ~term) +let discriminate term = apply_tactic (DiscriminationTactics.discriminate_tac ~term) +let decide_equality () = apply_tactic DiscriminationTactics.decide_equality_tac +let compare term = apply_tactic (DiscriminationTactics.compare_tac ~term) + +(* +let prova_tatticali () = apply_tactic Tacticals.prova_tac +*) -(*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,(context,ty)) -> metano,context,ty - 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 - else - raise NotConvertible -;;