From 086099d1a60948454cf0874744ef2222c2edc1b6 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 13 Jan 2005 07:08:55 +0000 Subject: [PATCH] snapshot (1st commit of fix body generation) --- helm/ocaml/cic_proof_checking/cicElim.ml | 153 ++++++++++++++++++++-- helm/ocaml/cic_proof_checking/cicElim.mli | 6 + 2 files changed, 148 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 77304c1ec..28a8ed31b 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -33,11 +33,13 @@ let fresh_binder = 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', _, _) -> UriManager.eq uri uri' - | Cic.Appl args -> List.exists (recursive uri) args + (** verifies if a given inductive type occurs in a term in target position *) +let rec recursive uri typeno subst = function + | Cic.Prod (_, _, target) -> recursive uri typeno subst target + | Cic.MutInd (uri', typeno', subst') + | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) -> + UriManager.eq uri uri' && typeno = typeno' && subst = subst' +(* | Cic.Appl args -> List.exists (recursive uri typeno subst) args *) | _ -> false let unfold_appl = function @@ -57,7 +59,8 @@ let rec split l n = let rec delta (uri, typeno, subst) dependent paramsno consno t p args = assert (subst = []); match t with - | Cic.MutInd (uri', typeno', subst') -> + | Cic.MutInd (uri', typeno', subst') when + UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> if dependent then (match args with | [] -> assert false @@ -80,7 +83,7 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args = | [] -> p | _ -> Cic.Appl (p :: rparams)) | Cic.Prod (binder, src, tgt) -> - if recursive uri src then + if recursive uri typeno subst src then let args = List.map (CicSubstitution.lift 2) args in let phi = let src = CicSubstitution.lift 1 src in @@ -166,6 +169,21 @@ let rec add_right_pi dependent strip liftno liftfrom rightno indty = function else Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno)) +let rec add_right_lambda dependent strip liftno liftfrom rightno indty case = +function + | Cic.Prod (_, src, tgt) when strip = 0 -> + Cic.Lambda (fresh_binder true, + CicSubstitution.lift_from (liftfrom + 1) liftno src, + add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty + case tgt) + | Cic.Prod (_, _, tgt) -> + add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty + case tgt + | t -> + Cic.Lambda (fresh_binder true, + CicSubstitution.lift_from (rightno + 1) liftno indty, + case) + exception Failure of string let string_of_sort = function @@ -185,6 +203,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = with Failure _ -> assert false in let paramsno = count_pi ty in (* number of (left or right) parameters *) + let rightno = paramsno - leftno in let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in let conslen = List.length constructors in let consno = ref (conslen + 1) in @@ -208,8 +227,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = let eliminator = let p_ty = type_of_p sort dependent leftno indty ty in let final_ty = - add_right_pi dependent leftno (conslen + 1) 1 (paramsno - leftno) - indty ty + add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty in Cic.Prod (Cic.Name "P", p_ty, (List.fold_right @@ -220,8 +238,121 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = (delta (uri, typeno, subst) dependent leftno !consno constructor p [mk_constructor !consno]), acc)) - constructors - final_ty)) + constructors final_ty)) + in + add_params leftno ty eliminator + | _ -> assert false + +let rec branch (uri, typeno, subst) insource paramsno t fix head args = + assert (subst = []); + match t with + | Cic.MutInd (uri', typeno', subst') when + UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> + let head = if insource then fix else head in + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) + | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when + UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> + let (lparams, rparams) = split tl paramsno in + (match args with + | [] when insource && rparams = [] -> fix + | [] when insource -> Cic.Appl (fix :: rparams) + | _ when insource -> Cic.Appl (fix :: rparams @ args) + | _ -> Cic.Appl (head :: rparams @ args)) + | Cic.Prod (binder, src, tgt) -> + if recursive uri typeno subst src then + let args = List.map (CicSubstitution.lift 1) args in + let phi = + let fix = CicSubstitution.lift 1 fix in + branch (uri, typeno, subst) true paramsno src fix head + (args @ [Cic.Rel 1]) + in + let tgt = CicSubstitution.lift 1 tgt in + Cic.Lambda (fresh_binder true, src, + branch (uri, typeno, subst) insource paramsno tgt + (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) + (args @ [Cic.Rel 1; phi])) + else (* non recursive *) + let args = List.map (CicSubstitution.lift 1) args in + Cic.Lambda (fresh_binder true, src, + branch (uri, typeno, subst) insource paramsno tgt + (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) + (args @ [Cic.Rel 1])) + | _ -> assert false + +let branch (uri, typeno, subst) insource liftno paramsno t fix head args = + let t = strip_left_params liftno paramsno t in + branch (uri, typeno, subst) insource paramsno t fix head args + +let body_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 + | 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 rightno = paramsno - leftno in + 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 paramsno = 0 then + indty + else + Cic.Appl (indty :: mk_rels 0 paramsno) + in + let mk_constructor consno = + let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in + if leftno = 0 then + constructor + else + Cic.Appl (constructor :: mk_rels consno leftno) + in + let eliminator = + let p_ty = type_of_p sort dependent leftno indty ty in + let final_ty = + add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty + in + let fix = Cic.Rel (rightno + 2) in + let (_, branches) = + List.fold_right + (fun (_, ty) (shift, branches) -> + let head = Cic.Rel (rightno + shift + 2) in + let b = + branch (uri, typeno, subst) false (rightno + conslen + 3) leftno + ty fix head [] + in + (shift + 1, b :: branches)) + constructors (1, []) + in + let case = + Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 3), Cic.Rel 1, + branches) + in + let fix_body = + add_right_lambda dependent leftno (conslen + 1) 1 rightno + indty case ty + in + let fix = Cic.Fix (0, ["f", 0, final_ty, fix_body]) in + Cic.Lambda (Cic.Name "P", p_ty, + (List.fold_right + (fun (_, constructor) acc -> + decr consno; + let p = Cic.Rel !consno in + Cic.Lambda (fresh_binder true, + (delta (uri, typeno, subst) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors fix)) in add_params leftno ty eliminator | _ -> assert false diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index b341d36a4..015b6c9d1 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -29,6 +29,12 @@ exception Failure of string * @param uri inductive type uri * @param typeno inductive type number * @raise Failure +* @return type of elimination principle for the given inductive type *) val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term +(** parameters as above +* @return body of elimination principle for the given inductive type +*) +val body_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term + -- 2.39.2