X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FprimitiveTactics.ml;h=8b3f025aa07a575e9e9015528010d725b9bee5f7;hb=7e9ee837f75f38bf01240cdc03dd51c764c2665f;hp=75f421cede4ec24c666700a69a1316d56fbdd818;hpb=4720c6af414c4a834a994fdb404fda2d0c04fc03;p=helm.git diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index 75f421ced..8b3f025aa 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -29,9 +29,7 @@ open ProofEngineTypes exception NotAnInductiveTypeToEliminate exception NotTheRightEliminatorShape exception NoHypothesesFound - -(* TODO problemone del fresh_name, aggiungerlo allo status? *) -let fresh_name () = "FOO" +exception WrongUriToVariable of string (* lambda_abstract newmeta ty *) (* returns a triple [bo],[context],[ty'] where *) @@ -49,7 +47,7 @@ let lambda_abstract context newmeta ty name = match n with C.Name _ -> n (*CSC: generatore di nomi? Chiedere il nome? *) - | C.Anonimous -> C.Name name + | C.Anonymous -> C.Name name in let (context',ty,bo) = collect_context ((Some (n',(C.Decl s)))::context) t @@ -74,7 +72,9 @@ let eta_expand metasenv context t arg = 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.Var (uri,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.Var (uri,exp_named_subst') | C.Meta _ | C.Sort _ | C.Implicit as t -> t @@ -83,11 +83,17 @@ let eta_expand metasenv context t arg = | 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.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, + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,aux n outt, aux n t, List.map (aux n) pl) | C.Fix (i,fl) -> let tylen = List.length fl in @@ -105,42 +111,14 @@ let eta_expand metasenv context t arg = fl in C.CoFix (i, substitutedfl) + and aux_exp_named_subst n = + List.map (function uri,t -> uri,aux n t) in let argty = T.type_of_aux' metasenv context 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 @@ -174,7 +152,7 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = (* 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 proof context ty = +let new_metasenv_for_apply newmeta proof context ty = let module C = Cic in let module S = CicSubstitution in let rec aux newmeta = @@ -189,11 +167,56 @@ let new_metasenv_for_apply proof context ty = res,(newmeta,context,s)::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 + (* 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,lastmeta + +(* Useful only inside apply_tac *) +let + generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst += + let module C = Cic in + let params = + match CicEnvironment.get_obj uri with + C.Constant (_,_,_,params) + | C.CurrentProof (_,_,_,_,params) + | C.Variable (_,_,_,params) + | C.InductiveDefinition (_,params,_) -> params + in + let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'= + let next_fresh_meta = ref newmeta in + let newmetasenvfragment = ref [] in + let exp_named_subst_diff = ref [] in + let rec aux = + function + [],[] -> [] + | uri::tl,[] -> + let ty = + match CicEnvironment.get_obj uri with + C.Variable (_,_,ty,_) -> + CicSubstitution.subst_vars !exp_named_subst_diff ty + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + in + let irl = identity_relocation_list_for_metavariable context in + let subst_item = uri,C.Meta (!next_fresh_meta,irl) in + newmetasenvfragment := + (!next_fresh_meta,context,ty)::!newmetasenvfragment ; + exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ; + incr next_fresh_meta ; + subst_item::(aux (tl,[])) + | uri::tl1,((uri',_) as s)::tl2 -> + assert (UriManager.eq uri uri') ; + s::(aux (tl1,tl2)) + | [],_ -> assert false + in + let exp_named_subst' = aux (params,exp_named_subst) in + !exp_named_subst_diff,!next_fresh_meta, + List.rev !newmetasenvfragment, exp_named_subst' + in +prerr_endline ("@@@ " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst)) ^ " |--> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst'))) ; + new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff +;; let apply_tac ~term ~status:(proof, goal) = (* Assumption: The term "term" must be closed in the current context *) @@ -202,12 +225,51 @@ let apply_tac ~term ~status:(proof, goal) = let module C = Cic in let (_,metasenv,_,_) = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let termty = CicTypeChecker.type_of_aux' metasenv context term in + let newmeta = new_meta ~proof in + let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = + match term with + C.Var (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Var (uri,exp_named_subst') + | C.Const (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | _ -> [],newmeta,[],term + in + let metasenv' = metasenv@newmetasenvfragment in +prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; + let termty = + CicSubstitution.subst_vars exp_named_subst_diff + (CicTypeChecker.type_of_aux' metasenv' context term) + in +prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; (* newmeta is the lowest index of the new metas introduced *) - let (consthead,newmetas,arguments,newmeta,_) = - new_metasenv_for_apply proof context 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 @@ -219,12 +281,14 @@ let apply_tac ~term ~status:(proof, goal) = 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') + apply_subst + (if List.length newmetas = 0 then + term' + else + Cic.Appl (term'::arguments) + ) in +prerr_endline ("XXXX " ^ CicPp.ppterm (if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)) ^ " |>>> " ^ CicPp.ppterm bo') ; let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in let (newproof, newmetasenv''') = let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in @@ -312,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 @@ -322,20 +386,17 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = let (curi,metasenv,_,_) = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let termty = T.type_of_aux' metasenv context term in - let uri,cookingno,typeno,args = + let uri,exp_named_subst,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) - | _ -> - prerr_endline ("MALFATTORE" ^ (CicPp.ppterm termty)); - flush stderr; - raise NotAnInductiveTypeToEliminate + 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) + | _ -> raise NotAnInductiveTypeToEliminate in let eliminator_uri = let buri = U.buri_of_uri uri in let name = - match CicEnvironment.get_cooked_obj uri cookingno with + match CicEnvironment.get_obj uri with C.InductiveDefinition (tys,_,_) -> let (name,_,_,_) = List.nth tys typeno in name @@ -350,18 +411,11 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = 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 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. *) @@ -390,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 @@ -424,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 *) @@ -434,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'' @@ -458,22 +490,61 @@ 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 + +(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal, *) +(*CSC: while [what] can have a richer context (because of binders) *) +(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *) +(*CSC: Is that evident? Is that right? Or should it be changed? *) +let change_tac ~what ~with_what ~status:(proof, goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + (* are_convertible works only on well-typed terms *) + ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; + if CicReduction.are_convertible context what with_what then + begin + let replace = + ProofEngineReduction.replace ~equality:(==) ~what ~with_what + 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 + (curi,metasenv',pbo,pty), [metano] + end + else + raise (ProofEngineTypes.Fail "Not convertible")