From: Enrico Tassi Date: Mon, 6 Apr 2009 17:03:55 +0000 (+0000) Subject: tactic cases works! delift clears tags X-Git-Tag: make_still_working~4113 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4b6193be548c96964beee706b75a06e269eed88d;p=helm.git tactic cases works! delift clears tags --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 2deacf2ac..512f5ede4 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -51,6 +51,7 @@ type 'term just = type ntactic = | NApply of loc * CicNotationPt.term + | NCases of loc * CicNotationPt.term * npattern | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term | NElim of loc * CicNotationPt.term * npattern diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 347eab2da..22e4cbe09 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -91,6 +91,8 @@ let pp_just ~term_pp = let pp_ntactic ~map_unicode_to_tex = function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t + | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false | NCase1 (_,n) -> "*" ^ n ^ ":" | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ " with " ^ CicNotationPp.pp_term wwhat diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 09eb2d345..af8b086bf 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -586,6 +586,10 @@ let eval_ng_punct (_text, _prefix_len, punct) = let eval_ng_tac (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) + | GrafiteAst.NCases (_loc, what, where) -> + NTactics.cases_tac + ~what:(text,prefix_len,what) + ~where:(text,prefix_len,where) | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n | GrafiteAst.NChange (_loc, pat, ww) -> NTactics.change_tac diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index fa2680811..b20ca85ba 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -182,6 +182,8 @@ EXTEND using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; ntactic: [ [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) + | IDENT "ncases"; what = tactic_term ; where = pattern_spec -> + GrafiteAst.NCases (loc, what, where) | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> GrafiteAst.NChange (loc, what, with_what) | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 1a2b5471b..adc1ac620 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -266,12 +266,18 @@ let delift ~unify metasenv subst context n l t = (NCicPp.ppterm ~context ~metasenv ~subst t)))) | NCic.Meta (i,l1) as orig -> (try - let tag,_,t,_ = NCicUtils.lookup_subst i subst in - let in_scope = + let tag,c,t,ty = NCicUtils.lookup_subst i subst in + let in_scope, clear = match tag with - | Some tag when tag = in_scope_tag -> 0 - | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag - | _ -> in_scope + | Some tag when tag = in_scope_tag -> 0, true + | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true + | _ -> in_scope, false + in + let ms = + if not clear then ms + else + metasenv, + (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst in aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 8c5dcae76..f79b45841 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -27,7 +27,7 @@ let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -let pp _ = ();; +(* let pp _ = ();; *) let wrap_exc msg = function | NCicUnification.Uncertain _ -> Uncertain msg diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 006fcafe1..22f896f21 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -86,7 +86,7 @@ let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -let pp _ = ();; +(* let pp _ = ();; *) let fix_sorts swap metasenv subst context meta t = let rec aux () = function @@ -302,23 +302,24 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = unify hdb test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) - | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when - not (NCicMetaSubst.flexible subst args) && - is_locked n subst && - not (List.mem_assoc i subst) - -> - (* we verify that none of the args is a Meta, - since beta expanding w.r.t a metavariable makes no sense *) - let metasenv, lambda_Mj = - lambda_intros metasenv subst context t1 args - in - let metasenv, subst = - unify hdb test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj - in + | _, NCic.Meta (n, _) when is_locked n subst -> + (let (metasenv, subst), i = + match NCicReduction.whd ~subst context t1 with + | NCic.Appl (NCic.Meta (i,l)::args) when + not (NCicMetaSubst.flexible subst args) + -> + let metasenv, lambda_Mj = + lambda_intros metasenv subst context t1 args + in + unify hdb test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj, + i + | NCic.Meta (i,_) -> (metasenv, subst), i + | _ -> assert false + in let t1 = NCicReduction.whd ~subst context t1 in let j, lj = - match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false + match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false in let metasenv, subst = instantiate hdb test_eq_only metasenv subst context j lj t2 true @@ -328,7 +329,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let term = eta_reduce subst term in let subst = List.filter (fun (j,_) -> j <> i) subst in metasenv, ((i, (name, ctx, term, ty)) :: subst) - with Not_found -> assert false) + with Not_found -> assert false)) | C.Meta (n,lc), t -> (try diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index f0d12aa8e..1c7029f4a 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -61,6 +61,10 @@ let relocate context (name,ctx,t as term) = assert false ;; +let term_of_cic_term t c = + let _,_,t = relocate c t in + t +;; type ast_term = string * int * CicNotationPt.term diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index ce3fd33b0..6c7d69823 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -33,6 +33,7 @@ type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input type cic_term val ctx_of : cic_term -> NCic.context +val term_of_cic_term : cic_term -> NCic.context -> NCic.term val mk_cic_term : NCic.context -> NCic.term -> cic_term type ast_term = string * int * CicNotationPt.term diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index f45aa656b..52a82af69 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -311,23 +311,27 @@ let intro_tac name = (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit))) ;; -let case ~what status goal = +let cases ~what status goal = let gty = get_goalty status goal in let status, what = disambiguate status what None (ctx_of gty) in let ty = typeof status (ctx_of what) what in let ref, consno, left, right = analyse_indty status ty in let t = - NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1, + NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty), HExtlib.mk_list (NCic.Implicit `Term) consno) in let ctx = ctx_of gty in - let status,t,ty = refine status ctx (mk_cic_term ctx t) None in + let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in instantiate status goal t ;; -let case_tac ~what = distribute_tac (case ~what);; +let cases_tac ~what ~where = + block_tac [ select_tac ~where ; distribute_tac (cases ~what) ] +;; let case1_tac name = block_tac [ intro_tac name; - case_tac ~what:("",0,CicNotationPt.Ident (name,None)) ] + cases_tac + ~where:("",0,(None,[],None)) + ~what:("",0,CicNotationPt.Ident (name,None)) ] ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index fffcad698..a834c4e52 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -32,5 +32,8 @@ val elim_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> NTacStatus.tactic val intro_tac: string -> NTacStatus.tactic +val cases_tac: + what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> + NTacStatus.tactic val case1_tac: string -> NTacStatus.tactic