elim tactic: now takes a pattern instead of just a term

[helm.git] / components / acic_procedural / proceduralConversion.ml

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index d2d305ed4cffc959e107a274479389d42cfb8f64..5f705053a1a3e405903fa06d2a081f278c057ffb 100644 (file)
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -39,26 +39,6 @@ module M    = ProceduralMode
 
 let cic = D.deannotate_term
 
-let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
-      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
-      | _                                           -> assert false
-
-let get_default_eliminator context uri tyno ty =
-   let _, (name, _, _, _) = get_ind_type uri tyno in
-   let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in
-   let ext = match sort with
-      | C.Sort C.Prop     -> "_ind"
-      | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
-      | 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, [])
-
 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
@@ -98,46 +78,6 @@ let lift k n =
    in
    lift_term k
 
-let fake_annotate 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 = Some (n, C.Def (v, None)) in
-   let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
-   let mk_cofix (name, _, bo) = mk_def (C.Name name) bo 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) =
-      "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
-   and ann_cofix newc c (name, ty, bo) =
-      "", name, ann_term c ty, ann_term (List.rev_append newc c) bo
-   and ann_term c = function
-      | C.Sort sort -> C.ASort ("", sort)
-      | C.Implicit ann -> C.AImplicit ("", ann)
-      | C.Rel m -> C.ARel ("", "", m, get_binder c m)
-      | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss)
-      | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss)
-      | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss)
-      | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss)
-      | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss)
-      | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts)
-      | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty)
-      | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)      
-      | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
-      | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
-      | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t)
-      | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
-      | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
-   in
-   ann_term c
-
 let clear_absts m =
    let rec aux k n = function
       | C.AImplicit (_, None) as t         -> t
@@ -152,42 +92,6 @@ let clear_absts m =
    in 
    aux m
 
-let mk_ind context id uri tyno outty arg cases =
-try
-   let sort_disp = 0 in
-   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 Rd.whd ~delta:true context 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 rpsno = List.length rps in
-   let eliminator = get_default_eliminator context uri tyno inty in
-   let eliminator = fake_annotate context eliminator 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
-        if is_recursive premise then 0, lift (succ k) 1 case, succ k else
-        0, case, succ k
-      in
-      let premises, _ = P.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"
-
 let hole id = C.AImplicit (id, Some `Hole)
 
 let meta id = C.AImplicit (id, None)
@@ -239,8 +143,6 @@ let generalize n =
    in
    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
+let mk_pattern rpsno predicate =
+   let body = generalize rpsno predicate in
+   clear_absts 0 rpsno body