From: Stefano Zacchiroli Date: Wed, 5 Jan 2005 14:06:41 +0000 (+0000) Subject: snapshot X-Git-Tag: V_0_1_0~154 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1850832c5f252cb6f79bce5184ccb9046a4057fb;p=helm.git snapshot --- diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 93d64a12c..1de440d56 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -25,64 +25,92 @@ let fresh_binder = let counter = ref ~-1 in - fun () -> - incr counter; - "elim" ^ string_of_int !counter + function + | true -> + incr counter; + Cic.Name ("elim" ^ string_of_int !counter) + | _ -> Cic.Anonymous (** verifies if a given uri occurs in a term in target position *) let rec recursive uri = function | Cic.Prod (_, _, target) -> recursive uri target - | Cic.MutInd (uri', _, _) - | Cic.Appl [ Cic.MutInd (uri', _, _); _ ] -> UriManager.eq uri uri' + | Cic.MutInd (uri', _, _) -> UriManager.eq uri uri' + | Cic.Appl args -> List.exists (recursive uri) args | _ -> false let unfold_appl = function | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl) | t -> t +let rec split l n = + match (l,n) with + (l,0) -> ([], l) + | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) + | (_,_) -> assert false + (** build elimination principle part related to a single constructor - * @param strip number of Prod to ignore in this constructor (i.e. number of - * inductive parameters) *) -let rec delta (uri, typeno, subst) strip consno t p args = + * @param paramsno number of Prod to ignore in this constructor (i.e. number of + * inductive parameters) + * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *) +let rec delta (uri, typeno, subst) dependent paramsno consno t p args = assert (subst = []); match t with - | Cic.MutInd (uri', typeno', subst') - | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) when - UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> - (match args with - | [] -> assert false - | [arg] -> unfold_appl (Cic.Appl [p; arg]) - | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)])) -(* - | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) when + | Cic.MutInd (uri', typeno', subst') -> + if dependent then + (match args with + | [] -> assert false + | [arg] -> unfold_appl (Cic.Appl [p; arg]) + | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)])) + else + p + | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> - Cic.Appl (Cic.Rel p_rel :: args) -*) - | Cic.Prod (binder, src, tgt) when strip = 0 -> + let (lparams, rparams) = split tl paramsno in + if dependent then + (match args with + | [] -> assert false + | [arg] -> unfold_appl (Cic.Appl (p :: rparams @ [arg])) + | _ -> + unfold_appl (Cic.Appl (p :: + rparams @ [unfold_appl (Cic.Appl args)]))) + else (* non dependent *) + (match rparams with + | [] -> p + | _ -> Cic.Appl (p :: rparams)) + | Cic.Prod (binder, src, tgt) -> if recursive uri src then let args = List.map (CicSubstitution.lift 2) args in let phi = - (delta (uri, typeno, subst) strip consno src + (delta (uri, typeno, subst) dependent paramsno consno src (CicSubstitution.lift 1 p) [Cic.Rel 1]) in - Cic.Prod (Cic.Name (fresh_binder ()), src, + Cic.Prod (fresh_binder dependent, src, Cic.Prod (Cic.Anonymous, phi, - delta (uri, typeno, subst) strip consno tgt + delta (uri, typeno, subst) dependent paramsno consno tgt (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2]))) else (* non recursive *) let args = List.map (CicSubstitution.lift 1) args in - Cic.Prod (Cic.Name (fresh_binder ()), src, - delta (uri, typeno, subst) strip consno tgt (CicSubstitution.lift 1 p) - (args @ [Cic.Rel 1])) - | Cic.Prod (_, _, tgt) (* when strip > 0 *) -> - (* after stripping the parameters we lift of 1 since P has been inserted - * in the way *) - let tgt = - if strip = 1 then CicSubstitution.lift consno tgt else tgt - in - delta (uri, typeno, subst) (strip - 1) consno tgt p args + Cic.Prod (fresh_binder dependent, src, + delta (uri, typeno, subst) dependent paramsno consno tgt + (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1])) | _ -> assert false +let rec strip_left_params consno leftno = function + | t when leftno = 0 -> t (* no need to lift, the term is (hopefully) closed *) + | Cic.Prod (_, _, tgt) (* when leftno > 0 *) -> + (* after stripping the parameters we lift of consno. consno is 1 based so, + * the first constructor will be lifted by 1 (for P), the second by 2 (1 + * for P and 1 for the 1st constructor), and so on *) + if leftno = 1 then + CicSubstitution.lift consno tgt + else + strip_left_params consno (leftno - 1) tgt + | _ -> assert false + +let delta (ury, typeno, subst) dependent paramsno consno t p args = + let t = strip_left_params consno paramsno t in + delta (ury, typeno, subst) dependent paramsno consno t p args + let rec add_params indno ty eliminator = if indno = 0 then eliminator @@ -96,52 +124,91 @@ let rec mk_rels consno = function | 0 -> [] | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1) +let rec strip_pi = function + | Cic.Prod (_, _, tgt) -> strip_pi tgt + | t -> t + +let rec count_pi = function + | Cic.Prod (_, _, tgt) -> count_pi tgt + 1 + | t -> 0 + +let rec type_of_p 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 + | t -> + if dependent then + Cic.Prod (Cic.Anonymous, indty, + Cic.Sort (Cic.Type (CicUniv.fresh ()))) + else + Cic.Sort (Cic.Type (CicUniv.fresh ())) + +let rec add_right_pi dependent strip liftno 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) + | Cic.Prod (_, _, tgt) -> + add_right_pi dependent (strip - 1) liftno rightno indty tgt + | t -> + if dependent then + Cic.Prod (fresh_binder dependent, + CicSubstitution.lift_from (rightno + 1) liftno indty, + Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1))) + else + Cic.Prod (Cic.Anonymous, + CicSubstitution.lift_from (rightno + 1) liftno indty, + if rightno = 0 then + Cic.Rel (1 + liftno + rightno) + else + Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno)) + let elim_of uri typeno = let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in let subst = [] in match obj with - | Cic.InductiveDefinition (indTypes, params, indno) -> + | Cic.InductiveDefinition (indTypes, params, leftno) -> let (name, inductive, ty, constructors) = try List.nth indTypes typeno with Failure _ -> assert false in + let paramsno = count_pi ty in (* number of (left or right) parameters *) + let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in let conslen = List.length constructors in let consno = ref (conslen + 1) in let indty = let indty = Cic.MutInd (uri, typeno, subst) in - if indno = 0 then + if leftno = 0 then indty else - Cic.Appl (indty :: mk_rels 0 indno) + Cic.Appl (indty :: mk_rels 0 paramsno) in let mk_constructor consno = let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in - if indno = 0 then + if leftno = 0 then constructor else - Cic.Appl (constructor :: mk_rels consno indno) + Cic.Appl (constructor :: mk_rels consno leftno) in let eliminator = - Cic.Prod (Cic.Name "P", - (Cic.Prod (Cic.Anonymous, - indty, - (* Cic.MutInd (uri, typeno, subst), *) - Cic.Sort (Cic.Type (CicUniv.fresh ())))), + let p_ty = type_of_p dependent leftno indty ty in + let final_ty = + add_right_pi dependent leftno (conslen + 1) (paramsno - leftno) + indty ty + in + Cic.Prod (Cic.Name "P", p_ty, (List.fold_right (fun (_, constructor) acc -> decr consno; let p = Cic.Rel !consno in Cic.Prod (Cic.Anonymous, - (delta (uri, typeno, subst) indno !consno constructor p - [mk_constructor !consno]), - acc)) (* lift acc? see assumption above on delta *) + (delta (uri, typeno, subst) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) constructors - (Cic.Prod (Cic.Name (fresh_binder ()), - CicSubstitution.lift (conslen + 1) indty - (* Cic.MutInd (uri, typeno, subst) *), - Cic.Appl [Cic.Rel (2 + conslen); Cic.Rel 1])))) + final_ty)) in - add_params indno ty eliminator + add_params leftno ty eliminator | _ -> assert false