From bf6f5b964bd4e6c16401a4bfab3c29d6824be22a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2009 16:13:40 +0000 Subject: [PATCH] tentative subst-sexpand and change --- .../components/binaries/transcript/.depend | 5 - .../binaries/transcript/.depend.opt | 5 - .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 2 + .../grafite_engine/grafiteEngine.ml | 2 + .../grafite_parser/grafiteParser.ml | 5 +- .../components/ng_tactics/nTactics.ml | 114 +++++++++++++++++- .../components/ng_tactics/nTactics.mli | 1 + .../components/syntax_extensions/.depend | 3 - 9 files changed, 119 insertions(+), 19 deletions(-) diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 8121968e9..660edb2f5 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,10 +1,5 @@ v8Parser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: v8Parser.cmo: types.cmo options.cmo v8Parser.cmi v8Parser.cmx: types.cmx options.cmx v8Parser.cmi v8Lexer.cmo: v8Parser.cmi options.cmo diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index b64d148de..5e2c3e23c 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,10 +1,5 @@ v8Parser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: v8Parser.cmo: types.cmx options.cmx v8Parser.cmi v8Parser.cmx: types.cmx options.cmx v8Parser.cmi v8Lexer.cmo: v8Parser.cmi options.cmx diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 7593fe53a..7b4411d02 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -48,6 +48,7 @@ type 'term just = type ntactic = | NApply of loc * CicNotationPt.term + | NChange of loc * CicNotationPt.term * CicNotationPt.term | 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 5785a1071..3ab738ab7 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 + | NChange (_,what,wwhat) -> "nchange " ^ CicNotationPp.pp_term what + ^ " " ^ CicNotationPp.pp_term wwhat | NId _ -> "nid" ;; diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 0b87b40be..b8310f3fc 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -586,6 +586,8 @@ 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.NChange (_loc, w,ww) -> + NTactics.change_tac (text,prefix_len,w) (text,prefix_len,ww) | GrafiteAst.NId _ -> fun x -> x ;; diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b9c33232e..6c5175890 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -181,8 +181,9 @@ EXTEND ]; using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; ntactic: [ - [ IDENT "napply"; t = tactic_term -> - GrafiteAst.NApply (loc, t) + [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) + | IDENT "nchange"; what = tactic_term; with_what = tactic_term -> + GrafiteAst.NChange (loc, what, with_what) ] ]; tactic: [ diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index dd09178c2..4f6a726df 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -233,14 +233,26 @@ let distribute_tac tac status = { gstatus = stack; istatus = sn } ;; -(* - type cic_term = NCic.conjecture type ast_term = string * int * CicNotationPt.term type position = Ctx of NCic.context | Term of cic_term + let relocate (name,ctx,t as term) context = - if ctx = context then term else assert false + let is_prefix l1 l2 = + let rec aux = function + | [],[] -> true + | x::xs, y::ys -> x=y && aux (xs,ys) + | _ -> false + in + aux (List.rev l1, List.rev l2) + in + if ctx = context then term else + if is_prefix ctx context then + (name, context, + NCicSubstitution.lift (List.length context - List.length ctx) t) + else + assert false ;; let disambiguate (status : lowtac_status) (t : ast_term) @@ -259,6 +271,62 @@ let disambiguate (status : lowtac_status) (t : ast_term) { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) ;; +let select_term low_status (name,context,term) (path, matched) = + let eq context (status as old_status) t1 t2 = + let _,_,t2 = relocate t2 context in + if t2 = t1 then true, status else false, old_status + in + let match_term m = + let rec aux ctx status t = + let b, status = eq ctx status t m in + if b then + let n,h,metasenv,subst,o = status.pstatus in + let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in + let metasenv, instance, ty = + NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty) + in + let metasenv, subst = + NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx + t instance + in + let status = { status with pstatus = n,h,metasenv,subst,o } in + status, instance + else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t + in + aux + in + let rec select status ctx pat cic = + match pat, cic with + | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) -> + let status, s = select status ctx s1 s2 in + let ctx = (n, NCic.Decl s2) :: ctx in + let status, t = select status ctx t1 t2 in + status, NCic.Prod (n,s,t) + | NCic.Appl l1, NCic.Appl l2 -> + let status, l = + List.fold_left2 + (fun (status,l) x y -> + let status, x = select status ctx x y in + status, l @ [x]) + (status,[]) l1 l2 + in + status, NCic.Appl l + | NCic.Implicit `Hole, t -> status, t + | NCic.Implicit `Term, t -> + let status, matched = disambiguate status matched None (Ctx ctx) in + match_term matched ctx status t + | _,t -> status, t + in + let status, term = select low_status context path term in + let _,_,_,subst,_ = status.pstatus in + let selections = + HExtlib.filter_map + (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None) + subst + in + status, (name, context, term), selections +;; + let get_goal (status : lowtac_status) (g : int) = let _,_,metasenv,_,_ = status.pstatus in List.assoc g metasenv @@ -281,13 +349,50 @@ let instantiate status i t = { status with pstatus = (name,height,metasenv,subst,obj) } ;; +let mkmeta name status (_,ctx,ty) = + let n,h,metasenv,s,o = status.pstatus in + let metasenv, instance, _ = + NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) + in + let status = { status with pstatus = n,h,metasenv,s,o } in + status, (name,ctx,instance) +;; + let apply t (status as orig, goal) = let goalty = get_goal status goal in let status, t = disambiguate status t (Some goalty) (Term goalty) in let status = instantiate status goal t in return ~orig status ;; -*) + +let change what (*where*) with_what (status as orig, goal) = + let (name,_,_ as goalty) = get_goal status goal in + let status, newgoalty, selections = + select_term status goalty + (NCic.Prod ("_",NCic.Implicit `Hole,NCic.Implicit `Term), what) + in + + let n,h,metasenv,subst,o = status.pstatus in + let subst, newm = + List.partition (fun i,_ -> not (List.mem i selections)) subst + in + let metasenv = List.map (fun (i,(n,c,_,t)) -> i,(n,c,t)) newm @ metasenv in + let status = { status with pstatus = n,h,metasenv,subst,o } in + + let status = (* queste sono apply, usa un tatticale! *) + List.fold_left + (fun status i -> + let x = get_goal status i in + let status, with_what = + disambiguate status with_what (Some x) (Term x) + in + instantiate status i with_what) + status selections + in + let status, m = mkmeta name status newgoalty in + let status = instantiate status goal m in + return ~orig status +;; let apply t (status,goal) = let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in @@ -314,4 +419,5 @@ let apply t (status,goal) = ;; let apply_tac t = distribute_tac (apply t) ;; +let change_tac w ww = distribute_tac (change w ww) ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index f9747e824..29b7613a5 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -42,6 +42,7 @@ val distribute_tac: lowtactic -> tactic val block_tac: tactic list -> tactic val apply_tac: tactic_term -> tactic +val change_tac: tactic_term -> tactic_term -> tactic val pp_tac_status: tac_status -> unit diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2