X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=ca6b0e58234d59737de1c71660887231e51ee9d6;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=2b67b521f6d0e1ea1cc26f184237280abc48ab11;hpb=bf40c378bd2c624405be2118a478a0734eb8d3aa;p=helm.git diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 2b67b521f..ca6b0e582 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -67,7 +67,7 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = in context, t, (C.Meta (newmeta,irl)) else - raise (Fail "intro(s): not enough products or let-ins") + raise (Fail (lazy "intro(s): not enough products or let-ins")) in collect_context context howmany ty @@ -152,7 +152,12 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in canonical_context' s),None)) | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,Cic.Def (bo,Some ty)) -> + Some + (n, + Cic.Def + (subst_in canonical_context' bo, + Some (subst_in canonical_context' ty))) in entry'::canonical_context' ) canonical_context [] @@ -223,9 +228,9 @@ let new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff ;; -let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty = +let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = - saturate_term newmeta' metasenv' context termty in + saturate_term newmeta' metasenv' context termty goal_arity in let subst,newmetasenv',_ = CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph in @@ -234,7 +239,12 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty = in subst,newmetasenv',t -let apply_tac_verbose ~term (proof, goal) = +let rec count_prods context ty = + match CicReduction.whd context ty with + Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + +let apply_tac_verbose_with_subst ~term (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in let module R = CicReduction in @@ -276,20 +286,20 @@ let apply_tac_verbose ~term (proof, goal) = in let metasenv' = metasenv@newmetasenvfragment in let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in - let termty = - CicSubstitution.subst_vars exp_named_subst_diff termty + CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in -(*CSC: this code is suspect and/or bugged: we try first without reduction - and then using whd. However, the saturate_term always tries with full - reduction without delta. *) + let termty = + CicSubstitution.subst_vars exp_named_subst_diff termty in + let goal_arity = count_prods context ty in let subst,newmetasenv',t = - try + let rec add_one_argument n = + try new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty - termty - with CicUnification.UnificationFailure _ -> - new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty - (CicReduction.whd context termty) + termty n + with CicUnification.UnificationFailure _ when n > 0 -> + add_one_argument (n - 1) + in + add_one_argument goal_arity in let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in let apply_subst = CicMetaSubst.apply_subst subst in @@ -300,7 +310,6 @@ let apply_tac_verbose ~term (proof, goal) = in let bo' = apply_subst t in let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in -(* prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *) let subst_in = (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will be dropped *) @@ -309,21 +318,28 @@ let apply_tac_verbose ~term (proof, goal) = 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)) + (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *) + (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 = +(* ALB *) +let apply_tac_verbose_with_subst ~term status = try - apply_tac_verbose ~term status +(* apply_tac_verbose ~term status *) + apply_tac_verbose_with_subst ~term status (* TODO cacciare anche altre eccezioni? *) with - | CicUnification.UnificationFailure _ as e -> - raise (Fail (Printexc.to_string e)) - | CicTypeChecker.TypeCheckerFailure _ as e -> - raise (Fail (Printexc.to_string e)) + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (Fail msg) + +(* ALB *) +let apply_tac_verbose ~term status = + let subst, status = apply_tac_verbose_with_subst ~term status in + (CicMetaSubst.apply_subst subst), status + +let apply_tac ~term status = snd (apply_tac_verbose ~term status) (* TODO per implementare i tatticali e' necessario che tutte le tattiche sollevino _solamente_ Fail *) @@ -333,10 +349,9 @@ let apply_tac ~term = apply_tac ~term status (* TODO cacciare anche altre eccezioni? *) with - | CicUnification.UnificationFailure _ as e -> - raise (Fail (Printexc.to_string e)) - | CicTypeChecker.TypeCheckerFailure _ as e -> - raise (Fail (Printexc.to_string e)) + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (Fail msg) in mk_tactic (apply_tac ~term) @@ -441,7 +456,7 @@ let exact_tac ~term = (newproof, []) end else - raise (Fail "The type of the provided term is not the one expected.") + raise (Fail (lazy "The type of the provided term is not the one expected.")) in mk_tactic (exact_tac ~term) @@ -455,6 +470,10 @@ let elim_tac ~term = 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 CicUniv.empty_ugraph in + let (termty,metasenv',arguments,fresh_meta) = + ProofEngineHelpers.saturate_term + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in + let term = if arguments = [] then term else Cic.Appl (term::arguments) in let uri,exp_named_subst,typeno,args = match termty with C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) @@ -472,7 +491,7 @@ let elim_tac ~term = name | _ -> assert false in - let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in + let ty_ty,_ = T.type_of_aux' metasenv' context ty CicUniv.empty_ugraph in let ext = match ty_ty with C.Sort C.Prop -> "_ind" @@ -486,7 +505,7 @@ let elim_tac ~term = in let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in let ety,_ = - T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in + 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 @@ -503,10 +522,8 @@ let elim_tac ~term = in 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' + CicRefine.type_of_aux' metasenv' context term_to_refine CicUniv.empty_ugraph in let new_goals =