From 463dc6672bcdc0eb63e1638fa75212387d54179a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Apr 2009 13:15:49 +0000 Subject: [PATCH] Analizyng the inductive type of the eliminated term and the sort of the goals are performed by tactics having a side-effect. This allows to write tactics like elim and cases as lists of tactics blocked together. --- .../components/ng_tactics/nTacStatus.ml | 11 +- .../components/ng_tactics/nTacStatus.mli | 2 +- .../components/ng_tactics/nTactics.ml | 145 ++++++++++++------ 3 files changed, 108 insertions(+), 50 deletions(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 6240c7430..9fc008efa 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -162,7 +162,14 @@ let mk_meta status ?name ctx bo_or_ty = status, (None,ctx,instance) ;; -let select_term low_status (name,context,term) (wanted,path) = +(* the following unification problem will be driven by + * select s argsno t pattern + * + * ? args = t + * + * where argsn = length args and the pattern matches t + *) +let select_term low_status argsno (name,context,term) (wanted,path) = let found status ctx t wanted = (* we could lift wanted step-by-step *) try true, unify status ctx (None, ctx, t) wanted @@ -242,7 +249,7 @@ let select_term low_status (name,context,term) (wanted,path) = in let status, term = select low_status context path term in let term = (name, context, term) in - mk_meta status ~name:(NCicMetaSubst.out_scope_tag 1) context (`Def term) + mk_meta status ~name:(NCicMetaSubst.out_scope_tag argsno) context (`Def term) ;; let analyse_indty status ty = diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 6c7d69823..2a065bc5f 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -61,7 +61,7 @@ val mk_meta: val instantiate: lowtac_status -> int -> cic_term -> lowtac_status val select_term: - lowtac_status -> cic_term -> ast_term option * NCic.term -> + lowtac_status -> int -> cic_term -> ast_term option * NCic.term -> lowtac_status * cic_term val pp_tac_status: tac_status -> unit diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index d54f97145..b34a3a34d 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -20,7 +20,8 @@ open Continuationals.Stack open NTacStatus module Ast = CicNotationPt -let id_tac status = status;; +let id_tac status = status ;; +let print_tac message status = prerr_endline message; status ;; let dot_tac status = let new_gstatus = @@ -155,8 +156,13 @@ let block_tac l status = 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) + let closed = + List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) + in + let opened = + List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present) + in + opened, closed ;; @@ -167,6 +173,7 @@ let compare_statuses ~past ~present = distribute_tac (exec tac) [s]::G = (G1@...Gn)::G' 3) tac G = distribute_tac (exec tac) G if tac = distribute_tac lowtac + 4) atomic_tac t === distribute_tac (exec t) Note that executing an high tactic on a set of goals may be stronger than executing the same tactic on those goals, but once at a time @@ -186,7 +193,9 @@ let distribute_tac tac status = debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function - | [] -> s, go, gc + | [] -> + debug_print (lazy "no selected goals"); + s, go, gc | loc :: loc_tl -> debug_print (lazy "inner eval tactical"); let s, go, gc = @@ -198,7 +207,7 @@ let distribute_tac tac status = | Open n -> let sn = tac s n in let go', gc' = compare_statuses ~past:s ~present:sn in - sn, (go @- gc') @+ go', gc @+ gc' + sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc' in aux s go gc loc_tl in @@ -214,6 +223,8 @@ let distribute_tac tac status = { gstatus = stack; istatus = sn } ;; +let atomic_tac htac = distribute_tac (exec htac) ;; + let exact t status goal = let goalty = get_goalty status goal in let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in @@ -255,26 +266,25 @@ let generalize0_tac args = else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args)) ;; -let select ~where:(wanted,_,where) status goal = - let goalty = get_goalty status goal 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 (ctx_of newgoalty) (`Decl newgoalty) - in - instantiate status goal instance +let select0_tac ~where:(wanted,_,where) ~argsno = + distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let path = + match where with None -> NCic.Implicit `Term | Some where -> where + in + let status, newgoalty = select_term status argsno goalty (wanted,path) in + let status, instance = + mk_meta status (ctx_of newgoalty) (`Decl newgoalty) + in + instantiate status goal instance) ;; -let select0_tac ~where = distribute_tac (select ~where) ;; - -let select_tac ~where move_down_hyps = +let select_tac ~where ~argsno move_down_hyps = let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in let path = match where with None -> NCic.Implicit `Term | Some where -> where in if not move_down_hyps then - select0_tac ~where:(wanted,hyps,Some path) + select0_tac ~where:(wanted,hyps,Some path) ~argsno else let path = List.fold_left @@ -283,7 +293,7 @@ let select_tac ~where move_down_hyps = in block_tac [ generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps); - select0_tac ~where:(wanted,[],Some path); + select0_tac ~where:(wanted,[],Some path) ~argsno; clear_tac (List.map fst hyps) ] ;; @@ -322,7 +332,7 @@ let change ~where ~with_what status goal = 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, newgoalty = select_term status 1 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 @@ -344,31 +354,67 @@ 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 true; - distribute_tac (fun status goal -> - let goalty = get_goalty status goal in - let goalsort = typeof status (ctx_of goalty) goalty in +type indtyinfo = { + rightno: int; + leftno: int; + consno: int; + lefts: NCic.term list; + rights: NCic.term list; + reference: NReference.reference; + } +;; + +let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let status, what = disambiguate status what None (ctx_of goalty) in + let ty_what = typeof status (ctx_of what) what in + let r,consno,lefts,rights = analyse_indty status ty_what in + let leftno = List.length rights in + let rightno = List.length rights in + indtyref := Some { + rightno = rightno; leftno = leftno; consno = consno; + lefts = lefts; rights = rights; reference = r; + }; + prerr_endline "FO"; + exec id_tac status goal) +;; + +let force f s = Lazy.force f s;; + +let elim_tac ~what ~where = + let indtyinfo = ref None in + let sort = ref None in + let compute_goal_sort_tac = distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let goalsort = typeof status (ctx_of goalty) goalty in + prerr_endline "XXXXXXXX"; + sort := Some goalsort; + exec id_tac status goal) + in + atomic_tac (block_tac [ + analyze_indty_tac ~what indtyinfo; + force (lazy (select_tac + ~where ~argsno:((HExtlib.unopt !indtyinfo).rightno+1) true)); + print_tac "CIAO"; + compute_goal_sort_tac; + print_tac "CIAO2"; + force (lazy ( + let sort = HExtlib.unopt !sort in + let ity = HExtlib.unopt !indtyinfo in + let NReference.Ref (uri, _) = ity.reference in + let name = NUri.name_of_uri uri ^ + match term_of_cic_term sort (ctx_of sort) with + | NCic.Sort NCic.Prop -> "_ind" + | NCic.Sort _ -> "_rect" + | _ -> assert false + in + let holes = + HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in + let eliminator = let _,_,w = what in - let status, what = - disambiguate status what None (ctx_of goalty) in - let ty_what = typeof status (ctx_of what) what in - let NReference.Ref (uri,_),consno,lefts,rights = - analyse_indty status ty_what in - let name = NUri.name_of_uri uri ^ - match term_of_cic_term goalsort (ctx_of goalsort) with - NCic.Sort NCic.Prop -> "_ind" - | NCic.Sort _ -> "_rect" - | _ -> assert false in - let leftno = List.length rights in - let rightno = List.length rights in - let holes=HExtlib.mk_list Ast.Implicit (leftno + 1 + consno + rightno) in - let eliminator = - Ast.Appl(Ast.Ident(name,None)::holes @ [ w ]) - in - exec (apply_tac ("",0,eliminator)) status goal) ] - status + Ast.Appl(Ast.Ident(name,None)::holes @ [ w ]) + in + exact_tac ("",0,eliminator))) ]) ;; let rewrite_tac ~dir ~what:(_,_,what) ~where = @@ -376,7 +422,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where = match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind" in block_tac - [ select_tac ~where true; + [ select_tac ~where ~argsno:2 true; exact_tac ("",0, Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @ @@ -406,7 +452,12 @@ let cases ~what status goal = ;; let cases_tac ~what ~where = - block_tac [ select_tac ~where true ; distribute_tac (cases ~what) ] + let indtyinfo = ref None in + atomic_tac + (block_tac [ + analyze_indty_tac ~what indtyinfo; + select_tac ~where ~argsno:((HExtlib.unopt !indtyinfo).rightno+1) true; + distribute_tac (cases ~what) ]) ;; let case1_tac name = -- 2.39.2