--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: destructTactic.ml 9774 2009-05-15 19:37:08Z sacerdot $ *)
+
+open NTacStatus
+
+let debug = true
+let pp =
+ if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
+
+let fresh_name =
+ let i = ref 0 in
+ function () ->
+ incr i;
+ "z" ^ string_of_int !i
+;;
+
+let mk_id id =
+ let id = if id = "_" then fresh_name () else id in
+ CicNotationPt.Ident (id,None)
+;;
+
+let mk_appl =
+ function
+ [] -> assert false
+ | [x] -> x
+ | l -> CicNotationPt.Appl l
+;;
+
+let rec iter f n acc =
+ if n < 0 then acc
+ else iter f (n-1) (f n acc)
+;;
+
+let subst_metasenv_and_fix_names status =
+ let u,h,metasenv, subst,o = status#obj in
+ let o =
+ NCicUntrusted.map_obj_kind ~skip_body:true
+ (NCicUntrusted.apply_subst subst []) o
+ in
+ status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
+;;
+
+(* input: nome della variabile riscritta
+ * output: lista dei nomi delle variabili il cui tipo dipende dall'input *)
+let cascade_select_in_ctx ~subst ctx iname =
+ prerr_endline "C";
+ let lctx, rctx = HExtlib.split_nth (iname - 1) ctx in
+ let lctx = List.rev lctx in
+ let rec rm_last = function
+ [] | [_] -> []
+ | hd::tl -> hd::(rm_last tl)
+ in
+
+ let indices,_ = List.fold_left
+ (fun (acc,context) item ->
+ prerr_endline "C2";
+ match item with
+ | n,(NCic.Decl s | NCic.Def (s,_))
+ when not (List.for_all (fun x -> NCicTypeChecker.does_not_occur ~subst context (x-1) x s) acc) ->
+ List.iter (fun m -> prerr_endline ("acc has " ^ (string_of_int m))) acc;
+ prerr_endline ("acc occurs in the type of " ^ n);
+ (1::List.map ((+) 1) acc, item::context)
+ | _ -> (List.map ((+) 1) acc, item::context))
+ ([1], rctx) lctx in
+ prerr_endline "C3:";
+ List.iter (fun n -> prerr_endline (string_of_int n)) indices;
+ let indices = match rm_last indices with
+ | [] -> []
+ | _::tl -> tl in
+ let res = List.map (fun n -> let s,_ = List.nth ctx (n-1) in s) indices in
+ prerr_endline "C4:";
+ List.iter (fun n -> prerr_endline n) res;
+ prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst ctx);
+ res, indices
+;;
+
+let rec mk_fresh_name ctx firstch n =
+ let candidate = (String.make 1 firstch) ^ (string_of_int n) in
+ if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
+ else mk_fresh_name ctx firstch (n+1)
+;;
+
+let arg_list nleft t =
+ let rec drop_prods n t =
+ if n <= 0 then t
+ else match t with
+ | NCic.Prod (_,_,ta) -> drop_prods (n-1) ta
+ | _ -> raise (Failure "drop_prods")
+ in
+ let rec aux = function
+ | NCic.Prod (_,so,ta) -> so::aux ta
+ | _ -> []
+ in aux (drop_prods nleft t)
+;;
+
+let nargs it nleft consno =
+ prerr_endline (Printf.sprintf "nargs %d %d" nleft consno);
+ let _,indname,_,cl = it in
+ let _,_,t_k = List.nth cl consno in
+ List.length (arg_list nleft t_k) ;;
+
+let default_pattern = "",0,(None,[],Some CicNotationPt.UserInput);;
+
+(* returns the discrimination = injection+contradiction principle *)
+(* FIXME: mi riservo di considerare tipi con parametri sx alla fine *)
+
+let mk_discriminator it status =
+ let nleft = 0 in
+ let _,indname,_,cl = it in
+
+
+ let mk_eq tys ts us es n =
+ (* eqty = Tn u0 e0...un-1 en-1 *)
+ let eqty = mk_appl
+ (List.nth tys n :: iter (fun i acc ->
+ List.nth us i::
+ List.nth es i:: acc)
+ (n-1) []) in
+
+ (* params = [T0;t0;...;Tn;tn;u0;e0;un-1;en-1] *)
+ let params = iter (fun i acc ->
+ List.nth tys i ::
+ List.nth ts i :: acc) n
+ (iter (fun i acc ->
+ List.nth us i::
+ List.nth es i:: acc) (n-1) []) in
+ mk_appl [mk_id "eq"; eqty;
+ mk_appl (mk_id ("R" ^ string_of_int n) :: params);
+ List.nth us n]
+ in
+
+ let kname it j =
+ let _,_,_,cl = it in
+ let _,name,_ = List.nth cl j in
+ name
+ in
+
+ let branch i j ts us =
+ let nargs = nargs it nleft i in
+ let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in
+ let tys = List.map
+ (fun x -> CicNotationPt.Implicit (`Tagged ("T" ^ (string_of_int x))))
+ (HExtlib.list_seq 0 nargs) in
+ let tys = tys @
+ [iter (fun i acc ->
+ CicNotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
+ CicNotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
+ acc))) (nargs-1)
+ (mk_appl [mk_id "eq"; CicNotationPt.Implicit `JustOne;
+ mk_appl (mk_id (kname it i)::
+ List.map (fun x -> mk_id ("x" ^string_of_int x))
+ (HExtlib.list_seq 0 (List.length ts)));
+ mk_appl (mk_id (kname it j)::us)])]
+ in
+ CicNotationPt.Binder (`Lambda, (mk_id "e",
+ Some (mk_appl
+ [mk_id "eq";
+ CicNotationPt.Implicit `JustOne;
+ mk_appl (mk_id (kname it i)::ts);
+ mk_appl (mk_id (kname it j)::us)])),
+ let ts = ts @ [mk_id "e"] in
+ let refl2 = mk_appl
+ [mk_id "refl";
+ CicNotationPt.Implicit `JustOne;
+ mk_appl (mk_id (kname it j)::us)] in
+ let us = us @ [refl2] in
+ CicNotationPt.Binder (`Forall, (mk_id "P", Some (CicNotationPt.Sort (`NType "1") )),
+ if i = j then
+ CicNotationPt.Binder (`Forall, (mk_id "_",
+ Some (iter (fun i acc ->
+ CicNotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc))
+ (nargs-1)
+ (CicNotationPt.Binder (`Forall, (mk_id "_",
+ Some (mk_eq tys ts us es nargs)),
+ mk_id "P")))), mk_id "P")
+ else mk_id "P"))
+ in
+
+ let inner i ts = CicNotationPt.Case
+ (mk_id "y",None,
+ Some (CicNotationPt.Binder (`Lambda, (mk_id "y",None),
+ CicNotationPt.Binder (`Forall, (mk_id "_", Some
+ (mk_appl [mk_id "eq";CicNotationPt.Implicit
+ `JustOne;CicNotationPt.Implicit `JustOne;mk_id "y"])),
+ CicNotationPt.Implicit `JustOne ))),
+ List.map
+ (fun j ->
+ let nargs_kty = nargs it nleft j in
+ let us = iter (fun m acc -> mk_id ("u" ^ (string_of_int m))::acc)
+ (nargs_kty - 1) [] in
+ let nones =
+ iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
+ CicNotationPt.Pattern (kname it j,
+ None,
+ List.combine us nones),
+ branch i j ts us)
+ (HExtlib.list_seq 0 (List.length cl)))
+ in
+ let outer = CicNotationPt.Case
+ (mk_id "x",None,
+ Some (CicNotationPt.Binder (`Lambda, (mk_id "_",None),
+ (*CicNotationPt.Sort (`NType "2")*) CicNotationPt.Implicit
+ `JustOne)) ,
+ List.map
+ (fun i ->
+ let nargs_kty = nargs it nleft i in
+ let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
+ (nargs_kty - 1) [] in
+ let nones =
+ iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
+ CicNotationPt.Pattern (kname it i,
+ None,
+ List.combine ts nones),
+ inner i ts)
+ (HExtlib.list_seq 0 (List.length cl))) in
+ let principle = CicNotationPt.Binder (`Lambda, (mk_id "x", Some (mk_id indname)),
+ CicNotationPt.Binder (`Lambda, (mk_id "y", Some (mk_id indname)), outer))
+ in
+ pp (lazy ("discriminator = " ^ (CicNotationPp.pp_term principle)));
+
+ status, principle
+;;
+
+let hd_of_term = function
+ | NCic.Appl (hd::_) -> hd
+ | t -> t
+;;
+
+let name_of_rel ~context rel =
+ let s, _ = List.nth context (rel-1) in s
+;;
+
+(* let lookup_in_ctx ~context n =
+ List.nth context ((List.length context) - n - 1)
+;;*)
+
+let discriminate_tac ~context cur_eq status =
+ pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq)));
+
+ let dbranch it leftno consno =
+ prerr_endline (Printf.sprintf "dbranch %d %d" leftno consno);
+ let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
+ (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
+ let params = List.map (fun x -> prerr_endline (Printf.sprintf "dbranch param a%d" x); NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
+ NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern::
+ params @ [
+ NTactics.intro_tac "P";
+ NTactics.intro_tac "DH";
+ NTactics.apply_tac ("",0,mk_id "DH");
+ NTactics.apply_tac ("",0,mk_id "refl");
+ ] in
+ let dbranches it leftno =
+ prerr_endline (Printf.sprintf "dbranches %d" leftno);
+ let _,_,_,cl = it in
+ let nbranches = List.length cl in
+ let branches = iter (fun n acc ->
+ let m = nbranches - n - 1 in
+ if m = 0 then (prerr_endline "no shift"; acc @ (dbranch it leftno m))
+ else (prerr_endline "sì shift"; acc @ NTactics.shift_tac :: (dbranch it
+ leftno m)))
+ (nbranches-1) [] in
+ if nbranches > 1 then
+ (prerr_endline "sì branch";
+ NTactics.branch_tac:: branches @ [NTactics.merge_tac])
+ else
+ (prerr_endline "no branch";
+ branches)
+ in
+
+ let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
+ let _,ctx' = HExtlib.split_nth cur_eq context 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
+ let status, leftno, it =
+ let it, t1, t2 = match s with
+ | NCic.Appl [_;it;t1;t2] -> it,t1,t2
+ | _ -> assert false in
+ (* XXX: serve? ho già fatto whd *)
+ let status, it = whd status ctx' (mk_cic_term ctx' it) in
+ let status, it = term_of_cic_term status it ctx' in
+ let _uri,indtyno,its = match it with
+ NCic.Const (NReference.Ref (uri, NReference.Ind (_,indtyno,_)) as r) ->
+ uri, indtyno, NCicEnvironment.get_checked_indtys r
+ | _ -> prerr_endline ("discriminate: indty =" ^ NCicPp.ppterm
+ ~metasenv:[] ~subst:[] ~context:[] it) ; assert false in
+ let _,leftno,its,_,_ = its in
+ status, leftno, List.nth its indtyno
+ in
+
+ NTactics.block_tac (
+ [(fun status ->
+ let status, discr = mk_discriminator it status in
+ NTactics.cut_tac ("",0, CicNotationPt.Binder (`Forall, (mk_id "x", None),
+ CicNotationPt.Binder (`Forall, (mk_id "y", None),
+ CicNotationPt.Binder (`Forall, (mk_id "e",
+ Some (mk_appl [mk_id "eq";CicNotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])),
+ mk_appl [discr; mk_id "x"; mk_id "y";
+ mk_id "e"]))))
+ status);
+ NTactics.branch_tac;
+ NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern;
+ NTactics.intro_tac "x";
+ NTactics.intro_tac "y";
+ 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 @
+ [NTactics.shift_tac;
+ 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.merge_tac]
+ ) status
+;;
+
+let subst_tac ~context ~dir cur_eq =
+ fun status ->
+ let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
+ let _,ctx' = HExtlib.split_nth cur_eq context 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
+ pp (lazy (Printf.sprintf "subst: equation %s" eq_name));
+ let l, r = match s with
+ | NCic.Appl [_;_;t1;t2] -> t1,t2
+ | _ -> assert false in
+ let var = match dir with
+ | `LeftToRight -> l
+ | `RightToLeft -> r in
+ let var = match var with
+ | NCic.Rel i -> i
+ | _ -> assert false in
+ let names_to_gen, indices_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.block_tac ((List.map gen_tac names_to_gen)@
+ [NTactics.clear_tac names_to_gen;
+ 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)
+;;
+
+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 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
+;;
+
+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 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)));
+ 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
+ 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
+;;
+
+let destruct_tac status = destruct_tac0 0 0 status [];;
projects / helm.git / commitdiff