]> matita.cs.unibo.it Git - helm.git/commitdiff
case to elim conversion works fine
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 11 Mar 2007 21:17:44 +0000 (21:17 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 11 Mar 2007 21:17:44 +0000 (21:17 +0000)
helm/software/components/acic_procedural/proceduralPreprocess.ml

index 6b2b2cc90ec3eecf255ceb55a1cc50354d37b521..dcd4cb58b20588734b9a40c5ee5ca27d2db0a1ba 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+module UM   = UriManager
 module C    = Cic
+module Pp   = CicPp
 module Un   = CicUniv
+module I    = CicInspect
+module E    = CicEnvironment
 module S    = CicSubstitution
 module Rd   = CicReduction
 module TC   = CicTypeChecker 
+module Rf   = CicRefine
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
 
@@ -36,12 +41,38 @@ module HEL  = HExtlib
 let identity x = x
 
 let comp f g x = f (g x)
+   
+let split c t =
+   let add s v c = Some (s, C.Decl v) :: c in
+   let rec aux whd a n c = function
+      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
+      | v when whd        -> v :: a, n
+      | v                 -> aux true a n c (Rd.whd ~delta:true c v)
+    in
+    aux false [] 0 c t
 
 let get_type c t =
-   let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+   with e -> 
+      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
+      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
+      raise e
+
+let refine c t =
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+   with e -> 
+      Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
+      Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
+      Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
+      raise e
+
+let get_tail c t =
+   match split c t with
+      | hd :: _, _ -> hd
+      | _          -> assert false
 
 let is_proof c t =
-   match Rd.whd ~delta:true c (get_type c (get_type c t)) with
+   match get_tail c (get_type c (get_type c t)) with
       | C.Sort C.Prop -> true
       | C.Sort _      -> false
       | _             -> assert false 
@@ -55,14 +86,57 @@ let is_not_atomic = function
    | C.MutConstruct _ -> false
    | _                -> true
 
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (Rd.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
+let clear_absts m =
+   let rec aux k n = function
+      | C.Lambda (s, v, t) when k > 0    -> 
+         C.Lambda (s, v, aux (pred k) n t)
+      | C.Lambda (_, _, t) when n > 0    -> 
+         aux 0 (pred n) (S.lift (-1) t)
+      | t                     when n > 0 ->
+         Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
+        assert false 
+      | t                                 -> t
+   in 
+   aux m
+
+let rec add_abst k = function 
+   | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, add_abst (pred k) t)
+   | t when k > 0 -> assert false
+   | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
+
+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_ind_parameters c t =
+   let ty = get_type c t in
+   let ps = match get_tail c ty with
+      | C.MutInd _                  -> []
+      | C.Appl (C.MutInd _ :: args) -> args
+      | _                           -> assert false
+   in
+   let disp = match get_tail c (get_type c ty) with
+      | C.Sort C.Prop -> 0
+      | C.Sort _      -> 1
+      | _             -> assert false
+   in
+   ps, disp
+
+let get_default_eliminator context uri tyno ty =
+   let _, (name, _, _, _) = get_ind_type uri tyno in
+   let ext = match get_tail context (get_type context ty) with
+      | C.Sort C.Prop     -> "_ind"
+      | C.Sort C.Set      -> "_rec"
+      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.Type _) -> "_rect"
+      | t                 -> 
+         Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
+         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 add g htbl t proof decurry =
    if proof then C.CicHash.add htbl t decurry; 
@@ -180,19 +254,49 @@ and pp_atomic g ht es c t =
    let _, premsno = split c (get_type c t) in
    g t true premsno
 
+and pp_mutcase g ht es c uri tyno outty arg cases =
+   let eliminator = get_default_eliminator c uri tyno outty in
+   let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
+   let ps, sort_disp = get_ind_parameters c arg in
+   let lps, rps = HEL.split_nth lpsno ps in
+   let rpsno = List.length rps in
+   let predicate = clear_absts rpsno (1 - sort_disp) outty in   
+   let is_recursive t =
+      I.S.mem tyno (I.get_mutinds_of_uri uri t) 
+   in
+   let map2 case (_, cty) = 
+      let map (h, case, k) premise = 
+         if h > 0 then pred h, case, k else
+        if is_recursive premise then 
+           0, add_abst k case, k + 2 
+        else
+           0, case, succ k
+      in
+      let premises, _ = split c 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
+   let x = refine c (C.Appl args) in
+   pp_proof g ht es c x
+
 and pp_proof g ht es c t = 
-  Printf.eprintf "IN: |- %s\n" (*CicPp.ppcontext c*) (CicPp.ppterm t);
+(*  Printf.eprintf "IN: |- %s\n" (*CicPp.ppcontext c*) (CicPp.ppterm t);
   let g t proof decurry = 
      Printf.eprintf "OUT: %b %u |- %s\n" proof decurry (CicPp.ppterm t);
      g t proof decurry
-  in
+  in *)
 (*   let g t proof decurry = add g ht t proof decurry in *)
    match t with
-      | C.Cast (t, v)         -> pp_cast g ht es c t v
-      | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
-      | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
-      | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
-      | t                     -> pp_atomic g ht es c t
+      | C.Cast (t, v)              -> pp_cast g ht es c t v
+      | C.Lambda (name, v, t)      -> pp_lambda g ht es c name v t
+      | C.LetIn (name, v, t)       -> pp_letin g ht es c name v t
+      | C.Appl (t :: vs)           -> pp_appl g ht es c t vs
+      | C.MutCase (u, n, t, v, ws) -> pp_mutcase g ht es c u n t v ws
+      | t                          -> pp_atomic g ht es c t
 
 and pp_term g ht es c t =
    if is_proof c t then pp_proof g ht es c t else g t false 0