From 780525c2f318cfe782c3d41b70607ba9d72bcc80 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Apr 2009 16:41:20 +0000 Subject: [PATCH] added tentative elim --- .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 2 + .../grafite_engine/grafiteEngine.ml | 4 ++ .../grafite_parser/grafiteParser.ml | 2 + .../ng_disambiguation/nCicDisambiguate.ml | 4 +- helm/software/components/ng_kernel/.depend | 1 - helm/software/components/ng_kernel/nCicPp.ml | 11 ++++ helm/software/components/ng_kernel/nCicPp.mli | 2 + .../components/ng_kernel/nCicReduction.ml | 5 +- .../components/ng_tactics/nTactics.ml | 53 +++++++++++++------ .../components/ng_tactics/nTactics.mli | 1 + 11 files changed, 66 insertions(+), 20 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index ed2d7b9a1..eada3bedc 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -52,6 +52,7 @@ type 'term just = type ntactic = | NApply of loc * CicNotationPt.term | NChange of loc * npattern * CicNotationPt.term + | NElim of loc * CicNotationPt.term * npattern | NId of loc type ('term, 'lazy_term, 'reduction, 'ident) tactic = diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 372ab7fb3..f3e336277 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -93,6 +93,8 @@ let pp_ntactic ~map_unicode_to_tex = function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ " with " ^ CicNotationPp.pp_term wwhat + | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false | NId _ -> "nid" ;; diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 89a63956a..ade6a3350 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -589,6 +589,10 @@ let eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NChange (_loc, pat, ww) -> NTactics.change_tac ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) + | GrafiteAst.NElim (_loc, what, where) -> + NTactics.elim_tac + ~what:(text,prefix_len,what) + ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> fun x -> x ;; diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index e6b3d8991..8e67c0f3e 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -184,6 +184,8 @@ EXTEND [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> GrafiteAst.NChange (loc, what, with_what) + | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> + GrafiteAst.NElim (loc, what, where) ] ]; tactic: [ diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4d8b13226..b9b4fa42b 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -36,8 +36,8 @@ let refine_term let localise t = try NCicUntrusted.NCicHash.find localization_tbl t with Not_found -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - assert false + prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t); + (*assert false*) HExtlib.dummy_floc in let metasenv, subst, term, _ = NCicRefiner.typeof diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index bb269130e..5d08f2d21 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,4 +1,3 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 5b4c9940c..6a38873fc 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -14,6 +14,9 @@ module C = NCic module R = NReference +let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);; +let set_head_beta_reduce = (:=) head_beta_reduce;; + let r2s pp_fix_name r = try match r with @@ -128,6 +131,14 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t = F.fprintf f "]@] @]"; | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> F.fprintf f "BAD APPLICATION" + | C.Appl (C.Meta (n,lc) :: args) when List.mem_assoc n subst -> + let _,_,t,_ = List.assoc n subst in + let hd = NCicSubstitution.subst_meta lc t in + aux ctx + (!head_beta_reduce ~upto:(List.length args) + (match hd with + | NCic.Appl l -> NCic.Appl (l@args) + | _ -> NCic.Appl (hd :: args))) | C.Appl l -> F.fprintf f "@["; if not toplevel then F.fprintf f "("; diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index bdccdd0fd..e8b7c6dab 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -11,6 +11,8 @@ (* $Id$ *) +val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit + val ppterm: context:NCic.context -> subst:NCic.substitution -> diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 0393fbcdd..2b1d4119b 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -400,8 +400,11 @@ let from_stack = RS.from_stack let unwind = R.unwind let _ = - NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t) + NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t); + NCicPp.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t); ;; + + (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 0c5f5360c..2521498ba 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -198,7 +198,7 @@ let compare_statuses ~past ~present = (e.g. the tactic could perform a global analysis of the set of goals) *) -let exec tac (low_status,g) = +let exec tac low_status g = let stack = [ [0,Open g], [], [], `NoTag ] in let status = tac { gstatus = stack ; istatus = low_status } in status.istatus @@ -427,6 +427,20 @@ let select_term low_status (name,context,term) (wanted,path) = mk_meta status ~name:out_scope_tag (`Ctx context) (`Def term) ;; +let select ~where status goal = + let name, _, _ as goalty = get_goal status goal in + let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in + let path = + match where with None -> NCic.Implicit `Term | Some where -> where + in + let status, newgoalty = select_term status goalty (wanted,path) in + let status, instance = + mk_meta status ?name (`Term newgoalty) (`Decl newgoalty) + in + instantiate status goal instance +;; + +let select_tac ~where = distribute_tac (select ~where) ;; let exact t status goal = let goalty = get_goal status goal in @@ -434,7 +448,6 @@ let exact t status goal = instantiate status goal t ;; - let reopen status = let n,h,metasenv,subst,o = status.pstatus in let subst, newm = @@ -477,21 +490,29 @@ let change ~where ~with_what status goal = instantiate status goal instance ;; -let apply t status goal = - let uri,height,metasenv, subst,obj = status.pstatus in - let name,context,gty = List.assoc goal metasenv in - let metasenv, subst, lexicon_status, t = - GrafiteDisambiguate.disambiguate_nterm (Some gty) - status.lstatus context metasenv subst t - in - let subst, metasenv = - (goal, (name, context, t, gty)):: subst, - List.filter(fun (x,_) -> x <> goal) metasenv - in - let new_pstatus = uri,height,metasenv,subst,obj in - { lstatus = lexicon_status; pstatus = new_pstatus } -;; +let apply t status goal = exact t status goal;; let apply_tac t = distribute_tac (apply t) ;; let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;; +let elim_tac ~what ~where status = + block_tac + [ select_tac ~where; + distribute_tac (fun status goal -> + let goalty = get_goal status goal in + let status, (_,_,w as what) = + disambiguate status what None (`Term goalty) in + let _ty_what = typeof status (`Term what) what in + (* check inductive... find eliminator *) + let w = (*astify what *) CicNotationPt.Ident ("m",None) in + let holes = [ + CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit] + in + let eliminator = + CicNotationPt.Appl(CicNotationPt.Ident("nat_ind",None)::holes @ [ w ]) + in + exec (apply_tac ("",0,eliminator)) status goal) ] + status +;; + + diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 0ce7b427e..6c318798e 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -45,6 +45,7 @@ val block_tac: tactic list -> tactic val apply_tac: tactic_term -> tactic val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic +val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic val pp_tac_status: tac_status -> unit -- 2.39.2