From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- interp/constrextern.ml | 74 +++++++++++++++---------- interp/constrextern.mli | 3 +- interp/constrintern.ml | 105 +++++++++++++++++------------------- interp/coqlib.ml | 11 ++-- interp/genarg.ml | 14 +++-- interp/genarg.mli | 141 ++++++++++++++++++++++++------------------------ interp/notation.ml | 8 +-- interp/reserve.ml | 10 ++-- interp/topconstr.ml | 48 ++++++++--------- interp/topconstr.mli | 12 ++--- 10 files changed, 217 insertions(+), 209 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 6442cb94..daa57b77 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 8675 2006-03-31 18:21:20Z herbelin $ *) +(* $Id: constrextern.ml 8831 2006-05-19 09:29:54Z herbelin $ *) (*i*) open Pp @@ -27,6 +27,7 @@ open Pattern open Nametab open Notation open Reserve +open Detyping (*i*) (* Translation from rawconstr to front constr *) @@ -259,7 +260,7 @@ let rec same_raw c d = (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> same_raw t1 t2; if al1 <> al2 then failwith "RCases"; - option_iter2(fun (_,i1,nl1) (_,i2,nl2) -> + option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) -> if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> List.iter2 same_patt pl1 pl2; @@ -622,6 +623,11 @@ let extern_optimal_prim_token scopes r r' = (**********************************************************************) (* mapping rawterms to constr_expr *) +let extern_rawsort = function + | RProp _ as s -> s + | RType (Some _) as s when !print_universes -> s + | RType _ -> RType None + let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try @@ -679,7 +685,7 @@ let rec extern inctx scopes vars r = let vars' = List.fold_right (name_fold Idset.add) (cases_predicate_names tml) vars in - let rtntypopt' = option_app (extern_typ scopes vars') rtntypopt in + let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na,tm with Anonymous, RVar (_,id) when @@ -689,26 +695,28 @@ let rec extern inctx scopes vars r = | Name id, RVar (_,id') when id=id' -> None | Name _, _ -> Some na in (sub_extern false scopes vars tm, - (na',option_app (fun (loc,ind,nal) -> + (na',option_map (fun (loc,ind,n,nal) -> + let params = list_tabulate + (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in let args = List.map (function | Anonymous -> RHole (dummy_loc,Evd.InternalHole) | Name id -> RVar (dummy_loc,id)) nal in - let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in + let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in (extern_typ scopes vars t)) x))) tml in let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in CCases (loc,rtntypopt',tml,eqns) | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, - (option_app (fun _ -> na) typopt, - option_app (extern_typ scopes (add_vname vars na)) typopt), + (option_map (fun _ -> na) typopt, + option_map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern false scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (option_app (fun _ -> na) typopt, - option_app (extern_typ scopes (add_vname vars na)) typopt), + (option_map (fun _ -> na) typopt, + option_map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars b1, sub_extern false scopes vars b2) | RRec (loc,fk,idv,blv,tyv,bv) -> @@ -737,12 +745,7 @@ let rec extern inctx scopes vars r = in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) - | RSort (loc,s) -> - let s = match s with - | RProp _ -> s - | RType (Some _) when !print_universes -> s - | RType _ -> RType None in - CSort (loc,s) + | RSort (loc,s) -> CSort (loc,extern_rawsort s) | RHole (loc,e) -> CHole loc @@ -870,9 +873,18 @@ let extern_type at_top env t = let r = Detyping.detype at_top avoid (names_of_rel_context env) t in extern_rawtype (vars_of_env env) r +let extern_sort s = extern_rawsort (detype_sort s) + (******************************************************************) (* Main translation function from pattern -> constr_expr *) +let it_destPLambda n c = + let rec aux n nal c = + if n=0 then (nal,c) else match c with + | PLambda (na,_,c) -> aux (n-1) (na::nal) c + | _ -> anomaly "it_destPLambda" in + aux n [] c + let rec raw_of_pat env = function | PRef ref -> RRef (loc,ref) | PVar id -> RVar (loc,id) @@ -897,20 +909,24 @@ let rec raw_of_pat env = function RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) | PLambda (na,t,c) -> RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) - | PCase ((_,cs),typopt,tm,[||]) -> - if typopt <> None then failwith "TODO: PCase to RCases"; - RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None, - [raw_of_pat env tm,(Anonymous,None)],[]) - | PCase ((Some ind,cs),typopt,tm,bv) -> - let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in - let mib,mip = lookup_mind_specif (Global.env()) ind in - let k = mip.Declarations.mind_nrealargs in - let nparams = mib.Declarations.mind_nparams in - let cstrnargs = mip.Declarations.mind_consnrealdecls in - Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env) - (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) - avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv - | PCase _ -> error "Unsupported case-analysis while printing pattern" + | PIf (c,b1,b2) -> + RIf (loc, raw_of_pat env c, (Anonymous,None), + raw_of_pat env b1, raw_of_pat env b2) + | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) -> + let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in + RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) + | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> + let brs = Array.to_list (Array.map (raw_of_pat env) bv) in + let brns = Array.to_list cstr_nargs in + (* ind is None only if no branch and no return type *) + let ind = out_some indo in + let mat = simple_cases_matrix_of_branches ind brns brs in + let indnames,rtn = + if p = PMeta None then (Anonymous,None),None + else + let nparams,n = out_some ind_nargs in + return_type_of_predicate ind nparams n (raw_of_pat env p) in + RCases (loc,rtn,[raw_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 1fc44250..ca145dd9 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: constrextern.mli 7837 2006-01-11 09:47:32Z herbelin $ i*) +(*i $Id: constrextern.mli 8831 2006-05-19 09:29:54Z herbelin $ i*) (*i*) open Util @@ -41,6 +41,7 @@ val extern_constr : bool -> env -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr val extern_reference : loc -> Idset.t -> global_reference -> reference val extern_type : bool -> env -> types -> constr_expr +val extern_sort : sorts -> rawsort (* Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6fcd9d7a..678fb87b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 8654 2006-03-22 15:36:58Z msozeau $ *) +(* $Id: constrintern.ml 8924 2006-06-08 17:49:01Z notin $ *) open Pp open Util @@ -22,6 +22,7 @@ open Cases open Topconstr open Nametab open Notation +open Inductiveops (* To interpret implicits and arg scopes of recursive variables in inductive types and recursive definitions *) @@ -38,8 +39,8 @@ let interning_grammar = ref false let for_grammar f x = interning_grammar := true; let a = f x in - interning_grammar := false; - a + interning_grammar := false; + a let variables_bind = ref false @@ -128,9 +129,9 @@ type coqdoc_state = Lexer.location_table * int * int let coqdoc_freeze () = let lt = Lexer.location_table() in let state = (lt,!token_number,!last_pos) in - token_number := 0; - last_pos := 0; - state + token_number := 0; + last_pos := 0; + state let coqdoc_unfreeze (lt,tn,lp) = Lexer.restore_location_table lt; @@ -138,21 +139,13 @@ let coqdoc_unfreeze (lt,tn,lp) = last_pos := lp let add_glob loc ref = -(*i - let sp = Nametab.sp_of_global (Global.env ()) ref in - let dir,_ = repr_path sp in - let rec find_module d = - try - let qid = let dir,id = split_dirpath d in make_qualid dir id in - let _ = Nametab.locate_loaded_library qid in d - with Not_found -> find_module (dirpath_prefix d) - in - let s = string_of_dirpath (find_module dir) in - i*) let sp = Nametab.sp_of_global ref in - let id = let _,id = repr_path sp in string_of_id id in - let dp = string_of_dirpath (Lib.library_part ref) in - dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id) + let lib_dp = Lib.library_part ref in + let mod_dp,id = repr_path sp in + let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in + let filepath = string_of_dirpath lib_dp in + let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in + dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname) let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) @@ -165,15 +158,15 @@ let dump_notation_location pos ((path,df),sc) = let rec next growing = let loc = Lexer.location_function !token_number in let (bp,_) = unloc loc in - if growing then if bp >= pos then loc else (incr token_number;next true) - else if bp = pos then loc - else if bp > pos then (decr token_number;next false) - else (incr token_number;next true) in + if growing then if bp >= pos then loc else (incr token_number;next true) + else if bp = pos then loc + else if bp > pos then (decr token_number;next false) + else (incr token_number;next true) in let loc = next (pos >= !last_pos) in - last_pos := pos; - let path = string_of_dirpath path in - let sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) + last_pos := pos; + let path = string_of_dirpath path in + let sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -390,11 +383,6 @@ let check_constructor_length env loc cstr pl pl0 = if n <> nargs && n <> nhyps (* i.e. with let's *) then error_wrong_numarg_constructor_loc loc env cstr nargs -let check_inductive_length env (loc,ind,nal) = - let n = Inductiveops.inductive_nargs env ind in - if n <> List.length nal then - error_wrong_numarg_inductive_loc loc env ind n - (* Manage multiple aliases *) (* [merge_aliases] returns the sets of all aliases encountered at this @@ -506,20 +494,20 @@ let find_constructor ref = try extended_locate qid with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in - match gref with - | SyntacticDef sp -> - let sdef = Syntax_def.search_syntactic_definition loc sp in - patt_of_rawterm loc sdef - | TrueGlobal r -> - let rec unf = function - | ConstRef cst -> - let v = Environ.constant_value (Global.env()) cst in - unf (global_of_constr v) - | ConstructRef c -> - if !dump then add_glob loc r; - c, [] - | _ -> raise Not_found - in unf r + match gref with + | SyntacticDef sp -> + let sdef = Syntax_def.search_syntactic_definition loc sp in + patt_of_rawterm loc sdef + | TrueGlobal r -> + let rec unf = function + | ConstRef cst -> + let v = Environ.constant_value (Global.env()) cst in + unf (global_of_constr v) + | ConstructRef c -> + if !dump then add_glob loc r; + c, [] + | _ -> raise Not_found + in unf r let find_pattern_variable = function | Ident (loc,id) -> id @@ -793,7 +781,7 @@ let internalise sigma globalenv env allow_soapp lvar c = RStructRec, List.fold_left intern_local_binder (env,[]) bl | CWfRec c -> - let before, after = list_chop (succ n) bl in + let before, after = list_chop (succ (out_some n)) bl in let ((ids',_,_),rafter) = List.fold_left intern_local_binder (env,[]) after in let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in @@ -887,21 +875,21 @@ let internalise sigma globalenv env allow_soapp lvar c = let (tm,ind),nal = intern_case_item env citm in (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal) tms ([],env) in - let rtnpo = option_app (intern_type env') rtnpo in + let rtnpo = option_map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in RCases (loc, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = option_app (intern_type env'') po in + let p' = option_map (intern_type env'') po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = option_app (intern_type env'') po in + let p' = option_map (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> RHole (loc, Evd.QuestionMark) @@ -958,18 +946,25 @@ let internalise sigma globalenv env allow_soapp lvar c = let tids = names_of_cases_indtype t in let tids = List.fold_right Idset.add tids Idset.empty in let t = intern_type (tids,None,scopes) t in - let (_,_,nal as indsign) = + let (_,_,_,nal as indsign) = match t with - | RRef (loc,IndRef ind) -> (loc,ind,[]) + | RRef (loc,IndRef ind) -> (loc,ind,0,[]) | RApp (loc,RRef (_,IndRef ind),l) -> + let nparams, nrealargs = inductive_nargs globalenv ind in + let nindargs = nparams + nrealargs in + if List.length l <> nindargs then + error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function | RHole _ -> Anonymous | RVar (_,id) -> Name id | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in - (loc,ind,nal) + let parnal,realnal = list_chop nparams nal in + if List.exists ((<>) Anonymous) parnal then + user_err_loc (loc,"", + str "The parameters of inductive type must be implicit"); + (loc,ind,nparams,realnal) | _ -> error_bad_inductive_type (loc_of_rawconstr t) in - check_inductive_length globalenv indsign; nal, Some indsign | None -> [], None in diff --git a/interp/coqlib.ml b/interp/coqlib.ml index afee83e8..79a217a1 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqlib.ml 8688 2006-04-07 15:08:12Z msozeau $ *) +(* $Id: coqlib.ml 8866 2006-05-28 16:21:04Z herbelin $ *) open Util open Pp @@ -152,12 +152,7 @@ type coq_sigma_data = { type 'a delayed = unit -> 'a -let build_sigma_set () = - { proj1 = init_constant ["Specif"] "projS1"; - proj2 = init_constant ["Specif"] "projS2"; - elim = init_constant ["Specif"] "sigS_rec"; - intro = init_constant ["Specif"] "existS"; - typ = init_constant ["Specif"] "sigS" } +let build_sigma_set () = anomaly "Use build_sigma_type" let build_sigma_type () = { proj1 = init_constant ["Specif"] "projT1"; @@ -257,7 +252,7 @@ let build_coq_ex () = Lazy.force coq_ex (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") -let coq_existS_ref = lazy (init_reference ["Specif"] "existS") +let coq_existS_ref = lazy (anomaly "use coq_existT_ref") let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_not_ref = lazy (init_reference ["Logic"] "not") let coq_False_ref = lazy (init_reference ["Logic"] "False") diff --git a/interp/genarg.ml b/interp/genarg.ml index 511cf88a..77ed1fe6 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: genarg.ml 7879 2006-01-16 13:58:09Z herbelin $ *) +(* $Id: genarg.ml 8926 2006-06-08 20:23:17Z herbelin $ *) open Pp open Util @@ -33,7 +33,6 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | TacticArgType of int | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType @@ -44,7 +43,6 @@ type argument_type = | PairArgType of argument_type * argument_type | ExtraArgType of string -type 'a or_var = ArgArg of 'a | ArgVar of identifier located type 'a and_short_name = 'a * identifier located option type rawconstr_and_expr = rawconstr * constr_expr option @@ -54,6 +52,10 @@ type ('a,'b) generic_argument = argument_type * Obj.t let dyntab = ref ([] : string list) +type rlevel = constr_expr +type glevel = rawconstr_and_expr +type tlevel = constr + type ('a,'b,'c) abstract_argument_type = argument_type let create_arg s = @@ -142,10 +144,6 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType -let rawwit_tactic n = TacticArgType n -let globwit_tactic n = TacticArgType n -let wit_tactic n = TacticArgType n - let rawwit_open_constr_gen b = OpenConstrArgType b let globwit_open_constr_gen b = OpenConstrArgType b let wit_open_constr_gen b = OpenConstrArgType b @@ -220,7 +218,7 @@ let app_list1 f = function let app_opt f = function | (OptArgType t as u, l) -> let o = Obj.magic l in - (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o)) + (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o)) | _ -> failwith "Genarg: not an opt" let app_pair f1 f2 = function diff --git a/interp/genarg.mli b/interp/genarg.mli index 99de4ca4..37b30927 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: genarg.mli 7879 2006-01-16 13:58:09Z herbelin $ i*) +(*i $Id: genarg.mli 8926 2006-06-08 20:23:17Z herbelin $ i*) open Util open Names @@ -16,7 +16,6 @@ open Rawterm open Topconstr open Term -type 'a or_var = ArgArg of 'a | ArgVar of identifier located type 'a and_short_name = 'a * identifier located option (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) @@ -73,7 +72,6 @@ RefArgType reference global_reference ConstrArgType constr_expr constr ConstrMayEvalArgType constr_expr may_eval constr QuantHypArgType quantified_hypothesis quantified_hypothesis -TacticArgType raw_tactic_expr tactic OpenConstrArgType constr_expr open_constr ConstrBindingsArgType constr_expr with_bindings constr with_bindings List0ArgType of argument_type @@ -83,88 +81,94 @@ ExtraArgType of string '_a '_b \end{verbatim} *) -type ('a,'co,'ta) abstract_argument_type +(* All of [rlevel], [glevel] and [tlevel] must be non convertible + to ensure the injectivity of the type inference from type + [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type] + is injective; this guarantees that, for 'b fixed, the type of + out_gen is monomorphic over 'a, hence type-safe +*) -val rawwit_bool : (bool,'co,'ta) abstract_argument_type -val globwit_bool : (bool,'co,'ta) abstract_argument_type -val wit_bool : (bool,'co,'ta) abstract_argument_type +type rlevel = constr_expr +type glevel = rawconstr_and_expr +type tlevel = constr + +type ('a,'co,'ta) abstract_argument_type -val rawwit_int : (int,'co,'ta) abstract_argument_type -val globwit_int : (int,'co,'ta) abstract_argument_type -val wit_int : (int,'co,'ta) abstract_argument_type +val rawwit_bool : (bool,rlevel,'ta) abstract_argument_type +val globwit_bool : (bool,glevel,'ta) abstract_argument_type +val wit_bool : (bool,tlevel,'ta) abstract_argument_type -val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type -val globwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type -val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type +val rawwit_int : (int,rlevel,'ta) abstract_argument_type +val globwit_int : (int,glevel,'ta) abstract_argument_type +val wit_int : (int,tlevel,'ta) abstract_argument_type -val rawwit_string : (string,'co,'ta) abstract_argument_type -val globwit_string : (string,'co,'ta) abstract_argument_type -val wit_string : (string,'co,'ta) abstract_argument_type +val rawwit_int_or_var : (int or_var,rlevel,'ta) abstract_argument_type +val globwit_int_or_var : (int or_var,glevel,'ta) abstract_argument_type +val wit_int_or_var : (int or_var,tlevel,'ta) abstract_argument_type -val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type -val globwit_pre_ident : (string,'co,'ta) abstract_argument_type -val wit_pre_ident : (string,'co,'ta) abstract_argument_type +val rawwit_string : (string,rlevel,'ta) abstract_argument_type +val globwit_string : (string,glevel,'ta) abstract_argument_type +val wit_string : (string,tlevel,'ta) abstract_argument_type -val rawwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type -val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type -val wit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type +val rawwit_pre_ident : (string,rlevel,'ta) abstract_argument_type +val globwit_pre_ident : (string,glevel,'ta) abstract_argument_type +val wit_pre_ident : (string,tlevel,'ta) abstract_argument_type -val rawwit_ident : (identifier,'co,'ta) abstract_argument_type -val globwit_ident : (identifier,'co,'ta) abstract_argument_type -val wit_ident : (identifier,'co,'ta) abstract_argument_type +val rawwit_intro_pattern : (intro_pattern_expr,rlevel,'ta) abstract_argument_type +val globwit_intro_pattern : (intro_pattern_expr,glevel,'ta) abstract_argument_type +val wit_intro_pattern : (intro_pattern_expr,tlevel,'ta) abstract_argument_type -val rawwit_var : (identifier located,'co,'ta) abstract_argument_type -val globwit_var : (identifier located,'co,'ta) abstract_argument_type -val wit_var : (identifier,'co,'ta) abstract_argument_type +val rawwit_ident : (identifier,rlevel,'ta) abstract_argument_type +val globwit_ident : (identifier,glevel,'ta) abstract_argument_type +val wit_ident : (identifier,tlevel,'ta) abstract_argument_type -val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type -val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type -val wit_ref : (global_reference,constr,'ta) abstract_argument_type +val rawwit_var : (identifier located,rlevel,'ta) abstract_argument_type +val globwit_var : (identifier located,glevel,'ta) abstract_argument_type +val wit_var : (identifier,tlevel,'ta) abstract_argument_type -val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type -val globwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type -val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type +val rawwit_ref : (reference,rlevel,'ta) abstract_argument_type +val globwit_ref : (global_reference located or_var,glevel,'ta) abstract_argument_type +val wit_ref : (global_reference,tlevel,'ta) abstract_argument_type -val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type -val globwit_sort : (rawsort,rawconstr_and_expr,'ta) abstract_argument_type -val wit_sort : (sorts,constr,'ta) abstract_argument_type +val rawwit_quant_hyp : (quantified_hypothesis,rlevel,'ta) abstract_argument_type +val globwit_quant_hyp : (quantified_hypothesis,glevel,'ta) abstract_argument_type +val wit_quant_hyp : (quantified_hypothesis,tlevel,'ta) abstract_argument_type -val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type -val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type -val wit_constr : (constr,constr,'ta) abstract_argument_type +val rawwit_sort : (rawsort,rlevel,'ta) abstract_argument_type +val globwit_sort : (rawsort,glevel,'ta) abstract_argument_type +val wit_sort : (sorts,tlevel,'ta) abstract_argument_type -val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) abstract_argument_type -val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type -val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type +val rawwit_constr : (constr_expr,rlevel,'ta) abstract_argument_type +val globwit_constr : (rawconstr_and_expr,glevel,'ta) abstract_argument_type +val wit_constr : (constr,tlevel,'ta) abstract_argument_type -val rawwit_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type -val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type -val wit_open_constr_gen : bool -> (open_constr,constr,'ta) abstract_argument_type +val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel,'ta) abstract_argument_type +val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel,'ta) abstract_argument_type +val wit_constr_may_eval : (constr,tlevel,'ta) abstract_argument_type -val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type -val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type -val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type +val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel,'ta) abstract_argument_type +val globwit_open_constr_gen : bool -> (open_rawconstr,glevel,'ta) abstract_argument_type +val wit_open_constr_gen : bool -> (open_constr,tlevel,'ta) abstract_argument_type -val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type -val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type -val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type +val rawwit_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type +val globwit_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type +val wit_open_constr : (open_constr,tlevel,'ta) abstract_argument_type -val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type -val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type -val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type +val rawwit_casted_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type +val globwit_casted_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type +val wit_casted_open_constr : (open_constr,tlevel,'ta) abstract_argument_type -val rawwit_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type -val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type -val wit_bindings : (constr bindings,constr,'ta) abstract_argument_type +val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel,'ta) abstract_argument_type +val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel,'ta) abstract_argument_type +val wit_constr_with_bindings : (constr with_bindings,tlevel,'ta) abstract_argument_type -val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type -val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type -val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type +val rawwit_bindings : (constr_expr bindings,rlevel,'ta) abstract_argument_type +val globwit_bindings : (rawconstr_and_expr bindings,glevel,'ta) abstract_argument_type +val wit_bindings : (constr bindings,tlevel,'ta) abstract_argument_type -(* TODO: transformer tactic en extra arg *) -val rawwit_tactic : int -> ('ta,constr_expr,'ta) abstract_argument_type -val globwit_tactic : int -> ('ta,rawconstr_and_expr,'ta) abstract_argument_type -val wit_tactic : int -> ('ta,constr,'ta) abstract_argument_type +val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract_argument_type +val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type +val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type val wit_list0 : ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type @@ -217,9 +221,9 @@ val app_pair : polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel de create *) val create_arg : string -> - ('a,'co,'ta) abstract_argument_type - * ('globa,'globco,'globta) abstract_argument_type - * ('rawa,'rawco,'rawta) abstract_argument_type + ('a,tlevel,'ta) abstract_argument_type + * ('globa,glevel,'globta) abstract_argument_type + * ('rawa,rlevel,'rawta) abstract_argument_type val exists_argtype : string -> bool @@ -239,7 +243,6 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | TacticArgType of int | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType diff --git a/interp/notation.ml b/interp/notation.ml index cb996dfe..7e101784 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 7984 2006-02-04 20:14:55Z herbelin $ *) +(* $Id: notation.ml 8752 2006-04-27 19:37:33Z herbelin $ *) (*i*) open Util @@ -234,12 +234,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x)) let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p) - (patl, (fun r -> option_app mkNumeral (uninterp r)), inpat) + (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat) let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p) - (patl, (fun r -> option_app mkString (uninterp r)), inpat) + (patl, (fun r -> option_map mkString (uninterp r)), inpat) let check_required_module loc sc (sp,d) = try let _ = Nametab.absolute_reference sp in () @@ -389,7 +389,7 @@ let uninterp_prim_token_cases_pattern c = let availability_of_prim_token printer_scope scopes = let f scope = Hashtbl.mem prim_token_interpreter_tab scope in - option_app snd (find_without_delimiters f (Some printer_scope,None) scopes) + option_map snd (find_without_delimiters f (Some printer_scope,None) scopes) (* Miscellaneous *) diff --git a/interp/reserve.ml b/interp/reserve.ml index 476fd7e6..aee981bd 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reserve.ml 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: reserve.ml 8752 2006-04-27 19:37:33Z herbelin $ i*) (* Reserved names *) @@ -59,17 +59,17 @@ let rec unloc = function | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) | RCases (_,rtntypopt,tml,pl) -> RCases (dummy_loc, - (option_app unloc rtntypopt), + (option_map unloc rtntypopt), List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) | RLetTuple (_,nal,(na,po),b,c) -> - RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c) + RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c) | RIf (_,c,(na,po),b1,b2) -> - RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2) + RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2) | RRec (_,fk,idl,bl,tyl,bv) -> RRec (dummy_loc,fk,idl, Array.map (List.map - (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty))) + (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty))) bl, Array.map unloc tyl, Array.map unloc bv) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 82f74f40..f7256026 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: topconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: topconstr.ml 8875 2006-05-29 19:59:11Z msozeau $ *) (*i*) open Pp @@ -38,14 +38,14 @@ type aconstr = | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr | ACases of aconstr option * - (aconstr * (name * (inductive * name list) option)) list * + (aconstr * (name * (inductive * int * name list) option)) list * (identifier list * cases_pattern list * aconstr) list | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * cast_kind * aconstr + | ACast of aconstr * cast_type * aconstr let name_app f e = function | Name id -> let (id, e) = f id e in (e, Name id) @@ -76,25 +76,25 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None - | Some (ind,nal) -> + | Some (ind,npar,nal) -> let e',nal' = List.fold_right (fun na (e',nal) -> let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in - e',Some (loc,ind,nal') in + e',Some (loc,ind,npar,nal') in let e',na' = name_app g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in let eqnl' = List.map (fun (idl,pat,rhs) -> let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in - RCases (loc,option_app (f e') rtntypopt,tml',eqnl') + RCases (loc,option_map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> let e,nal = list_fold_map (name_app g) e nal in let e,na = name_app g e na in - RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c) + RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c) | AIf (c,(na,po),b1,b2) -> let e,na = name_app g e na in - RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2) - | ACast (c,k,t) -> RCast (loc,f e c,k,f e t) + RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2) + | ACast (c,k,t) -> RCast (loc,f e c, k,f e t) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) | APatVar n -> RPatVar (loc,(false,n)) @@ -182,20 +182,20 @@ let aconstr_and_vars_of_rawconstr a = let f (_,idl,pat,rhs) = found := idl@(!found); (idl,pat,aux rhs) in - ACases (option_app aux rtntypopt, + ACases (option_map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; option_iter - (fun (_,_,nl) -> List.iter (add_name found) nl) x; - (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml, + (fun (_,_,_,nl) -> List.iter (add_name found) nl) x; + (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml, List.map f eqnl) | RLetTuple (loc,nal,(na,po),b,c) -> add_name found na; List.iter (add_name found) nal; - ALetTuple (nal,(na,option_app aux po),aux b,aux c) + ALetTuple (nal,(na,option_map aux po),aux b,aux c) | RIf (loc,c,(na,po),b1,b2) -> add_name found na; - AIf (aux c,(na,option_app aux po),aux b1,aux b2) + AIf (aux c,(na,option_map aux po),aux b1,aux b2) | RCast (_,c,k,t) -> ACast (aux c,k,aux t) | RSort (_,s) -> ASort s | RHole (_,w) -> AHole w @@ -289,9 +289,9 @@ let rec subst_aconstr subst bound raw = and rl' = list_smartmap (fun (a,(n,signopt) as x) -> let a' = subst_aconstr subst bound a in - let signopt' = option_app (fun ((indkn,i),nal as z) -> + let signopt' = option_map (fun ((indkn,i),n,nal as z) -> let indkn' = subst_kn subst indkn in - if indkn == indkn' then z else ((indkn',i),nal)) signopt in + if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl and branches' = list_smartmap @@ -341,7 +341,7 @@ let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) (* Pattern-matching rawconstr and aconstr *) let abstract_return_type_context pi mklam tml rtno = - option_app (fun rtn -> + option_map (fun rtn -> let nal = List.flatten (List.map (fun (_,(na,t)) -> match t with Some x -> (pi x)@[na] | None -> [na]) tml) in @@ -349,11 +349,11 @@ let abstract_return_type_context pi mklam tml rtno = rtno let abstract_return_type_context_rawconstr = - abstract_return_type_context pi3 + abstract_return_type_context (fun (_,_,_,nal) -> nal) (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c)) let abstract_return_type_context_aconstr = - abstract_return_type_context snd + abstract_return_type_context pi3 (fun na c -> ALambda(na,AHole Evd.InternalHole,c)) let rec adjust_scopes = function @@ -524,7 +524,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * cast_kind * constr_expr + | CCast of loc * constr_expr * cast_type * constr_expr | CNotation of loc * notation * constr_expr list | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr @@ -532,7 +532,7 @@ type constr_expr = and fixpoint_expr = - identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr + identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr and local_binder = | LocalRawDef of name located * constr_expr @@ -718,15 +718,15 @@ let map_constr_expr_with_binders f g e = function indnal (option_fold_right (name_fold g) na e)) a e in - CCases (loc,option_app (f e') rtnpo, + CCases (loc,option_map (f e') rtnpo, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> let e' = List.fold_right (name_fold g) nal e in let e'' = option_fold_right (name_fold g) ona e in - CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c) + CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c) | CIf (loc,c,(ona,po),b1,b2) -> let e' = option_fold_right (name_fold g) ona e in - CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2) + CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2) | CFix (loc,id,dl) -> CFix (loc,id,List.map (fun (id,n,bl,t,d) -> let (e',bl') = map_local_binders f g e bl in diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 2f4f667d..8305ea54 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: topconstr.mli 8624 2006-03-13 17:38:17Z msozeau $ i*) +(*i $Id: topconstr.mli 8875 2006-05-29 19:59:11Z msozeau $ i*) (*i*) open Pp @@ -34,14 +34,14 @@ type aconstr = | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr | ACases of aconstr option * - (aconstr * (name * (inductive * name list) option)) list * + (aconstr * (name * (inductive * int * name list) option)) list * (identifier list * cases_pattern list * aconstr) list | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * cast_kind * aconstr + | ACast of aconstr * cast_type * aconstr val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> @@ -107,14 +107,14 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * cast_kind * constr_expr + | CCast of loc * constr_expr * cast_type * constr_expr | CNotation of loc * notation * constr_expr list | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t and fixpoint_expr = - identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr + identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr and cofixpoint_expr = identifier * local_binder list * constr_expr * constr_expr @@ -143,7 +143,7 @@ val names_of_cases_indtype : constr_expr -> identifier list val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr +val mkCastC : constr_expr * cast_type * constr_expr -> constr_expr val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * constr_expr * constr_expr -> constr_expr -- cgit v1.2.3