From b4fd90e993045c2a71b6fd2479cd515f09d36d06 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 21 May 2009 19:04:29 +0000 Subject: [PATCH] Procedural: we use the expected type rather than the inferred type when we perform a cut to keep the goal in sync with the expected type. we try to beta-reduce the elimination pattern when it does not match the goal/expected type now nat/compare.ma and Z/z.ma are fully reconstructed :) --- .../components/acic_procedural/procedural2.ml | 40 ++-- .../acic_procedural/proceduralConversion.ml | 172 +++++++++++------- .../acic_procedural/proceduralConversion.mli | 2 +- 3 files changed, 128 insertions(+), 86 deletions(-) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index e736842b7..46d4431bd 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -230,14 +230,14 @@ let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what | _ -> [] -let mk_fwd_rewrite st dtext name tl direction v t ity = +let mk_fwd_rewrite st dtext name tl direction v t ity ety = let compare premise = function | None -> true | Some s -> s = premise in assert (List.length tl = 6); let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in - let e = Cn.mk_pattern 1 predicate in + let e = Cn.mk_pattern 1 ety predicate in if (Cn.does_not_occur e) then st, [] else match where with | C.ARel (_, _, i, premise) as w -> @@ -258,10 +258,10 @@ let mk_fwd_rewrite st dtext name tl direction v t ity = end | _ -> assert false -let mk_rewrite st dtext where qs tl direction t = +let mk_rewrite st dtext where qs tl direction t ety = assert (List.length tl = 5); let predicate = List.nth tl 2 in - let e = Cn.mk_pattern 1 predicate in + let e = Cn.mk_pattern 1 ety predicate in let script = [T.Branch (qs, "")] in if (Cn.does_not_occur e) then script else T.Rewrite (direction, where, None, e, dtext) :: script @@ -284,17 +284,17 @@ and proc_letin st what name v w t = let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with | Some (C.ALetIn _, _), _ -> st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)] - | _, Some (ity, _) -> + | _, Some (ity, ety) -> let st, rqv = match v with | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl -> - mk_fwd_rewrite st dtext intro tl true v t ity + mk_fwd_rewrite st dtext intro tl true v t ity ety | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left st hd tl -> - mk_fwd_rewrite st dtext intro tl false v t ity + mk_fwd_rewrite st dtext intro tl false v t ity ety | v -> - assert (Ut.is_sober st.context (H.cic ity)); - let ity = H.acic_bc st.context ity in + assert (Ut.is_sober st.context (H.cic ety)); + let ety = H.acic_bc st.context ety in let qs = [proc_proof (next st) v; [T.Id ""]] in - st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] + st, [T.Branch (qs, ""); T.Cut (intro, ety, dtext)] in st, C.Decl (H.cic ity), rqv | _, None -> @@ -359,17 +359,22 @@ and proc_appl st what hd tl = let synth2 = I.S.add 1 synth in let names = H.get_ind_names uri tyno in let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in - if List.length qs <> List.length names then + let ety = match get_inner_types st what with + | Some (_, ety) -> ety + | None -> + Cn.fake_annotate "" st.context (get_type "TC3" st what) + in + if List.length qs <> List.length names then let qs = proc_bkd_proofs (next st) synth [] classes tl in let b, hd = mk_exp_args hd tl classes synth in script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else if is_rewrite_right st hd then - script2 @ mk_rewrite st dtext where qs tl2 false what + script2 @ mk_rewrite st dtext where qs tl2 false what ety else if is_rewrite_left st hd then - script2 @ mk_rewrite st dtext where qs tl2 true what + script2 @ mk_rewrite st dtext where qs tl2 true what ety else let predicate = List.nth tl2 (parsno - i) in - let e = Cn.mk_pattern j predicate in + let e = Cn.mk_pattern j ety predicate in let using = Some hd in script2 @ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] @@ -393,7 +398,12 @@ and proc_case st what uri tyno u v ts = let ps, _ = H.get_ind_parameters st.context (H.cic v) in let _, rps = HEL.split_nth lpsno ps in let rpsno = List.length rps in - let e = Cn.mk_pattern rpsno u in + let ety = match get_inner_types st what with + | Some (_, ety) -> ety + | None -> + Cn.fake_annotate "" st.context (get_type "TC4" st what) + in + let e = Cn.mk_pattern rpsno ety u in let text = "" in let script = List.rev (mk_arg st v) in script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")] diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 8c9a1ddc6..f6dd83be3 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -44,80 +44,91 @@ let rec list_sub start length = function (* proof construction *******************************************************) -let lift k n = - let rec lift_xns k (uri, t) = uri, lift_term k t - and lift_ms k = function +let iter f k = + let rec iter_xns k (uri, t) = uri, iter_term k t + and iter_ms k = function | None -> None - | Some t -> Some (lift_term k t) - and lift_fix len k (id, name, i, ty, bo) = - id, name, i, lift_term k ty, lift_term (k + len) bo - and lift_cofix len k (id, name, ty, bo) = - id, name, lift_term k ty, lift_term (k + len) bo - and lift_term k = function + | Some t -> Some (iter_term k t) + and iter_fix len k (id, name, i, ty, bo) = + id, name, i, iter_term k ty, iter_term (k + len) bo + and iter_cofix len k (id, name, ty, bo) = + id, name, iter_term k ty, iter_term (k + len) bo + and iter_term k = function | C.ASort _ as t -> t | C.AImplicit _ as t -> t | C.ARel (id, rid, m, b) as t -> - if m < k then t else - if m + n > 0 then C.ARel (id, rid, m + n, b) else - begin - HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n); - assert false - end - | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss) - | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss) - | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss) - | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss) - | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss) - | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts) - | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty) - | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl) - | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t) - | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t) - | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k ty, lift_term k s, lift_term (succ k) t) - | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl) - | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) + if m < k then t else f k id rid m b + | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (iter_xns k) xnss) + | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (iter_xns k) xnss) + | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (iter_xns k) xnss) + | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (iter_xns k) xnss) + | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (iter_ms k) mss) + | C.AAppl (id, ts) -> C.AAppl (id, List.map (iter_term k) ts) + | C.ACast (id, te, ty) -> C.ACast (id, iter_term k te, iter_term k ty) + | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, iter_term k outty, iter_term k t, List.map (iter_term k) pl) + | C.AProd (id, n, s, t) -> C.AProd (id, n, iter_term k s, iter_term (succ k) t) + | C.ALambda (id, n, s, t) -> C.ALambda (id, n, iter_term k s, iter_term (succ k) t) + | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, iter_term k ty, iter_term k s, iter_term (succ k) t) + | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (iter_fix (List.length fl) k) fl) + | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (iter_cofix (List.length fl) k) fl) in - lift_term k + iter_term k - let fake_annotate id c = - let get_binder c m = - try match List.nth c (pred m) with - | Some (C.Name s, _) -> s - | _ -> assert false - with - | Invalid_argument _ -> assert false - in - let mk_decl n v = Some (n, C.Decl v) in - let mk_def n v ty = Some (n, C.Def (v, ty)) in - let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in - let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in - let rec ann_xns c (uri, t) = uri, ann_term c t - and ann_ms c = function - | None -> None - | Some t -> Some (ann_term c t) - and ann_fix newc c (name, i, ty, bo) = - id, name, i, ann_term c ty, ann_term (List.rev_append newc c) bo - and ann_cofix newc c (name, ty, bo) = - id, name, ann_term c ty, ann_term (List.rev_append newc c) bo - and ann_term c = function - | C.Sort sort -> C.ASort (id, sort) - | C.Implicit ann -> C.AImplicit (id, ann) - | C.Rel m -> C.ARel (id, id, m, get_binder c m) - | C.Const (uri, xnss) -> C.AConst (id, uri, List.map (ann_xns c) xnss) - | C.Var (uri, xnss) -> C.AVar (id, uri, List.map (ann_xns c) xnss) - | C.MutInd (uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (ann_xns c) xnss) - | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (ann_xns c) xnss) - | C.Meta (i, mss) -> C.AMeta(id, i, List.map (ann_ms c) mss) - | C.Appl ts -> C.AAppl (id, List.map (ann_term c) ts) - | C.Cast (te, ty) -> C.ACast (id, ann_term c te, ann_term c ty) - | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl) - | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) - | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) - | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t) - | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl) - | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl) - in - ann_term c +let lift k n = + let f _ id rid m b = + if m + n > 0 then C.ARel (id, rid, m + n, b) else + begin + HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n); + assert false + end + in + iter f k + +let subst k v = + let f k id rid m b = + if m = k then lift 1 (pred k) v else C.ARel (id, rid, pred m, b) + in + iter f k + +let fake_annotate id c = + let get_binder c m = + try match List.nth c (pred m) with + | Some (C.Name s, _) -> s + | _ -> assert false + with + | Invalid_argument _ -> assert false + in + let mk_decl n v = Some (n, C.Decl v) in + let mk_def n v ty = Some (n, C.Def (v, ty)) in + let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in + let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in + let rec ann_xns c (uri, t) = uri, ann_term c t + and ann_ms c = function + | None -> None + | Some t -> Some (ann_term c t) + and ann_fix newc c (name, i, ty, bo) = + id, name, i, ann_term c ty, ann_term (List.rev_append newc c) bo + and ann_cofix newc c (name, ty, bo) = + id, name, ann_term c ty, ann_term (List.rev_append newc c) bo + and ann_term c = function + | C.Sort sort -> C.ASort (id, sort) + | C.Implicit ann -> C.AImplicit (id, ann) + | C.Rel m -> C.ARel (id, id, m, get_binder c m) + | C.Const (uri, xnss) -> C.AConst (id, uri, List.map (ann_xns c) xnss) + | C.Var (uri, xnss) -> C.AVar (id, uri, List.map (ann_xns c) xnss) + | C.MutInd (uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (ann_xns c) xnss) + | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (ann_xns c) xnss) + | C.Meta (i, mss) -> C.AMeta(id, i, List.map (ann_ms c) mss) + | C.Appl ts -> C.AAppl (id, List.map (ann_term c) ts) + | C.Cast (te, ty) -> C.ACast (id, ann_term c te, ann_term c ty) + | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl) + | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) + | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) + | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t) + | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl) + | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl) + in + ann_term c let mk_arel k = C.ARel ("", "", k, "") @@ -184,8 +195,29 @@ let generalize n = in gen_term -let mk_pattern psno predicate = - clear_absts (generalize psno) psno 0 predicate +let convert g ety k predicate = + let rec aux = function + | C.ALambda (_, _, b, ety), C.ALambda (id, n, u, pred) -> + C.ALambda (id, n, aux (b, u), aux (ety, pred)) + | C.AProd (_, _, b, ety), C.AProd (id, n, u, pred) -> + C.AProd (id, n, aux (b, u), aux (ety, pred)) + | C.ALetIn (_, _, a, b, ety), C.ALetIn (id, n, v, u, pred) -> + C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ety, pred)) + | C.AAppl (_, bs), C.AAppl (id, us) when List.length bs = List.length us -> + let map b u = aux (b,u) in + C.AAppl (id, List.map2 map bs us) + | C.ACast (_, ety, b), C.ACast (id, pred, u) -> + C.ACast (id, aux (ety, pred), aux (b, u)) + | ety, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) -> + aux (ety, subst 1 v pred) + | ety, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) -> + aux (ety, C.AAppl (id, subst 1 v pred :: vs)) + | _, pred -> pred + in + g k (aux (ety, predicate)) + +let mk_pattern psno ety predicate = + clear_absts (convert (generalize psno) ety) psno 0 predicate let get_clears c p xtypes = let meta = C.Implicit None in diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli index bc49b9a22..210813331 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.mli +++ b/helm/software/components/acic_procedural/proceduralConversion.mli @@ -31,7 +31,7 @@ val lift: int -> int -> Cic.annterm -> Cic.annterm val fake_annotate: Cic.id -> Cic.context -> Cic.term -> Cic.annterm -val mk_pattern: int -> Cic.annterm -> Cic.annterm +val mk_pattern: int -> Cic.annterm -> Cic.annterm -> Cic.annterm val get_clears: Cic.context -> Cic.term -> (Cic.term * Cic.term) option -> -- 2.39.2