From d27e9241c554dc82f1e7703d0d3ebec3a66776a7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 14 Jan 2005 17:35:26 +0000 Subject: [PATCH] snapshot, notably: - changed interface, now returns a Cic.obj - added consistency check between generated body and type --- helm/ocaml/cic_proof_checking/cicElim.ml | 204 ++++++++++++---------- helm/ocaml/cic_proof_checking/cicElim.mli | 17 +- 2 files changed, 117 insertions(+), 104 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 28a8ed31b..fb64aae09 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -25,12 +25,15 @@ open Printf +exception Elim_failure of string +exception Can_t_eliminate + let fresh_binder = let counter = ref ~-1 in function | true -> incr counter; - Cic.Name ("elim" ^ string_of_int !counter) + Cic.Name ("e" ^ string_of_int !counter) | _ -> Cic.Anonymous (** verifies if a given inductive type occurs in a term in target position *) @@ -42,6 +45,15 @@ let rec recursive uri typeno subst = function (* | Cic.Appl args -> List.exists (recursive uri typeno subst) args *) | _ -> false + (** given a list of constructor types, return true if at least one of them is + * recursive, false otherwise *) +let recursive_type uri typeno subst constructors = + let rec aux = function + | Cic.Prod (_, src, tgt) -> recursive uri typeno subst src || aux tgt + | _ -> false + in + List.exists (fun (_, ty) -> aux ty) constructors + let unfold_appl = function | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl) | t -> t @@ -118,13 +130,13 @@ 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 = +let rec add_params binder indno ty eliminator = if indno = 0 then eliminator else match ty with - | Cic.Prod (binder, src, tgt) -> - Cic.Prod (binder, src, add_params (indno - 1) tgt eliminator) + | Cic.Prod (name, src, tgt) -> + binder name src (add_params binder (indno - 1) tgt eliminator) | _ -> assert false let rec mk_rels consno = function @@ -181,10 +193,7 @@ function case tgt | t -> Cic.Lambda (fresh_binder true, - CicSubstitution.lift_from (rightno + 1) liftno indty, - case) - -exception Failure of string + CicSubstitution.lift_from (rightno + 1) liftno indty, case) let string_of_sort = function | Cic.Prop -> "Prop" @@ -192,57 +201,6 @@ let string_of_sort = function | 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 - | 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 - 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) dependent leftno !consno - constructor p [mk_constructor !consno]), - acc)) - 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 @@ -254,21 +212,21 @@ let rec branch (uri, typeno, subst) insource paramsno t fix head args = | _ -> 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)) + if insource then + let (lparams, rparams) = split tl paramsno in + Cic.Appl (fix :: rparams @ args) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: 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]) + let src = CicSubstitution.lift 1 src in + branch (uri, typeno, subst) true paramsno src fix head [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) @@ -285,7 +243,7 @@ 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 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 @@ -301,8 +259,7 @@ let body_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = 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))); + raise Can_t_eliminate; let indty = let indty = Cic.MutInd (uri, typeno, subst) in if paramsno = 0 then @@ -317,43 +274,98 @@ let body_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = 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 + 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 eliminator_type = + let cic = + 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) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors final_ty)) in + add_params (fun b s t -> Cic.Prod (b, s, t)) leftno ty cic + in + let consno = ref (conslen + 1) in + let eliminator_body = let fix = Cic.Rel (rightno + 2) in + let is_recursive = recursive_type uri typeno subst constructors in + let recshift = if is_recursive then 1 else 0 in let (_, branches) = List.fold_right (fun (_, ty) (shift, branches) -> - let head = Cic.Rel (rightno + shift + 2) in + let head = Cic.Rel (rightno + shift + 1 + recshift) in let b = - branch (uri, typeno, subst) false (rightno + conslen + 3) leftno - ty fix head [] + branch (uri, typeno, subst) false + (rightno + conslen + 2 + recshift) 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) + let mutcase = + Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 2 + recshift), + Cic.Rel 1, branches) + in + let body = + if is_recursive then + let fixfun = + add_right_lambda dependent leftno (conslen + 2) 2 rightno + indty mutcase ty + in + (* rightno is the decreasing argument, i.e. the argument of + * inductive type *) + Cic.Fix (0, ["f", rightno, final_ty, fixfun]) + else + add_right_lambda dependent leftno (conslen + 1) 1 rightno indty + mutcase ty in - let fix_body = - add_right_lambda dependent leftno (conslen + 1) 1 rightno - indty case ty + let cic = + 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 body)) 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)) + add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic + in +(* +prerr_endline (CicPp.ppterm eliminator_type); +prerr_endline (CicPp.ppterm eliminator_body); +*) + let (computed_type, ugraph) = + try + CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph + with CicTypeChecker.TypeCheckerFailure msg -> + raise (Elim_failure (sprintf + "type checker failure while type checking:\n%s\nerror:\n%s" + (CicPp.ppterm eliminator_body) msg)) + in + if not (fst (CicReduction.are_convertible [] + eliminator_type computed_type ugraph)) + then + raise (Failure (sprintf + "internal error: type mismatch on eliminator type\n%s\n%s" + (CicPp.ppterm eliminator_type) (CicPp.ppterm computed_type))); + let suffix = + match sort with + | Cic.Prop -> "_ind" + | Cic.Set -> "_rec" + | Cic.Type _ -> "_rect" + | _ -> assert false in - add_params leftno ty eliminator + let name = UriManager.name_of_uri uri ^ suffix in + Cic.Constant (name, Some eliminator_body, eliminator_type, []) | _ -> assert false diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index 015b6c9d1..722e52f33 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -23,18 +23,19 @@ * http://helm.cs.unibo.it/ *) -exception Failure of string + (** can't build the required elimination principle (e.g. elimination from Prop + * to Set *) +exception Can_t_eliminate + + (** internal error while generating elimination principle *) +exception Elim_failure of string (** @param sort target sort, defaults to Type * @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 +* @raise Can_t_eliminate +* @return Cic constant corresponding to the required elimination principle *) -val body_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term +val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.obj -- 2.39.2