From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 10:11:00 +0000 (+0000) Subject: Generation of auxiliary lemmas for inductive types and records moved X-Git-Tag: make_still_working~8068 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2034db684e1d295527afad07a94f2f3b6b4ed7e2;p=helm.git Generation of auxiliary lemmas for inductive types and records moved from cic_proof_checking and matita to ocaml/library. --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 0fc5f6ab8..8f417485a 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -633,43 +633,6 @@ let eval_coercion status coercion = let status = add_moo_content moo_content status in { status with proof_status = No_proof } -let generate_elimination_principles uri status = - let status' = ref status in - let elim sort = - try - let uri,obj = CicElim.elim_of ~sort uri 0 in - status' := MatitaSync.add_obj uri obj !status' - with CicElim.Can_t_eliminate -> () - in - try - List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - !status' - with exn -> - MatitaSync.time_travel ~present:!status' ~past:status; - raise exn - -let generate_projections uri fields status = - let projections = CicRecord.projections_of uri fields in - List.fold_left - (fun status (uri, name, bo) -> - try - let ty, ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in - let attrs = [`Class `Projection; `Generated] in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - MatitaSync.add_obj uri obj status - with - CicTypeChecker.TypeCheckerFailure s -> - HLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s)); - status - | CicEnvironment.Object_not_found uri -> - let depend = UriManager.name_of_uri uri in - HLog.message - ("Unable to create projection " ^ name ^ " because it requires " ^ depend); - status - ) status projections - (* to avoid a long list of recursive functions *) let eval_from_moo_ref = ref (fun _ _ _ -> assert false);; @@ -793,7 +756,7 @@ let eval_command opts status cmd = command_error "Proof not completed! metasenv is not empty!"; let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some bo,ty,[],[]) in - MatitaSync.add_obj uri obj status + MatitaSync.add_obj uri obj {status with proof_status = No_proof} | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion | GrafiteAst.Alias (loc, spec) -> let diff = @@ -887,30 +850,8 @@ let eval_command opts status cmd = command_error ( "metasenv not empty while giving a definition with body: " ^ CicMetaSubst.ppmetasenv [] metasenv); - let status' = ref status in - (try - status' := MatitaSync.add_obj uri obj !status'; - (match obj with - | Cic.Constant _ -> () - | Cic.InductiveDefinition (_,_,_,attrs) -> - status' := generate_elimination_principles uri !status'; - let rec get_record_attrs = - function - | [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in - (match get_record_attrs attrs with - | None -> () (* not a record *) - | Some fields -> - status' := generate_projections uri fields !status') - | Cic.CurrentProof _ - | Cic.Variable _ -> assert false); - !status' - with exn -> - MatitaSync.time_travel ~present:!status' ~past:status; - raise exn) - + MatitaSync.add_obj uri obj {status with proof_status = No_proof} + let eval_executable opts status ex = match ex with | GrafiteAst.Tactical (_, tac, None) -> eval_tactical status tac diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 96ec76013..92999a49e 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -116,11 +116,9 @@ let add_aliases_for_object status uri = let add_obj uri obj status = let basedir = Helm_registry.get "matita.basedir" in - let status = - { add_aliases_for_object status uri obj with proof_status = No_proof} - in - LibrarySync.add_obj uri obj basedir; - status + let lemmas = LibrarySync.add_obj uri obj basedir in + List.fold_left add_alias_for_constant + (add_aliases_for_object status uri obj) lemmas let add_obj = let profiler = HExtlib.profile "add_obj" in diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 630876902..06b9188a0 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -22,9 +22,3 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \ freshNamesGenerator.cmi freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \ freshNamesGenerator.cmi -cicElim.cmo: freshNamesGenerator.cmi cicTypeChecker.cmi cicSubstitution.cmi \ - cicReduction.cmi cicPp.cmi cicEnvironment.cmi cicElim.cmi -cicElim.cmx: freshNamesGenerator.cmx cicTypeChecker.cmx cicSubstitution.cmx \ - cicReduction.cmx cicPp.cmx cicEnvironment.cmx cicElim.cmi -cicRecord.cmo: cicSubstitution.cmi cicEnvironment.cmi cicRecord.cmi -cicRecord.cmx: cicSubstitution.cmx cicEnvironment.cmx cicRecord.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index b5d1baa1a..3fbe90ddb 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -14,8 +14,7 @@ INTERFACE_FILES = \ cicReduction.mli \ cicTypeChecker.mli \ freshNamesGenerator.mli \ - cicElim.mli \ - cicRecord.mli + $(NULL) 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 deleted file mode 100644 index 74fa6d038..000000000 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ /dev/null @@ -1,419 +0,0 @@ -(* 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/ - *) - -open Printf - -exception Elim_failure of string Lazy.t -exception Can_t_eliminate - -let debug_print = fun _ -> () -(*let debug_print s = prerr_endline (Lazy.force s) *) - -let counter = ref ~-1 ;; - -let fresh_binder () = Cic.Name "matita_dummy" -(* - incr counter; - Cic.Name ("e" ^ string_of_int !counter) *) - - (** verifies if a given inductive type occurs in a term in target position *) -let rec recursive uri typeno = function - | Cic.Prod (_, _, target) -> recursive uri typeno target - | Cic.MutInd (uri', typeno', []) - | Cic.Appl (Cic.MutInd (uri', typeno', []) :: _) -> - UriManager.eq uri uri' && typeno = typeno' - | _ -> false - - (** given a list of constructor types, return true if at least one of them is - * recursive, false otherwise *) -let recursive_type uri typeno constructors = - let rec aux = function - | Cic.Prod (_, src, tgt) -> recursive uri typeno 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 - -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 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) dependent paramsno consno t p args = - match t with - | Cic.MutInd (uri', typeno', []) when - UriManager.eq uri uri' && typeno = typeno' -> - 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', []) :: tl) when - UriManager.eq uri uri' && typeno = typeno' -> - 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 typeno src then - let args = List.map (CicSubstitution.lift 2) args in - let phi = - let src = CicSubstitution.lift 1 src in - delta (uri, typeno) dependent paramsno consno src - (CicSubstitution.lift 1 p) [Cic.Rel 1] - in - let tgt = CicSubstitution.lift 1 tgt in - Cic.Prod (fresh_binder (), src, - Cic.Prod (Cic.Anonymous, phi, - delta (uri, typeno) 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 (fresh_binder (), src, - delta (uri, typeno) 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) dependent paramsno consno t p args = - let t = strip_left_params consno paramsno t in - delta (ury, typeno) dependent paramsno consno t p args - -let rec add_params binder indno ty eliminator = - if indno = 0 then - eliminator - else - match ty with - | Cic.Prod (name, src, tgt) -> - let name = - match name with - Cic.Name _ -> name - | Cic.Anonymous -> fresh_binder () - in - binder name src (add_params binder (indno - 1) tgt eliminator) - | _ -> assert false - -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 sort dependent leftno indty = function - | Cic.Prod (n, src, tgt) when leftno = 0 -> - let n = - if dependent then - match n with - Cic.Name _ -> n - | Cic.Anonymous -> fresh_binder () - else - n - in - 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 sort) - else - Cic.Sort sort - -let rec add_right_pi dependent strip liftno liftfrom rightno indty = function - | Cic.Prod (_, src, tgt) when strip = 0 -> - Cic.Prod (fresh_binder (), - CicSubstitution.lift_from liftfrom liftno src, - add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt) - | Cic.Prod (_, _, tgt) -> - add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt - | t -> - if dependent then - Cic.Prod (fresh_binder (), - 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 rec add_right_lambda dependent strip liftno liftfrom rightno indty case = -function - | Cic.Prod (_, src, tgt) when strip = 0 -> - Cic.Lambda (fresh_binder (), - CicSubstitution.lift_from liftfrom liftno src, - add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty - case tgt) - | Cic.Prod (_, _, tgt) -> - add_right_lambda true (strip - 1) liftno liftfrom rightno indty - case tgt - | t -> - Cic.Lambda (fresh_binder (), - CicSubstitution.lift_from (rightno + 1) liftno indty, case) - -let rec branch (uri, typeno) insource paramsno t fix head args = - match t with - | Cic.MutInd (uri', typeno', []) when - UriManager.eq uri uri' && typeno = typeno' -> - if insource then - (match args with - | [arg] -> Cic.Appl (fix :: args) - | _ -> Cic.Appl (head :: [Cic.Appl args])) - else - (match args with - | [] -> head - | _ -> Cic.Appl (head :: args)) - | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when - UriManager.eq uri uri' && typeno = typeno' -> - if insource then - let (lparams, rparams) = split tl paramsno in - match args with - | [arg] -> Cic.Appl (fix :: rparams @ args) - | _ -> Cic.Appl (fix :: rparams @ [Cic.Appl args]) - else - (match args with - | [] -> head - | _ -> Cic.Appl (head :: args)) - | Cic.Prod (binder, src, tgt) -> - if recursive uri typeno src then - let args = List.map (CicSubstitution.lift 1) args in - let phi = - let fix = CicSubstitution.lift 1 fix in - let src = CicSubstitution.lift 1 src in - branch (uri, typeno) true paramsno src fix head [Cic.Rel 1] - in - Cic.Lambda (fresh_binder (), src, - branch (uri, typeno) 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 (), src, - branch (uri, typeno) insource paramsno tgt - (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) - (args @ [Cic.Rel 1])) - | _ -> assert false - -let branch (uri, typeno) insource liftno paramsno t fix head args = - let t = strip_left_params liftno paramsno t in - branch (uri, typeno) insource paramsno t fix head args - -let elim_of ~sort uri typeno = - counter := ~-1; - let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) 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 head = - match strip_pi ty with - Cic.Sort s -> s - | _ -> assert false - in - let conslen = List.length constructors in - let consno = ref (conslen + 1) in - if - not - (CicTypeChecker.check_allowed_sort_elimination uri typeno head sort) - then - raise Can_t_eliminate; - let indty = - let indty = Cic.MutInd (uri, typeno, []) 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, []) in - if leftno = 0 then - constructor - else - Cic.Appl (constructor :: mk_rels consno leftno) - in - 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) 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 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 + 1 + recshift) in - let b = - branch (uri, typeno) false - (rightno + conslen + 2 + recshift) leftno ty fix head [] - in - (shift + 1, b :: branches)) - constructors (1, []) - in - let shiftno = conslen + rightno + 2 + recshift in - let outtype = - if dependent then - Cic.Rel shiftno - else - let head = - if rightno = 0 then - CicSubstitution.lift 1 (Cic.Rel shiftno) - else - Cic.Appl - ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) :: - mk_rels 1 rightno) - in - add_right_lambda true leftno shiftno 1 rightno indty head ty - in - let mutcase = - Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches) - in - let body = - if is_recursive then - let fixfun = - add_right_lambda dependent leftno (conslen + 2) 1 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 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 (), - (delta (uri, typeno) dependent leftno !consno - constructor p [mk_constructor !consno]), - acc)) - constructors body)) - in - add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic - in -(* -debug_print (lazy (CicPp.ppterm eliminator_type)); -debug_print (lazy (CicPp.ppterm eliminator_body)); -*) - let eliminator_type = - FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in - let eliminator_body = - FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in -(* -debug_print (lazy (CicPp.ppterm eliminator_type)); -debug_print (lazy (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 (lazy (sprintf - "type checker failure while type checking:\n%s\nerror:\n%s" - (CicPp.ppterm eliminator_body) (Lazy.force 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 - let name = UriManager.name_of_uri uri ^ suffix in - let buri = UriManager.buri_of_uri uri in - let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in - let obj_attrs = [`Class (`Elim sort); `Generated] in - uri, - Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) - | _ -> - failwith (sprintf "not an inductive definition (%s)" - (UriManager.string_of_uri uri)) - diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli deleted file mode 100644 index f1f84c92e..000000000 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ /dev/null @@ -1,41 +0,0 @@ -(* 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/ - *) - - (** 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 Lazy.t - -(** @param sort target sort -* @param uri inductive type uri -* @param typeno inductive type number -* @raise Failure -* @raise Can_t_eliminate -* @return Cic constant corresponding to the required elimination principle -* and its uri -*) -val elim_of: sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml deleted file mode 100644 index a251bad87..000000000 --- a/helm/ocaml/cic_proof_checking/cicRecord.ml +++ /dev/null @@ -1,91 +0,0 @@ -(* Copyright (C) 2004-2005, 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 rec_ty uri leftno = - let rec_ty = Cic.MutInd (uri,0,[]) in - if leftno = 0 then rec_ty else - Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0)) - -let generate_one_proj uri params paramsno fields t i = - let mk_lambdas l start = - List.fold_right (fun (name,ty) acc -> - Cic.Lambda (Cic.Name name,ty,acc)) l start in - let recty = rec_ty uri paramsno in - let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in - Some - (mk_lambdas params - (Cic.Lambda (Cic.Name "w", recty, - Cic.MutCase (uri,0,outtype, Cic.Rel 1, - [mk_lambdas fields (Cic.Rel i)])))) - -let projections_of uri field_names = - let buri = UriManager.buri_of_uri uri in - let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in - match obj with - Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) -> - assert (params = []); (* general case not implemented *) - let leftparams,ty = - let rec aux = - function - 0,ty -> [],ty - | n,Cic.Prod (Cic.Name name,s,t) -> - let leftparams,ty = aux (n - 1,t) in - (name,s)::leftparams,ty - | _,_ -> assert false - in - aux (paramsno,ty) - in - let fields = - let rec aux = - function - Cic.MutInd _, [] - | Cic.Appl _, [] -> [] - | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl) - | _,_ -> assert false - in - aux ((CicSubstitution.lift 1 ty),field_names) - in - let rec aux i = - function - Cic.MutInd _, [] - | Cic.Appl _, [] -> [] - | Cic.Prod (_,s,t), name::tl -> - (match generate_one_proj uri leftparams paramsno fields s i with - Some p -> - let puri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - (puri,name,p) :: - aux (i - 1) - (CicSubstitution.subst - (Cic.Appl - (Cic.Const (puri,[]) :: - CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) - ) t, tl) - | None -> assert false) - | _,_ -> assert false - in - aux (List.length fields) (CicSubstitution.lift 2 ty,field_names) - | _ -> assert false diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli deleted file mode 100644 index b966f317c..000000000 --- a/helm/ocaml/cic_proof_checking/cicRecord.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* Copyright (C) 2004-2005, 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/ - *) - -(** projections_of [uri] returns uri * name * term *) -val projections_of: - UriManager.uri -> string list -> (UriManager.uri * string * Cic.term) list diff --git a/helm/ocaml/library/.depend b/helm/ocaml/library/.depend new file mode 100644 index 000000000..34914e505 --- /dev/null +++ b/helm/ocaml/library/.depend @@ -0,0 +1,18 @@ +cicElim.cmo: cicElim.cmi +cicElim.cmx: cicElim.cmi +cicRecord.cmo: cicRecord.cmi +cicRecord.cmx: cicRecord.cmi +libraryMisc.cmo: libraryMisc.cmi +libraryMisc.cmx: libraryMisc.cmi +libraryDb.cmo: libraryDb.cmi +libraryDb.cmx: libraryDb.cmi +coercDb.cmo: coercDb.cmi +coercDb.cmx: coercDb.cmi +librarySync.cmo: libraryDb.cmi coercDb.cmi cicRecord.cmi cicElim.cmi \ + librarySync.cmi +librarySync.cmx: libraryDb.cmx coercDb.cmx cicRecord.cmx cicElim.cmx \ + librarySync.cmi +libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ + libraryClean.cmi +libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ + libraryClean.cmi diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile index e50f03e93..d64c5020f 100644 --- a/helm/ocaml/library/Makefile +++ b/helm/ocaml/library/Makefile @@ -2,6 +2,8 @@ PACKAGE = library PREDICATES = INTERFACE_FILES = \ + cicElim.mli \ + cicRecord.mli \ libraryMisc.mli \ libraryDb.mli \ coercDb.mli \ diff --git a/helm/ocaml/library/cicElim.ml b/helm/ocaml/library/cicElim.ml new file mode 100644 index 000000000..74fa6d038 --- /dev/null +++ b/helm/ocaml/library/cicElim.ml @@ -0,0 +1,419 @@ +(* 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/ + *) + +open Printf + +exception Elim_failure of string Lazy.t +exception Can_t_eliminate + +let debug_print = fun _ -> () +(*let debug_print s = prerr_endline (Lazy.force s) *) + +let counter = ref ~-1 ;; + +let fresh_binder () = Cic.Name "matita_dummy" +(* + incr counter; + Cic.Name ("e" ^ string_of_int !counter) *) + + (** verifies if a given inductive type occurs in a term in target position *) +let rec recursive uri typeno = function + | Cic.Prod (_, _, target) -> recursive uri typeno target + | Cic.MutInd (uri', typeno', []) + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: _) -> + UriManager.eq uri uri' && typeno = typeno' + | _ -> false + + (** given a list of constructor types, return true if at least one of them is + * recursive, false otherwise *) +let recursive_type uri typeno constructors = + let rec aux = function + | Cic.Prod (_, src, tgt) -> recursive uri typeno 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 + +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 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) dependent paramsno consno t p args = + match t with + | Cic.MutInd (uri', typeno', []) when + UriManager.eq uri uri' && typeno = typeno' -> + 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', []) :: tl) when + UriManager.eq uri uri' && typeno = typeno' -> + 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 typeno src then + let args = List.map (CicSubstitution.lift 2) args in + let phi = + let src = CicSubstitution.lift 1 src in + delta (uri, typeno) dependent paramsno consno src + (CicSubstitution.lift 1 p) [Cic.Rel 1] + in + let tgt = CicSubstitution.lift 1 tgt in + Cic.Prod (fresh_binder (), src, + Cic.Prod (Cic.Anonymous, phi, + delta (uri, typeno) 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 (fresh_binder (), src, + delta (uri, typeno) 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) dependent paramsno consno t p args = + let t = strip_left_params consno paramsno t in + delta (ury, typeno) dependent paramsno consno t p args + +let rec add_params binder indno ty eliminator = + if indno = 0 then + eliminator + else + match ty with + | Cic.Prod (name, src, tgt) -> + let name = + match name with + Cic.Name _ -> name + | Cic.Anonymous -> fresh_binder () + in + binder name src (add_params binder (indno - 1) tgt eliminator) + | _ -> assert false + +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 sort dependent leftno indty = function + | Cic.Prod (n, src, tgt) when leftno = 0 -> + let n = + if dependent then + match n with + Cic.Name _ -> n + | Cic.Anonymous -> fresh_binder () + else + n + in + 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 sort) + else + Cic.Sort sort + +let rec add_right_pi dependent strip liftno liftfrom rightno indty = function + | Cic.Prod (_, src, tgt) when strip = 0 -> + Cic.Prod (fresh_binder (), + CicSubstitution.lift_from liftfrom liftno src, + add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt) + | Cic.Prod (_, _, tgt) -> + add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt + | t -> + if dependent then + Cic.Prod (fresh_binder (), + 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 rec add_right_lambda dependent strip liftno liftfrom rightno indty case = +function + | Cic.Prod (_, src, tgt) when strip = 0 -> + Cic.Lambda (fresh_binder (), + CicSubstitution.lift_from liftfrom liftno src, + add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty + case tgt) + | Cic.Prod (_, _, tgt) -> + add_right_lambda true (strip - 1) liftno liftfrom rightno indty + case tgt + | t -> + Cic.Lambda (fresh_binder (), + CicSubstitution.lift_from (rightno + 1) liftno indty, case) + +let rec branch (uri, typeno) insource paramsno t fix head args = + match t with + | Cic.MutInd (uri', typeno', []) when + UriManager.eq uri uri' && typeno = typeno' -> + if insource then + (match args with + | [arg] -> Cic.Appl (fix :: args) + | _ -> Cic.Appl (head :: [Cic.Appl args])) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when + UriManager.eq uri uri' && typeno = typeno' -> + if insource then + let (lparams, rparams) = split tl paramsno in + match args with + | [arg] -> Cic.Appl (fix :: rparams @ args) + | _ -> Cic.Appl (fix :: rparams @ [Cic.Appl args]) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) + | Cic.Prod (binder, src, tgt) -> + if recursive uri typeno src then + let args = List.map (CicSubstitution.lift 1) args in + let phi = + let fix = CicSubstitution.lift 1 fix in + let src = CicSubstitution.lift 1 src in + branch (uri, typeno) true paramsno src fix head [Cic.Rel 1] + in + Cic.Lambda (fresh_binder (), src, + branch (uri, typeno) 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 (), src, + branch (uri, typeno) insource paramsno tgt + (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) + (args @ [Cic.Rel 1])) + | _ -> assert false + +let branch (uri, typeno) insource liftno paramsno t fix head args = + let t = strip_left_params liftno paramsno t in + branch (uri, typeno) insource paramsno t fix head args + +let elim_of ~sort uri typeno = + counter := ~-1; + let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) 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 head = + match strip_pi ty with + Cic.Sort s -> s + | _ -> assert false + in + let conslen = List.length constructors in + let consno = ref (conslen + 1) in + if + not + (CicTypeChecker.check_allowed_sort_elimination uri typeno head sort) + then + raise Can_t_eliminate; + let indty = + let indty = Cic.MutInd (uri, typeno, []) 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, []) in + if leftno = 0 then + constructor + else + Cic.Appl (constructor :: mk_rels consno leftno) + in + 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) 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 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 + 1 + recshift) in + let b = + branch (uri, typeno) false + (rightno + conslen + 2 + recshift) leftno ty fix head [] + in + (shift + 1, b :: branches)) + constructors (1, []) + in + let shiftno = conslen + rightno + 2 + recshift in + let outtype = + if dependent then + Cic.Rel shiftno + else + let head = + if rightno = 0 then + CicSubstitution.lift 1 (Cic.Rel shiftno) + else + Cic.Appl + ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) :: + mk_rels 1 rightno) + in + add_right_lambda true leftno shiftno 1 rightno indty head ty + in + let mutcase = + Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches) + in + let body = + if is_recursive then + let fixfun = + add_right_lambda dependent leftno (conslen + 2) 1 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 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 (), + (delta (uri, typeno) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors body)) + in + add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic + in +(* +debug_print (lazy (CicPp.ppterm eliminator_type)); +debug_print (lazy (CicPp.ppterm eliminator_body)); +*) + let eliminator_type = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in + let eliminator_body = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in +(* +debug_print (lazy (CicPp.ppterm eliminator_type)); +debug_print (lazy (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 (lazy (sprintf + "type checker failure while type checking:\n%s\nerror:\n%s" + (CicPp.ppterm eliminator_body) (Lazy.force 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 + let name = UriManager.name_of_uri uri ^ suffix in + let buri = UriManager.buri_of_uri uri in + let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in + let obj_attrs = [`Class (`Elim sort); `Generated] in + uri, + Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) + | _ -> + failwith (sprintf "not an inductive definition (%s)" + (UriManager.string_of_uri uri)) + diff --git a/helm/ocaml/library/cicElim.mli b/helm/ocaml/library/cicElim.mli new file mode 100644 index 000000000..f1f84c92e --- /dev/null +++ b/helm/ocaml/library/cicElim.mli @@ -0,0 +1,41 @@ +(* 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/ + *) + + (** 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 Lazy.t + +(** @param sort target sort +* @param uri inductive type uri +* @param typeno inductive type number +* @raise Failure +* @raise Can_t_eliminate +* @return Cic constant corresponding to the required elimination principle +* and its uri +*) +val elim_of: sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj diff --git a/helm/ocaml/library/cicRecord.ml b/helm/ocaml/library/cicRecord.ml new file mode 100644 index 000000000..a251bad87 --- /dev/null +++ b/helm/ocaml/library/cicRecord.ml @@ -0,0 +1,91 @@ +(* Copyright (C) 2004-2005, 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 rec_ty uri leftno = + let rec_ty = Cic.MutInd (uri,0,[]) in + if leftno = 0 then rec_ty else + Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0)) + +let generate_one_proj uri params paramsno fields t i = + let mk_lambdas l start = + List.fold_right (fun (name,ty) acc -> + Cic.Lambda (Cic.Name name,ty,acc)) l start in + let recty = rec_ty uri paramsno in + let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in + Some + (mk_lambdas params + (Cic.Lambda (Cic.Name "w", recty, + Cic.MutCase (uri,0,outtype, Cic.Rel 1, + [mk_lambdas fields (Cic.Rel i)])))) + +let projections_of uri field_names = + let buri = UriManager.buri_of_uri uri in + let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in + match obj with + Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) -> + assert (params = []); (* general case not implemented *) + let leftparams,ty = + let rec aux = + function + 0,ty -> [],ty + | n,Cic.Prod (Cic.Name name,s,t) -> + let leftparams,ty = aux (n - 1,t) in + (name,s)::leftparams,ty + | _,_ -> assert false + in + aux (paramsno,ty) + in + let fields = + let rec aux = + function + Cic.MutInd _, [] + | Cic.Appl _, [] -> [] + | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl) + | _,_ -> assert false + in + aux ((CicSubstitution.lift 1 ty),field_names) + in + let rec aux i = + function + Cic.MutInd _, [] + | Cic.Appl _, [] -> [] + | Cic.Prod (_,s,t), name::tl -> + (match generate_one_proj uri leftparams paramsno fields s i with + Some p -> + let puri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + (puri,name,p) :: + aux (i - 1) + (CicSubstitution.subst + (Cic.Appl + (Cic.Const (puri,[]) :: + CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) + ) t, tl) + | None -> assert false) + | _,_ -> assert false + in + aux (List.length fields) (CicSubstitution.lift 2 ty,field_names) + | _ -> assert false diff --git a/helm/ocaml/library/cicRecord.mli b/helm/ocaml/library/cicRecord.mli new file mode 100644 index 000000000..b966f317c --- /dev/null +++ b/helm/ocaml/library/cicRecord.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2004-2005, 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/ + *) + +(** projections_of [uri] returns uri * name * term *) +val projections_of: + UriManager.uri -> string list -> (UriManager.uri * string * Cic.term) list diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index d853243dd..4aa966947 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -92,7 +92,7 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_obj uri obj ~basedir = +let add_single_obj uri obj ~basedir = let dbd = LibraryDb.instance () in if CicEnvironment.in_library uri then raise (AlreadyDefined uri) @@ -119,7 +119,7 @@ let add_obj uri obj ~basedir = raise exc end -let remove_obj uri = +let remove_single_obj uri = let derived_uris_of_uri uri = let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) @@ -140,3 +140,88 @@ let remove_obj uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri); CicEnvironment.remove_obj uri) to_remove + +(*** GENERATION OF AUXILIARY LEMMAS ***) + +let generate_elimination_principles ~basedir uri = + let uris = ref [] in + let elim sort = + try + let uri,obj = CicElim.elim_of ~sort uri 0 in + add_single_obj uri obj ~basedir; + uris := uri :: !uris + with CicElim.Can_t_eliminate -> () + in + try + List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + !uris + with exn -> + List.iter remove_single_obj !uris; + raise exn + +let generate_projections ~basedir uri fields = + let uris = ref [] in + let projections = CicRecord.projections_of uri fields in + try + List.iter + (fun (uri, name, bo) -> + try + let ty, ugraph = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let attrs = [`Class `Projection; `Generated] in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj ~basedir uri obj; + uris := uri :: !uris + with + CicTypeChecker.TypeCheckerFailure s -> + HLog.message + ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s); + | CicEnvironment.Object_not_found uri -> + let depend = UriManager.name_of_uri uri in + HLog.message + ("Unable to create projection " ^ name ^ " because it requires " ^ + depend) + ) projections; + !uris + with exn -> + List.iter remove_single_obj !uris; + raise exn + +let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 + +let add_obj uri obj ~basedir = + add_single_obj uri obj ~basedir; + let uris = ref [] in + try + begin + match obj with + | Cic.Constant _ -> () + | Cic.InductiveDefinition (_,_,_,attrs) -> + uris := !uris @ generate_elimination_principles ~basedir uri; + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + | None -> () (* not a record *) + | Some fields -> + uris := !uris @ (generate_projections ~basedir uri fields)) + | Cic.CurrentProof _ + | Cic.Variable _ -> assert false + end; + UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; + !uris + with exn -> + List.iter remove_single_obj !uris; + raise exn + +let remove_obj uri = + let uris = + try + UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri + with + Not_found -> [] + in + List.iter remove_single_obj (uri::uris) diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli index 0e0916e4d..89262e393 100644 --- a/helm/ocaml/library/librarySync.mli +++ b/helm/ocaml/library/librarySync.mli @@ -23,9 +23,12 @@ * http://helm.cs.unibo.it/ *) -(* returns a list of added URIs and their paths on disk *) -(*CSC: the path on disk should be computable from the URI!!! *) -val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> unit +(* adds an object to the library together with all auxiliary lemmas on it *) +(* (e.g. elimination principles, projections, etc.) *) +(* it returns the list of the uris of the auxiliary lemmas generated *) +val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list -(* inverse of add_obj; it does not remove the objects depending on it! *) +(* inverse of add_obj; *) +(* Warning: it does not remove the dependencies on the object and on its *) +(* auxiliary lemmas! *) val remove_obj: UriManager.uri -> unit