X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=80aae9e7f3668b83fcee3378d7cb148174b5c31c;hb=d178a0a4809c0c6693b2c00ab7359a1b414cd805;hp=3bee4dd57e0cdebc9c7bbb3298b159ec964d5b36;hpb=8a4fdd910446fb3635719d979613aad2bd56db16;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 3bee4dd57..80aae9e7f 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -29,41 +29,17 @@ module Un   = CicUniv
 module TC   = CicTypeChecker 
 module D    = Deannotate
 module UM   = UriManager
-
-module T    = ProceduralTypes
-module Cl   = ProceduralClassify
-module M    = ProceduralMode
+module Rd   = CicReduction
 
 (* helpers ******************************************************************)
 
 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
    | _                        -> []
     
-
 (* proof construction *******************************************************)
 
 let lift k n =
@@ -98,93 +74,20 @@ 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
       | 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 -> 
+      | C.ALambda (_, _, _, t) when n > 0  -> 
          aux 0 (pred n) (lift 1 (-1) t)
-      | t                      when n > 0 -> assert false
-      | t                                 -> t
+      | t                      when n > 0  ->
+	    Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+	    assert false 
+      | t                                  -> t
    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 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, _ = 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"
-
 let hole id = C.AImplicit (id, Some `Hole)
 
 let meta id = C.AImplicit (id, None)
@@ -212,7 +115,7 @@ let generalize n =
       | C.AMutConstruct (id, _, _, _, _)
       | C.AMeta (id, _, _) -> meta id
       | C.ARel (id, _, m, _) -> 
-         if m = succ (n - k) then hole id else meta id
+         if succ (k - n) <= m && m <= 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)
@@ -236,8 +139,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 psno predicate =
+   let body = generalize psno predicate in
+   clear_absts 0 psno body