open Continuationals.Stack
open NTacStatus
-module Ast = CicNotationPt
+module Ast = NotationPt
let id_tac status = status ;;
let print_tac print_status message status =
let gstatus =
match status#stack with
| [] -> assert false
- | ([], _, [], _) :: _ as stack ->
+ | ([], _, [], _, _) :: _ as stack ->
(* backward compatibility: do-nothing-dot *)
stack
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
match filter_open g, k with
| loc :: loc_tl, _ ->
- (([ loc ], t, loc_tl @+ k, tag) :: s)
+ (([ loc ], t, loc_tl @+ k, tag, p) :: s)
| [], loc :: k ->
assert (is_open loc);
- (([ loc ], t, k, tag) :: s)
+ (([ loc ], t, k, tag, p) :: s)
| _ -> fail (lazy "can't use \".\" here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
match init_pos g with (* TODO *)
| [] -> fail (lazy "empty goals")
- | [_] when (not force) -> fail (lazy "too few goals to branch")
+ | [_] when (not force) -> fail (lazy "too few goals to branch")
| loc :: loc_tl ->
- ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
+ ([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag, p) :: s
in
status#set_stack gstatus
;;
let shift_tac status =
let gstatus =
match status#stack with
- | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+ | (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->
(match g' with
| [] -> fail (lazy "no more goals to shift")
| loc :: loc_tl ->
- (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
- :: (loc_tl, t', k', tag) :: s))
+ (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
+ :: (loc_tl, t', k', tag, p') :: s))
| _ -> fail (lazy "can't shift goals here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
- ((l_js, t , [],`BranchTag)
- :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ ((l_js, t , [],`BranchTag, p)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
| _ -> fail (lazy "can't use relative positioning here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
let l_js =
List.filter
match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
attrs,_,_ when List.mem (`Name lab) attrs -> true
| _ -> false) ([loc] @+ g') in
- ((l_js, t , [],`BranchTag)
- :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ ((l_js, t , [],`BranchTag, p)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
| _ -> fail (lazy "can't use relative positioning here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+ | ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
- (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
+ (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: s)
| _ -> fail (lazy "can't use wildcard here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
- ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+ | (g, t, k,`BranchTag, _) :: (g', t', k', tag, p) :: s ->
+ ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: s)
| _ -> fail (lazy "can't merge goals here")
in
status#set_stack gstatus
if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
fail (lazy (sprintf "goal %d not found (or closed)" g)))
gs;
- (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
+ (zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s
in
status#set_stack gstatus
;;
let gstatus =
match status#stack with
| [] -> assert false
- | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s
+ | (g, [], [], `FocusTag, _) :: s when filter_open g = [] -> s
| _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^
Continuationals.Stack.pp s))
in
let gstatus =
match status#stack with
| [] -> assert false
- | (gl, t, k, tag) :: s ->
+ | (gl, t, k, tag, p) :: s ->
let gl = List.map switch_of_loc gl in
if List.exists (function Open _ -> true | Closed _ -> false) gl then
fail (lazy "cannot skip an open goal")
else
- ([],t,k,tag) :: s
+ ([],t,k,tag,p) :: s
in
status#set_stack gstatus
;;
(e.g. the tactic could perform a global analysis of the set of goals)
*)
+(* CSC: potential bug here: the new methods still use the instance variables
+ of the old status and not the instance variables of the new one *)
+let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStatus.status =
+ let o =
+ object
+ inherit ['b] NTacStatus.status status#obj stack
+ method ppterm = status#ppterm
+ method ppcontext = status#ppcontext
+ method ppsubst = status#ppsubst
+ method ppobj = status#ppobj
+ method ppmetasenv = status#ppmetasenv
+ end
+ in
+ o#set_pstatus status
+;;
+
let exec tac (low_status : #lowtac_status) g =
- let stack = [ [0,Open g], [], [], `NoTag ] in
- let status =
- (new NTacStatus.status low_status#obj stack)#set_estatus low_status
- in
+ let stack = [ [0,Open g], [], [], `NoTag, [] ] in
+ let status = change_stack_type low_status stack in
let status = tac status in
- (low_status#set_estatus status)#set_obj status#obj
+ (low_status#set_pstatus status)#set_obj status#obj
;;
let distribute_tac tac (status : #tac_status) =
match status#stack with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
debug_print (lazy ("context length " ^string_of_int (List.length g)));
let rec aux s go gc =
function
in
aux s go gc loc_tl
in
- let s0 = (new NTacStatus.status status#obj ())#set_estatus status in
+ let s0 = change_stack_type status () in
let s0, go0, gc0 = s0, [], [] in
let sn, gon, gcn = aux s0 go0 gc0 g in
debug_print (lazy ("opened: "
debug_print (lazy ("closed: "
^ String.concat " " (List.map string_of_int gcn)));
let stack =
- (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+ (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s
in
- ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
+ ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
;;
-let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
+let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
let repeat_tac t s =
let rec repeat t (status : #tac_status as 'a) : 'a =
let try_tac tac status =
+ let try_tac status =
try
tac status
with NTacStatus.Error _ ->
status
+ in
+ atomic_tac try_tac status
;;
let first_tac tacl status =
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | (hd,_) :: tl when hd = name -> acc
+ | (hd,_) :: _ when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
names
in
let n,h,metasenv,subst,o = status#obj in
- let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in
+ let metasenv,subst,_,_ = NCicMetaSubst.restrict status metasenv subst goal js in
status#set_obj (n,h,metasenv,subst,o))
;;
else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
;;
-let select0_tac ~where:(wanted,hyps,where) ~job =
+let select0_tac ~where ~job =
let found, postprocess =
match job with
| `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
| `ChangeWith f -> f,(fun s t -> s, t)
in
distribute_tac (fun status goal ->
+ let wanted,hyps,where =
+ GrafiteDisambiguate.disambiguate_npattern status where in
let goalty = get_goalty status goal in
let path =
match where with None -> NCic.Implicit `Term | Some where -> where
let status, instance =
mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
in
- instantiate status goal instance)
+ instantiate ~refine:false status goal instance)
;;
-let select_tac ~where ~job 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
+let select_tac ~where:((txt,txtlen,(wanted,hyps,path)) as where) ~job
+ move_down_hyps
+=
if not move_down_hyps then
- select0_tac ~where:(wanted,hyps,Some path) ~job
+ select0_tac ~where ~job
else
let path =
List.fold_left
- (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
- path (List.rev hyps)
+ (fun path (name,ty) ->
+ NotationPt.Binder (`Forall, (NotationPt.Ident (name,None),Some ty),path))
+ (match path with Some x -> x | None -> NotationPt.UserInput) (List.rev hyps)
in
block_tac [
generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
- select0_tac ~where:(wanted,[],Some path) ~job;
+ select0_tac ~where:(txt,txtlen,(wanted,[],Some path)) ~job;
clear_tac (List.map fst hyps) ]
;;
_,_,(None,_,_) -> fail (lazy "No term to generalize")
| txt,txtlen,(Some what,_,_) ->
let status, what =
- disambiguate status (ctx_of goalty) (txt,txtlen,what) None
+ disambiguate status (ctx_of goalty) (txt,txtlen,what) `XTNone
in
status,what,[]
)
whd status
?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
in
- let where = GrafiteDisambiguate.disambiguate_npattern where in
- select0_tac ~where ~job:(`ChangeWith change)
+ select_tac ~where ~job:(`ChangeWith change) false
;;
let change_tac ~where ~with_what =
let change status t =
- let status, ww = disambiguate status (ctx_of t) with_what None in
+(* FG: `XTSort could be used when we change the whole goal *)
+ let status, ww = disambiguate status (ctx_of t) with_what `XTNone in
let status = unify status (ctx_of t) t ww in
status, ww
in
- let where = GrafiteDisambiguate.disambiguate_npattern where in
- select0_tac ~where ~job:(`ChangeWith change)
+ select_tac ~where ~job:(`ChangeWith change) false
;;
let letin_tac ~where ~what:(_,_,w) name =
rightno: int;
leftno: int;
consno: int;
- lefts: NCic.term list;
- rights: NCic.term list;
reference: NReference.reference;
+ cl: NCic.constructor list;
}
;;
let ref_of_indtyinfo iti = iti.reference;;
let analyze_indty_tac ~what indtyref =
- distribute_tac (fun status goal ->
+ distribute_tac (fun (status as orig_status) goal ->
let goalty = get_goalty status goal in
- let status, what = disambiguate status (ctx_of goalty) what None in
+ let status, what = disambiguate status (ctx_of goalty) what `XTInd in
let status, ty_what = typeof status (ctx_of what) what in
- let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
+ let _status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in
let leftno = List.length lefts in
let rightno = List.length rights in
indtyref := Some {
- rightno = rightno; leftno = leftno; consno = consno;
- lefts = lefts; rights = rights; reference = r;
+ rightno = rightno; leftno = leftno; consno = consno; reference = r;
+ cl = cl;
};
- exec id_tac status goal)
+ exec id_tac orig_status goal)
;;
let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status,sort = typeof status (ctx_of goalty) goalty in
let status, sort = fix_sorts status sort in
- let status, sort = term_of_cic_term status sort (ctx_of goalty) in
+ let ctx = ctx_of goalty in
+ let status, sort = whd status (ctx_of sort) sort in
+ let status, sort = term_of_cic_term status sort ctx in
sortref := sort;
status)
;;
+let pp_ref reference =
+ let NReference.Ref (uri,spec) = reference in
+ let nstring = NUri.string_of_uri uri in
+ (*"Shareno: " ^ (string_of_int nuri) ^*) "Uri: " ^ nstring ^
+ (match spec with
+ | NReference.Decl -> "Decl"
+ | NReference.Def n -> "Def " ^ (string_of_int n)
+ | NReference.Fix (n1,n2,n3) -> "Fix " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* fixno, recparamno, height *)
+ | NReference.CoFix n -> "CoFix " ^ (string_of_int n)
+ | NReference.Ind (b,n1,n2) -> "Ind " ^ (string_of_bool b) ^ " " ^ (string_of_int n1) ^ " " ^ (string_of_int n2)(* inductive, indtyno, leftno *)
+ | NReference.Con (n1,n2,n3) -> "Con " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* indtyno, constrno, leftno *)
+ ) ;;
+
+let pp_cl cl =
+ let rec pp_aux acc =
+ match acc with
+ | [] -> ""
+ | (_,consname,_) :: tl -> consname ^ ", " ^ pp_aux tl
+ in
+ pp_aux cl
+;;
+
+let pp_indtyinfo ity = "leftno: " ^ (string_of_int ity.leftno) ^ ", consno: " ^ (string_of_int
+ ity.consno) ^ ", rightno: " ^
+ (string_of_int ity.rightno) ^ ", reference: " ^ (pp_ref ity.reference) ^ ",
+ cl: " ^ (pp_cl ity.cl);;
+
let elim_tac ~what:(txt,len,what) ~where =
let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
let indtyinfo = ref None in
`LeftToRight -> "eq" ^ suffix ^ "_r"
| `RightToLeft -> "eq" ^ suffix
in
+ let what = Ast.Appl [what; Ast.Implicit `Vector] in
block_tac
[ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac
let cases ~what status goal =
let gty = get_goalty status goal in
- let status, what = disambiguate status (ctx_of gty) what None in
+ let status, what = disambiguate status (ctx_of gty) what `XTInd in
let status, ty = typeof status (ctx_of what) what in
- let status, (ref, consno, _, _) = analyse_indty status ty in
+ let status, (ref, consno, _, _,_) = analyse_indty status ty in
let status, what = term_of_cic_term status what (ctx_of gty) in
let t =
NCic.Match (ref,NCic.Implicit `Term, what,
HExtlib.mk_list (NCic.Implicit `Term) consno)
- in
+ in
instantiate status goal (mk_cic_term (ctx_of gty) t)
;;
;;
let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
- if num < 1 then fail (lazy "constructor numbers begin with 1");
let gty = get_goalty status goal in
- let status, (r,_,_,_) = analyse_indty status gty in
+ let status, (r,consno,_,_,_) = analyse_indty status gty in
+ if num < 1 || num > consno then fail (lazy "Non existant constructor");
let ref = NReference.mk_constructor num r in
let t =
if args = [] then Ast.NRef ref else
let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
let gty = get_goalty status goal in
let eq status ctx t1 t2 =
- let status,t1 = disambiguate status ctx t1 None in
+ let status,t1 = disambiguate status ctx t1 `XTSort 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);
+ prerr_endline ("COMPARING: " ^ status#ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ status#ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
assert (t1=t2);
status
in
let assert_tac seqs status =
match status#stack with
| [] -> assert false
- | (g,_,_,_) :: s ->
+ | (g,_,_,_,_) :: _s ->
assert (List.length g = List.length seqs);
(match seqs with
[] -> id_tac
in
let eliminator =
let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ; Ast.Implicit `Vector]
in
exact_tac ("",0,eliminator) status) ])
;;
projects / helm.git / blobdiff