From: Ferruccio Guidi Date: Sun, 11 Mar 2007 21:17:44 +0000 (+0000) Subject: case to elim conversion works fine X-Git-Tag: 0.4.95@7852~570 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcc533e4ea80eb0b7b34d745c5632abcfc1b4182;p=helm.git case to elim conversion works fine --- diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml index 6b2b2cc90..dcd4cb58b 100644 --- a/components/acic_procedural/proceduralPreprocess.ml +++ b/components/acic_procedural/proceduralPreprocess.ml @@ -23,11 +23,16 @@ * 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