X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=ca6b0e58234d59737de1c71660887231e51ee9d6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c43034f93dfd7f672ade503c0723e9474bd021ea;hpb=e6005301fcbccbca31571795ed6071283f45d5a8;p=helm.git diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c43034f93..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) @@ -457,7 +472,7 @@ let elim_tac ~term = 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 in + (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 @@ -507,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 =