From: Ferruccio Guidi Date: Tue, 27 Feb 2007 16:36:45 +0000 (+0000) Subject: - Procedural: some improvements X-Git-Tag: 0.4.95@7852~583 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=474a2de3446753bd9660f185187087d5fa10afd3;p=helm.git - Procedural: some improvements - intros n tactic: now tries whd when Pi or let-ins are not enough --- diff --git a/components/acic_procedural/.depend b/components/acic_procedural/.depend index 61c8bfef8..1b2fc5ff0 100644 --- a/components/acic_procedural/.depend +++ b/components/acic_procedural/.depend @@ -1,11 +1,13 @@ +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi proceduralClassify.cmo: proceduralClassify.cmi proceduralClassify.cmx: proceduralClassify.cmi proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi -proceduralConversion.cmo: proceduralConversion.cmi -proceduralConversion.cmx: proceduralConversion.cmi -proceduralTypes.cmo: proceduralTypes.cmi -proceduralTypes.cmx: proceduralTypes.cmi +proceduralConversion.cmo: proceduralTypes.cmi proceduralClassify.cmi \ + proceduralConversion.cmi +proceduralConversion.cmx: proceduralTypes.cmx proceduralClassify.cmx \ + proceduralConversion.cmi acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \ proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \ diff --git a/components/acic_procedural/.depend.opt b/components/acic_procedural/.depend.opt index 61c8bfef8..1b2fc5ff0 100644 --- a/components/acic_procedural/.depend.opt +++ b/components/acic_procedural/.depend.opt @@ -1,11 +1,13 @@ +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi proceduralClassify.cmo: proceduralClassify.cmi proceduralClassify.cmx: proceduralClassify.cmi proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi -proceduralConversion.cmo: proceduralConversion.cmi -proceduralConversion.cmx: proceduralConversion.cmi -proceduralTypes.cmo: proceduralTypes.cmi -proceduralTypes.cmx: proceduralTypes.cmi +proceduralConversion.cmo: proceduralTypes.cmi proceduralClassify.cmi \ + proceduralConversion.cmi +proceduralConversion.cmx: proceduralTypes.cmx proceduralClassify.cmx \ + proceduralConversion.cmi acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \ proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \ diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 42214b57b..cf8159b0c 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -55,7 +55,7 @@ type status = { (* helpers ******************************************************************) -let id x = x +let identity x = x let comp f g x = f (g x) @@ -115,6 +115,18 @@ let is_rewrite_left = function | C.AConst (_, uri, []) -> UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri | _ -> false + +let is_fwd_rewrite_right hd tl = + if is_rewrite_right hd then match List.nth tl 3 with + | C.ARel _ -> true + | _ -> false + else false + +let is_fwd_rewrite_left hd tl = + if is_rewrite_left hd then match List.nth tl 3 with + | C.ARel _ -> true + | _ -> false + else false (* let get_ind_name uri tno xcno = try @@ -156,23 +168,26 @@ let assumed_premise = "ASSUMED" let expanded_premise = "EXPANDED" -let convert st v = +let convert st ?name v = match get_inner_types st v with + | None -> [] | Some (st, et) -> let cst, cet = cic st, cic et in if PER.alpha_equivalence cst cet then [] else - [T.Change (st, et, "")] - | None -> [] + match name with + | None -> [T.Change (st, et, None, "")] + | Some id -> [T.Change (st, et, Some (id, id), ""); T.ClearBody (id, "")] let eta_expand n t = + let id = Ut.id_of_annterm t in let ty = C.AImplicit ("", None) in let name i = Printf.sprintf "%s%u" expanded_premise i in - let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in + let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in let arg i n = T.mk_arel (n - i) (name i) in let rec aux i f a = if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a) in - let absts, args = aux 0 id [] in + let absts, args = aux 0 identity [] in match Cn.lift 1 n t with | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args)) | t -> absts (C.AAppl ("", t :: args)) @@ -203,9 +218,14 @@ try with Invalid_argument _ -> failwith "A2P.mk_intros" let rec mk_atomic st dtext what = - if T.is_atomic what then [], what else - let name = defined_premise in - mk_fwd_proof st dtext name what, T.mk_arel 0 name + if T.is_atomic what then + match what with + | C.ARel (_, _, _, name) -> convert st ~name what, what + | _ -> [], what + else + let name = defined_premise in + let script = convert st ~name what in + script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name and mk_fwd_rewrite st dtext name tl direction = let what, where = List.nth tl 5, List.nth tl 3 in @@ -215,7 +235,9 @@ and mk_fwd_rewrite st dtext name tl direction = in match where with | C.ARel (_, _, _, binder) -> rewrite binder - | _ -> + | _ -> assert false + +(* assert (get_inner_sort st where = `Prop); let pred, old = List.nth tl 2, List.nth tl 1 in let pred_name = defined_premise in @@ -227,11 +249,11 @@ and mk_fwd_rewrite st dtext name tl direction = let p2 = T.Cut (cut_name, cut_type, cut_text) in let qs = [rewrite cut_name; mk_proof (next st) where] in [T.Branch (qs, ""); p2; p1] - +*) and mk_fwd_proof st dtext name = function | C.AAppl (_, hd :: tl) as v -> - if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else - if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else + if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else + if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in begin match get_inner_types st v with | Some (ity, _) when M.bkd st.context ty -> @@ -240,7 +262,7 @@ and mk_fwd_proof st dtext name = function | _ -> let (classes, rc) as h = Cl.classify st.context ty in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in - [T.LetIn (name, v, dtext ^ text)] + [T.LetIn (name, v, dtext ^ text)] end | C.AMutCase (id, uri, tyno, outty, arg, cases) as v -> begin match Cn.mk_ind st.context id uri tyno outty arg cases with @@ -284,13 +306,14 @@ and mk_proof st = function let script = if proceed then let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in let (classes, rc) as h = Cl.classify st.context ty in - let decurry = List.length classes - List.length tl in + let premises, _ = Cl.split st.context ty in + let decurry = List.length classes - List.length tl in if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else let synth = I.S.singleton 0 in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in match rc with - | Some (i, j) when i > 1 && i <= List.length classes -> + | Some (i, j) when i > 1 && i <= List.length classes && M.is_eliminator premises -> let classes, tl, _, what = split2_last classes tl in let script, what = mk_atomic st dtext what in let synth = I.S.add 1 synth in @@ -316,11 +339,11 @@ and mk_proof st = function mk_intros st script | C.AMutCase (id, uri, tyno, outty, arg, cases) -> begin match Cn.mk_ind st.context id uri tyno outty arg cases with - | None -> + | _ (* None *) -> let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in let script = [T.Note text] in mk_intros st script - | Some t -> mk_proof st t +(* | Some t -> mk_proof st t *) end | t -> let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index 555523a62..4e43164cb 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -31,6 +31,7 @@ module D = Deannotate module UM = UriManager module T = ProceduralTypes +module Cl = ProceduralClassify (* helpers ******************************************************************) @@ -51,10 +52,16 @@ let get_default_eliminator context uri tyno ty = | C.Sort (C.Type _) -> "_rect" | C.Meta (_,_) -> assert false | _ -> assert false - in - let buri = UM.buri_of_uri uri in - let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in - C.Const (uri, []) + in + let buri = UM.buri_of_uri uri in + let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in + C.Const (uri, []) + +let rec list_sub start length = function + | _ :: tl when start > 0 -> list_sub (pred start) length tl + | hd :: tl when length > 0 -> hd :: list_sub start (pred length) tl + | _ -> [] + (* proof construction *******************************************************) @@ -135,20 +142,41 @@ let fake_annotate c = let rec add_abst n t = if n <= 0 then t else - let t = C.ALambda ("", C.Anonymous, C.AImplicit ("", None), lift 0 1 t) in + let t = C.ALambda ("", C.Name "foo", C.AImplicit ("", None), lift 0 1 t) in add_abst (pred n) t let mk_ind context id uri tyno outty arg cases = - let lpsno, (_, _, arity, constructors) = get_ind_type uri tyno in +try + let is_recursive = function + | C.MutInd (u, no, _) -> UM.eq u uri && no = tyno + | _ -> false + in + let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in let ps = match inty with | C.MutInd _ -> [] | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args | _ -> assert false in - let lps, rps = T.list_split lpsno ps in + let lps, rps = T.list_split lpsno ps in let eliminator = get_default_eliminator context uri tyno inty in - let arg_ref = T.mk_arel 0 "" in + let eliminator = fake_annotate context eliminator in + let arg_ref = T.mk_arel 0 "foo" in let body = C.AMutCase (id, uri, tyno, outty, arg_ref, cases) in let predicate = add_abst (succ (List.length rps)) body in - None + let map2 case (_, cty) = + let map (h, case, k) premise = + if h > 0 then pred h, lift k 1 case, k else + if is_recursive premise then 0, lift (succ k) 1 case, succ k else + 0, case, succ k + in + let premises, _ = Cl.split context cty in + let _, lifted_case, _ = + List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises)) + in + lifted_case + in + let lifted_cases = List.map2 map2 cases constructors in + let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in + Some (C.AAppl (id, args)) +with Invalid_argument _ -> failwith "PCn.mk_ind" diff --git a/components/acic_procedural/proceduralMode.ml b/components/acic_procedural/proceduralMode.ml index bd2c3a438..433966d1b 100644 --- a/components/acic_procedural/proceduralMode.ml +++ b/components/acic_procedural/proceduralMode.ml @@ -26,6 +26,11 @@ module C = Cic module Cl = ProceduralClassify +let is_eliminator = function + | _ :: C.MutInd _ :: _ -> true + | _ :: C.Appl (C.MutInd _ :: _) :: _ -> true + | _ -> false + let is_const = function | C.Sort _ | C.Const _ @@ -41,5 +46,10 @@ let rec is_appl b = function | _ -> false let bkd c t = - let ts, _ = Cl.split c t in - is_appl true (List.hd ts) + let classes, rc = Cl.classify c t in + let premises, _ = Cl.split c t in + match rc with + | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true + | _ -> + let ts, _ = Cl.split c t in + is_appl true (List.hd ts) diff --git a/components/acic_procedural/proceduralMode.mli b/components/acic_procedural/proceduralMode.mli index dc382693f..2f0e7e9f4 100644 --- a/components/acic_procedural/proceduralMode.mli +++ b/components/acic_procedural/proceduralMode.mli @@ -23,4 +23,6 @@ * http://cs.unibo.it/helm/. *) +val is_eliminator: Cic.term list -> bool + val bkd: Cic.context -> Cic.term -> bool diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index 1d8bbbc21..b81a7c3de 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -88,7 +88,8 @@ type step = Note of note | Elim of what * using option * note | Apply of what * note | Whd of count * note - | Change of inferred * what * note + | Change of inferred * what * where * note + | ClearBody of name * note | Branch of step list list * note (* annterm constructors *****************************************************) @@ -151,11 +152,18 @@ let mk_whd i = let tactic = G.Reduce (floc, `Whd, pattern) in mk_tactic tactic -let mk_change t = - let pattern = None, [], Some hole in +let mk_change t where = + let pattern = match where with + | None -> None, [], Some hole + | Some (premise, _) -> None, [premise, hole], None + in let tactic = G.Change (floc, pattern, t) in mk_tactic tactic +let mk_clearbody id = + let tactic = G.ClearBody (floc, id) in + mk_tactic tactic + let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None)) let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None)) @@ -180,7 +188,8 @@ let rec render_step sep a = function | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a) | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a) - | Change (t, _, s) -> mk_note s :: cont sep (mk_change t :: a) + | Change (t, _, w, s) -> mk_note s :: cont sep (mk_change t w :: a) + | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a) | Branch ([], s) -> a | Branch ([ps], s) -> render_steps sep a ps | Branch (pss, s) -> diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli index 9fb7f3035..f26c19d87 100644 --- a/components/acic_procedural/proceduralTypes.mli +++ b/components/acic_procedural/proceduralTypes.mli @@ -55,7 +55,8 @@ type step = Note of note | Elim of what * using option * note | Apply of what * note | Whd of count * note - | Change of inferred * what * note + | Change of inferred * what * where * note + | ClearBody of name * note | Branch of step list list * note val render_steps: diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 1012fc935..60eb4dc5b 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -40,7 +40,7 @@ exception WrongUriToVariable of string (* howmany = -1 means Intros, howmany > 0 means Intros n *) let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = let module C = Cic in - let rec collect_context context howmany ty = + let rec collect_context context howmany do_whd ty = match howmany with | 0 -> let irl = @@ -49,16 +49,16 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = context, ty, (C.Meta (newmeta,irl)) | _ -> match ty with - C.Cast (te,_) -> collect_context context howmany te + C.Cast (te,_) -> collect_context context howmany do_whd te | C.Prod (n,s,t) -> let n' = mk_fresh_name metasenv context n ~typ:s in let (context',ty,bo) = - collect_context ((Some (n',(C.Decl s)))::context) (howmany - 1) t + collect_context ((Some (n',(C.Decl s)))::context) (howmany - 1) do_whd t in (context',ty,C.Lambda(n',s,bo)) | C.LetIn (n,s,t) -> let (context',ty,bo) = - collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) t + collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t in (context',ty,C.LetIn(n,s,bo)) | _ as t -> @@ -67,10 +67,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = CicMkImplicit.identity_relocation_list_for_metavariable context in context, t, (C.Meta (newmeta,irl)) - else + else if do_whd then + let t = CicReduction.whd ~delta:true context t in + collect_context context howmany false t + else raise (Fail (lazy "intro(s): not enough products or let-ins")) in - collect_context context howmany ty + collect_context context howmany true ty let eta_expand metasenv context t arg = let module T = CicTypeChecker in