diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /toplevel | |
parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'toplevel')
42 files changed, 1388 insertions, 2205 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 21098a57..ab9c4c63 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml,v 1.12.2.2 2004/07/16 20:48:17 herbelin Exp $ *) +(* $Id: cerrors.ml 8003 2006-02-07 22:11:50Z herbelin $ *) open Pp open Util -open Ast open Indtypes open Type_errors open Pretype_errors +open Indrec open Lexer let print_loc loc = @@ -47,8 +47,6 @@ let rec explain_exn_default = function hov 0 (str "Out of memory") | Stack_overflow -> hov 0 (str "Stack overflow") - | Ast.No_match s -> - hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ()) | Anomaly (s,pps) -> hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ()) | Match_failure(filename,pos1,pos2) -> @@ -76,9 +74,13 @@ let rec explain_exn_default = function hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) | InductiveError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) + | RecursionSchemeError e -> + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,e) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) + | Tacred.ReductionTacticError e -> + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> @@ -90,8 +92,7 @@ let rec explain_exn_default = function hov 0 (str "Error:" ++ spc () ++ str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q) | Refiner.FailError (i,s) -> - let s = if s="" then "" else " \""^s^"\"" in - hov 0 (str "Error: Tactic failure" ++ str s ++ + hov 0 (str "Error: Tactic failure" ++ s ++ if i=0 then mt () else str " (level " ++ int i ++ str").") | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 09d79cec..1236ecf5 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cerrors.mli,v 1.2.6.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: cerrors.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/class.ml b/toplevel/class.ml index f5493929..5f385934 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml,v 1.44.2.3 2004/11/26 18:06:54 herbelin Exp $ *) +(* $Id: class.ml 7941 2006-01-28 23:07:59Z herbelin $ *) open Util open Pp @@ -92,42 +92,16 @@ let explain_coercion_error g = function (* Verifications pour l'ajout d'une classe *) -let rec arity_sort (ctx,a) = match kind_of_term a with - | Sort (Prop _ | Type _) -> List.length ctx - | _ -> raise Not_found - let check_reference_arity ref = - let t = Global.type_of_global ref in - try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t) - with Not_found -> raise (CoercionError (NotAClass ref)) + if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then + raise (CoercionError (NotAClass ref)) let check_arity = function - | CL_FUN | CL_SORT -> 0 + | CL_FUN | CL_SORT -> () | CL_CONST sp -> check_reference_arity (ConstRef sp) | CL_SECVAR sp -> check_reference_arity (VarRef sp) | CL_IND sp -> check_reference_arity (IndRef sp) -(* try_add_class : cl_typ -> strength option -> bool -> unit *) - -let strength_of_cl = function - | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) - | CL_SECVAR sp -> variable_strength sp - | _ -> Global - -let try_add_class cl streopt fail_if_exists = - if not (class_exists cl) then - let p = check_arity cl in - let stre' = strength_of_cl cl in - let stre = match streopt with - | Some stre -> strength_min (stre,stre') - | None -> stre' - in - declare_class (cl,stre,p) - else - if fail_if_exists then errorlabstrm "try_add_new_class" - (pr_class cl ++ str " is already a class") - - (* Coercions *) (* check that the computed target is the provided one *) @@ -148,18 +122,18 @@ let uniform_cond nargs lt = let id_of_cl = function | CL_FUN -> id_of_string "FUNCLASS" | CL_SORT -> id_of_string "SORTCLASS" - | CL_CONST kn -> id_of_label (label kn) + | CL_CONST kn -> id_of_label (con_label kn) | CL_IND ind -> let (_,mip) = Global.lookup_inductive ind in mip.mind_typename | CL_SECVAR id -> id -let class_of_ref = function +let class_of_global = function | ConstRef sp -> CL_CONST sp | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id | ConstructRef _ as c -> - errorlabstrm "class_of_ref" + errorlabstrm "class_of_global" (str "Constructors, such as " ++ Printer.pr_global c ++ str " cannot be used as class") @@ -204,14 +178,19 @@ let get_target t ind = let prods_of t = let rec aux acc d = match kind_of_term d with | Prod (_,c1,c2) -> aux (c1::acc) c2 - | Cast (c,_) -> aux acc c + | Cast (c,_,_) -> aux acc c | _ -> (d,acc) in aux [] t +let strength_of_cl = function + | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) + | CL_SECVAR sp -> variable_strength sp + | _ -> Global + let get_strength stre ref cls clt = - let stres = (snd (class_info cls)).cl_strength in - let stret = (snd (class_info clt)).cl_strength in + let stres = strength_of_cl cls in + let stret = strength_of_cl clt in let stref = strength_of_global ref in (* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? let streunif = stre_unif_cond (s_vardep,f_vardep) in @@ -265,10 +244,11 @@ let build_id_coercion idf_opt source = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - { const_entry_body = mkCast (val_f, typ_f); + { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; - const_entry_opaque = false } in - let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions()} in + let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn let check_source = function @@ -288,11 +268,9 @@ lorque source est None alors target est None aussi. let add_new_coercion_core coef stre source target isid = check_source source; - let env = Global.env () in - let v = constr_of_reference coef in - let vj = Retyping.get_judgment_of env Evd.empty v in + let t = Global.type_of_global coef in if coercion_exists coef then raise (CoercionError AlreadyExists); - let tg,lp = prods_of (vj.uj_type) in + let tg,lp = prods_of t in let llp = List.length lp in if llp = 0 then raise (CoercionError NotAFunction); let (cls,lvs,ind) = @@ -311,10 +289,10 @@ let add_new_coercion_core coef stre source target isid = raise (CoercionError NoTarget) in check_target clt target; - try_add_class cls None false; - try_add_class clt None false; + check_arity cls; + check_arity clt; let stre' = get_strength stre coef cls clt in - declare_coercion coef vj stre' isid cls clt (List.length lvs) + declare_coercion coef stre' isid cls clt (List.length lvs) let try_add_new_coercion_core ref b c d e = try add_new_coercion_core ref b c d e @@ -345,114 +323,5 @@ let add_coercion_hook stre ref = ^ " is now a coercion") let add_subclass_hook stre ref = - let cl = class_of_ref ref in + let cl = class_of_global ref in try_add_new_coercion_subclass cl stre - -(* try_add_new_class : global_reference -> strength -> unit *) - -let class_of_global = function - | VarRef sp -> CL_SECVAR sp - | ConstRef sp -> CL_CONST sp - | IndRef sp -> CL_IND sp - | ConstructRef _ as ref -> raise (CoercionError (NotAClass ref)) - -let try_add_new_class ref stre = - try try_add_class (class_of_global ref) (Some stre) true - with CoercionError e -> - errorlabstrm "try_add_new_class" (explain_coercion_error ref e) - -(* fonctions pour le discharge: encore un peu sale mais ça s'améliore *) - -type coercion_entry = - global_reference * strength * bool * cl_typ * cl_typ * int - -let add_new_coercion (ref,stre,isid,cls,clt,n) = - (* Un peu lourd, tout cela pour trouver l'instance *) - let env = Global.env () in - let v = constr_of_reference ref in - let vj = Retyping.get_judgment_of env Evd.empty v in - declare_coercion ref vj stre isid cls clt n - -let count_extra_abstractions hyps ids_to_discard = - let _,n = - List.fold_left - (fun (hyps,n as sofar) id -> - match hyps with - | (hyp,None,_)::rest when id = hyp ->(rest, n+1) - | _ -> sofar) - (hyps,0) ids_to_discard - in n - -let defined_in_sec kn olddir = - let _,dir,_ = repr_kn kn in - dir = olddir - -(* This moves the global path one step below *) -let process_global olddir = function - | VarRef _ -> - anomaly "process_global only processes global surviving the section" - | ConstRef kn as x -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - ConstRef newkn - else x - | IndRef (kn,i) as x -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - IndRef (newkn,i) - else x - | ConstructRef ((kn,i),j) as x -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - ConstructRef ((newkn,i),j) - else x - -let process_class olddir ids_to_discard x = - let (cl,{cl_strength=stre; cl_param=p}) = x in -(* let env = Global.env () in*) - match cl with - | CL_SECVAR _ -> x - | CL_CONST kn -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - let hyps = (Global.lookup_constant kn).const_hyps in - let n = count_extra_abstractions hyps ids_to_discard in - (CL_CONST newkn,{cl_strength=stre;cl_param=p+n}) - else - x - | CL_IND (kn,i) -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - let hyps = (Global.lookup_mind kn).mind_hyps in - let n = count_extra_abstractions hyps ids_to_discard in - (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n}) - else - x - | _ -> anomaly "process_class" - -let process_cl sec_sp cl = - match cl with - | CL_SECVAR id -> cl - | CL_CONST kn -> - if defined_in_sec kn sec_sp then - let newkn = Lib.make_kn (id_of_label (label kn)) in - CL_CONST newkn - else - cl - | CL_IND (kn,i) -> - if defined_in_sec kn sec_sp then - let newkn = Lib.make_kn (id_of_label (label kn)) in - CL_IND (newkn,i) - else - cl - | _ -> cl - -let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) = - let hyps = context_of_global_reference coe in - let nargs = count_extra_abstractions hyps ids_to_discard in - (process_global olddir coe, - coercion_strength coeinfo, - coercion_identity coeinfo, - process_cl olddir cls, - process_cl olddir clt, - nargs + coercion_params coeinfo) diff --git a/toplevel/class.mli b/toplevel/class.mli index b0350985..7717d754 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: class.mli,v 1.17.6.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: class.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) (*i*) open Names @@ -50,19 +50,4 @@ val add_coercion_hook : Tacexpr.declaration_hook val add_subclass_hook : Tacexpr.declaration_hook -(* [try_add_new_class ref] declares [ref] as a new class; usually, - this is done implicitely by [try_add_new_coercion]'s functions *) -val try_add_new_class : global_reference -> strength -> unit - -(*s This is used for the discharge *) -type coercion_entry - -val add_new_coercion : coercion_entry -> unit - -val process_class : - dir_path -> identifier list -> - (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) -val process_coercion : - dir_path -> identifier list -> coercion -> coercion_entry - -val class_of_ref : global_reference -> cl_typ +val class_of_global : global_reference -> cl_typ diff --git a/toplevel/command.ml b/toplevel/command.ml index 10d6a620..7ff1b1b5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml,v 1.116.2.4 2005/11/29 21:40:53 letouzey Exp $ *) +(* $Id: command.ml 8689 2006-04-07 20:20:16Z herbelin $ *) open Pp open Util @@ -18,7 +18,7 @@ open Entries open Inductive open Environ open Reduction -open Tacred +open Redexpr open Declare open Nametab open Names @@ -37,31 +37,45 @@ open Indtypes open Vernacexpr open Decl_kinds open Pretyping -open Symbols +open Notation let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) -let rec abstract_rawconstr c = function +let rec abstract_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl) + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) | LocalRawAssum (idl,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl - (abstract_rawconstr c bl) + (abstract_constr_expr c bl) -let rec generalize_rawconstr c = function +let rec generalize_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_rawconstr c bl) + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl) | LocalRawAssum (idl,t)::bl -> List.fold_right (fun x b -> mkProdC([x],t,b)) idl - (generalize_rawconstr c bl) + (generalize_constr_expr c bl) + +let rec length_of_raw_binders = function + | [] -> 0 + | LocalRawDef _::bl -> 1 + length_of_raw_binders bl + | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl + +let rec under_binders env f n c = + if n = 0 then f env Evd.empty c else + match kind_of_term c with + | Lambda (x,t,c) -> + mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c) + | LetIn (x,b,t,c) -> + mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c) + | _ -> assert false let rec destSubCast c = match kind_of_term c with | Lambda (x,t,c) -> let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u) | LetIn (x,b,t,c) -> let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u) - | Cast (b,u) -> (b,u) + | Cast (b,_, u) -> (b,u) | _ -> assert false let rec adjust_conclusion a cs = function @@ -84,63 +98,51 @@ let rec adjust_conclusion a cs = function let definition_message id = if_verbose message ((string_of_id id) ^ " is defined") -let constant_entry_of_com (bl,com,comtypopt,opacity) = +let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = let sigma = Evd.empty in let env = Global.env() in match comtypopt with None -> - let b = abstract_rawconstr com bl in - let j = judgment_of_rawconstr sigma env b in + let b = abstract_constr_expr com bl in + let j = interp_constr_judgment sigma env b in { const_entry_body = j.uj_val; - const_entry_type = Some (Evarutil.refresh_universes j.uj_type); - const_entry_opaque = opacity } + const_entry_type = Some (refresh_universes j.uj_type); + const_entry_opaque = opacity; + const_entry_boxed = boxed } | Some comtyp -> (* We use a cast to avoid troubles with evars in comtyp *) (* that can only be resolved knowing com *) - let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in + let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in let (body,typ) = destSubCast (interp_constr sigma env b) in { const_entry_body = body; const_entry_type = Some typ; - const_entry_opaque = opacity } - -let rec length_of_raw_binders = function - | [] -> 0 - | LocalRawDef _::bl -> 1 + length_of_raw_binders bl - | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl - -let rec under_binders env f n c = - if n = 0 then f env Evd.empty c else - match kind_of_term c with - | Lambda (x,t,c) -> - mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c) - | LetIn (x,b,t,c) -> - mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c) - | _ -> assert false + const_entry_opaque = opacity; + const_entry_boxed = boxed } let red_constant_entry bl ce = function | None -> ce | Some red -> let body = ce.const_entry_body in { ce with const_entry_body = - under_binders (Global.env()) (reduction_of_redexp red) - (length_of_raw_binders bl) - body } + under_binders (Global.env()) (fst (reduction_of_red_expr red)) + (length_of_raw_binders bl) + body } let declare_global_definition ident ce local = - let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in - if local = Local then + let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in + if local = Local && Options.is_verbose() then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; ConstRef kn -let declare_definition ident (local,_) bl red_option c typopt hook = - let ce = constant_entry_of_com (bl,c,typopt,false) in +let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = + let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in let ce' = red_constant_entry bl ce red_option in let r = match local with | Local when Lib.sections_are_opened () -> let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in - let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in + let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in definition_message ident; if Pfedit.refining () then msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ @@ -152,7 +154,6 @@ let declare_definition ident (local,_) bl red_option c typopt hook = let syntax_definition ident c local onlyparse = let c = snd (interp_aconstr [] [] c) in - let onlyparse = !Options.v7_only or onlyparse in Syntax_def.declare_syntactic_definition local ident onlyparse c (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) @@ -163,7 +164,7 @@ let assumption_message id = let declare_one_assumption is_coe (local,kind) c (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> - let r = + let _ = declare_variable ident (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in assumption_message ident; @@ -172,7 +173,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = str" is not visible from current goals"); VarRef ident | (Global|Local) -> - let (_,kn) = + let kn = declare_constant ident (ParameterEntry c, IsAssumption kind) in assumption_message ident; if local=Local & Options.is_verbose () then @@ -182,9 +183,13 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = if is_coe then Class.try_add_new_coercion r local let declare_assumption idl is_coe k bl c = - let c = generalize_rawconstr c bl in - let c = interp_type Evd.empty (Global.env()) c in - List.iter (declare_one_assumption is_coe k c) idl + if not (Pfedit.refining ()) then + let c = generalize_constr_expr c bl in + let c = interp_type Evd.empty (Global.env()) c in + List.iter (declare_one_assumption is_coe k c) idl + else + errorlabstrm "Command.Assumption" + (str "Cannot declare an assumption while in proof editing mode.") (* 3a| Elimination schemes for mutual inductive definitions *) @@ -203,16 +208,17 @@ let declare_one_elimination ind = (DefinitionEntry { const_entry_body = c; const_entry_type = t; - const_entry_opaque = false }, - Decl_kinds.IsDefinition) in + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() }, + Decl_kinds.IsDefinition Definition) in definition_message id; kn in let env = Global.env () in let sigma = Evd.empty in let elim_scheme = Indrec.build_indrec env sigma ind in - let npars = mip.mind_nparams in - let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in + let npars = mib.mind_nparams_rec in + let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in let kelim = mip.mind_kelim in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the @@ -220,10 +226,10 @@ let declare_one_elimination ind = if List.mem InType kelim then let elim = make_elim (new_sort_in_family InType) in let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in - let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in + let c = mkConst cte and t = constant_type (Global.env()) cte in List.iter (fun (sort,suff) -> let (t',c') = - Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort) + Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort) npars c t in let _ = declare (mindstr^suff) c' (Some t') in ()) non_type_eliminations @@ -270,27 +276,9 @@ let interp_mutual lparams lnamearconstrs finite = [] lnamearconstrs in if not (list_distinct allnames) then error "Two inductive objects have the same name"; - let nparams = local_binders_length lparams - and sigma = Evd.empty - and env0 = Global.env() in - let env_params, params = - List.fold_left - (fun (env, params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> - let t = interp_binder sigma env na t in - let d = (na,None,t) in - (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> - let t = interp_type sigma env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in - let ctx = List.rev ctx in - (push_rel_context ctx env, ctx@params) - | LocalRawDef ((_,na),c) -> - let c = judgment_of_rawconstr sigma env c in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env,d::params)) - (env0,[]) lparams - in + let sigma = Evd.empty and env0 = Global.env() in + let env_params, params = interp_context sigma env0 lparams in + (* Builds the params of the inductive entry *) let params' = List.map (fun (na,b,t) -> @@ -304,8 +292,6 @@ let interp_mutual lparams lnamearconstrs finite = let paramassums = List.fold_right (fun d l -> match d with (id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in - let indnames = - List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in let nparamassums = List.length paramassums in let (ind_env,ind_impls,arityl) = List.fold_left @@ -316,7 +302,7 @@ let interp_mutual lparams lnamearconstrs finite = let argsc = compute_arguments_scope fullarity in let ind_impls' = if Impargs.is_implicit_args() then - let impl = Impargs.compute_implicits false env_params fullarity in + let impl = Impargs.compute_implicits env_params fullarity in let paramimpl,_ = list_chop nparamassums impl in let l = List.fold_right (fun imp l -> if Impargs.is_status_implicit imp then @@ -337,8 +323,9 @@ let interp_mutual lparams lnamearconstrs finite = let fs = States.freeze() in (* Declare the notations for the inductive types pushed in local context*) try - List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df ind_impls c None) notations; + List.iter (fun (df,c,scope) -> + silently (Metasyntax.add_notation_interpretation df ind_impls c) scope) + notations; let ind_env_params = push_rel_context params ind_env in let mispecvec = @@ -358,21 +345,20 @@ let interp_mutual lparams lnamearconstrs finite = (* Interpret the constructor types *) let constrs = List.map - (interp_type_with_implicits sigma ind_env_params - (paramassums,ind_impls)) + (interp_type sigma ind_env_params ~impls:(paramassums,ind_impls)) bodies in (* Build the inductive entry *) - { mind_entry_params = params'; - mind_entry_typename = name; + { mind_entry_typename = name; mind_entry_arity = ar; mind_entry_consnames = constrnames; mind_entry_lc = constrs }) (List.rev arityl) lnamearconstrs in States.unfreeze fs; - notations, { mind_entry_record = false; + notations, { mind_entry_params = params'; + mind_entry_record = false; mind_entry_finite = finite; mind_entry_inds = mispecvec } with e -> States.unfreeze fs; raise e @@ -388,6 +374,7 @@ let declare_mutual_with_eliminations isrecord mie = (* Very syntactical equality *) let eq_la d1 d2 = match d1,d2 with | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') -> + (List.length nal = List.length nal') && List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal' & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false) | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') -> @@ -422,7 +409,7 @@ let extract_coe_la_lc = function let build_mutual lind finite = let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in let notations,mie = interp_mutual lparams lnamearconstructs finite in - let kn = declare_mutual_with_eliminations false mie in + let _ = declare_mutual_with_eliminations false mie in (* Declare the notations now bound to the inductive types *) List.iter (fun (df,c,scope) -> Metasyntax.add_notation_interpretation df [] c scope) notations; @@ -465,7 +452,8 @@ let collect_non_rec env = in searchrec [] -let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = +let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) + boxed = let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef and sigma = Evd.empty and env0 = Global.env() @@ -474,11 +462,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = let (rec_sign,rec_impls,arityl) = List.fold_left (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> - let arityc = generalize_rawconstr arityc bl in + let arityc = generalize_constr_expr arityc bl in let arity = interp_type sigma env0 arityc in let impl = if Impargs.is_implicit_args() - then Impargs.compute_implicits false env0 arity + then Impargs.compute_implicits env0 arity else [] in let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls', arity::arl)) @@ -494,13 +482,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = let fs = States.freeze() in let def = try - List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df rec_impls c None) notations; + List.iter (fun (df,c,scope) -> + silently + (Metasyntax.add_notation_interpretation df rec_impls c) scope) + notations; List.map2 (fun ((_,_,bl,_,def),_) arity -> - let def = abstract_rawconstr def bl in - interp_casted_constr_with_implicits - sigma rec_sign rec_impls def arity) + let def = abstract_constr_expr def bl in + interp_casted_constr sigma rec_sign ~impls:([],rec_impls) + def arity) lnameargsardef arityl with e -> States.unfreeze fs; raise e in @@ -514,11 +504,12 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = let ce = - { const_entry_body = mkFix ((nvrec,i),recdecls); + { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *) const_entry_type = Some arrec.(i); - const_entry_opaque = false } in - let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in - (ConstRef kn) + const_entry_opaque = false; + const_entry_boxed = boxed} in + let kn = declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) + in (ConstRef kn) in (* declare the recursive definitions *) let lrefrec = Array.mapi declare namerec in @@ -530,8 +521,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = (fun subst (f,def,t) -> let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; - const_entry_opaque = false } in - let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in + const_entry_opaque = false; + const_entry_boxed = boxed } in + let _ = + declare_constant f (DefinitionEntry ce,IsDefinition Definition) + in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -540,7 +534,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = List.iter (fun (df,c,scope) -> Metasyntax.add_notation_interpretation df [] c scope) notations -let build_corecursive lnameardef = +let build_corecursive lnameardef boxed = let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef and sigma = Evd.empty and env0 = Global.env() in @@ -549,11 +543,10 @@ let build_corecursive lnameardef = try List.fold_left (fun (env,arl) (recname,bl,arityc,_) -> - let arityc = generalize_rawconstr arityc bl in - let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in - let arity = arj.utj_val in + let arityc = generalize_constr_expr arityc bl in + let arity = interp_type Evd.empty env0 arityc in let _ = declare_variable recname - (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in + (Lib.cwd(),SectionLocalAssum arity,IsAssumption Definitional) in (Environ.push_named (recname,None,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> @@ -562,10 +555,10 @@ let build_corecursive lnameardef = let recdef = try List.map (fun (_,bl,arityc,def) -> - let arityc = generalize_rawconstr arityc bl in - let def = abstract_rawconstr def bl in + let arityc = generalize_constr_expr arityc bl in + let def = abstract_constr_expr def bl in let arity = interp_constr sigma rec_sign arityc in - interp_casted_constr sigma rec_sign def arity) + interp_casted_constr sigma rec_sign def arity) lnameardef with e -> States.unfreeze fs; raise e @@ -580,10 +573,11 @@ let build_corecursive lnameardef = let ce = { const_entry_body = mkCoFix (i, recdecls); const_entry_type = Some (arrec.(i)); - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_boxed = boxed } in - let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in - (ConstRef kn) + let kn = declare_constant fi (DefinitionEntry ce,IsDefinition CoFixpoint) + in (ConstRef kn) in let lrefrec = Array.mapi declare namerec in if_verbose ppnl (corecursive_message lrefrec); @@ -593,8 +587,10 @@ let build_corecursive lnameardef = (fun subst (f,def,t) -> let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; - const_entry_opaque = false } in - let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in + const_entry_opaque = false; + const_entry_boxed = boxed } in + let _ = + declare_constant f (DefinitionEntry ce,IsDefinition Definition) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -616,11 +612,12 @@ let build_scheme lnamedepindsort = let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in - let decltype = Evarutil.refresh_universes decltype in + let decltype = refresh_universes decltype in let ce = { const_entry_body = decl; const_entry_type = Some decltype; - const_entry_opaque = false } in - let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() } in + let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in ConstRef kn :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in @@ -643,29 +640,30 @@ let start_proof_com sopt kind (bl,t) hook = (Pfedit.get_all_proof_names ()) in let env = Global.env () in - let c = interp_type Evd.empty env (generalize_rawconstr t bl) in + let c = interp_type Evd.empty env (generalize_constr_expr t bl) in let _ = Typeops.infer_type env c in start_proof id kind c hook -let save id const kind hook = +let save id const (locality,kind) hook = let {const_entry_body = pft; const_entry_type = tpo; const_entry_opaque = opacity } = const in - let l,r = match kind with - | IsLocal when Lib.sections_are_opened () -> + let l,r = match locality with + | Local when Lib.sections_are_opened () -> + let k = logical_kind_of_goal_kind kind in let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in + let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) - | IsLocal -> - let k = IsDefinition in - let _,kn = declare_constant id (DefinitionEntry const, k) in + | Local -> + let k = logical_kind_of_goal_kind kind in + let kn = declare_constant id (DefinitionEntry const, k) in (Global, ConstRef kn) - | IsGlobal k -> - let k = theorem_kind_of_goal_kind k in - let _,kn = declare_constant id (DefinitionEntry const, k) in + | Global -> + let k = logical_kind_of_goal_kind kind in + let kn = declare_constant id (DefinitionEntry const, k) in (Global, ConstRef kn) in - hook l r; Pfedit.delete_current_proof (); + hook l r; definition_message id let save_named opacity = @@ -691,7 +689,7 @@ let save_anonymous_with_strength kind opacity save_ident = 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 (IsGlobal (Proof kind)) hook + save save_ident const (Global, Proof kind) hook let admit () = let (id,k,typ,hook) = Pfedit.current_proof_statement () in @@ -699,9 +697,10 @@ let admit () = if k <> IsGlobal (Proof Conjecture) then error "Only statements declared as conjecture can be admitted"; *) - let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in - hook Global (ConstRef kn); + let kn = + declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in Pfedit.delete_current_proof (); + hook Global (ConstRef kn); assumption_message id let get_current_context () = diff --git a/toplevel/command.mli b/toplevel/command.mli index 7997288c..c93f69be 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,v 1.38.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: command.mli 7682 2005-12-21 15:06:11Z herbelin $ i*) (*i*) open Util @@ -22,6 +22,7 @@ open Vernacexpr open Rawterm open Topconstr open Decl_kinds +open Redexpr (*i*) (*s Declaration functions. The following functions take ASTs, @@ -30,7 +31,7 @@ open Decl_kinds defined object *) val declare_definition : identifier -> definition_kind -> - local_binder list -> Tacred.red_expr option -> constr_expr -> + local_binder list -> red_expr option -> constr_expr -> constr_expr option -> declaration_hook -> unit val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit @@ -43,13 +44,13 @@ val build_mutual : inductive_expr list -> bool -> unit val declare_mutual_with_eliminations : bool -> Entries.mutual_inductive_entry -> mutual_inductive -val build_recursive : (fixpoint_expr * decl_notation) list -> unit +val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit -val build_corecursive : cofixpoint_expr list -> unit +val build_corecursive : cofixpoint_expr list -> bool -> unit val build_scheme : (identifier located * bool * reference * rawsort) list -> unit -val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr +val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr val start_proof : identifier -> goal_kind -> constr -> declaration_hook -> unit @@ -83,3 +84,5 @@ val admit : unit -> unit and the current global env *) val get_current_context : unit -> Evd.evar_map * Environ.env + + diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 4ba8f6c2..44b2e231 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml,v 1.30.2.4 2006/01/11 23:18:06 barras Exp $ *) +(* $Id: coqinit.ml 7732 2005-12-26 13:51:24Z herbelin $ *) open Pp open System @@ -73,23 +73,19 @@ let init_load_path () = (* developper specific directories to open *) let dev = if Coq_config.local then [ "dev" ] else [] in let coqlib = - if !Options.boot then Coq_config.coqtop - (* variable COQLIB overrides the default library *) - else getenv_else "COQLIB" Coq_config.coqlib in - let coqlib = canonical_path_name coqlib in + (* variable COQLIB overrides the default library *) + getenv_else "COQLIB" + (if Coq_config.local || !Options.boot then Coq_config.coqtop + else Coq_config.coqlib) in (* first user-contrib *) let user_contrib = coqlib/"user-contrib" in if Sys.file_exists user_contrib then - Mltop.add_path user_contrib Nameops.default_root_prefix; + Mltop.add_rec_path user_contrib Nameops.default_root_prefix; (* then standard library *) - let vdirs = - if !Options.v7 then [ "theories7"; "contrib7" ] - else [ "theories"; "contrib" ] in - let dirs = - (if !Options.v7 then "states7" else "states") :: dev @ vdirs in + let vdirs = [ "theories"; "contrib" ] in + let dirs = "states" :: dev @ vdirs in List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in - let camlp4 = canonical_path_name camlp4 in add_ml_include camlp4; (* then current directory *) Mltop.add_path "." Nameops.default_root_prefix; diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index e029d8ac..d7856170 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqinit.mli,v 1.7.16.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: coqinit.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Initialization. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index af787460..c3f79e0a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml,v 1.72.2.5 2005/11/23 14:46:09 barras Exp $ *) +(* $Id: coqtop.ml 7740 2005-12-26 20:07:21Z herbelin $ *) open Pp open Util @@ -29,9 +29,8 @@ let get_version_date () = with _ -> Coq_config.date let print_header () = - Printf.printf "Welcome to Coq %s%s (%s)\n" + Printf.printf "Welcome to Coq %s (%s)\n" Coq_config.version - (if !Options.v7 then " (V7 syntax)" else "") (get_version_date ()); flush stdout @@ -50,8 +49,10 @@ let engage () = let set_batch_mode () = batch_mode := true -let toplevel_name = ref (make_dirpath [id_of_string "Top"]) -let set_toplevel_name dir = toplevel_name := dir +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 unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () @@ -91,12 +92,13 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter Library.read_library_from_file (List.rev !load_vernacular_obj) + List.iter (fun f -> Library.require_library_from_file None f None) + (List.rev !load_vernacular_obj) let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - List.iter (fun s -> Library.require_library_from_file None None s false) + List.iter (fun s -> Library.require_library_from_file None s (Some false)) (List.rev !require_list) let compile_list = ref ([] : (bool * string) list) @@ -128,7 +130,6 @@ let re_exec is_ide = let s = !re_exec_version in let is_native = (Mltop.get()) = Mltop.Native in let prog = Sys.argv.(0) in - let coq = Filename.basename prog in if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let s = if s = "" then if is_native then "opt" else "byte" else s in @@ -142,6 +143,17 @@ let re_exec is_ide = Unix.handle_unix_error (Unix.execvp newprog) Sys.argv end +(*s options for the virtual machine *) + +let boxed_val = ref false +let boxed_def = ref false +let use_vm = ref false + +let set_vm_opt () = + Vm.set_transp_values (not !boxed_val); + Options.set_boxed_definitions !boxed_def; + Vconv.set_use_vm !use_vm + (*s Parsing of the command line. We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) @@ -162,7 +174,7 @@ let parse_args is_ide = | [] -> () | "-impredicative-set" :: rem -> - set_engagement Environ.ImpredicativeSet; parse rem + set_engagement Declarations.ImpredicativeSet; parse rem | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () @@ -173,6 +185,7 @@ let parse_args is_ide = | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem | "-top" :: [] -> usage () + | "-notop" :: rem -> unset_toplevel_name (); parse rem | "-q" :: rem -> no_load_rc (); parse rem | "-opt" :: rem -> set_opt(); parse rem @@ -228,6 +241,7 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Options.print_emacs := true; parse rem | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0 @@ -253,12 +267,10 @@ let parse_args is_ide = | "-xml" :: rem -> Options.xml_export := true; parse rem (* Scanned in Options! *) - | "-v7" :: rem -> (* Options.v7 := true; *) parse rem - | "-v8" :: rem -> (* Options.v7 := false; *) parse rem + | "-v7" :: rem -> error "This version of Coq does not support v7 syntax" + | "-v8" :: rem -> parse rem - (* Translator options *) - | "-strict-implicit" :: rem -> - Options.translate_strict_impargs := false; parse rem + | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem | s :: rem -> if is_ide then begin @@ -294,9 +306,10 @@ let init is_ide = if_verbose print_header (); init_load_path (); inputstate (); + set_vm_opt (); engage (); - if not !batch_mode && Global.env_is_empty() then - Declaremods.start_library !toplevel_name; + if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then + option_iter Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index ef8b4b37..b5a1106c 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqtop.mli,v 1.5.4.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: coqtop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 281ff1b6..6c543079 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,325 +6,83 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml,v 1.81.2.2 2005/11/29 21:40:53 letouzey Exp $ *) +(* $Id: discharge.ml 7493 2005-11-02 22:12:16Z mohring $ *) -open Pp -open Util open Names -open Nameops +open Util open Sign open Term -open Declarations open Entries -open Inductive -open Instantiate -open Reduction +open Declarations open Cooking -open Typeops -open Libnames -open Libobject -open Lib -open Nametab -open Declare -open Impargs -open Classops -open Class -open Recordops -open Library -open Indtypes -open Nametab -open Decl_kinds -let recalc_sp dir sp = - let (_,spid) = repr_path sp in Libnames.make_path dir spid +(********************************) +(* Discharging mutual inductive *) -let recalc_kn dir kn = - let (mp,_,l) = Names.repr_kn kn in - Names.make_kn mp dir l +let detype_param = function + | (Name id,None,p) -> id, Entries.LocalAssum p + | (Name id,Some p,_) -> id, Entries.LocalDef p + | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable" -let rec find_var id = function - | [] -> false - | (x,b,_)::l -> if x = id then b=None else find_var id l +(* Replace -let build_abstract_list sec_sp hyps ids_to_discard = - let l1,l2 = - List.split - (List.fold_left - (fun vars id -> - if find_var id hyps then (mkVar id, Libnames.make_path sec_sp id)::vars - else vars) - [] ids_to_discard) in - Array.of_list l1, l2 + Var(y1)..Var(yq):C1..Cq |- Ij:Bj + Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti -(* Discharge of inductives is done here (while discharge of constants - is done by the kernel for efficiency). *) + by -let abstract_inductive sec_sp ids_to_abs hyps inds = - let abstract_one_assum id t inds = - let ntyp = List.length inds in - let new_refs = - list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in - let inds' = - List.map - (function (np,tname,arity,cnames,lc) -> - let arity' = mkNamedProd id t arity in - let lc' = - List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc - in - (np,tname,arity',cnames,lc')) - inds - in - inds' in - let abstract_one_def id c inds = - List.map - (function (np,tname,arity,cnames,lc) -> - let arity' = replace_vars [id, c] arity in - let lc' = List.map (replace_vars [id, c]) lc in - (np,tname,arity',cnames,lc')) - inds in - let abstract_once ((hyps,inds,vars) as sofar) id = - match hyps with - | (hyp,None,t as d)::rest when id = hyp -> - let inds' = abstract_one_assum hyp t inds in - (rest, inds', (mkVar id, Libnames.make_path sec_sp id)::vars) - | (hyp,Some b,t as d)::rest when id = hyp -> - let inds' = abstract_one_def hyp b inds in - (rest, inds', vars) - | _ -> sofar in - let (_,inds',vars) = - List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in - let inds'' = - List.map - (fun (nparams,a,arity,c,lc) -> - let nparams' = nparams + (List.length vars) in - let params, short_arity = decompose_prod_n_assum nparams' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in - let params' = - List.map - (function - | (Name id,None,p) -> id, Entries.LocalAssum p - | (Name id,Some p,_) -> id, Entries.LocalDef p - | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable") - params in - { mind_entry_params = params'; - mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' in - let l1,l2 = List.split vars in - (inds'', Array.of_list l1, l2) + |- Ij: (y1..yq:C1..Cq)Bj + I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] +*) -let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib = - assert (Array.length mib.mind_packets > 0); - let record = mib.mind_record in - let finite = mib.mind_finite in +let abstract_inductive hyps nparams inds = + let ntyp = List.length inds in + let nhyp = named_context_length hyps in + let args = instance_from_named_context (List.rev hyps) in + let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in + let inds' = + List.map + (function (tname,arity,cnames,lc) -> + let lc' = List.map (substl subs) lc in + let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in + let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in + (tname,arity',cnames,lc'')) + inds in + let nparams' = nparams + Array.length args in +(* To be sure to be the same as before, should probably be moved to process_inductive *) + let params' = let (_,arity,_,_) = List.hd inds' in + let (params,_) = decompose_prod_n_assum nparams' arity in + List.map detype_param params + in + let ind'' = + List.map + (fun (a,arity,c,lc) -> + let _, short_arity = decompose_prod_n_assum nparams' arity in + let shortlc = + List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in + { mind_entry_typename = a; + mind_entry_arity = short_arity; + mind_entry_consnames = c; + mind_entry_lc = shortlc }) + inds' + in (params',ind'') + + +let process_inductive sechyps modlist mib = + let nparams = mib.mind_nparams in let inds = array_map_to_list (fun mip -> - let nparams = mip.mind_nparams in - let arity = expmod_type modlist mip.mind_user_arity in - let lc = Array.map (expmod_type modlist) mip.mind_user_lc in - (nparams, - mip.mind_typename, + let arity = expmod_constr modlist mip.mind_user_arity in + let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + (mip.mind_typename, arity, Array.to_list mip.mind_consnames, Array.to_list lc)) - mib.mind_packets - in - let hyps = mib.mind_hyps in - let hyps' = - Sign.fold_named_context - (fun (x,b,t) sgn -> - Sign.add_named_decl - (x, option_app (expmod_constr modlist) b,expmod_constr modlist t) - sgn) - mib.mind_hyps ~init:empty_named_context in - let (inds',abs_vars,discharged_hyps ) = - abstract_inductive sec_sp ids_to_discard hyps' inds in - let lmodif_one_mind i = - let nbc = Array.length mib.mind_packets.(i).mind_consnames in - (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)), - list_tabulate - (function j -> - let j' = j + 1 in - (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),abs_vars))) - nbc) - in - let indmodifs,cstrmodifs = - List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in - ({ mind_entry_record = record; - mind_entry_finite = finite; - mind_entry_inds = inds' }, - indmodifs, - List.flatten cstrmodifs, - discharged_hyps) - -(* Discharge messages. *) - -let constant_message id = - Options.if_verbose ppnl (pr_id id ++ str " is discharged.") - -let inductive_message inds = - Options.if_verbose - ppnl - (hov 0 - (match inds with - | [] -> assert false - | [ind] -> - (pr_id ind.mind_entry_typename ++ str " is discharged.") - | l -> - (prlist_with_sep pr_coma - (fun ind -> pr_id ind.mind_entry_typename) l ++ - spc () ++ str "are discharged."))) - -(* Discharge operations for the various objects of the environment. *) - -type opacity = bool - -type discharge_operation = - | Variable of identifier * section_variable_entry * local_kind * - implicits_flags * Dischargedhypsmap.discharged_hyps - | Constant of identifier * recipe * global_kind * constant * - implicits_flags * Dischargedhypsmap.discharged_hyps - | Inductive of mutual_inductive_entry * implicits_flags * - Dischargedhypsmap.discharged_hyps - | Class of cl_typ * cl_info_typ - | Struc of inductive * (unit -> struc_typ) - | Objdef of constant - | Coercion of coercion_entry - | Require of library_reference - | Constraints of Univ.constraints - -(* Main function to traverse the library segment and compute the various - discharge operations. *) - -let process_object oldenv olddir full_olddir newdir -(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *) - (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) = - let tag = object_tag lobj in - match tag with - | "VARIABLE" -> - let ((id,c,t),cst) = get_variable_with_constraints (basename sp) in - (* VARIABLE means local (entry Variable/Hypothesis/Local and are *) - (* always discharged *) - (Constraints cst :: ops, id :: ids_to_discard, work_alist) - - | "CONSTANT" -> - (* CONSTANT means never discharge (though visibility may vary) *) - let kind = constant_kind sp in - let kn = Nametab.locate_constant (qualid_of_sp sp) in - let lab = label kn in - let cb = Environ.lookup_constant kn oldenv in - let imp = is_implicit_constant kn in - let newkn = recalc_kn newdir kn in - let abs_vars,discharged_hyps0 = - build_abstract_list full_olddir cb.const_hyps ids_to_discard in - (* let's add the new discharged hypothesis to those already discharged*) - let discharged_hyps = - discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in - let mods = [ (kn, DO_ABSTRACT(newkn,abs_vars)) ] - in - let r = { d_from = cb; - d_modlist = work_alist; - d_abstract = ids_to_discard } in - let op = Constant (id_of_label lab,r,kind,newkn,imp,discharged_hyps) in - (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) - - | "INDUCTIVE" -> - let kn = Nametab.locate_mind (qualid_of_sp sp) in - let mib = Environ.lookup_mind kn oldenv in - let newkn = recalc_kn newdir kn in - let imp = is_implicit_inductive_definition kn in -(* let imp = is_implicit_args (* CHANGE *) in*) - let (mie,indmods,cstrmods,discharged_hyps0) = - process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in - (* let's add the new discharged hypothesis to those already discharged*) - let discharged_hyps = - discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in - ((Inductive(mie,imp,discharged_hyps)) :: ops, ids_to_discard, - (constl,indmods@indl,cstrmods@cstrl)) - - | "CLASS" -> - let ((cl,clinfo) as x) = outClass lobj in - if clinfo.cl_strength = Local then - (ops,ids_to_discard,work_alist) - else - let (y1,y2) = process_class olddir ids_to_discard x in - ((Class (y1,y2))::ops, ids_to_discard, work_alist) - - | "COERCION" -> - let (_,coeinfo,_,_ as x) = outCoercion lobj in - if coercion_strength coeinfo = Local then - (ops,ids_to_discard,work_alist) - else - let y = process_coercion olddir ids_to_discard x in - ((Coercion y)::ops, ids_to_discard, work_alist) - - | "STRUCTURE" -> - let ((kn,i),info) = outStruc lobj in - let newkn = recalc_kn newdir kn in - let strobj () = - let mib = Environ.lookup_mind newkn (Global.env ()) in - { s_CONST = info.s_CONST; - s_PARAM = mib.mind_packets.(0).mind_nparams; - s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in - ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist) - - | "OBJDEF1" -> - let kn = outObjDef1 lobj in - let new_kn = recalc_kn newdir kn in - ((Objdef new_kn)::ops, ids_to_discard, work_alist) - - | "REQUIRE" -> - let c = out_require lobj in - ((Require c)::ops, ids_to_discard, work_alist) - - | _ -> (ops,ids_to_discard,work_alist) - -let process_item oldenv olddir full_olddir newdir acc = function - | (sp,Leaf lobj) -> - process_object oldenv olddir full_olddir newdir acc (sp,lobj) - | (_,_) -> acc - -let process_operation = function - | Variable (id,expmod_a,stre,imp,discharged_hyps) -> - (* Warning:parentheses needed to get a side-effect from with_implicits *) - with_implicits imp (redeclare_variable id discharged_hyps) - (Lib.cwd(),expmod_a,stre) - | Constant (id,r,stre,kn,imp,discharged_hyps) -> - with_implicits imp (redeclare_constant id discharged_hyps) (r,stre); - constant_message id - | Inductive (mie,imp,discharged_hyps) -> - let _ = with_implicits imp (redeclare_inductive discharged_hyps) mie in - inductive_message mie.mind_entry_inds - | Class (y1,y2) -> - Lib.add_anonymous_leaf (inClass (y1,y2)) - | Struc (newsp,strobj) -> - Lib.add_anonymous_leaf (inStruc (newsp,strobj ())) - | Objdef newsp -> - begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end - | Coercion y -> add_new_coercion y - | Require y -> reload_library y - | Constraints y -> Global.add_constraints y - -let catch_not_found f x = - try f x - with Not_found -> - error ("Something is missing; perhaps a reference to a"^ - " module required inside the section") - -let close_section _ s = - let oldenv = Global.env() in - let prefix,decls,fs = close_section false s in - let full_olddir, (_,olddir) = prefix in - let newdir = fst (split_dirpath olddir) in - let (ops,ids,_) = - List.fold_left - (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls - in - let ids = last_section_hyps olddir in - Summary.section_unfreeze_summaries fs; - catch_not_found (List.iter process_operation) (List.rev ops); - Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir) + mib.mind_packets in + let sechyps' = map_named_context (expmod_constr modlist) sechyps in + let (params',inds') = abstract_inductive sechyps' nparams inds in + { mind_entry_record = mib.mind_record; + mind_entry_finite = mib.mind_finite; + mind_entry_params = params'; + mind_entry_inds = inds' } diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index c80b93ce..dcf88f31 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -6,13 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: discharge.mli,v 1.6.16.1 2004/07/16 19:31:48 herbelin Exp $ i*) +(*i $Id: discharge.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) -open Names +open Sign +open Cooking +open Declarations +open Entries -(* This module implements the discharge mechanism. It provides a function to - close the last opened section. That function calls [Lib.close_section] and - then re-introduce all the discharged versions of the objects that were - defined in the section. *) - -val close_section : bool -> identifier -> unit +val process_inductive : + named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index b5185cd3..4ef5d5fd 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: fhimsg.ml,v 1.19.2.1 2004/07/16 19:31:48 herbelin Exp $ *) +(* $Id: fhimsg.ml 7837 2006-01-11 09:47:32Z herbelin $ *) open Pp open Util @@ -231,7 +231,7 @@ let explain_ill_formed_rec_body k ctx err names i vdefs = | RecCallInCasePred c -> (str "Not allowed recursive call in the type of cases in") | NotGuardedForm c -> - str "Sub-expression " ++ prterm_env ctx c ++ spc() ++ + str "Sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++ str "not in guarded form (should be a constructor, Cases or CoFix)" in let pvd = P.pr_term k ctx vdefs.(i) in @@ -278,14 +278,7 @@ let explain_ml_case k ctx mes c ct br brt = hov 0 (str "In ML case expression on " ++ pc ++ ws 1 ++ cut () ++ str "of type" ++ ws 1 ++ pct ++ ws 1 ++ cut () ++ str "which is an inductive predicate." ++ fnl () ++ expln) -(* -let explain_cant_find_case_type loc k ctx c = - let pe = P.pr_term k ctx c in - Ast.user_err_loc - (loc,"pretype", - hov 3 (str "Cannot infer type of whole Case expression on" ++ - ws 1 ++ pe)) -*) + let explain_type_error k ctx = function | UnboundRel n -> explain_unbound_rel k ctx n diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli index 10175e2a..1ab786d1 100644 --- a/toplevel/fhimsg.mli +++ b/toplevel/fhimsg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: fhimsg.mli,v 1.8.16.1 2004/07/16 19:31:48 herbelin Exp $ i*) +(*i $Id: fhimsg.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index beb80d03..3fe51b5a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml,v 1.86.2.4 2004/12/03 18:45:53 herbelin Exp $ *) +(* $Id: himsg.ml 8005 2006-02-07 22:50:35Z herbelin $ *) open Pp open Util @@ -21,18 +21,20 @@ open Sign open Environ open Pretype_errors open Type_errors +open Indrec open Reduction open Cases open Logic open Printer -open Ast open Rawterm +open Evd -let quote s = if !Options.v7 then s else h 0 (str "\"" ++ s ++ str "\"") +let quote s = h 0 (str "\"" ++ s ++ str "\"") -let prterm c = quote (prterm c) -let prterm_env e c = quote (prterm_env e c) -let prjudge_env e c = let v,t = prjudge_env e c in (quote v,quote t) +let pr_lconstr c = quote (pr_lconstr c) +let pr_lconstr_env e c = quote (pr_lconstr_env e c) +let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) +let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) let nth i = let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in @@ -56,20 +58,20 @@ let explain_unbound_var ctx v = let explain_not_type ctx j = let pe = pr_ne_context_of (str"In environment") ctx in - let pc,pt = prjudge_env ctx j in + let pc,pt = pr_ljudge_env ctx j in pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++ str"has type" ++ spc () ++ pt ++ spc () ++ str"which should be Set, Prop or Type." let explain_bad_assumption ctx j = let pe = pr_ne_context_of (str"In environment") ctx in - let pc,pt = prjudge_env ctx j in + let pc,pt = pr_ljudge_env ctx j in pe ++ str "cannot declare a variable or hypothesis over the term" ++ brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." let explain_reference_variables c = - let pc = prterm c in + let pc = pr_lconstr c in str "the constant" ++ spc () ++ pc ++ spc () ++ str "refers to variables which are not in the context" @@ -82,12 +84,11 @@ let rec pr_disjunction pr = function let explain_elim_arity ctx ind aritylst c pj okinds = let ctx = make_all_name_different ctx in let pi = pr_inductive ctx ind in - let pc = prterm_env ctx c in - let ppt = prterm_env ctx pj.uj_type in + let pc = pr_lconstr_env ctx c in let msg = match okinds with | Some(kp,ki,explanation) -> - let pki = prterm_env ctx ki in - let pkp = prterm_env ctx kp in + let pki = pr_lconstr_env ctx ki in + let pkp = pr_lconstr_env ctx kp in let explanation = match explanation with | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" @@ -106,29 +107,19 @@ let explain_elim_arity ctx ind aritylst c pj okinds = hov 0 ( str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++ str "in the inductive type " ++ spc() ++ quote pi ++ - (if !Options.v7 then - let pp = prterm_env ctx pj.uj_val in - let ppar = pr_disjunction (prterm_env ctx) aritylst in - let ppt = prterm_env ctx pj.uj_type in - fnl () ++ - str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++ - str "has arity" ++ brk(1,1) ++ ppt ++ fnl () ++ - str "It should be " ++ brk(1,1) ++ ppar - else - let sorts = List.map (fun x -> mkSort (new_sort_in_family x)) + (let sorts = List.map (fun x -> mkSort (new_sort_in_family x)) (list_uniquize (List.map (fun ar -> family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in - let ppar = pr_disjunction (prterm_env ctx) sorts in - let ppt = prterm_env ctx (snd (decompose_prod_assum pj.uj_type)) in + let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in + let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ spc () ++ str "while it should be " ++ ppar)) ++ fnl () ++ msg - - + let explain_case_not_inductive ctx cj = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx cj.uj_val in - let pct = prterm_env ctx cj.uj_type in + let pc = pr_lconstr_env ctx cj.uj_val in + let pct = pr_lconstr_env ctx cj.uj_type in match kind_of_term cj.uj_type with | Evar _ -> str "Cannot infer a type for this expression" @@ -139,26 +130,30 @@ let explain_case_not_inductive ctx cj = let explain_number_branches ctx cj expn = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx cj.uj_val in - let pct = prterm_env ctx cj.uj_type in + let pc = pr_lconstr_env ctx cj.uj_val in + let pct = pr_lconstr_env ctx cj.uj_type in str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches" +let ordinal n = + let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in + string_of_int n ^ s + let explain_ill_formed_branch ctx c i actty expty = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx c in - let pa = prterm_env ctx actty in - let pe = prterm_env ctx expty in + let pc = pr_lconstr_env ctx c in + let pa = pr_lconstr_env ctx actty in + let pe = pr_lconstr_env ctx expty in str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the branch " ++ int (i+1) ++ - str " has type" ++ brk(1,1) ++ pa ++ spc () ++ + spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++ + brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe let explain_generalization ctx (name,var) j = let pe = pr_ne_context_of (str "In environment") ctx in - let pv = prtype_env ctx var in - let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in + let pv = pr_ltype_env ctx var in + let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) ctx) j in str"Illegal generalization: " ++ pe ++ str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++ @@ -167,17 +162,18 @@ let explain_generalization ctx (name,var) j = let explain_actual_type ctx j pt = let pe = pr_ne_context_of (str "In environment") ctx in - let (pc,pct) = prjudge_env ctx j in - let pt = prterm_env ctx pt in + let (pc,pct) = pr_ljudge_env ctx j in + let pt = pr_lconstr_env ctx pt in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ str "while it is expected to have type" ++ brk(1,1) ++ pt let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = + let ctx = make_all_name_different ctx in let randl = Array.to_list randl in (* let pe = pr_ne_context_of (str"in environment") ctx in*) - let pr,prt = prjudge_env ctx rator in + let pr,prt = pr_ljudge_env ctx rator in let term_string1,term_string2 = if List.length randl > 1 then str "terms", (str"The "++nth n++str" term") @@ -185,7 +181,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = str "term", str "This term" in let appl = prlist_with_sep pr_fnl (fun c -> - let pc,pct = prjudge_env ctx c in + let pc,pct = pr_ljudge_env ctx c in hov 2 (pc ++ spc () ++ str": " ++ pct)) randl in str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ @@ -193,19 +189,20 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = str"of type" ++ brk(1,1) ++ prt ++ spc () ++ str"cannot be applied to the " ++ term_string1 ++ fnl () ++ str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++ - brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++ - str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp + brk(1,1) ++ pr_lconstr_env ctx actualtyp ++ spc () ++ + str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env ctx exptyp let explain_cant_apply_not_functional ctx rator randl = + let ctx = make_all_name_different ctx in let randl = Array.to_list randl in (* let pe = pr_ne_context_of (str"in environment") ctx in*) - let pr = prterm_env ctx rator.uj_val in - let prt = prterm_env ctx rator.uj_type in + let pr = pr_lconstr_env ctx rator.uj_val in + let prt = pr_lconstr_env ctx rator.uj_type in let term_string = if List.length randl > 1 then "terms" else "term" in let appl = prlist_with_sep pr_fnl (fun c -> - let pc = prterm_env ctx c.uj_val in - let pct = prterm_env ctx c.uj_type in + let pc = pr_lconstr_env ctx c.uj_val in + let pct = pr_lconstr_env ctx c.uj_type in hov 2 (pc ++ spc () ++ str": " ++ pct)) randl in str"Illegal application (Non-functional construction): " ++ @@ -216,14 +213,14 @@ let explain_cant_apply_not_functional ctx rator randl = str" " ++ v 0 appl let explain_unexpected_type ctx actual_type expected_type = - let pract = prterm_env ctx actual_type in - let prexp = prterm_env ctx expected_type in + let pract = pr_lconstr_env ctx actual_type in + let prexp = pr_lconstr_env ctx expected_type in str"This type is" ++ spc () ++ pract ++ spc () ++ str "but is expected to be" ++ spc () ++ prexp let explain_not_product ctx c = - let pr = prterm_env ctx c in + let pr = pr_lconstr_env ctx c in str"The type of this term is a product," ++ spc () ++ str"but it is casted with type" ++ brk(1,1) ++ pr @@ -241,8 +238,9 @@ let explain_ill_formed_rec_body ctx err names i = (* Fixpoint guard errors *) | NotEnoughAbstractionInFixBody -> str "Not enough abstractions in the definition" - | RecursionNotOnInductiveType -> - str "Recursive definition on a non inductive type" + | RecursionNotOnInductiveType c -> + str "Recursive definition on" ++ spc() ++ pr_lconstr_env ctx c ++ spc() ++ + str "which should be an inductive type" | RecursionOnIllegalTerm(j,arg,le,lt) -> let called = match names.(j) with @@ -262,7 +260,7 @@ let explain_ill_formed_rec_body ctx err names i = prlist_with_sep pr_spc (pr_db ctx) lt in str "Recursive call to " ++ called ++ spc() ++ str "has principal argument equal to" ++ spc() ++ - prterm_env ctx arg ++ fnl() ++ str "instead of " ++ vars + pr_lconstr_env ctx arg ++ fnl() ++ str "instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = @@ -273,31 +271,31 @@ let explain_ill_formed_rec_body ctx err names i = (* CoFixpoint guard errors *) | CodomainNotInductiveType c -> - str "the codomain is" ++ spc () ++ prterm_env ctx c ++ spc () ++ + str "the codomain is" ++ spc () ++ pr_lconstr_env ctx c ++ spc () ++ str "which should be a coinductive type" | NestedRecursiveOccurrences -> str "nested recursive occurrences" | UnguardedRecursiveCall c -> - str "unguarded recursive call in" ++ spc() ++ prterm_env ctx c + str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env ctx c | RecCallInTypeOfAbstraction c -> str "recursive call forbidden in the domain of an abstraction:" ++ - spc() ++ prterm_env ctx c + spc() ++ pr_lconstr_env ctx c | RecCallInNonRecArgOfConstructor c -> str "recursive call on a non-recursive argument of constructor" ++ - spc() ++ prterm_env ctx c + spc() ++ pr_lconstr_env ctx c | RecCallInTypeOfDef c -> str "recursive call forbidden in the type of a recursive definition" ++ - spc() ++ prterm_env ctx c + spc() ++ pr_lconstr_env ctx c | RecCallInCaseFun c -> - str "recursive call in a branch of" ++ spc() ++ prterm_env ctx c + str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env ctx c | RecCallInCaseArg c -> str "recursive call in the argument of cases in" ++ spc() ++ - prterm_env ctx c + pr_lconstr_env ctx c | RecCallInCasePred c -> str "recursive call in the type of cases in" ++ spc() ++ - prterm_env ctx c + pr_lconstr_env ctx c | NotGuardedForm c -> - str "sub-expression " ++ prterm_env ctx c ++ spc() ++ + str "sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++ str "not in guarded form" ++ spc()++ str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)" in @@ -307,8 +305,8 @@ let explain_ill_formed_rec_body ctx err names i = let explain_ill_typed_rec_body ctx i names vdefj vargs = let ctx = make_all_name_different ctx in - let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in - let pv = prterm_env ctx vargs.(i) in + let pvd,pvdt = pr_ljudge_env ctx (vdefj.(i)) in + let pv = pr_lconstr_env ctx vargs.(i) in str"The " ++ (if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++ str"recursive definition" ++ spc () ++ pvd ++ spc () ++ @@ -317,19 +315,19 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs = (* let explain_not_inductive ctx c = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx c in + let pc = pr_lconstr_env ctx c in str"The term" ++ brk(1,1) ++ pc ++ spc () ++ str "is not an inductive definition" *) let explain_cant_find_case_type ctx c = let ctx = make_all_name_different ctx in - let pe = prterm_env ctx c in + let pe = pr_lconstr_env ctx c in hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe) let explain_occur_check ctx ev rhs = let ctx = make_all_name_different ctx in let id = Evd.string_of_existential ev in - let pt = prterm_env ctx rhs in + let pt = pr_lconstr_env ctx rhs in str"Occur check failed: tried to define " ++ str id ++ str" with term" ++ brk(1,1) ++ pt @@ -342,14 +340,10 @@ let explain_hole_kind env = function | BinderType Anonymous -> str "a type for this anonymous binder" | ImplicitArg (c,(n,ido)) -> - if !Options.v7 then - str "the " ++ pr_ord n ++ - str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c - else - let id = out_some ido in - str "an instance for the implicit parameter " ++ - pr_id id ++ spc () ++ str "of" ++ - spc () ++ Nametab.pr_global_env Idset.empty c + let id = out_some ido in + str "an instance for the implicit parameter " ++ + pr_id id ++ spc () ++ str "of" ++ + spc () ++ Nametab.pr_global_env Idset.empty c | InternalHole -> str "a term for an internal placeholder" | TomatchTypeParameter (tyi,n) -> @@ -361,7 +355,7 @@ let explain_not_clean ctx ev t k = let ctx = make_all_name_different ctx in let c = mkRel (Intset.choose (free_rels t)) in let id = Evd.string_of_existential ev in - let var = prterm_env ctx c in + let var = pr_lconstr_env ctx c in str"Tried to define " ++ explain_hole_kind ctx k ++ str" (" ++ str id ++ str ")" ++ spc() ++ str"with a term using variable " ++ var ++ spc () ++ @@ -377,18 +371,36 @@ let explain_var_not_found ctx id = spc () ++ str "in the current" ++ spc () ++ str "environment" let explain_wrong_case_info ctx ind ci = - let ctx = make_all_name_different ctx in - let pi = prterm (mkInd ind) in + let pi = pr_lconstr (mkInd ind) in if ci.ci_ind = ind then str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++ spc () ++ str"has invalid information" else - let pc = prterm (mkInd ci.ci_ind) in + let pc = pr_lconstr (mkInd ci.ci_ind) in str"A term of inductive type" ++ spc () ++ pi ++ spc () ++ str"was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc +let explain_cannot_unify m n = + let pm = pr_lconstr m in + let pn = pr_lconstr n in + str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str"with" ++ brk(1,1) ++ pn + +let explain_refiner_cannot_generalize ty = + str "Cannot find a well-typed generalisation of the goal with type : " ++ + pr_lconstr ty + +let explain_no_occurrence_found c = + str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal" + +let explain_cannot_unify_binding_type m n = + let pm = pr_lconstr m in + let pn = pr_lconstr n in + str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ + str "which should be unifiable with" ++ brk(1,1) ++ pn + let explain_type_error ctx err = let ctx = make_all_name_different ctx in match err with @@ -445,93 +457,74 @@ let explain_pretype_error ctx err = explain_unexpected_type ctx actual expected | NotProduct c -> explain_not_product ctx c + | CannotUnify (m,n) -> explain_cannot_unify m n + | CannotGeneralize ty -> explain_refiner_cannot_generalize ty + | NoOccurrenceFound c -> explain_no_occurrence_found c + | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n (* Refiner errors *) let explain_refiner_bad_type arg ty conclty = str"refiner was given an argument" ++ brk(1,1) ++ - prterm arg ++ spc () ++ - str"of type" ++ brk(1,1) ++ prterm ty ++ spc () ++ - str"instead of" ++ brk(1,1) ++ prterm conclty + pr_lconstr arg ++ spc () ++ + str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ + str"instead of" ++ brk(1,1) ++ pr_lconstr conclty let explain_refiner_occur_meta t = - str"cannot refine with term" ++ brk(1,1) ++ prterm t ++ + str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++ spc () ++ str"because there are metavariables, and it is" ++ spc () ++ str"neither an application nor a Case" let explain_refiner_occur_meta_goal t = - str"generated subgoal" ++ brk(1,1) ++ prterm t ++ + str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++ spc () ++ str"has metavariables in it" -let explain_refiner_cannot_applt t harg = +let explain_refiner_cannot_apply t harg = str"in refiner, a term of type " ++ brk(1,1) ++ - prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ - prterm harg - -let explain_cannot_unify m n = - let pm = prterm m in - let pn = prterm n in - str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str"with" ++ brk(1,1) ++ pn - -let explain_cannot_unify_binding_type m n = - let pm = prterm m in - let pn = prterm n in - str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ - str "which should be unifiable with" ++ brk(1,1) ++ pn - -let explain_refiner_cannot_generalize ty = - str "Cannot find a well-typed generalisation of the goal with type : " ++ - prterm ty + pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ + pr_lconstr harg let explain_refiner_not_well_typed c = - str"The term " ++ prterm c ++ str" is not well-typed" + str"The term " ++ pr_lconstr c ++ str" is not well-typed" let explain_intro_needs_product () = str "Introduction tactics needs products" let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ prterm c ++ spc () ++ str "does not occur in" ++ + str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++ spc () ++ pr_id hyp let explain_non_linear_proof c = - str "cannot refine with term" ++ brk(1,1) ++ prterm c ++ + str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ spc () ++ str"because a metavariable has several occurrences" -let explain_no_occurrence_found c = - str "Found no subterm matching " ++ prterm c ++ str " in the current goal" - let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | OccurMeta t -> explain_refiner_occur_meta t | OccurMetaGoal t -> explain_refiner_occur_meta_goal t - | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg - | CannotUnify (m,n) -> explain_cannot_unify m n - | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n - | CannotGeneralize ty -> explain_refiner_cannot_generalize ty + | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg | NotWellTyped c -> explain_refiner_not_well_typed c | IntroNeedsProduct -> explain_intro_needs_product () | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp | NonLinearProof c -> explain_non_linear_proof c - | NoOccurrenceFound c -> explain_no_occurrence_found c (* Inductive errors *) let error_non_strictly_positive env c v = - let pc = prterm_env env c in - let pv = prterm_env env v in + let pc = pr_lconstr_env env c in + let pv = pr_lconstr_env env v in str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ brk(1,1) ++ pc let error_ill_formed_inductive env c v = - let pc = prterm_env env c in - let pv = prterm_env env v in + let pc = pr_lconstr_env env c in + let pv = pr_lconstr_env env v in str "Not enough arguments applied to the " ++ pv ++ str " in" ++ brk(1,1) ++ pc let error_ill_formed_constructor env c v = - let pc = prterm_env env c in - let pv = prterm_env env v in + let pc = pr_lconstr_env env c in + let pv = pr_lconstr_env env v in str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv @@ -544,9 +537,9 @@ let str_of_nth n = | _ -> "th") let error_bad_ind_parameters env c n v1 v2 = - let pc = prterm_env_at_top env c in - let pv1 = prterm_env env v1 in - let pv2 = prterm_env env v2 in + 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 "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++ str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc @@ -583,10 +576,11 @@ let error_bad_induction dep indid kind = str "is not allowed" let error_not_mutual_in_scheme () = - str "Induction schemes is concerned only with mutually inductive types" + str "Induction schemes are concerned only with distinct mutually inductive types" + +(* Inductive constructions errors *) let explain_inductive_error = function - (* These are errors related to inductive constructions *) | NonPos (env,c,v) -> error_non_strictly_positive env c v | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v @@ -596,7 +590,10 @@ let explain_inductive_error = function | SameNamesOverlap idl -> error_same_names_overlap idl | NotAnArity id -> error_not_an_arity id | BadEntry -> error_bad_entry () - (* These are errors related to recursors *) + +(* 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 @@ -606,7 +603,7 @@ let explain_inductive_error = function let explain_bad_pattern ctx cstr ty = let ctx = make_all_name_different ctx in - let pt = prterm_env ctx ty in + let pt = pr_lconstr_env ctx ty in let pc = pr_constructor ctx cstr in str "Found the constructor " ++ pc ++ brk(1,1) ++ str "while matching a term of type " ++ pt ++ brk(1,1) ++ @@ -620,31 +617,38 @@ let explain_bad_constructor ctx cstr ind = str "while a constructor of " ++ pi ++ brk(1,1) ++ str "is expected" -let explain_wrong_numarg_of_constructor ctx cstr n = - let pc = pr_constructor ctx cstr in - str "The constructor " ++ pc ++ str " expects " ++ - (if n = 0 then str "no argument." else if n = 1 then str "1 argument." - else (int n ++ str " arguments.")) +let decline_string n s = + if n = 0 then "no "^s + else if n = 1 then "1 "^s + else (string_of_int n^" "^s^"s") + +let explain_wrong_numarg_constructor ctx cstr n = + str "The constructor " ++ pr_constructor ctx cstr ++ + str " expects " ++ str (decline_string n "argument") + +let explain_wrong_numarg_inductive ctx ind n = + str "The inductive type " ++ pr_inductive ctx ind ++ + str " expects " ++ str (decline_string n "argument") let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity= let ctx = make_all_name_different ctx in - let pp = prterm_env ctx pred in + let pp = pr_lconstr_env ctx pred in str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++ str "should be of arity" ++ spc () ++ - prterm_env ctx nondep_arity ++ spc () ++ + pr_lconstr_env ctx nondep_arity ++ spc () ++ str "(for non dependent case) or" ++ - spc () ++ prterm_env ctx dep_arity ++ spc () ++ str "(for dependent case)." + spc () ++ pr_lconstr_env ctx dep_arity ++ spc () ++ str "(for dependent case)." let explain_needs_inversion ctx x t = let ctx = make_all_name_different ctx in - let px = prterm_env ctx x in - let pt = prterm_env ctx t in + let px = pr_lconstr_env ctx x in + let pt = pr_lconstr_env ctx t in str "Sorry, I need inversion to compile pattern matching of term " ++ px ++ str " of type: " ++ pt let explain_unused_clause env pats = - let s = if List.length pats > 1 then "s" else "" in (* Without localisation + let s = if List.length pats > 1 then "s" else "" in (str ("Unused clause with pattern"^s) ++ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")") *) @@ -659,7 +663,7 @@ let explain_cannot_infer_predicate ctx typs = let ctx = make_all_name_different ctx in let pr_branch (cstr,typ) = let cstr,_ = decompose_app cstr in - str "For " ++ prterm_env ctx cstr ++ str " : " ++ prterm_env ctx typ + str "For " ++ pr_lconstr_env ctx cstr ++ str " : " ++ pr_lconstr_env ctx typ in str "Unable to unify the types found in the branches:" ++ spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) @@ -670,7 +674,9 @@ let explain_pattern_matching_error env = function | BadConstructor (c,ind) -> explain_bad_constructor env c ind | WrongNumargConstructor (c,n) -> - explain_wrong_numarg_of_constructor env c n + explain_wrong_numarg_constructor env c n + | WrongNumargInductive (c,n) -> + explain_wrong_numarg_inductive env c n | WrongPredicateArity (pred,n,dep) -> explain_wrong_predicate_arity env pred n dep | NeedsInversion (x,t) -> @@ -681,3 +687,9 @@ let explain_pattern_matching_error env = function explain_non_exhaustive env tms | CannotInferPredicate typs -> explain_cannot_infer_predicate env typs + +let explain_reduction_tactic_error = function + | Tacred.InvalidAbstraction (env,c,(env',e)) -> + str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++ + spc() ++ str "is not well typed." ++ fnl () ++ + explain_type_error env' e diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 3e7ba575..92fcafb7 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: himsg.mli,v 1.13.14.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: himsg.mli 8003 2006-02-07 22:11:50Z herbelin $ i*) (*i*) open Pp @@ -15,6 +15,7 @@ open Indtypes open Environ open Type_errors open Pretype_errors +open Indrec open Cases open Logic (*i*) @@ -27,7 +28,12 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds val explain_inductive_error : inductive_error -> std_ppcmds +val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds + val explain_refiner_error : refiner_error -> std_ppcmds val explain_pattern_matching_error : env -> pattern_matching_error -> std_ppcmds + +val explain_reduction_tactic_error : + Tacred.reduction_tactic_error -> std_ppcmds diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml index 81221196..77f5198a 100644 --- a/toplevel/line_oriented_parser.ml +++ b/toplevel/line_oriented_parser.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: line_oriented_parser.ml,v 1.2.16.1 2004/07/16 19:31:49 herbelin Exp $ *) +(* $Id: line_oriented_parser.ml 5920 2004-07-16 20:01:26Z herbelin $ *) let line_oriented_channel_to_option stop_string input_channel = let count = ref 0 in diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli index 13af0e06..f37472c0 100644 --- a/toplevel/line_oriented_parser.mli +++ b/toplevel/line_oriented_parser.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: line_oriented_parser.mli,v 1.3.16.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: line_oriented_parser.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) val line_oriented_channel_to_option: string -> in_channel -> int -> char option diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 4c554209..92ce6e36 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,120 +6,27 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml,v 1.105.2.12 2006/01/04 20:31:16 herbelin Exp $ *) +(* $Id: metasyntax.ml 7822 2006-01-08 17:14:56Z herbelin $ *) open Pp open Util open Names open Topconstr -open Coqast -open Ast open Ppextend open Extend -open Esyntax open Libobject -open Library open Summary open Constrintern open Vernacexpr open Pcoq open Rawterm open Libnames - -let interp_global_rawconstr_with_vars vars c = - interp_rawconstr_gen false Evd.empty (Global.env()) false (vars,[]) c - -(**********************************************************************) -(* Parsing via ast (used in Zsyntax) *) - -(* This updates default parsers for Grammar actions and Syntax *) -(* patterns by inserting globalization *) -(* Done here to get parsing/g_*.ml4 non dependent from kernel *) -let constr_to_ast a = - Termast.ast_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a) - -(* This installs default quotations parsers to escape the ast parser *) -(* "constr" is used by default in quotations found in the ast parser *) -let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr - -let _ = define_ast_quotation true "constr" constr_parser_with_glob +open Lexer +open Egrammar +open Notation (**********************************************************************) -(* Globalisation for constr_expr *) - -let globalize_ref vars ref = - match Constrintern.interp_reference (vars,[]) ref with - | RRef (loc,VarRef a) -> Ident (loc,a) - | RRef (loc,a) -> Qualid (loc,qualid_of_sp (Nametab.sp_of_global a)) - | RVar (loc,x) -> Ident (loc,x) - | _ -> anomaly "globalize_ref: not a reference" - -let globalize_ref_term vars ref = - match Constrintern.interp_reference (vars,[]) ref with - | RRef (loc,VarRef a) -> CRef (Ident (loc,a)) - | RRef (loc,a) -> CRef (Qualid (loc,qualid_of_sp (Nametab.sp_of_global a))) - | RVar (loc,x) -> CRef (Ident (loc,x)) - | c -> Constrextern.extern_rawconstr Idset.empty c - -let rec globalize_constr_expr vars = function - | CRef ref -> globalize_ref_term vars ref - | CAppExpl (_,(p,ref),l) -> - let f = - map_constr_expr_with_binders globalize_constr_expr - (fun x e -> e) vars - in - CAppExpl (dummy_loc,(p,globalize_ref vars ref), List.map f l) - | c -> - map_constr_expr_with_binders globalize_constr_expr (fun id e -> id::e) - vars c - -let without_translation f x = - let old = Options.do_translate () in - let oldv7 = !Options.v7 in - Options.make_translate false; - try let r = f x in Options.make_translate old; Options.v7:=oldv7; r - with e -> Options.make_translate old; Options.v7:=oldv7; raise e - -let _ = set_constr_globalizer - (fun vars e -> for_grammar (without_translation (globalize_constr_expr vars)) e) - -(**********************************************************************) -(** For old ast printer *) - -(* Pretty-printer state summary *) -let _ = - declare_summary "syntax" - { freeze_function = Esyntax.freeze; - unfreeze_function = Esyntax.unfreeze; - init_function = Esyntax.init; - survive_module = false; - survive_section = false } - -(* Pretty-printing objects = syntax_entry *) -let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj - -let subst_syntax (_,subst,ppobj) = - Extend.subst_syntax_command Ast.subst_astpat subst ppobj - -let (inPPSyntax,outPPSyntax) = - declare_object {(default_object "PPSYNTAX") with - open_function = (fun i o -> if i=1 then cache_syntax o); - cache_function = cache_syntax; - subst_function = subst_syntax; - classify_function = (fun (_,o) -> Substitute o); - export_function = (fun x -> Some x) } - -(* Syntax extension functions (registered in the environnement) *) - -(* Checking the pretty-printing rules against free meta-variables. - * Note that object are checked before they are added in the environment. - * Syntax objects in compiled modules are not re-checked. *) - -let add_syntax_obj whatfor sel = -(* if not !Options.v7_only then*) - Lib.add_anonymous_leaf (inPPSyntax (interp_syntax_entry whatfor sel)) - -(* Tokens *) +(* Tokens *) let cache_token (_,s) = Pcoq.lexer.Token.using ("", s) @@ -134,69 +41,40 @@ let (inToken, outToken) = let add_token_obj s = Lib.add_anonymous_leaf (inToken s) (**********************************************************************) -(* Grammars (especially Tactic Notation) *) +(* Tactic Notation *) let make_terminal_status = function | VTerm s -> Some s | VNonTerm _ -> None -let qualified_nterm current_univ = function - | NtQual (univ, en) -> (univ, en) - | NtShort en -> (current_univ, en) - -let rec make_tags = function - | VTerm s :: l -> make_tags l +let rec make_tags lev = function + | VTerm s :: l -> make_tags lev l | VNonTerm (loc, nt, po) :: l -> - let (u,nt) = qualified_nterm "tactic" nt in - let (etyp, _) = Egrammar.interp_entry_name u nt in - etyp :: make_tags l + let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in + etyp :: make_tags lev l | [] -> [] -let declare_pprule = function - (* Pretty-printing rules only for Grammar (Tactic Notation) *) - | Egrammar.TacticGrammar (_,pp) -> - let f (s,t,p) = - Pptactic.declare_extra_tactic_pprule true s (t,p); - Pptactic.declare_extra_tactic_pprule false s (t,p) in - List.iter f pp - | _ -> () +let cache_tactic_notation (_,(pa,pp)) = + Egrammar.extend_grammar (Egrammar.TacticGrammar pa); + Pptactic.declare_extra_tactic_pprule pp -let cache_grammar (_,a) = - Egrammar.extend_grammar a; - declare_pprule a +let subst_tactic_parule subst (key,n,p,(d,tac)) = + (key,n,p,(d,Tacinterp.subst_tactic subst tac)) -let subst_grammar (_,subst,a) = - Egrammar.subst_all_grammar_command subst a +let subst_tactic_notation (_,subst,(pa,pp)) = + (subst_tactic_parule subst pa,pp) -let (inGrammar, outGrammar) = - declare_object {(default_object "GRAMMAR") with - open_function = (fun i o -> if i=1 then cache_grammar o); - cache_function = cache_grammar; - subst_function = subst_grammar; +let (inTacticGrammar, outTacticGrammar) = + declare_object {(default_object "TacticGrammar") with + open_function = (fun i o -> if i=1 then cache_tactic_notation o); + cache_function = cache_tactic_notation; + subst_function = subst_tactic_notation; classify_function = (fun (_,o) -> Substitute o); export_function = (fun x -> Some x)} -(**********************************************************************) -(* V7 Grammar *) - -open Genarg - -let check_entry_type (u,n) = - if u = "tactic" or u = "vernac" then error "tactic and vernac not supported"; - match entry_type (get_univ u) n with - | None -> Pcoq.create_entry_if_new (get_univ u) n ConstrArgType - | Some (ConstrArgType | IdentArgType | RefArgType) -> () - | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries" - -let add_grammar_obj univ entryl = - let u = create_univ_if_new univ in - let g = interp_grammar_command univ check_entry_type entryl in - Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g)) - -(**********************************************************************) -(* V8 Grammar *) - -(* Tactic notations *) +let cons_production_parameter l = function + | VTerm _ -> l + | VNonTerm (_,_,ido) -> option_cons ido l let rec tactic_notation_key = function | VTerm id :: _ -> id @@ -207,41 +85,49 @@ let rec next_key_away key t = if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t else key -let locate_tactic_body dir (s,(s',prods as x),e) = - let tags = make_tags prods in - let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in - (s,x,(dir,e)),(s,tags,(s',List.map make_terminal_status prods)) - -let add_tactic_grammar g = - let dir = Lib.cwd () in - let pa,pp = List.split (List.map (locate_tactic_body dir) g) in - Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (pa,pp))) - -(* Printing grammar entries *) +let add_tactic_notation (n,prods,e) = + let tags = make_tags n prods in + let key = next_key_away (tactic_notation_key prods) tags in + let pprule = (key,tags,(n,List.map make_terminal_status prods)) in + let ids = List.fold_left cons_production_parameter [] prods in + let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in + let parule = (key,n,prods,(Lib.cwd(),tac)) in + Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule)) -let print_grammar univ entry = - if !Options.v7 then - let u = get_univ univ in - let typ = explicitize_entry (fst u) entry in - let te,_,_ = get_constr_entry false typ in - Gram.Entry.print te - else - match entry with - | "constr" | "operconstr" | "binder_constr" -> - msgnl (str "Entry constr is"); - Gram.Entry.print Pcoq.Constr.constr; - msgnl (str "and lconstr is"); - Gram.Entry.print Pcoq.Constr.lconstr; - msgnl (str "where binder_constr is"); - Gram.Entry.print Pcoq.Constr.binder_constr; - msgnl (str "and operconstr is"); - Gram.Entry.print Pcoq.Constr.operconstr; - | "pattern" -> - Gram.Entry.print Pcoq.Constr.pattern - | "tactic" -> - Gram.Entry.print Pcoq.Tactic.simple_tactic - | _ -> error "Unknown or unprintable grammar entry" +(**********************************************************************) +(* Printing grammar entries *) + +let print_grammar univ = function + | "constr" | "operconstr" | "binder_constr" -> + msgnl (str "Entry constr is"); + Gram.Entry.print Pcoq.Constr.constr; + msgnl (str "and lconstr is"); + Gram.Entry.print Pcoq.Constr.lconstr; + msgnl (str "where binder_constr is"); + Gram.Entry.print Pcoq.Constr.binder_constr; + msgnl (str "and operconstr is"); + Gram.Entry.print Pcoq.Constr.operconstr; + | "pattern" -> + Gram.Entry.print Pcoq.Constr.pattern + | "tactic" -> + msgnl (str "Entry tactic_expr is"); + Gram.Entry.print Pcoq.Tactic.tactic_expr; + msgnl (str "Entry simple_tactic is"); + Gram.Entry.print Pcoq.Tactic.simple_tactic; + | "vernac" -> + msgnl (str "Entry vernac is"); + Gram.Entry.print Pcoq.Vernac_.vernac; + msgnl (str "Entry command is"); + Gram.Entry.print Pcoq.Vernac_.command; + msgnl (str "Entry syntax is"); + Gram.Entry.print Pcoq.Vernac_.syntax; + msgnl (str "Entry gallina is"); + Gram.Entry.print Pcoq.Vernac_.gallina; + msgnl (str "Entry gallina_ext is"); + Gram.Entry.print Pcoq.Vernac_.gallina_ext; + | _ -> error "Unknown or unprintable grammar entry" +(**********************************************************************) (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) @@ -342,12 +228,12 @@ let parse_format (loc,str) = Stdpp.raise_with_loc loc e (***********************) -(* Analysing notations *) - -open Symbols +(* Analyzing notations *) type symbol_token = WhiteSpace of int | String of string +(* Decompose the notation string into tokens *) + let split_notation_string str = let push_token beg i l = if beg = i then l else @@ -376,6 +262,43 @@ let split_notation_string str = in loop 0 0 +(* Interpret notations with a recursive component *) + +let rec find_pattern xl = function + | Break n as x :: l, Break n' :: l' when n=n' -> + find_pattern (x::xl) (l,l') + | Terminal s as x :: l, Terminal s' :: l' when s = s' -> + find_pattern (x::xl) (l,l') + | [NonTerminal x], NonTerminal x' :: l' -> + (x,x',xl),l' + | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> + error ("The token "^s^" occurs on one side of \"..\" but not on the other side") + | [NonTerminal _], Break s :: _ | Break s :: _, _ -> + error ("A break occurs on one side of \"..\" but not on the other side") + | ((SProdList _ | NonTerminal _) :: _ | []), _ -> + 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 + | 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'' + | (Terminal _ | Break _) as s :: tl -> + if hd = [] then + let yl,tl' = interp_list_parser [] tl in + yl, 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' + | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" + +(* Find non-terminal tokens of notation *) + let unquote_notation_token s = let n = String.length s in if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s @@ -410,38 +333,12 @@ let rec raw_analyse_notation_tokens = function let (vars,l) = raw_analyse_notation_tokens sl in (vars, Break n :: l) -let rec find_pattern xl = function - | Break n as x :: l, Break n' :: l' when n=n' -> - find_pattern (x::xl) (l,l') - | Terminal s as x :: l, Terminal s' :: l' when s = s' -> - find_pattern (x::xl) (l,l') - | [NonTerminal x], NonTerminal x' :: l' -> - (x,x',xl),l' - | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> - error ("The token "^s^" occurs on one side of \"..\" but not on the other side") - | [NonTerminal _], Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side") - | ((SProdList _ | NonTerminal _) :: _ | []), _ -> - 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 - | 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'' - | (Terminal _ | Break _) as s :: tl -> - if hd = [] then - let yl,tl' = interp_list_parser [] tl in - yl, 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' - | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" +let is_numeral symbs = + match List.filter (function Break _ -> false | _ -> true) symbs with + | ([Terminal "-"; Terminal x] | [Terminal x]) -> + (try let _ = Bigint.of_string x in true with _ -> false) + | _ -> + false let analyse_notation_tokens l = let vars,l = raw_analyse_notation_tokens l in @@ -450,7 +347,8 @@ let analyse_notation_tokens l = let remove_vars = List.fold_right List.remove_assoc -(* Build the syntax and grammar rules *) +(**********************************************************************) +(* Build pretty-printing rules *) type printing_precedence = int * parenRelation type parsing_precedence = int option @@ -460,15 +358,10 @@ let prec_assoc = function | Gramext.LeftA -> (E,L) | Gramext.NonA -> (L,L) -(* For old ast printer *) -let meta_pattern m = Pmeta(m,Tany) - -type white_status = Juxtapose | Separate of int | NextIsTerminal - let precedence_of_entry_type from = function | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n - | ETConstr (NumLevel n,BorderProd (left,Some a)) -> - n, let (lp,rp) = prec_assoc a in if left then lp else rp + | ETConstr (NumLevel n,BorderProd (b,Some a)) -> + n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp | ETConstr (NumLevel n,InternalProd) -> n, Prec n | ETConstr (NextLevel,_) -> from, L | ETOther ("constr","annot") -> 10, Prec 10 @@ -506,57 +399,15 @@ let is_operator s = s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~') -type previous_prod_status = NoBreak | CanBreak - let rec is_non_terminal = function | NonTerminal _ | SProdList _ -> true | _ -> false -let add_break n l = UNP_BRK (n,1) :: l - -(* For old ast printer *) -let make_hunks_ast symbols etyps from = - let rec make ws = function - | NonTerminal m :: prods -> - let _,lp = precedence_of_entry_type from (List.assoc m etyps) in - let u = PH (meta_pattern (string_of_id m), None, lp) in - if prods <> [] && is_non_terminal (List.hd prods) then - u :: add_break 1 (make CanBreak prods) - else - u :: make CanBreak prods - - | Terminal s :: prods when List.exists is_non_terminal prods -> - let protect = - is_letter s.[0] || - (is_non_terminal (List.hd prods) && - (is_letter (s.[String.length s -1])) || - (is_digit (s.[String.length s -1]))) in - if is_comma s || is_right_bracket s then - RO s :: add_break 0 (make NoBreak prods) - else if (is_operator s || is_left_bracket s) && ws = CanBreak then - add_break (if protect then 1 else 0) - (RO (if protect then s^" " else s) :: make CanBreak prods) - else - if protect then - (if ws = CanBreak then add_break 1 else (fun x -> x)) - (RO (s^" ") :: make CanBreak prods) - else - RO s :: make CanBreak prods - - | Terminal s :: prods -> - RO s :: make NoBreak prods - - | Break n :: prods -> - add_break n (make NoBreak prods) - - | SProdList _ :: _ -> - anomaly "Recursive notations not supported in old syntax" - - | [] -> [] +let add_break n l = UnpCut (PpBrk(n,0)) :: l - in make NoBreak symbols +(* Heuristics for building default printing rules *) -let add_break n l = UnpCut (PpBrk(n,0)) :: l +type previous_prod_status = NoBreak | CanBreak let make_hunks etyps symbols from = let vars,typs = List.split etyps in @@ -621,6 +472,8 @@ let make_hunks etyps symbols from = in make NoBreak symbols +(* Build default printing rules from explicit format *) + let error_format () = error "The format does not match the notation" let rec split_format_at_ldots hd = function @@ -656,12 +509,12 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let hunks_of_format (from,(vars,typs) as vt) symfmt = +let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when s' = String.make (String.length s') ' ' -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt + | Terminal s :: symbs, (UnpTerminal s') :: fmt when s = unquote_notation_token s' -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' -> @@ -689,36 +542,31 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt = | [], l -> l | _ -> error_format () -let string_of_prec (n,p) = - (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "") +(**********************************************************************) +(* Build parsing rules *) let assoc_of_type n (_,typ) = precedence_of_entry_type n typ -let string_of_assoc = function - | Some(Gramext.RightA) -> "RIGHTA" - | Some(Gramext.LeftA) | None -> "LEFTA" - | Some(Gramext.NonA) -> "NONA" - let is_not_small_constr = function ETConstr _ -> true | ETOther("constr","binder_constr") -> true | _ -> false -let rec define_keywords = function +let rec define_keywords_aux = function NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l - when not !Options.v7 && is_not_small_constr e -> + when is_not_small_constr e -> prerr_endline ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); - n1 :: Term("",k) :: define_keywords l - | n :: l -> n :: define_keywords l + n1 :: Term("",k) :: define_keywords_aux l + | n :: l -> n :: define_keywords_aux l | [] -> [] let define_keywords = function - Term("IDENT",k)::l when not !Options.v7 -> + Term("IDENT",k)::l -> prerr_endline ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); - Term("",k) :: define_keywords l - | l -> define_keywords l + Term("",k) :: define_keywords_aux l + | l -> define_keywords_aux l let make_production etyps symbols = let prod = @@ -728,12 +576,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in NonTerm (typ, Some (m,typ)) :: l | Terminal s -> - Term (Extend.terminal s) :: l + Term (terminal s) :: l | Break _ -> l | SProdList (x,sl) -> let sl = List.flatten - (List.map (function Terminal s -> [Extend.terminal s] + (List.map (function Terminal s -> [terminal s] | Break _ -> [] | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in let y = match List.assoc x etyps with @@ -766,44 +614,8 @@ let recompute_assoc typs = | _, Some Gramext.RightA -> Some Gramext.RightA | _ -> None -let make_grammar_rule n typs symbols ntn perm = - let assoc = recompute_assoc typs in - let prod = make_production typs symbols in - (n,assoc,ntn,prod, perm) - -(* For old ast printer *) -let metas_of sl = - List.fold_right - (fun it metatl -> match it with - | NonTerminal m -> m::metatl - | _ -> metatl) - sl [] - -(* For old ast printer *) -let make_pattern symbols ast = - let env = List.map (fun m -> (string_of_id m,ETast)) (metas_of symbols) in - fst (to_pat env ast) - -(* For old ast printer *) -let make_syntax_rule n name symbols typs ast ntn sc = - [{syn_id = name; - syn_prec = n; - syn_astpat = make_pattern symbols ast; - syn_hunks = - [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}] - -let make_pp_rule (n,typs,symbols,fmt) = - match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] - | Some fmt -> - [UnpBox (PpHOVB 0, - hunks_of_format (n,List.split typs) (symbols,parse_format fmt))] - (**************************************************************************) -(* Syntax extenstion: common parsing/printing rules and no interpretation *) - -(* v7 and translator : prec is for v7 (None if V8Notation), prec8 is for v8 *) -(* v8 : prec is for v8, prec8 is the same *) +(* Registration of syntax extensions (parsing/printing, no interpretation)*) let pr_arg_level from = function | (n,L) when n=from -> str "at next level" @@ -813,66 +625,38 @@ let pr_arg_level from = function | (n,_) -> str "Unknown level" let pr_level ntn (from,args) = - let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in -(* - let ppassoc, args = match args with - | [] -> mt (), [] - | (nl,lpr)::l when nl=from & fst (list_last l)=from -> - let (_,rpr),l = list_sep_last l in - match lpr, snd (list_last l) with - | L,E -> Gramext.RightA, l - | E,L -> Gramext.LeftA, l - | L,L -> Gramext.NoneA, l - | _ -> args -*) str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ prlist_with_sep pr_coma (pr_arg_level from) args -(* In v8: prec = Some prec8 is for both parsing and printing *) -(* In v7 and translator: - prec is for parsing (None if V8Notation), - prec8 for v8 printing (v7 printing is via ast) *) -let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) = +let error_incompatible_level ntn oldprec prec = + errorlabstrm "" + (str ("Notation "^ntn^" is already defined") ++ spc() ++ + pr_level ntn oldprec ++ + spc() ++ str "while it is now required to be" ++ spc() ++ + pr_level ntn prec) + +let cache_one_syntax_extension (prec,ntn,gr,pp) = try - let oldprec, oldprec8 = Symbols.level_of_notation ntn in - if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then - errorlabstrm "" - (str ((if Options.do_translate () then "For new syntax, notation " - else "Notation ") - ^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec8 ++ - spc() ++ str "while it is now required to be" ++ spc() ++ - pr_level ntn prec8) - else - (* Inconsistent v8 notations but not while translating; forget... *) - (); - (* V8 notations are consistent (from both translator or v8) *) - if prec <> None & !Options.v7 then begin - (* Update the V7 parsing rule *) - if oldprec <> None & out_some oldprec <> out_some prec then - (* None of them is V8Notation and they are different: warn *) - Options.if_verbose - warning ("Notation "^ntn^ - " was already assigned a different level or sublevels"); - if oldprec = None or out_some oldprec <> out_some prec then - Egrammar.extend_grammar (Egrammar.Notation (out_some prec,out_some gr)) - end + let oldprec = Notation.level_of_notation ntn in + if prec <> oldprec then error_incompatible_level ntn oldprec prec with Not_found -> (* Reserve the notation level *) - Symbols.declare_notation_level ntn (prec,prec8); + Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - option_iter (fun gr -> - Egrammar.extend_grammar (Egrammar.Notation (out_some prec,gr))) gr; + Egrammar.extend_grammar (Egrammar.Notation (prec,gr)); (* Declare the printing rule *) - Symbols.declare_notation_printing_rule ntn (se,fst prec8) + Notation.declare_notation_printing_rule ntn (pp,fst prec) + +let cache_syntax_extension (_,(_,sy_rules)) = + List.iter cache_one_syntax_extension sy_rules -let subst_notation_grammar subst x = x +let subst_parsing_rule subst x = x let subst_printing_rule subst x = x -let subst_syntax_extension (_,subst,(local,(prec,ntn,gr,se))) = - (local,(prec,ntn, - option_app (subst_notation_grammar subst) gr, - subst_printing_rule subst se)) +let subst_syntax_extension (_,subst,(local,sy)) = + (local, List.map (fun (prec,ntn,gr,pp) -> + (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy) let classify_syntax_definition (_,(local,_ as o)) = if local then Dispose else Substitute o @@ -888,6 +672,11 @@ let (inSyntaxExtension, outSyntaxExtension) = classify_function = classify_syntax_definition; export_function = export_syntax_definition} +(**************************************************************************) +(* Precedences *) + +(* Interpreting user-provided modifiers *) + let interp_modifiers modl = let onlyparsing = ref false in let rec interp assoc level etyps format = function @@ -896,23 +685,22 @@ let interp_modifiers modl = | SetEntryType (s,typ) :: l -> let id = id_of_string s in if List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level") - else interp assoc level ((id,typ)::etyps) format l + error (s^" is already assigned to an entry or constr level"); + interp assoc level ((id,typ)::etyps) format l | SetItemLevel ([],n) :: l -> interp assoc level etyps format l | SetItemLevel (s::idl,n) :: l -> let id = id_of_string s in if List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level") - else - let typ = ETConstr (n,()) in - interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l) + error (s^" is already assigned to an entry or constr level"); + let typ = ETConstr (n,()) in + interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l) | SetLevel n :: l -> - if level <> None then error "A level is given more than once" - else interp assoc (Some n) etyps format l + if level <> None then error "A level is given more than once"; + interp assoc (Some n) etyps format l | SetAssoc a :: l -> - if assoc <> None then error "An associativity is given more than once" - else interp (Some a) level etyps format l + if assoc <> None then error "An associativity is given more than once"; + interp (Some a) level etyps format l | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps format l @@ -921,21 +709,15 @@ let interp_modifiers modl = interp assoc level etyps (Some s) l in interp None None [] None modl -let merge_modifiers a n l = - (match a with None -> [] | Some a -> [SetAssoc a]) @ - (match n with None -> [] | Some n -> [SetLevel n]) @ l - -let interp_infix_modifiers modl = - let (assoc,level,t,b,fmt) = interp_modifiers modl in +let check_infix_modifiers modifiers = + let (assoc,level,t,b,fmt) = interp_modifiers modifiers in if t <> [] then - error "explicit entry level or type unexpected in infix notation"; - (assoc,level,b,fmt) + error "explicit entry level or type unexpected in infix notation" + +let no_syntax_modifiers modifiers = + modifiers = [] or modifiers = [SetOnlyParsing] -(* 2nd list of types has priority *) -let rec merge_entry_types etyps' = function - | [] -> etyps' - | (x,_ as e)::etyps -> - e :: merge_entry_types (List.remove_assoc x etyps') etyps +(* Compute precedences from modifiers (or find default ones) *) let set_entry_type etyps (x,typ) = let typ = try @@ -948,7 +730,7 @@ let set_entry_type etyps (x,typ) = with Not_found -> ETConstr typ in (x,typ) -let check_rule_reversibility l = +let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then error "A notation must include at least one symbol" @@ -956,17 +738,6 @@ let is_not_printable = function | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true | _ -> false -let find_precedence_v7 lev etyps symbols = - (match symbols with - | NonTerminal x :: _ -> - (try match List.assoc x etyps with - | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed" - | _ -> () - with Not_found -> ()) - | _ -> ()); - if lev = None then 1 else out_some lev - let find_precedence lev etyps symbols = match symbols with | NonTerminal x :: _ -> @@ -1000,7 +771,7 @@ let find_precedence lev etyps symbols = out_some lev let check_curly_brackets_notation_exists () = - try let _ = Symbols.level_of_notation "{ _ }" in () + try let _ = Notation.level_of_notation "{ _ }" in () with Not_found -> error "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved" @@ -1028,95 +799,59 @@ let remove_curly_brackets l = | x :: l -> x :: aux false l in aux true l -let compute_syntax_data forv7 (df,modifiers) = +let compute_syntax_data (df,modifiers) = let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in (* 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 ntn_for_interp = make_notation_key symbols in - let symbols = remove_curly_brackets symbols in - let notation = make_notation_key symbols in - check_rule_reversibility symbols; - let n = - if !Options.v7 then find_precedence_v7 n etyps symbols - else find_precedence n etyps symbols in - let innerlevel = NumLevel (if forv7 then 10 else 200) in + let symbols' = remove_curly_brackets symbols in + let need_squash = (symbols <> symbols') in + let ntn_for_grammar = make_notation_key symbols' in + check_rule_productivity symbols'; + let n = find_precedence n etyps symbols' in + let innerlevel = NumLevel 200 in let typs = find_symbols - (NumLevel n,BorderProd(true,assoc)) + (NumLevel n,BorderProd(Left,assoc)) (innerlevel,InternalProd) - (NumLevel n,BorderProd(false,assoc)) - symbols in + (NumLevel n,BorderProd(Right,assoc)) + symbols' in (* To globalize... *) let typs = List.map (set_entry_type etyps) typs in - let ppdata = (n,typs,symbols,fmt) in let prec = (n,List.map (assoc_of_type n) typs) in - ((onlyparse,recvars,vars, - ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df)) - -(* Uninterpreted (reserved) notations *) -let add_syntax_extension local mv mv8 = - (* from v7: - if mv8 <> None: tells the translator how to print in v8 - if mv <> None: tells how to parse and, how to print in v7 - mv = None = mv8 does not occur - from v8 (mv8 is always None and mv is always Some) - mv tells how to parse and print in v8 - *) - let data8 = option_app (compute_syntax_data false) mv8 in - let data = option_app (compute_syntax_data !Options.v7) mv in - let prec,gram_rule = match data with - | None -> None, None (* Case of V8Notation from v7 *) - | Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) -> - Some prec, Some (make_grammar_rule n typs symbols notation None) in - match data, data8 with - | None, None -> (* Nothing to do: V8Notation while not translating *) () - | _, Some d | Some d, None -> - let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in (* tells how to print *) - let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in - let pp_rule = make_pp_rule ppdata in - Lib.add_anonymous_leaf - (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule))) + 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 + (i_data,sy_data) (**********************************************************************) -(* Distfix, Infix, Symbols *) - -(* A notation comes with a grammar rule, a pretty-printing rule, an - identifiying pattern called notation and an associated scope *) -let load_notation _ (_,(_,_,ntn,scope,pat,onlyparse,_,_)) = - option_iter Symbols.declare_scope scope - -let open_notation i (_,(_,oldse,ntn,scope,pat,onlyparse,pp8only,df)) = - if i=1 then begin - let b,oldpp8only = Symbols.exists_notation_in_scope scope ntn pat in - (* Declare the old printer rule and its interpretation *) - if (not b or oldpp8only) & oldse <> None then - Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse}; +(* Registration of notations interpretation *) + +let load_notation _ (_,(_,scope,pat,onlyparse,_)) = + option_iter Notation.declare_scope scope + +let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = + if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) - if not b then - Symbols.declare_notation_interpretation ntn scope pat df pp8only; - if oldpp8only & not pp8only then - Options.silently - (Symbols.declare_notation_interpretation ntn scope pat df) pp8only; - if not b & not onlyparse then - Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat + Notation.declare_notation_interpretation ntn scope pat df; + (* Declare the uninterpretation *) + if not onlyparse then + Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat end let cache_notation o = load_notation 1 o; open_notation 1 o -let subst_notation (_,subst,(lc,oldse,ntn,scope,(metas,pat),b,b',df)) = - (lc,option_app - (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse, - ntn,scope, - (metas,subst_aconstr subst pat), b, b', df) +let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) = + (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf) -let classify_notation (_,(local,_,_,_,_,_,_,_ as o)) = +let classify_notation (_,(local,_,_,_,_ as o)) = if local then Dispose else Substitute o -let export_notation (local,_,_,_,_,_,_,_ as o) = +let export_notation (local,_,_,_,_ as o) = if local then None else Some o let (inNotation, outNotation) = @@ -1128,37 +863,8 @@ let (inNotation, outNotation) = classify_function = classify_notation; export_function = export_notation} -(* For old ast printer *) -let rec reify_meta_ast vars = function - | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast vars body) -(* | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)*) - | Node(loc,"ISEVAR",[]) -> Nmeta (loc,"$_") - | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast vars) args) - | Slam(loc,Some id,body) when List.mem id vars -> - Smetalam (loc,string_of_id id,reify_meta_ast vars body) - | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body) - | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id) - | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a - | Dynamic _ as a -> (* Hum... what to do here *) a - -(* For old ast syntax *) -let make_old_pp_rule n symbols typs r ntn scope vars = - let ast = Termast.ast_of_rawconstr r in - let ast = reify_meta_ast vars ast in - let scope_name = match scope with Some s -> s | None -> "core_scope" in - let rule_name = ntn^"_"^scope_name^"_notation" in - make_syntax_rule n rule_name symbols typs ast ntn scope - -(* maps positions in v8-notation into positions in v7-notation (used - for parsing). - For instance Notation "x < y < z" := .. V8only "y < z < x" - yields [1; 2; 0] (y is the second arg in v7; z is 3rd; x is fst) *) -let mk_permut vars7 vars8 = - if vars7=vars8 then None else - Some - (List.fold_right - (fun v8 subs -> list_index v8 vars7 - 1 :: subs) - vars8 []) +(**********************************************************************) +(* Recovering existing syntax *) let contract_notation ntn = if ntn = "{ _ }" then ntn else @@ -1173,304 +879,120 @@ let contract_notation ntn = else ntn in aux ntn 0 -let add_notation_in_scope local df c mods omodv8 scope = - let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')= - compute_syntax_data !Options.v7 (df,mods) in - (* Declare the parsing and printing rules if not already done *) - (* For both v7 and translate: parsing is as described for v7 in v7 file *) - (* For v8: parsing is as described in v8 file *) - (* For v7: printing is by the old printer - see below *) - (* For translate: printing is as described for v8 in v7 file *) - (* For v8: printing is as described in v8 file *) - (* In short: parsing does not depend on omodv8 *) - (* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *) - (* if in v7, or of mods without scaling if in v8 *) - let intnot,ntn,pprecvars,ppvars,ppprec,pp_rule = - match omodv8 with - | Some mv8 -> - let (_,recs8,vars8,intnot8,ntn8),p,d,_ = compute_syntax_data false mv8 in - intnot8,ntn8,recs8,vars8,p,make_pp_rule d - | None when not !Options.v7 -> - intnot,notation,recs,vars,prec,make_pp_rule ppdata - | None -> - (* means the rule already exists: recover it *) - (* occurs only with V8only flag alone *) - try - let ntn = contract_notation notation in - let _, oldprec8 = Symbols.level_of_notation ntn in - let rule,_ = Symbols.find_notation_printing_rule ntn in - notation,ntn,recs,vars,oldprec8,rule - with Not_found -> error "No known parsing rule for this notation in V8" - in - let permut = mk_permut vars ppvars in - let gram_rule = make_grammar_rule n typs symbols ntn permut in - Lib.add_anonymous_leaf - (inSyntaxExtension - (local,((Some prec,ppprec),ntn,Some gram_rule,pp_rule))); - - (* Declare interpretation *) - let (acvars,ac) = interp_aconstr [] ppvars c in - let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in - let old_pp_rule = - (* Used only by v7; disable if contains a recursive pattern *) - if onlyparse or pprecvars <> [] or not (!Options.v7) then None - else - let r = interp_global_rawconstr_with_vars vars c in - Some (make_old_pp_rule n symbols typs r intnot scope vars) in - let onlyparse = onlyparse or !Options.v7_only or is_not_printable ac in - Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df')) - -let level_rule (n,p) = if p = E then n else max (n-1) 0 +exception NoSyntaxRule -let recover_syntax ntn = +let recover_syntax ntn = try - match Symbols.level_of_notation ntn with - | (Some prec,_ as pprec) -> - let rule,_ = Symbols.find_notation_printing_rule ntn in - let gr = Egrammar.recover_notation_grammar ntn prec in - Some (pprec,ntn,Some gr,rule) - | None,_ -> None - with Not_found -> None + let prec = Notation.level_of_notation ntn in + let pprule,_ = Notation.find_notation_printing_rule ntn in + let gr = Egrammar.recover_notation_grammar ntn prec in + (prec,ntn,gr,pprule) + with Not_found -> + raise NoSyntaxRule + +let recover_squash_syntax () = recover_syntax "{ _ }" let recover_notation_syntax rawntn = let ntn = contract_notation rawntn in - match recover_syntax ntn with - | None -> None - | Some gr -> Some (gr,if ntn=rawntn then None else recover_syntax "{ _ }") - -let set_data_for_v7_pp recs a vars = - if not !Options.v7 then None else - if recs=[] then Some (a,vars) - else (warning "No recursive notation in v7 syntax";None) - -let build_old_pp_rule notation scope symbs (r,vars) = - let prec = - try - let a,_ = Symbols.level_of_notation (contract_notation notation) in - if a = None then raise Not_found else out_some a - with Not_found -> - error "Parsing rule for this notation has to be previously declared" in - let typs = List.map2 - (fun id n -> - id,ETConstr (NumLevel (level_rule n),InternalProd)) vars (snd prec) in - make_old_pp_rule (fst prec) symbs typs r notation scope vars - -let add_notation_interpretation_core local symbs for_old df a scope onlyparse - onlypp gram_data = - let notation = make_notation_key symbs in - let old_pp_rule = - if !Options.v7 then - option_app (build_old_pp_rule notation scope symbs) for_old - else None in - option_iter - (fun (x,y) -> - Lib.add_anonymous_leaf (inSyntaxExtension (local,x)); - option_iter - (fun z -> Lib.add_anonymous_leaf (inSyntaxExtension (local,z))) y) - gram_data; - Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp, - (Lib.library_dp(),df))) + let sy_rule = recover_syntax ntn in + let need_squash = ntn<>rawntn in + if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] -let add_notation_interpretation df names c sc = +(**********************************************************************) +(* Main entry point for building parsing and printing rules *) + +let make_pa_rule (n,typs,symbols,_) ntn = + let assoc = recompute_assoc typs in + let prod = make_production typs symbols in + (n,assoc,ntn,prod) + +let make_pp_rule (n,typs,symbols,fmt) = + match fmt with + | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] + | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt) + +let make_syntax_rules (ntn,prec,need_squash,sy_data) = + let pa_rule = make_pa_rule sy_data ntn in + let pp_rule = make_pp_rule sy_data in + let sy_rule = (prec,ntn,pa_rule,pp_rule) in + (* By construction, the rule for "{ _ }" is declared, but we need to + redeclare it because the file where it is declared needs not be open + when the current file opens (especially in presence of -nois) *) + if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] + +(**********************************************************************) +(* Main functions about notations *) + +let add_notation_in_scope local df c mods scope = + let (i_data,sy_data) = compute_syntax_data (df,mods) in + (* Declare the parsing and printing rules *) + 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 = onlyparse or is_not_printable ac in + 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 gram_data = recover_notation_syntax (make_notation_key symbs) in - if gram_data = None then - error "Parsing rule for this notation has to be previously declared"; + (* Redeclare pa/pp rules *) + if not (is_numeral symbs) then begin + let sy_rules = recover_notation_syntax (make_notation_key symbs) in + Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) + 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 a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in - let for_oldpp = set_data_for_v7_pp recs a_for_old vars in - let onlyparse = is_not_printable ac in - add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse - false gram_data - -let add_notation_in_scope_v8only local df c mv8 scope = - let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in - let pp_rule = make_pp_rule ppdata in - Lib.add_anonymous_leaf - (inSyntaxExtension(local,((None,prec),notation,None,pp_rule))); - (* Declare the interpretation *) - let (acvars,ac) = interp_aconstr [] vars c in - let a = (remove_vars recs acvars,ac) (* For recursive parts *) in - let onlyparse = is_not_printable ac in - Lib.add_anonymous_leaf - (inNotation(local,None,intnot,scope,a,onlyparse,true,df')) + let onlyparse = onlyparse or is_not_printable ac in + Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df')) -let add_notation_v8only local c (df,modifiers) sc = - let toks = split_notation_string df in - match toks with - | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> - (* This is a ident to be declared as a rule *) - add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc - | _ -> - let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in - match lev with - | None-> - if modifiers <> [] & modifiers <> [SetOnlyParsing] then - error "Parsing rule for this notation includes no level" - else - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let (acvars,ac) = interp_aconstr [] vars c in - let onlyparse = modifiers = [SetOnlyParsing] - or is_not_printable ac in - let a = (remove_vars recs acvars,ac) in - add_notation_interpretation_core local symbs None df a sc - onlyparse true None - | Some n -> - (* Declare both syntax and interpretation *) - let mods = - if List.for_all (function SetAssoc _ -> false | _ -> true) - modifiers - then SetAssoc Gramext.NonA :: modifiers else modifiers in - add_notation_in_scope_v8only local df c mods sc - -let is_quoted_ident x = - let x' = unquote_notation_token x in - x <> x' & try Lexer.check_ident x'; true with _ -> false - -(* v7: dfmod=None; mv8=Some: add only v8 printing rule *) -(* dfmod=Some: add v7 parsing rule; mv8=Some: add v8 printing rule *) -(* dfmod=Some; mv8=None: same v7-parsing and v8-printing rules *) -(* v8: dfmod=Some; mv8=None: same v8 parsing and printing rules *) -let add_notation local c dfmod mv8 sc = - match dfmod with - | None -> add_notation_v8only local c (out_some mv8) sc - | Some (df,modifiers) -> - let toks = split_notation_string df in - match toks with - | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> - (* This is a ident to be declared as a rule *) - add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc - | _ -> - let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in - match lev with - | None-> - if modifiers <> [] & modifiers <> [SetOnlyParsing] then - error "Parsing rule for this notation includes no level" - else - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let gram_data = - recover_notation_syntax (make_notation_key symbs) in - if gram_data <> None then - let (acvars,ac) = interp_aconstr [] vars c in - let a = (remove_vars recs acvars,ac) in - let onlyparse = modifiers = [SetOnlyParsing] - or is_not_printable ac in - let a_for_old = interp_global_rawconstr_with_vars vars c in - let for_old = set_data_for_v7_pp recs a_for_old vars in - add_notation_interpretation_core local symbs for_old df a - sc onlyparse false gram_data - else - add_notation_in_scope local df c modifiers mv8 sc - | Some n -> - (* Declare both syntax and interpretation *) - let assoc = match assoc with None -> Some Gramext.NonA | a -> a in - add_notation_in_scope local df c modifiers mv8 sc - -(* TODO add boxes information in the expression *) +(* Notations without interpretation (Reserved Notation) *) + +let add_syntax_extension local mv = + let (_,sy_data) = compute_syntax_data mv in + let sy_rules = make_syntax_rules sy_data in + Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) + +(* Notations with only interpretation *) + +let add_notation_interpretation df names c sc = + try add_notation_interpretation_core false df names c sc false + with NoSyntaxRule -> + error "Parsing rule for this notation has to be previously declared" + +(* Main entry point *) + +let add_notation local c (df,modifiers) sc = + if no_syntax_modifiers modifiers then + (* No syntax data: try to rely on a previously declared rule *) + let onlyparse = modifiers=[SetOnlyParsing] in + try add_notation_interpretation_core local df [] c sc onlyparse + with NoSyntaxRule -> + (* Try to determine a default syntax rule *) + add_notation_in_scope local df c modifiers sc + else + (* Declare both syntax and interpretation *) + add_notation_in_scope local df c modifiers sc + +(* Infix notations *) let inject_var x = CRef (Ident (dummy_loc, id_of_string x)) -let rec rename x vars n = function - | [] -> - (vars,[]) - | String "_"::l -> - let (vars,l) = rename x vars (n+1) l in - let xn = x^(string_of_int n) in - ((inject_var xn)::vars,xn::l) - | String y::l -> - let (vars,l) = rename x vars n l in (vars,(quote_notation_token y)::l) - | WhiteSpace _::l -> - rename x vars n l - -let translate_distfix assoc df r = - let (vars,l) = rename "x" [] 1 (split_notation_string df) in - let df = String.concat " " l in - let a = mkAppC (mkRefC r, vars) in - let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in - (assoc,df,a) - -let add_distfix local assoc n df r sc = - (* "x" cannot clash since r is globalized (included section vars) *) - let (vars,l) = rename "x" [] 1 (split_notation_string df) in - let df = String.concat " " l in - let a = mkAppC (mkRefC r, vars) in - let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in - add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc - -let make_infix_data n assoc modl mv8 = - (* Infix defaults to LEFTA in V7 (cf doc) *) - let mv = match n with None when !Options.v7 -> SetLevel 1 :: modl | _ -> modl in - let mv = match assoc with None when !Options.v7 -> SetAssoc Gramext.LeftA :: mv | _ -> mv in - let mv8 = match mv8 with - None -> None - | Some(s8,mv8) -> - if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then - error "Needs a level" - else Some (("x "^quote_notation_token s8^" y"),mv8) in - mv,mv8 - -let add_infix local (inf,modl) pr mv8 sc = - if inf="" (* Code for V8Infix only *) then - let (p8,mv8) = out_some mv8 in - let (a8,n8,onlyparse,fmt) = interp_infix_modifiers mv8 in - let metas = [inject_var "x"; inject_var "y"] in - let a = mkAppC (mkRefC pr,metas) in - let df = "x "^(quote_notation_token p8)^" y" in - let toks = split_notation_string df in - if a8=None & n8=None & fmt=None then - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let (acvars,ac) = interp_aconstr [] vars a in - let a' = (remove_vars recs acvars,ac) in - let a_for_old = interp_global_rawconstr_with_vars vars a in - add_notation_interpretation_core local symbs None df a' sc - onlyparse true None - else - if n8 = None then error "Needs a level" else - let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in - add_notation_in_scope_v8only local df a mv8 sc - else begin - let (assoc,n,onlyparse,fmt) = interp_infix_modifiers modl in +let add_infix local (inf,modifiers) pr sc = + check_infix_modifiers modifiers; (* check the precedence *) - if !Options.v7 & (n<> None & (out_some n < 1 or out_some n > 10)) then - errorlabstrm "Metasyntax.infix_grammar_entry" - (str"Precedence must be between 1 and 10."); - (* - if (assoc<>None) & (n<6 or n>9) then - errorlabstrm "Vernacentries.infix_grammar_entry" - (str"Associativity Precedence must be 6,7,8 or 9."); - *) let metas = [inject_var "x"; inject_var "y"] in - let a = mkAppC (mkRefC pr,metas) in + let c = mkAppC (mkRefC pr,metas) in let df = "x "^(quote_notation_token inf)^" y" in - let toks = split_notation_string df in - if not !Options.v7 & n=None & assoc=None then - (* En v8, une notation sans information de parsing signifie *) - (* de ne déclarer que l'interprétation *) - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let gram_data = recover_notation_syntax (make_notation_key symbs) in - if gram_data <> None then - let (acvars,ac) = interp_aconstr [] vars a in - let a' = (remove_vars recs acvars,ac) in - let a_for_old = interp_global_rawconstr_with_vars vars a in - let for_old = set_data_for_v7_pp recs a_for_old vars in - add_notation_interpretation_core local symbs for_old df a' sc - onlyparse false gram_data - else - let mv,mv8 = make_infix_data n assoc modl mv8 in - add_notation_in_scope local df a mv mv8 sc - else - let mv,mv8 = make_infix_data n assoc modl mv8 in - add_notation_in_scope local df a mv mv8 sc - end + add_notation local c (df,modifiers) sc + +(**********************************************************************) +(* Miscellaneous *) -let standardise_locatable_notation ntn = +let standardize_locatable_notation ntn = let unquote = function | String s -> [unquote_notation_token s] | _ -> [] in @@ -1480,17 +1002,19 @@ let standardise_locatable_notation ntn = else unquote_notation_token ntn -(* Delimiters and classes bound to scopes *) +(**********************************************************************) +(* Delimiters and classes bound to scopes *) + type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ let load_scope_command _ (_,(scope,dlm)) = - Symbols.declare_scope scope + Notation.declare_scope scope let open_scope_command i (_,(scope,o)) = if i=1 then match o with - | ScopeDelim dlm -> Symbols.declare_delimiters scope dlm - | ScopeClasses cl -> Symbols.declare_class_scope scope cl + | ScopeDelim dlm -> Notation.declare_delimiters scope dlm + | ScopeClasses cl -> Notation.declare_class_scope scope cl let cache_scope_command o = load_scope_command 1 o; diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index be90cd7a..71522567 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,v 1.26.2.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: metasyntax.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) (*i*) open Util @@ -15,49 +15,44 @@ open Ppextend open Extend open Tacexpr open Vernacexpr -open Symbols +open Notation open Topconstr (*i*) -(* Adding grammar and pretty-printing objects in the environment *) +val add_token_obj : string -> unit -val add_syntax_obj : string -> raw_syntax_entry list -> unit +(* Adding a tactic notation in the environment *) -val add_grammar_obj : string -> raw_grammar_entry list -> unit -val add_token_obj : string -> unit -val add_tactic_grammar : - (string * (string * grammar_production list) * raw_tactic_expr) list -> unit +val add_tactic_notation : + int * grammar_production list * raw_tactic_expr -> unit + +(* Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (string * syntax_modifier list) -> - reference -> (string * syntax_modifier list) option -> - scope_name option -> unit -val add_distfix : locality_flag -> - grammar_associativity -> precedence -> string -> reference - -> scope_name option -> unit -val translate_distfix : grammar_associativity -> string -> reference -> - Gramext.g_assoc * string * constr_expr + reference -> scope_name option -> unit + +val add_notation : locality_flag -> constr_expr -> + (string * syntax_modifier list) -> scope_name option -> unit + +(* Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit val add_class_scope : scope_name -> Classops.cl_typ -> unit -val add_notation : locality_flag -> constr_expr - -> (string * syntax_modifier list) option - -> (string * syntax_modifier list) option - -> scope_name option -> unit +(* Add only the interpretation of a notation that already has pa/pp rules *) -val add_notation_interpretation : string -> Constrintern.implicits_env - -> constr_expr -> scope_name option -> unit +val add_notation_interpretation : string -> Constrintern.implicits_env -> + constr_expr -> scope_name option -> unit -val add_syntax_extension : locality_flag - -> (string * syntax_modifier list) option - -> (string * syntax_modifier list) option -> unit +(* Add only the parsing/printing rule of a notation *) -val print_grammar : string -> string -> unit +val add_syntax_extension : + locality_flag -> (string * syntax_modifier list) -> unit -val merge_modifiers : Gramext.g_assoc option -> int option -> - syntax_modifier list -> syntax_modifier list +(* Print the Camlp4 state of a grammar *) + +val print_grammar : string -> string -> unit -val interp_infix_modifiers : syntax_modifier list -> - Gramext.g_assoc option * precedence option * bool * string located option +(* Removes quotes in a notation *) -val standardise_locatable_notation : string -> string +val standardize_locatable_notation : string -> string diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index dcf3e307..490765a4 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: minicoq.ml,v 1.28.14.1 2004/07/16 19:31:49 herbelin Exp $ *) +(* $Id: minicoq.ml 5920 2004-07-16 20:01:26Z herbelin $ *) open Pp open Util diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 4da23d42..a3b7fc14 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mltop.ml4,v 1.29.2.3 2004/07/17 13:00:15 herbelin Exp $ *) +(* $Id: mltop.ml4 6692 2005-02-06 13:03:51Z herbelin $ *) open Util open Pp @@ -109,7 +109,7 @@ let dir_ml_load s = [Filename.dirname gname] with | Dynlink.Error a -> errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >] - else () + else () | Native -> errorlabstrm "Mltop.no_load_object" [< str"Loading of ML object file forbidden in a native Coq" >] @@ -137,7 +137,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = if exists_dir dir then begin add_ml_dir dir; - Library.add_load_path_entry (dir,coq_dirpath) + Library.add_load_path (dir,coq_dirpath) end else msg_warning [< str ("Cannot open " ^ dir) >] @@ -160,7 +160,7 @@ let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = let dirs = map_succeed convert_dirs dirs in begin List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - List.iter Library.add_load_path_entry dirs + List.iter Library.add_load_path dirs end else msg_warning [< str ("Cannot open " ^ dir) >] diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 6ba8cd76..b869f70b 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,v 1.8.14.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: mltop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* If there is a toplevel under Coq, it is described by the following record. *) diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index c748a12d..a9ff3326 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: protectedtoplevel.ml,v 1.9.10.1 2004/07/16 19:31:49 herbelin Exp $ *) +(* $Id: protectedtoplevel.ml 5920 2004-07-16 20:01:26Z herbelin $ *) open Pp open Line_oriented_parser diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli index b31afbf6..1d4ba9fc 100644 --- a/toplevel/protectedtoplevel.mli +++ b/toplevel/protectedtoplevel.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: protectedtoplevel.mli,v 1.5.16.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: protectedtoplevel.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/record.ml b/toplevel/record.ml index 3a10c7e5..b24e85da 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml,v 1.52.2.2 2005/11/29 21:40:53 letouzey Exp $ *) +(* $Id: record.ml 7941 2006-01-28 23:07:59Z herbelin $ *) open Pp open Util @@ -20,7 +20,6 @@ open Declarations open Entries open Declare open Nametab -open Coqast open Constrintern open Command open Inductive @@ -37,31 +36,14 @@ let interp_decl sigma env = function | Vernacexpr.DefExpr((_,id),c,t) -> let c = match t with | None -> c - | Some t -> mkCastC (c,t) + | Some t -> mkCastC (c,DEFAULTcast,t) in - let j = judgment_of_rawconstr Evd.empty env c in + let j = interp_constr_judgment Evd.empty env c in (id,Some j.uj_val, j.uj_type) let typecheck_params_and_fields ps fs = let env0 = Global.env () in - let env1,newps = - List.fold_left - (fun (env,newps) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> - let t = interp_binder Evd.empty env na t in - let d = (na,None,t) in - (push_rel d env, d::newps) - | LocalRawAssum (nal,t) -> - let t = interp_type Evd.empty env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in - let ctx = List.rev ctx in - (push_rel_context ctx env, ctx@newps) - | LocalRawDef ((_,na),c) -> - let c = judgment_of_rawconstr Evd.empty env c in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env, d::newps)) - (env0,[]) ps - in + let env1,newps = interp_context Evd.empty env0 ps in let env2,newfs = List.fold_left (fun (env,newfs) d -> @@ -146,19 +128,20 @@ let subst_projection fid l c = let declare_projections indsp coers fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let paramdecls = mip.mind_params_ctxt in + let paramdecls = mib.mind_params_ctxt in let r = mkInd indsp in let rp = applist (r, extended_rel_list 0 paramdecls) in let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = Termops.named_hd (Global.env()) r Anonymous in let lifted_fields = lift_rel_context 1 fields in - let (_,sp_projs,_) = + let (_,kinds,sp_projs,_) = List.fold_left2 - (fun (nfi,sp_projs,subst) coe (fi,optci,ti) -> - match fi with - | Anonymous -> - (nfi-1, None::sp_projs,NoProjection fi::subst) - | Name fid -> + (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) -> + let (sp_projs,subst) = + match fi with + | Anonymous -> + (None::sp_projs,NoProjection fi::subst) + | Name fid -> try let ccl = subst_projection fid subst ti in let body = match optci with @@ -176,32 +159,34 @@ let declare_projections indsp coers fields = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in - let (sp,kn) = + let kn = try let cie = { const_entry_body = proj; const_entry_type = Some projtyp; - const_entry_opaque = false } in - let k = (DefinitionEntry cie,IsDefinition) in - let sp = declare_internal_constant fid k in + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() } in + let k = (DefinitionEntry cie,IsDefinition StructureComponent) in + let kn = declare_internal_constant fid k in Options.if_verbose message (string_of_id fid ^" is defined"); - sp + kn with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = ConstRef kn in let constr_fi = mkConst kn in if coe then begin - let cl = Class.class_of_ref (IndRef indsp) in + let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi Global cl end; let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in let constr_fip = applist (constr_fi,proj_args) in - (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst) + (Some kn::sp_projs, Projection constr_fip::subst) with NotDefinable why -> warning_or_error coe indsp why; - (nfi-1, None::sp_projs,NoProjection fi::subst)) - (List.length fields,[],[]) coers (List.rev fields) - in sp_projs + (None::sp_projs,NoProjection fi::subst) in + (nfi-1,(optci=None)::kinds,sp_projs,subst)) + (List.length fields,[],[],[]) coers (List.rev fields) + in (kinds,sp_projs) (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) @@ -220,18 +205,18 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let ind = applist (mkRel (1+List.length params+List.length fields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let mie_ind = - { mind_entry_params = List.map degenerate_decl params; - mind_entry_typename = idstruc; + { mind_entry_typename = idstruc; mind_entry_arity = mkSort s; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in let mie = - { mind_entry_record = true; + { mind_entry_params = List.map degenerate_decl params; + mind_entry_record = true; mind_entry_finite = true; mind_entry_inds = [mie_ind] } in let sp = declare_mutual_with_eliminations true mie in let rsp = (sp,0) in (* This is ind path of idstruc *) - let sp_projs = declare_projections rsp coers fields in + let kinds,sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) if is_coe then Class.try_add_new_coercion build Global; - Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs) + Recordops.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs) diff --git a/toplevel/record.mli b/toplevel/record.mli index 8eff2ed5..66282c20 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,v 1.16.2.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: record.mli 6743 2005-02-18 22:14:08Z herbelin $ i*) (*i*) open Names @@ -21,7 +21,7 @@ open Topconstr [coers]; it returns the absolute names of projections *) val declare_projections : - inductive -> bool list -> rel_context -> constant option list + inductive -> bool list -> rel_context -> bool list * constant option list val definition_structure : lident with_coercion * local_binder list * diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml deleted file mode 100755 index d2a1e36e..00000000 --- a/toplevel/recordobj.ml +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: recordobj.ml,v 1.12.2.1 2004/07/16 19:31:49 herbelin Exp $ *) - -open Util -open Pp -open Names -open Libnames -open Nameops -open Term -open Instantiate -open Lib -open Declare -open Recordops -open Classops -open Nametab - -(***** object definition ******) - -let typ_lams_of t = - let rec aux acc c = match kind_of_term c with - | Lambda (x,c1,c2) -> aux (c1::acc) c2 - | Cast (c,_) -> aux acc c - | t -> acc,t - in aux [] t - -let objdef_err ref = - errorlabstrm "object_declare" - (pr_id (id_of_global ref) ++ - str" is not a structure object") - -let objdef_declare ref = - let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in - let env = Global.env () in - let v = constr_of_reference ref in - let vc = match Environ.constant_opt_value env sp with - | Some vc -> vc - | None -> objdef_err ref in - let lt,t = decompose_lam vc in - let lt = List.rev (List.map snd lt) in - let f,args = match kind_of_term t with - | App (f,args) -> f,args - | _ -> objdef_err ref in - let { s_PARAM = p; s_PROJ = lpj } = - try (find_structure - (match kind_of_term f with - | Construct (indsp,1) -> indsp - | _ -> objdef_err ref)) - with Not_found -> objdef_err ref in - let params, projs = - try list_chop p (Array.to_list args) - with _ -> objdef_err ref in - let lps = - try List.combine lpj projs - with _ -> objdef_err ref in - let comp = - List.fold_left - (fun l (spopt,t) -> (* comp=components *) - match spopt with - | None -> l - | Some proji_sp -> - let c, args = decompose_app t in - try (ConstRef proji_sp, reference_of_constr c, args) :: l - with Not_found -> l) - [] lps in - add_anonymous_leaf (inObjDef1 sp); - List.iter - (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj)) - comp - -let add_object_hook _ = objdef_declare diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli index f1ad7d5a..184725b2 100644 --- a/toplevel/searchisos.mli +++ b/toplevel/searchisos.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: searchisos.mli,v 1.3.16.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: searchisos.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) val search_in_lib : bool ref val type_search : Term.constr -> unit diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7fa80bcb..a5c2564c 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml,v 1.22.2.2 2004/07/16 20:48:17 herbelin Exp $ *) +(* $Id: toplevel.ml 6947 2005-04-20 16:18:41Z coq $ *) open Pp open Util @@ -182,11 +182,44 @@ let make_prompt () = with _ -> "Coq < " +(*let build_pending_list l = + let pl = ref ">" in + let l' = ref l in + let res = + while List.length !l' > 1 do + pl := !pl ^ "|" Names.string_of_id x; + l':=List.tl !l' + done in + let last = try List.hd !l' with _ -> in + "<"^l' +*) + +(* the coq prompt added to the default one when in emacs mode + The prompt contains the current state label [n] (for global + backtracking) and the current proof state [p] (for proof + backtracking) plus the list of open (nested) proofs (for proof + aborting when backtracking). It looks like: + + "n |lem1|lem2|lem3| p < " +*) +let make_emacs_prompt() = + let statnum = string_of_int (Lib.current_command_label ()) in + let endchar = String.make 1 (Char.chr 249) in + let dpth = Pfedit.current_proof_depth() in + let pending = Pfedit.get_all_proof_names() in + let pendingprompt = + List.fold_left + (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) + "" pending in + let proof_info = if dpth >= 0 then string_of_int dpth else "0" in + statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ endchar + (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) let top_buffer = - let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249))) + let pr() = + make_prompt() ^ Printer.emacs_str (make_emacs_prompt()) in { prompt = pr; str = ""; @@ -197,7 +230,7 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> (prompt ()) ^ (emacs_str (String.make 1 (Char.chr 249)))) + <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249)))) (* Removes and prints the location of the error. The following exceptions need not be located. *) diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 1b6b48d4..f4d2e28a 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: toplevel.mli,v 1.6.10.1 2004/07/16 19:31:50 herbelin Exp $ i*) +(*i $Id: toplevel.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/usage.ml b/toplevel/usage.ml index b00cfffc..354aff0b 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml,v 1.15.2.2 2004/09/03 14:35:26 herbelin Exp $ *) +(* $Id: usage.ml 6053 2004-09-03 14:33:35Z herbelin $ *) let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 16929d68..97814fd2 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: usage.mli,v 1.5.16.1 2004/07/16 19:31:50 herbelin Exp $ i*) +(*i $Id: usage.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*s Prints the version number on the standard output and exits (with 0). *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a5716619..64d77b74 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml,v 1.59.2.3 2004/07/16 20:48:17 herbelin Exp $ *) +(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *) (* Parsing of vernacular. *) @@ -15,10 +15,9 @@ open Lexer open Util open Options open System -open Coqast open Vernacexpr open Vernacinterp -open Ppvernacnew +open Ppvernac (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions @@ -57,7 +56,7 @@ 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_path ()) fname in + let _,longfname = find_file_in_path (Library.get_load_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 @@ -95,62 +94,18 @@ let parse_phrase (po, verbch) = let just_parsing = ref false let chan_translate = ref stdout -let last_char = ref '\000' -(* postprocessor to avoid lexical icompatibilities between V7 and V8. - Ex: auto.(* comment *) or simpl.auto - *) let set_formatter_translator() = let ch = !chan_translate in - let out s b e = - let n = e-b in - if n > 0 then begin - (match !last_char with - '.' -> - (match s.[b] with - '('|'a'..'z'|'A'..'Z' -> output ch " " 0 1 - | _ -> ()) - | _ -> ()); - last_char := s.[e-1] - end; - output ch s b e - 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 pre_printing = function - | VernacSolve (i,tac,deftac) when Options.do_translate () -> - (try - let (_,env) = Pfedit.get_goal_context i in - let t = Options.with_option Options.translate_syntax - (Tacinterp.glob_tactic_env [] env) tac in - let pfts = Pfedit.get_pftreestate () in - let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in - Some (env,t,Pfedit.focus(),List.length gls) - with UserError _|Stdpp.Exc_located _ -> None) - | _ -> None - -let post_printing loc (env,t,f,n) = function - | VernacSolve (i,_,deftac) -> - let loc = unloc loc in - set_formatter_translator(); - let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in - (if !translate_file then begin - msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1))); - end - else - msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp))); - Format.set_formatter_out_channel stdout - | _ -> () - let pr_new_syntax loc ocom = let loc = unloc loc in if !translate_file then set_formatter_translator(); let fs = States.freeze () in let com = match ocom with - | Some (VernacV7only _) -> - Options.v7_only := true; - mt() | Some VernacNop -> mt() | Some com -> pr_vernac com | None -> mt() in @@ -159,8 +114,6 @@ let pr_new_syntax loc ocom = else msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; - Constrintern.set_temporary_implicits_in []; - Constrextern.set_temporary_implicits_out []; Format.set_formatter_out_channel stdout let rec vernac_com interpfun (loc,com) = @@ -174,7 +127,7 @@ let rec vernac_com interpfun (loc,com) = (* coqdoc state *) let cds = Constrintern.coqdoc_freeze() in if !Options.translate_file then begin - let _,f = find_file_in_path (Library.get_load_path ()) + let _,f = find_file_in_path (Library.get_load_paths ()) (make_suffix fname ".v") in chan_translate := open_out (f^"8"); Pp.comments := [] @@ -203,39 +156,14 @@ let rec vernac_com interpfun (loc,com) = msgnl (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) - (* To be interpreted in v7 or translator input only *) - | VernacV7only v -> - Options.v7_only := true; - if !Options.v7 || Options.do_translate() then interp v; - Options.v7_only := false - - (* To be interpreted in translator output only *) - | VernacV8only v -> - if not !Options.v7 && not (do_translate()) then - interp v - | v -> if not !just_parsing then interpfun v in try - Options.v7_only := false; - if do_translate () then - match pre_printing com with - None -> - pr_new_syntax loc (Some com); - interp com - | Some state -> - (try - interp com; - post_printing loc state com - with e -> - post_printing loc state com; - raise e) - else - interp com + if do_translate () then pr_new_syntax loc (Some com); + interp com with e -> Format.set_formatter_out_channel stdout; - Options.v7_only := false; raise (DuringCommandInterp (loc, e)) and vernac interpfun input = diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d8f4b247..4f95376f 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernac.mli,v 1.10.2.1 2004/07/16 19:31:50 herbelin Exp $ i*) +(*i $Id: vernac.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Parsing of vernacular. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1c6ad9a6..7394bd8f 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,v 1.195.2.1 2004/07/16 19:31:50 herbelin Exp $ i*) +(*i $Id: vernacentries.ml 8700 2006-04-11 23:14:15Z courtieu $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -23,6 +23,7 @@ open Proof_trees open Constrintern open Prettyp open Printer +open Tactic_printer open Tacinterp open Command open Goptions @@ -32,6 +33,7 @@ open Vernacexpr open Decl_kinds open Topconstr open Pretyping +open Redexpr (* Pcoq hooks *) @@ -55,14 +57,13 @@ let set_pcoq_hook f = pcoq := Some f let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_ref (Nametab.global r) + | RefClass r -> Class.class_of_global (Nametab.global r) (*******************) (* "Show" commands *) let show_proof () = let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts in let cursor = cursor_of_pftreestate pts in let evc = evc_of_pftreestate pts in let (pfterm,meta_types) = extract_open_pftreestate pts in @@ -70,41 +71,41 @@ let show_proof () = prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ str"Subgoals" ++ fnl () ++ prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ - prtype ty ++ fnl ()) + pr_ltype ty ++ fnl ()) meta_types - ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm)) + ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm)) let show_node () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and cursor = cursor_of_pftreestate pts in msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - prgl (goal_of_proof pf) ++ fnl () ++ + pr_goal (goal_of_proof pf) ++ fnl () ++ (match pf.Proof_type.ref with | None -> (str"BY <rule>") | Some(r,spfl) -> - (str"BY " ++ Refiner.pr_rule r ++ fnl () ++ + (str"BY " ++ pr_rule r ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl prgl + hov 0 (prlist_with_sep pr_fnl pr_goal (List.map goal_of_proof spfl))))) let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (Refiner.print_treescript true evc (Global.named_context()) pf) + msgnl (print_treescript true evc (Global.named_context()) pf) let show_top_evars () = let pfts = get_pftreestate () in let gls = top_goal_of_pftreestate pfts in let sigma = project gls in - msg (pr_evars_int 1 (Evd.non_instantiated sigma)) + msg (pr_evars_int 1 (Evarutil.non_instantiated sigma)) let show_prooftree () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msg (Refiner.print_proof evc (Global.named_context()) pf) + msg (print_proof evc (Global.named_context()) pf) let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () @@ -112,7 +113,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () let fresh_id_of_name avoid gl = function Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl - | Name id -> id + | Name id -> Tactics.fresh_id avoid id gl let rec do_renum avoid gl = function [] -> mt () @@ -121,27 +122,83 @@ let rec do_renum avoid gl = function let id = fresh_id_of_name avoid gl n in pr_id id ++ spc () ++ do_renum (id :: avoid) gl l +(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *) +let decompose_prod_letins = + let rec prodec_rec l c = match kind_of_term c with + | Prod (x,t,c) -> prodec_rec ((x,t)::l) c + | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c + | Cast (c,_,_) -> prodec_rec l c + | _ -> l,c + in + prodec_rec [] + let show_intro all = let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in - let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in + let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in let nl = List.rev_map fst l in - if all then - msgnl (do_renum [] gl nl) - else - try - let n = List.hd nl in - msgnl (pr_id (fresh_id_of_name [] gl n)) - with Failure "hd" -> message "" + if all then msgnl (hov 0 (do_renum [] gl nl)) + else try + let n = List.hd nl in + msgnl (pr_id (fresh_id_of_name [] gl n)) + with Failure "hd" -> message "" + + +let id_of_name = function + | Names.Anonymous -> id_of_string "x" + | Names.Name x -> x + + +(* Building of match expression *) +(* From ide/coq.ml *) +let make_cases s = + let qualified_name = Libnames.qualid_of_string s in + let glob_ref = Nametab.locate qualified_name in + match glob_ref with + | Libnames.IndRef i -> + let {Declarations.mind_nparams = np} + , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } + = Global.lookup_inductive i in + Util.array_fold_right2 + (fun n t l -> + let (al,_) = Term.decompose_prod t in + let al,_ = Util.list_chop (List.length al - np) al in + let rec rename avoid = function + | [] -> [] + | (n,_)::l -> + let n' = Termops.next_global_ident_away true (id_of_name n) avoid in + string_of_id n' :: rename (n'::avoid) l in + let al' = rename [] (List.rev al) in + (string_of_id n :: al') :: l) + carr tarr [] + | _ -> raise Not_found + + +let show_match id = + try + let s = string_of_id (snd id) in + let patterns = make_cases s in + let cases = + List.fold_left + (fun acc x -> + match x with + | [] -> assert false + | [x] -> "| "^ x ^ " => \n" ^ acc + | x::l -> + "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")" + ^ " => \n" ^ acc) + "end" patterns in + msg (str ("match # with\n" ^ cases)) + with Not_found -> error "Unknown inductive type" -(********************) (* "Print" commands *) let print_path_entry (s,l) = (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l)) let print_loadpath () = - let l = Library.get_full_load_path () in + let l = Library.get_full_load_paths () in msgnl (Pp.t (str "Physical path: " ++ tab () ++ str "Logical Path:" ++ fnl () ++ prlist_with_sep pr_fnl print_path_entry l)) @@ -190,8 +247,7 @@ let dump_universes s = let locate_file f = try - let _,file = - System.where_in_path (Library.get_load_path()) f in + let _,file = System.where_in_path (Library.get_load_paths ()) f in msgnl (str file) with Not_found -> msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ @@ -219,13 +275,22 @@ let print_located_library r = try msg_found_library (Library.locate_qualified_library qid) with e -> msg_notfound_library loc qid e +let print_located_module r = + let (loc,qid) = qualid_of_reference r in + let msg = + try + let dir = Nametab.full_name_module qid in + str "Module " ++ pr_dirpath dir + with Not_found -> + (if fst (repr_qualid qid) = empty_dirpath then + str "No module is referred to by basename " + else + str "No module is referred to by name ") ++ pr_qualid qid + in msgnl msg + (**********) (* Syntax *) -let vernac_syntax = Metasyntax.add_syntax_obj - -let vernac_grammar = Metasyntax.add_grammar_obj - let vernac_syntax_extension = Metasyntax.add_syntax_extension let vernac_delimiters = Metasyntax.add_delimiters @@ -233,15 +298,13 @@ let vernac_delimiters = Metasyntax.add_delimiters let vernac_bind_scope sc cll = List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll -let vernac_open_close_scope = Symbols.open_close_scope +let vernac_open_close_scope = Notation.open_close_scope let vernac_arguments_scope qid scl = - Symbols.declare_arguments_scope (global qid) scl + Notation.declare_arguments_scope (global qid) scl let vernac_infix = Metasyntax.add_infix -let vernac_distfix = Metasyntax.add_distfix - let vernac_notation = Metasyntax.add_notation (***********) @@ -252,7 +315,7 @@ let start_proof_and_print idopt k t hook = print_subgoals (); if !pcoq <> None then (out_some !pcoq).start_proof () -let vernac_definition (local,_ as k) id def hook = +let vernac_definition (local,_,_ as k) id def hook = match def with | ProveBody (bl,t) -> (* local binders, typ *) if Lib.is_modtype () then @@ -260,8 +323,7 @@ let vernac_definition (local,_ as k) id def hook = (str "Proof editing mode not supported in module types") else let hook _ _ = () in - let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in - start_proof_and_print (Some id) kind (bl,t) hook + start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -278,7 +340,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook = if Lib.is_modtype () then errorlabstrm "Vernacentries.StartProof" (str "Proof editing mode not supported in module types"); - start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook + start_proof_and_print sopt (Global, Proof kind) (bl,t) hook let vernac_end_proof = function | Admitted -> admit () @@ -293,9 +355,15 @@ let vernac_end_proof = function the theories [??] *) let vernac_exact_proof c = - by (Tactics.exact_proof c); - save_named true - + let pfs = top_of_tree (get_pftreestate()) in + let pf = proof_of_pftreestate pfs in + if (is_leaf_proof pf) then begin + by (Tactics.exact_proof c); + save_named true end + else + errorlabstrm "Vernacentries.ExactProof" + (str "Command 'Proof ...' can only be used at the beginning of the proof") + let vernac_assumption kind l = List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l @@ -310,107 +378,70 @@ let vernac_scheme = build_scheme (**********************) (* Modules *) -let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o = +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 vernac_declare_module export id binders_ast mty_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; - - if not (Lib.is_modtype ()) then - error "Declare Module allowed in module types only"; - - let constrain_mty = match mty_ast_o with - Some (_,true) -> true - | _ -> false - in - - match mty_ast_o, constrain_mty, mexpr_ast_o with - | _, false, None -> (* no ident, no/soft type *) - Declaremods.start_module Modintern.interp_modtype - id binders_ast mty_ast_o; - if_verbose message - ("Interactive Declaration of Module "^ string_of_id id ^" started") - - | Some _, true, None (* no ident, hard type *) - | _, false, Some (CMEident _) -> (* ident, no/soft type *) - Declaremods.declare_module - Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast mty_ast_o mexpr_ast_o; - if_verbose message - ("Module "^ string_of_id id ^" is declared") - - | _, true, Some (CMEident _) -> (* ident, hard type *) - error "You cannot declare an equality and a type in module declaration" - - | _, _, Some _ -> (* not ident *) - error "Only simple modules allowed in module declarations" - - | None,true,None -> assert false (* 1st None ==> false *) - -let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o = + let binders_ast = List.map + (fun (export,idl,ty) -> + if export <> None then + error ("Arguments of a functor declaration cannot be exported. " ^ + "Remove the \"Export\" and \"Import\" keywords from every functor " ^ + "argument.") + else (idl,ty)) binders_ast in + Declaremods.declare_module + Modintern.interp_modtype Modintern.interp_modexpr + id binders_ast (Some mty_ast_o) None; + 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 id binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; - - if Lib.is_modtype () then - error "Module definitions not allowed in module types. Use Declare Module instead"; - match mexpr_ast_o with | None -> - Declaremods.start_module Modintern.interp_modtype + let binders_ast,argsexport = + List.fold_right + (fun (export,idl,ty) (args,argsexport) -> + (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast + ([],[]) in + Declaremods.start_module Modintern.interp_modtype export id binders_ast mty_ast_o; if_verbose message - ("Interactive Module "^ string_of_id id ^" started") - + ("Interactive Module "^ string_of_id id ^" started") ; + List.iter + (fun (export,id) -> + option_iter + (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + ) argsexport | Some _ -> + 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 Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr id binders_ast mty_ast_o mexpr_ast_o; if_verbose message - ("Module "^ string_of_id id ^" is defined") - -(* let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o = *) -(* (\* We check the state of the system (in section, in module type) *) -(* and what module information is supplied *\) *) -(* if Lib.sections_are_opened () then *) -(* error "Modules and Module Types are not allowed inside sections"; *) - -(* let constrain_mty = match mty_ast_o with *) -(* Some (_,true) -> true *) -(* | _ -> false *) -(* in *) - -(* match Lib.is_modtype (), mty_ast_o, constrain_mty, mexpr_ast_o with *) -(* | _, None, _, None *) -(* | true, Some _, false, None *) -(* | false, _, _, None -> *) -(* Declaremods.start_module Modintern.interp_modtype *) -(* id binders_ast mty_ast_o; *) -(* if_verbose message *) -(* ("Interactive Module "^ string_of_id id ^" started") *) - -(* | true, Some _, true, None *) -(* | true, _, false, Some (CMEident _) *) -(* | false, _, _, Some _ -> *) -(* Declaremods.declare_module *) -(* Modintern.interp_modtype Modintern.interp_modexpr *) -(* id binders_ast mty_ast_o mexpr_ast_o; *) -(* if_verbose message *) -(* ("Module "^ string_of_id id ^" is defined") *) - -(* | true, _, _, _ -> *) -(* error "Module definition not allowed in a Module Type" *) - -let vernac_end_module id = - Declaremods.end_module id; - if_verbose message - (if Lib.is_modtype () then - "Module "^ string_of_id id ^" is declared" - else - "Module "^ string_of_id id ^" is defined") + ("Module "^ string_of_id id ^" is defined"); + option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + export - +let vernac_end_module export id = + Declaremods.end_module id; + 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 id binders_ast mty_ast_o = @@ -419,11 +450,28 @@ let vernac_declare_module_type id binders_ast mty_ast_o = match mty_ast_o with | None -> + let binders_ast,argsexport = + List.fold_right + (fun (export,idl,ty) (args,argsexport) -> + (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast + ([],[]) in Declaremods.start_modtype Modintern.interp_modtype id binders_ast; if_verbose message - ("Interactive Module Type "^ string_of_id id ^" started") + ("Interactive Module Type "^ string_of_id id ^" started"); + List.iter + (fun (export,id) -> + option_iter + (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + ) 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 Declaremods.declare_modtype Modintern.interp_modtype id binders_ast base_mty; if_verbose message @@ -455,86 +503,26 @@ let vernac_record struc binders sort nameopt cfs = (* Sections *) -let vernac_begin_section id = let _ = Lib.open_section id in () - -let vernac_end_section id = - Discharge.close_section (is_verbose ()) id - +let vernac_begin_section = Lib.open_section +let vernac_end_section = Lib.close_section let vernac_end_segment id = check_no_pending_proofs (); - try - match Lib.what_is_opened () with - | _,Lib.OpenedModule _ -> vernac_end_module id - | _,Lib.OpenedModtype _ -> vernac_end_modtype id - | _,Lib.OpenedSection _ -> vernac_end_section id - | _ -> anomaly "No more opened things" - with - Not_found -> error "There is nothing to end." - -let is_obsolete_module (_,qid) = - match repr_qualid qid with - | dir, id when dir = empty_dirpath -> - (match string_of_id id with - | ("Refine" | "Inv" | "Equality" | "EAuto" | "AutoRewrite" - | "EqDecide" | "Xml" | "Extraction" | "Tauto" | "Setoid_replace" - | "Elimdep" - | "DatatypesSyntax" | "LogicSyntax" | "Logic_TypeSyntax" - | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax" | "PolyListSyntax") - -> true - | _ -> false) - | _ -> false - -let test_renamed_module (_,qid) = - match repr_qualid qid with - | dir, id when dir = empty_dirpath -> - (match string_of_id id with - | "List" -> warning "List has been renamed into MonoList" - | "PolyList" -> warning "PolyList has been renamed into List and old List into MonoList" - | _ -> ()) - | _ -> () - + let o = + try Lib.what_is_opened () + with Not_found -> error "There is nothing to end." in + match o with + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id + | _,Lib.OpenedModtype _ -> vernac_end_modtype id + | _,Lib.OpenedSection _ -> vernac_end_section id + | _ -> anomaly "No more opened things" + let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in - try - match import with - | None -> List.iter Library.read_library qidl - | Some b -> Library.require_library None qidl b - with e -> - (* Compatibility message *) - let qidl' = List.filter is_obsolete_module qidl in - if qidl' = qidl then - List.iter - (fun (_,qid) -> - warning ("Module "^(string_of_qualid qid)^ - " is now built-in and shouldn't be required")) qidl - else - (if not !Options.v7 then List.iter test_renamed_module qidl; - raise e) - -let vernac_import export refl = - let import_one ref = - let qid = qualid_of_reference ref in - Library.import_library export qid - in - List.iter import_one refl; - Lib.add_frozen_state () - -(* else - let import (loc,qid) = - try - let mp = Nametab.locate_module qid in - Declaremods.import_module mp - with Not_found -> - user_err_loc - (loc,"vernac_import", - str ((string_of_qualid qid)^" is not a module")) - in - List.iter import qidl; -*) + Library.require_library qidl import let vernac_canonical locqid = - Recordobj.objdef_declare (Nametab.global locqid) + Recordops.declare_canonical_structure (Nametab.global locqid) let locate_reference ref = let (loc,qid) = qualid_of_reference ref in @@ -591,18 +579,14 @@ let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = if not (refining ()) then error "Unknown command of the non proof-editing mode"; - if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac) -(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) - - + if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else () + (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) + (*****************************) (* Auxiliary file management *) let vernac_require_from export spec filename = - match export with - Some exp -> - Library.require_library_from_file spec None filename exp - | None -> Library.read_library_from_file filename + Library.require_library_from_file None filename export let vernac_add_loadpath isrec pdir ldiropt = let alias = match ldiropt with @@ -610,7 +594,7 @@ let vernac_add_loadpath isrec pdir ldiropt = | Some ldir -> ldir in (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias -let vernac_remove_loadpath = Library.remove_path +let vernac_remove_loadpath = Library.remove_load_path (* Coq syntax for ML or system commands *) @@ -651,7 +635,9 @@ let vernac_reset_initial () = abort_refine Lib.reset_initial () let vernac_back n = Lib.back n +let vernac_backto n = Lib.reset_label n +(* see also [vernac_backtrack] which combines undoing and resetting *) (************) (* Commands *) @@ -667,7 +653,7 @@ let vernac_declare_implicits locqid = function let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in - let t = Detyping.detype (false,Global.env()) [] [] t in + let t = Detyping.detype false [] [] t in List.iter (fun id -> Reserve.declare_reserved_type id t) idl let make_silent_if_not_pcoq b = @@ -691,13 +677,11 @@ let _ = optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } -let impargs = if !Options.v7 then "Implicits" else "Implicit" - let _ = declare_bool_option - { optsync = false; (* synchronisation is in Impargs *) + { optsync = true; optname = "strict implicit arguments"; - optkey = (SecondaryTable ("Strict",impargs)); + optkey = (SecondaryTable ("Strict","Implicit")); optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } @@ -705,7 +689,7 @@ let _ = declare_bool_option { optsync = true; optname = "contextual implicit arguments"; - optkey = (SecondaryTable ("Contextual",impargs)); + optkey = (SecondaryTable ("Contextual","Implicit")); optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } @@ -721,7 +705,7 @@ let _ = declare_bool_option { optsync = true; optname = "implicit arguments printing"; - optkey = (SecondaryTable ("Printing",impargs)); + optkey = (SecondaryTable ("Printing","Implicit")); optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } @@ -737,7 +721,7 @@ let _ = declare_bool_option { optsync = true; optname = "notations printing"; - optkey = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations")); + optkey = (SecondaryTable ("Printing","Notations")); optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } @@ -750,6 +734,30 @@ let _ = optwrite = (fun b -> Options.raw_print := b) } let _ = + declare_bool_option + { optsync = true; + optname = "use of virtual machine inside the kernel"; + optkey = (SecondaryTable ("Virtual","Machine")); + optread = (fun () -> Vconv.use_vm ()); + optwrite = (fun b -> Vconv.set_use_vm b) } + +let _ = + declare_bool_option + { optsync = true; + optname = "use of boxed definitions"; + optkey = (SecondaryTable ("Boxed","Definitions")); + optread = Options.boxed_definitions; + optwrite = (fun b -> Options.set_boxed_definitions b) } + +let _ = + declare_bool_option + { optsync = true; + optname = "use of boxed values"; + optkey = (SecondaryTable ("Boxed","Values")); + optread = (fun _ -> not (Vm.transp_values ())); + optwrite = (fun b -> Vm.set_transp_values (not b)) } + +let _ = declare_int_option { optsync=false; optkey=PrimaryTable("Undo"); @@ -784,11 +792,11 @@ let _ = let vernac_set_opacity opaq locqid = match Nametab.global locqid with | ConstRef sp -> - if opaq then Tacred.set_opaque_const sp - else Tacred.set_transparent_const sp + if opaq then set_opaque_const sp + else set_transparent_const sp | VarRef id -> - if opaq then Tacred.set_opaque_var id - else Tacred.set_transparent_var id + if opaq then set_opaque_var id + else set_transparent_var id | _ -> error "cannot set an inductive type or a constructor as transparent" let vernac_set_option key = function @@ -843,7 +851,7 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (out_some !pcoq).print_check j else msg (print_judgment env j) | Some r -> - let redfun = Tacred.reduction_of_redexp (interp_redexp env evmap r) in + let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in if !pcoq <> None then (out_some !pcoq).print_eval (redfun env evmap) env rc j else msg (print_eval redfun env j) @@ -859,7 +867,6 @@ let vernac_global_check c = let vernac_print = function | PrintTables -> print_tables () - | PrintLocalContext -> msg (print_local_context ()) | PrintFullContext -> msg (print_full_context_typ ()) | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) @@ -876,21 +883,25 @@ let vernac_print = function | PrintOpaqueName qid -> msg (print_opaque_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) | PrintClasses -> ppnl (Prettyp.print_classes()) + | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> ppnl (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) | PrintUniverses (Some s) -> dump_universes s | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid) | PrintHintGoal -> Auto.print_applicable_hint () | 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 (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm)) + pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr)) | PrintScope s -> - pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s) + pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) | PrintVisibility s -> - pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s) + pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) @@ -929,10 +940,11 @@ let vernac_search s r = let vernac_locate = function | LocateTerm qid -> msgnl (print_located_qualid qid) | LocateLibrary qid -> print_located_library qid + | LocateModule qid -> print_located_module qid | LocateFile f -> locate_file f | LocateNotation ntn -> - ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm) - (Metasyntax.standardise_locatable_notation ntn)) + ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr) + (Metasyntax.standardize_locatable_notation ntn)) (********************) (* Proof management *) @@ -942,7 +954,7 @@ let vernac_goal = function | Some c -> if not (refining()) then begin let unnamed_kind = Lemma (* Arbitrary *) in - start_proof_com None (IsGlobal (Proof unnamed_kind)) c (fun _ _ ->()); + start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->()); print_subgoals () end else error "repeated Goal not permitted in refining mode" @@ -979,6 +991,17 @@ let vernac_undo n = undo n; print_subgoals () +(* backtrack with [naborts] abort, then undo_todepth to [pnum], then + back-to state number [snum]. This allows to backtrack proofs and + state with one command (easier for proofgeneral). *) +let vernac_backtrack snum pnum naborts = + for i = 1 to naborts do vernac_abort None done; + undo_todepth pnum; + vernac_backto snum; + (* there may be no proof in progress, even if no abort *) + (try print_subgoals () with UserError _ -> ()) + + (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *) let vernac_focus = function | None -> traverse_nth_goal 1; print_subgoals () @@ -1005,10 +1028,10 @@ let apply_subproof f occ = f evc (Global.named_context()) pf let explain_proof occ = - msg (apply_subproof (Refiner.print_treescript true) occ) + msg (apply_subproof (print_treescript true) occ) let explain_tree occ = - msg (apply_subproof Refiner.print_proof occ) + msg (apply_subproof print_proof occ) let vernac_show = function | ShowGoal nopt -> @@ -1028,17 +1051,17 @@ let vernac_show = function | ShowProofNames -> msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names())) | ShowIntros all -> show_intro all + | ShowMatch id -> show_match id | ExplainProof occ -> explain_proof occ | ExplainTree occ -> explain_tree occ let vernac_check_guard () = let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and cursor = cursor_of_pftreestate pts in + let pf = proof_of_pftreestate pts in let (pfterm,_) = extract_open_pftreestate pts in let message = try - Inductiveops.control_only_guard (Evarutil.evar_env (goal_of_proof pf)) + Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf)) pfterm; (str "The condition holds up to here") with UserError(_,s) -> @@ -1049,100 +1072,19 @@ let vernac_check_guard () = let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) - -(**************************) -(* Not supported commands *) -(*** -let _ = - add "ResetSection" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> reset_section (string_of_id id)) - | _ -> bad_vernac_args "ResetSection") - -(* Modules *) - -let _ = - vinterp_add "BeginModule" - (function - | [VARG_IDENTIFIER id] -> - let s = string_of_id id in - let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in - let dir = extend_dirpath (Library.find_logical_path lpe) id in - fun () -> - Lib.start_module dir - | _ -> bad_vernac_args "BeginModule") - -let _ = - vinterp_add "WriteModule" - (function - | [VARG_IDENTIFIER id] -> - let mid = Lib.end_module id in - fun () -> let m = string_of_id id in Library.save_module_to mid m - | [VARG_IDENTIFIER id; VARG_STRING f] -> - let mid = Lib.end_module id in - fun () -> Library.save_module_to mid f - | _ -> bad_vernac_args "WriteModule") - -let _ = - vinterp_add "CLASS" - (function - | [VARG_STRING kind; VARG_QUALID qid] -> - let stre = - if kind = "LOCAL" then - make_strength_0() - else - Nametab.NeverDischarge - in - fun () -> - let ref = Nametab.global (dummy_loc, qid) in - Class.try_add_new_class ref stre; - if_verbose message - ((string_of_qualid qid) ^ " is now a class") - | _ -> bad_vernac_args "CLASS") - -(* Meta-syntax commands *) -let _ = - add "TOKEN" - (function - | [VARG_STRING s] -> (fun () -> Metasyntax.add_token_obj s) - | _ -> bad_vernac_args "TOKEN") -***) - -(* Search commands *) - -(*** -let _ = - add "Searchisos" - (function - | [VARG_CONSTR com] -> - (fun () -> - let env = Global.env() in - let c = constr_of_com Evd.empty env com in - let cc = nf_betaiota env Evd.empty c in - Searchisos.type_search cc) - | _ -> bad_vernac_args "Searchisos") -***) - let interp c = match c with (* Control (done in vernac) *) | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false - | (VernacV7only _ | VernacV8only _) -> assert false (* Syntax *) - | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel - | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al - | VernacGrammar (univ,al) -> vernac_grammar univ al - | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8 + | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e) + | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope sc -> vernac_open_close_scope sc | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl - | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc - | VernacDistfix (local,assoc,n,inf,qid,sc) -> - vernac_distfix local assoc n inf qid sc - | VernacNotation (local,c,infpl,mv8,sc) -> - vernac_notation local c infpl mv8 sc + | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc + | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc (* Gallina *) | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f @@ -1152,15 +1094,15 @@ let interp c = match c with | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,l) -> vernac_assumption stre l | VernacInductive (finite,l) -> vernac_inductive finite l - | VernacFixpoint l -> vernac_fixpoint l - | VernacCoFixpoint l -> vernac_cofixpoint l + | VernacFixpoint (l,b) -> vernac_fixpoint l b + | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b | VernacScheme l -> vernac_scheme l (* Modules *) - | VernacDeclareModule ((_,id),bl,mtyo,mexpro) -> - vernac_declare_module id bl mtyo mexpro - | VernacDefineModule ((_,id),bl,mtyo,mexpro) -> - vernac_define_module id bl mtyo mexpro + | VernacDeclareModule (export,(_,id),bl,mtyo) -> + vernac_declare_module export id bl mtyo + | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) -> + vernac_define_module export id bl mtyo mexpro | VernacDeclareModuleType ((_,id),bl,mtyo) -> vernac_declare_module_type id bl mtyo @@ -1196,6 +1138,7 @@ let interp c = match c with | VernacResetName id -> vernac_reset_name id | VernacResetInitial -> vernac_reset_initial () | VernacBack n -> vernac_back n + | VernacBackTo n -> vernac_backto n (* Commands *) | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l @@ -1226,6 +1169,7 @@ let interp c = match c with | VernacSuspend -> vernac_suspend () | VernacResume id -> vernac_resume id | VernacUndo n -> vernac_undo n + | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacGo g -> vernac_go g diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 89e0d708..a2bcd990 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.mli,v 1.16.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) +(*i $Id: vernacentries.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 382434dc..a00901a4 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,v 1.55.2.2 2005/01/21 17:14:10 herbelin Exp $ i*) +(*i $Id: vernacexpr.ml 7936 2006-01-28 18:36:54Z herbelin $ i*) open Util open Names @@ -34,7 +34,6 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference type printable = | PrintTables - | PrintLocalContext | PrintFullContext | PrintSectionContext of reference | PrintInspect of int @@ -49,13 +48,17 @@ type printable = | PrintOpaqueName of reference | PrintGraph | PrintClasses + | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr + | PrintCanonicalConversions | PrintUniverses of string option | PrintHint of reference | PrintHintGoal | PrintHintDbName of string + | PrintRewriteHintDbName of string | PrintHintDb + | PrintSetoids | PrintScopes | PrintScope of string | PrintVisibility of string option @@ -75,6 +78,7 @@ type searchable = type locatable = | LocateTerm of reference | LocateLibrary of reference + | LocateModule of reference | LocateFile of string | LocateNotation of notation @@ -94,6 +98,7 @@ type showable = | ShowTree | ShowProofNames | ShowIntros of bool + | ShowMatch of lident | ExplainProof of int list | ExplainTree of int list @@ -103,11 +108,11 @@ type comment = | CommentInt of int type hints = - | HintsResolve of (identifier option * constr_expr) list - | HintsImmediate of (identifier option * constr_expr) list - | HintsUnfold of (identifier option * reference) list - | HintsConstructors of identifier option * reference list - | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr + | HintsResolve of constr_expr list + | HintsImmediate of constr_expr list + | HintsUnfold of reference list + | HintsConstructors of reference list + | HintsExtern of int * constr_expr * raw_tactic_expr | HintsDestruct of identifier * int * (bool,unit) location * constr_expr * raw_tactic_expr @@ -152,7 +157,11 @@ type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option -type module_binder = lident list * module_type_ast +type module_binder = bool option * lident list * module_type_ast + +type grammar_production = + | VTerm of string + | VNonTerm of loc * string * Names.identifier option type proof_end = | Admitted @@ -166,25 +175,17 @@ type vernac_expr = | VernacVar of lident (* Syntax *) - | VernacGrammar of lstring * raw_grammar_entry list - | VernacTacticGrammar of - (lstring * (lstring * grammar_production list) * raw_tactic_expr) list - | VernacSyntax of lstring * raw_syntax_entry list - | VernacSyntaxExtension of locality_flag * - (lstring * syntax_modifier list) option - * (lstring * syntax_modifier list) option - | VernacDistfix of locality_flag * - grammar_associativity * precedence * lstring * lreference * - scope_name option + | VernacTacticNotation of int * grammar_production list * raw_tactic_expr + | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * lstring | VernacBindScope of scope_name * class_rawexpr list | VernacArgumentsScope of lreference * scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * - lreference * (lstring * syntax_modifier list) option * scope_name option + lreference * scope_name option | VernacNotation of - locality_flag * constr_expr * (lstring * syntax_modifier list) option * - (lstring * syntax_modifier list) option * scope_name option + locality_flag * constr_expr * (lstring * syntax_modifier list) * + scope_name option (* Gallina *) | VernacDefinition of definition_kind * lident * definition_expr * @@ -195,8 +196,8 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * simple_binder with_coercion list | VernacInductive of inductive_flag * inductive_expr list - | VernacFixpoint of (fixpoint_expr * decl_notation) list - | VernacCoFixpoint of cofixpoint_expr list + | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool + | VernacCoFixpoint of cofixpoint_expr list * bool | VernacScheme of (lident * bool * lreference * sort_expr) list (* Gallina extensions *) @@ -214,9 +215,9 @@ type vernac_expr = class_rawexpr * class_rawexpr (* Modules and Module Types *) - | VernacDeclareModule of lident * - module_binder list * (module_type_ast * bool) option * module_ast option - | VernacDefineModule of lident * + | VernacDeclareModule of bool option * lident * + module_binder list * (module_type_ast * bool) + | VernacDefineModule of bool option * lident * module_binder list * (module_type_ast * bool) option * module_ast option | VernacDeclareModuleType of lident * module_binder list * module_type_ast option @@ -241,6 +242,7 @@ type vernac_expr = | VernacResetName of lident | VernacResetInitial | VernacBack of int + | VernacBackTo of int (* Commands *) | VernacDeclareTacticDefinition of @@ -273,6 +275,7 @@ type vernac_expr = | VernacSuspend | VernacResume of lident option | VernacUndo of int + | VernacBacktrack of int*int*int | VernacFocus of int option | VernacUnfocus | VernacGo of goable @@ -283,10 +286,6 @@ type vernac_expr = (* Toplevel control *) | VernacToplevelControl of exn - (* For translation from V7 to V8 syntax *) - | VernacV8only of vernac_expr - | VernacV7only of vernac_expr - (* For extension *) | VernacExtend of string * raw_generic_argument list diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index c7846d71..98584bac 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacinterp.ml,v 1.17.8.1 2004/07/16 19:31:50 herbelin Exp $ *) +(* $Id: vernacinterp.ml 7732 2005-12-26 13:51:24Z herbelin $ *) open Pp open Util @@ -15,10 +15,7 @@ open Libnames open Himsg open Proof_type open Tacinterp -open Coqast open Vernacexpr -open Ast -open Extend let disable_drop e = if e <> Drop then e diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 86b80935..e0c34dc9 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacinterp.mli,v 1.11.10.1 2004/07/16 19:31:50 herbelin Exp $ i*) +(*i $Id: vernacinterp.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*i*) open Tacexpr diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 new file mode 100644 index 00000000..042ee5c8 --- /dev/null +++ b/toplevel/whelp.ml4 @@ -0,0 +1,209 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id: whelp.ml4 7837 2006-01-11 09:47:32Z herbelin $ *) + +open Options +open Pp +open Util +open System +open Names +open Term +open Environ +open Rawterm +open Libnames +open Nametab +open Termops +open Detyping +open Constrintern +open Dischargedhypsmap +open Command +open Pfedit +open Refiner +open Tacmach + +(* Coq interface to the Whelp query engine developed at + the University of Bologna *) + +let make_whelp_request req c = + "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req + +let b = Buffer.create 16 + +let url_char c = + if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or + '0' <= c & c <= '9' or c ='.' + then Buffer.add_char b c + else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) + +let url_string s = String.iter url_char s + +let rec url_list_with_sep sep f = function + | [] -> () + | [a] -> f a + | a::l -> f a; url_string sep; url_list_with_sep sep f l + +let url_id id = url_string (string_of_id id) + +let uri_of_dirpath dir = + url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir) + +let error_whelp_unknown_reference ref = + let qid = Nametab.shortest_qualid_of_global Idset.empty ref in + error ("Definitions of the current session not supported in Whelp: " ^ string_of_qualid qid) + +let uri_of_repr_kn ref (mp,dir,l) = + match mp with + | MPfile sl -> + uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl) + | _ -> + error_whelp_unknown_reference ref + +let url_paren f l = url_char '('; f l; url_char ')' +let url_bracket f l = url_char '['; f l; url_char ']' + +let whelp_of_rawsort = function + | RProp Null -> "Prop" + | RProp Pos -> "Set" + | RType _ -> "Type" + +let uri_int n = Buffer.add_string b (string_of_int n) + +let uri_of_ind_pointer l = + url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l + +let uri_of_global ref = + match ref with + | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)) + | ConstRef cst -> + uri_of_repr_kn ref (repr_con cst); url_string ".con" + | IndRef (kn,i) -> + uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1] + | ConstructRef ((kn,i),j) -> + uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1;j] + +let whelm_special = id_of_string "WHELM_ANON_VAR" + +let url_of_name = function + | Name id -> url_id id + | Anonymous -> url_id whelm_special (* No anon id in Whelp *) + +let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c + +let uri_params f = function + | [] -> () + | l -> url_string "\\subst"; + url_bracket (url_list_with_sep ";" (uri_of_binding f)) l + +let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) + +let section_parameters = function + | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) -> + get_discharged_hyp_names (sp_of_global (IndRef(induri,0))) + | RRef (_,(ConstRef cst as ref)) -> + get_discharged_hyp_names (sp_of_global ref) + | _ -> [] + +let merge vl al = + let rec aux acc = function + | ([],l) | (_,([] as l)) -> List.rev acc, l + | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al) + in aux [] (vl,al) + +let rec uri_of_constr c = + match c with + | RVar (_,id) -> url_id id + | RRef (_,ref) -> uri_of_global ref + | RHole _ | REvar _ -> url_string "?" + | RSort (_,s) -> url_string (whelp_of_rawsort s) + | _ -> url_paren (fun () -> match c with + | RApp (_,f,args) -> + let inst,rest = merge (section_parameters f) args in + uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; + url_list_with_sep " " uri_of_constr rest + | RLambda (_,na,ty,c) -> + url_string "\\lambda "; url_of_name na; url_string ":"; + uri_of_constr ty; url_string "."; uri_of_constr c + | RProd (_,Anonymous,ty,c) -> + uri_of_constr ty; url_string "\\to "; uri_of_constr c + | RProd (_,Name id,ty,c) -> + url_string "\\forall "; url_id id; url_string ":"; + uri_of_constr ty; url_string "."; uri_of_constr c + | RLetIn (_,na,b,c) -> + url_string "let "; url_of_name na; url_string "\\def "; + uri_of_constr b; url_string " in "; uri_of_constr c + | RCast (_,c,_,t) -> + uri_of_constr c; url_string ":"; uri_of_constr t + | RRec _ | RIf _ | RLetTuple _ | RCases _ -> + error "Whelp does not support pattern-matching and (co-)fixpoint" + | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ -> + anomaly "Written w/o parenthesis" + | RPatVar _ | RDynamic _ -> + anomaly "Found constructors not supported in constr") () + +let make_string f x = Buffer.reset b; f x; Buffer.contents b + +let send_whelp req s = + let url = make_whelp_request req s in + let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in + let _ = run_command (fun x -> x) print_string command in () + +let whelp_constr req c = + let c = detype false [whelm_special] [] c in + send_whelp req (make_string uri_of_constr c) + +let whelp_constr_expr req c = + let (sigma,env)= get_current_context () in + let _,c = interp_open_constr sigma env c in + whelp_constr req c + +let whelp_locate s = + send_whelp "locate" s + +let whelp_elim ind = + send_whelp "elim" (make_string uri_of_global (IndRef ind)) + +let locate_inductive r = + let (loc,qid) = qualid_of_reference r in + try match Syntax_def.locate_global qid with + | IndRef ind -> ind + | _ -> user_err_loc (loc,"",str "Inductive type expected") + with Not_found -> error_global_not_found_loc loc qid + +let on_goal f = + let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in + f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) + +type whelp_request = + | Locate of string + | Elim of inductive + | Constr of string * constr + +let whelp = function + | Locate s -> whelp_locate s + | Elim ind -> whelp_elim ind + | Constr (s,c) -> whelp_constr s c + +VERNAC ARGUMENT EXTEND whelp_constr_request +| [ "Match" ] -> [ "match" ] +| [ "Instance" ] -> [ "instance" ] +END + +VERNAC COMMAND EXTEND Whelp +| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] +| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] +| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] +END + +VERNAC COMMAND EXTEND WhelpHint +| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] +| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] +END diff --git a/toplevel/recordobj.mli b/toplevel/whelp.mli index 91550c34..f3f7408a 100755..100644 --- a/toplevel/recordobj.mli +++ b/toplevel/whelp.mli @@ -6,7 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordobj.mli,v 1.7.6.2 2005/01/21 17:18:33 herbelin Exp $ i*) +(*i $Id: whelp.mli 7837 2006-01-11 09:47:32Z herbelin $ i*) -val objdef_declare : Libnames.global_reference -> unit -val add_object_hook : Tacexpr.declaration_hook +(* Coq interface to the Whelp query engine developed at + the University of Bologna *) + +open Names +open Term +open Topconstr +open Environ + +type whelp_request = + | Locate of string + | Elim of inductive + | Constr of string * constr + +val whelp : whelp_request -> unit |