X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FprimitiveTactics.ml;h=8b3f025aa07a575e9e9015528010d725b9bee5f7;hb=b5dd63f1413ba984c2e09239ad4554775467f653;hp=b52fb78826a53ff12a8ef333058ac1d32a2dcf67;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index b52fb7882..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,34 +167,109 @@ 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 -let apply_tac ~status:(proof, goal) ~term = +(* 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 *) let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let metasenv = - match proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let metano,context,ty = - match goal with - None -> assert false - | Some metano -> - List.find (function (m,_,_) -> m=metano) metasenv - in - let termty = CicTypeChecker.type_of_aux' metasenv context term in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv 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 @@ -228,65 +281,47 @@ let apply_tac ~status:(proof, goal) ~term = 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 subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv'' in - (newproof, - (match newmetasenv''' with - | [] -> None - | (i,_,_)::_ -> Some i)) + (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) (* TODO per implementare i tatticali e' necessario che tutte le tattiche sollevino _solamente_ Fail *) -let apply_tac ~status ~term = +let apply_tac ~term ~status = try - apply_tac ~status ~term + apply_tac ~term ~status (* TODO cacciare anche altre eccezioni? *) with CicUnification.UnificationFailed as e -> raise (Fail (Printexc.to_string e)) -let intros_tac ~status:(proof, goal) ~name = +let intros_tac ~name ~status:(proof, goal) = let module C = Cic in let module R = CicReduction in - let metasenv = - match proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let metano,context,ty = - match goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let newmeta = new_meta ~proof in let (context',ty',bo') = lambda_abstract context newmeta ty name in let (newproof, _) = subst_meta_in_proof proof metano bo' [newmeta,context',ty'] in - let newgoal = Some newmeta in - (newproof, newgoal) + (newproof, [newmeta]) -let cut_tac ~status:(proof, goal) ~term = +let cut_tac ~term ~status:(proof, goal) = 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 curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let newmeta1 = new_meta ~proof in let newmeta2 = newmeta1 + 1 in let context_for_newmeta1 = @@ -304,21 +339,12 @@ let cut_tac ~status:(proof, goal) ~term = subst_meta_in_proof proof metano bo' [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; in - let newgoal = Some newmeta1 in - (newproof, newgoal) + (newproof, [newmeta1 ; newmeta2]) -let letin_tac ~status:(proof, goal) ~term = +let letin_tac ~term ~status:(proof, goal) = 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 curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let _ = CicTypeChecker.type_of_aux' metasenv context term in let newmeta = new_meta ~proof in let context_for_newmeta = @@ -331,72 +357,46 @@ let letin_tac ~status:(proof, goal) ~term = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in - let newgoal = Some newmeta in - (newproof, newgoal) + (newproof, [newmeta]) (** functional part of the "exact" tactic *) -let exact_tac ~status:(proof, goal) ~term = +let exact_tac ~term ~status:(proof, goal) = (* Assumption: the term bo must be closed in the current context *) - let metasenv = - match proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let metano,context,ty = - match goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let module T = CicTypeChecker in let module R = CicReduction in if R.are_convertible context (T.type_of_aux' metasenv context term) ty then begin let (newproof, metasenv') = subst_meta_in_proof proof metano term [] in - let newgoal = - (match metasenv' with - [] -> None - | (n,_,_)::_ -> Some n) - in - (newproof, newgoal) + (newproof, []) end else 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 ~status:(proof, goal) ~term = +let elim_tac ~term ~status:(proof, goal) = let module T = CicTypeChecker in let module U = UriManager in let module R = CicReduction in let module C = Cic in - let curi,metasenv = - match proof with - None -> assert false - | Some (curi,metasenv,_,_) -> curi,metasenv - in - let metano,context,ty = - match goal with - None -> assert false - | Some metano -> - List.find (function (m,_,_) -> m=metano) metasenv - in + let (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 @@ -411,18 +411,11 @@ let elim_intros_simpl_tac ~status:(proof, goal) ~term = 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. *) @@ -451,22 +444,8 @@ let elim_intros_simpl_tac ~status:(proof, goal) ~term = (* 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 @@ -485,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 *) @@ -495,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'' @@ -519,25 +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, - (match newmetasenv'''' with - | [] -> None - | (i,_,_)::_ -> Some i)) + 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")