From 3ca25660341410dd0f8694e6863c7c16f4e912a7 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 8 Oct 2012 14:33:46 +0000 Subject: [PATCH] Downgrades buggy destruct patch. --- matita/components/ng_tactics/nDestructTac.ml | 86 ++++++-------------- 1 file changed, 25 insertions(+), 61 deletions(-) diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index 2b6f4688a..fdee9e127 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -184,40 +184,29 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = (* PHASE 1: derive the type of the discriminator (we'll name it "principle") *) - let mk_eq tys ts us es n deps = + let mk_eq tys ts us es n = if use_jmeq then mk_appl [mk_id "jmeq"; NotationPt.Implicit `JustOne; List.nth ts n; NotationPt.Implicit `JustOne; List.nth us n] else - (* we use deps in an attempt to remove unnecessary rewritings when the type - is not maximally dependent *) (* eqty = Tn u0 e0...un-1 en-1 *) let eqty = mk_appl - (List.nth tys n :: iter - (fun i acc -> - if (List.mem (List.nth ts i) deps) - then List.nth us i:: - List.nth es i::acc - else acc) - (n-1) []) in - - (* params = [T0;t0;...;Tn;tn;u0;e0;...;un-1;en-1] *) + (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 -> - if (List.mem (List.nth ts i) deps) - then List.nth tys i :: - List.nth ts i :: acc - else acc) (n-1) - (List.nth tys n::List.nth ts n:: - iter (fun i acc -> - if (List.mem (List.nth ts i) deps) - then List.nth us i:: - List.nth es i::acc - else acc) (n-1) []) in - let nrewrites = List.length deps in + 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 nrewrites) :: params); - List.nth us n] + mk_appl (mk_id ("R" ^ string_of_int n) :: params); + List.nth us n] in @@ -228,20 +217,15 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = name in - let branch i j ts us deps = + let branch i j ts us = let nargs = nargs it leftno i in let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in - let ndepargs k = - let tk = List.nth ts k in - List.length (List.assoc tk deps) - in let tys = List.map - (fun x -> - iter + (fun x -> iter (fun i acc -> NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None), NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), - acc))) ((ndepargs x) - 1) + acc))) (x-1) (NotationPt.Implicit (`Tagged ("T" ^ (string_of_int x))))) (HExtlib.list_seq 0 nargs) in let tys = tys @ @@ -271,7 +255,7 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = if i = j then NotationPt.Binder (`Forall, (mk_id "_", Some (iter (fun i acc -> - NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i (List.assoc (List.nth ts i) deps))), acc)) + NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc)) (nargs-1) (** (NotationPt.Binder (`Forall, (mk_id "_", Some (mk_eq tys ts us es nargs)),*) @@ -279,8 +263,7 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = else mk_id "P") in - let inner i ts deps = - NotationPt.Case + let inner i ts = NotationPt.Case (mk_id "y",None, (*Some (NotationPt.Binder (`Lambda, (mk_id "y",None), NotationPt.Binder (`Forall, (mk_id "_", Some @@ -299,43 +282,24 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = NotationPt.Pattern (kname j, None, List.combine us nones), - branch i j ts us deps) + branch i j ts us) (HExtlib.list_seq 0 (List.length cl))) in let outer = NotationPt.Case (mk_id "x",None, None , List.map - (fun i -> - let _,_,kty = List.nth cl i in + (fun i -> let nargs_kty = nargs it leftno i in - let ts = iter (fun m acc -> ("t" ^ (string_of_int m))::acc) + if (nargs_kty > 5 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i)); + let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc) (nargs_kty - 1) [] in - (* this context is used to compute dependencies between constructor arguments *) - let kctx = List.map2 (fun t ty -> t, NCic.Decl ty) (List.rev ts) (List.rev (arg_list leftno kty)) in - let ts = List.map mk_id ts in - (* compute graph of dependencies *) - let deps,_ = List.fold_left - (fun (acc,i) (t,_) -> - let name,_ = List.nth kctx (i-1) in - (name,fst (cascade_select_in_ctx status ~subst:[] kctx [] i))::acc,i+1) ([],1) kctx - in - (* transpose graph *) - let deps = List.fold_left - (fun acc (t,_) -> - let t_deps = List.map fst (List.filter (fun (name,rev_deps) -> List.mem t rev_deps) deps) in - (t,t_deps)::acc) [] deps - in - let deps = List.map (fun (x,xs) -> mk_id x, (List.map mk_id) xs) deps in - let max_dep = List.fold_left max 0 (List.map (fun (_,xs) -> List.length xs) deps) in - if (max_dep > 4 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i)); - - let nones = + let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in NotationPt.Pattern (kname i, None, List.combine ts nones), - inner i ts deps) + inner i ts) (HExtlib.list_seq 0 (List.length cl))) in let principle = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", -- 2.39.2