from cic_proof_checking and matita to ocaml/library.
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);;
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 =
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
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
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
cicReduction.mli \
cicTypeChecker.mli \
freshNamesGenerator.mli \
- cicElim.mli \
- cicRecord.mli
+ $(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
# Metadata tools only need zeta-reduction
+++ /dev/null
-(* 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))
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
--- /dev/null
+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
PREDICATES =
INTERFACE_FILES = \
+ cicElim.mli \
+ cicRecord.mli \
libraryMisc.mli \
libraryDb.mli \
coercDb.mli \
--- /dev/null
+(* 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))
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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
--- /dev/null
+(* 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
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)
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])
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)
* 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
projects / helm.git / commitdiff