X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FprimitiveTactics.ml;h=8b3f025aa07a575e9e9015528010d725b9bee5f7;hb=850b1a2e1b00104239484ac25aef29c0b943e1e5;hp=25d8899d7cbc645fb6b71571cd80659b07394694;hpb=7074f0403d1bec7f4d60715e50a0fe0ef0993567;p=helm.git diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index 25d8899d7..8b3f025aa 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -31,9 +31,6 @@ exception NotTheRightEliminatorShape exception NoHypothesesFound exception WrongUriToVariable of string -(* TODO problemone del fresh_name, aggiungerlo allo status? *) -let fresh_name () = "FOO" - (* lambda_abstract newmeta ty *) (* returns a triple [bo],[context],[ty'] where *) (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) @@ -122,36 +119,6 @@ let eta_expand metasenv context t arg = in (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) -(*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 proof 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 (fresh_name ()) - 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 ~proof 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 @@ -291,7 +258,7 @@ let apply_tac ~term ~status:(proof, goal) = C.MutConstruct (uri,tyno,consno,exp_named_subst') | _ -> [],newmeta,[],term in - let metasenv' = newmetasenvfragment@metasenv in + let metasenv' = metasenv@newmetasenvfragment in prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; let termty = CicSubstitution.subst_vars exp_named_subst_diff @@ -302,7 +269,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; let (consthead,newmetas,arguments,_) = new_metasenv_for_apply newmeta' proof context termty in - let newmetasenv = newmetas@metasenv' in + let newmetasenv = metasenv'@newmetas in let subst,newmetasenv' = CicUnification.fo_unif newmetasenv context consthead ty in @@ -311,7 +278,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; 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' + classify_metas newmeta in_subst_domain subst_in newmetasenv' in let bo' = apply_subst @@ -409,9 +376,9 @@ let exact_tac ~term ~status:(proof, goal) = raise (Fail "The type of the provided term is not the one expected.") -(* not really "primite" tactics .... *) +(* not really "primitive" tactics .... *) -let elim_intros_simpl_tac ~term ~status:(proof, goal) = +let elim_tac ~term ~status:(proof, goal) = let module T = CicTypeChecker in let module U = UriManager in let module R = CicReduction in @@ -424,10 +391,7 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args) - | _ -> - prerr_endline ("MALFATTORE" ^ (CicPp.ppterm termty)); - flush stderr; - raise NotAnInductiveTypeToEliminate + | _ -> raise NotAnInductiveTypeToEliminate in let eliminator_uri = let buri = U.buri_of_uri uri in @@ -447,16 +411,11 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = in U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in -(*CSC: BUG HERE!!! [] MUST BE COMPUTED SOMEHOW. USING UNIFICATION? *) - let eliminator_ref = C.Const (eliminator_uri,[]) 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 proof context ety + let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in + let ety = T.type_of_aux' metasenv context eliminator_ref in + let newmeta = new_meta ~proof in + let (econclusion,newmetas,arguments,lastmeta) = + new_metasenv_for_apply newmeta proof 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. *) @@ -485,22 +444,8 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = (* 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 @@ -519,7 +464,6 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) 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 *) @@ -529,13 +473,6 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) 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'' @@ -553,25 +490,26 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) (* 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_proof proof metano apply_subst' newmetasenv''' in (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) +;; + +let elim_simpl_intros_tac ~term = + Tacticals.then_ ~start:(elim_tac ~term) + ~continuation: + (Tacticals.then_ + ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~continuation:(intros_tac ~name:"FOO")) +;; exception NotConvertible