From 1463900504de5429c344223b9775ea32d3025059 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 2 Mar 2007 22:24:16 +0000 Subject: [PATCH] Procedural: now patterns for rewrite are generated correctly --- components/acic_procedural/acic2Procedural.ml | 4 + .../acic_procedural/proceduralConversion.ml | 121 ++++++++++-------- components/acic_procedural/proceduralMode.mli | 2 - 3 files changed, 75 insertions(+), 52 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 6512938df..bbc358f71 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -252,6 +252,8 @@ and mk_fwd_proof st dtext name = function | None -> [T.LetIn (name, v, dtext)] | Some v -> mk_fwd_proof st dtext name v end + | C.ACast (_, v, _) -> + mk_fwd_proof st dtext name v | v -> match get_inner_types st v with | Some (ity, _) -> @@ -333,6 +335,8 @@ and mk_proof st = function mk_intros st script (* | Some t -> mk_proof st t *) end + | C.ACast (_, t, _) -> + mk_proof st t | t -> let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in let script = [T.Note text] in diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index 77b5a1817..3bee4dd57 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -78,7 +78,10 @@ let lift k n = and lift_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 C.ARel (id, rid, m + n, b) + | 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 + assert false | 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) @@ -135,13 +138,20 @@ let fake_annotate c = in ann_term c -let rec add_abst n t = - if n <= 0 then t else - let t = C.ALambda ("", C.Name "foo", C.AImplicit ("", None), lift 0 1 t) in - add_abst (pred n) t +let clear_absts m = + let rec aux k n = function + | C.ALambda (id, s, v, t) when k > 0 -> + C.ALambda (id, s, v, aux (pred k) n t) + | C.ALambda (_, _, _, t) when n > 0 -> + aux 0 (pred n) (lift 1 (-1) t) + | t when n > 0 -> assert false + | t -> t + in + aux m let mk_ind context id uri tyno outty arg cases = -try +try + let sort_disp = 0 in let is_recursive = function | C.MutInd (u, no, _) -> UM.eq u uri && no = tyno | _ -> false @@ -154,11 +164,10 @@ try | _ -> assert false in let lps, rps = T.list_split lpsno ps in + let rpsno = List.length rps in let eliminator = get_default_eliminator context uri tyno inty 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 + let predicate = clear_absts rpsno (1 - sort_disp) outty in let map2 case (_, cty) = let map (h, case, k) premise = if h > 0 then pred h, lift k 1 case, k else @@ -176,47 +185,59 @@ try Some (C.AAppl (id, args)) with Invalid_argument _ -> failwith "PCn.mk_ind" -let apply_substs substs = - let length = List.length substs in - let rec apply_xns k (uri, t) = uri, apply_term k t - and apply_ms k = function - | None -> None - | Some t -> Some (apply_term k t) - and apply_fix len k (id, name, i, ty, bo) = - id, name, i, apply_term k ty, apply_term (k + len) bo - and apply_cofix len k (id, name, ty, bo) = - id, name, apply_term k ty, apply_term (k + len) bo - and apply_term k = function - | C.ASort _ as t -> t - | C.AImplicit _ as t -> t - | C.ARel (id, rid, m, b) as t -> - if m < k || m >= length + k then t - else lift 1 k (List.nth substs (m - k)) - | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (apply_xns k) xnss) - | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (apply_xns k) xnss) - | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (apply_xns k) xnss) - | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (apply_xns k) xnss) - | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (apply_ms k) mss) - | C.AAppl (id, ts) -> C.AAppl (id, List.map (apply_term k) ts) - | C.ACast (id, te, ty) -> C.ACast (id, apply_term k te, apply_term k ty) - | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, apply_term k outty, apply_term k t, List.map (apply_term k) pl) - | C.AProd (id, n, s, t) -> C.AProd (id, n, apply_term k s, apply_term (succ k) t) - | C.ALambda (id, n, s, t) -> C.ALambda (id, n, apply_term k s, apply_term (succ k) t) - | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, apply_term k s, apply_term (succ k) t) - | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (apply_fix (List.length fl) k) fl) - | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (apply_cofix (List.length fl) k) fl) - in - apply_term 1 +let hole id = C.AImplicit (id, Some `Hole) -let hole = C.AImplicit ("", Some `Hole) +let meta id = C.AImplicit (id, None) -let mk_pattern rps predicate = hole -(* let rec clear_absts n = function - | C.ALambda (_, _, _, t) when n > 0 -> clear_absts (pred n) t -(* | t when n > 0 -> assert false *) - | t -> t +let anon = C.Anonymous + +let generalize n = + let is_meta = + let map b = function + | C.AImplicit (_, None) when b -> b + | _ -> false + in + List.fold_left map true + in + let rec gen_fix len k (id, name, i, ty, bo) = + id, name, i, gen_term k ty, gen_term (k + len) bo + and gen_cofix len k (id, name, ty, bo) = + id, name, gen_term k ty, gen_term (k + len) bo + and gen_term k = function + | C.ASort (id, _) + | C.AImplicit (id, _) + | C.AConst (id, _, _) + | C.AVar (id, _, _) + | C.AMutInd (id, _, _, _) + | C.AMutConstruct (id, _, _, _, _) + | C.AMeta (id, _, _) -> meta id + | C.ARel (id, _, m, _) -> + if m = succ (n - k) then hole id else meta id + | C.AAppl (id, ts) -> + let ts = List.map (gen_term k) ts in + if is_meta ts then meta id else C.AAppl (id, ts) + | C.ACast (id, te, ty) -> + let te, ty = gen_term k te, gen_term k ty in + if is_meta [te; ty] then meta id else C.ACast (id, te, ty) + | C.AMutCase (id, sp, i, outty, t, pl) -> + let outty, t, pl = gen_term k outty, gen_term k t, List.map (gen_term k) pl in + if is_meta (outty :: t :: pl) then meta id else hole id (* C.AMutCase (id, sp, i, outty, t, pl) *) + | C.AProd (id, _, s, t) -> + let s, t = gen_term k s, gen_term (succ k) t in + if is_meta [s; t] then meta id else C.AProd (id, anon, s, t) + | C.ALambda (id, _, s, t) -> + let s, t = gen_term k s, gen_term (succ k) t in + if is_meta [s; t] then meta id else C.ALambda (id, anon, s, t) + | C.ALetIn (id, _, s, t) -> + let s, t = gen_term k s, gen_term (succ k) t in + if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, t) + | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (gen_fix (List.length fl) k) fl) + | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (gen_cofix (List.length fl) k) fl) in - let substs = hole :: List.rev rps in - let body = clear_absts (succ (List.length rps)) predicate in - if M.is_appl true (cic body) then apply_substs substs body else hole -*) + gen_term 0 + +let mk_pattern rps predicate = + let sort_disp = 0 in + let rpsno = List.length rps in + let body = generalize (rpsno + sort_disp) predicate in + clear_absts 0 (rpsno + sort_disp) body diff --git a/components/acic_procedural/proceduralMode.mli b/components/acic_procedural/proceduralMode.mli index 96a0b3b13..2f0e7e9f4 100644 --- a/components/acic_procedural/proceduralMode.mli +++ b/components/acic_procedural/proceduralMode.mli @@ -26,5 +26,3 @@ val is_eliminator: Cic.term list -> bool val bkd: Cic.context -> Cic.term -> bool - -val is_appl: bool -> Cic.term -> bool -- 2.39.2