From cbd78f48f8aa055e2d66922291717842d84383d1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 21 Dec 2004 15:49:03 +0000 Subject: [PATCH] first commit (in the wrong place --by CSC) of induction principles generation --- helm/ocaml/cic_proof_checking/.depend | 18 +-- helm/ocaml/cic_proof_checking/Makefile | 12 +- helm/ocaml/cic_proof_checking/cicElim.ml | 147 ++++++++++++++++++++++ helm/ocaml/cic_proof_checking/cicElim.mli | 30 +++++ 4 files changed, 196 insertions(+), 11 deletions(-) create mode 100644 helm/ocaml/cic_proof_checking/cicElim.ml create mode 100644 helm/ocaml/cic_proof_checking/cicElim.mli diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 808126a3f..c212f6cad 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -10,15 +10,17 @@ cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi -cicReductionNaif.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ +cicReductionNaif.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \ cicReductionNaif.cmi -cicReductionNaif.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ +cicReductionNaif.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \ cicReductionNaif.cmi -cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ +cicReduction.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \ cicReduction.cmi -cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ +cicReduction.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \ cicReduction.cmi -cicTypeChecker.cmo: cicEnvironment.cmi cicLogger.cmi cicPp.cmi \ - cicReduction.cmi cicSubstitution.cmi cicTypeChecker.cmi -cicTypeChecker.cmx: cicEnvironment.cmx cicLogger.cmx cicPp.cmx \ - cicReduction.cmx cicSubstitution.cmx cicTypeChecker.cmi +cicTypeChecker.cmo: cicSubstitution.cmi cicReduction.cmi cicPp.cmi \ + cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi +cicTypeChecker.cmx: cicSubstitution.cmx cicReduction.cmx cicPp.cmx \ + cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi +cicElim.cmo: cicSubstitution.cmi cicEnvironment.cmi cicElim.cmi +cicElim.cmx: cicSubstitution.cmx cicEnvironment.cmx cicElim.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 5a5e21389..c8828a224 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -7,9 +7,15 @@ REDUCTION_IMPLEMENTATION = cicReductionMachine.ml INTERFACE_FILES = \ cicLogger.mli \ - cicEnvironment.mli cicUnivUtils.mli cicPp.mli cicSubstitution.mli \ - cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ - cicTypeChecker.mli + cicEnvironment.mli \ + cicUnivUtils.mli \ + cicPp.mli \ + cicSubstitution.mli \ + cicMiniReduction.mli \ + cicReductionNaif.mli \ + cicReduction.mli \ + cicTypeChecker.mli \ + cicElim.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml new file mode 100644 index 000000000..93d64a12c --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -0,0 +1,147 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let fresh_binder = + let counter = ref ~-1 in + fun () -> + incr counter; + "elim" ^ string_of_int !counter + + (** 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' + | _ -> false + +let unfold_appl = function + | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl) + | t -> t + + (** 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 = + 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 + UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> + Cic.Appl (Cic.Rel p_rel :: args) +*) + | Cic.Prod (binder, src, tgt) when strip = 0 -> + if recursive uri src then + let args = List.map (CicSubstitution.lift 2) args in + let phi = + (delta (uri, typeno, subst) strip consno src + (CicSubstitution.lift 1 p) [Cic.Rel 1]) + in + Cic.Prod (Cic.Name (fresh_binder ()), src, + Cic.Prod (Cic.Anonymous, phi, + delta (uri, typeno, subst) strip 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 + | _ -> assert false + +let rec add_params 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) + | _ -> assert false + +let rec mk_rels consno = function + | 0 -> [] + | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1) + +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) -> + let (name, inductive, ty, constructors) = + try + List.nth indTypes typeno + with Failure _ -> assert false + 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 + indty + else + Cic.Appl (indty :: mk_rels 0 indno) + in + let mk_constructor consno = + let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in + if indno = 0 then + constructor + else + Cic.Appl (constructor :: mk_rels consno indno) + in + let eliminator = + Cic.Prod (Cic.Name "P", + (Cic.Prod (Cic.Anonymous, + indty, + (* Cic.MutInd (uri, typeno, subst), *) + Cic.Sort (Cic.Type (CicUniv.fresh ())))), + (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 *) + 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])))) + in + add_params indno ty eliminator + | _ -> assert false + diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli new file mode 100644 index 000000000..828028d0a --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(** @param uri inductive type uri +* @param typeno inductive type number +*) +val elim_of: UriManager.uri -> int -> Cic.term + -- 2.39.2