From 79659e9015f1f7079b1e7ef846288de60019093a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 14 Apr 2009 13:36:39 +0000 Subject: [PATCH] assert_tac now takes a list of sequents and also checks that the number of sequents is the appropriate one. It is the first example of a high-tactic that works also with the stack. --- .../software/components/grafite/grafiteAst.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 13 ++++- .../grafite_parser/grafiteParser.ml | 5 +- .../components/ng_tactics/nTactics.ml | 57 +++++++++++-------- .../components/ng_tactics/nTactics.mli | 2 +- 5 files changed, 48 insertions(+), 31 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 7c0a3fc99..2e6f450ca 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -51,7 +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 + | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list | 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 1ad89f462..354413f1b 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -586,10 +586,17 @@ 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) -> + | GrafiteAst.NAssert (_loc, seqs) -> 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)) + ((List.map + (function (hyps,concl) -> + 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)) + ) seqs) | 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 db5fa1294..7b4e6157b 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -183,14 +183,15 @@ EXTEND ntactic: [ [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) | IDENT "nassert"; + seqs = LIST0 [ 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) + concl = tactic_term -> (hyps,concl) ] -> + GrafiteAst.NAssert (loc, seqs) | 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/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 3be17c5e7..110e882af 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -497,43 +497,52 @@ let case1_tac name = if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; -let assert_tac (hyps,concl) = distribute_tac (fun status goal -> +let assert0_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 eq status ctx t1 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 + prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2); + assert (t1=t2); + status + in let status,gty' = term_of_cic_term status gty (ctx_of gty) in - assert (concl=gty'); + let status = eq status (ctx_of gty) concl gty' in 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); + let status = eq status ctx t1 t2 in 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); + let status = eq status ctx t1 t2 in + let status = eq status ctx b1 b2 in status,item::ctx | _ -> assert false ) hyps (ctx_of gty) (status,[]) in exec id_tac status goal) ;; + +let assert_tac seqs status = + match status.gstatus with + | [] -> assert false + | (g,_,_,_) :: s -> + assert (List.length g = List.length seqs); + (match seqs with + [] -> id_tac + | [seq] -> assert0_tac seq + | _ -> + block_tac + (branch_tac:: + HExtlib.list_concat ~sep:[shift_tac] + (List.map (fun seq -> [assert0_tac seq]) seqs)@ + [merge_tac]) + ) status +;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 4c3e4d159..b558b4c9b 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -49,5 +49,5 @@ val letin_tac: 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 -> + ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list -> NTacStatus.tactic -- 2.39.2