X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=0cb8aceadbaaf3a14bbc43d95fd65897b7a53468;hb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;hp=2d741f1d1c317a72cfcf62d9b25be6f4cf88f496;hpb=2697b6b76d4a2449ac9ad6657128c0cc3d90ac65;p=helm.git diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 2d741f1d1..0cb8acead 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -72,7 +72,11 @@ let eta_expand metasenv context t arg = | 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.Meta (i,l) -> + let l' = + List.map (function None -> None | Some t -> Some (aux n t)) l + in + C.Meta (i, l') | C.Sort _ | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) @@ -111,11 +115,11 @@ let eta_expand metasenv context t arg = 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 + let argty,_ = + T.type_of_aux' metasenv context arg CicUniv.empty_ugraph (* TASSI: FIXME *) in let fresh_name = - FreshNamesGenerator.mk_fresh_name + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context (Cic.Name "Heta") ~typ:argty in (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg]) @@ -200,11 +204,12 @@ let = 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 + let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o 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 @@ -215,10 +220,11 @@ let [],[] -> [] | 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)) + let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with + C.Variable (_,_,ty,_) -> + CicSubstitution.subst_vars !exp_named_subst_diff ty + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) in (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type (match ty with @@ -256,7 +262,7 @@ let new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff ;; -let apply_tac ~term (proof, goal) = +let apply_tac_verbose ~term (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in let module R = CicReduction in @@ -297,17 +303,19 @@ let apply_tac ~term (proof, goal) = | _ -> [],newmeta,[],term in let metasenv' = metasenv@newmetasenvfragment in + let termty,_ = (* TASSI:FIXME *) + CicTypeChecker.type_of_aux' metasenv' context term CicUniv.empty_ugraph in let termty = - CicSubstitution.subst_vars exp_named_subst_diff - (CicTypeChecker.type_of_aux' metasenv' context term) + CicSubstitution.subst_vars exp_named_subst_diff termty in (* newmeta is the lowest index of the new metas introduced *) let (consthead,newmetas,arguments,_) = new_metasenv_for_apply newmeta' proof context termty in let newmetasenv = metasenv'@newmetas in - let subst,newmetasenv' = - CicUnification.fo_unif newmetasenv context consthead ty + let subst,newmetasenv',_ = (* TASSI:FIXME *) + CicUnification.fo_unif newmetasenv context consthead ty + CicUniv.empty_ugraph in let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in let apply_subst = CicMetaSubst.apply_subst subst in @@ -324,13 +332,27 @@ let apply_tac ~term (proof, goal) = Cic.Appl (term'::arguments) ) in - let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in - let (newproof, newmetasenv''') = - let subst_in = CicMetaSubst.apply_subst ((metano,bo')::subst) in - subst_meta_and_metasenv_in_proof - proof metano subst_in newmetasenv'' - in - (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in + let subst_in = + (* if we just apply the subtitution, the type is irrelevant: + we may use Implicit, since it will be dropped *) + CicMetaSubst.apply_subst + ((metano,(context, bo', Cic.Implicit None))::subst) + in + let (newproof, newmetasenv''') = + subst_meta_and_metasenv_in_proof + proof metano subst_in newmetasenv'' + in + (subst_in,(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas)) + +let apply_tac ~term status = snd (apply_tac_verbose ~term status) + +let apply_tac_verbose ~term status = + try + apply_tac_verbose ~term status + (* TODO cacciare anche altre eccezioni? *) + with CicUnification.UnificationFailure _ as e -> + raise (Fail (Printexc.to_string e)) (* TODO per implementare i tatticali e' necessario che tutte le tattiche sollevino _solamente_ Fail *) @@ -344,9 +366,9 @@ let apply_tac ~term = in mk_tactic (apply_tac ~term) -let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()= +let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()= let intros_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) () + ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) () (proof, goal) = let module C = Cic in @@ -364,9 +386,9 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()= in mk_tactic (intros_tac ~mk_fresh_name_callback ()) -let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term= +let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term= let cut_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term (proof, goal) = let module C = Cic in @@ -399,15 +421,16 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term= in mk_tactic (cut_tac ~mk_fresh_name_callback term) -let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) term= +let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term= let letin_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term (proof, goal) = let module C = Cic in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let _ = CicTypeChecker.type_of_aux' metasenv context term in + let _,_ = (* TASSI: FIXME *) + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in let newmeta = new_meta_of_proof ~proof in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in @@ -435,7 +458,9 @@ let exact_tac ~term = let metano,context,ty = CicUtil.lookup_meta 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 + let ty_term,u = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *) + if b then begin let (newproof, metasenv') = subst_meta_in_proof proof metano term [] in @@ -455,7 +480,8 @@ let elim_tac ~term = let module C = Cic in let (curi,metasenv,proofbo,proofty) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let termty = T.type_of_aux' metasenv context term in + let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + (* TASSI: FIXME *) let uri,exp_named_subst,typeno,args = match termty with C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) @@ -466,24 +492,28 @@ let elim_tac ~term = let eliminator_uri = let buri = U.buri_of_uri uri in let name = - match CicEnvironment.get_obj uri with + let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with C.InductiveDefinition (tys,_,_) -> let (name,_,_,_) = List.nth tys typeno in name | _ -> assert false in + let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in + (* TASSI: FIXME *) let ext = - match T.type_of_aux' metasenv context ty with + match ty_ty with C.Sort C.Prop -> "_ind" | C.Sort C.Set -> "_rec" | C.Sort C.CProp -> "_rec" - | C.Sort (C.Type _)-> "_rect" (* TASSI *) + | C.Sort (C.Type _)-> "_rect" | _ -> assert false in U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in - let ety = T.type_of_aux' metasenv context eliminator_ref in + let ety,_ = + T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in let rec find_args_no = function C.Prod (_,_,t) -> 1 + find_args_no t @@ -501,9 +531,10 @@ let elim_tac ~term = C.Appl (eliminator_ref :: make_tl term (args_no - 1)) in let metasenv', term_to_refine' = - CicMkImplicit.expand_implicits metasenv context term_to_refine in - let refined_term,_,metasenv'' = - CicRefine.type_of_aux' metasenv' context term_to_refine' + CicMkImplicit.expand_implicits metasenv [] context term_to_refine in + let refined_term,_,metasenv'',_ = (* TASSI: FIXME *) + CicRefine.type_of_aux' metasenv' context term_to_refine' + CicUniv.empty_ugraph in let new_goals = ProofEngineHelpers.compare_metasenvs @@ -542,37 +573,45 @@ exception NotConvertible (*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 = - let change_tac ~what ~with_what (proof, goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta 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:[what] ~with_what:[with_what] - in - let ty' = replace ty in - let context' = - List.map - (function - Some (name,Cic.Def (t,None))->Some (name,Cic.Def ((replace t),None)) - | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) - | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false - ) 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") - in - mk_tactic (change_tac ~what ~with_what) + let change_tac ~what ~with_what (proof, goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + (* are_convertible works only on well-typed terms *) + let _,u = + CicTypeChecker.type_of_aux' metasenv context with_what + CicUniv.empty_ugraph + in (* TASSI: FIXME *) + let b,_ = + CicReduction.are_convertible context what with_what u + in + if b then + begin + let replace = + ProofEngineReduction.replace + ~equality:(==) ~what:[what] ~with_what:[with_what] + in + let ty' = replace ty in + let context' = + List.map + (function + Some (name,Cic.Def (t,None))-> + Some (name,Cic.Def ((replace t),None)) + | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) + | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false + ) 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") + in + mk_tactic (change_tac ~what ~with_what) +