diff options
41 files changed, 330 insertions, 751 deletions
@@ -1031,14 +1031,6 @@ toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \ library/lib.cmx library/libobject.cmx library/library.cmx \ parsing/pcoq.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \ toplevel/metasyntax.cmi -toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \ - parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi lib/util.cmi -toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \ - parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/type_errors.cmx lib/util.cmx toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \ lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \ toplevel/protectedtoplevel.cmi diff --git a/.depend.camlp4 b/.depend.camlp4 index 9804b6c895..2e98cf9417 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -1,40 +1,8 @@ -parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ - parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi -parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ - parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi -parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ - toplevel/vernac.cmi -parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ - toplevel/vernac.cmx -parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx -parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx -parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \ - lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ - parsing/g_minicoq.cmi -parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \ - lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ - parsing/g_minicoq.cmi -parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx -parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ - lib/pp.cmi lib/util.cmi -parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ - lib/pp.cmx lib/util.cmx -parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi -parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx -parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ - lib/util.cmi parsing/pcoq.cmi -parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ - lib/util.cmx parsing/pcoq.cmi -parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi -scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi -scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx -toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ - lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi toplevel/mltop.cmi -toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ - lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx toplevel/mltop.cmi +parsing/extend.cmo: parsing/extend.cmi +parsing/extend.cmx: parsing/extend.cmi +parsing/g_minicoq.cmo: parsing/g_minicoq.cmi +parsing/g_minicoq.cmx: parsing/g_minicoq.cmi +parsing/pcoq.cmo: parsing/pcoq.cmi +parsing/pcoq.cmx: parsing/pcoq.cmi +toplevel/mltop.cmo: toplevel/mltop.cmi +toplevel/mltop.cmx: toplevel/mltop.cmi @@ -22,3 +22,8 @@ maintenant celui associé au nom de la grammaire (vernac, tactic ou constr). Donc plus de piquants <:vernac:<...>> etc. Pour retourner de l'ast, il faut typer explicitement la grammaire avec Ast ou List (renommé d'ailleurs AstList). + +- AddPath -> Add Path; + Print LoadPath -> Print Path; + DelPath -> Remove Path; + Print Path -> Print Coercion Paths.
\ No newline at end of file diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 2418e1abe9..9085041d37 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -535,7 +535,6 @@ let polynom_unfold_tac = { r_beta = true; r_delta = (function | Const sp -> SectionPathSet.mem sp constants_to_unfold - | Abst sp -> SectionPathSet.mem sp constants_to_unfold | _ -> false); r_iota = true }) in diff --git a/kernel/closure.ml b/kernel/closure.ml index 948361690d..178e5a9de7 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -144,7 +144,7 @@ let const_value_cache info c = try Some (Hashtbl.find info.i_tab c) with Not_found -> - match const_abst_opt_value info.i_env info.i_evc c with + match const_evar_opt_value info.i_env info.i_evc c with | Some body -> let v = info.i_repr info body in Hashtbl.add info.i_tab c v; @@ -450,7 +450,6 @@ let rec norm_head info env t stack = (VAL(0, mkProd (x, cbv_norm_term info env t, cbv_norm_term info (subs_lift env) c)), stack) - | IsAbst (_,_) -> failwith "No longer implemented" (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak @@ -519,8 +518,8 @@ and apply_stack info t = function apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st | CASE (ty,br,ci,env,st) -> apply_stack info - (mkMutCaseA ci (cbv_norm_term info env ty) t - (Array.map (cbv_norm_term info env) br)) + (mkMutCase (ci, cbv_norm_term info env ty, t, + Array.map (cbv_norm_term info env) br)) st @@ -883,7 +882,7 @@ and whnf_frterm info ft = { norm = uf.norm; term = FLIFT(k, uf) } | FOP2 (Cast,f,_) -> whnf_frterm info f (* remove outer casts *) | FOPN (AppL,appl) -> whnf_apply info appl.(0) (array_tl appl) - | FOPN ((Const _ | Evar _ | Abst _) as op,vars) -> + | FOPN ((Const _ | Evar _) as op,vars) -> if red_under info.i_flags (DELTA op) then let cst = DOPN(op, Array.map term_of_freeze vars) in (match const_value_cache info cst with @@ -953,7 +952,7 @@ and whnf_term info env t = | DOP1 (op, nt) -> { norm = false; term = FOP1 (op, freeze env nt) } | DOP2 (Cast,ct,c) -> whnf_term info env ct (* remove outer casts *) | DOP2 (_,_,_) -> assert false (* Lambda|Prod made explicit *) - | DOPN ((AppL | Const _ | Evar _ | Abst _ | MutCase _) as op, ve) -> + | DOPN ((AppL | Const _ | Evar _ | MutCase _) as op, ve) -> whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) } | DOPN ((MutInd _ | MutConstruct _) as op,v) -> { norm = (v=[||]); term = FOPN (op, freeze_vect env v) } diff --git a/kernel/environ.ml b/kernel/environ.ml index 4909e4444f..604d0aea36 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -262,7 +262,7 @@ let hdchar env c = | IsCoFix (i,(_,ln,_)) -> let id = match List.nth ln i with Name id -> id | _ -> assert false in lowercase_first_char id - | IsMeta _|IsXtra _|IsAbst (_, _)|IsEvar _|IsMutCase (_, _, _, _) -> "y" + | IsMeta _|IsXtra _|IsEvar _|IsMutCase (_, _, _, _) -> "y" in hdrec 0 c @@ -311,7 +311,7 @@ let make_all_name_different env = env (* Abstractions. *) - +(* let evaluable_abst env = function | DOPN (Abst _,_) -> true | _ -> invalid_arg "evaluable_abst" @@ -324,7 +324,7 @@ let abst_value env = function | DOPN(Abst sp, args) -> contract_abstraction (lookup_abst sp env) args | _ -> invalid_arg "abst_value" - +*) let defined_constant env = function | DOPN (Const sp, _) -> is_defined (lookup_constant sp env) | _ -> invalid_arg "defined_constant" diff --git a/kernel/environ.mli b/kernel/environ.mli index b99410bd3b..4b483c7dd9 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -144,11 +144,11 @@ val it_mkNamedProd_or_LetIn : constr -> var_context -> constr val lambda_create : env -> constr * constr -> constr val prod_create : env -> constr * constr -> constr - +(* val translucent_abst : env -> constr -> bool val evaluable_abst : env -> constr -> bool val abst_value : env -> constr -> constr - +*) val defined_constant : env -> constr -> bool val evaluable_constant : env -> constr -> bool diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 627f0d45c1..9b1d9289a5 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -72,7 +72,7 @@ let existential_value sigma (n,args) = | Evar_empty -> anomaly "a defined existential with no body" -let const_abst_opt_value env sigma c = +let const_evar_opt_value env sigma c = match c with | DOPN(Const sp,_) -> if evaluable_constant env c then Some (constant_value env c) else None @@ -81,7 +81,5 @@ let const_abst_opt_value env sigma c = Some (existential_value sigma (ev,args)) else None - | DOPN(Abst sp,_) -> - if evaluable_abst env c then Some (abst_value env c) else None | _ -> invalid_arg "const_abst_opt_value" diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index d3454f1ccc..0d8c2a3039 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -27,4 +27,4 @@ val constant_type : env -> 'a evar_map -> constant -> typed_type val existential_value : 'a evar_map -> existential -> constr val existential_type : 'a evar_map -> existential -> constr -val const_abst_opt_value : env -> 'a evar_map -> constr -> constr option +val const_evar_opt_value : env -> 'a evar_map -> constr -> constr option diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f0f7945d6e..352e41e382 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -25,7 +25,7 @@ type 'a contextual_stack_reduction_function = type 'a stack_reduction_function = 'a contextual_stack_reduction_function type local_stack_reduction_function = constr -> constr list -> constr * constr list - +(* type stack = | EmptyStack | ConsStack of constr array * int * stack @@ -36,6 +36,15 @@ let decomp_stack = function Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s))) let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s) +*) + +type stack = constr list + +let decomp_stack = function + | [] -> None + | v :: s -> Some (v,s) + +let append_stack v s = v@s (*************************************) (*** Reduction Functions Operators ***) @@ -160,7 +169,6 @@ let red_product env sigma c = | IsConst (_,_) when evaluable_constant env x -> constant_value env x | IsEvar (ev,args) when Evd.is_defined sigma ev -> existential_value sigma (ev,args) - | IsAbst (_,_) when evaluable_abst env x -> abst_value env x | IsCast (c,_) -> redrec c | IsProd (x,a,b) -> mkProd (x, a, redrec b) | _ -> error "Term not reducible" @@ -182,12 +190,6 @@ let rec substlin env name n ol c = else ((n+1),ol,c) - | IsAbst (_,_) when path_of_abst c = name -> - if List.hd ol = n then - (n+1, List.tl ol, abst_value env c) - else - (n+1,ol,c) - (* INEFFICIENT: OPTIMIZE *) | IsAppL (c1,cl) -> List.fold_left @@ -236,14 +238,14 @@ let rec substlin env name n ol c = in let (n1,ol1,p') = substlin env name n ol p in (* ATTENTION ERREUR *) (match ol1 with (* si P pas affiche *) - | [] -> (n1,[],mkMutCaseA ci p' d llf) + | [] -> (n1,[],mkMutCase (ci, p', d, llf)) | _ -> let (n2,ol2,d') = substlin env name n1 ol1 d in (match ol2 with - | [] -> (n2,[],mkMutCaseA ci p' d' llf) + | [] -> (n2,[],mkMutCase (ci, p', d', llf)) | _ -> let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf) - in (n3,ol3,mkMutCase (ci, p', d', lf')))) + in (n3,ol3,mkMutCaseL (ci, p', d', lf')))) | IsCast (c1,c2) -> let (n1,ol1,c1') = substlin env name n ol c1 in @@ -260,14 +262,13 @@ let rec substlin env name n ol c = (warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ - |IsAbst (_, _)|IsEvar _|IsConst _ - |IsMutInd _|IsMutConstruct _) -> (n,ol,c) + |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c) let unfold env sigma name = let flag = (UNIFORM,{ r_beta = true; - r_delta = (fun op -> op=(Const name) or op=(Abst name)); + r_delta = (fun op -> op=(Const name)); r_iota = true }) in clos_norm_flags flag env sigma @@ -336,9 +337,9 @@ let beta_applist (c,l) = stacklam applist [] c l let whd_beta_stack x stack = let rec whrec (x, stack as s) = match x with | CLam (name,c1,c2) -> - (match stack with - | [] -> (x,[]) - | a1::rest -> stacklam whrec [a1] c2 rest) + (match decomp_stack stack with + | None -> (x,[]) + | Some (a1,rest) -> stacklam whrec [a1] c2 rest) | DOPN(AppL,cl) -> whrec (array_hd cl, array_app_tl cl stack) | DOP2(Cast,c,_) -> whrec (c, stack) @@ -362,15 +363,6 @@ let whd_const_stack namelist env sigma = else x,l - | (DOPN(Abst sp,_)) as c -> - if List.mem sp namelist then - if evaluable_abst env c then - whrec (abst_value env c) l - else - error "whd_const_stack" - else - x,l - | DOP2(Cast,c,_) -> whrec c l | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) | x -> x,l @@ -393,14 +385,9 @@ let whd_delta_stack env sigma = whrec (existential_value sigma (ev,args)) l else x,l - | (DOPN(Abst _,_)) as c -> - if evaluable_abst env c then - whrec (abst_value env c) l - else - x,l - | DOP2(Cast,c,_) -> whrec c l - | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) - | x -> x,l + | DOP2(Cast,c,_) -> whrec c l + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) + | x -> x,l in whrec @@ -420,19 +407,12 @@ let whd_betadelta_stack env sigma x l = whrec (existential_value sigma (ev,args), l) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) l - else - (x,l) -*) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,cl) -> whrec (f, cl@l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) | IsLambda (_,_,c) -> - (match l with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack l with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | x -> s in whrec (x, l) @@ -448,19 +428,12 @@ let whd_betaevar_stack env sigma x l = whrec (existential_value sigma (ev,args), l) else s -(* - | DOPN(Abst _,_) -> - if translucent_abst env x then - whrec (abst_value env x) l - else - (x,l) -*) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,cl) -> whrec (f, cl@l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) | IsLambda (_,_,c) -> - (match l with - | [] -> (x,l) - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack l with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | x -> s in whrec (x, l) @@ -480,18 +453,11 @@ let whd_betadeltaeta_stack env sigma x l = whrec (existential_value sigma (ev,args), l) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) l - else - (x,l) -*) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,cl) -> whrec (f, cl@l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) | IsLambda (_,_,c) -> - (match l with - | [] -> + (match decomp_stack l with + | None -> (match applist (whrec (c, [])) with | DOPN(AppL,cl) -> let napp = (Array.length cl) -1 in @@ -502,7 +468,7 @@ let whd_betadeltaeta_stack env sigma x l = in if noccurn 1 u then (pop u,[]) else s | _ -> s) | _ -> s) - | (a::m) -> stacklam whrec [a] c m) + | Some (a,m) -> stacklam whrec [a] c m) | x -> s in whrec (x, l) @@ -545,7 +511,7 @@ let reduce_mind_case mia = applist (mia.mlf.(i-1),real_cargs) | DOPN(CoFix _,_) as cofix -> let cofix_def = contract_cofix (destCoFix cofix) in - mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf + mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce @@ -595,18 +561,18 @@ let whd_betaiota_stack x l = let rec whrec (x,stack as s) = match kind_of_term x with | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | a::m -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in if reducible_mind_case c then whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with @@ -626,26 +592,19 @@ let whd_betaiotaevar_stack env sigma x l = whrec (existential_value sigma (ev,args), stack) else s -(* - | DOPN(Abst _,_) -> - if translucent_abst env x then - whrec (abst_value env x) stack - else - (x,stack) -*) | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in if reducible_mind_case c then whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' @@ -670,26 +629,19 @@ let whd_betadeltaiota_stack env sigma x l = whrec (existential_value sigma (ev,args), stack) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) stack - else - (x,stack) -*) | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in if reducible_mind_case c then whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' @@ -715,18 +667,11 @@ let whd_betadeltaiotaeta_stack env sigma x l = whrec (existential_value sigma (ev,args), stack) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) stack - else - (x,stack) -*) | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> + (match decomp_stack stack with + | None -> (match applist (whrec (c, [])) with | DOPN(AppL,cl) -> let napp = (Array.length cl) -1 in @@ -737,7 +682,7 @@ let whd_betadeltaiotaeta_stack env sigma x l = in if noccurn 1 u then (pop u,[]) else s | _ -> s) | _ -> s) - | (a::m) -> stacklam whrec [a] c m) + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in @@ -745,7 +690,7 @@ let whd_betadeltaiotaeta_stack env sigma x l = whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' @@ -882,31 +827,14 @@ and eqappr cv_pb infos appr1 appr2 = (lft1, fhnf_apply infos n1 def1 v1) appr2 | None -> fun _ -> raise NotConvertible)) - | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) -> - convert_or - (* try first intensional equality *) - (bool_and_convert (sp1 = sp2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2))) - (* else expand the second occurrence (arbitrary heuristic) *) - (match search_frozen_cst infos (Abst sp2) al2 with - | Some def2 -> - eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) - | None -> (match search_frozen_cst infos (Abst sp1) al2 with - | Some def1 -> eqappr cv_pb infos - (lft1, fhnf_apply infos n1 def1 v1) appr2 - | None -> fun _ -> raise NotConvertible)) - (* only one constant, existential or abstraction *) - | (FOPN((Const _ | Evar _ | Abst _) as op,al1), _) -> + | (FOPN((Const _ | Evar _) as op,al1), _) -> (match search_frozen_cst infos op al1 with | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 | None -> fun _ -> raise NotConvertible) - | (_, FOPN((Const _ | Evar _ | Abst _) as op,al2)) -> + | (_, FOPN((Const _ | Evar _) as op,al2)) -> (match search_frozen_cst infos op al2 with | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) @@ -1125,7 +1053,7 @@ let rec apprec env sigma c stack = match kind_of_term t with | IsMutCase (ci,p,d,lf) -> let (cr,crargs) = whd_betadeltaiota_stack env sigma d [] in - let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in + let rslt = mkMutCase (ci, p, applist(cr,crargs), lf) in if reducible_mind_case cr then apprec env sigma rslt stack else @@ -1152,9 +1080,9 @@ let whd_programs_stack env sigma x l = match kind_of_term x with | IsAppL (f,[c]) -> if occur_meta c then s else whrec (f, c::stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> if occur_meta d then s @@ -1164,7 +1092,7 @@ let whd_programs_stack env sigma x l = whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6b97c63ac6..68cd846b75 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -50,12 +50,6 @@ let rec execute mf env cstr = | IsVar id -> (make_judge cstr (lookup_var_type id env), cst0) - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - (* ATTENTION : faudra faire le typage du contexte des Const, MutInd et MutConstructsi un jour cela devient des constructions arbitraires et non plus des variables *) diff --git a/kernel/term.ml b/kernel/term.ml index 40feeaab12..1933483901 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -26,7 +26,7 @@ type 'a oper = (* DOP2 *) | Cast | Prod | Lambda (* DOPN *) - | AppL | Const of section_path | Abst of section_path + | AppL | Const of section_path | Evar of existential_key | MutInd of inductive_path | MutConstruct of constructor_path @@ -505,9 +505,6 @@ let mkConst (sp,a) = DOPN (Const sp, a) (* Constructs an existential variable *) let mkEvar (n,a) = DOPN (Evar n, a) -(* Constructs an abstract object *) -let mkAbst sp a = DOPN (Abst sp, a) - (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l) @@ -518,9 +515,9 @@ let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l) let mkMutConstruct (cstr_sp,l) = DOPN (MutConstruct cstr_sp,l) (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -let mkMutCase (ci, p, c, ac) = +let mkMutCaseL (ci, p, c, ac) = DOPN (MutCase ci, Array.append [|p;c|] (Array.of_list ac)) -let mkMutCaseA ci p c ac = +let mkMutCase (ci, p, c, ac) = DOPN (MutCase ci, Array.append [|p;c|] ac) (* If recindxs = [|i1,...in|] @@ -782,6 +779,7 @@ let num_of_evar = function | DOPN (Evar n, _) -> n | _ -> anomaly "num_of_evar called with bad args" +(* (* Destructs an abstract term *) let destAbst = function | DOPN (Abst sp, a) -> (sp, a) @@ -794,7 +792,7 @@ let path_of_abst = function let args_of_abst = function | DOPN(Abst _,args) -> args | _ -> anomaly "args_of_abst called with bad args" - +*) (* Destructs a (co)inductive type named sp *) let destMutInd = function | DOPN (MutInd ind_sp, l) -> (ind_sp,l) @@ -870,7 +868,6 @@ type 'ctxt reference = | RConst of section_path * 'ctxt | RInd of inductive_path * 'ctxt | RConstruct of constructor_path * 'ctxt - | RAbst of section_path | RVar of identifier | REVar of int * 'ctxt @@ -902,7 +899,6 @@ type kindOfTerm = | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr | IsAppL of constr * constr list - | IsAbst of section_path * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -932,7 +928,6 @@ let kind_of_term c = IsAppL (a.(0), List.tl (Array.to_list a)) | DOPN (Const sp, a) -> IsConst (sp,a) | DOPN (Evar sp, a) -> IsEvar (sp,a) - | DOPN (Abst sp, a) -> IsAbst (sp, a) | DOPN (MutInd ind_sp, l) -> IsMutInd (ind_sp,l) | DOPN (MutConstruct cstr_sp,l) -> IsMutConstruct (cstr_sp,l) | DOPN (MutCase ci,v) -> @@ -1709,7 +1704,6 @@ module Hoper = | XTRA s -> XTRA (hstr s) | Sort s -> Sort (hsort s) | Const sp -> Const (hsp sp) - | Abst sp -> Abst (hsp sp) | MutInd (sp,i) -> MutInd (hsp sp, i) | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j) | MutCase ci as t -> t (* TO DO: extract ind_sp *) @@ -1719,7 +1713,6 @@ module Hoper = | (XTRA s1, XTRA s2) -> s1==s2 | (Sort s1, Sort s2) -> s1==s2 | (Const sp1, Const sp2) -> sp1==sp2 - | (Abst sp1, Abst sp2) -> sp1==sp2 | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2 | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) -> sp1==sp2 & i1=i2 & j1=j2 @@ -1795,7 +1788,7 @@ type constr_operator = | OpSort of sorts | OpRel of int | OpVar of identifier | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpAppL | OpConst of section_path | OpAbst of section_path + | OpAppL | OpConst of section_path | OpEvar of existential_key | OpMutInd of inductive_path | OpMutConstruct of constructor_path @@ -1922,3 +1915,88 @@ let generic_fold_left f acc bl tl = | None -> f acc t | Some b -> f (f acc b) t) acc bl in Array.fold_left f acc tl + +let fold_constr f acc c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> acc + | IsCast (c,t) -> f (f acc c) t + | IsProd (_,t,c) -> f (f acc t) c + | IsLambda (_,t,c) -> f (f acc t) c + | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c + | IsAppL (c,l) -> List.fold_left f (f acc c) l + | IsEvar (_,l) -> Array.fold_left f acc l + | IsConst (_,l) -> Array.fold_left f acc l + | IsMutInd (_,l) -> Array.fold_left f acc l + | IsMutConstruct (_,l) -> Array.fold_left f acc l + | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl + | IsFix (_,(tl,_,bl)) -> Array.fold_left f (Array.fold_left f acc tl) bl + | IsCoFix (_,(tl,_,bl)) -> Array.fold_left f (Array.fold_left f acc tl) bl + +let fold_constr_with_binders g f n acc c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> acc + | IsCast (c,t) -> f n (f n acc c) t + | IsProd (_,t,c) -> f (g n) (f n acc t) c + | IsLambda (_,t,c) -> f (g n) (f n acc t) c + | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c + | IsAppL (c,l) -> List.fold_left (f n) (f n acc c) l + | IsEvar (_,l) -> Array.fold_left (f n) acc l + | IsConst (_,l) -> Array.fold_left (f n) acc l + | IsMutInd (_,l) -> Array.fold_left (f n) acc l + | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l + | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | IsFix (_,(tl,_,bl)) -> + let n' = iterate g (Array.length tl) n in + Array.fold_left (f n') (Array.fold_left (f n) acc tl) bl + | IsCoFix (_,(tl,_,bl)) -> + let n' = iterate g (Array.length tl) n in + Array.fold_left (f n') (Array.fold_left (f n) acc tl) bl + +let iter_constr_with_binders g f n c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> () + | IsCast (c,t) -> f n c; f n t + | IsProd (_,t,c) -> f n t; f (g n) c + | IsLambda (_,t,c) -> f n t; f (g n) c + | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c + | IsAppL (c,l) -> f n c; List.iter (f n) l + | IsEvar (_,l) -> Array.iter (f n) l + | IsConst (_,l) -> Array.iter (f n) l + | IsMutInd (_,l) -> Array.iter (f n) l + | IsMutConstruct (_,l) -> Array.iter (f n) l + | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl + | IsFix (_,(tl,_,bl)) -> + Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | IsCoFix (_,(tl,_,bl)) -> + Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + +let map_constr f c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsCast (c,t) -> mkCast (f c, f t) + | IsProd (na,t,c) -> mkProd (na, f t, f c) + | IsLambda (na,t,c) -> mkLambda (na, f t, f c) + | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) + | IsAppL (c,l) -> applist (f c, List.map f l) + | IsEvar (e,l) -> mkEvar (e, Array.map f l) + | IsConst (c,l) -> mkConst (c, Array.map f l) + | IsMutInd (c,l) -> mkMutInd (c, Array.map f l) + | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l) + | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl) + | IsFix (ln,(tl,lna,bl)) -> mkFix (ln,(Array.map f tl,lna,Array.map f bl)) + | IsCoFix(ln,(tl,lna,bl)) -> mkCoFix (ln,(Array.map f tl,lna,Array.map f bl)) + +let map_constr_with_binders g f l c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsCast (c,t) -> mkCast (f l c, f l t) + | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c) + | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) + | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) + | IsAppL (c,al) -> applist (f l c, List.map (f l) al) + | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) + | IsConst (c,al) -> mkConst (c, Array.map (f l) al) + | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) + | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) + | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) + | IsFix (ln,(tl,lna,bl)) -> + let l' = List.fold_right g lna l in + mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsCoFix(ln,(tl,lna,bl)) -> + let l' = List.fold_right g lna l in + mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) diff --git a/kernel/term.mli b/kernel/term.mli index 0eb1d645d7..e4e0e1df5c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -42,7 +42,7 @@ type 'a oper = | Meta of int | Sort of 'a | Cast | Prod | Lambda - | AppL | Const of section_path | Abst of section_path + | AppL | Const of section_path | Evar of existential_key | MutInd of inductive_path | MutConstruct of constructor_path @@ -104,7 +104,6 @@ type 'ctxt reference = | RConst of section_path * 'ctxt | RInd of inductive_path * 'ctxt | RConstruct of constructor_path * 'ctxt - | RAbst of section_path | RVar of identifier | REVar of int * 'ctxt @@ -136,7 +135,6 @@ type kindOfTerm = | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr | IsAppL of constr * constr list - | IsAbst of section_path * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -230,9 +228,6 @@ val mkConst : constant -> constr (* Constructs an existential variable *) val mkEvar : existential -> constr -(* Constructs an abstract object *) -val mkAbst : section_path -> constr array -> constr - (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) val mkMutInd : inductive -> constr @@ -243,8 +238,8 @@ val mkMutInd : inductive -> constr val mkMutConstruct : constructor -> constr (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -val mkMutCase : case_info * constr * constr * constr list -> constr -val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr +val mkMutCaseL : case_info * constr * constr * constr list -> constr +val mkMutCase : case_info * constr * constr * constr array -> constr (* If [recindxs = [|i1,...in|]] [typarray = [|t1,...tn|]] @@ -363,11 +358,12 @@ val args_of_const : constr -> constr array val destEvar : constr -> int * constr array val num_of_evar : constr -> int +(* (* Destructs an abstract term *) val destAbst : constr -> section_path * constr array val path_of_abst : constr -> section_path val args_of_abst : constr -> constr array - +*) (* Destructs a (co)inductive type *) val destMutInd : constr -> inductive val op_of_mind : constr -> inductive_path @@ -697,7 +693,7 @@ type constr_operator = | OpSort of sorts | OpRel of int | OpVar of identifier | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpAppL | OpConst of section_path | OpAbst of section_path + | OpAppL | OpConst of section_path | OpEvar of existential_key | OpMutInd of inductive_path | OpMutConstruct of constructor_path @@ -717,6 +713,20 @@ val generic_fold_left : ('a -> constr -> 'a) -> 'a -> (name * constr option * constr) list -> constr array -> 'a +val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + +val iter_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit + +val map_constr : (constr -> constr) -> constr -> constr + +val map_constr_with_binders : + (name -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr + + (*s Hash-consing functions for constr. *) val hcons_constr: diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4b22b0b6a8..37dfccf9ee 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -213,7 +213,7 @@ let type_of_case env sigma ci pj cj lfj = type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft); - { uj_val = mkMutCaseA ci pj.uj_val cj.uj_val (Array.map j_val_only lfj); + { uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val_only lfj); uj_type = make_typed rslty kind } (* Prop and Set *) @@ -636,7 +636,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsVar _ | IsSort _ -> List.for_all (check_rec_call n lst) l - | IsXtra _ | IsAbst _ -> List.for_all (check_rec_call n lst) l + | IsXtra _ -> List.for_all (check_rec_call n lst) l ) in @@ -856,7 +856,6 @@ let control_only_guard env sigma = | IsMutConstruct (_,cl) -> Array.iter control_rec cl | IsConst (_,cl) -> Array.iter control_rec cl | IsEvar (_,cl) -> Array.iter control_rec cl - | IsAbst (_,cl) -> Array.iter control_rec cl | IsAppL (_,cl) -> List.iter control_rec cl | IsCast (c1,c2) -> control_rec c1; control_rec c2 | IsProd (_,c1,c2) -> control_rec c1; control_rec c2 diff --git a/library/indrec.ml b/library/indrec.ml index c895787358..ddba73abed 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -56,10 +56,10 @@ let mis_make_case_com depopt env sigma mispec kind = it_lambda_name env' (lambda_create env' (build_dependent_inductive ind, - mkMutCaseA ci - (Rel (nbprod+nbargsprod)) - (Rel 1) - (rel_vect nbargsprod k))) + mkMutCase (ci, + Rel (nbprod+nbargsprod), + Rel 1, + rel_vect nbargsprod k))) lnamesar else let cs = lift_constructor (k+1) constrs.(k) in @@ -239,8 +239,8 @@ let mis_make_indrec env sigma listdepkind mispec = (lambda_create env (build_dependent_inductive (lift_inductive_family nrec indf), - mkMutCaseA (make_default_case_info mispeci) - (Rel (dect+j+1)) (Rel 1) branches)) + mkMutCase (make_default_case_info mispeci, + Rel (dect+j+1), Rel 1, branches))) (lift_context nrec lnames) in let typtyi = diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 5415d819cf..72b7e1cf55 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -153,8 +153,6 @@ let dbize_global loc = function RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt)) | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) -> RRef (loc,RConstruct (((dbize_sp sp,ti),n),dbize_ctxt ctxt)) - (* | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp) *) - (* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *) | _ -> anomaly_loc (loc,"dbize_global", [< 'sTR "Bad ast for this global a reference">]) @@ -595,7 +593,6 @@ let rec pat_of_ref metas vars = function | RInd (ip,ctxt) -> RInd (ip, dbize_rawconstr_ctxt ctxt) | RConstruct(cp,ctxt) ->RConstruct(cp, dbize_rawconstr_ctxt ctxt) | REVar (n,ctxt) -> REVar (n, dbize_rawconstr_ctxt ctxt) - | RAbst _ -> error "pattern_of_rawconstr: not implemented" | RVar _ -> assert false (* Capturé dans pattern_of_raw *) and pat_of_raw metas vars lvar = function diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 2a7f5ac8e6..fac13a4e08 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -86,7 +86,6 @@ GEXTEND Gram ($SLAM $b $c1))) >> | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> <:ast< (LETIN $c [$id1]$c1) >> -(* <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>*) | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >> diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index 21163804ec..f3aaa4e2a7 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -5,7 +5,7 @@ open Pp open Util open Names open Univ -open Generic +(*i open Generic i*) open Term open Environ diff --git a/parsing/pattern.ml b/parsing/pattern.ml index ff747d4e35..17a4535a4d 100644 --- a/parsing/pattern.ml +++ b/parsing/pattern.ml @@ -53,7 +53,6 @@ let label_of_ref = function | RInd (sp,_) -> IndNode sp | RConstruct (sp,_) -> CstrNode sp | RVar id -> VarNode id - | RAbst _ -> error "Obsolète" | REVar _ -> raise BoundPattern let rec head_pattern_bound t = @@ -265,12 +264,12 @@ let rec sub_match nocc pat c = (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with | PatternMatchingFailure -> let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in - (lm,mkMutCase (ci,hd,List.hd le,List.tl le)) + (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)) | NextOccurrence nocc -> let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in - (lm,mkMutCase (ci,hd,List.hd le,List.tl le))) + (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))) | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _ - | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _|IsAbst (_, _) -> + | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ -> (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with | PatternMatchingFailure -> raise (NextOccurrence nocc) | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) @@ -327,4 +326,4 @@ let rec pattern_of_constr t = Array.map pattern_of_constr br) | IsFix _ | IsCoFix _ -> error "pattern_of_constr: (co)fix currently not supported" - | IsAbst _ | IsXtra _ -> anomaly "No longer supported" + | IsXtra _ -> anomaly "No longer supported" diff --git a/parsing/termast.ml b/parsing/termast.ml index 98aed4f567..0d04bd2b21 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -110,9 +110,6 @@ let ast_of_inductive_ref pr ((sp,tyi) as ind_sp,ids) = let ast_of_ref pr = function | RConst (sp,ctxt) -> ast_of_constant_ref pr (sp,ctxt) - | RAbst (sp) -> - ope("ABST", (path_section dummy_loc sp) - ::(List.map ast_of_ident (* on triche *) [])) | RInd (ind,ctxt) -> ast_of_inductive_ref pr (ind,ctxt) | RConstruct (cstr,ctxt) -> ast_of_constructor_ref pr (cstr,ctxt) | RVar id -> ast_of_ident id @@ -310,399 +307,17 @@ and factorize_binder n oper na aty c = let ast_of_rawconstr = ast_of_raw -(*****************************************************************) -(* TO EJECT ... REPRIS DANS detyping *) - - -(* Nouvelle version de renommage des variables (DEC 98) *) -(* This is the algorithm to display distinct bound variables - - - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste - des noms à éviter - - Règle 2 : c'est la dépendance qui décide si on affiche ou pas - - Exemple : - si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors - il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b) - mais f et f0 contribue à la liste des variables à éviter (en supposant - que les noms f et f0 ne sont pas déjà pris) - Intérêt : noms homogènes dans un but avant et après Intro -*) - -type used_idents = identifier list - -(* This avoids var names, const/ind/construct names but also names of - de Bruijn variables bound in env *) - -let occur_id env id0 c = - let rec occur n = function - | VAR id -> id=id0 - | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) - | DOPN (Abst sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) - | DOPN (MutInd ind_sp, cl) as t -> - (basename (path_of_inductive_path ind_sp) = id0) - or (array_exists (occur n) cl) - | DOPN (MutConstruct cstr_sp, cl) as t -> - (basename (path_of_constructor_path cstr_sp) = id0) - or (array_exists (occur n) cl) - | DOPN(_,cl) -> array_exists (occur n) cl - | DOP1(_,c) -> occur n c - | DOP2(_,c1,c2) -> (occur n c1) or (occur n c2) - | DLAM(_,c) -> occur (n+1) c - | DLAMV(_,v) -> array_exists (occur (n+1)) v - | CLam (_,t,c) -> occur n (body_of_type t) or occur (n+1) c - | CPrd (_,t,c) -> occur n (body_of_type t) or occur (n+1) c - | CLet (_,b,t,c) -> occur n b or occur n (body_of_type t) or occur (n+1) c - | Rel p -> - p>n & - (try lookup_name_of_rel (p-n) env = Name id0 - with Not_found -> false) (* Unbound indice : may happen in debug *) - | DOP0 _ -> false - in - occur 1 c - -let next_name_not_occuring name l env t = - let rec next id = - if List.mem id l or occur_id env id t then next (lift_ident id) else id - in - match name with - | Name id -> next id - | Anonymous -> id_of_string "_" - -(* Remark: Anonymous var may be dependent in Evar's contexts *) -let concrete_name islam l env n c = - if n = Anonymous & not (dependent (mkRel 1) c) then - (None,l) - else - let fresh_id = next_name_not_occuring n l env c in - let idopt = - if islam or dependent (mkRel 1) c then (Some fresh_id) else None in - (idopt, fresh_id::l) - - (* Returns the list of global variables and constants in a term *) -let global_vars_and_consts t = - let rec collect acc c = - let op, cl = splay_constr c in - let acc' = Array.fold_left collect acc cl in - match op with - | OpVar id -> id::acc' - | OpConst sp -> (basename sp)::acc' - | OpAbst sp -> (basename sp)::acc' - | OpMutInd ind_sp -> (basename (path_of_inductive_path ind_sp))::acc' - | OpMutConstruct csp -> (basename (path_of_constructor_path csp))::acc' - | _ -> acc' - in - list_uniquize (collect [] t) - -let used_of = global_vars_and_consts - -(****************************************************************************) -(* Tools for printing of Cases *) -(* These functions implement a light form of Termenv.mind_specif_of_mind *) -(* specially for handle Cases printing; they respect arities but not typing *) - -let bdize_app c al = - let impl = - match c with - | DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp - | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp - | DOPN(Const sp,_) -> constant_implicits_list sp - | VAR id -> (try implicits_of_var id with _ -> []) (* et FW? *) - | _ -> [] - in - if !print_implicits then - ope("APPLISTEXPL", al) - else - ope("APPLIST", explicitize impl al) - -(* Auxiliary function for MutCase printing *) -(* [computable] tries to tell if the predicate typing the result is inferable*) - -let computable p k = - (* We first remove as many lambda as the arity, then we look - if it remains a lambda for a dependent elimination. This function - works for normal eta-expanded term. For non eta-expanded or - non-normal terms, it may affirm the pred is synthetisable - because of an undetected ultimate dependent variable in the second - clause, or else, it may affirms the pred non synthetisable - because of a non normal term in the fourth clause. - A solution could be to store, in the MutCase, the eta-expanded - normal form of pred to decide if it depends on its variables - - Lorsque le prédicat est dépendant de manière certaine, on - ne déclare pas le prédicat synthétisable (même si la - variable dépendante ne l'est pas effectivement) parce que - sinon on perd la réciprocité de la synthèse (qui, lui, - engendrera un prédicat non dépendant) *) - - let rec striprec n c = match n,kind_of_term c with - | (0,IsLambda (_,_,d)) -> false - | (0,_) -> noccur_between 1 k c - | (n,IsLambda (_,_,d)) -> striprec (n-1) d - | _ -> false - in - striprec k p - -let ids_of_var cl = - List.map - (function - | RRef (_,RVar id) -> id - | _-> anomaly "ids_of_var") - (Array.to_list cl) - -(* Main translation function from constr -> ast *) - -let old_bdize at_top env t = - let init_avoid = if at_top then ids_of_context env else [] in - let rec bdrec avoid env t = match collapse_appl t with - (* Not well-formed constructions *) - | DLAM(na,c) -> - (match concrete_name true (*On ne sait pas si prod*)avoid env na c with - | (Some id,avoid') -> - slam(Some (string_of_id id), - bdrec avoid' (add_name (Name id) env) c) - | (None,avoid') -> - slam(None,bdrec avoid' env (pop c))) - | DLAMV(na,cl) -> - if not(array_exists (dependent (mkRel 1)) cl) then - slam(None,ope("V$",array_map_to_list - (fun c -> bdrec avoid env (pop c)) cl)) - else - let id = next_name_away na avoid in - slam(Some (string_of_id id), - ope("V$", array_map_to_list - (bdrec (id::avoid) (add_name (Name id) env)) cl)) - - (* Well-formed constructions *) - | regular_constr -> - (match kind_of_term regular_constr with - | IsRel n -> - (try - match lookup_name_of_rel n env with - | Name id -> nvar (string_of_id id) - | Anonymous -> raise Not_found - with Not_found -> - ope("REL",[num n])) - (* TODO: Change this to subtract the current depth *) - | IsMeta n -> ope("META",[num n]) - | IsVar id -> nvar (string_of_id id) - | IsXtra s -> ope("XTRA",[str s]) - | IsSort s -> - (match s with - | Prop Null -> ope("PROP",[]) - | Prop Pos -> ope("SET",[]) - | Type u -> - ope("TYPE", - [path_section dummy_loc u.u_sp; num u.u_num])) - | IsCast (c1,c2) -> - if !print_casts then - bdrec avoid env c1 - else - ope("CAST",[bdrec avoid env c1;bdrec avoid env c2]) - | IsLetIn (na,b,_,c) -> - ope("LETIN",[bdrec [] env b; - slam(stringopt_of_name na,bdrec avoid env (pop c))]) - | IsProd (Anonymous,ty,c) -> - (* Anonymous product are never factorized *) - ope("PROD",[bdrec [] env ty; - slam(None,bdrec avoid env (pop c))]) - | IsProd (Name _ as na,ty,c) -> - let (n,a) = factorize_binder 1 avoid env Prod na ty c in - (* PROD et PRODLIST doivent être distingués à cause du cas - non dépendant, pour isoler l'implication; peut-être - un constructeur ARROW serait-il plus justifié ? *) - let oper = if n=1 then "PROD" else "PRODLIST" in - ope(oper,[bdrec [] env ty;a]) - | IsLambda (na,ty,c) -> - let (n,a) = factorize_binder 1 avoid env Lambda na ty c in - (* LAMBDA et LAMBDALIST se comportent pareil *) - let oper = if n=1 then "LAMBDA" else "LAMBDALIST" in - ope(oper,[bdrec [] env ty;a]) - | IsAppL (f,args) -> - bdize_app f (List.map (bdrec avoid env) (f::args)) - | IsConst (sp,cl) -> - ope("CONST",((path_section dummy_loc sp):: - (array_map_to_list (bdrec avoid env) cl))) - | IsEvar (ev,cl) -> - ope("EVAR",((num ev):: - (array_map_to_list (bdrec avoid env) cl))) - | IsAbst (sp,cl) -> - ope("ABST",((path_section dummy_loc sp):: - (array_map_to_list (bdrec avoid env) cl))) - | IsMutInd ((sp,tyi),cl) -> - ope("MUTIND",((path_section dummy_loc sp)::(num tyi):: - (array_map_to_list (bdrec avoid env) cl))) - | IsMutConstruct (((sp,tyi),n),cl) -> - ope("MUTCONSTRUCT", - ((path_section dummy_loc sp)::(num tyi)::(num n):: - (array_map_to_list (bdrec avoid env) cl))) - | IsMutCase (annot,p,c,bl) -> - let synth_type = Detyping.synthetize_type () in - let tomatch = bdrec avoid env c in - begin - match annot with -(* | None -> - (* Pas d'annotation --> affichage avec vieux Case *) - let pred = bdrec avoid env p in - let bl' = array_map_to_list (bdrec avoid env) bl in - ope("MUTCASE",pred::tomatch::bl') - | Some *) (consnargsl,(_,considl,k,style,tags) as ci) -> - let pred = - if synth_type & computable p k & considl <> [||] then - (str "SYNTH") - else - bdrec avoid env p - in - if Detyping.force_if ci then - ope("FORCEIF", [ pred; tomatch; - bdrec avoid env bl.(0); - bdrec avoid env bl.(1) ]) - else - let asttomatch = ope("TOMATCH", [tomatch]) in - let eqnv = - array_map3 (bdize_eqn avoid env) - considl consnargsl bl in - let eqnl = Array.to_list eqnv in - let tag = - if Detyping.force_let ci then - "FORCELET" - else - "CASES" - in - ope(tag,pred::asttomatch::eqnl) - end - - | IsFix ((nv,n),(cl,lfn,vt)) -> - let lfi = List.map (fun na -> next_name_away na avoid) lfn in - let def_env = - List.fold_left - (fun env id -> add_name (Name id) env) env lfi in - let def_avoid = lfi@avoid in - let f = List.nth lfi n in - let rec split_lambda binds env avoid n t = - match (n,kind_of_term t) with - | (0, _) -> (binds,bdrec avoid env t) - | (n, IsCast (t,_)) -> split_lambda binds env avoid n t - | (n, IsLambda (na,t,b)) -> - let ast = bdrec avoid env t in - let id = next_name_away na avoid in - let ast_of_bind = - ope("BINDER",[ast;nvar (string_of_id id)]) in - let new_env = add_name (Name id) env in - split_lambda (ast_of_bind::binds) - new_env (id::avoid) (n-1) b - | _ -> error "split_lambda" - in - let rec split_product env avoid n t = - match (n,kind_of_term t) with - | (0, _) -> bdrec avoid env t - | (n, IsCast (t,_)) -> split_product env avoid n t - | (n, IsProd (na,t,b)) -> - let ast = bdrec avoid env t in - let id = next_name_away na avoid in - let new_env = add_name (Name id) env in - split_product new_env (id::avoid) (n-1) b - | _ -> error "split_product" - in - let listdecl = - list_map_i - (fun i fi -> - let (lparams,ast_of_def) = - split_lambda [] def_env def_avoid (nv.(i)+1) vt.(i) in - let ast_of_typ = - split_product env avoid (nv.(i)+1) cl.(i) in - ope("FDECL", - [nvar (string_of_id fi); - ope ("BINDERS",List.rev lparams); - ast_of_typ; ast_of_def ])) - 0 lfi - in - ope("FIX", (nvar (string_of_id f))::listdecl) - - | IsCoFix (n,(cl,lfn,vt)) -> - let lfi = List.map (fun na -> next_name_away na avoid) lfn in - let def_env = - List.fold_left - (fun env id -> add_name (Name id) env) env lfi in - let def_avoid = lfi@avoid in - let f = List.nth lfi n in - let listdecl = - list_map_i (fun i fi -> ope("CFDECL", - [nvar (string_of_id fi); - bdrec avoid env cl.(i); - bdrec def_avoid def_env vt.(i)])) - 0 lfi - in - ope("COFIX", (nvar (string_of_id f))::listdecl)) - - and bdize_eqn avoid env constructid nargs branch = - let print_underscore = Detyping.force_wildcard () in - let cnvar = nvar (string_of_id constructid) in - let rec buildrec nvarlist avoid env = function - - | 0, b - -> let pattern = - if nvarlist = [] then cnvar - else ope ("PATTCONSTRUCT", cnvar::(List.rev nvarlist)) in - let action = bdrec avoid env b in - ope("EQN", [action; pattern]) - - | n, DOP2(Lambda,_,DLAM(x,b)) - -> let x'= - if not print_underscore or (dependent (mkRel 1) b) then x - else Anonymous in - let id = next_name_away x' avoid in - let new_env = (add_name (Name id) env) in - let new_avoid = id::avoid in - let new_nvarlist = (nvar (string_of_id id))::nvarlist in - buildrec new_nvarlist new_avoid new_env (n-1,b) - - | n, DOP2(Cast,b,_) (* Oui, il y a parfois des cast *) - -> buildrec nvarlist avoid env (n,b) - - | n, b (* eta-expansion : n'arrivera plus lorsque tous les - termes seront construits à partir de la syntaxe Cases *) - -> (* nommage de la nouvelle variable *) - let id = next_ident_away (id_of_string "x") avoid in - let new_nvarlist = (nvar (string_of_id id))::nvarlist in - let new_env = (add_name (Name id) env) in - let new_avoid = id::avoid in - let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in - buildrec new_nvarlist new_avoid new_env (n-1,new_b) - - in buildrec [] avoid env (nargs,branch) - - and factorize_binder n avoid env oper na ty c = - let (env2, avoid2,na2) = - match concrete_name (oper=Lambda) avoid env na c with - (Some id,l') -> add_name (Name id) env, l', Some (string_of_id id) - | (None,l') -> add_name Anonymous env, l', None - in - let (p,body) = match c with - DOP2(oper',ty',DLAM(na',c')) - when (oper = oper') - & eq_constr (lift 1 ty) ty' - & not (na' = Anonymous & oper = Prod) - -> factorize_binder (n+1) avoid2 env2 oper na' ty' c' - | _ -> (n,bdrec avoid2 env2 c) - in (p,slam(na2, body)) - - in - bdrec init_avoid (names_of_rel_context env) t -(* FIN TO EJECT *) (******************************************************************) +(* Main translation function from constr -> ast *) let ast_of_constr at_top env t = let t' = if !print_casts then t else Reduction.strong (fun _ _ -> strip_outer_cast) empty_env Evd.empty t in - try - let avoid = if at_top then ids_of_context env else [] in - ast_of_raw - (Detyping.detype avoid (names_of_rel_context env) t') - with Detyping.StillDLAM -> - old_bdize at_top env t' + let avoid = if at_top then ids_of_context env else [] in + ast_of_raw + (Detyping.detype avoid (names_of_rel_context env) t') let ast_of_constant env = ast_of_constant_ref (ast_of_constr false env) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b01b3e283a..54869505ee 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -79,7 +79,7 @@ let make_case_ml isrec pred c ci lf = if isrec then DOPN(XTRA("REC"),Array.append [|pred;c|] lf) else - mkMutCaseA ci pred c lf + mkMutCase (ci, pred, c, lf) (* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the * K parameters. Then then build_notdep builds the predicate @@ -598,7 +598,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) = let predpred = lam_it (mkSort s) sign in let caseinfo = make_default_case_info mis in let brs = array_map2 abstract_conclusion typs cstrs in - let predbody = mkMutCaseA caseinfo predpred (Rel 1) brs in + let predbody = mkMutCase (caseinfo, predpred, Rel 1, brs) in let pred = lam_it (lift (List.length sign) typn) sign in failwith "TODO4-2"; (true,pred) @@ -833,7 +833,7 @@ and match_current pb (n,tm) = find_predicate pb.env pb.isevars pb.pred brtyps cstrs current indt in let ci = make_case_info mis None tags in - { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals; + { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)pred,current,brvals); uj_type = make_typed typ s } and compile_further pb firstnext rest = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 596310512a..a6d06f3f95 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -30,11 +30,30 @@ open Rawterm type used_idents = identifier list +exception Occur + +let occur_rel p env id = + try lookup_name_of_rel p env = Name id + with Not_found -> false (* Unbound indice : may happen in debug *) + +let occur_id env id0 c = + let rec occur n c = match kind_of_term c with + | IsVar id when id=id0 -> raise Occur + | IsConst (sp, _) when basename sp = id0 -> raise Occur + | IsMutInd (ind_sp, _) + when basename (path_of_inductive_path ind_sp) = id0 -> raise Occur + | IsMutConstruct (cstr_sp, _) + when basename (path_of_constructor_path cstr_sp) = id0 -> raise Occur + | IsRel p when p>n & occur_rel (p-n) env id0 -> raise Occur + | _ -> iter_constr_with_binders succ occur n c + in + try occur 1 c; false + with Occur -> true +(* let occur_id env_names id0 c = let rec occur n = function | VAR id -> id=id0 | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) - | DOPN (Abst sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) | DOPN (MutInd ind_sp, cl) as t -> (basename (path_of_inductive_path ind_sp) = id0) or (array_exists (occur n) cl) @@ -56,7 +75,7 @@ let occur_id env_names id0 c = | DOP0 _ -> false in occur 1 c - +*) let next_name_not_occuring name l env_names t = let rec next id = if List.mem id l or occur_id env_names id t then next (lift_ident id) @@ -83,7 +102,6 @@ let global_vars_and_consts t = match op with | OpVar id -> id::acc' | OpConst sp -> (basename sp)::acc' - | OpAbst sp -> (basename sp)::acc' | OpMutInd ind_sp -> (basename (path_of_inductive_path ind_sp))::acc' | OpMutConstruct csp -> (basename (path_of_constructor_path csp))::acc' | _ -> acc' @@ -247,15 +265,6 @@ let computable p k = in striprec (k,p) -(* -let ids_of_var cl = - List.map - (function - | RRef (_,RVar id) -> id - | _-> anomaly "ids_of_var") - (Array.to_list cl) -*) - let lookup_name_as_renamed ctxt t s = let rec lookup avoid env_names n c = match kind_of_term c with | IsProd (name,t,c') -> @@ -278,12 +287,10 @@ let lookup_index_as_renamed t n = | _ -> None in lookup n 1 t -exception StillDLAM - let rec detype avoid env t = match collapse_appl t with (* Not well-formed constructions *) - | DLAM _ | DLAMV _ -> raise StillDLAM + | DLAM _ | DLAMV _ -> error "Cannot detype" (* Well-formed constructions *) | regular_constr -> (match kind_of_term regular_constr with @@ -312,8 +319,6 @@ let rec detype avoid env t = RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) | IsEvar (ev,cl) -> RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl)) - | IsAbst (sp,cl) -> - anomaly "bdize: Abst should no longer occur in constr" | IsMutInd (ind_sp,cl) -> RRef (dummy_loc,RInd (ind_sp,Array.map (detype avoid env) cl)) | IsMutConstruct (cstr_sp,cl) -> diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index e961cfe917..8c8dd417d1 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -12,8 +12,6 @@ open Rawterm (* [detype avoid env c] turns [c], typed in [env], into a rawconstr. *) (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *) -exception StillDLAM - val detype : identifier list -> names_context -> constr -> rawconstr (* look for the index of a named var or a nondep var as it is renamed *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e4e2e48c59..f9a3fe69b0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -210,32 +210,6 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f3; f4] - | IsAbst (_,_), IsAbst (_,_) -> - let f1 () = - (term1=term2) & - (List.length(l1) = List.length(l2)) & - (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) - and f2 () = - if evaluable_abst env term2 then - evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 (abst_value env term2)) - else - evaluable_abst env term1 - & evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 (abst_value env term1)) appr2 - in - ise_try isevars [f1; f2] - - | IsAbst (_,_), _ -> - (evaluable_abst env term1) - & evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 (abst_value env term1)) appr2 - - | _, IsAbst (_,_) -> - (evaluable_abst env term2) - & evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 (abst_value env term2)) - | IsRel n, IsRel m -> n=m & (List.length(l1) = List.length(l2)) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 09dd230654..295e081a34 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -96,7 +96,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = (lambda_create env (applist (mI,List.append (List.map (lift (nar+1)) params) (rel_list 0 nar)), - mkMutCaseA ci (lift (nar+2) p) (Rel 1) branches)) + mkMutCase (ci, lift (nar+2) p, Rel 1, branches))) (lift_context 1 lnames) in if noccurn 1 deffix then @@ -119,7 +119,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = applist (fix,realargs@[c]) else let ci = make_default_case_info mispec in - mkMutCaseA ci p c lf + mkMutCase (ci, p, c, lf) (***********************************************************************) @@ -217,8 +217,6 @@ let pretype_ref pretype loc isevars env lvar = function let cst = (sp,Array.map pretype ctxt) in make_judge (mkConst cst) (type_of_constant env !isevars cst) -| RAbst sp -> failwith "Pretype: abst doit disparaître" - | REVar (sp,ctxt) -> error " Not able to type terms with dependent subgoals" | RInd (ind_sp,ctxt) -> @@ -401,7 +399,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) else let mis,_ = dest_ind_family indf in let ci = make_default_case_info mis in - mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj) + mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map (fun j-> j.uj_val) lfj) in let s = snd (splay_arity env !isevars evalPt) in {uj_val = v; diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index aa499fb630..bd1b88bea5 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -48,7 +48,6 @@ let rec type_of env cstr= (try body_of_type (snd (lookup_var id env)) with Not_found -> anomaly ("type_of: variable "^(string_of_id id)^" unbound")) - | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*) | IsConst c -> body_of_type (type_of_constant env sigma c) | IsEvar _ -> type_of_existential env sigma cstr | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 16eebbefb7..dde27dbae8 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -91,7 +91,7 @@ let reduce_mind_case_use_function env f mia = applist (mia.mlf.(i-1),real_cargs) | DOPN(CoFix _,_) as cofix -> let cofix_def = contract_cofix_use_function f (destCoFix cofix) in - mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf + mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false let special_red_case env whfun p c ci lf = @@ -160,13 +160,6 @@ and construct_const env sigma c stack = | _ -> hnfstack (cval, stack)) else raise Redelimination) -(* - | (DOPN(Abst _,_) as a) -> - if evaluable_abst env a then - hnfstack (abst_value env a) stack - else - raise Redelimination -*) | IsCast (c,_) -> hnfstack (c, stack) | IsAppL (f,cl) -> hnfstack (f, cl@stack) | IsLambda (_,_,c) -> @@ -208,13 +201,6 @@ let hnf_constr env sigma c = | _ -> redrec (c, largs)) else applist s) -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - redrec (abst_value env x) largs - else - applist s -*) | IsCast (c,_) -> redrec (c, largs) | IsMutCase (ci,p,c,lf) -> (try @@ -307,11 +293,7 @@ let one_step_reduce env sigma c = if evaluable_constant env x then applistc (constant_value env x) largs else error "Not reductible 1") -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then applistc (abst_value env x) largs - else error "Not reducible 0" -*) + | IsMutCase (ci,p,c,lf) -> (try applistc diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 5dfcfdce3c..cbe8b36013 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -40,12 +40,6 @@ let rec execute mf env sigma cstr = with Not_found -> error ("execute: variable " ^ (string_of_id id) ^ " not defined")) - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env sigma (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - | IsConst c -> make_judge cstr (type_of_constant env sigma c) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ab301c4506..0cd364b93e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -429,10 +429,10 @@ let clenv_instance_term clenv c = let clenv_cast_meta clenv = let rec crec u = - match splay_constr u with - | (OpAppL | OpMutCase _), _ -> crec_hd u - | OpCast , [|c;_|] when isMeta c -> u - | op, cl -> gather_constr (op, Array.map crec cl) + match kind_of_term u with + | IsAppL _ | IsMutCase _ -> crec_hd u + | IsCast (c,_) when isMeta c -> u + | _ -> map_constr crec u and crec_hd u = match kind_of_term (strip_outer_cast u) with @@ -447,7 +447,7 @@ let clenv_cast_meta clenv = u) | IsAppL(f,args) -> mkAppList (crec_hd f) (List.map crec args) | IsMutCase(ci,p,c,br) -> - mkMutCaseA ci (crec_hd p) (crec_hd c) (Array.map crec br) + mkMutCase (ci, crec_hd p, crec_hd c, Array.map crec br) | _ -> u in crec diff --git a/proofs/logic.ml b/proofs/logic.ml index a92276cc83..db9b7c1107 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -157,7 +157,7 @@ let new_meta_variables = | IsCast (c,t) -> mkCast (newrec c, t) | IsAppL (f,cl) -> applist (newrec f, List.map newrec cl) | IsMutCase (ci,p,c,lf) -> - mkMutCaseA ci (newrec p) (newrec c) (Array.map newrec lf) + mkMutCase (ci, newrec p, newrec c, Array.map newrec lf) | _ -> x in newrec diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 28eaa7ad4b..b96f17af55 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -765,8 +765,7 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = in idents := Some (function - Const sp -> List.mem sp idl - | Abst sp -> List.mem sp idl + | Const sp -> List.mem sp idl | _ -> false) else user_err_loc(loc,"flag_of_ast", [<'sTR "Cannot specify identifiers to unfold twice">]) @@ -781,8 +780,7 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = in idents := Some (function - Const sp -> not (List.mem sp idl) - | Abst sp -> not (List.mem sp idl) + | Const sp -> not (List.mem sp idl) | _ -> false) else user_err_loc(loc,"flag_of_ast", [<'sTR "Cannot specify identifiers to unfold twice">]) diff --git a/tactics/equality.ml b/tactics/equality.ml index c301b62d11..f325621820 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -464,7 +464,7 @@ let descend_then sigma env head dirn = let result = if i = dirn then dirnval else dfltval in it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in - mkMutCase (make_default_case_info mispec, p, head, + mkMutCaseL (make_default_case_info mispec, p, head, List.map build_branch (interval 1 (mis_nconstr mispec))))) (* Now we need to construct the discriminator, given a discriminable @@ -509,7 +509,7 @@ let construct_discriminator sigma env dirn c sort = it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in let build_match = - mkMutCase (make_default_case_info mispec, p, c, + mkMutCaseL (make_default_case_info mispec, p, c, List.map build_branch (interval 1 (mis_nconstr mispec))) in build_match diff --git a/tactics/refine.ml b/tactics/refine.ml index f188eba7f5..f5a95d59c1 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -124,7 +124,7 @@ let fresh env n = let rec compute_metamap env c = match kind_of_term c with (* le terme est directement une preuve *) - | (IsConst _ | IsEvar _ | IsAbst _ | IsMutInd _ | IsMutConstruct _ | + | (IsConst _ | IsEvar _ | IsMutInd _ | IsMutConstruct _ | IsSort _ | IsVar _ | IsRel _) -> TH (c,[],[]) (* le terme est une mv => un but *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87a4370cb6..b77ac413c8 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -297,9 +297,9 @@ let general_elim_then_using elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl = let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in let name_elim = - (match elim with - | DOPN(Const sp,_) -> id_of_string(string_of_path sp) - | VAR id -> id + (match kind_of_term elim with + | IsConst (sp,_) -> id_of_string (string_of_path sp) + | IsVar id -> id | _ -> id_of_string " ") in (* applying elimination_scheme just a little modified *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3b24ad75d1..4312071b48 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -40,6 +40,7 @@ let get_pairs_from_bindings = in List.map pair_from_binding +(* let force_reference c = match fst (decomp_app c) with | DOPN (Const sp,ctxt) -> c @@ -48,18 +49,18 @@ let force_reference c = | DOPN (MutInd (sp,i),ctxt) -> c | VAR id -> c | _ -> error "Not an atomic type" +*) -let rec string_head_bound = function - | DOPN(Const _,_) as x -> - string_of_id (basename (path_of_const x)) - | DOPN(MutInd ind_sp,args) as x -> +let rec string_head_bound x = match kind_of_term x with + | IsConst _ -> string_of_id (basename (path_of_const x)) + | IsMutInd (ind_sp,args) -> let mispec = Global.lookup_mind_specif (ind_sp,args) in string_of_id (mis_typename mispec) - | DOPN(MutConstruct (ind_sp,i),args) -> + | IsMutConstruct ((ind_sp,i),args) -> let mispec = Global.lookup_mind_specif (ind_sp,args) in string_of_id (mis_consnames mispec).(i-1) - | VAR id -> string_of_id id - | _ -> raise Bound + | IsVar id -> string_of_id id + | _ -> raise Bound let string_head c = try string_head_bound c with Bound -> error "Bound head variable" @@ -232,10 +233,10 @@ let dyn_reduce = function (* Unfolding occurrences of a constant *) let unfold_constr c = - match strip_outer_cast c with - | DOPN(Const(sp),_) -> + match kind_of_term (strip_outer_cast c) with + | IsConst(sp,_) -> unfold_in_concl [[],sp] - | t -> + | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant." >] @@ -937,14 +938,14 @@ let dyn_split = function * gl : the current goal *) -let last_arg = function - | DOPN(AppL,cl) -> cl.(Array.length cl - 1) +let last_arg c = match kind_of_term c with + | IsAppL (f,cl) -> List.nth cl (List.length cl - 1) | _ -> anomaly "last_arg" let elimination_clause_scheme kONT wc elimclause indclause gl = let indmv = - (match last_arg (clenv_template elimclause).rebus with - | DOP0(Meta mv) -> mv + (match kind_of_term (last_arg (clenv_template elimclause).rebus) with + | IsMeta mv -> mv | _ -> errorlabstrm "elimination_clause" [< 'sTR "The type of elimination clause is not well-formed" >]) in @@ -1416,8 +1417,8 @@ let dyn_destruct = function let elim_scheme_type elim t gl = let (wc,kONT) = startWalk gl in let clause = mk_clenv_type_of wc elim in - match last_arg (clenv_template clause).rebus with - | DOP0(Meta mv) -> + match kind_of_term (last_arg (clenv_template clause).rebus) with + | IsMeta mv -> let clause' = clenv_unify (clenv_instance_type clause mv) t clause in elim_res_pf kONT clause' gl | _ -> anomaly "elim_scheme_type" diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 92e76fbd3d..25fabac03e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -26,7 +26,9 @@ val type_clenv_binding : walking_constraints -> constr * constr -> constr substitution -> constr (* [force_reference c] fails if [c] is not a reference *) +(* val force_reference : constr -> constr +*) val string_head : constr -> string val head_constr : constr -> constr list diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index c37aa6ff1a..bee6f074a9 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -190,7 +190,43 @@ let explain_cant_apply_not_functional k ctx rator randl = 'sTR" "; v 0 appl; 'fNL >] (* (co)fixpoints *) -let explain_ill_formed_rec_body k ctx str lna i vdefs = +let explain_ill_formed_rec_body k ctx err lna i vdefs = + let str = match err with + + (* Fixpoint guard errors *) + | NotEnoughAbstractionInFixBody -> + [< 'sTR "Not enough abstractions in the definition" >] + | RecursionNotOnInductiveType -> + [< 'sTR "Recursive definition on a non inductive type" >] + | RecursionOnIllegalTerm -> + [< 'sTR "Recursive call applied to an illegal term" >] + | NotEnoughArgumentsForFixCall -> + [< 'sTR "Not enough arguments for the recursive call" >] + + (* CoFixpoint guard errors *) + (* TODO : récupérer le contexte des termes pour pouvoir les afficher *) + | CodomainNotInductiveType c -> + [< 'sTR "The codomain is"; 'sPC; P.pr_term k ctx c; 'sPC; + 'sTR "which should be a coinductive type" >] + | NestedRecursiveOccurrences -> + [< 'sTR "Nested recursive occurrences" >] + | UnguardedRecursiveCall c -> + [< 'sTR "Unguarded recursive call" >] + | RecCallInTypeOfAbstraction c -> + [< 'sTR "Not allowed recursive call in the domain of an abstraction" >] + | RecCallInNonRecArgOfConstructor c -> + [< 'sTR "Not allowed recursive call in a non-recursive argument of constructor" >] + | RecCallInTypeOfDef c -> + [< 'sTR "Not allowed recursive call in the type of a recursive definition" >] + | RecCallInCaseFun c -> + [< 'sTR "Not allowed recursive call in a branch of cases" >] + | RecCallInCaseArg c -> + [< 'sTR "Not allowed recursive call in the argument of cases" >] + | RecCallInCasePred c -> + [< 'sTR "Not allowed recursive call in the type of cases in" >] + | NotGuardedForm -> + [< 'sTR "Definition not in guarded form" >] +in let pvd = P.pr_term k ctx vdefs.(i) in let s = match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli index ad0e7e6646..0ba0e73a70 100644 --- a/toplevel/fhimsg.mli +++ b/toplevel/fhimsg.mli @@ -57,7 +57,7 @@ val explain_actual_type : path_kind -> env -> constr -> constr -> constr -> std_ppcmds val explain_ill_formed_rec_body : - path_kind -> env -> std_ppcmds -> + path_kind -> env -> guard_error -> name list -> int -> constr array -> std_ppcmds val explain_ill_typed_rec_body : diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f33633517a..a6e63497d0 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -335,8 +335,8 @@ let explain_type_error k ctx = function explain_cant_apply_not_functional k ctx rator randl | IllFormedRecBody (i, lna, vdefj, vargs) -> explain_ill_formed_rec_body k ctx i lna vdefj vargs - | IllTypedRecBody (i, lna, vdefj, vargs) -> - explain_ill_typed_rec_body k ctx i lna vdefj vargs + | IllTypedRecBody (i, lna, vdefj, vargs) -> + explain_ill_typed_rec_body k ctx i lna vdefj vargs | NotInductive c -> explain_not_inductive k ctx c | MLCase (mes,c,ct,br,brt) -> diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 0395b94d95..ab55fe549a 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -26,6 +26,17 @@ let lookup_var id = let args sign = Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign)) +let rec globalize bv c = match kind_of_term c with + | IsVar id -> lookup_var id bv + | IsConst (sp, _) -> + let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps) + | IsMutInd (sp,_ as spi, _) -> + let mib = lookup_mind sp !env in mkMutInd (spi, args mib.mind_hyps) + | IsMutConstruct ((sp,_),_ as spc, _) -> + let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps) + | _ -> map_constr_with_binders (fun na l -> na::l) globalize bv c + +(* let rec globalize bv = function | VAR id -> lookup_var id bv | DOP1 (op,c) -> DOP1 (op, globalize bv c) @@ -43,6 +54,7 @@ let rec globalize bv = function | CPrd(n,t,c) -> CPrd (n, globalize bv t, globalize (n::bv) c) | CLet(n,b,t,c) -> CLet (n,globalize bv b,globalize bv t,globalize (n::bv) c) | Rel _ | DOP0 _ as c -> c +*) let check c = let c = globalize [] c in diff --git a/toplevel/record.ml b/toplevel/record.ml index f3169a066a..30f7dbdee8 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -134,7 +134,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = (Some PrintLet) [| RegularPat |] in let proj = mk_LambdaCit newps (mkLambda (x, rp1, - mkMutCaseA ci p (Rel 1) [|branch|])) in + mkMutCase (ci, p, Rel 1, [|branch|]))) in let ok = try let cie = |