From e898ca2563cc4dfbd328efc7aa3a4ff86feaec92 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Apr 2009 15:28:33 +0000 Subject: [PATCH] 1) mk_meta now returns also the index of the created meta 2) added datatypes for new patterns 3) added tactic nchange (using new patterns) 4) changed the type lowtac so that they no longer return the lists of open and closed goals, that are always computable in the new system 5) added some wrappers for kernel/refinement functions that work on statuses and terms labelled with their context 6) new implementation of select that performs subst-expansion. in-scope/out-scope used to mark regions selected by the pattern 7) ugly implementation of change based on re-opening of tagged subst entries --- .../software/components/grafite/grafiteAst.ml | 5 +- .../components/grafite/grafiteAstPp.ml | 4 +- .../grafite_engine/grafiteEngine.ml | 5 +- .../grafite_parser/grafiteDisambiguate.ml | 14 + .../grafite_parser/grafiteDisambiguate.mli | 9 + .../grafite_parser/grafiteParser.ml | 2 +- .../ng_disambiguation/nCicDisambiguate.ml | 16 +- .../ng_disambiguation/nCicDisambiguate.mli | 2 + helm/software/components/ng_refiner/check.ml | 3 +- .../components/ng_refiner/nCicMetaSubst.ml | 8 +- .../components/ng_refiner/nCicMetaSubst.mli | 2 +- .../components/ng_refiner/nCicRefiner.ml | 8 +- .../components/ng_refiner/nCicUnifHint.ml | 5 +- .../components/ng_tactics/nTactics.ml | 302 +++++++++++------- .../components/ng_tactics/nTactics.mli | 6 +- 15 files changed, 253 insertions(+), 138 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 7b4411d02..ed2d7b9a1 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -32,6 +32,9 @@ type loc = Stdpp.location type ('term, 'lazy_term, 'ident) pattern = 'lazy_term option * ('ident * 'term) list * 'term option +type npattern = + CicNotationPt.term option * (string * CicNotationPt.term) list * CicNotationPt.term option + type 'lazy_term reduction = [ `Normalize | `Simpl @@ -48,7 +51,7 @@ type 'term just = type ntactic = | NApply of loc * CicNotationPt.term - | NChange of loc * CicNotationPt.term * CicNotationPt.term + | NChange of loc * npattern * 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 3ab738ab7..372ab7fb3 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -91,8 +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 + | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ + " with " ^ 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 b8310f3fc..89a63956a 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -586,8 +586,9 @@ 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.NChange (_loc, pat, ww) -> + NTactics.change_tac + ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) | GrafiteAst.NId _ -> fun x -> x ;; diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 027cde4a5..323c8985e 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -234,6 +234,20 @@ let disambiguate_pattern (wanted, hyp_paths, goal_path) ;; +type pattern = + CicNotationPt.term Disambiguate.disambiguator_input option * + (string * NCic.term) list * NCic.term option + +let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = + let interp path = NCicDisambiguate.disambiguate_path path in + let goal_path = HExtlib.map_option interp goal_path in + let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in + let wanted = + match wanted with None -> None | Some x -> Some (text,prefix_len,x) + in + (wanted, hyp_paths, goal_path) +;; + let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function | `Unfold (Some t) -> let t = diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index 163e6db6d..b8814d4d8 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -60,3 +60,12 @@ val disambiguate_nterm : NCic.context -> NCic.metasenv -> NCic.substitution -> CicNotationPt.term Disambiguate.disambiguator_input -> NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term + +type pattern = + CicNotationPt.term Disambiguate.disambiguator_input option * + (string * NCic.term) list * NCic.term option + +val disambiguate_npattern: + GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern + + diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 6c5175890..e6b3d8991 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -182,7 +182,7 @@ EXTEND using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; ntactic: [ [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) - | IDENT "nchange"; what = tactic_term; with_what = tactic_term -> + | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> GrafiteAst.NChange (loc, what, with_what) ] ]; diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index f426f7126..4d8b13226 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -61,8 +61,8 @@ let refine_term ;; let refine_obj - ~coercion_db metasenv subst context uri - ~use_coercions obj _ ugraph ~localization_tbl + ~coercion_db metasenv subst context _uri + ~use_coercions obj _ _ugraph ~localization_tbl = assert (metasenv=[]); assert (subst=[]); @@ -322,8 +322,7 @@ let interpretate_term_and_interpretate_term_option with NRef.IllFormedReference _ -> CicNotationPt.fail loc "Ill formed reference") | CicNotationPt.Implicit -> NCic.Implicit `Term - | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole) -patterns not implemented *) + | CicNotationPt.UserInput -> NCic.Implicit `Hole | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) | CicNotationPt.Meta (index, subst) -> @@ -386,6 +385,15 @@ let interpretate_term_option ~context ;; +let disambiguate_path path = + let localization_tbl = NCicUntrusted.NCicHash.create 23 in + fst + (interpretate_term_and_interpretate_term_option + ~obj_context:[] ~mk_choice:(fun _ -> assert false) + ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty + ~uri:None ~is_path:true ~localization_tbl) ~context:[] path +;; + let new_flavour_of_flavour = function | `Definition -> `Definition | `MutualDefinition -> `Definition diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index d1175648a..6ae8bb036 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -50,3 +50,5 @@ val disambiguate_obj : NCic.substitution * NCic.obj) list * bool +val disambiguate_path: CicNotationPt.term -> NCic.term + diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 4e85f9bae..e039f1129 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -220,7 +220,8 @@ let _ = | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_) when NUri.string_of_uri u = "cic:/matita/tests/hole.con" -> let metasenv, ty = perforate ctx metasenv ty in - let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b + let a,_,b,_ = + NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b | t -> NCicUntrusted.map_term_fold_a (fun e ctx -> e::ctx) ctx perforate metasenv t diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index dd3485df0..3f2f43df0 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -347,16 +347,16 @@ let mk_meta ?name metasenv context ty = | `WithType ty -> let len = List.length context in let menv_entry = (n, (name, context, ty)) in - menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)), ty + menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty | `Sort -> let ty = NCic.Implicit (`Typeof n) in mk_meta (tyof name) n metasenv [] (`WithType ty) | `Type -> - let metasenv, ty, _ = + let metasenv, _, ty, _ = mk_meta (tyof name) (newmeta ()) metasenv context `Sort in mk_meta name n metasenv context (`WithType ty) | `Term -> - let metasenv, ty, _ = + let metasenv, _, ty, _ = mk_meta (tyof name) (newmeta ()) metasenv context `Type in mk_meta name n metasenv context (`WithType ty) in @@ -367,7 +367,7 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function | NCic.Prod (name,s,t) as ty -> - let metasenv1, arg,_ = + let metasenv1, _, arg,_ = mk_meta ~name:name metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 1d7b6729e..033ea1b1b 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -57,7 +57,7 @@ val mk_meta: ?name:string -> NCic.metasenv -> NCic.context -> [ `WithType of NCic.term | `Term | `Type | `Sort ] -> - NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *) + NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *) (* returns the resulting type, the metasenv and the arguments *) val saturate: diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index dd03356c4..7871d86e9 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -60,7 +60,7 @@ let check_allowed_sort_elimination hdb localise r orig = NCicPp.ppmetasenv ~subst metasenv)); match arity1 with | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) -> - let metasenv, meta, _ = + let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type in let metasenv, subst = @@ -74,7 +74,7 @@ let check_allowed_sort_elimination hdb localise r orig = aux metasenv subst ((name, C.Decl so1)::context) (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta | C.Sort _ (* , t ==?== C.Prod _ *) -> - let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in + let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in let metasenv, subst = try NCicUnification.unify hdb metasenv subst context arity2 (C.Prod ("_", ind, meta)) @@ -145,7 +145,7 @@ let rec typeof hdb NCicPp.ppterm ~subst ~metasenv ~context t))) | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0)) | C.Implicit infos -> - let metasenv,t,ty = exp_implicit metasenv context expty infos in + let metasenv,_,t,ty = exp_implicit metasenv context expty infos in metasenv, subst, t, ty | C.Meta (n,l) as t -> let ty = @@ -427,7 +427,7 @@ and eat_prods hdb let metasenv, subst, arg, ty_arg = typeof hdb ~look_for_coercion ~localise metasenv subst context arg None in - let metasenv, meta, _ = + let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv (("_",C.Decl ty_arg) :: context) `Type in diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index 3b6d163f4..b7d2b67d7 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -149,7 +149,7 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function | NCic.Prod (name,s,t) as ty -> - let metasenv1, arg,_ = + let metasenv1, _, arg,_ = NCicMetaSubst.mk_meta ~name:name metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) @@ -196,7 +196,8 @@ let look_for_hint hdb metasenv subst context t1 t2 = let rec aux () (m,l as acc) = function | NCic.Meta _ as t -> acc, t | NCic.LetIn (name,ty,bo,t) -> - let m,i,_=NCicMetaSubst.mk_meta ~name m context (`WithType ty)in + let m,_,i,_= + NCicMetaSubst.mk_meta ~name m context (`WithType ty)in let t = NCicSubstitution.subst i t in aux () (m, (i,bo)::l) t | t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 4f6a726df..0c5f5360c 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -24,7 +24,7 @@ type lowtac_status = { lstatus : LexiconEngine.status } -type lowtactic = lowtac_status * int -> lowtac_status * int list * int list +type lowtactic = lowtac_status -> int -> lowtac_status type tac_status = { gstatus : Continuationals.Stack.t; @@ -34,11 +34,17 @@ type tac_status = { type tactic = tac_status -> tac_status type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input +type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input let pp_tac_status status = prerr_endline (NCicPp.ppobj status.istatus.pstatus) ;; +let pp_lowtac_status status = + prerr_endline "--------------------------------------------"; + prerr_endline (NCicPp.ppobj status.pstatus) +;; + open Continuationals.Stack let dot_tac status = @@ -170,12 +176,16 @@ let skip_tac status = let block_tac l status = List.fold_left (fun status tac -> tac status) status l ;; - -let compare_menv ~past ~present = - List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present), - List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) + +let compare_statuses ~past ~present = + let _,_,past,_,_ = past.pstatus in + let _,_,present,_,_ = present.pstatus in + List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present), + List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) ;; + + (* Exec and distribute_tac form a retraction pair: 1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i) 2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed => @@ -190,13 +200,8 @@ let compare_menv ~past ~present = let exec tac (low_status,g) = let stack = [ [0,Open g], [], [], `NoTag ] in - let _,_,old_metasenv,_,_ = low_status.pstatus in let status = tac { gstatus = stack ; istatus = low_status } in - let _,_,metasenv,_,_ = status.istatus.pstatus in - let open_goals, closed_goals = - compare_menv ~past:old_metasenv ~present:metasenv - in - status.istatus, open_goals, closed_goals + status.istatus ;; let distribute_tac tac status = @@ -216,8 +221,9 @@ let distribute_tac tac status = match switch_of_loc loc with | Closed _ -> fail (lazy "cannot apply to a Closed goal") | Open n -> - let s, go', gc' = tac (s,n) in - s, (go @- gc') @+ go', gc @+ gc' + let sn = tac s n in + let go', gc' = compare_statuses ~past:s ~present:sn in + sn, (go @- gc') @+ go', gc @+ gc' in aux s go gc loc_tl in @@ -235,10 +241,10 @@ let distribute_tac tac status = type cic_term = NCic.conjecture type ast_term = string * int * CicNotationPt.term -type position = Ctx of NCic.context | Term of cic_term +type position = [ `Ctx of NCic.context | `Term of cic_term ] -let relocate (name,ctx,t as term) context = +let relocate context (name,ctx,t as term) = let is_prefix l1 l2 = let rec aux = function | [],[] -> true @@ -258,10 +264,10 @@ let relocate (name,ctx,t as term) context = let disambiguate (status : lowtac_status) (t : ast_term) (ty : cic_term option) (where : position) = let uri,height,metasenv,subst,obj = status.pstatus in - let context = match where with Ctx c -> c | Term (_,c,_) -> c in + let context = match where with `Ctx c -> c | `Term (_,c,_) -> c in let expty = match ty with - | None -> None | Some ty -> let _,_,x = relocate ty context in Some x + | None -> None | Some ty -> let _,_,x = relocate context ty in Some x in let metasenv, subst, lexicon_status, t = GrafiteDisambiguate.disambiguate_nterm expty @@ -271,32 +277,115 @@ 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 +let in_scope_tag = "tag:in_scope" ;; +let out_scope_tag = "tag:out_scope" ;; + +let typeof status where t = + let _,_,metasenv,subst,_ = status.pstatus in + let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in + let _,_,t = relocate ctx t in + let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in + None, ctx, ty +;; + +let unify status where a b = + let n,h,metasenv,subst,o = status.pstatus in + let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in + let _,_,a = relocate ctx a in + let _,_,b = relocate ctx b in + let metasenv, subst = + NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx a b in - let match_term m = + { status with pstatus = n,h,metasenv,subst,o } +;; + +let refine status where term expty = + let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in + let nt,_,term = relocate ctx term in + let ne, ty = + match expty with None -> None, None + | Some e -> let n,_, e = relocate ctx e in Some n, Some e + in + let name,height,metasenv,subst,obj = status.pstatus in + let db = NCicUnifHint.db () in (* XXX fixme *) + let coercion_db = NCicCoercion.db () in + let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in + let metasenv, subst, t, ty = + NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term ty + in + { status with pstatus = (name,height,metasenv,subst,obj) }, + (nt,ctx,t), (ne,ctx,ty) +;; + +let get_goal (status : lowtac_status) (g : int) = + let _,_,metasenv,_,_ = status.pstatus in + List.assoc g metasenv +;; + +let instantiate status i t = + let (goalname, context, _ as ety) = get_goal status i in + let status, (_,_,t), (_,_,ty) = refine status (`Term ety) t (Some ety) in + + let name,height,metasenv,subst,obj = status.pstatus in + let metasenv = List.filter (fun j,_ -> j <> i) metasenv in + let subst = (i, (goalname, context, t, ty)) :: subst in + { status with pstatus = (name,height,metasenv,subst,obj) } +;; + +let mk_meta status ?name where bo_or_ty = + let n,h,metasenv,subst,o = status.pstatus in + let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in + match bo_or_ty with + | `Decl ty -> + let _,_,ty = relocate ctx ty in + let metasenv, _, instance, _ = + NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) + in + let status = { status with pstatus = n,h,metasenv,subst,o } in + status, (None,ctx,instance) + | `Def bo -> + let _,_,ty = typeof status (`Ctx ctx) bo in + let metasenv, metano, instance, _ = + NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) + in + let status = { status with pstatus = n,h,metasenv,subst,o } in + let status = instantiate status metano bo in + status, (None,ctx,instance) +;; + +let select_term low_status (name,context,term) (wanted,path) = + let found status ctx t wanted = + (* we could lift wanted step-by-step *) + try true, unify status (`Ctx ctx) (None,ctx,t) wanted + with + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ -> false, status + in + let match_term status ctx (wanted : cic_term) t = let rec aux ctx status t = - let b, status = eq ctx status t m in + let b, status = found status ctx t wanted 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 + let status, (_,_,t) = + mk_meta status ~name:in_scope_tag (`Ctx ctx) (`Def (None,ctx,t)) + in + status, t else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t in - aux + aux ctx status t in let rec select status ctx pat cic = match pat, cic with + | NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) -> + let status, t = select status ctx t1 t2 in + let status, s = select status ctx s1 s2 in + let ctx = (n, NCic.Def (s2,t2)) :: ctx in + let status, b = select status ctx b1 b2 in + status, NCic.LetIn (n,t,s,b) + | NCic.Lambda (_,s1,t1), NCic.Lambda (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.Lambda (n,s,t) | 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 @@ -307,95 +396,89 @@ let select_term low_status (name,context,term) (path, matched) = List.fold_left2 (fun (status,l) x y -> let status, x = select status ctx x y in - status, l @ [x]) + status, x::l) (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 + status, NCic.Appl (List.rev l) + | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) -> + let status, t = select status ctx t1 t2 in + let status, ot = select status ctx ot1 ot2 in + let status, pl = + List.fold_left2 + (fun (status,l) x y -> + let status, x = select status ctx x y in + status, x::l) + (status,[]) pl1 pl2 + in + status, NCic.Match (u,ot,t,List.rev pl) + | NCic.Implicit `Hole, t -> + (match wanted with + | Some wanted -> + let status, wanted = disambiguate status wanted None (`Ctx ctx) in + match_term status ctx wanted t + | None -> match_term status ctx (None,ctx,t) t) + | NCic.Implicit _, t -> status, t + | _,t -> + fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[] + ~context:[] ~subst:[] pat)) 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 + let term = (name, context, term) in + mk_meta status ~name:out_scope_tag (`Ctx context) (`Def term) ;; -let return ~orig status = - let _,_,past,_,_ = orig.pstatus in - let _,_,present,_,_ = status.pstatus in - let open_goals, closed_goals = compare_menv ~past ~present in - status, open_goals, closed_goals -;; -let instantiate status i t = - let name,height,metasenv,subst,obj = status.pstatus in - let _, context, ty = List.assoc i metasenv in - let _,_,t = relocate t context in - let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in - let db = NCicUnifHint.db () in (* XXX fixme *) - let metasenv, subst = NCicUnification.unify db metasenv subst context m t in - { status with pstatus = (name,height,metasenv,subst,obj) } +let exact t status goal = + let goalty = get_goal status goal in + let status, t = disambiguate status t (Some goalty) (`Term goalty) in + instantiate status goal t ;; -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 reopen status = + let n,h,metasenv,subst,o = status.pstatus in + let subst, newm = + List.partition + (function (_,(Some tag,_,_,_)) -> tag <> in_scope_tag && tag <> out_scope_tag + | _ -> true) + subst + in + let in_m, out_m = + List.partition + (function (_,(Some tag,_,_,_)) -> tag = in_scope_tag | _ -> assert false) + newm + in + let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in + let in_m = List.map fst in_m in + let out_m = match out_m with [i] -> i | _ -> assert false in + { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m ;; -let change what (*where*) with_what (status as orig, goal) = +let change ~where ~with_what status 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) + 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, in_scope, out_scope = reopen status in + let status = List.fold_left (exact with_what) status in_scope in + + let j,(n,cctx,bo,_) = out_scope in + let _ = typeof status (`Term goalty) (n,cctx,bo) 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 subst = out_scope :: subst 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 + let status, instance = + mk_meta status ?name (`Term newgoalty) (`Decl newgoalty) in - let status, m = mkmeta name status newgoalty in - let status = instantiate status goal m in - return ~orig status + instantiate status goal instance ;; -let apply t (status,goal) = - let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in +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) @@ -405,19 +488,10 @@ let apply t (status,goal) = (goal, (name, context, t, gty)):: subst, List.filter(fun (x,_) -> x <> goal) metasenv in - let open_goals, closed_goals = - compare_menv ~past:old_metasenv ~present:metasenv in let new_pstatus = uri,height,metasenv,subst,obj in - - prerr_endline ("termine disambiguato: " ^ - NCicPp.ppterm ~context ~metasenv ~subst t); - prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv); - prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv); - prerr_endline "fine napply"; - - { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals + { lstatus = lexicon_status; pstatus = new_pstatus } ;; let apply_tac t = distribute_tac (apply t) ;; -let change_tac w ww = distribute_tac (change w ww) ;; +let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 29b7613a5..0ce7b427e 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -11,13 +11,14 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +exception Error of string lazy_t type lowtac_status = { pstatus : NCic.obj; lstatus : LexiconEngine.status } -type lowtactic = lowtac_status * int -> lowtac_status * int list * int list +type lowtactic = lowtac_status -> int -> lowtac_status type tac_status = { gstatus : Continuationals.Stack.t; @@ -27,6 +28,7 @@ type tac_status = { type tactic = tac_status -> tac_status type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input +type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input val dot_tac: tactic val branch_tac: tactic @@ -42,7 +44,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 change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic val pp_tac_status: tac_status -> unit -- 2.39.2