From: Stefano Zacchiroli Date: Tue, 11 Jan 2005 16:02:53 +0000 (+0000) Subject: snapshot, not yet completed, but ... X-Git-Tag: V_0_1_0~149 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa70e8149a0c5405c4498cb3b7898d733a91910b;p=helm.git snapshot, not yet completed, but ... --- diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 1de440d56..77304c1ec 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + let fresh_binder = let counter = ref ~-1 in function @@ -81,9 +83,11 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args = if recursive uri src then let args = List.map (CicSubstitution.lift 2) args in let phi = - (delta (uri, typeno, subst) dependent paramsno consno src - (CicSubstitution.lift 1 p) [Cic.Rel 1]) + let src = CicSubstitution.lift 1 src in + delta (uri, typeno, subst) dependent paramsno consno src + (CicSubstitution.lift 1 p) [Cic.Rel 1] in + let tgt = CicSubstitution.lift 1 tgt in Cic.Prod (fresh_binder dependent, src, Cic.Prod (Cic.Anonymous, phi, delta (uri, typeno, subst) dependent paramsno consno tgt @@ -132,24 +136,23 @@ let rec count_pi = function | Cic.Prod (_, _, tgt) -> count_pi tgt + 1 | t -> 0 -let rec type_of_p dependent leftno indty = function +let rec type_of_p sort dependent leftno indty = function | Cic.Prod (n, src, tgt) when leftno = 0 -> - Cic.Prod (n, src, type_of_p dependent leftno indty tgt) - | Cic.Prod (_, _, tgt) -> type_of_p dependent (leftno - 1) indty tgt + Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt) + | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt | t -> if dependent then - Cic.Prod (Cic.Anonymous, indty, - Cic.Sort (Cic.Type (CicUniv.fresh ()))) + Cic.Prod (Cic.Anonymous, indty, Cic.Sort sort) else - Cic.Sort (Cic.Type (CicUniv.fresh ())) + Cic.Sort sort -let rec add_right_pi dependent strip liftno rightno indty = function +let rec add_right_pi dependent strip liftno liftfrom rightno indty = function | Cic.Prod (_, src, tgt) when strip = 0 -> Cic.Prod (fresh_binder true, - CicSubstitution.lift liftno src, - add_right_pi dependent strip liftno rightno indty tgt) + CicSubstitution.lift_from (liftfrom + 1) liftno src, + add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt) | Cic.Prod (_, _, tgt) -> - add_right_pi dependent (strip - 1) liftno rightno indty tgt + add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt | t -> if dependent then Cic.Prod (fresh_binder dependent, @@ -163,7 +166,15 @@ let rec add_right_pi dependent strip liftno rightno indty = function else Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno)) -let elim_of uri typeno = +exception Failure of string + +let string_of_sort = function + | Cic.Prop -> "Prop" + | Cic.CProp -> "CProp" + | Cic.Set -> "Set" + | Cic.Type _ -> "Type" + +let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in let subst = [] in match obj with @@ -177,9 +188,12 @@ let elim_of uri typeno = let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in let conslen = List.length constructors in let consno = ref (conslen + 1) in + if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then + raise (Failure (sprintf "can't eliminate from Prop to %s" + (string_of_sort sort))); let indty = let indty = Cic.MutInd (uri, typeno, subst) in - if leftno = 0 then + if paramsno = 0 then indty else Cic.Appl (indty :: mk_rels 0 paramsno) @@ -192,9 +206,9 @@ let elim_of uri typeno = Cic.Appl (constructor :: mk_rels consno leftno) in let eliminator = - let p_ty = type_of_p dependent leftno indty ty in + let p_ty = type_of_p sort dependent leftno indty ty in let final_ty = - add_right_pi dependent leftno (conslen + 1) (paramsno - leftno) + add_right_pi dependent leftno (conslen + 1) 1 (paramsno - leftno) indty ty in Cic.Prod (Cic.Name "P", p_ty, diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index 828028d0a..b341d36a4 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -23,8 +23,12 @@ * http://helm.cs.unibo.it/ *) -(** @param uri inductive type uri +exception Failure of string + +(** @param sort target sort, defaults to Type +* @param uri inductive type uri * @param typeno inductive type number +* @raise Failure *) -val elim_of: UriManager.uri -> int -> Cic.term +val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term