(* $Id: destructTactic.ml 9774 2009-05-15 19:37:08Z sacerdot $ *)
open NTacStatus
+open Continuationals.Stack
-let debug = true
+let debug = false
let pp =
if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
NTactics.intro_tac "Deq";
NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern;
NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern]
- @ dbranches it leftno @
+ @ dbranches it leftno @
[NTactics.shift_tac;
- NTactics.intro_tac "discriminate";
- NTactics.apply_tac ("",0,mk_appl [mk_id "discriminate";
+ NTactics.intro_tac "#discriminate";
+ NTactics.apply_tac ("",0,mk_appl [mk_id "#discriminate";
CicNotationPt.Implicit `JustOne;
CicNotationPt.Implicit `JustOne; mk_id eq_name ]);
- NTactics.reduce_tac ~reduction:(`Normalize true)
- ~where:default_pattern;
- NTactics.clear_tac ["discriminate"];
+ NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern;
+ NTactics.clear_tac ["#discriminate"];
NTactics.merge_tac]
) status
;;
let var = match var with
| NCic.Rel i -> i
| _ -> assert false in
- let names_to_gen, indices_to_gen =
+ let names_to_gen, _ =
cascade_select_in_ctx ~subst:(get_subst status) context (var+cur_eq) in
- let moved_indices = List.fold_left
- (fun acc x -> if x > cur_eq then acc+1 else acc) 0 indices_to_gen in
let gen_tac x =
NTactics.generalize_tac
~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
NTactics.rewrite_tac ~dir
~what:("",0,mk_id eq_name) ~where:default_pattern;
NTactics.reduce_tac ~reduction:(`Normalize true)
- ~where:default_pattern]@
- (List.map NTactics.intro_tac (List.rev names_to_gen))) status,
- (List.length context - cur_eq + 1 - moved_indices)
+ ~where:default_pattern;
+ NTactics.clear_tac [eq_name]]@
+ (List.map NTactics.intro_tac (List.rev names_to_gen))) status
;;
-let get_ctx status =
- let ref_ctx = ref [] in
- let status = NTactics.distribute_tac
- (fun st goal ->
- let ctx = ctx_of (get_goalty st goal) in
- ref_ctx := ctx; st) status in
- !ref_ctx
+let get_ctx st goal =
+ ctx_of (get_goalty st goal)
;;
-let rec select_eq ctx i status acc =
- try
- match (List.nth ctx (List.length ctx - i - 1)) with
- | n, (NCic.Decl s | NCic.Def (s,_)) ->
- (let _,ctx_s = HExtlib.split_nth (List.length ctx - i) ctx in
- let status, s = NTacStatus.whd status ctx_s (mk_cic_term ctx_s s) in
- let status, s = term_of_cic_term status s ctx_s in
- pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_s ~subst:[] ~metasenv:[] s)));
- if (List.for_all (fun x -> x <> n) acc) then
- match s with
- | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;_;_] ->
- if NUri.name_of_uri u = "eq" then status, Some (List.length ctx - i)
- else select_eq ctx (i+1) status acc
- | _ -> select_eq ctx (i+1) status acc
- else select_eq ctx (i+1) status acc)
- with Failure _ | Invalid_argument _ -> status, None
+(* = select + classify *)
+let select_eq ctx acc status goal =
+ let classify ~subst ctx' l r =
+ (* FIXME: metasenv *)
+ if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r
+ then status, `Identity
+ else status, (match hd_of_term l, hd_of_term r with
+ | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref),
+ NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) ->
+ if ki != kj then `Discriminate (0,true)
+ else
+ let rit = NReference.mk_indty true kref in
+ let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in
+ let it = List.nth its itno in
+ let newprods = (nargs it nleft (ki-1)) + 1 in
+ `Discriminate (newprods, false)
+ | NCic.Rel j, _
+ when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r ->
+ `Subst `LeftToRight
+ | _, NCic.Rel j
+ when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l ->
+ `Subst `RightToLeft
+ | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle
+ | _ -> `Blob) in
+ let rec aux i =
+ try
+ let index = List.length ctx - i in
+ match (List.nth ctx (index - 1)) with
+ | n, (NCic.Decl ty | NCic.Def (ty,_)) ->
+ (let _,ctx_ty = HExtlib.split_nth index ctx in
+ let status, ty = NTacStatus.whd status ctx_ty (mk_cic_term ctx_ty ty) in
+ let status, ty = term_of_cic_term status ty ctx_ty in
+ pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_ty ~subst:[] ~metasenv:[] ty)));
+ match ty with
+ | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r] when NUri.name_of_uri u = "eq" ->
+ (let status, kind = classify ~subst:(get_subst status) ctx_ty l r in
+ match kind with
+ | `Identity ->
+ let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+ if NCicTypeChecker.does_not_occur ~subst:(get_subst status) ctx (index - 1) index goalty
+ then status, Some (List.length ctx - i), kind
+ else aux (i+1)
+ | `Cycle | `Blob -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
+ | _ ->
+ if (List.for_all (fun x -> x <> n) acc) then
+ status, Some (List.length ctx - i), kind
+ else aux (i+1))
+ | _ -> aux (i+1))
+ with Failure _ | Invalid_argument _ -> status, None, `Blob
+ in aux 0
;;
-let classify ~subst ctx i status =
- let _, (NCic.Decl s | NCic.Def (s,_)) = List.nth ctx (i-1) in
- let _,ctx' = HExtlib.split_nth i ctx in
- let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
- let status, s = term_of_cic_term status s ctx' in
- match s with
- | NCic.Appl [_;_;l;r] ->
- (* FIXME: metasenv *)
- if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r
- then status, `Identity
- else status, (match hd_of_term l, hd_of_term r with
- | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref),
- NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) ->
- if ki != kj then `Discriminate (0,true)
- else
- let rit = NReference.mk_indty true kref in
- let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in
- let it = List.nth its itno in
- let newprods = (nargs it nleft (ki-1)) + 1 in
- `Discriminate (newprods, false)
- | NCic.Rel j, _
- when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r ->
- `Subst `LeftToRight
- | _, NCic.Rel j
- when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l ->
- `Subst `RightToLeft
- | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle
- | _ -> `Blob)
- | _ -> raise (Failure "classify")
-;;
-
-let rec destruct_tac0 nprods i status acc =
- let ctx = get_ctx status in
+let rec destruct_tac0 nprods acc status goal =
+ let ctx = get_ctx status goal in
let subst = get_subst status in
- let status, selection = select_eq ctx i status acc in
- match selection with
- | None ->
- pp (lazy (Printf.sprintf "destruct: nprods is %d, i is %d, no selection, context is %s" nprods i (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
+ let get_newgoal os ns ogoal =
+ let go, gc = NTactics.compare_statuses ~past:os ~present:ns in
+ let go' = ([ogoal] @- gc) @+ go in
+ match go' with [] -> assert false | g::_ -> g
+ in
+ let status, selection, kind = select_eq ctx acc status goal in
+ pp (lazy ("destruct: acc is " ^ String.concat "," acc ));
+ match selection, kind with
+ | None, _ ->
+ pp (lazy (Printf.sprintf "destruct: nprods is %d, no selection, context is %s" nprods (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
if nprods > 0 then
- let status' = NTactics.intro_tac (mk_fresh_name ctx 'e' 0) status in
- destruct_tac0 (nprods-1) (List.length ctx) status' acc
+ let status' = NTactics.exec (NTactics.intro_tac (mk_fresh_name ctx 'e' 0)) status goal in
+ destruct_tac0 (nprods-1) acc status' (get_newgoal status status' goal)
else
status
- | Some cur_eq -> pp (lazy (Printf.sprintf
- "destruct: nprods is %d, i is %d, selection is %s, context is %s"
- nprods i (name_of_rel ~context:ctx cur_eq) (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
- match classify ~subst ctx cur_eq status with
- | status,`Discriminate (newprods,conflict) ->
- let status' = discriminate_tac ~context:ctx cur_eq status in
- if conflict then status'
- else destruct_tac0 (nprods+newprods) (List.length ctx - cur_eq + 1)
- status' (name_of_rel ~context:ctx cur_eq::acc)
- | status, `Subst dir ->
- let status', next_i = subst_tac ~context:ctx ~dir cur_eq status in
- destruct_tac0 nprods next_i status' acc
- | status, `Identity
- | status, `Cycle (* TODO *)
- | status, `Blob ->
- destruct_tac0 nprods (cur_eq+1) status acc
+ | Some cur_eq, `Discriminate (newprods,conflict) ->
+ pp (lazy (Printf.sprintf "destruct: discriminate - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
+ let status' = NTactics.exec (discriminate_tac ~context:ctx cur_eq) status goal in
+ if conflict then status'
+ else destruct_tac0 (nprods+newprods)
+ (name_of_rel ~context:ctx cur_eq::acc) status' (get_newgoal status status' goal)
+ | Some cur_eq, `Subst dir ->
+ pp (lazy (Printf.sprintf "destruct: subst - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
+ let status' = NTactics.exec (subst_tac ~context:ctx ~dir cur_eq) status goal in
+ pp (lazy (Printf.sprintf " ctx after subst = %s" (NCicPp.ppcontext ~metasenv:[] ~subst (get_ctx status' (get_newgoal status status' goal)))));
+ let eq_name,_ = List.nth ctx (cur_eq-1) in
+ destruct_tac0 nprods (List.filter (fun x -> x <> eq_name) acc) status' (get_newgoal status status' goal)
+ | Some cur_eq, `Identity ->
+ pp (lazy (Printf.sprintf "destruct: identity - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
+ let eq_name,_ = List.nth ctx (cur_eq-1) in
+ let status' = NTactics.exec (NTactics.clear_tac [eq_name]) status goal in
+ destruct_tac0 nprods (List.filter (fun x -> x <> eq_name) acc) status' (get_newgoal status status' goal)
+ | Some cur_eq, `Cycle -> (* TODO, should never happen *)
+ pp (lazy (Printf.sprintf "destruct: cycle - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
+ assert false
+ | Some cur_eq, `Blob ->
+ pp (lazy (Printf.sprintf "destruct: blob - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx)));
+ assert false
;;
-let destruct_tac status = destruct_tac0 0 0 status [];;
+let destruct_tac s = NTactics.distribute_tac (destruct_tac0 0 []) s;;
projects / helm.git / commitdiff