diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/auto_ind_decl.ml | 12 | ||||
-rw-r--r-- | toplevel/classes.ml | 343 | ||||
-rw-r--r-- | toplevel/classes.mli | 27 | ||||
-rw-r--r-- | toplevel/command.ml | 166 | ||||
-rw-r--r-- | toplevel/command.mli | 12 | ||||
-rw-r--r-- | toplevel/coqinit.ml | 27 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 58 | ||||
-rw-r--r-- | toplevel/himsg.ml | 92 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 65 | ||||
-rw-r--r-- | toplevel/metasyntax.mli | 6 | ||||
-rw-r--r-- | toplevel/mltop.ml4 | 100 | ||||
-rw-r--r-- | toplevel/mltop.mli | 19 | ||||
-rw-r--r-- | toplevel/protectedtoplevel.ml | 9 | ||||
-rw-r--r-- | toplevel/record.ml | 186 | ||||
-rw-r--r-- | toplevel/record.mli | 17 | ||||
-rw-r--r-- | toplevel/toplevel.ml | 10 | ||||
-rw-r--r-- | toplevel/usage.ml | 19 | ||||
-rw-r--r-- | toplevel/usage.mli | 7 | ||||
-rw-r--r-- | toplevel/vernac.ml | 72 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 289 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 131 |
21 files changed, 883 insertions, 784 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 49b9ce7a..82709db4 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto_ind_decl.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: auto_ind_decl.ml 11671 2008-12-12 12:43:03Z herbelin $ i*) open Tacmach open Util @@ -530,13 +530,13 @@ let compute_bl_tact ind lnamesparrec nparrec = tclORELSE reflexivity (Equality.discr_tac false None) ); simpl_in_hyp - ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp); + ((Rawterm.all_occurrences_expr,freshz),InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) tclREPEAT ( tclTHENSEQ [ - apply_in false freshz [(andb_prop()),Rawterm.NoBindings]; + apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None; fun gl -> let fresht = fresh_id (!avoid) (id_of_string "Z") gsig in @@ -748,8 +748,8 @@ let compute_dec_tact ind lnamesparrec nparrec = Pfedit.by ( tclTHENSEQ [ intros_using fresh_first_intros; intros_using [freshn;freshm]; - assert_as true (dl,Genarg.IntroIdentifier freshH) ( - mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + assert_tac (Name freshH) ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) ) ]); (*we do this so we don't have to prove the same goal twice *) Pfedit.by ( tclTHEN @@ -795,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec = unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all; - assert_as true (dl,Genarg.IntroIdentifier freshH3) + assert_tac (Name freshH3) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) ]); Pfedit.by diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 511befd8..04945040 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) (*i*) open Names @@ -32,19 +32,23 @@ open Topconstr open Decl_kinds open Entries -let hint_db = "typeclass_instances" +let typeclasses_db = "typeclass_instances" let qualid_of_con c = Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) +let set_rigid c = + Auto.add_hints false [typeclasses_db] + (Vernacexpr.HintsTransparency ([qualid_of_con c], false)) + let _ = Typeclasses.register_add_instance_hint (fun inst pri -> Flags.silently (fun () -> - Auto.add_hints false [hint_db] + Auto.add_hints false [typeclasses_db] (Vernacexpr.HintsResolve - [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) - + [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) + let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in @@ -67,207 +71,27 @@ type binder_list = (identifier located * bool * constr_expr) list (* Calls to interpretation functions. *) -let interp_binders_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) ((loc, i), t) -> - let n = Name i in - let t' = interp_binder_evars isevars env n t in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - -let interp_typeclass_context_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) (iid, bk, l) -> - let t' = interp_binder_evars isevars env (snd iid) l in - let i = match snd iid with - | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids - | Name id -> id - in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - let interp_type_evars evdref env ?(impls=([],[])) typ = let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - -let mk_interning_data env na impls typ = - let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (na, ([], impl, Notation.compute_arguments_scope typ)) -let interp_fields_evars isevars env avoid l = - List.fold_left - (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> - let impl, t' = interp_type_evars isevars env ~impls t in - let data = mk_interning_data env i impl t' in - let d = (Name i,None,t') in - (push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) - (env, [], avoid, [], ([], [])) l - (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr - -let implicits_of_context ctx = - list_map_i (fun i name -> - let explname = - match name with - | Name n -> Some n - | Anonymous -> None - in ExplByPos (i, explname), (true, true)) - 1 (List.rev (Anonymous :: (List.map pi1 ctx))) - -let degenerate_decl (na,b,t) = - let id = match na with - | Name id -> id - | Anonymous -> anomaly "Unnamed record variable" in - match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) - -let name_typeclass_binder avoid = function - | LocalRawAssum ([loc, Anonymous], bk, c) -> - let name = - let id = - match c with - CApp (_, (_, CRef (Ident (loc,id))), _) -> id - | _ -> id_of_string "assum" - in Implicit_quantifiers.make_fresh avoid (Global.env ()) id - in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid - | x -> x, avoid - -let name_typeclass_binders avoid l = - let l', avoid = - List.fold_left - (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in - b' :: binders, avoid) - ([], avoid) l - in List.rev l', avoid - -let new_class id par ar sup props = - let env0 = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in - let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in - let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in - let sup, bound = name_typeclass_binders bound sup in - let supnames = - List.fold_left (fun acc b -> - match b with - LocalRawAssum (nl, _, _) -> nl @ acc - | LocalRawDef _ -> assert(false)) - [] sup - in - - (* Interpret the arity *) - let arity_imps, fullarity = - let ar = - match ar with - Some ar -> ar | None -> (dummy_loc, Rawterm.RType None) - in - let arity = CSort (fst ar, snd ar) in - let term = prod_constr_expr (prod_constr_expr arity par) sup in - interp_type_evars isevars env0 term - in - let ctx_params, arity = decompose_prod_assum fullarity in - let env_params = push_rel_context ctx_params env0 in - (* Interpret the definitions and propositions *) - let env_props, prop_impls, bound, ctx_props, _ = - interp_fields_evars isevars env_params bound props - in - let subs = List.map (fun ((loc, id), b, _) -> b) props in - (* Instantiate evars and check all are resolved *) - let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in - let isevars = Typeclasses.resolve_typeclasses env_props isevars in - let sigma = Evd.evars_of isevars in - let ctx_params = Evarutil.nf_rel_context_evar sigma ctx_params in - let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in - let arity = Reductionops.nf_evar sigma arity in - let ce t = Evarutil.check_evars env0 Evd.empty isevars t in - let fieldimpls = - (* Make the class and all params implicits in the projections *) - let ctx_impls = implicits_of_context ctx_params in - let len = succ (List.length ctx_params) in - List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls - in - let impl, projs = - let params = ctx_params and fields = ctx_props in - List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); - match fields with - [(Name proj_name, _, field)] -> - let class_body = it_mkLambda_or_LetIn field params in - let class_type = - match ar with - Some _ -> Some (it_mkProd_or_LetIn arity params) - | None -> None - in - let class_entry = - { const_entry_body = class_body; - const_entry_type = class_type; - const_entry_opaque = false; - const_entry_boxed = false } - in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in - let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in - let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in - let proj_entry = - { const_entry_body = proj_body; - const_entry_type = Some proj_type; - const_entry_opaque = false; - const_entry_boxed = false } - in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls); - cref, [proj_name, proj_cst] - | _ -> - let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in - let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in - let kn = Record.declare_structure (snd id) idb arity_imps - params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) - in - IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) - fields (Recordops.lookup_projections (kn,0))) - in - let ctx_context = - List.map (fun ((na, b, t) as d) -> - match Typeclasses.class_of_constr t with - | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d) - | None -> (None, d)) - ctx_params - in - let k = - { cl_impl = impl; - cl_context = ctx_context; - cl_props = ctx_props; - cl_projs = projs } - in - List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p)) - k.cl_projs subs; - add_class k - -type binder_def_list = (identifier located * identifier located list * constr_expr) list - -let binders_of_lidents l = - List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l - let type_ctx_instance isevars env ctx inst subst = let (s, _) = List.fold_left2 - (fun (subst, instctx) (na, _, t) ce -> + (fun (subst, instctx) (na, b, t) ce -> let t' = substl subst t in - let c = interp_casted_constr_evars isevars env ce t' in - let d = na, Some c, t' in - c :: subst, d :: instctx) + let c' = + match b with + | None -> interp_casted_constr_evars isevars env ce t' + | Some b -> substl subst b + in + let d = na, Some c', t' in + c' :: subst, d :: instctx) (subst, []) (List.rev ctx) inst in s @@ -284,27 +108,10 @@ let id_of_class cl = open Pp let ($$) g f = fun x -> g (f x) - -let default_on_free_vars = - Flags.if_verbose - (fun fvs -> - match fvs with - [] -> () - | l -> msgnl (str"Implicitly generalizing " ++ - prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str".")) - -let fail_on_free_vars = function - [] -> () - | [fv] -> - errorlabstrm "Classes" - (str"Unbound variable " ++ Nameops.pr_id fv ++ str".") - | fvs -> errorlabstrm "Classes" - (str"Unbound variables " ++ - prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".") let instance_hook k pri global imps ?hook cst = let inst = Typeclasses.new_instance k pri global cst in - Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps; + Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps; Typeclasses.add_instance inst; (match hook with Some h -> h cst | None -> ()) @@ -323,51 +130,30 @@ let declare_instance_constant k pri global imps ?hook id term termtype = instance_hook k pri global imps ?hook kn; id -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in - let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in let tclass = match bk with - | Implicit -> - let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in - let k = class_info (Nametab.global id) in - let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in - let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in - if needlen <> applen then - mismatched_params env (List.map fst par) (List.map snd k.cl_context); - let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *) - (fun avoid (clname, (id, _, t)) -> - match clname with - Some (cl, b) -> - let t = - if b then - let _k = class_info cl in - CHole (Util.dummy_loc, Some (Evd.ImplicitArg (k.cl_impl, (1, None)))) - else CHole (Util.dummy_loc, None) - in t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - par (List.rev k.cl_context) - in Topconstr.CAppExpl (loc, (None, id), pars) - - | Explicit -> cl + | Implicit -> + Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false + (fun avoid (clname, (id, _, t)) -> + match clname with + | Some (cl, b) -> + let t = CHole (Util.dummy_loc, None) in + t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + cl + | Explicit -> cl in - let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in - let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in - on_free_vars (List.rev fvs @ List.rev gen_ids); - let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in - let bound = Idset.union gen_idset ctx_bound in - let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in - let ctx, avoid = name_typeclass_binders bound ctx in - let ctx = List.append ctx (List.rev gen_ctx) in + let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let imps, c' = interp_type_evars isevars env c in let ctx, c = decompose_prod_assum c' in - let cl, args = Typeclasses.dest_class_app c in - cl, ctx, imps, List.rev (Array.to_list args) + let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in + cl, ctx, imps, List.rev args in let id = match snd instid with @@ -384,7 +170,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses env !isevars; let sigma = Evd.evars_of !isevars in - let substctx = List.map (Evarutil.nf_evar sigma) subst in + let subst = List.map (Evarutil.nf_evar sigma) subst in if Lib.is_modtype () then begin let _, ty_constr = instance_constructor k (List.rev subst) in @@ -399,31 +185,48 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau end else begin + let props = + match props with + | CRecord (loc, _, fs) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + fs + | _ -> + if List.length k.cl_props <> 1 then + errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body") + else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] + in let subst = - let props = - List.map (fun (x, l, d) -> - x, Topconstr.abstract_constr_expr d (binders_of_lidents l)) - props - in - if List.length props > List.length k.cl_props then - mismatched_props env' (List.map snd props) k.cl_props; - let props, rest = - List.fold_left - (fun (props, rest) (id,_,_) -> - try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); - c :: props, rest' - with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) - else - type_ctx_instance isevars env' k.cl_props props substctx + match k.cl_props with + | [(na,b,ty)] -> + let term = match props with [] -> CHole (Util.dummy_loc, None) + | [(_,f)] -> f | _ -> assert false in + let ty' = substl subst ty in + let c = interp_casted_constr_evars isevars env' term ty' in + c :: subst + | _ -> + let props, rest = + List.fold_left + (fun (props, rest) (id,b,_) -> + try + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); + c :: props, rest' + with Not_found -> + (CHole (Util.dummy_loc, None) :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (fst (List.hd rest)) + else + type_ctx_instance isevars env' k.cl_props props subst + in + let subst = List.fold_left2 + (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) in - let app, ty_constr = instance_constructor k (List.rev subst) in + let app, ty_constr = instance_constructor k subst in let termtype = let t = it_mkProd_or_LetIn ty_constr ctx' in Evarutil.nf_isevar !isevars t diff --git a/toplevel/classes.mli b/toplevel/classes.mli index f149ac72..1bbf29a6 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: classes.mli 11709 2008-12-20 11:42:15Z msozeau $ i*) (*i*) open Names @@ -29,27 +29,6 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a val mismatched_props : env -> constr_expr list -> rel_context -> 'a -type binder_list = (identifier located * bool * constr_expr) list -type binder_def_list = (identifier located * identifier located list * constr_expr) list - -val binders_of_lidents : identifier located list -> local_binder list - -val name_typeclass_binders : Idset.t -> - Topconstr.local_binder list -> - Topconstr.local_binder list * Idset.t - -val new_class : identifier located -> - local_binder list -> - Vernacexpr.sort_expr located option -> - local_binder list -> - binder_list -> unit - -(* By default, print the free variables that are implicitely generalized. *) - -val default_on_free_vars : identifier list -> unit - -val fail_on_free_vars : identifier list -> unit - (* Instance declaration *) val declare_instance : bool -> identifier located -> unit @@ -69,8 +48,8 @@ val new_instance : ?global:bool -> (* Not global by default. *) local_binder list -> typeclass_constraint -> - binder_def_list -> - ?on_free_vars:(identifier list -> unit) -> + constr_expr -> + ?generalize:bool -> ?tac:Proof_type.tactic -> ?hook:(constant -> unit) -> int option -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 3688c347..b50c9bbd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *) open Pp open Util @@ -136,7 +136,7 @@ let red_constant_entry bl ce = function let declare_global_definition ident ce local imps = let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + maybe_declare_manual_implicits false gr imps; if local = Local && Flags.is_verbose() then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; @@ -166,8 +166,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = hook local r let syntax_definition ident (vars,c) local onlyparse = - let pat = interp_aconstr [] vars c in - Syntax_def.declare_syntactic_definition local ident onlyparse pat + let ((vars,_),pat) = interp_aconstr [] (vars,[]) c in + let onlyparse = onlyparse or Metasyntax.is_not_printable pat in + Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) @@ -189,7 +190,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let kn = declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + maybe_declare_manual_implicits false gr imps; assumption_message ident; if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ @@ -339,13 +340,26 @@ let (inDec,outDec) = let start_hook = ref ignore let set_start_hook = (:=) start_hook -let start_proof id kind c ?init_tac hook = +let start_proof id kind c ?init_tac ?(compute_guard=false) hook = let sign = Global.named_context () in let sign = clear_proofs sign in !start_hook c; - Pfedit.start_proof id kind sign c ?init_tac:init_tac hook - -let save id const (locality,kind) hook = + Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook + +let adjust_guardness_conditions const = + (* Try all combinations... not optimal *) + match kind_of_term const.const_entry_body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let possible_indexes = + List.map (fun c -> + interval 0 (List.length (fst (Sign.decompose_lam_assum c)))) + (Array.to_list fixdefs) in + let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in + { const with const_entry_body = mkFix ((indexes,0),fixdecls) } + | c -> const + +let save id const do_guard (locality,kind) hook = + let const = if do_guard then adjust_guardness_conditions const else const in let {const_entry_body = pft; const_entry_type = tpo; const_entry_opaque = opacity } = const in @@ -366,9 +380,9 @@ let save_hook = ref ignore let set_save_hook f = save_hook := f let save_named opacity = - let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in + let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in - save id const persistence hook + save id const do_guard persistence hook let make_eq_decidability ind = (* fetching data *) @@ -442,7 +456,7 @@ let declare_eliminations sp = (* 3b| Mutual inductive definitions *) -let compute_interning_datas env l nal typl impll = +let compute_interning_datas env ty l nal typl impll = let mk_interning_data na typ impls = let idl, impl = let impl = @@ -452,7 +466,7 @@ let compute_interning_datas env l nal typl impll = let sub_impl' = List.filter is_status_implicit sub_impl in (List.map name_of_implicit sub_impl', impl) in - (na, (idl, impl, compute_arguments_scope typ)) in + (na, (ty, idl, impl, compute_arguments_scope typ)) in (l, list_map3 mk_interning_data nal typl impll) let declare_interning_data (_,impls) (df,c,scope) = @@ -511,7 +525,9 @@ let interp_mutual paramsl indl notations finite = check_all_names_different indl; let env0 = Global.env() in let evdref = ref (Evd.create_evar_defs Evd.empty) in - let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in + let (env_params, ctx_params), userimpls = + interp_context_evars ~fail_anonymous:false evdref env0 paramsl + in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) @@ -526,7 +542,7 @@ let interp_mutual paramsl indl notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun _ -> userimpls) fullarities in - let impls = compute_interning_datas env0 params indnames fullarities indimpls in + let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -539,6 +555,7 @@ let interp_mutual paramsl indl notations finite = (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_params !evdref in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in let sigma = evars_of evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in @@ -604,7 +621,7 @@ let prepare_inductive ntnl indl = let indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = ar; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl in List.fold_right Option.List.cons ntnl [], indl @@ -624,12 +641,10 @@ let declare_mutual_with_eliminations isrecord mie impls = let (_,kn) = declare_mind isrecord mie in list_iter_i (fun i (indimpls, constrimpls) -> let ind = (kn,i) in - maybe_declare_manual_implicits false (IndRef ind) - (is_implicit_args()) indimpls; + maybe_declare_manual_implicits false (IndRef ind) indimpls; list_iter_i (fun j impls -> - maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) - (is_implicit_args()) impls) + maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) constrimpls) impls; if_verbose ppnl (minductive_message names); @@ -784,7 +799,7 @@ let declare_fix boxed kind f def t imps = } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + maybe_declare_manual_implicits false gr imps; gr let prepare_recursive_declaration fixnames fixtypes fixdefs = @@ -831,7 +846,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) @@ -1044,13 +1059,12 @@ let build_combined_scheme name schemes = (* 4.1| Support for mutually proved theorems *) let retrieve_first_recthm = function - | VarRef id -> - (pi2 (Global.lookup_named id),variable_opacity id) - | ConstRef cst -> - let {const_body=body;const_opaque=opaq} = - Global.lookup_constant cst in - (Option.map Declarations.force body,opaq) - | _ -> assert false + | VarRef id -> + (pi2 (Global.lookup_named id),variable_opacity id) + | ConstRef cst -> + let {const_body=body;const_opaque=opaq} = Global.lookup_constant cst in + (Option.map Declarations.force body,opaq) + | _ -> assert false let default_thm_id = id_of_string "Unnamed_thm" @@ -1108,19 +1122,19 @@ let look_for_mutual_statements thms = (* common coinductive conclusion *) let n = List.length thms in let inds = List.map (fun (id,(t,_) as x) -> - let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in + let (hyps,ccl) = Sign.decompose_prod_assum t in let whnf_hyp_hds = map_rel_context_with_binders (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) hyps in let ind_hyps = - List.filter ((<>) None) (list_map_i (fun i (_,b,t) -> + List.flatten (list_map_i (fun i (_,b,t) -> match kind_of_term t with | Ind (kn,_ as ind) when let mind = Global.lookup_mind kn in - mind.mind_ntypes = n & mind.mind_finite & b = None -> - Some (ind,x,i) + mind.mind_finite & b = None -> + [ind,x,i] | _ -> - None) 1 whnf_hyp_hds) in + []) 1 (List.rev whnf_hyp_hds)) in let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in @@ -1128,53 +1142,45 @@ let look_for_mutual_statements thms = | Ind (kn,_ as ind) when let mind = Global.lookup_mind kn in mind.mind_ntypes = n & not mind.mind_finite -> - Some (ind,x,0) + [ind,x,0] | _ -> - None in + [] in ind_hyps,ind_ccl) thms in let inds_hyps,ind_ccls = List.split inds in - let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in - let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in + let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in (* Check if all conclusions are coinductive in the same type *) + (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = - match ind_ccls with - | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest - -> Some (x :: List.map Option.get rest) - | _ -> None in + list_cartesians_filter (fun hyp oks -> + if List.for_all (of_same_mutind hyp) oks + then Some (hyp::oks) else None) [] ind_ccls in + let ordered_same_indccl = + List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in (* Check if some hypotheses are inductive in the same type *) let common_same_indhyp = - let rec find_same_ind inds = - match inds with - | []::_ -> - [] - | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms -> - let others' = List.map (List.filter (is_same_ind kn)) other_thms in - (x,others')::find_same_ind (hyps_thms1::other_thms) - | (None::hyps_thm1)::other_thms -> - find_same_ind (hyps_thm1::other_thms) - | [] -> - assert false in - find_same_ind inds_hyps in - let common_inds,finite = - match same_indccl, common_same_indhyp with - | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest -> - (* One occurrence of common inductive hyps and no common coind ccls *) - Option.get x::List.map (fun x -> Option.get (List.hd x)) rest, - false - | Some indccl, [] -> - (* One occurrence of common coind ccls and no common inductive hyps *) + list_cartesians_filter (fun hyp oks -> + if List.for_all (of_same_mutind hyp) oks + then Some (hyp::oks) else None) [] inds_hyps in + let ordered_inds,finite = + match ordered_same_indccl, common_same_indhyp with + | indccl::rest, _ -> + assert (rest=[]); + (* One occ. of common coind ccls and no common inductive hyps *) + if common_same_indhyp <> [] then + if_verbose warning "Assuming mutual coinductive statements."; + flush_all (); indccl, true - | _ -> - error - ("Cannot find a common mutual inductive premise or coinductive" ^ - " conclusion in the statements") in - let ordered_inds = List.sort compare_kn common_inds in - list_iter_i (fun i' ((kn,i),_,_) -> - if i <> i' then - error - ("Cannot find distinct (co)inductive types of the same family" ^ - "of mutual (co)inductive types")) - ordered_inds; + | [], _::_ -> + if same_indccl <> [] && + list_distinct (List.map pi1 (List.hd same_indccl)) then + if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all (); + (* assume the largest indices as possible *) + list_last common_same_indhyp, false + | _, [] -> + error + ("Cannot find common (mutual) inductive premises or coinductive" ^ + " conclusions in the statements.") + in let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in let rec_tac = if finite then @@ -1182,6 +1188,7 @@ let look_for_mutual_statements thms = | (id,_)::l -> Hiddentac.h_mutual_cofix true id l | _ -> assert false else + (* nl is dummy: it will be recomputed at Qed-time *) match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l | _ -> assert false in @@ -1208,9 +1215,10 @@ let start_proof_com kind thms hook = list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> - maybe_declare_manual_implicits false ref (is_implicit_args ()) imps; + maybe_declare_manual_implicits false ref imps; hook strength ref) thms_data in - start_proof id kind t ?init_tac:rec_tac hook + start_proof id kind t ?init_tac:rec_tac + ~compute_guard:(rec_tac<>None) hook let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then @@ -1220,17 +1228,17 @@ let check_anonymity id save_ident = *) let save_anonymous opacity save_ident = - let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in + let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; - save save_ident const persistence hook + save save_ident const do_guard persistence hook let save_anonymous_with_strength kind opacity save_ident = - let id,(const,_,hook) = Pfedit.cook_proof !save_hook in + let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save save_ident const (Global, Proof kind) hook + save save_ident const do_guard (Global, Proof kind) hook let admit () = let (id,k,typ,hook) = Pfedit.current_proof_statement () in diff --git a/toplevel/command.mli b/toplevel/command.mli index 8ac8c234..b42fafd0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: command.mli 11745 2009-01-04 18:43:08Z herbelin $ i*) (*i*) open Util @@ -56,17 +56,19 @@ val declare_assumption : identifier located list -> val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit -val compute_interning_datas : Environ.env -> 'a list -> 'b list -> +val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> + 'a list -> 'b list -> Term.types list ->Impargs.manual_explicitation list list -> 'a list * - ('b * (Names.identifier list * Impargs.implicits_list * + ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list * Topconstr.scope_name option list)) list val check_mutuality : Environ.env -> definition_object_kind -> (identifier * types) list -> unit -val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit +val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) * + decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : bool -> Entries.mutual_inductive_entry -> @@ -107,7 +109,7 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val set_start_hook : (types -> unit) -> unit val start_proof : identifier -> goal_kind -> types -> - ?init_tac:Proof_type.tactic -> declaration_hook -> unit + ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit val start_proof_com : goal_kind -> (lident option * (local_binder list * constr_expr)) list -> diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 884589e7..d32a773d 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml 10901 2008-05-07 18:53:48Z letouzey $ *) +(* $Id: coqinit.ml 11749 2009-01-05 14:01:04Z notin $ *) open Pp open System @@ -93,16 +93,11 @@ let theories_dirs_map = [ "theories/Init", "Init" ] -(* Initializes the LoadPath according to COQLIB and Coq_config *) +(* Initializes the LoadPath *) let init_load_path () = - let coqlib = - (* variable COQLIB overrides the default library *) - getenv_else "COQLIB" - (if Coq_config.local || !Flags.boot then Coq_config.coqtop - else Coq_config.coqlib) in + let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let dirs = "states" :: ["contrib"] in - let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in (* first user-contrib *) if Sys.file_exists user_contrib then Mltop.add_rec_path user_contrib Nameops.default_root_prefix; @@ -114,8 +109,6 @@ let init_load_path () = List.iter (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) theories_dirs_map; - (* then camlp4lib *) - add_ml_include camlp4; (* then current directory *) Mltop.add_path "." Nameops.default_root_prefix; (* additional loadpath, given with -I -include -R options *) @@ -129,13 +122,13 @@ let init_library_roots () = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) -(* We only assume that the variable COQTOP is set *) let init_ocaml_path () = - let coqtop = getenv_else "COQTOP" Coq_config.coqtop in + let coqsrc = Coq_config.coqsrc in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqtop dl) + Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) in - List.iter add_subdir - [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; - [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; - [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] + Mltop.add_ml_dir (Envars.coqlib ()); + List.iter add_subdir + [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; + [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; + [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f8c57ad2..f5d1d142 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 11209 2008-07-05 10:17:49Z herbelin $ *) +(* $Id: coqtop.ml 11830 2009-01-22 06:45:13Z notin $ *) open Pp open Util @@ -21,7 +21,8 @@ open Coqinit let get_version_date () = try - let ch = open_in (Coq_config.coqlib^"/revision") in + let coqlib = Envars.coqlib () in + let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -51,7 +52,9 @@ let set_batch_mode () = batch_mode := true let toplevel_default_name = make_dirpath [id_of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) -let set_toplevel_name dir = toplevel_name := Some dir +let set_toplevel_name dir = + if dir = empty_dirpath then error "Need a non empty toplevel module name"; + toplevel_name := Some dir let unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () @@ -68,16 +71,16 @@ let outputstate = ref "" let set_outputstate s = outputstate:=s let outputstate () = if !outputstate <> "" then extern_state !outputstate -let check_coq_overwriting p = - if string_of_id (list_last (repr_dirpath p)) = "Coq" then - error "The \"Coq\" logical root directory is reserved for the Coq library" - let set_default_include d = push_include (d,Nameops.default_root_prefix) let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix) let set_include d p = - let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p) + let p = dirpath_of_string p in + Library.check_coq_overwriting p; + push_include (d,p) let set_rec_include d p = - let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) + let p = dirpath_of_string p in + Library.check_coq_overwriting p; + push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -85,8 +88,8 @@ let add_load_vernacular verb s = let load_vernacular () = List.iter (fun (s,b) -> - if Flags.do_translate () then - with_option translate_file (Vernac.load_vernac b) s + if Flags.do_beautify () then + with_option beautify_file (Vernac.load_vernac b) s else Vernac.load_vernac b s) (List.rev !load_vernacular_list) @@ -110,13 +113,13 @@ let add_compile verbose s = compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in - let coqdoc_init_state = Constrintern.coqdoc_freeze () in + let coqdoc_init_state = Dumpglob.coqdoc_freeze () in List.iter (fun (v,f) -> States.unfreeze init_state; - Constrintern.coqdoc_unfreeze coqdoc_init_state; - if Flags.do_translate () then - with_option translate_file (Vernac.compile v) f + Dumpglob.coqdoc_unfreeze coqdoc_init_state; + if Flags.do_beautify () then + with_option beautify_file (Vernac.compile v) f else Vernac.compile v f) (List.rev !compile_list) @@ -132,7 +135,7 @@ let set_opt () = re_exec_version := "opt" let re_exec is_ide = let s = !re_exec_version in - let is_native = (Mltop.get()) = Mltop.Native in + let is_native = Mltop.is_native in (* Unix.readlink is not implemented on Windows architectures :-( let prog = try Unix.readlink "/proc/self/exe" @@ -177,8 +180,10 @@ let usage () = let warning s = msg_warning (str s) + let ide_args = ref [] let parse_args is_ide = + let glob_opt = ref false in let rec parse = function | [] -> () | "-with-geoproof" :: s :: rem -> @@ -240,21 +245,25 @@ let parse_args is_ide = | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem | "-load-vernac-object" :: [] -> usage () - | "-dump-glob" :: f :: rem -> dump_into_file f; parse rem + | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem + (* À ne pas documenter : l'option 'stdout' n'étant + éventuellement utile que pour le debugging... *) + | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem | "-dump-glob" :: [] -> usage () + | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem | "-require" :: f :: rem -> add_require f; parse rem | "-require" :: [] -> usage () - | "-compile" :: f :: rem -> add_compile false f; parse rem + | "-compile" :: f :: rem -> add_compile false f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem | "-compile" :: [] -> usage () - | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem + | "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem | "-compile-verbose" :: [] -> usage () | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem - | "-translate" :: rem -> make_translate true; parse rem + | "-beautify" :: rem -> make_beautify true; parse rem | "-unsafe" :: f :: rem -> add_unsafe f; parse rem | "-unsafe" :: [] -> usage () @@ -265,10 +274,15 @@ let parse_args is_ide = | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-emacs-U" :: rem -> Flags.print_emacs := true; Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem - + | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem - | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem + | "-coqlib" :: [] -> usage () + + | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0 + + | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 41783faa..f733a3d5 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *) open Pp open Util @@ -312,7 +312,13 @@ let explain_occur_check env ev rhs = str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself." -let explain_hole_kind env = function +let pr_ne_context_of header footer env = + if Environ.rel_context env = empty_rel_context & + Environ.named_context env = empty_named_context + then footer + else pr_ne_context_of header env + +let explain_hole_kind env evi = function | QuestionMark _ -> str "this placeholder" | CasesType -> str "the type of this pattern-matching problem" @@ -326,7 +332,12 @@ let explain_hole_kind env = function pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c | InternalHole -> - str "an internal placeholder" + str "an internal placeholder" ++ + Option.cata (fun evi -> + let env = Evd.evar_env evi in + str " of type " ++ pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env) + (mt ()) evi | TomatchTypeParameter (tyi,n) -> str "the " ++ nth n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ @@ -340,7 +351,7 @@ let explain_not_clean env ev t k = let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in - str "Tried to instantiate " ++ explain_hole_kind env k ++ + str "Tried to instantiate " ++ explain_hole_kind env None k ++ str " (" ++ str id ++ str ")" ++ spc () ++ str "with a term using variable " ++ var ++ spc () ++ str "which is not in its scope." @@ -350,25 +361,20 @@ let explain_unsolvability = function | Some (SeveralInstancesFound n) -> strbrk " (several distinct possible instances found)" -let pr_ne_context_of header footer env = - if Environ.rel_context env = empty_rel_context & - Environ.named_context env = empty_named_context then footer - else pr_ne_context_of header env - let explain_typeclass_resolution env evi k = match k with - InternalHole | ImplicitArg _ -> - (match Typeclasses.class_of_constr evi.evar_concl with - | Some c -> - let env = Evd.evar_env evi in - fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env evi.evar_concl ++ - pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env - | None -> mt()) - | _ -> mt() - + | GoalEvar | InternalHole | ImplicitArg _ -> + (match Typeclasses.class_of_constr evi.evar_concl with + | Some c -> + let env = Evd.evar_env evi in + fnl () ++ str "Could not find an instance for " ++ + pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env + | None -> mt()) + | _ -> mt() + let explain_unsolvable_implicit env evi k explain = - str "Cannot infer " ++ explain_hole_kind env k ++ + str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++ explain_unsolvability explain ++ str "." ++ explain_typeclass_resolution env evi k @@ -500,7 +506,7 @@ let explain_no_instance env (_,id) l = str "applied to arguments" ++ spc () ++ prlist_with_sep pr_spc (pr_lconstr_env env) l -let pr_constraints env evm = +let pr_constraints printenv env evm = let l = Evd.to_list evm in let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> @@ -508,7 +514,7 @@ let pr_constraints env evm = then let pe = pr_ne_context_of (str "In environment:") (mt ()) (reset_with_named_context evi.evar_hyps env) in - pe ++ fnl () ++ + (if printenv then pe ++ fnl () else mt ()) ++ prlist_with_sep (fun () -> fnl ()) (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l else @@ -518,13 +524,13 @@ let explain_unsatisfiable_constraints env evd constr = let evm = Evd.evars_of evd in match constr with | None -> - str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++ - pr_constraints env evm + str"Unable to satisfy the following constraints:" ++ fnl() ++ + pr_constraints true env evm | Some (evi, k) -> explain_unsolvable_implicit env evi k None ++ fnl () ++ if List.length (Evd.to_list evm) > 1 then - str"With the following meta variables:" ++ - fnl() ++ Evd.pr_evar_map evm + str"With the following constraints:" ++ fnl() ++ + pr_constraints false env evm else mt () let explain_mismatched_contexts env c i j = @@ -572,6 +578,10 @@ let explain_non_linear_proof c = str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ spc () ++ str "because a metavariable has several occurrences." +let explain_meta_in_type c = + str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++ + str " of another meta" + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t @@ -580,6 +590,7 @@ let explain_refiner_error = function | IntroNeedsProduct -> explain_intro_needs_product () | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp | NonLinearProof c -> explain_non_linear_proof c + | MetaInType c -> explain_meta_in_type c (* Inductive errors *) @@ -618,8 +629,8 @@ let error_bad_ind_parameters env c n v1 v2 = let pc = pr_lconstr_env_at_top env c in let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in - str "The " ++ nth n ++ str " argument of " ++ pv2 ++ brk(1,1) ++ - str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc ++ str "." + str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ + str " as " ++ nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = str "The name" ++ spc () ++ pr_id id ++ spc () ++ @@ -640,17 +651,16 @@ let error_not_an_arity id = let error_bad_entry () = str "Bad inductive definition." -let error_not_allowed_case_analysis dep kind i = - str (if dep then "Dependent" else "Non dependent") ++ - str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++ - str "is not allowed for inductive definition: " ++ - pr_inductive (Global.env()) i ++ str "." +let error_large_non_prop_inductive_not_in_type () = + str "Large non-propositional inductive types must be in Type." -let error_bad_induction dep indid kind = - str (if dep then "Dependent" else "Non dependent") ++ - str " induction for type " ++ pr_id indid ++ - str " and sort " ++ pr_sort kind ++ spc () ++ - str "is not allowed." +(* Recursion schemes errors *) + +let error_not_allowed_case_analysis isrec kind i = + str (if isrec then "Induction" else "Case analysis") ++ + strbrk " on sort " ++ pr_sort kind ++ + strbrk " is not allowed for inductive definition " ++ + pr_inductive (Global.env()) i ++ str "." let error_not_mutual_in_scheme ind ind' = if ind = ind' then @@ -674,13 +684,13 @@ let explain_inductive_error = function | SameNamesOverlap idl -> error_same_names_overlap idl | NotAnArity id -> error_not_an_arity id | BadEntry -> error_bad_entry () + | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () (* Recursion schemes errors *) let explain_recursion_scheme_error = function - | NotAllowedCaseAnalysis (dep,k,i) -> - error_not_allowed_case_analysis dep k i - | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind + | NotAllowedCaseAnalysis (isrec,k,i) -> + error_not_allowed_case_analysis isrec k i | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' (* Pattern-matching errors *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 89ba6aac..6a75b99c 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *) open Pp open Util @@ -281,22 +281,22 @@ let rec find_pattern xl = function error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") let rec interp_list_parser hd = function - | [] -> [], List.rev hd + | [] -> [], [], List.rev hd | NonTerminal id :: tl when id = ldots_var -> let ((x,y,sl),tl') = find_pattern [] (hd,tl) in - let yl,tl'' = interp_list_parser [] tl' in - (* We remember the second copy of each recursive part variable to *) - (* remove it afterwards *) - y::yl, SProdList (x,sl) :: tl'' + let yl,xl,tl'' = interp_list_parser [] tl' in + (* We remember each pair of variable denoting a recursive part to *) + (* remove the second copy of it afterwards *) + (y,x)::yl, x::xl, SProdList (x,sl) :: tl'' | (Terminal _ | Break _) as s :: tl -> if hd = [] then - let yl,tl' = interp_list_parser [] tl in - yl, s :: tl' + let yl,xl,tl' = interp_list_parser [] tl in + yl, xl, s :: tl' else interp_list_parser (s::hd) tl | NonTerminal _ as x :: tl -> - let yl,tl' = interp_list_parser [x] tl in - yl, List.rev_append hd tl' + let yl,xl,tl' = interp_list_parser [x] tl in + yl, xl, List.rev_append hd tl' | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" (* Find non-terminal tokens of notation *) @@ -345,10 +345,20 @@ let is_numeral symbs = let analyse_notation_tokens l = let vars,l = raw_analyse_notation_tokens l in - let recvars,l = interp_list_parser [] l in - ((if recvars = [] then [] else ldots_var::recvars), vars, l) - -let remove_vars = List.fold_right List.remove_assoc + let extrarecvars,recvars,l = interp_list_parser [] l in + (if extrarecvars = [] then [], [], vars, l + else extrarecvars, recvars, list_subtract vars recvars, l) + +let remove_extravars extrarecvars (vars,recvars) = + let vars = + List.fold_right (fun (x,y) l -> + if List.assoc x l <> List.assoc y recvars then + error + "Two end variables of a recursive notation are not in the same scope." + else + List.remove_assoc x l) + extrarecvars (List.remove_assoc ldots_var vars) in + (vars,recvars) (**********************************************************************) (* Build pretty-printing rules *) @@ -400,7 +410,7 @@ let is_operator s = let l = String.length s in l <> 0 & (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or - s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~') + s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~' or s.[0] = '$') let is_prod_ident = function | Terminal s when is_letter s.[0] or s.[0] = '_' -> true @@ -422,7 +432,7 @@ let make_hunks etyps symbols from = | NonTerminal m :: prods -> let i = list_index m vars in let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in - let u = UnpMetaVar (i ,prec) in + let u = UnpMetaVar (i,prec) in if prods <> [] && is_non_terminal (List.hd prods) then u :: add_break 1 (make CanBreak prods) else @@ -745,7 +755,7 @@ let check_rule_productivity l = error "A recursive notation must start with at least one symbol." let is_not_printable = function - | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true + | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true | _ -> false let find_precedence lev etyps symbols = @@ -814,7 +824,7 @@ let compute_syntax_data (df,modifiers) = (* Notation defaults to NONA *) let assoc = match assoc with None -> Some Gramext.NonA | a -> a in let toks = split_notation_string df in - let (recvars,vars,symbols) = analyse_notation_tokens toks in + let (extrarecvars,recvars,vars,symbols) = analyse_notation_tokens toks in let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in let need_squash = (symbols <> symbols') in @@ -833,7 +843,7 @@ let compute_syntax_data (df,modifiers) = let prec = (n,List.map (assoc_of_type n) typs) in let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in let df' = (Lib.library_dp(),df) in - let i_data = (onlyparse,recvars,vars,(ntn_for_interp,df')) in + let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in (i_data,sy_data) (**********************************************************************) @@ -939,14 +949,15 @@ let add_notation_in_scope local df c mods scope = let sy_rules = make_syntax_rules sy_data in Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)); (* Declare interpretation *) - let (onlyparse,recvars,vars,df') = i_data in - let (acvars,ac) = interp_aconstr [] vars c in - let a = (remove_vars recvars acvars,ac) (* For recursive parts *) in + let (onlyparse,extrarecvars,recvars,vars,df') = i_data in + let (acvars,ac) = interp_aconstr [] (vars,recvars) c in + let a = (remove_extravars extrarecvars acvars,ac) in let onlyparse = onlyparse or is_not_printable ac in - Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df')) + Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')) let add_notation_interpretation_core local df names c scope onlyparse = - let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in + let dfs = split_notation_string df in + let (extrarecvars,recvars,vars,symbs) = analyse_notation_tokens dfs in (* Redeclare pa/pp rules *) if not (is_numeral symbs) then begin let sy_rules = recover_notation_syntax (make_notation_key symbs) in @@ -954,10 +965,10 @@ let add_notation_interpretation_core local df names c scope onlyparse = end; (* Declare interpretation *) let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in - let (acvars,ac) = interp_aconstr names vars c in - let a = (remove_vars recs acvars,ac) (* For recursive parts *) in + let (acvars,ac) = interp_aconstr names (vars,recvars) c in + let a = (remove_extravars extrarecvars acvars,ac) in let onlyparse = onlyparse or is_not_printable ac in - Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df')) + Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')) (* Notations without interpretation (Reserved Notation) *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index c3bdadfa..fefc0b27 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli 9677 2007-02-24 14:17:54Z herbelin $ i*) +(*i $Id: metasyntax.mli 11481 2008-10-20 19:23:51Z herbelin $ i*) (*i*) open Util @@ -56,3 +56,7 @@ val print_grammar : string -> unit (* Removes quotes in a notation *) val standardize_locatable_notation : string -> string + +(* Evaluate whether a notation is not printable *) + +val is_not_printable : aconstr -> bool diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index ac30f890..176f336b 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -11,7 +11,7 @@ * camlp4deps will not work for this file unless Makefile system enhanced. *) -(* $Id: mltop.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *) open Util open Pp @@ -47,8 +47,10 @@ open Vernacinterp (* This path is where we look for .cmo *) let coq_mlpath_copy = ref ["."] -let keep_copy_mlpath path = - coq_mlpath_copy := path :: !coq_mlpath_copy +let keep_copy_mlpath path = + let cpath = canonical_path_name path in + let filter path' = (cpath <> canonical_path_name path') in + coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy (* If there is a toplevel under Coq *) type toplevel = { @@ -62,17 +64,18 @@ type toplevel = { type kind_load = | WithTop of toplevel | WithoutTop - | Native (* Must be always initialized *) -let load = ref Native +let load = ref WithoutTop -(* Sets and initializes the kind of loading *) -let set kload = load := kload -let get () = !load +(* Are we in a native version of Coq? *) +let is_native = IFDEF Byte THEN false ELSE true END -(* Resets load *) -let remove ()= load := Native +(* Sets and initializes a toplevel (if any) *) +let set_top toplevel = load := WithTop toplevel + +(* Removes the toplevel (if any) *) +let remove ()= load := WithoutTop (* Tests if an Ocaml toplevel runs under Coq *) let is_ocaml_top () = @@ -81,10 +84,7 @@ let is_ocaml_top () = |_ -> false (* Tests if we can load ML files *) -let enable_load () = - match !load with - | WithTop _ | WithoutTop -> true - |_ -> false +let has_dynlink = IFDEF HasDynlink THEN true ELSE false END (* Runs the toplevel loop of Ocaml *) let ocaml_toploop () = @@ -103,24 +103,21 @@ let dir_ml_load s = str s ++ str" to Coq code.")) (* TO DO: .cma loading without toplevel *) | WithoutTop -> - IFDEF Byte THEN + IFDEF HasDynlink THEN (* WARNING * if this code section starts to use a module not used elsewhere * in this file, the Makefile dependency logic needs to be updated. *) - let _,gname = where_in_path true !coq_mlpath_copy s in + let warn = Flags.is_verbose() in + let _,gname = where_in_path ~warn !coq_mlpath_copy s in try Dynlink.loadfile gname; - Dynlink.add_interfaces - [(String.capitalize (Filename.chop_suffix - (Filename.basename gname) ".cmo"))] - [Filename.dirname gname] with | Dynlink.Error a -> errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) - ELSE () END - | Native -> - errorlabstrm "Mltop.no_load_object" - (str"Loading of ML object file forbidden in a native Coq.") + ELSE + errorlabstrm "Mltop.no_load_object" + (str"Loading of ML object file forbidden in a native Coq.") + END (* Dynamic interpretation of .ml *) let dir_ml_use s = @@ -132,7 +129,7 @@ let dir_ml_use s = let add_ml_dir s = match !load with | WithTop t -> t.add_dir s; keep_copy_mlpath s - | WithoutTop -> keep_copy_mlpath s + | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () (* For Rec Add ML Path *) @@ -182,15 +179,44 @@ let mod_of_name name = in String.capitalize base -let file_of_name name = - let bname = String.uncapitalize name in - let fname = make_suffix bname ".cmo" in - if (is_in_path !coq_mlpath_copy fname) then fname - else let fname=make_suffix bname ".cma" in - if (is_in_path !coq_mlpath_copy fname) then fname +let get_ml_object_suffix name = + if Filename.check_suffix name ".cmo" then + Some ".cmo" + else if Filename.check_suffix name ".cma" then + Some ".cma" + else if Filename.check_suffix name ".cmxs" then + Some ".cmxs" else + None + +let file_of_name name = + let name = String.uncapitalize name in + let suffix = get_ml_object_suffix name in + let fail s = errorlabstrm "Mltop.load_object" - (str"File not found on loadpath : " ++ str (bname^".cm[oa]")) + (str"File not found on loadpath : " ++ str s) in + if is_native then + let name = match suffix with + | Some ((".cmo"|".cma") as suffix) -> + (Filename.chop_suffix name suffix) ^ ".cmxs" + | Some ".cmxs" -> name + | _ -> name ^ ".cmxs" + in + if is_in_path !coq_mlpath_copy name then name else fail name + else + let (full, base) = match suffix with + | Some ".cmo" | Some ".cma" -> true, name + | Some ".cmxs" -> false, Filename.chop_suffix name ".cmxs" + | _ -> false, name + in + if full then + if is_in_path !coq_mlpath_copy base then base else fail base + else + let name = base ^ ".cmo" in + if is_in_path !coq_mlpath_copy name then name else + let name = base ^ ".cma" in + if is_in_path !coq_mlpath_copy name then name else + fail (base ^ ".cm[oa]") (* TODO: supprimer ce hack, si possible *) (* Initialisation of ML modules that need the state (ex: tactics like @@ -242,7 +268,7 @@ let unfreeze_ml_modules x = (fun name -> let mname = mod_of_name name in if not (module_is_known mname) then - if enable_load() then + if has_dynlink then let fname = file_of_name mname in load_object mname fname else @@ -272,9 +298,9 @@ let cache_ml_module_object (_,{mnames=mnames}) = if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_object mname fname; - if_verbose msgnl (str"done]") + if_verbose msgnl (str" done]") with e -> - if_verbose msgnl (str"failed]"); + if_verbose msgnl (str" failed]"); raise e end; add_loaded_module mname) @@ -286,7 +312,9 @@ let (inMLModule,outMLModule) = declare_object {(default_object "ML-MODULE") with load_function = (fun _ -> cache_ml_module_object); cache_function = cache_ml_module_object; - export_function = export_ml_module_object } + export_function = export_ml_module_object; + subst_function = (fun (_,_,o) -> o); + classify_function = (fun (_,o) -> Substitute o) } let declare_ml_modules l = Lib.add_anonymous_leaf (inMLModule {mnames=l}) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index b869f70b..875fb423 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mltop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: mltop.mli 11528 2008-10-31 08:40:42Z glondu $ i*) (* If there is a toplevel under Coq, it is described by the following record. *) @@ -16,25 +16,20 @@ type toplevel = { add_dir : string -> unit; ml_loop : unit -> unit } -(* Determines the behaviour of Coq with respect to ML files (compiled - or not) *) -type kind_load= - | WithTop of toplevel - | WithoutTop - | Native +(* Sets and initializes a toplevel (if any) *) +val set_top : toplevel -> unit -(* Sets and initializes the kind of loading *) -val set : kind_load -> unit -val get : unit -> kind_load +(* Are we in a native version of Coq? *) +val is_native : bool -(* Resets the kind of loading *) +(* Removes the toplevel (if any) *) val remove : unit -> unit (* Tests if an Ocaml toplevel runs under Coq *) val is_ocaml_top : unit -> bool (* Tests if we can load ML files *) -val enable_load : unit -> bool +val has_dynlink : bool (* Starts the Ocaml toplevel loop *) val ocaml_toploop : unit -> unit diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index a9ff3326..caf32305 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: protectedtoplevel.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: protectedtoplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *) open Pp open Line_oriented_parser open Vernac +open Vernacexpr (* The toplevel parsing loop we propose here is more robust to printing errors. The philosophy is that all commands should be individually wrapped @@ -130,7 +131,8 @@ let rec parse_one_command_group input_channel = !global_request_id !count None) | Some(rank, e) -> (match e with - DuringCommandInterp(a,e1) -> + | DuringCommandInterp(a,e1) + | Stdpp.Exc_located (a,DuringSyntaxChecking e1) -> output_results_nl (acknowledge_command !global_request_id rank (Some e1)) @@ -164,7 +166,8 @@ let protected_loop input_chan = | End_of_file -> exit 0 | DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit | DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop - | DuringCommandInterp(loc, e) -> + | DuringCommandInterp(loc, e) + | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> explain_and_restart e | e -> explain_and_restart e in begin diff --git a/toplevel/record.ml b/toplevel/record.ml index 306ab047..4a2ef7db 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *) open Pp open Util @@ -38,17 +38,23 @@ let interp_evars evdref env ?(impls=([],[])) k typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (out_name na, ([], impl, Notation.compute_arguments_scope typ)) + in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) -let interp_fields_evars isevars env l = - List.fold_left - (fun (env, uimpls, params, impls) ((loc, i), b, t) -> +let interp_fields_evars isevars env nots l = + List.fold_left2 + (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in - let data = mk_interning_data env i impl t' in + let impls = + match i with + | Anonymous -> impls + | Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls) + in let d = (i,b',t') in - (push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls))) - (env, [], [], ([], [])) l + (* Temporary declaration of notations and scopes *) + Option.iter (declare_interning_data impls) no; + (push_rel d env, impl :: uimpls, d::params, impls)) + (env, [], [], ([], [])) nots l let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) @@ -56,18 +62,21 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields id t ps fs = +let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in - let (env1,newps), imps = interp_context Evd.empty env0 ps in - let fullarity = it_mkProd_or_LetIn t newps in - let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let evars = ref (Evd.create_evar_defs Evd.empty) in + let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in + let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in + let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,impls,newfs,data = - interp_fields_evars evars env_ar (binders_of_decls fs) + interp_fields_evars evars env_ar nots (binders_of_decls fs) in - let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in - let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in - let ce t = Evarutil.check_evars env0 Evd.empty !evars t in + let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in + let evars = Typeclasses.resolve_typeclasses env_ar evars in + let sigma = Evd.evars_of evars in + let newps = Evarutil.nf_rel_context_evar sigma newps in + let newfs = Evarutil.nf_rel_context_evar sigma newfs in + let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps; List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs; imps, newps, impls, newfs @@ -198,8 +207,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = ConstRef kn in let constr_fi = mkConst kn in - Impargs.maybe_declare_manual_implicits - false refi (Impargs.is_implicit_args()) impls; + Impargs.maybe_declare_manual_implicits false refi impls; if coe then begin let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi Global cl @@ -210,11 +218,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls with NotDefinable why -> warning_or_error coe indsp why; (None::sp_projs,NoProjection fi::subst) in - (nfi-1,(optci=None)::kinds,sp_projs,subst)) + (nfi-1,(fi, optci=None)::kinds,sp_projs,subst)) (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) -let declare_structure id idbuild paramimpls params arity fieldimpls fields +let declare_structure finite id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = let nparams = List.length params and nfields = List.length fields in let args = extended_rel_list nfields params in @@ -224,26 +232,130 @@ let declare_structure id idbuild paramimpls params arity fieldimpls fields { mind_entry_typename = id; mind_entry_arity = arity; mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let declare_as_coind = - (* CoInd if recursive; otherwise Ind to have compat on _ind schemes *) - dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) in + mind_entry_lc = [type_constructor] } + in + (* spiwack: raises an error if the structure is supposed to be non-recursive, + but isn't *) + (* there is probably a way to push this to "declare_mutual" *) + begin match finite with + | BiFinite -> + if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then + error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record." + | _ -> () + end; let mie = { mind_entry_params = List.map degenerate_decl params; mind_entry_record = true; - mind_entry_finite = not declare_as_coind; + mind_entry_finite = recursivity_flag_of_kind finite; mind_entry_inds = [mie_ind] } in let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in let build = ConstructRef (rsp,1) in if is_coe then Class.try_add_new_coercion build Global; - Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); - kn + Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs); + kn,0 + +let implicits_of_context ctx = + list_map_i (fun i name -> + let explname = + match name with + | Name n -> Some n + | Anonymous -> None + in ExplByPos (i, explname), (true, true)) + 1 (List.rev (Anonymous :: (List.map pi1 ctx))) + +open Typeclasses + +let typeclasses_db = "typeclass_instances" + +let qualid_of_con c = + Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) + +let set_rigid c = + Auto.add_hints false [typeclasses_db] + (Vernacexpr.HintsTransparency ([qualid_of_con c], false)) + +let declare_instance_cst glob con = + let instance = Typeops.type_of_constant (Global.env ()) con in + let _, r = Sign.decompose_prod_assum instance in + match class_of_constr r with + | Some tc -> add_instance (new_instance tc None glob con) + | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") + +let declare_class finite def id idbuild paramimpls params arity fieldimpls fields + ?(kind=StructureComponent) ?name is_coe coers = + let fieldimpls = + (* Make the class and all params implicits in the projections *) + let ctx_impls = implicits_of_context params in + let len = succ (List.length params) in + List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) fieldimpls + in + let impl, projs = + match fields with + | [(Name proj_name, _, field)] when def -> + let class_body = it_mkLambda_or_LetIn field params in + let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in + let class_entry = + { const_entry_body = class_body; + const_entry_type = class_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in + let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in + let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in + let proj_entry = + { const_entry_body = proj_body; + const_entry_type = Some proj_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref paramimpls; + Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); + set_rigid cst; (* set_rigid proj_cst; *) + cref, [proj_name, Some proj_cst] + | _ -> + let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in + let ind = declare_structure BiFinite (snd id) idbuild paramimpls + params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields + ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) + in + (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *) + IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y)) + (List.rev fields) (Recordops.lookup_projections ind)) + in + let ctx_context = + List.map (fun (na, b, t) -> + match Typeclasses.class_of_constr t with + | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*) + | None -> None) + params, params + in + let k = + { cl_impl = impl; + cl_context = ctx_context; + cl_props = fields; + cl_projs = projs } + in + List.iter2 (fun p sub -> + if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) + k.cl_projs coers; + add_class k; impl + +open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) -let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = +let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = + let cfs,notations = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function Vernacexpr.AssumExpr((_,Name id),_) -> id::acc @@ -252,8 +364,16 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let allnames = idstruc::(List.fold_left extract_name [] fs) in if not (list_distinct allnames) then error "Two objects have the same name"; (* Now, younger decl in params and fields is on top *) - let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - declare_structure idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers - + let sc = Option.map mkSort s in + let implpars, params, implfs, fields = + States.with_heavy_rollback (fun () -> + typecheck_params_and_fields idstruc sc ps notations fs) () + in + match kind with + | Class b -> + declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers + | _ -> + let arity = Option.cata (fun x -> x) (new_Type ()) sc in + let implfs = List.map + (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs + in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers) diff --git a/toplevel/record.mli b/toplevel/record.mli index 48181437..b49c26bc 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: record.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: record.mli 11809 2009-01-20 11:39:55Z aspiwack $ i*) (*i*) open Names @@ -15,6 +15,7 @@ open Sign open Vernacexpr open Topconstr open Impargs +open Libnames (*i*) (* [declare_projections ref name coers params fields] declare projections of @@ -24,17 +25,17 @@ open Impargs val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> manual_explicitation list list -> rel_context -> - bool list * constant option list + (name * bool) list * constant option list -val declare_structure : identifier -> identifier -> - manual_explicitation list -> rel_context -> (* params *) - Term.constr -> (* arity *) +val declare_structure : Decl_kinds.recursivity_kind -> + identifier -> identifier -> + manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool -> (* coercion? *) bool list -> (* field coercions *) - mutual_inductive + inductive val definition_structure : - lident with_coercion * local_binder list * - (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name + inductive_kind*Decl_kinds.recursivity_kind *lident with_coercion * local_binder list * + (local_decl_expr with_coercion with_notation) list * identifier * sorts option -> global_reference diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 8a9ef501..a1acd1d6 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 11317 2008-08-07 15:52:38Z barras $ *) +(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *) open Pp open Util open Flags open Cerrors open Vernac +open Vernacexpr open Pcoq open Protectedtoplevel @@ -262,6 +263,7 @@ let rec is_pervasive_exn = function | Error_in_file (_,_,e) -> is_pervasive_exn e | Stdpp.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e + | DuringSyntaxChecking e -> is_pervasive_exn e | _ -> false (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D @@ -270,7 +272,8 @@ let rec is_pervasive_exn = function let print_toplevel_error exc = let (dloc,exc) = match exc with - | DuringCommandInterp (loc,ie) -> + | DuringCommandInterp (loc,ie) + | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) | _ -> (None, exc) in @@ -321,7 +324,8 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ as e -> e + | DuringCommandInterp _ + | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e | e -> if is_pervasive_exn e then e diff --git a/toplevel/usage.ml b/toplevel/usage.ml index b0b0f826..96ff8cbc 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml 11209 2008-07-05 10:17:49Z herbelin $ *) +(* $Id: usage.ml 11858 2009-01-26 13:27:23Z notin $ *) let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; - Printf.printf "compiled on %s\n" Coq_config.compile_date; + Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; exit 0 (* print the usage of coqtop (or coqc) on channel co *) @@ -57,6 +57,7 @@ let print_usage_channel co command = -batch batch mode (exits just after arguments parsing) -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs + -noglob f do not dump globalizations -dump-glob f dump globalizations in file f (to be used by coqdoc) -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) -impredicative-set set sort Set impredicative @@ -80,6 +81,18 @@ let print_usage_coqc () = print_usage "Usage: coqc <options> <Coq options> file...\n options are: -verbose compile verbosely - -bindir override the default directory where coqc looks for coqtop -image f specify an alternative executable for Coq -t keep temporary files\n\n" + +(* Print the configuration information *) + +let print_config () = + if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; + Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; + Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc; + Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin; + Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib; + Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; + Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin; + Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib + diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 97814fd2..0ee58f4d 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -6,15 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: usage.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: usage.mli 11830 2009-01-22 06:45:13Z notin $ i*) (*s Prints the version number on the standard output and exits (with 0). *) val version : unit -> 'a -(*s Prints the usage on the error output, preceeded by a user-provided message. *) +(*s Prints the usage on the error output, preceded by a user-provided message. *) val print_usage : string -> unit (*s Prints the usage on the error output. *) val print_usage_coqtop : unit -> unit val print_usage_coqc : unit -> unit + +(*s Prints the configuration information. *) +val print_config : unit -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c331c13b..c5549503 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 10836 2008-04-23 11:43:58Z courtieu $ *) +(* $Id: vernac.ml 11801 2009-01-18 20:11:41Z herbelin $ *) (* Parsing of vernacular. *) @@ -32,7 +32,8 @@ exception DuringCommandInterp of Util.loc * exn let raise_with_file file exc = let (cmdloc,re) = match exc with - | DuringCommandInterp(loc,e) -> (loc,e) + | DuringCommandInterp(loc,e) + | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e) | e -> (dummy_loc,e) in let (inner,inex) = @@ -56,7 +57,9 @@ let real_error = function the file we parse seems a bit risky to me. B.B. *) let open_file_twice_if verbosely fname = - let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in + let paths = Library.get_load_paths () in + let _,longfname = + find_file_in_path ~warn:(Flags.is_verbose()) paths fname in let in_chan = open_in longfname in let verb_ch = if verbosely then Some (open_in longfname) else None in let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in @@ -93,23 +96,24 @@ let parse_phrase (po, verbch) = * parses, and is verbose on "primitives" commands if verbosely is true *) let just_parsing = ref false -let chan_translate = ref stdout +let chan_beautify = ref stdout +let beautify_suffix = ".beautified" let set_formatter_translator() = - let ch = !chan_translate in + let ch = !chan_beautify in let out s b e = output ch s b e in Format.set_formatter_output_functions out (fun () -> flush ch); Format.set_max_boxes max_int let pr_new_syntax loc ocom = let loc = unloc loc in - if !translate_file then set_formatter_translator(); + if !beautify_file then set_formatter_translator(); let fs = States.freeze () in let com = match ocom with | Some VernacNop -> mt() | Some com -> pr_vernac com | None -> mt() in - if !translate_file then + if !beautify_file then msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) else msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); @@ -121,33 +125,34 @@ let rec vernac_com interpfun (loc,com) = | VernacLoad (verbosely, fname) -> let fname = expand_path_macros fname in (* translator state *) - let ch = !chan_translate in + let ch = !chan_beautify in let cs = Lexer.com_state() in let cl = !Pp.comments in (* end translator state *) (* coqdoc state *) - let cds = Constrintern.coqdoc_freeze() in - if !Flags.translate_file then + let cds = Dumpglob.coqdoc_freeze() in + if !Flags.beautify_file then begin - let _,f = find_file_in_path (Library.get_load_paths ()) + let _,f = find_file_in_path ~warn:(Flags.is_verbose()) + (Library.get_load_paths ()) (make_suffix fname ".v") in - chan_translate := open_out (f^"8"); + chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] end; begin try read_vernac_file verbosely (make_suffix fname ".v"); - if !Flags.translate_file then close_out !chan_translate; - chan_translate := ch; + if !Flags.beautify_file then close_out !chan_beautify; + chan_beautify := ch; Lexer.restore_com_state cs; Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds + Dumpglob.coqdoc_unfreeze cds with e -> - if !Flags.translate_file then close_out !chan_translate; - chan_translate := ch; + if !Flags.beautify_file then close_out !chan_beautify; + chan_beautify := ch; Lexer.restore_com_state cs; Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds; + Dumpglob.coqdoc_unfreeze cds; raise e end @@ -164,7 +169,7 @@ let rec vernac_com interpfun (loc,com) = in try - if do_translate () then pr_new_syntax loc (Some com); + if do_beautify () then pr_new_syntax loc (Some com); interp com with e -> Format.set_formatter_out_channel stdout; @@ -191,7 +196,7 @@ and read_vernac_file verbosely s = close_input in_chan input; (* we must close the file first *) match real_error e with | End_of_input -> - if do_translate () then pr_new_syntax (make_loc (max_int,max_int)) None + if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None | _ -> raise_with_file fname e (* raw_do_vernac : char Stream.t -> unit @@ -214,23 +219,26 @@ let set_xml_end_library f = xml_end_library := f (* Load a vernac file. Errors are annotated with file and location *) let load_vernac verb file = - chan_translate := - if !Flags.translate_file then open_out (file^"8") else stdout; + chan_beautify := + if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; try read_vernac_file verb file; - if !Flags.translate_file then close_out !chan_translate; + if !Flags.beautify_file then close_out !chan_beautify; with e -> - if !Flags.translate_file then close_out !chan_translate; + if !Flags.beautify_file then close_out !chan_beautify; raise_with_file file e (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = - let ldir,long_f_dot_v = Library.start_library f in - if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); - if !Flags.xml_export then !xml_start_library (); - let _ = load_vernac verbosely long_f_dot_v in - if Pfedit.get_all_proof_names () <> [] then - (message "Error: There are pending proofs"; exit 1); - if !Flags.xml_export then !xml_end_library (); - Library.save_library_to ldir (long_f_dot_v ^ "o") + let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in + if Dumpglob.multi_dump () then + Dumpglob.open_glob_file (f ^ ".glob"); + Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); + if !Flags.xml_export then !xml_start_library (); + let _ = load_vernac verbosely long_f_dot_v in + if Pfedit.get_all_proof_names () <> [] then + (message "Error: There are pending proofs"; exit 1); + if !Flags.xml_export then !xml_end_library (); + if Dumpglob.multi_dump () then Dumpglob.close_glob_file (); + Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3f474239..c95c89d3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 11313 2008-08-07 11:15:03Z barras $ i*) +(*i $Id: vernacentries.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -182,8 +182,11 @@ let show_match id = let print_path_entry (s,l) = (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s) -let print_loadpath () = +let print_loadpath dir = let l = Library.get_full_load_paths () in + let l = match dir with + | None -> l + | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in msgnl (Pp.t (str "Logical Path: " ++ tab () ++ str "Physical path:" ++ fnl () ++ prlist_with_sep pr_fnl print_path_entry l)) @@ -232,7 +235,7 @@ let dump_universes s = let locate_file f = try - let _,file = System.where_in_path false (Library.get_load_paths ()) f in + let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in msgnl (str file) with Not_found -> msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ @@ -277,7 +280,7 @@ let print_located_module r = let global_with_alias r = let gr = global_with_alias r in - if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + Dumpglob.add_glob (loc_of_reference r) gr; gr (**********) @@ -307,49 +310,31 @@ let start_proof_and_print k l hook = print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let current_dirpath sec = - drop_dirpath_prefix (Lib.library_dp ()) - (if sec then Lib.cwd () - else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())) - -let dump_definition (loc, id) sec s = - Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc)) - (string_of_dirpath (current_dirpath sec)) (string_of_id id)) - -let dump_reference loc modpath ident ty = - dump_string (Printf.sprintf "R%d %s %s %s %s\n" - (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty) - -let dump_constraint ((loc, n), _, _) sec ty = - match n with - | Name id -> dump_definition (loc, id) sec ty - | Anonymous -> () - -let vernac_definition (local,_,_ as k) (_,id as lid) def hook = - if !Flags.dump then dump_definition lid false "def"; - match def with - | ProveBody (bl,t) -> (* local binders, typ *) - if Lib.is_modtype () then - errorlabstrm "Vernacentries.VernacDefinition" - (str "Proof editing mode not supported in module types.") - else - let hook _ _ = () in - start_proof_and_print (local,DefinitionBody Definition) - [Some lid,(bl,t)] hook - | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with - | None -> None - | Some r -> - let (evc,env)= Command.get_current_context () in - Some (interp_redexp env evc r) in - declare_definition id k bl red_option c typ_opt hook - +let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = + Dumpglob.dump_definition lid false "def"; + (match def with + | ProveBody (bl,t) -> (* local binders, typ *) + if Lib.is_modtype () then + errorlabstrm "Vernacentries.VernacDefinition" + (str "Proof editing mode not supported in module types") + else + let hook _ _ = () in + start_proof_and_print (local,DefinitionBody Definition) + [Some lid, (bl,t)] hook + | DefineBody (bl,red_option,c,typ_opt) -> + let red_option = match red_option with + | None -> None + | Some r -> + let (evc,env)= Command.get_current_context () in + Some (interp_redexp env evc r) in + declare_definition id k bl red_option c typ_opt hook) + let vernac_start_proof kind l lettop hook = - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun (id, _) -> match id with - | Some lid -> dump_definition lid false "prf" - | None -> ()) l; + | Some lid -> Dumpglob.dump_definition lid false "prf" + | None -> ()) l; if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" @@ -383,28 +368,75 @@ let vernac_exact_proof c = let vernac_assumption kind l nl= let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> - if !dump then - List.iter (fun lid -> - if global then dump_definition lid false "ax" - else dump_definition lid true "var") idl; - declare_assumption idl is_coe kind [] c false false nl) l - -let vernac_inductive f indl = - if !dump then - List.iter (fun ((lid, _, _, cstrs), _) -> - dump_definition lid false"ind"; - List.iter (fun (_, (lid, _)) -> - dump_definition lid false "constr") cstrs) - indl; - build_mutual indl f + List.iter (fun (is_coe,(idl,c)) -> + if Dumpglob.dump () then + List.iter (fun lid -> + if global then Dumpglob.dump_definition lid false "ax" + else Dumpglob.dump_definition lid true "var") idl; + declare_assumption idl is_coe kind [] c false false nl) l + +let vernac_record k finite struc binders sort nameopt cfs = + let const = match nameopt with + | None -> add_prefix "Build_" (snd (snd struc)) + | Some (_,id as lid) -> + Dumpglob.dump_definition lid false "constr"; id in + let sigma = Evd.empty in + let env = Global.env() in + let s = Option.map (fun x -> + let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in + match kind_of_term s with + | Sort s -> s + | _ -> user_err_loc + (constr_loc x,"definition_structure", str "Sort expected.")) sort + in + if Dumpglob.dump () then ( + Dumpglob.dump_definition (snd struc) false "rec"; + List.iter (fun ((_, x), _) -> + match x with + | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" + | _ -> ()) cfs); + ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s)) + +let vernac_inductive finite indl = + if Dumpglob.dump () then + List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> + match cstrs with + | Constructors cstrs -> + Dumpglob.dump_definition lid false "ind"; + List.iter (fun (_, (lid, _)) -> + Dumpglob.dump_definition lid false "constr") cstrs + | _ -> () (* dumping is done by vernac_record (called below) *) ) + indl; + match indl with + | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> + vernac_record (match b with Class true -> Class false | _ -> b) + finite id bl c oc fs + | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> + let f = + let (coe, ((loc, id), ce)) = l in + ((coe, AssumExpr ((loc, Name id), ce)), None) + in vernac_record (Class true) finite id bl c None [f] + | [ ( id , bl , c , Class true, _), _ ] -> + Util.error "Definitional classes must have a single method" + | [ ( id , bl , c , Class false, Constructors _), _ ] -> + Util.error "Inductive classes not supported" + | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> + Util.error "where clause not supported for (co)inductive records" + | _ -> let unpack = function + | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn + | _ -> Util.error "Cannot handle mutually (co)inductive records." + in + let indl = List.map unpack indl in + Command.build_mutual indl (recursivity_flag_of_kind finite) let vernac_fixpoint l b = - List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l; + if Dumpglob.dump () then + List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_recursive l b let vernac_cofixpoint l b = - List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l; + if Dumpglob.dump () then + List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_corecursive l b let vernac_scheme = build_scheme @@ -415,9 +447,11 @@ let vernac_combined_scheme = build_combined_scheme (* Modules *) let vernac_import export refl = - let import ref = Library.import_module export (qualid_of_reference ref) in - List.iter import refl; - Lib.add_frozen_state () + let import ref = + Library.import_module export (qualid_of_reference ref) + in + List.iter import refl; + Lib.add_frozen_state () let vernac_declare_module export (loc, id) binders_ast mty_ast_o = (* We check the state of the system (in section, in module type) @@ -435,9 +469,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast (Some mty_ast_o) None in - Modintern.dump_moddef loc mp "mod"; - if_verbose message ("Module "^ string_of_id id ^" is declared"); - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Dumpglob.dump_moddef loc mp "mod"; + if_verbose message ("Module "^ string_of_id id ^" is declared"); + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) @@ -455,7 +489,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = let mp = Declaremods.start_module Modintern.interp_modtype export id binders_ast mty_ast_o in - Modintern.dump_moddef loc mp "mod"; + Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Interactive Module "^ string_of_id id ^" started") ; List.iter @@ -475,7 +509,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast mty_ast_o mexpr_ast_o in - Modintern.dump_moddef loc mp "mod"; + Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is defined"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) @@ -483,9 +517,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = let vernac_end_module export (loc,id) = let mp = Declaremods.end_module id in - Modintern.dump_modref loc mp "mod"; - if_verbose message ("Module "^ string_of_id id ^" is defined") ; - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Dumpglob.dump_modref loc mp "mod"; + if_verbose message ("Module "^ string_of_id id ^" is defined") ; + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = @@ -501,7 +535,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast ([],[]) in let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in - Modintern.dump_moddef loc mp "modtype"; + Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter @@ -511,25 +545,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = ) argsexport | Some base_mty -> - let binders_ast = List.map - (fun (export,idl,ty) -> - if export <> None then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" " ^ - "and \"Import\" keywords from every functor argument.") - else (idl,ty)) binders_ast in - let mp = Declaremods.declare_modtype Modintern.interp_modtype + let binders_ast = List.map + (fun (export,idl,ty) -> + if export <> None then + error ("Arguments of a functor definition can be imported only if" ^ + " the definition is interactive. Remove the \"Export\" " ^ + "and \"Import\" keywords from every functor argument.") + else (idl,ty)) binders_ast in + let mp = Declaremods.declare_modtype Modintern.interp_modtype id binders_ast base_mty in - Modintern.dump_moddef loc mp "modtype"; - if_verbose message - ("Module Type "^ string_of_id id ^" is defined") + Dumpglob.dump_moddef loc mp "modtype"; + if_verbose message + ("Module Type "^ string_of_id id ^" is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype id in - Modintern.dump_modref loc mp "modtype"; - if_verbose message - ("Module Type "^ string_of_id id ^" is defined") + Dumpglob.dump_modref loc mp "modtype"; + if_verbose message + ("Module Type "^ string_of_id id ^" is defined") let vernac_include = function | CIMTE mty_ast -> @@ -541,39 +575,18 @@ let vernac_include = function (**********************) (* Gallina extensions *) - -let vernac_record struc binders sort nameopt cfs = - let const = match nameopt with - | None -> add_prefix "Build_" (snd (snd struc)) - | Some (_,id as lid) -> - if !dump then dump_definition lid false "constr"; id in - let sigma = Evd.empty in - let env = Global.env() in - let s = interp_constr sigma env sort in - let s = Reductionops.whd_betadeltaiota env sigma s in - let s = match kind_of_term s with - | Sort s -> s - | _ -> user_err_loc - (constr_loc sort,"definition_structure", str "Sort expected.") in - if !dump then ( - dump_definition (snd struc) false "rec"; - List.iter (fun (_, x) -> - match x with - | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj" - | _ -> ()) cfs); - ignore(Record.definition_structure (struc,binders,cfs,const,s)) (* Sections *) let vernac_begin_section (_, id as lid) = check_no_pending_proofs (); - if !Flags.dump then dump_definition lid true "sec"; + Dumpglob.dump_definition lid true "sec"; Lib.open_section id let vernac_end_section (loc, id) = - if !Flags.dump then - dump_reference loc - (string_of_dirpath (current_dirpath true)) "<>" "sec"; + + Dumpglob.dump_reference loc + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section id let vernac_end_segment lid = @@ -588,6 +601,10 @@ let vernac_end_segment lid = let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in + if Dumpglob.dump () then begin + let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in + List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl) + end; Library.require_library qidl import let vernac_canonical r = @@ -606,21 +623,17 @@ let vernac_identity_coercion stre id qids qidt = Class.try_add_new_identity_coercion id stre source target (* Type classes *) -let vernac_class id par ar sup props = - if !dump then ( - dump_definition id false "class"; - List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props); - Classes.new_class id par ar sup props let vernac_instance glob sup inst props pri = - if !dump then dump_constraint inst false "inst"; + Dumpglob.dump_constraint inst false "inst"; ignore(Classes.new_instance ~global:glob sup inst props pri) let vernac_context l = + List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l; Classes.context l let vernac_declare_instance id = - if !dump then dump_definition id false "inst"; + Dumpglob.dump_definition id false "inst"; Classes.declare_instance false id (***********) @@ -752,15 +765,18 @@ let vernac_backto n = Lib.reset_label n let vernac_declare_tactic_definition = Tacinterp.add_tacdef +let vernac_create_hintdb local id b = + Auto.create_hint_db local id full_transparent_state b + let vernac_hints = Auto.add_hints let vernac_syntactic_definition lid = - dump_definition lid false "syndef"; + Dumpglob.dump_definition lid false "syndef"; Command.syntax_definition (snd lid) let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (global_with_alias r) false + Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false (List.map (fun (ex,b,f) -> ex, (b,f)) imps) | None -> Impargs.declare_implicits local (global_with_alias r) @@ -1059,7 +1075,7 @@ let vernac_print = function | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) | PrintGrammar ent -> Metasyntax.print_grammar ent - | PrintLoadPath -> (* For compatibility ? *) print_loadpath () + | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> msg (print_modules ()) | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid @@ -1085,7 +1101,6 @@ let vernac_print = function | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s | PrintHintDb -> Auto.print_searchtable () - | PrintSetoids -> Setoid_replace.print_setoids() | PrintScopes -> pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr)) | PrintScope s -> @@ -1113,24 +1128,38 @@ let interp_search_restriction = function open Search +let is_ident s = try ignore (check_ident s); true with UserError _ -> false + let interp_search_about_item = function - | SearchRef r -> GlobSearchRef (global_with_alias r) - | SearchString s -> GlobSearchString s + | SearchSubPattern pat -> + let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in + GlobSearchSubPattern pat + | SearchString (s,None) when is_ident s -> + GlobSearchString s + | SearchString (s,sc) -> + try + let ref = + Notation.interp_notation_as_global_reference dummy_loc + (fun _ -> true) s sc in + GlobSearchSubPattern (Pattern.PRef ref) + with UserError _ -> + error ("Unable to interp \""^s^"\" either as a reference or + as an identifier component") let vernac_search s r = let r = interp_search_restriction r in if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in Search.search_pattern pat r | SearchRewrite c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in Search.search_rewrite pat r | SearchHead ref -> Search.search_by_head (global_with_alias ref) r | SearchAbout sl -> - Search.search_about (List.map interp_search_about_item sl) r + Search.search_about (List.map (on_snd interp_search_about_item) sl) r let vernac_locate = function | LocateTerm qid -> msgnl (print_located_qualid qid) @@ -1309,7 +1338,6 @@ let interp c = match c with | VernacEndSegment lid -> vernac_end_segment lid - | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid @@ -1317,8 +1345,6 @@ let interp c = match c with | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t (* Type classes *) - | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props - | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri | VernacContext sup -> vernac_context sup | VernacDeclareInstance id -> vernac_declare_instance id @@ -1356,6 +1382,7 @@ let interp c = match c with (* Commands *) | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l + | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 663e2e3c..3e9dfb25 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: vernacexpr.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*) open Util open Names @@ -38,7 +38,7 @@ type printable = | PrintSectionContext of reference | PrintInspect of int | PrintGrammar of string - | PrintLoadPath + | PrintLoadPath of dir_path option | PrintModules | PrintModule of reference | PrintModuleType of reference @@ -60,7 +60,6 @@ type printable = | PrintHintDbName of string | PrintRewriteHintDbName of string | PrintHintDb - | PrintSetoids | PrintScopes | PrintScope of string | PrintVisibility of string option @@ -69,14 +68,14 @@ type printable = | PrintAssumptions of reference type search_about_item = - | SearchRef of reference - | SearchString of string + | SearchSubPattern of constr_pattern_expr + | SearchString of string * scope_name option type searchable = - | SearchPattern of pattern_expr - | SearchRewrite of pattern_expr + | SearchPattern of constr_pattern_expr + | SearchRewrite of constr_pattern_expr | SearchHead of reference - | SearchAbout of search_about_item list + | SearchAbout of (bool * search_about_item) list type locatable = | LocateTerm of reference @@ -112,11 +111,12 @@ type comment = | CommentInt of int type hints = - | HintsResolve of (int option * constr_expr) list + | HintsResolve of (int option * bool * constr_expr) list | HintsImmediate of constr_expr list | HintsUnfold of reference list + | HintsTransparency of reference list * bool | HintsConstructors of reference list - | HintsExtern of int * constr_expr * raw_tactic_expr + | HintsExtern of int * constr_expr option * raw_tactic_expr | HintsDestruct of identifier * int * (bool,unit) location * constr_expr * raw_tactic_expr @@ -140,19 +140,11 @@ type locality_flag = bool (* true = Local; false = Global *) type coercion_flag = bool (* true = AddCoercion; false = NoCoercion *) type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) -type inductive_flag = bool (* true = Inductive; false = CoInductive *) +type inductive_flag = Decl_kinds.recursivity_kind type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type sort_expr = Rawterm.rawsort -type decl_notation = (string * constr_expr * scope_name option) option -type simple_binder = lident list * constr_expr -type class_binder = lident * constr_expr list -type 'a with_coercion = coercion_flag * 'a -type constructor_expr = (lident * constr_expr) with_coercion -type inductive_expr = - lident * local_binder list * constr_expr * constructor_expr list - type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr @@ -162,6 +154,20 @@ type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option +type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *) +type decl_notation = (string * constr_expr * scope_name option) option +type simple_binder = lident list * constr_expr +type class_binder = lident * constr_expr list +type 'a with_coercion = coercion_flag * 'a +type 'a with_notation = 'a * decl_notation +type constructor_expr = (lident * constr_expr) with_coercion +type constructor_list_or_record_decl_expr = + | Constructors of constructor_expr list + | RecordDecl of lident option * local_decl_expr with_coercion with_notation list +type inductive_expr = + lident with_coercion * local_binder list * constr_expr option * inductive_kind * + constructor_list_or_record_decl_expr + type module_binder = bool option * lident list * module_type_ast type grammar_production = @@ -211,9 +217,6 @@ type vernac_expr = | VernacCombinedScheme of lident * lident list (* Gallina extensions *) - | VernacRecord of bool (* = Record or Structure *) - * lident with_coercion * local_binder list - * constr_expr * lident option * local_decl_expr with_coercion list | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of @@ -225,18 +228,18 @@ type vernac_expr = class_rawexpr * class_rawexpr (* Type classes *) - | VernacClass of - lident * (* name *) - local_binder list * (* params *) - sort_expr located option * (* arity *) - local_binder list * (* constraints *) - (lident * bool * constr_expr) list (* props, with substructure hints *) +(* | VernacClass of *) +(* lident * (\* name *\) *) +(* local_binder list * (\* params *\) *) +(* sort_expr located option * (\* arity *\) *) +(* local_binder list * (\* constraints *\) *) +(* (lident * bool * constr_expr) list (\* props, with substructure hints *\) *) | VernacInstance of bool * (* global *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - (lident * lident list * constr_expr) list * (* props *) + constr_expr * (* props *) int option (* Priority *) | VernacContext of local_binder list @@ -287,6 +290,7 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of rec_flag * (reference * bool * raw_tactic_expr) list + | VernacCreateHintDb of locality_flag * lstring * bool | VernacHints of locality_flag * lstring list * hints | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag @@ -332,3 +336,72 @@ type vernac_expr = | VernacExtend of string * raw_generic_argument list and located_vernac_expr = loc * vernac_expr + +(* Locating errors raised just after the dot is parsed but before the + interpretation phase *) + +exception DuringSyntaxChecking of exn + +let syntax_checking_error s = + raise (DuringSyntaxChecking (UserError ("",Pp.str s))) + +(* Managing locality *) + +let locality_flag = ref None + +let local_of_bool = function true -> Local | false -> Global + +let check_locality () = + if !locality_flag = Some true then + syntax_checking_error "This command does not support the \"Local\" prefix."; + if !locality_flag = Some false then + syntax_checking_error "This command does not support the \"Global\" prefix." + +let use_locality () = + let local = match !locality_flag with Some true -> true | _ -> false in + locality_flag := None; + local + +let use_locality_exp () = local_of_bool (use_locality ()) + +let use_section_locality () = + let local = + match !locality_flag with Some b -> b | None -> Lib.sections_are_opened () + in + locality_flag := None; + local + +let use_non_locality () = + let local = match !locality_flag with Some false -> false | _ -> true in + locality_flag := None; + local + +let enforce_locality () = + let local = + match !locality_flag with + | Some false -> + error "Cannot be simultaneously Local and Global." + | _ -> + Flags.if_verbose + Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; + true in + locality_flag := None; + local + +let enforce_locality_exp () = local_of_bool (enforce_locality ()) + +let enforce_locality_of local = + let local = + match !locality_flag with + | Some false when local -> + error "Cannot be simultaneously Local and Global." + | Some true when local -> + error "Use only prefix \"Local\"." + | None -> + if local then + Flags.if_verbose + Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; + local + | Some b -> b in + locality_flag := None; + local |