From 8d7287519cc51145fcac0ee603ba136dc749857d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 14 Apr 2009 12:44:31 +0000 Subject: [PATCH] New debugging tactic nassert: nassert H1: t1 ... Hn: tn \vdash T asserts (using OCaml's assert) that the current goal is equal (using OCaml equality) to the one given the user. The substitution is fully expanded just before calling OCaml equality. --- .../software/components/grafite/grafiteAst.ml | 1 + .../grafite_engine/grafiteEngine.ml | 4 ++ .../grafite_parser/grafiteParser.ml | 9 ++++ .../components/ng_tactics/nTacStatus.ml | 23 +++++++++++ .../components/ng_tactics/nTacStatus.mli | 3 ++ .../components/ng_tactics/nTactics.ml | 41 +++++++++++++++++++ .../components/ng_tactics/nTactics.mli | 4 +- 7 files changed, 84 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 062f2c0d2..7c0a3fc99 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 + | NAssert of loc * (string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term | NCases of loc * CicNotationPt.term * npattern | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ebf0d8a63..1ad89f462 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.NAssert (_loc, hyps, concl) -> + NTactics.assert_tac + (List.map (function (id,`Decl t) -> id,`Decl (text,prefix_len,t) | (id,`Def (b,t)) -> id,`Def ((text,prefix_len,b),(text,prefix_len,t))) hyps, + (text,prefix_len,concl)) | GrafiteAst.NCases (_loc, what, where) -> NTactics.cases_tac ~what:(text,prefix_len,what) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 56da062e8..db5fa1294 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -182,6 +182,15 @@ EXTEND using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; ntactic: [ [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) + | IDENT "nassert"; + hyps = LIST0 + [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty + | id = IDENT ; SYMBOL ":" ; ty = tactic_term ; + SYMBOL <:unicode> ; bo = tactic_term -> + id,`Def (bo,ty)]; + SYMBOL <:unicode>; + concl = tactic_term -> + GrafiteAst.NAssert (loc, hyps, concl) | IDENT "ncases"; what = tactic_term ; where = pattern_spec -> GrafiteAst.NCases (loc, what, where) | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 86487e20d..55448ae2d 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -319,3 +319,26 @@ let analyse_indty status ty = ;; let mk_cic_term c t = None,c,t ;; + +let apply_subst status ctx t = + let status, (name,_,t) = relocate status ctx t in + let _,_,_,subst,_ = status.pstatus in + let rec aux ctx = + function + NCic.Meta (i,lc) -> + (try + let _,_,t,_ = NCicUtils.lookup_subst i subst in + let t = NCicSubstitution.subst_meta lc t in + aux ctx t + with + Not_found -> + match lc with + _,NCic.Irl _ -> NCic.Meta (i,lc) + | n,NCic.Ctx l -> + NCic.Meta + (i,(0,NCic.Ctx + (List.map (fun t -> aux ctx (NCicSubstitution.lift n t)) l)))) + | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx aux t + in + status, (name, ctx, aux ctx t) +;; diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 81436f53d..c0f0ca4db 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -56,6 +56,9 @@ val unify: val refine: lowtac_status -> NCic.context -> cic_term -> cic_term option -> lowtac_status * cic_term * cic_term (* status, term, type *) +val apply_subst: + lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term + val get_goalty: lowtac_status -> int -> cic_term val mk_meta: diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 30ccaf86d..3be17c5e7 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -496,3 +496,44 @@ let case1_tac name = ~what:("",0,Ast.Ident (name,None)); if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; + +let assert_tac (hyps,concl) = distribute_tac (fun status goal -> + let gty = get_goalty status goal in + let status,concl = disambiguate status concl None (ctx_of gty) in + let status,concl = term_of_cic_term status concl (ctx_of gty) in + let status,gty' = term_of_cic_term status gty (ctx_of gty) in + assert (concl=gty'); + let status,_ = + List.fold_right2 + (fun (id1,e1) ((id2,e2) as item) (status,ctx) -> + assert (id1=id2); + match e1,e2 with + `Decl t1, NCic.Decl t2 -> + let status,t1 = disambiguate status t1 None ctx in + let status,t1 = apply_subst status ctx t1 in + let status,t1 = term_of_cic_term status t1 ctx in + let t2 = mk_cic_term ctx t2 in + let status,t2 = apply_subst status ctx t2 in + let status,t2 = term_of_cic_term status t2 ctx in + assert (t1=t2); + status,item::ctx + | `Def (b1,t1), NCic.Def (b2,t2) -> + let status,t1 = disambiguate status t1 None ctx in + let status,t1 = apply_subst status ctx t1 in + let status,t1 = term_of_cic_term status t1 ctx in + let status,b1 = disambiguate status b1 None ctx in + let status,b1 = apply_subst status ctx b1 in + let status,b1 = term_of_cic_term status b1 ctx in + let t2 = mk_cic_term ctx t2 in + let status,t2 = apply_subst status ctx t2 in + let status,t2 = term_of_cic_term status t2 ctx in + let b2 = mk_cic_term ctx b2 in + let status,b2 = apply_subst status ctx b2 in + let status,b2 = term_of_cic_term status b2 ctx in + assert (t1=t2 && b1=b2); + status,item::ctx + | _ -> assert false + ) hyps (ctx_of gty) (status,[]) + in + exec id_tac status goal) +;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 0605b993f..4c3e4d159 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -48,4 +48,6 @@ val letin_tac: where:NTacStatus.tactic_pattern -> what: NTacStatus.tactic_term -> string -> NTacStatus.tactic - +val assert_tac: + (string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term -> + NTacStatus.tactic -- 2.39.2