From a25ab736af3b79559ceae828558195e1deb51a29 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 11 Jan 2000 09:38:09 +0000 Subject: Ajout de Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@275 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 66 ++++--- Makefile | 4 +- pretyping/class.ml | 459 ++++++++++++++++++++++++++++++++++++++++++++ pretyping/class.mli | 26 +++ pretyping/recordops.ml | 4 +- pretyping/recordops.mli | 10 +- toplevel/class.ml | 474 ---------------------------------------------- toplevel/class.mli | 26 --- toplevel/command.ml | 15 +- toplevel/discharge.ml | 6 +- toplevel/record.ml | 127 ++++++------- toplevel/record.mli | 2 +- toplevel/vernacentries.ml | 25 ++- 13 files changed, 611 insertions(+), 633 deletions(-) create mode 100644 pretyping/class.ml create mode 100644 pretyping/class.mli delete mode 100644 toplevel/class.ml delete mode 100644 toplevel/class.mli diff --git a/.depend b/.depend index ac0d842998..6dfd64e554 100644 --- a/.depend +++ b/.depend @@ -77,6 +77,8 @@ pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ kernel/type_errors.cmi pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi +pretyping/class.cmi: pretyping/classops.cmi library/declare.cmi \ + kernel/names.cmi kernel/term.cmi pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ library/libobject.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \ kernel/term.cmi @@ -156,8 +158,6 @@ tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \ tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi -toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \ - kernel/names.cmi kernel/term.cmi toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \ pretyping/tacred.cmi kernel/term.cmi toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi @@ -499,6 +499,16 @@ pretyping/cases.cmx: kernel/environ.cmx pretyping/evarconv.cmx \ pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/cases.cmi +pretyping/class.cmo: pretyping/classops.cmi kernel/constant.cmi \ + library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ + library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \ + library/lib.cmi kernel/names.cmi lib/pp.cmi pretyping/retyping.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/class.cmi +pretyping/class.cmx: pretyping/classops.cmx kernel/constant.cmx \ + library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ + library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \ + library/lib.cmx kernel/names.cmx lib/pp.cmx pretyping/retyping.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/class.cmi pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \ kernel/generic.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \ lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi library/summary.cmi \ @@ -825,16 +835,6 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi tools/coqdep.cmo: config/coq_config.cmi tools/coqdep.cmx: config/coq_config.cmx -toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \ - library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ - library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \ - library/lib.cmi kernel/names.cmi lib/pp.cmi pretyping/retyping.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi toplevel/class.cmi -toplevel/class.cmx: pretyping/classops.cmx kernel/constant.cmx \ - library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ - library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \ - library/lib.cmx kernel/names.cmx lib/pp.cmx pretyping/retyping.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx toplevel/class.cmi toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \ parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi library/indrec.cmi \ @@ -865,14 +865,14 @@ toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \ toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/profile.cmx \ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi -toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \ +toplevel/discharge.cmo: pretyping/class.cmi pretyping/classops.cmi \ kernel/constant.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi kernel/inductive.cmi \ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \ kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/recordops.cmi \ kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \ kernel/typeops.cmi lib/util.cmi toplevel/discharge.cmi -toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \ +toplevel/discharge.cmx: pretyping/class.cmx pretyping/classops.cmx \ kernel/constant.cmx library/declare.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx library/global.cmx kernel/inductive.cmx \ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \ @@ -925,11 +925,15 @@ toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \ toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmx \ lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \ toplevel/protectedtoplevel.cmi -toplevel/record.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \ - library/declare.cmi library/global.cmi kernel/names.cmi lib/pp.cmi \ +toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi pretyping/class.cmi \ + toplevel/command.cmi kernel/constant.cmi parsing/coqast.cmi \ + library/declare.cmi kernel/environ.cmi kernel/generic.cmi \ + library/global.cmi kernel/names.cmi lib/pp.cmi pretyping/recordops.cmi \ kernel/term.cmi lib/util.cmi toplevel/record.cmi -toplevel/record.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \ - library/declare.cmx library/global.cmx kernel/names.cmx lib/pp.cmx \ +toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx pretyping/class.cmx \ + toplevel/command.cmx kernel/constant.cmx parsing/coqast.cmx \ + library/declare.cmx kernel/environ.cmx kernel/generic.cmx \ + library/global.cmx kernel/names.cmx lib/pp.cmx pretyping/recordops.cmx \ kernel/term.cmx lib/util.cmx toplevel/record.cmi toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \ lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ @@ -950,31 +954,33 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ - toplevel/class.cmi toplevel/command.cmi parsing/coqast.cmi \ + pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \ library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \ kernel/evd.cmi parsing/extend.cmi library/global.cmi library/goptions.cmi \ library/impargs.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi proofs/macros.cmi toplevel/metasyntax.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \ proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - proofs/refiner.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tactics.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi toplevel/vernacentries.cmi + parsing/printer.cmi proofs/proof_trees.cmi toplevel/record.cmi \ + kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \ + lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tactics.cmi kernel/term.cmi \ + kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ - toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \ + pretyping/class.cmx toplevel/command.cmx parsing/coqast.cmx \ library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \ kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \ library/impargs.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx proofs/macros.cmx toplevel/metasyntax.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \ proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ - proofs/refiner.cmx lib/stamps.cmx library/states.cmx lib/system.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tactics.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx toplevel/vernacentries.cmi + parsing/printer.cmx proofs/proof_trees.cmx toplevel/record.cmx \ + kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \ + lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \ + kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \ diff --git a/Makefile b/Makefile index 2d651d905c..af53a8121d 100644 --- a/Makefile +++ b/Makefile @@ -76,7 +76,7 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \ pretyping/tacred.cmo pretyping/pretype_errors.cmo \ pretyping/retyping.cmo pretyping/typing.cmo \ - pretyping/classops.cmo pretyping/recordops.cmo \ + pretyping/classops.cmo pretyping/class.cmo pretyping/recordops.cmo \ pretyping/evarutil.cmo pretyping/evarconv.cmo \ pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \ pretyping/syntax_def.cmo @@ -101,7 +101,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ - toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \ + toplevel/metasyntax.cmo toplevel/command.cmo toplevel/record.cmo \ toplevel/discharge.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \ toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \ diff --git a/pretyping/class.ml b/pretyping/class.ml new file mode 100644 index 0000000000..9b5a02c6f5 --- /dev/null +++ b/pretyping/class.ml @@ -0,0 +1,459 @@ + +(* $Id$ *) + +open Util +open Pp +open Names +open Generic +open Term +open Inductive +open Constant +open Environ +open Lib +open Classops +open Declare + +(* manipulations concernant les strength *) + +(* gt dans le sens de "longueur du sp" (donc le moins persistant) *) + +(* strength * strength -> bool *) + +let stre_gt = function + | (NeverDischarge,NeverDischarge) -> false + | (NeverDischarge,x) -> false + | (x,NeverDischarge) -> true + | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) + +let stre_max (stre1,stre2) = + if stre_gt (stre1,stre2) then stre1 else stre2 + +let stre_max4 stre1 stre2 stre3 stre4 = + stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4))) + +let id_of_varid = function + | VAR id -> id + | _ -> anomaly "class__id_of_varid" + +let stre_of_VAR c = variable_strength (destVar c) + +(* lf liste des variable dont depend la coercion f + lc liste des variable dont depend la classe source *) + +let rec stre_unif_cond = function + | ([],[]) -> NeverDischarge + | (v::l,[]) -> stre_of_VAR v + | ([],v::l) -> stre_of_VAR v + | (v1::l1,v2::l2) -> + if v1=v2 then + stre_unif_cond (l1,l2) + else + let stre1 = (stre_of_VAR v1) + and stre2 = (stre_of_VAR v2) in + stre_max (stre1,stre2) + +let stre_of_coe = function + | NAM_Constant sp -> constant_strength sp + | NAM_Var id -> variable_strength id + | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge + +(* try_add_class : Names.identifier -> + Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *) + +let try_add_class id v clpopt streopt check_exist = + let env = Global.env () in + let t = Retyping.get_type_of env Evd.empty v in + let p1 = + try + arity_sort t + with Not_found -> + errorlabstrm "try_add_class" + [< 'sTR "Type of "; 'sTR (string_of_id id); + 'sTR " does not end with a sort" >] + in + let cl,p = + match clpopt with + | None -> let (cl,_)=constructor_at_head v in (cl,p1) + | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) + in + if check_exist & class_exists cl then + errorlabstrm "try_add_new_class" + [< 'sTR (string_of_id id) ; 'sTR " is already a class" >]; + let stre' = stre_of_cl cl in + let stre = match streopt with + | Some stre -> stre_max (stre,stre') + | None -> stre' + in + add_new_class (cl,(string_of_id id),stre,p); + stre + +(* try_add_new_class : Names.identifier -> unit *) + +let try_add_new_class id stre = + let v = global_reference CCI id in + let _ = try_add_class id v None (Some stre) true in () + +(* check_class : Names.identifier -> + Term.constr -> cl_typ -> int -> int * Libobject.strength *) + +let check_class id v cl p = + try + let _,clinfo = class_info cl in + if p = clinfo.cL_PARAM then + clinfo.cL_STRE + else + errorlabstrm "fully_applied" + [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >] + with Not_found -> + try_add_class id v (Some (cl,p)) None false + + +(* decomposition de constr vers coe_typ *) + +(* t provient de global_reference donc pas de Cast, pas de AppL *) +let coe_of_reference t = + match kind_of_term t with + | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp + | IsMutInd (ind_sp,l) -> (Array.to_list l),NAM_Inductive ind_sp + | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Constructor cstr_sp + | IsVar id -> [],NAM_Var id + | _ -> anomaly "Not a reference" + +let constructor_at_head1 t = + let rec aux t' = + match kind_of_term t' with + | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0 + | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0 + | IsVar id -> t',[],[],CL_Var id,0 + | IsCast (c,_) -> aux c + | IsAppL(f,args) -> + let t',_,l,c,_ = aux f in t',args,l,c,List.length args + | IsProd (_,_,_) -> t',[],[],CL_FUN,0 + | IsSort _ -> t',[],[],CL_SORT,0 + | _ -> raise Not_found + in + aux (collapse_appl t) + + +(* condition d'heritage uniforme *) + +let uniform_cond nargs lt = + let rec aux = function + | (0,[]) -> true + | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l)) + | _ -> false + in + aux (nargs,lt) + +let id_of_cl = function + | CL_FUN -> (id_of_string "FUNCLASS") + | CL_SORT -> (id_of_string "SORTCLASS") + | CL_SP sp -> (basename sp) + | CL_IND (sp,i) -> + (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename + | CL_Var id -> id + +let string_of_cl = function + | CL_FUN -> "FUNCLASS" + | CL_SORT -> "SORTCLASS" + | CL_SP sp -> string_of_id (basename sp) + | CL_IND (sp,i) -> + string_of_id + (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename + | CL_Var id -> string_of_id id + +(* +lp est la liste (inverse'e) des arguments de la coercion +ids est le nom de la classe source +sps_opt est le sp de la classe source dans le cas des structures +retourne: +la classe souce +nbre d'arguments de la classe +le constr de la class +l'indice de la classe source dans la liste lp +la liste des variables dont depend la classe source +*) + +let get_source lp source = + match source with + | None -> + let (v1,lv1,l,cl1,p1) as x = + match lp with + | [] -> raise Not_found + | t1::_ -> + try constructor_at_head1 t1 + with _ -> raise Not_found + in + (id_of_cl cl1),(cl1,p1,v1,lv1,1,l) + | Some id -> + let rec aux n = function + | [] -> raise Not_found + | t1::lt -> + try + let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in + if id_of_cl cl1 = id then cl1,p1,v1,lv1,n,l + else aux (n+1) lt + with _ -> aux (n + 1) lt + in id, aux 1 lp + +let get_target t ind = + if (ind > 1) then + CL_FUN,0,t + else + let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2 + +let prods_of t = + let rec aux acc = function + | DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2 + | (DOP2(Cast,c,_)) -> aux acc c + | t -> t::acc + in + aux [] t + +(* coercion identite' *) + +let lams_of t = + let rec aux acc = function + | DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2 + | DOP2(Cast,c,_) -> aux acc c + | t -> acc,t + in + aux [] t + +let build_id_coercion idf_opt ids = + let env = Global.env () in + let vs = construct_reference env CCI ids in + let c = match (strip_outer_cast vs) with + | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' -> + (try Instantiate.constant_value env c' + with _ -> errorlabstrm "build_id_coercion" + [< 'sTR(string_of_id ids); + 'sTR" must be a transparent constant" >]) + | _ -> + errorlabstrm "build_id_coercion" + [< 'sTR(string_of_id ids); + 'sTR" must be a transparent constant" >] + in + let lams,t = lams_of c in + let lams = List.rev lams in + let llams = List.length lams in + let val_f = + List.fold_right + (fun (x,t) u -> DOP2(Lambda,t,DLAM(x,u))) + lams + (DOP2(Lambda,(applistc vs (rel_list 0 llams)), + DLAM(Name (id_of_string "x"),Rel 1))) + in + let typ_f = + List.fold_right + (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c))) + lams + (DOP2(Prod,(applistc vs (rel_list 0 llams)), + DLAM(Anonymous,lift 1 t))) + in + let constr_f = DOP2(Cast,val_f,typ_f) in + (* juste pour verification *) + let _ = + try + Typing.type_of env Evd.empty constr_f + with _ -> + error ("cannot be defined as coercion - "^ + "may be a bad number of arguments") + in + let idf = + match idf_opt with + | Some(idf) -> idf + | None -> + id_of_string ("Id_"^(string_of_id ids)^"_"^ + (string_of_cl (fst (constructor_at_head t)))) + in + let constr_entry = + { const_entry_body = Cooked constr_f; const_entry_type = None } in + declare_constant idf (constr_entry,NeverDischarge); + idf + +let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps = + add_anonymous_leaf + (inCoercion + ((coef, + {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}), + cls,clt)) + +(* +nom de la fonction coercion +strength de f +nom de la classe source (optionnel) +sp de la classe source (dans le cas des structures) +nom de la classe target (optionnel) +booleen "coercion identite'?" + +lorque source est None alors target est None aussi. +*) + +let try_add_new_coercion_core idf stre source target isid = + let env = Global.env () in + let v = construct_reference env CCI idf in + let t = Retyping.get_type_of env Evd.empty v in + let k = Retyping.get_type_of env Evd.empty t in + let vj = {uj_val=v; uj_type=t; uj_kind = k} in + let f_vardep,coef = coe_of_reference v in + if coercion_exists coef then + errorlabstrm "try_add_coercion" + [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >]; + let lp = prods_of t in + let llp = List.length lp in + if llp <= 1 then + errorlabstrm "try_add_coercion" + [< 'sTR"Does not correspond to a coercion" >]; + let ids,(cls,ps,vs,lvs,ind,s_vardep) = + try + get_source (List.tl lp) source + with Not_found -> + errorlabstrm "try_add_coercion" + [<'sTR"We do not find the source class " >] + in + if (cls = CL_FUN) then + errorlabstrm "try_add_coercion" + [< 'sTR"FUNCLASS cannot be a source class" >]; + if (cls = CL_SORT) then + errorlabstrm "try_add_coercion" + [< 'sTR"SORTCLASS cannot be a source class" >]; + if not (uniform_cond (llp-1-ind) lvs) then + errorlabstrm "try_add_coercion" + [<'sTR(string_of_id idf); + 'sTR" does not respect the inheritance uniform condition" >]; + let clt,pt,vt = + try + get_target (List.hd lp) ind + with Not_found -> + errorlabstrm "try_add_coercion" + [<'sTR"We cannot find the target class" >] + in + let idt = + (match target with + | Some idt -> + if idt = id_of_cl clt then + idt + else + errorlabstrm "try_add_coercion" + [<'sTR"The target class does not correspond to "; + 'sTR(string_of_id idt) >] + | None -> (id_of_cl clt)) + in + let stres = check_class ids vs cls ps in + let stret = check_class idt vt clt pt in + let stref = stre_of_coe coef in +(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? + let streunif = stre_unif_cond (s_vardep,f_vardep) in + *) + let streunif = NeverDischarge in + let stre' = stre_max4 stres stret stref streunif in + (* if (stre=NeverDischarge) & (stre'<>NeverDischarge) + then errorlabstrm "try_add_coercion" + [<'sTR(string_of_id idf); + 'sTR" must be declared as a local coercion (its strength is "; + 'sTR(string_of_strength stre');'sTR")" >] *) + let stre = stre_max (stre,stre') in + add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) idf ps + + +let try_add_new_coercion id stre = + try_add_new_coercion_core id stre None None false + +let try_add_new_coercion_subclass id stre = + let idf = build_id_coercion None id in + try_add_new_coercion_core idf stre (Some id) None true + +let try_add_new_coercion_with_target id stre source target isid = + if isid then + let idf = build_id_coercion (Some id) source in + try_add_new_coercion_core idf stre (Some source) (Some target) true + else + try_add_new_coercion_core id stre (Some source) (Some target) false + +let try_add_new_coercion_record id stre source = + try_add_new_coercion_core id stre (Some source) None false + +(* fonctions pour le discharge: plutot sale *) + +let defined_in_sec sp sec_sp = + let ((p1,id1,k1)) = repr_path sp in + let ((p2,id2,k2)) = repr_path sec_sp in + p1 = (string_of_id id2)::p2 + +let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) = + let env = Global.env () in + match cl with + | CL_Var id -> x + | CL_SP sp -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let v = global_reference CCI spid in + let t = Retyping.get_type_of env Evd.empty v in + let p = arity_sort t in + (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) + else + x + | CL_IND (sp,i) -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let v = global_reference CCI spid in + let t = Retyping.get_type_of env Evd.empty v in + let p = arity_sort t in + (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) + else + x + | _ -> anomaly "process_class" + +let process_cl sec_sp cl = + match cl with + | CL_Var id -> CL_Var id + | CL_SP sp -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + CL_SP newsp + else + cl + | CL_IND (sp,i) -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + CL_IND (newsp,i) + else + cl + | _ -> cl + +(* Pour le discharge *) +let process_coercion sec_sp (((coe,coeinfo),s,t) as x) = + let s1= process_cl sec_sp s in + let t1 = process_cl sec_sp t in + let p = (snd (class_info s1)).cL_PARAM in + match coe with + | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p + | NAM_Constant sp -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + ((NAM_Constant newsp,coeinfo),s1,t1),spid,p + else + ((coe,coeinfo),s1,t1),basename sp,p + | NAM_Inductive (sp,i) -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + ((NAM_Inductive (newsp,i),coeinfo),s1,t1),spid,p + else + ((coe,coeinfo),s1,t1),basename sp,p + | NAM_Constructor ((sp,i),j) -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let id = Global.id_of_global (MutConstruct((newsp,i),j)) in + (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p + else + ((coe,coeinfo),s1,t1), + Global.id_of_global (MutConstruct((sp,i),j)), + p diff --git a/pretyping/class.mli b/pretyping/class.mli new file mode 100644 index 0000000000..dc19ccce01 --- /dev/null +++ b/pretyping/class.mli @@ -0,0 +1,26 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Classops +open Declare +(*i*) + +(* Classes and coercions. *) + +val try_add_new_coercion : identifier -> strength -> unit +val try_add_new_coercion_subclass : identifier -> strength -> unit +val try_add_new_coercion_record : identifier -> strength -> identifier -> unit +val try_add_new_coercion_with_target : identifier -> strength -> + identifier -> identifier -> bool -> unit + +val try_add_new_class : identifier -> strength -> unit +val process_class : + section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) +val process_coercion : + section_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> + ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int + +val defined_in_sec : section_path -> section_path -> bool diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index dea95d0e04..911df0a8aa 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -32,7 +32,7 @@ type struc_typ = { s_PARAM : int; s_PROJ : section_path option list } -let sTRUCS = (ref [] : (section_path * struc_typ) list ref) +let sTRUCS = (ref [] : (inductive_path * struc_typ) list ref) let add_new_struc1 x = sTRUCS:=x::(!sTRUCS) @@ -46,8 +46,6 @@ let (inStruc,outStruc) = let add_new_struc (s,c,n,l) = Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) -let struc_info s = List.assoc s !sTRUCS - (*** table des definitions "object" : pour chaque object c, c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 9b666513f7..5872bd9225 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -23,8 +23,7 @@ type struc_typ = { s_PROJ : section_path option list } val add_new_struc : - section_path * identifier * int * section_path option list -> unit -val struc_info : section_path -> struc_typ + inductive_path * identifier * int * section_path option list -> unit type obj_typ = { o_DEF : constr; @@ -32,17 +31,14 @@ type obj_typ = { o_TPARAMS : constr list; (* dans l'ordre *) o_TCOMPS : constr list } (* dans l'ordre *) -val oBJDEFS : ((cte_typ * cte_typ) * obj_typ) list ref -val sTRUCS : (section_path * struc_typ) list ref - val objdef_info : (cte_typ * cte_typ) -> obj_typ val add_new_objdef : (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list * Term.constr list * Term.constr list -> unit -val inStruc : section_path * struc_typ -> obj -val outStruc : obj -> section_path * struc_typ +val inStruc : inductive_path * struc_typ -> obj +val outStruc : obj -> inductive_path * struc_typ val inObjDef1 : section_path -> obj val outObjDef1 : obj -> section_path diff --git a/toplevel/class.ml b/toplevel/class.ml deleted file mode 100644 index 2262d00835..0000000000 --- a/toplevel/class.ml +++ /dev/null @@ -1,474 +0,0 @@ - -(* $Id$ *) - -open Util -open Pp -open Names -open Generic -open Term -open Inductive -open Constant -open Environ -open Lib -open Classops -open Declare - -(* manipulations concernant les strength *) - -(* gt dans le sens de "longueur du sp" (donc le moins persistant) *) - -(* strength * strength -> bool *) - -let stre_gt = function - | (NeverDischarge,NeverDischarge) -> false - | (NeverDischarge,x) -> false - | (x,NeverDischarge) -> true - | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) - -let stre_max (stre1,stre2) = - if stre_gt (stre1,stre2) then stre1 else stre2 - -let stre_max4 stre1 stre2 stre3 stre4 = - stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4))) - -let id_of_varid = function - | VAR id -> id - | _ -> anomaly "class__id_of_varid" - -let stre_of_VAR c = variable_strength (destVar c) - -(* lf liste des variable dont depend la coercion f - lc liste des variable dont depend la classe source *) - -let rec stre_unif_cond = function - | ([],[]) -> NeverDischarge - | (v::l,[]) -> stre_of_VAR v - | ([],v::l) -> stre_of_VAR v - | (v1::l1,v2::l2) -> - if v1=v2 then - stre_unif_cond (l1,l2) - else - let stre1 = (stre_of_VAR v1) - and stre2 = (stre_of_VAR v2) in - stre_max (stre1,stre2) - -let stre_of_coe = function - | NAM_Constant sp -> constant_strength sp - | NAM_Var id -> variable_strength id - | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge - -(* try_add_class : Names.identifier -> - Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *) - -let try_add_class id v clpopt streopt check_exist = - let env = Global.env () in - let t = Retyping.get_type_of env Evd.empty v in - let p1 = - try - arity_sort t - with Not_found -> - errorlabstrm "try_add_class" - [< 'sTR "Type of "; 'sTR (string_of_id id); - 'sTR " does not end with a sort" >] - in - let cl,p = - match clpopt with - | None -> let (cl,_)=constructor_at_head v in (cl,p1) - | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) - in - if check_exist & class_exists cl then - errorlabstrm "try_add_new_class" - [< 'sTR (string_of_id id) ; 'sTR " is already a class" >]; - let stre' = stre_of_cl cl in - let stre = match streopt with - | Some stre -> stre_max (stre,stre') - | None -> stre' - in - add_new_class (cl,(string_of_id id),stre,p); - stre - -(* try_add_new_class : Names.identifier -> unit *) - -let try_add_new_class id stre = - let v = global_reference CCI id in - let _ = try_add_class id v None (Some stre) true in () - -(* check_class : Names.identifier -> - Term.constr -> cl_typ -> int -> int * Libobject.strength *) - -let check_class id v cl p = - try - let _,clinfo = class_info cl in - if p = clinfo.cL_PARAM then - clinfo.cL_STRE - else - errorlabstrm "fully_applied" - [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >] - with Not_found -> - try_add_class id v (Some (cl,p)) None false - - -(* decomposition de constr vers coe_typ *) - -(* t provient de global_reference donc pas de Cast, pas de AppL *) -let coe_of_reference t = - match kind_of_term t with - | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp - | IsMutInd (ind_sp,l) -> (Array.to_list l),NAM_Inductive ind_sp - | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Constructor cstr_sp - | IsVar id -> [],NAM_Var id - | _ -> anomaly "Not a reference" - -let constructor_at_head1 t = - let rec aux t' = - match kind_of_term t' with - | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0 - | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0 - | IsVar id -> t',[],[],CL_Var id,0 - | IsCast (c,_) -> aux c - | IsAppL(f,args) -> - let t',_,l,c,_ = aux f in t',args,l,c,List.length args - | IsProd (_,_,_) -> t',[],[],CL_FUN,0 - | IsSort _ -> t',[],[],CL_SORT,0 - | _ -> raise Not_found - in - aux (collapse_appl t) - - -(* condition d'heritage uniforme *) - -let uniform_cond nargs lt = - let rec aux = function - | (0,[]) -> true - | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l)) - | _ -> false - in - aux (nargs,lt) - -let id_of_cl = function - | CL_FUN -> (id_of_string "FUNCLASS") - | CL_SORT -> (id_of_string "SORTCLASS") - | CL_SP sp -> (basename sp) - | CL_IND (sp,i) -> - (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename - | CL_Var id -> id - -let string_of_cl = function - | CL_FUN -> "FUNCLASS" - | CL_SORT -> "SORTCLASS" - | CL_SP sp -> string_of_id (basename sp) - | CL_IND (sp,i) -> - string_of_id - (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename - | CL_Var id -> string_of_id id - -(* -lp est la liste (inverse'e) des arguments de la coercion -ids est le nom de la classe source -sps_opt est le sp de la classe source dans le cas des structures -retourne: -la classe souce -nbre d'arguments de la classe -le constr de la class -l'indice de la classe source dans la liste lp -la liste des variables dont depend la classe source -*) - -type choice = Ident of identifier | Section_path of section_path - -let get_source lp source = - let aux test = - let rec aux1 n = function - | [] -> raise Not_found - | t1::lt -> - try - let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in - if test cl1 then - cl1,p1,v1,lv1,n,l - else - aux1 (n+1) lt - with _ -> - aux1 (n + 1) lt - in - aux1 1 lp - in - match source with - | None -> - let (v1,lv1,l,cl1,p1) as x = - match lp with - | [] -> raise Not_found - | t1::_ -> - try constructor_at_head1 t1 - with _ -> raise Not_found - in - (id_of_cl cl1),(cl1,p1,v1,lv1,1,l) - | Some (Ident id) -> - id, aux (function cl -> id_of_cl cl = id) - | Some (Section_path sp) -> - basename sp, - aux (function - | CL_SP sp1 -> sp=sp1 - | CL_IND (sp1,i) -> sp=sp1 - | _ -> false) - -let get_target t ind = - if (ind > 1) then - CL_FUN,0,t - else - let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2 - -let prods_of t = - let rec aux acc = function - | DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2 - | (DOP2(Cast,c,_)) -> aux acc c - | t -> t::acc - in - aux [] t - -(* coercion identite' *) - -let lams_of t = - let rec aux acc = function - | DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2 - | DOP2(Cast,c,_) -> aux acc c - | t -> acc,t - in - aux [] t - -let build_id_coercion idf_opt ids = - let env = Global.env () in - let vs = construct_reference env CCI ids in - let c = match (strip_outer_cast vs) with - | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' -> - (try Instantiate.constant_value env c' - with _ -> errorlabstrm "build_id_coercion" - [< 'sTR(string_of_id ids); - 'sTR" must be a transparent constant" >]) - | _ -> - errorlabstrm "build_id_coercion" - [< 'sTR(string_of_id ids); - 'sTR" must be a transparent constant" >] - in - let lams,t = lams_of c in - let lams = List.rev lams in - let llams = List.length lams in - let val_f = - List.fold_right - (fun (x,t) u -> DOP2(Lambda,t,DLAM(x,u))) - lams - (DOP2(Lambda,(applistc vs (rel_list 0 llams)), - DLAM(Name (id_of_string "x"),Rel 1))) - in - let typ_f = - List.fold_right - (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c))) - lams - (DOP2(Prod,(applistc vs (rel_list 0 llams)), - DLAM(Anonymous,lift 1 t))) - in - let constr_f = DOP2(Cast,val_f,typ_f) in - (* juste pour verification *) - let _ = - try - Typing.type_of env Evd.empty constr_f - with _ -> - error ("cannot be defined as coercion - "^ - "may be a bad number of arguments") - in - let idf = - match idf_opt with - | Some(idf) -> idf - | None -> - id_of_string ("Id_"^(string_of_id ids)^"_"^ - (string_of_cl (fst (constructor_at_head t)))) - in - let constr_entry = - { const_entry_body = Cooked constr_f; const_entry_type = None } in - declare_constant idf (constr_entry,NeverDischarge); - idf - -let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps = - add_anonymous_leaf - (inCoercion - ((coef, - {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}), - cls,clt)) - -(* -nom de la fonction coercion -strength de f -nom de la classe source (optionnel) -sp de la classe source (dans le cas des structures) -nom de la classe target (optionnel) -booleen "coercion identite'?" - -lorque source est None alors target est None aussi. -*) - -let try_add_new_coercion_core idf stre source target isid = - let env = Global.env () in - let v = construct_reference env CCI idf in - let t = Retyping.get_type_of env Evd.empty v in - let k = Retyping.get_type_of env Evd.empty t in - let vj = {uj_val=v; uj_type=t; uj_kind = k} in - let f_vardep,coef = coe_of_reference v in - if coercion_exists coef then - errorlabstrm "try_add_coercion" - [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >]; - let lp = prods_of t in - let llp = List.length lp in - if llp <= 1 then - errorlabstrm "try_add_coercion" - [< 'sTR"Does not correspond to a coercion" >]; - let ids,(cls,ps,vs,lvs,ind,s_vardep) = - try - get_source (List.tl lp) source - with Not_found -> - errorlabstrm "try_add_coercion" - [<'sTR"We do not find the source class " >] - in - if (cls = CL_FUN) then - errorlabstrm "try_add_coercion" - [< 'sTR"FUNCLASS cannot be a source class" >]; - if (cls = CL_SORT) then - errorlabstrm "try_add_coercion" - [< 'sTR"SORTCLASS cannot be a source class" >]; - if not (uniform_cond (llp-1-ind) lvs) then - errorlabstrm "try_add_coercion" - [<'sTR(string_of_id idf); - 'sTR" does not respect the inheritance uniform condition" >]; - let clt,pt,vt = - try - get_target (List.hd lp) ind - with Not_found -> - errorlabstrm "try_add_coercion" - [<'sTR"We cannot find the target class" >] - in - let idt = - (match target with - | Some idt -> - if idt = id_of_cl clt then - idt - else - errorlabstrm "try_add_coercion" - [<'sTR"The target class does not correspond to "; - 'sTR(string_of_id idt) >] - | None -> (id_of_cl clt)) - in - let stres = check_class ids vs cls ps in - let stret = check_class idt vt clt pt in - let stref = stre_of_coe coef in -(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? - let streunif = stre_unif_cond (s_vardep,f_vardep) in - *) - let streunif = NeverDischarge in - let stre' = stre_max4 stres stret stref streunif in - (* if (stre=NeverDischarge) & (stre'<>NeverDischarge) - then errorlabstrm "try_add_coercion" - [<'sTR(string_of_id idf); - 'sTR" must be declared as a local coercion (its strength is "; - 'sTR(string_of_strength stre');'sTR")" >] *) - let stre = stre_max (stre,stre') in - add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) idf ps - - -let try_add_new_coercion id stre = - try_add_new_coercion_core id stre None None false - -let try_add_new_coercion_subclass id stre = - let idf = build_id_coercion None id in - try_add_new_coercion_core idf stre (Some (Ident id)) None true - -let try_add_new_coercion_with_target id stre source target isid = - if isid then - let idf = build_id_coercion (Some id) source in - try_add_new_coercion_core idf stre (Some (Ident source)) (Some target) true - else - try_add_new_coercion_core id stre (Some (Ident source)) (Some target) false - -let try_add_new_coercion_record id stre source_sp = - try_add_new_coercion_core id stre (Some (Section_path source_sp)) None false - -(* fonctions pour le discharge: plutot sale *) - -let defined_in_sec sp sec_sp = - let ((p1,id1,k1)) = repr_path sp in - let ((p2,id2,k2)) = repr_path sec_sp in - p1 = (string_of_id id2)::p2 - -let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) = - let env = Global.env () in - match cl with - | CL_Var id -> x - | CL_SP sp -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - let v = global_reference CCI spid in - let t = Retyping.get_type_of env Evd.empty v in - let p = arity_sort t in - (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) - else - x - | CL_IND (sp,i) -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - let v = global_reference CCI spid in - let t = Retyping.get_type_of env Evd.empty v in - let p = arity_sort t in - (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) - else - x - | _ -> anomaly "process_class" - -let process_cl sec_sp cl = - match cl with - | CL_Var id -> CL_Var id - | CL_SP sp -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - CL_SP newsp - else - cl - | CL_IND (sp,i) -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - CL_IND (newsp,i) - else - cl - | _ -> cl - -(* Pour le discharge *) -let process_coercion sec_sp (((coe,coeinfo),s,t) as x) = - let s1= process_cl sec_sp s in - let t1 = process_cl sec_sp t in - let p = (snd (class_info s1)).cL_PARAM in - match coe with - | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p - | NAM_Constant sp -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - ((NAM_Constant newsp,coeinfo),s1,t1),spid,p - else - ((coe,coeinfo),s1,t1),basename sp,p - | NAM_Inductive (sp,i) -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - ((NAM_Inductive (newsp,i),coeinfo),s1,t1),spid,p - else - ((coe,coeinfo),s1,t1),basename sp,p - | NAM_Constructor ((sp,i),j) -> - if defined_in_sec sp sec_sp then - let ((_,spid,spk)) = repr_path sp in - let newsp = Lib.make_path spid CCI in - let id = Global.id_of_global (MutConstruct((newsp,i),j)) in - (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p - else - ((coe,coeinfo),s1,t1), - Global.id_of_global (MutConstruct((sp,i),j)), - p diff --git a/toplevel/class.mli b/toplevel/class.mli deleted file mode 100644 index f828215548..0000000000 --- a/toplevel/class.mli +++ /dev/null @@ -1,26 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Names -open Term -open Classops -open Declare -(*i*) - -(* Classes and coercions. *) - -val try_add_new_coercion : identifier -> strength -> unit -val try_add_new_coercion_subclass : identifier -> strength -> unit -val try_add_new_coercion_record: identifier -> strength -> section_path -> unit -val try_add_new_coercion_with_target : identifier -> strength -> - identifier -> identifier -> bool -> unit - -val try_add_new_class : identifier -> strength -> unit -val process_class : - section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) -val process_coercion : - section_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> - ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int - -val defined_in_sec : section_path -> section_path -> bool diff --git a/toplevel/command.ml b/toplevel/command.ml index 04fdd2e399..e62e85d57d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -134,15 +134,16 @@ let build_mutual lparams lnamearconstrs finite = and nparams = List.length lparams and sigma = Evd.empty and env0 = Global.env() in - let fs = States.freeze() in +(* let fs = States.freeze() in*) try let mispecvec = - let (ind_sign,arityl) = + let (ind_env,arityl) = List.fold_left (fun (env,arl) (recname,arityc,_) -> let arity = type_of_com env (mkProdCit lparams arityc) in let env' = Environ.push_var (recname,arity) env in - declare_variable recname (arity.body,NeverDischarge,false); +(* A quoi cela sert ? + declare_variable recname (arity.body,NeverDischarge,false);*) (env', (arity::arl))) (env0,[]) lnamearconstrs in @@ -150,27 +151,27 @@ let build_mutual lparams lnamearconstrs finite = (fun ar (name,_,lname_constr) -> let consconstrl = List.map - (fun (_,constr) -> constr_of_com sigma ind_sign + (fun (_,constr) -> constr_of_com sigma ind_env (mkProdCit lparams constr)) lname_constr in (name, ar.body, List.map fst lname_constr, put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl))) (List.rev arityl) lnamearconstrs - in + in let mie = { mind_entry_nparams = nparams; mind_entry_finite = finite; mind_entry_inds = mispecvec } in - States.unfreeze fs; +(* States.unfreeze fs;*) let sp = declare_mind mie in if is_verbose() then pPNL(minductive_message lrecnames); for i = 0 to List.length mispecvec - 1 do declare_eliminations sp i done with e -> - States.unfreeze fs; raise e +(* States.unfreeze fs; *)raise e (* try to find non recursive definitions *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 2942e7e5a3..f57ddb3787 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -201,7 +201,7 @@ type discharge_operation = | Constant of identifier * constant_entry * strength | Inductive of mutual_inductive_entry | Class of cl_typ * cl_info_typ - | Struc of section_path * struc_typ + | Struc of inductive_path * struc_typ | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int @@ -261,14 +261,14 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) = ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist) | "STRUCTURE" -> - let (sp,info) = outStruc lobj in + let ((sp,i),info) = outStruc lobj in let newsp = recalc_sp sp in let mib = Environ.lookup_mind newsp oldenv in let strobj = { s_CONST = info.s_CONST; s_PARAM = mib.mind_nparams; s_PROJ = List.map (option_app recalc_sp) info.s_PROJ } in - ((Struc (newsp,strobj))::ops, ids_to_discard, work_alist) + ((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist) (***TODO | "OBJDEF1" -> diff --git a/toplevel/record.ml b/toplevel/record.ml index 99cbac0b8b..1a5536a230 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -4,16 +4,13 @@ open Pp open Util open Names +open Generic open Term +open Declare open Coqast open Ast -(* -open Generic +open Astterm open Command -open Machops -open Classops -open Recordops -*) (********** definition d'un record (structure) **************) @@ -69,94 +66,92 @@ let print_id_list l = [< 'sTR "[" ; prlist (fun id -> [< 'sTR (string_of_id id) >]) l; 'sTR "]" >] let typecheck_params_and_field ps fs = - let sign0 = initial_sign() in - let sign1,newps = + let env0 = Global.env () in + let env1,newps = List.fold_left - (fun (sign,newps) (id,t) -> - let tj = type_of_com sign t in - (add_sign (id,tj) sign,(id,tj.body)::newps)) - (sign0,[]) ps + (fun (env,newps) (id,t) -> + let tj = type_of_com env t in + (Environ.push_var (id,tj) env,(id,tj.body)::newps)) + (env0,[]) ps in - let sign2,newfs = + let env2,newfs = List.fold_left - (fun (sign,newfs) (id,t) -> - let tj = type_of_com sign t in - (add_sign (id,tj) sign,(id,tj.body)::newfs)) (sign1,[]) fs + (fun (env,newfs) (id,t) -> + let tj = type_of_com env t in + (Environ.push_var (id,tj) env,(id,tj.body)::newfs)) (env1,[]) fs in List.rev(newps),List.rev(newfs) let mk_LambdaCit = List.fold_right (fun (x,a) b -> mkNamedLambda x a b) -let definition_structure (coe_constr,struc,ps,cfs,const,s) = - let (sign,fsign) = initial_assumptions() in - let fs = List.map snd cfs in - let coers = List.map fst cfs in - let idps = List.map fst ps in - let typs = List.map snd ps in - let idfs = List.map fst fs in - let tyfs = List.map snd fs in - if not (free_in_asts struc tyfs) then +let warning_or_error coe st = + if coe then errorlabstrm "structure" st; + pPNL [< 'sTR"Warning: "; st >] + +(* Fields have names [idfs] and types [tyfs]; [coers] is a boolean list + telling if the corresponding field must me a coercion *) + +let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = + let coers,fs = List.split cfs in + let idps,typs = List.split ps in + let idfs,tyfs = List.split fs in + if not (free_in_asts idstruc tyfs) then message "Error: A record cannot be recursive"; let newps,newfs = typecheck_params_and_field ps fs in let app_constructor = - ope("APPLIST", - (ope("XTRA",[str "!";(nvar (string_of_id struc))])):: - List.map (fun id -> nvar(string_of_id id)) idps) - in + ope("APPLISTEXPL", + (nvar (string_of_id idstruc)):: + List.map (fun id -> nvar(string_of_id id)) idps) in let type_constructor = make_constructor fs app_constructor in - let _ = build_mutual ps [(struc,s,[(const,type_constructor)])] true in - let x = next_ident_away (id_of_string "x") - (List.fold_left (fun l ty -> union (all_vars ty) l) - (union idps (fst sign)) tyfs) in - let r = Machops.global (gLOB sign) struc in - let (rsp,_,_) = destMutInd r in - let rid = basename rsp in - let lp = length idps in + let _ = build_mutual ps [(idstruc,s,[(idbuild,type_constructor)])] true in + let r = global_reference CCI idstruc in + let rsp = op_of_mind r in + let x = Environ.named_hd (Global.env()) r Anonymous in + let lp = List.length idps in let rp1 = applist (r,(rel_list 0 lp)) in let rp2 = applist (r,(rel_list 1 lp)) in - let warning_or_error coe st = - if coe then errorlabstrm "structure" st; - pPNL [< 'sTR"Warning: "; st >] - in - let (sp_projs,_,_,_,_) = - List.fold_left - (fun (sp_projs,ids_ok,ids_not_ok,sigma,coes) (fi,ti) -> + + (* We build projections *) + let (sp_projs,_,_) = + List.fold_left2 + (fun (sp_projs,ids_not_ok,subst) coe (fi,ti) -> let fv_ti = global_vars ti in - let bad_projs = (intersect ids_not_ok fv_ti) in + let bad_projs = (list_intersect ids_not_ok fv_ti) in if bad_projs <> [] then begin - (warning_or_error (hd coes) + (warning_or_error coe [< 'sTR(string_of_id fi); 'sTR" cannot be defined. The projections "; print_id_list bad_projs; 'sTR " were not defined" >]); - (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes)) + (None::sp_projs,fi::ids_not_ok,subst) end else - let p = mkNamedLambda x rp2 (replace_vars sigma ti) in + let p = mkLambda x rp2 (replace_vars subst ti) in let branch = mk_LambdaCit newfs (VAR fi) in let proj = mk_LambdaCit newps - (mkNamedLambda x rp1 + (mkLambda x rp1 (mkMutCaseA (ci_of_mind r) p (Rel 1) [|branch|])) in let ok = - try - (Declare.machine_constant (sign,fsign) - ((fi,false,NeverDischarge),proj); true) + try + let cie = + { Constant.const_entry_body = Constant.Cooked proj; + Constant.const_entry_type = None } in + (declare_constant fi (cie,NeverDischarge); true) with UserError(s,pps) -> - ((warning_or_error (hd coes) + ((warning_or_error coe [<'sTR (string_of_id fi); 'sTR" cannot be defined. "; pps >]);false) in if not ok then - (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes)) + (None::sp_projs,fi::ids_not_ok,subst) else begin - if List.hd coes then - Class.try_add_new_coercion_record fi NeverDischarge rsp; - let constr_fi = Machops.global (gLOB sign) fi in - let constr_fip = - applist (constr_fi,(List.map (fun id -> VAR id) idps)@[VAR x]) - in (Some(path_of_const constr_fi)::sp_projs,fi::ids_ok,ids_not_ok, - (fi,{sinfo=Closed;sit=constr_fip})::sigma,(tl coes)) + if coe then + Class.try_add_new_coercion_record fi NeverDischarge idstruc; + let constr_fi = global_reference CCI fi in + let constr_fip = (* Rel 1 refers to "x" *) + applist (constr_fi,(List.map (fun id -> VAR id) idps)@[Rel 1]) + in (Some(path_of_const constr_fi)::sp_projs, + ids_not_ok, + (fi,{sinfo=Closed;sit=constr_fip})::subst) end) - ([],[],[],[],coers) newfs + ([],[],[]) coers newfs in - if coe_constr="COERCION" then - Class.try_add_new_coercion const NeverDischarge; - add_new_struc (rsp,const,lp,rev sp_projs) - + if is_coe then Class.try_add_new_coercion idbuild NeverDischarge; + Recordops.add_new_struc (rsp,idbuild,lp,List.rev sp_projs) diff --git a/toplevel/record.mli b/toplevel/record.mli index 2020a3b26b..842754b9ad 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -7,6 +7,6 @@ open Term (*i*) val definition_structure : - string * identifier * (identifier * Coqast.t) list * + bool * identifier * (identifier * Coqast.t) list * (bool * (identifier * Coqast.t)) list * identifier * Coqast.t -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4dad9e2bc1..54629fe2d3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -962,7 +962,6 @@ let _ = fun () -> build_mutual la lnamearconstructs (isfinite f) | _ -> bad_vernac_args "MUTUALINDUCTIVE") -(*** let _ = add "RECORD" (function @@ -973,23 +972,21 @@ let _ = VARG_VARGLIST namec; VARG_VARGLIST cfs] -> let ps = join_binders binders in - let cfs = List.map - (function - | (VARG_VARGLIST - [VARG_STRING str;VARG_IDENTIFIER id; - VARG_CONSTR c]) -> - (str = "COERCION",(id,c)) - | _ -> bad_vernac_args "RECORD") - cfs - in + let cfs = + List.map + (function + | (VARG_VARGLIST + [VARG_STRING str; VARG_IDENTIFIER id; VARG_CONSTR c]) -> + (str = "COERCION",(id,c)) + | _ -> bad_vernac_args "RECORD") + cfs in let const = match namec with | [] -> (id_of_string ("Build_"^(string_of_id struc))) | [VARG_IDENTIFIER id] -> id - | _ -> bad_vernac_args "RECORD" - in - fun () -> definition_structure (coe,struc,ps,cfs,const,s) + | _ -> bad_vernac_args "RECORD" in + let iscoe = (coe = "COERCION") in + fun () -> Record.definition_structure (iscoe,struc,ps,cfs,const,s) | _ -> bad_vernac_args "RECORD") -***) let _ = add "MUTUALRECURSIVE" -- cgit v1.2.3