diff options
| author | herbelin | 2000-09-12 11:02:30 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-12 11:02:30 +0000 |
| commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
| tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec | |
| parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) | |
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
38 files changed, 627 insertions, 690 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index a8ecf4cd1f..9b770512a0 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -155,15 +155,16 @@ let hide_constr,find_constr,clear_tables,dump_tables = (fun () -> l := []), (fun () -> !l) -let get_applist c = whd_stack c [] +let get_applist = whd_stack exception Destruct let dest_const_apply t = let f,args = get_applist t in - match f with - | DOPN((Const _ | MutConstruct _ | MutInd _) as s,_) -> - Global.id_of_global s,args + match kind_of_term f with + | IsConst (sp,_) -> Global.id_of_global (Const sp),args + | IsMutConstruct (csp,_) -> Global.id_of_global (MutConstruct csp),args + | IsMutInd (isp,_) -> Global.id_of_global (MutInd isp),args | _ -> raise Destruct type result = @@ -390,30 +391,30 @@ let sp_Zge = path_of_string "#zarith_aux#Zge.cci" let sp_Zlt = path_of_string "#zarith_aux#Zlt.cci" let sp_not = path_of_string "#Logic#not.cci" -let mk_var v = VAR(id_of_string v) -let mk_plus t1 t2 = mkAppL [| Lazy.force coq_Zplus; t1; t2 |] -let mk_times t1 t2 = mkAppL [| Lazy.force coq_Zmult; t1; t2 |] -let mk_minus t1 t2 = mkAppL [| Lazy.force coq_Zminus ; t1;t2 |] -let mk_eq t1 t2 = mkAppL [| Lazy.force coq_eq; Lazy.force coq_Z; t1; t2 |] -let mk_le t1 t2 = mkAppL [| Lazy.force coq_Zle; t1; t2 |] -let mk_gt t1 t2 = mkAppL [| Lazy.force coq_Zgt; t1; t2 |] -let mk_inv t = mkAppL [| Lazy.force coq_Zopp; t |] -let mk_and t1 t2 = mkAppL [| Lazy.force coq_and; t1; t2 |] -let mk_or t1 t2 = mkAppL [| Lazy.force coq_or; t1; t2 |] -let mk_not t = mkAppL [| Lazy.force coq_not; t |] -let mk_eq_rel t1 t2 = mkAppL [| Lazy.force coq_eq; - Lazy.force coq_relation; t1; t2 |] -let mk_inj t = mkAppL [| Lazy.force coq_inject_nat; t |] +let mk_var v = mkVar (id_of_string v) +let mk_plus t1 t2 = mkAppL (Lazy.force coq_Zplus, [| t1; t2 |]) +let mk_times t1 t2 = mkAppL (Lazy.force coq_Zmult, [| t1; t2 |]) +let mk_minus t1 t2 = mkAppL (Lazy.force coq_Zminus, [| t1;t2 |]) +let mk_eq t1 t2 = mkAppL (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |]) +let mk_le t1 t2 = mkAppL (Lazy.force coq_Zle, [| t1; t2 |]) +let mk_gt t1 t2 = mkAppL (Lazy.force coq_Zgt, [| t1; t2 |]) +let mk_inv t = mkAppL (Lazy.force coq_Zopp, [| t |]) +let mk_and t1 t2 = mkAppL (Lazy.force coq_and, [| t1; t2 |]) +let mk_or t1 t2 = mkAppL (Lazy.force coq_or, [| t1; t2 |]) +let mk_not t = mkAppL (Lazy.force coq_not, [| t |]) +let mk_eq_rel t1 t2 = mkAppL (Lazy.force coq_eq, + [| Lazy.force coq_relation; t1; t2 |]) +let mk_inj t = mkAppL (Lazy.force coq_inject_nat, [| t |]) let mk_integer n = let rec loop n = if n=1 then Lazy.force coq_xH else - mkAppL [| if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI; - loop (n/2) |] + mkAppL ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI), + [| loop (n/2) |]) in if n = 0 then Lazy.force coq_ZERO - else mkAppL [| if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG; - loop (abs n) |] + else mkAppL ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG), + [| loop (abs n) |]) type constr_path = | P_APP of int @@ -430,16 +431,20 @@ let context operation path (t : constr) = match (p0,kind_of_term t) with | (p, IsCast (c,t)) -> mkCast (loop i p c,t) | ([], _) -> operation i t - | ((P_APP n :: p), IsAppL _) -> - let f,l = get_applist t in - let v' = Array.of_list (f::l) in - v'.(n) <- loop i p v'.(n); (mkAppL v') - | ((P_BRANCH n :: p), IsMutCase (_,_,_,v)) -> - v.(n) <- loop i p v.(n); (mkAppL v) (* Not Mutcase ?? *) + | ((P_APP n :: p), IsAppL (f,v)) -> +(* let f,l = get_applist t in NECESSAIRE ?? + let v' = Array.of_list (f::l) in *) + let v' = Array.copy v in + v'.(n-1) <- loop i p v'.(n-1); mkAppL (f, v') + | ((P_BRANCH n :: p), IsMutCase (ci,q,c,v)) -> + (* avant, y avait mkAppL... anyway, BRANCH seems nowhere used *) + let v' = Array.copy v in + v'.(n) <- loop i p v'.(n); (mkMutCase (ci,q,c,v')) | ((P_ARITY :: p), IsAppL (f,l)) -> - applist (loop i p f,l) - | ((P_ARG :: p), IsAppL (f,a::l)) -> - applist (f,(loop i p a)::l) + appvect (loop i p f,l) + | ((P_ARG :: p), IsAppL (f,v)) -> + let v' = Array.copy v in + v'.(0) <- loop i p v'.(0); mkAppL (f,v') | (p, IsFix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in @@ -466,10 +471,10 @@ let occurence path (t : constr) = let rec loop p0 t = match (p0,kind_of_term t) with | (p, IsCast (c,t)) -> loop p c | ([], _) -> t - | ((P_APP n :: p), IsAppL (f,l)) -> loop p (List.nth l (n-1)) + | ((P_APP n :: p), IsAppL (f,v)) -> loop p v.(n-1) | ((P_BRANCH n :: p), IsMutCase (_,_,_,v)) -> loop p v.(n) | ((P_ARITY :: p), IsAppL (f,_)) -> loop p f - | ((P_ARG :: p), IsAppL (f,a::l)) -> loop p a + | ((P_ARG :: p), IsAppL (f,v)) -> loop p v.(0) | (p, IsFix((_,n) ,(_,_,v))) -> loop p v.(n) | ((P_BODY :: p), IsProd (n,t,c)) -> loop p c | ((P_BODY :: p), IsLambda (n,t,c)) -> loop p c @@ -523,11 +528,11 @@ let rec weight = function | Oufo _ -> -1 let rec val_of = function - | Oatom c -> (VAR (id_of_string c)) + | Oatom c -> (mkVar (id_of_string c)) | Oz c -> mk_integer c - | Oinv c -> mkAppL [| Lazy.force coq_Zopp; val_of c |] - | Otimes (t1,t2) -> mkAppL [| Lazy.force coq_Zmult; val_of t1; val_of t2 |] - | Oplus(t1,t2) -> mkAppL [| Lazy.force coq_Zplus; val_of t1; val_of t2 |] + | Oinv c -> mkAppL (Lazy.force coq_Zopp, [| val_of c |]) + | Otimes (t1,t2) -> mkAppL (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |]) + | Oplus(t1,t2) -> mkAppL (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) | Oufo c -> c let compile name kind = @@ -561,8 +566,8 @@ let clever_rewrite_base_poly typ p result theorem gl = mkLambda (Name (id_of_string "H"), applist (Rel 1,[result]), - mkAppL [| Lazy.force coq_eq_ind_r; - typ; result; Rel 2; Rel 1; occ; theorem |])), + mkAppL (Lazy.force coq_eq_ind_r, + [| typ; result; Rel 2; Rel 1; occ; theorem |]))), [abstracted]) in exact (applist(t,[mkNewMeta()])) gl @@ -772,7 +777,7 @@ let rec scalar p n = function | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> [], Otimes(t,Oz n) | Oz i -> [focused_simpl p],Oz(n*i) - | Oufo c -> [], Oufo (mkAppL [| Lazy.force coq_Zmult; mk_integer n |]) + | Oufo c -> [], Oufo (mkAppL (Lazy.force coq_Zmult, [| mk_integer n |])) let rec scalar_norm p_init = let rec loop p = function @@ -826,18 +831,18 @@ let rec negate p = function let r = Otimes(t,Oz(-1)) in [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_one)], r | Oz i -> [focused_simpl p],Oz(-i) - | Oufo c -> [], Oufo (mkAppL [| Lazy.force coq_Zopp; c |]) + | Oufo c -> [], Oufo (mkAppL (Lazy.force coq_Zopp, [| c |])) let rec transform p t = let default () = try let v,th,_ = find_constr t in - [clever_rewrite_base p (VAR v) (VAR th)], Oatom (string_of_id v) + [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom (string_of_id v) with _ -> let v = new_identifier_var () and th = new_identifier () in hide_constr t v th false; - [clever_rewrite_base p (VAR v) (VAR th)], Oatom (string_of_id v) + [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom (string_of_id v) in try match destructurate t with | Kapp("Zplus",[t1;t2]) -> @@ -847,12 +852,13 @@ let rec transform p t = tac1 @ tac2 @ tac, t' | Kapp("Zminus",[t1;t2]) -> let tac,t = - transform p (mkAppL [| Lazy.force coq_Zplus; t1; - (mkAppL [| Lazy.force coq_Zopp; t2 |]) |]) in + transform p + (mkAppL (Lazy.force coq_Zplus, + [| t1; (mkAppL (Lazy.force coq_Zopp, [| t2 |])) |])) in unfold sp_Zminus :: tac,t | Kapp("Zs",[t1]) -> - let tac,t = transform p (mkAppL [| Lazy.force coq_Zplus; t1; - mk_integer 1 |]) in + let tac,t = transform p (mkAppL (Lazy.force coq_Zplus, + [| t1; mk_integer 1 |])) in unfold sp_Zs :: tac,t | Kapp("Zmult",[t1;t2]) -> let tac1,t1' = transform (P_APP 1 :: p) t1 @@ -876,11 +882,11 @@ let rec transform p t = | Kapp("inject_nat",[t']) -> begin try let v,th,_ = find_constr t' in - [clever_rewrite_base p (VAR v) (VAR th)],Oatom(string_of_id v) + [clever_rewrite_base p (mkVar v) (mkVar th)],Oatom(string_of_id v) with _ -> let v = new_identifier_var () and th = new_identifier () in hide_constr t' v th true; - [clever_rewrite_base p (VAR v) (VAR th)], Oatom (string_of_id v) + [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom (string_of_id v) end | _ -> default () with e when catchable_exception e -> default () @@ -995,11 +1001,11 @@ let replay_history tactic_normalisation = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_OMEGA17; + [mkAppL (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; - VAR id1; VAR id2 |]]) + mkVar id1; mkVar id2 |])]) (mk_then tac)) (intros_using [aux])) (resolve_id aux)) @@ -1011,10 +1017,10 @@ let replay_history tactic_normalisation = let tac = shuffle_cancel p_initial e1.body in let solve_le = let superieur = Lazy.force coq_SUPERIEUR in - let not_sup_sup = mkAppL [| Lazy.force coq_eq; + let not_sup_sup = mkAppL (Lazy.force coq_eq, [| Lazy.force coq_relation; Lazy.force coq_SUPERIEUR; - Lazy.force coq_SUPERIEUR |] + Lazy.force coq_SUPERIEUR |]) in tclTHENS (tclTHEN @@ -1027,10 +1033,10 @@ let replay_history tactic_normalisation = [ assumption ; reflexivity ] in let theorem = - mkAppL [| Lazy.force coq_OMEGA2; + mkAppL (Lazy.force coq_OMEGA2, [| val_of eq1; val_of eq2; - VAR (hyp_of_tag e1.id); - VAR (hyp_of_tag e2.id) |] + mkVar (hyp_of_tag e1.id); + mkVar (hyp_of_tag e2.id) |]) in tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le) | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> @@ -1051,9 +1057,8 @@ let replay_history tactic_normalisation = (tclTHEN (intros_using [aux]) (generalize_tac - [mkAppL [| - Lazy.force coq_OMEGA1; - eq1; rhs; VAR aux; VAR id |]])) + [mkAppL (Lazy.force coq_OMEGA1, + [| eq1; rhs; mkVar aux; mkVar id |])])) (clear [aux;id])) (intros_using [id])) (cut (mk_gt kk dd))) @@ -1065,10 +1070,9 @@ let replay_history tactic_normalisation = (tclTHEN (intros_using [aux1; aux2]) (generalize_tac - [mkAppL [| - Lazy.force coq_Zmult_le_approx; - kk;eq2;dd;VAR aux1;VAR aux2; - VAR id |]])) + [mkAppL (Lazy.force coq_Zmult_le_approx, [| + kk;eq2;dd;mkVar aux1;mkVar aux2; + mkVar id |])])) (clear [aux1;aux2;id])) (intros_using [id])) (loop l); @@ -1106,9 +1110,9 @@ let replay_history tactic_normalisation = (tclTHEN (intros_using [aux2;aux1]) (generalize_tac - [mkAppL [| Lazy.force coq_OMEGA4; - dd;kk;eq2;VAR aux1; - VAR aux2 |]])) + [mkAppL (Lazy.force coq_OMEGA4, [| + dd;kk;eq2;mkVar aux1; + mkVar aux2 |])])) (clear [aux1;aux2])) (unfold sp_not)) (intros_using [aux])) @@ -1141,9 +1145,8 @@ let replay_history tactic_normalisation = (tclTHEN (intros_using [aux1]) (generalize_tac - [mkAppL [| - Lazy.force coq_OMEGA18; - eq1;eq2;kk;VAR aux1; VAR id |]])) + [mkAppL (Lazy.force coq_OMEGA18, [| + eq1;eq2;kk;mkVar aux1; mkVar id |])])) (clear [aux1;id])) (intros_using [id])) (loop l); @@ -1160,9 +1163,9 @@ let replay_history tactic_normalisation = (tclTHEN (intros_using [aux2;aux1]) (generalize_tac - [mkAppL [| Lazy.force coq_OMEGA3; - eq1; eq2; kk; VAR aux2; - VAR aux1;VAR id|]])) + [mkAppL (Lazy.force coq_OMEGA3, [| + eq1; eq2; kk; mkVar aux2; + mkVar aux1;mkVar id|])])) (clear [aux1;aux2;id])) (intros_using [id])) (loop l); @@ -1189,10 +1192,9 @@ let replay_history tactic_normalisation = (tclTHEN (tclTHEN (intros_using [aux]) - (generalize_tac [mkAppL [| - Lazy.force coq_OMEGA8; - eq1;eq2;VAR id1;VAR id2; - VAR aux|]])) + (generalize_tac [mkAppL (Lazy.force coq_OMEGA8, [| + eq1;eq2;mkVar id1;mkVar id2; + mkVar aux|])])) (clear [id1;id2;aux])) (intros_using [id])) (loop l); @@ -1207,16 +1209,16 @@ let replay_history tactic_normalisation = let v = unintern_id sigma in let vid = id_of_string v in let theorem = - mkAppL [| Lazy.force coq_ex; + mkAppL (Lazy.force coq_ex, [| Lazy.force coq_Z; mkLambda (Name(id_of_string v), Lazy.force coq_Z, - mk_eq (Rel 1) eq1) |] + mk_eq (Rel 1) eq1) |]) in let mm = mk_integer m in let p_initial = [P_APP 2;P_TYPE] in - let r = mk_plus eq2 (mk_times (mk_plus (mk_inv (VAR vid)) eq1) mm) in + let r = mk_plus eq2 (mk_times (mk_plus (mk_inv (mkVar vid)) eq1) mm) in let tac = clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) [[P_APP 1]] (Lazy.force coq_fast_Zopp_one) :: @@ -1237,9 +1239,9 @@ let replay_history tactic_normalisation = (clear [aux])) (intros_using [vid; aux])) (generalize_tac - [mkAppL [| Lazy.force coq_OMEGA9; - VAR vid;eq2;eq1;mm; - VAR id2;VAR aux |] ])) + [mkAppL (Lazy.force coq_OMEGA9, [| + mkVar vid;eq2;eq1;mm; + mkVar id2;mkVar aux |])])) (mk_then tac)) (clear [aux])) (intros_using [id])) @@ -1254,7 +1256,7 @@ let replay_history tactic_normalisation = let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in let eq = val_of(decompile e) in tclTHENS - (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; VAR id]))) + (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) [tclTHEN (tclTHEN (mk_then tac1) (intros_using [id1])) (loop act1); tclTHEN (tclTHEN (mk_then tac2) (intros_using [id2])) @@ -1280,8 +1282,8 @@ let replay_history tactic_normalisation = tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| tac_thm; eq1; eq2; - kk; VAR id1; VAR id2 |]]) + (generalize_tac [mkAppL (tac_thm, [| eq1; eq2; + kk; mkVar id1; mkVar id2 |])]) (mk_then tac)) (intros_using [id])) (loop l) @@ -1300,10 +1302,10 @@ let replay_history tactic_normalisation = (tclTHEN (intros_using [aux2;aux1]) (generalize_tac - [mkAppL [| Lazy.force coq_OMEGA7; + [mkAppL (Lazy.force coq_OMEGA7, [| eq1;eq2;kk1;kk2; - VAR aux1;VAR aux2; - VAR id1;VAR id2 |] ])) + mkVar aux1;mkVar aux2; + mkVar id1;mkVar id2 |])])) (clear [aux1;aux2])) (mk_then tac)) (intros_using [id])) @@ -1315,7 +1317,7 @@ let replay_history tactic_normalisation = (tclTHEN (unfold sp_Zgt) simpl_in_concl) reflexivity ] | CONSTANT_NOT_NUL(e,k) :: l -> - tclTHEN (generalize_tac [VAR (hyp_of_tag e)]) Equality.discrConcl + tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl | CONSTANT_NUL(e) :: l -> tclTHEN (resolve_id (hyp_of_tag e)) reflexivity | CONSTANT_NEG(e,k) :: l -> @@ -1325,7 +1327,7 @@ let replay_history tactic_normalisation = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [VAR (hyp_of_tag e)]) + (generalize_tac [mkVar (hyp_of_tag e)]) (unfold sp_Zle)) simpl_in_concl) (unfold sp_not)) @@ -1347,7 +1349,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = let (tac,t') = normalize p_initial t in let shift_left = tclTHEN - (generalize_tac [mkAppL [| theorem; t1; t2; VAR id |] ]) + (generalize_tac [mkAppL (theorem, [| t1; t2; mkVar id |]) ]) (clear [id]) in if tac <> [] then @@ -1475,15 +1477,15 @@ let nat_inject gl = (tclTHEN (clever_rewrite_gen p (mk_minus (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_minus1),[t1;t2;VAR id])) - (loop [id,mkAppL [| Lazy.force coq_le; t2;t1 |]])) + ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])) + (loop [id,mkAppL (Lazy.force coq_le, [| t2;t1 |])])) (explore (P_APP 1 :: p) t1)) (explore (P_APP 2 :: p) t2)); (tclTHEN (clever_rewrite_gen p (mk_integer 0) - ((Lazy.force coq_inj_minus2),[t1;t2;VAR id])) - (loop [id,mkAppL [| Lazy.force coq_gt; t2;t1 |]])) + ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) + (loop [id,mkAppL (Lazy.force coq_gt, [| t2;t1 |])])) ] | Kapp("S",[t']) -> let rec is_number t = @@ -1498,7 +1500,7 @@ let nat_inject gl = Kapp("S",[t]) -> (tclTHEN (clever_rewrite_gen p - (mkAppL [| Lazy.force coq_Zs; mk_inj t |]) + (mkAppL (Lazy.force coq_Zs, [| mk_inj t |])) ((Lazy.force coq_inj_S),[t])) (loop (P_APP 1 :: p) t)) | _ -> explore p t @@ -1507,8 +1509,8 @@ let nat_inject gl = if is_number t' then focused_simpl p else loop p t | Kapp("pred",[t]) -> let t_minus_one = - mkAppL [| Lazy.force coq_minus ; t; - mkAppL [| Lazy.force coq_S; Lazy.force coq_O |] |] in + mkAppL (Lazy.force coq_minus, [| t; + mkAppL (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in tclTHEN (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one ((Lazy.force coq_pred_of_minus),[t])) @@ -1528,8 +1530,8 @@ let nat_inject gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_inj_le; - t1;t2;VAR i |] ]) + [mkAppL (Lazy.force coq_inj_le, + [| t1;t2;mkVar i |]) ]) (explore [P_APP 1; P_TYPE] t1)) (explore [P_APP 2; P_TYPE] t2)) (clear [i])) @@ -1542,8 +1544,8 @@ let nat_inject gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_inj_lt; - t1;t2;VAR i |] ]) + [mkAppL (Lazy.force coq_inj_lt, [| + t1;t2;mkVar i |]) ]) (explore [P_APP 1; P_TYPE] t1)) (explore [P_APP 2; P_TYPE] t2)) (clear [i])) @@ -1556,8 +1558,8 @@ let nat_inject gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_inj_ge; - t1;t2;VAR i |] ]) + [mkAppL (Lazy.force coq_inj_ge, + [| t1;t2;mkVar i |]) ]) (explore [P_APP 1; P_TYPE] t1)) (explore [P_APP 2; P_TYPE] t2)) (clear [i])) @@ -1570,8 +1572,8 @@ let nat_inject gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_inj_gt; - t1;t2;VAR i |] ]) + [mkAppL (Lazy.force coq_inj_gt, [| + t1;t2;mkVar i |]) ]) (explore [P_APP 1; P_TYPE] t1)) (explore [P_APP 2; P_TYPE] t2)) (clear [i])) @@ -1584,8 +1586,8 @@ let nat_inject gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_inj_neq; - t1;t2;VAR i |] ]) + [mkAppL (Lazy.force coq_inj_neq, [| + t1;t2;mkVar i |]) ]) (explore [P_APP 1; P_TYPE] t1)) (explore [P_APP 2; P_TYPE] t2)) (clear [i])) @@ -1599,8 +1601,8 @@ let nat_inject gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_inj_eq; - t1;t2;VAR i |] ]) + [mkAppL (Lazy.force coq_inj_eq, [| + t1;t2;mkVar i |]) ]) (explore [P_APP 2; P_TYPE] t1)) (explore [P_APP 3; P_TYPE] t2)) (clear [i])) @@ -1615,33 +1617,33 @@ let nat_inject gl = let rec decidability gl t = match destructurate t with | Kapp("or",[t1;t2]) -> - mkAppL [| Lazy.force coq_dec_or; t1; t2; - decidability gl t1; decidability gl t2 |] + mkAppL (Lazy.force coq_dec_or, [| t1; t2; + decidability gl t1; decidability gl t2 |]) | Kapp("and",[t1;t2]) -> - mkAppL [| Lazy.force coq_dec_and; t1; t2; - decidability gl t1; decidability gl t2 |] + mkAppL (Lazy.force coq_dec_and, [| t1; t2; + decidability gl t1; decidability gl t2 |]) | Kimp(t1,t2) -> - mkAppL [| Lazy.force coq_dec_imp; t1; t2; - decidability gl t1; decidability gl t2 |] - | Kapp("not",[t1]) -> mkAppL [| Lazy.force coq_dec_not; t1; - decidability gl t1 |] + mkAppL (Lazy.force coq_dec_imp, [| t1; t2; + decidability gl t1; decidability gl t2 |]) + | Kapp("not",[t1]) -> mkAppL (Lazy.force coq_dec_not, [| t1; + decidability gl t1 |]) | Kapp("eq",[typ;t1;t2]) -> begin match destructurate (pf_nf gl typ) with - | Kapp("Z",[]) -> mkAppL [| Lazy.force coq_dec_eq; t1;t2 |] - | Kapp("nat",[]) -> mkAppL [| Lazy.force coq_dec_eq_nat; t1;t2 |] + | Kapp("Z",[]) -> mkAppL (Lazy.force coq_dec_eq, [| t1;t2 |]) + | Kapp("nat",[]) -> mkAppL (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) | _ -> errorlabstrm "decidability" [< 'sTR "Omega: Can't solve a goal with equality on "; Printer.prterm typ >] end - | Kapp("Zne",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zne; t1;t2 |] - | Kapp("Zle",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zle; t1;t2 |] - | Kapp("Zlt",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zlt; t1;t2 |] - | Kapp("Zge",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zge; t1;t2 |] - | Kapp("Zgt",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zgt; t1;t2 |] - | Kapp("le", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_le; t1;t2 |] - | Kapp("lt", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_lt; t1;t2 |] - | Kapp("ge", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_ge; t1;t2 |] - | Kapp("gt", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_gt; t1;t2 |] + | Kapp("Zne",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zne, [| t1;t2 |]) + | Kapp("Zle",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zle, [| t1;t2 |]) + | Kapp("Zlt",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zlt, [| t1;t2 |]) + | Kapp("Zge",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zge, [| t1;t2 |]) + | Kapp("Zgt",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zgt, [| t1;t2 |]) + | Kapp("le", [t1;t2]) -> mkAppL (Lazy.force coq_dec_le, [| t1;t2 |]) + | Kapp("lt", [t1;t2]) -> mkAppL (Lazy.force coq_dec_lt, [| t1;t2 |]) + | Kapp("ge", [t1;t2]) -> mkAppL (Lazy.force coq_dec_ge, [| t1;t2 |]) + | Kapp("gt", [t1;t2]) -> mkAppL (Lazy.force coq_dec_gt, [| t1;t2 |]) | Kapp("False",[]) -> Lazy.force coq_dec_False | Kapp("True",[]) -> Lazy.force coq_dec_True | Kapp(t,_::_) -> error ("Omega: Unrecognized predicate or connective: " @@ -1673,10 +1675,10 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_imp_simp; + (generalize_tac [mkAppL (Lazy.force coq_imp_simp, [| t1; t2; decidability gl t1; - VAR i|]]) + mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd ((i,mk_or (mk_not t1) t2)::lit))) @@ -1687,8 +1689,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_or; - t1; t2; VAR i |]]) + (generalize_tac [mkAppL (Lazy.force coq_not_or,[| + t1; t2; mkVar i |])]) (clear [i])) (intros_using [i])) (loop evbd ((i,mk_and (mk_not t1) (mk_not t2)):: lit))) @@ -1697,8 +1699,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_not_and; t1; t2; - decidability gl t1;VAR i|]]) + [mkAppL (Lazy.force coq_not_and, [| t1; t2; + decidability gl t1;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd ((i,mk_or (mk_not t1) (mk_not t2))::lit))) @@ -1707,8 +1709,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_not_imp; t1; t2; - decidability gl t1;VAR i |]]) + [mkAppL (Lazy.force coq_not_imp, [| t1; t2; + decidability gl t1;mkVar i |])]) (clear [i])) (intros_using [i])) (loop evbd ((i,mk_and t1 (mk_not t2)) :: lit))) @@ -1717,8 +1719,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (generalize_tac - [mkAppL [| Lazy.force coq_not_not; t; - decidability gl t; VAR i |]]) + [mkAppL (Lazy.force coq_not_not, [| t; + decidability gl t; mkVar i |])]) (clear [i])) (intros_using [i])) (loop evbd ((i,t)::lit))) @@ -1726,8 +1728,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_Zle; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_Zle, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1735,8 +1737,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_Zge; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_Zge, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1744,8 +1746,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_Zlt; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_Zlt, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1753,8 +1755,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_Zgt; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_Zgt, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1762,8 +1764,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_le; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_le, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1771,8 +1773,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_ge; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_ge, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1780,8 +1782,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_lt; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_lt, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1789,8 +1791,8 @@ let destructure_hyps gl = (tclTHEN (tclTHEN (tclTHEN - (generalize_tac [mkAppL [| Lazy.force coq_not_gt; - t1;t2;VAR i|]]) + (generalize_tac [mkAppL (Lazy.force coq_not_gt, + [| t1;t2;mkVar i|])]) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1804,7 +1806,7 @@ let destructure_hyps gl = (simplest_elim (applist (Lazy.force coq_not_eq, - [t1;t2;VAR i]))) + [t1;t2;mkVar i]))) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1815,7 +1817,7 @@ let destructure_hyps gl = (simplest_elim (applist (Lazy.force coq_not_Zeq, - [t1;t2;VAR i]))) + [t1;t2;mkVar i]))) (clear [i])) (intros_using [i])) (loop evbd lit)) @@ -1825,12 +1827,12 @@ let destructure_hyps gl = | Kapp("nat",_) -> (tclTHEN (convert_hyp i - (mkAppL [| Lazy.force coq_neq; t1;t2|])) + (mkAppL (Lazy.force coq_neq, [| t1;t2|]))) (loop evbd lit)) | Kapp("Z",_) -> (tclTHEN (convert_hyp i - (mkAppL [| Lazy.force coq_Zne; t1;t2|])) + (mkAppL (Lazy.force coq_Zne, [| t1;t2|]))) (loop evbd lit)) | _ -> loop evbd lit end @@ -1856,8 +1858,8 @@ let destructure_goal gl = (tclTHEN (tclTHEN (Tactics.refine - (mkAppL [| Lazy.force coq_dec_not_not; t; - decidability gl t; mkNewMeta () |])) + (mkAppL (Lazy.force coq_dec_not_not, [| t; + decidability gl t; mkNewMeta () |]))) intro) (destructure_hyps)) in diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 8351357e60..633be8d914 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -189,7 +189,7 @@ let compute_lhs typ i nargsi = match kind_of_term typ with | IsMutInd((sp,0),args) -> let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkAppL (Array.append [| mkMutConstruct (((sp,0),i+1), args) |] argsi) + mkAppL (mkMutConstruct (((sp,0),i+1), args), argsi) | _ -> i_can't_do_that () (*s This function builds the pattern from the RHS. Recursive calls are @@ -199,9 +199,9 @@ let compute_rhs bodyi index_of_f = let rec aux c = match decomp_term c with | IsAppL (Rel j, args) when j = index_of_f (* recursive call *) -> - let i = destRel (list_last args) in mkMeta i + let i = destRel (array_last args) in mkMeta i | IsAppL (f,args) -> - mkAppList f (List.map aux args) + mkAppL (f, Array.map aux args) | IsCast (c,t) -> aux c | _ -> c in @@ -280,7 +280,7 @@ let rec closed_under cset t = (ConstrSet.mem t cset) or (match (kind_of_term t) with | IsCast(c,_) -> closed_under cset c - | IsAppL(f,l) -> List.for_all (closed_under cset) (f::l) + | IsAppL(f,l) -> closed_under cset f & array_for_all (closed_under cset) l | _ -> false) (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete @@ -301,13 +301,13 @@ let btree_of_array a ty = let size_of_a = Array.length a in let semi_size_of_a = size_of_a lsr 1 in let node = Lazy.force coq_Node_vm - and empty = mkAppL [| Lazy.force coq_Empty_vm; ty |] in + and empty = mkAppL (Lazy.force coq_Empty_vm, [| ty |]) in let rec aux n = if n > size_of_a then empty else if n > semi_size_of_a - then mkAppL [| node; ty; a.(n-1); empty; empty |] - else mkAppL [| node; ty; a.(n-1); aux (2*n); aux (2*n+1) |] + then mkAppL (node, [| ty; a.(n-1); empty; empty |]) + else mkAppL (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |]) in aux 1 @@ -324,9 +324,9 @@ let path_of_int n = else (n mod 2 = 1)::(digits_of_int (n lsr 1)) in List.fold_right - (fun b c -> mkAppL [| if b then Lazy.force coq_Right_idx - else Lazy.force coq_Left_idx; - c |]) + (fun b c -> mkAppL ((if b then Lazy.force coq_Right_idx + else Lazy.force coq_Left_idx), + [| c |])) (List.rev (digits_of_int n)) (Lazy.force coq_End_idx) @@ -341,7 +341,7 @@ let path_of_int n = let rec subterm gl (t : constr) (t' : constr) = (pf_conv_x gl t t') or (match (kind_of_term t) with - | IsAppL (f,args) -> List.exists (fun t -> subterm gl t t') args + | IsAppL (f,args) -> array_exists (fun t -> subterm gl t t') args | IsCast(t,_) -> (subterm gl t t') | _ -> false) @@ -426,8 +426,8 @@ let quote f lid gl = | _ -> assert false in match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkAppL [| f ; p |]) gl - | Some _ -> Tactics.convert_concl (mkAppL [| f ; vm; p |]) gl + | None -> Tactics.convert_concl (mkAppL (f, [| p |])) gl + | Some _ -> Tactics.convert_concl (mkAppL (f, [| vm; p |])) gl (*i*) let dyn_quote = function diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 9085041d37..b628956af7 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -172,13 +172,13 @@ let add_theory want_ring want_abstract a aplus amult aone azero aopp aeq t cset let env = Global.env () in if (want_ring & not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkAppL [| Lazy.force coq_Ring_Theory; a; aplus; amult; - aone; azero; aopp; aeq |]))) then + (mkAppL (Lazy.force coq_Ring_Theory, [| a; aplus; amult; + aone; azero; aopp; aeq |])))) then errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >]; if (not want_ring & not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkAppL [| Lazy.force coq_Semi_Ring_Theory; a; - aplus; amult; aone; azero; aeq |]))) then + (mkAppL (Lazy.force coq_Semi_Ring_Theory, [| a; + aplus; amult; aone; azero; aeq |])))) then errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >]; Lib.add_anonymous_leaf (theory_to_obj @@ -299,16 +299,16 @@ let build_spolynom gl th lc = and builds the varmap with side-effects *) let rec aux c = match (kind_of_term (whd_castapp c)) with - | IsAppL (binop,[c1; c2]) when pf_conv_x gl binop th.th_plus -> - mkAppL [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |] - | IsAppL (binop,[c1; c2]) when pf_conv_x gl binop th.th_mult -> - mkAppL [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |] + | IsAppL (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus -> + mkAppA [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |] + | IsAppL (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult -> + mkAppA [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |] | _ when closed_under th.th_closed c -> - mkAppL [| Lazy.force coq_SPconst; th.th_a; c |] + mkAppA [| Lazy.force coq_SPconst; th.th_a; c |] | _ -> try Hashtbl.find varhash c with Not_found -> - let newvar = mkAppL [| Lazy.force coq_SPvar; th.th_a; + let newvar = mkAppA [| Lazy.force coq_SPvar; th.th_a; (path_of_int !counter) |] in begin incr counter; @@ -321,16 +321,16 @@ let build_spolynom gl th lc = let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in List.map (fun p -> - (mkAppL [| Lazy.force coq_interp_sp; th.th_a; th.th_plus; th.th_mult; + (mkAppA [| Lazy.force coq_interp_sp; th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |], - mkAppL [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; + mkAppA [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; pf_reduce cbv_betadeltaiota gl - (mkAppL [| Lazy.force coq_spolynomial_simplify; + (mkAppA [| Lazy.force coq_spolynomial_simplify; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_eq; p|]) |], - mkAppL [| Lazy.force coq_spolynomial_simplify_ok; + mkAppA [| Lazy.force coq_spolynomial_simplify_ok; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_eq; v; th.th_t; p |])) lp @@ -353,24 +353,24 @@ let build_polynom gl th lc = let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = match (kind_of_term (whd_castapp c)) with - | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus -> - mkAppL [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |] - | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult -> - mkAppL [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |] + | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus -> + mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |] + | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult -> + mkAppA [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |] (* The special case of Zminus *) - | IsAppL (binop, [c1; c2]) - when pf_conv_x gl c (mkAppL [| th.th_plus; c1; - mkAppL [| th.th_opp; c2 |] |]) -> - mkAppL [| Lazy.force coq_Pplus; th.th_a; aux c1; - mkAppL [| Lazy.force coq_Popp; th.th_a; aux c2 |] |] - | IsAppL (unop, [c1]) when pf_conv_x gl unop th.th_opp -> - mkAppL [| Lazy.force coq_Popp; th.th_a; aux c1 |] + | IsAppL (binop, [|c1; c2|]) + when pf_conv_x gl c (mkAppA [| th.th_plus; c1; + mkAppA [| th.th_opp; c2 |] |]) -> + mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1; + mkAppA [| Lazy.force coq_Popp; th.th_a; aux c2 |] |] + | IsAppL (unop, [|c1|]) when pf_conv_x gl unop th.th_opp -> + mkAppA [| Lazy.force coq_Popp; th.th_a; aux c1 |] | _ when closed_under th.th_closed c -> - mkAppL [| Lazy.force coq_Pconst; th.th_a; c |] + mkAppA [| Lazy.force coq_Pconst; th.th_a; c |] | _ -> try Hashtbl.find varhash c with Not_found -> - let newvar = mkAppL [| Lazy.force coq_Pvar; th.th_a; + let newvar = mkAppA [| Lazy.force coq_Pvar; th.th_a; (path_of_int !counter) |] in begin incr counter; @@ -383,17 +383,17 @@ let build_polynom gl th lc = let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in List.map (fun p -> - (mkAppL [| Lazy.force coq_interp_p; + (mkAppA [| Lazy.force coq_interp_p; th.th_a; th.th_plus; th.th_mult; th.th_zero; th.th_opp; v; p |], - mkAppL [| Lazy.force coq_interp_cs; + mkAppA [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; pf_reduce cbv_betadeltaiota gl - (mkAppL [| Lazy.force coq_polynomial_simplify; + (mkAppA [| Lazy.force coq_polynomial_simplify; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_opp; th.th_eq; p |]) |], - mkAppL [| Lazy.force coq_polynomial_simplify_ok; + mkAppA [| Lazy.force coq_polynomial_simplify_ok; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_opp; th.th_eq; v; th.th_t; p |])) lp @@ -418,16 +418,16 @@ let build_aspolynom gl th lc = and builds the varmap with side-effects *) let rec aux c = match (kind_of_term (whd_castapp c)) with - | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus -> - mkAppL [| Lazy.force coq_ASPplus; aux c1; aux c2 |] - | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult -> - mkAppL [| Lazy.force coq_ASPmult; aux c1; aux c2 |] + | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus -> + mkAppA [| Lazy.force coq_ASPplus; aux c1; aux c2 |] + | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult -> + mkAppA [| Lazy.force coq_ASPmult; aux c1; aux c2 |] | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0 | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1 | _ -> try Hashtbl.find varhash c with Not_found -> - let newvar = mkAppL [| Lazy.force coq_ASPvar; + let newvar = mkAppA [| Lazy.force coq_ASPvar; (path_of_int !counter) |] in begin incr counter; @@ -440,13 +440,13 @@ let build_aspolynom gl th lc = let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in List.map (fun p -> - (mkAppL [| Lazy.force coq_interp_asp; th.th_a; th.th_plus; th.th_mult; + (mkAppA [| Lazy.force coq_interp_asp; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; p |], - mkAppL [| Lazy.force coq_interp_acs; th.th_a; th.th_plus; th.th_mult; + mkAppA [| Lazy.force coq_interp_acs; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; pf_reduce cbv_betadeltaiota gl - (mkAppL [| Lazy.force coq_aspolynomial_normalize; p|]) |], - mkAppL [| Lazy.force coq_spolynomial_simplify_ok; + (mkAppA [| Lazy.force coq_aspolynomial_normalize; p|]) |], + mkAppA [| Lazy.force coq_spolynomial_simplify_ok; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_eq; v; th.th_t; p |])) lp @@ -469,24 +469,24 @@ let build_apolynom gl th lc = let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = match (kind_of_term (whd_castapp c)) with - | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus -> - mkAppL [| Lazy.force coq_APplus; aux c1; aux c2 |] - | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult -> - mkAppL [| Lazy.force coq_APmult; aux c1; aux c2 |] + | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus -> + mkAppA [| Lazy.force coq_APplus; aux c1; aux c2 |] + | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult -> + mkAppA [| Lazy.force coq_APmult; aux c1; aux c2 |] (* The special case of Zminus *) - | IsAppL (binop, [c1; c2]) - when pf_conv_x gl c (mkAppL [| th.th_plus; c1; - mkAppL [| th.th_opp; c2 |] |]) -> - mkAppL [| Lazy.force coq_APplus; aux c1; - mkAppL [| Lazy.force coq_APopp; aux c2 |] |] - | IsAppL (unop, [c1]) when pf_conv_x gl unop th.th_opp -> - mkAppL [| Lazy.force coq_APopp; aux c1 |] + | IsAppL (binop, [|c1; c2|]) + when pf_conv_x gl c (mkAppA [| th.th_plus; c1; + mkAppA [| th.th_opp; c2 |] |]) -> + mkAppA [| Lazy.force coq_APplus; aux c1; + mkAppA [| Lazy.force coq_APopp; aux c2 |] |] + | IsAppL (unop, [|c1|]) when pf_conv_x gl unop th.th_opp -> + mkAppA [| Lazy.force coq_APopp; aux c1 |] | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0 | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1 | _ -> try Hashtbl.find varhash c with Not_found -> - let newvar = mkAppL [| Lazy.force coq_APvar; + let newvar = mkAppA [| Lazy.force coq_APvar; (path_of_int !counter) |] in begin incr counter; @@ -499,15 +499,15 @@ let build_apolynom gl th lc = let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in List.map (fun p -> - (mkAppL [| Lazy.force coq_interp_ap; + (mkAppA [| Lazy.force coq_interp_ap; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_opp; v; p |], - mkAppL [| Lazy.force coq_interp_sacs; + mkAppA [| Lazy.force coq_interp_sacs; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_opp; v; pf_reduce cbv_betadeltaiota gl - (mkAppL [| Lazy.force coq_apolynomial_normalize; p |]) |], - mkAppL [| Lazy.force coq_apolynomial_normalize_ok; + (mkAppA [| Lazy.force coq_apolynomial_normalize; p |]) |], + mkAppA [| Lazy.force coq_apolynomial_normalize_ok; th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_opp; th.th_eq; v; th.th_t; p |])) lp @@ -565,10 +565,10 @@ let raw_polynom th op lc gl = List.fold_right2 (fun ci (c'i, c''i, c'i_eq_c''i) tac -> tclTHENS - (elim_type (mkAppL [| Lazy.force coq_eqT; th.th_a; c'i; ci |])) + (elim_type (mkAppA [| Lazy.force coq_eqT; th.th_a; c'i; ci |])) [ tclTHENS (elim_type - (mkAppL [| Lazy.force coq_eqT; th.th_a; c''i; c'i |])) + (mkAppA [| Lazy.force coq_eqT; th.th_a; c''i; c'i |])) [ tac; h_exact c'i_eq_c''i ]; h_reflexivity]) @@ -582,10 +582,10 @@ let guess_eq_tac th = polynom_unfold_tac (tclREPEAT (tclORELSE - (apply (mkAppL [| Lazy.force coq_f_equal2; + (apply (mkAppA [| Lazy.force coq_f_equal2; th.th_a; th.th_a; th.th_a; th.th_plus |])) - (apply (mkAppL [| Lazy.force coq_f_equal2; + (apply (mkAppA [| Lazy.force coq_f_equal2; th.th_a; th.th_a; th.th_a; th.th_mult |])))))) diff --git a/kernel/closure.ml b/kernel/closure.ml index 178e5a9de7..783017e8a4 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -395,8 +395,8 @@ let rec norm_head info env t stack = (* stack grows (remove casts) *) | IsAppL (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) - let nargs = List.map (cbv_stack_term info TOP env) args in - norm_head info env head (stack_app nargs stack) + let nargs = Array.map (cbv_stack_term info TOP env) args in + norm_head info env head (stack_app (Array.to_list nargs) stack) | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) | IsCast (ct,_) -> norm_head info env ct stack diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 534a95c944..b8649ffb2e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -175,7 +175,7 @@ let decomp_par n c = snd (mind_extract_params n c) let listrec_mconstr env ntypes nparams i indlc = (* check the inductive types occur positively in [c] *) let rec check_pos n c = - let x,largs = whd_betadeltaiota_stack env Evd.empty c [] in + let x,largs = whd_betadeltaiota_stack env Evd.empty c in match kind_of_term x with | IsProd (na,b,d) -> assert (largs = []); @@ -258,12 +258,23 @@ let listrec_mconstr env ntypes nparams i indlc = and check_construct check_head = let rec check_constr_rec lrec n c = - let x,largs = whd_betadeltaiota_stack env Evd.empty c [] in + let x,largs = whd_betadeltaiota_stack env Evd.empty c in match kind_of_term x with + | IsProd (na,b,d) -> assert (largs = []); let recarg = check_pos n b in - check_constr_rec (recarg::lrec) (n+1) d + check_constr_rec (recarg::lrec) (n+1) d + + (* LetIn's must be free of occurrence of the inductive types and + they do not contribute to recargs *) + | IsLetIn (na,b,t,d) -> + assert (largs = []); + if not (noccur_between n ntypes b & noccur_between n ntypes t) then + raise (IllFormedInd (LocalNonPos n)); + let recarg = check_pos n b in + check_constr_rec lrec (n+1) d + | hd -> if check_head then if hd = IsRel (n+ntypes-i) then diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 569b681e9a..2f5e02ad43 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -182,29 +182,29 @@ let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args) exception Induc let extract_mrectype t = - let (t,l) = whd_stack t [] in - match t with - | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) + let (t, l) = whd_stack t in + match kind_of_term t with + | IsMutInd ind -> (ind, l) | _ -> raise Induc let find_mrectype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ind -> (ind, l) | _ -> raise Induc let find_minductype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd (sp,i),_) - when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ((sp,i),_ as ind) + when mind_type_finite (lookup_mind sp env) i -> (ind, l) | _ -> raise Induc let find_mcoinductype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd (sp,i),_) - when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ((sp,i),_ as ind) + when not (mind_type_finite (lookup_mind sp env) i) -> (ind, l) | _ -> raise Induc (* raise Induc if not an inductive type *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e0c951c224..5c1493e2a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -94,8 +94,9 @@ let rec execute mf env cstr = | IsAppL (f,args) -> let (j,cst1) = execute mf env f in - let (jl,cst2) = execute_list mf env args in - let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck jl j in + let (jl,cst2) = execute_array mf env args in + let (j,cst3) = + apply_rel_list env Evd.empty mf.nocheck (Array.to_list jl) j in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) @@ -205,16 +206,6 @@ let unsafe_infer_type env constr = let type_of env c = let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type) -(* obsolètes -let type_of_type env c = - let tt = safe_infer_type env c in DOP0 (Sort (level_of_type tt.typ) - -let unsafe_type_of env c = - let (j,_) = unsafe_infer env c in nf_betaiota env Evd.empty j.uj_type - -let unsafe_type_of_type env c = - let tt = unsafe_infer_type env c in DOP0 (Sort tt.typ) -*) (* Typing of several terms. *) let safe_infer_l env cl = diff --git a/kernel/term.ml b/kernel/term.ml index 1933483901..e6c5fa4b51 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -495,8 +495,9 @@ let mkNamedProd_wo_LetIn (id,body,t) c = let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) -let mkAppL a = DOPN (AppL, a) -let mkAppList a l = DOPN (AppL, Array.of_list (a::l)) +let mkAppL (f, a) = DOPN (AppL, Array.append [|f|] a) +let mkAppList l = DOPN (AppL, Array.of_list l) +let mkAppA v = DOPN (AppL, v) (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) @@ -609,6 +610,10 @@ let destXtra = function | _ -> invalid_arg "destXtra" (* Destructs a type *) +let isSort = function + | (DOP0 (Sort s)) -> true + | _ -> false + let destSort = function | (DOP0 (Sort s)) -> s | _ -> invalid_arg "destSort" @@ -674,6 +679,10 @@ let under_outer_cast f = function | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t) | c -> f c +let rec under_casts f = function + | DOP2 (Cast,c,t) -> DOP2 (Cast,under_casts f c, t) + | c -> f c + let rec strip_all_casts t = match t with | DOP2 (Cast, b, _) -> strip_all_casts b @@ -779,20 +788,6 @@ 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) - | _ -> invalid_arg "destAbst" - -let path_of_abst = function - | DOPN(Abst sp,_) -> sp - | _ -> anomaly "path_of_abst called with bad args" - -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) @@ -898,7 +893,7 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr - | IsAppL of constr * constr list + | IsAppL of constr * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -924,8 +919,7 @@ let kind_of_term c = | CPrd (x,t1,t2) -> IsProd (x,t1,t2) | CLam (x,t1,t2) -> IsLambda (x,t1,t2) | CLet (x,b,t1,t2) -> IsLetIn (x,b,t1,t2) - | DOPN (AppL,a) when Array.length a <> 0 -> - IsAppL (a.(0), List.tl (Array.to_list a)) + | DOPN (AppL,a) when Array.length a <> 0 -> IsAppL (a.(0), array_tl a) | DOPN (Const sp, a) -> IsConst (sp,a) | DOPN (Evar sp, a) -> IsEvar (sp,a) | DOPN (MutInd ind_sp, l) -> IsMutInd (ind_sp,l) @@ -1922,7 +1916,7 @@ let fold_constr f acc c = match kind_of_term c with | 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 + | IsAppL (c,l) -> Array.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 @@ -1937,7 +1931,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | 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 + | IsAppL (c,l) -> Array.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 @@ -1956,7 +1950,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with | 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 + | IsAppL (c,l) -> f n c; Array.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 @@ -1973,7 +1967,7 @@ let map_constr f c = match kind_of_term c with | 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) + | IsAppL (c,l) -> appvect (f c, Array.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) @@ -1988,7 +1982,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with | 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) + | IsAppL (c,al) -> appvect (f l c, Array.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) diff --git a/kernel/term.mli b/kernel/term.mli index fe3996c5c6..fa0d076730 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -134,7 +134,7 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr - | IsAppL of constr * constr list + | IsAppL of constr * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -216,10 +216,11 @@ val mkNamedLambda : identifier -> constr -> constr -> constr (* [mkLambda_string s t c] constructs $[s:t]c$ *) val mkLambda_string : string -> constr -> constr -> constr -(* If $a = [| t_1; \dots; t_n |]$, constructs the application - $(t_1~\dots~t_n)$. *) -val mkAppL : constr array -> constr -val mkAppList : constr -> constr list -> constr +(* [mkAppL (f,[| t_1; ...; t_n |]] constructs the application + $(f~t_1~\dots~t_n)$. *) +val mkAppL : constr * constr array -> constr +val mkAppList : constr list -> constr +val mkAppA : constr array -> constr (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) @@ -307,6 +308,7 @@ val is_Set : constr -> bool val isprop : constr -> bool val is_Type : constr -> bool val iskind : constr -> bool +val isSort : constr -> bool val is_existential_oper : sorts oper -> bool @@ -324,6 +326,9 @@ val strip_outer_cast : constr -> constr (* Special function, which keep the key casts under Fix and MutCase. *) val strip_all_casts : constr -> constr +(* Apply a function letting Casted types in place *) +val under_casts : (constr -> constr) -> constr -> constr + (* Tests if a de Bruijn index *) val isRel : constr -> bool diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 078b6b96b1..58295ee35e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -337,6 +337,7 @@ let apply_rel_list env sigma nocheck argjl funj = error_cant_apply_bad_type CCI env sigma (n,body_of_type hj.uj_type,c1) funj argjl) + | _ -> error_cant_apply_not_functional CCI env funj argjl in @@ -395,13 +396,13 @@ let check_term env mind_recvec f = crec let is_inst_var env sigma k c = - match whd_betadeltaiota_stack env sigma c [] with - | (Rel n,_) -> n=k + match kind_of_term (fst (whd_betadeltaiota_stack env sigma c)) with + | IsRel n -> n=k | _ -> false let is_subterm_specif env sigma lcx mind_recvec = let rec crec n lst c = - let f,l = whd_betadeltaiota_stack env sigma c [] in + let f,l = whd_betadeltaiota_stack env sigma c in match kind_of_term f with | IsRel k -> find_sorted_assoc k lst @@ -495,7 +496,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = (* n gives the index of the recursive variable *) (noccur_with_meta (n+k+1) nfi t) or (* no recursive call in the term *) - (let f,l = whd_betadeltaiota_stack env sigma t [] in + (let f,l = whd_betadeltaiota_stack env sigma t in match kind_of_term f with | IsRel p -> if n+k+1 <= p & p < n+k+nfi+1 then @@ -617,7 +618,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsAppL (f,la) -> (check_rec_call n lst f) && - (List.for_all (check_rec_call n lst) la) && + (array_for_all (check_rec_call n lst) la) && (List.for_all (check_rec_call n lst) l) | IsCoFix (i,(typarray,funnames,bodies)) -> @@ -686,15 +687,16 @@ let check_guard_rec_meta env sigma nbfix def deftype = let rec check_rec_call alreadygrd n vlra t = if noccur_with_meta n nbfix t then true - else - match whd_betadeltaiota_stack env sigma t [] with - | (DOP0 (Meta _), l) -> true + else + let c,args = whd_betadeltaiota_stack env sigma t in + match kind_of_term c with + | IsMeta _ -> true - | (Rel p,l) -> + | IsRel p -> if n <= p && p < n+nbfix then (* recursive call *) if alreadygrd then - if List.for_all (noccur_with_meta n nbfix) l then + if List.for_all (noccur_with_meta n nbfix) args then true else raise (CoFixGuardError NestedRecursiveOccurrences) @@ -703,7 +705,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = else error "check_guard_rec_meta: ???" (* ??? *) - | (DOPN (MutConstruct(_,i as cstr_sp),l), args) -> + | IsMutConstruct ((_,i as cstr_sp),l) -> let lra =vlra.(i-1) in let mI = inductive_of_constructor (cstr_sp,l) in let mis = lookup_mind_specif mI env in @@ -741,38 +743,37 @@ let check_guard_rec_meta env sigma nbfix def deftype = in (process_args_of_constr realargs lra) - | (DOP2(Lambda,a,DLAM(_,b)),[]) -> + | IsLambda (_,a,b) -> + assert (args = []); if (noccur_with_meta n nbfix a) then check_rec_call alreadygrd (n+1) vlra b else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) - | (DOPN(CoFix(j),vargs) as cofix,l) -> - if (List.for_all (noccur_with_meta n nbfix) l) + | IsCoFix (j,(varit,lna,vdefs)) -> + if (List.for_all (noccur_with_meta n nbfix) args) then - let (j,(varit,lna,vdefs)) = destFix cofix in let nbfix = Array.length vdefs in if (array_for_all (noccur_with_meta n nbfix) varit) then (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) && - (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) + (List.for_all (check_rec_call alreadygrd (n+1) vlra) args) else - raise (CoFixGuardError (RecCallInTypeOfDef cofix)) + raise (CoFixGuardError (RecCallInTypeOfDef c)) else - raise (CoFixGuardError (UnguardedRecursiveCall cofix)) + raise (CoFixGuardError (UnguardedRecursiveCall c)) - | (DOPN(MutCase _,_) as mc,l) -> - let (_,p,c,vrest) = destCase mc in + | IsMutCase (_,p,tm,vrest) -> if (noccur_with_meta n nbfix p) then - if (noccur_with_meta n nbfix c) then - if (List.for_all (noccur_with_meta n nbfix) l) then + if (noccur_with_meta n nbfix tm) then + if (List.for_all (noccur_with_meta n nbfix) args) then (array_for_all (check_rec_call alreadygrd n vlra) vrest) else - raise (CoFixGuardError (RecCallInCaseFun mc)) + raise (CoFixGuardError (RecCallInCaseFun c)) else - raise (CoFixGuardError (RecCallInCaseArg mc)) + raise (CoFixGuardError (RecCallInCaseArg c)) else - raise (CoFixGuardError (RecCallInCasePred mc)) + raise (CoFixGuardError (RecCallInCasePred c)) | _ -> raise (CoFixGuardError NotGuardedForm) @@ -790,32 +791,6 @@ let check_cofix env sigma (bodynum,(types,names,bodies)) = with CoFixGuardError err -> error_ill_formed_rec_body CCI env err (List.rev names) i bodies done -(* -let check_cofix env sigma f = - match f with - | DOPN(CoFix(j),vargs) -> - let nbfix = let nv = Array.length vargs in - if nv < 2 then - error "Ill-formed recursive definition" - else - nv-1 - in - let varit = Array.sub vargs 0 nbfix in - let ldef = array_last vargs in - let la = Array.length varit in - let (lna,vdefs) = decomp_DLAMV_name la ldef in - let vlna = Array.of_list lna in - let check_type i = - try - let _ = - check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in - () - with UserError (s,str) -> - error_ill_formed_rec_body CCI env str lna i vdefs - in - for i = 0 to nbfix-1 do check_type i done - | _ -> assert false -*) (* Checks the type of a (co)fixpoint. Fix and CoFix are typed the same way; only the guard condition differs. *) @@ -856,7 +831,7 @@ 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 - | IsAppL (_,cl) -> List.iter control_rec cl + | IsAppL (_,cl) -> Array.iter control_rec cl | IsCast (c1,c2) -> control_rec c1; control_rec c2 | IsProd (_,c1,c2) -> control_rec c1; control_rec c2 | IsLambda (_,c1,c2) -> control_rec c1; control_rec c2 diff --git a/library/declare.ml b/library/declare.ml index 5d62f067a7..33fb0f284a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -314,15 +314,11 @@ let global_reference kind id = let global_reference_imps kind id = let c = global_reference kind id in - match c with - | DOPN (Const sp,_) -> - c, list_of_implicits (constant_implicits sp) - | DOPN (MutInd (sp,i),_) -> - c, list_of_implicits (inductive_implicits (sp,i)) - | DOPN (MutConstruct ((sp,i),j),_) -> - c, list_of_implicits (constructor_implicits ((sp,i),j)) - | VAR id -> - c, implicits_of_var id + match kind_of_term c with + | IsConst (sp,_) -> c, list_of_implicits (constant_implicits sp) + | IsMutInd (isp,_) -> c, list_of_implicits (inductive_implicits isp) + | IsMutConstruct (csp,_) -> c,list_of_implicits (constructor_implicits csp) + | IsVar id -> c, implicits_of_var id | _ -> assert false (* let global env id = diff --git a/library/indrec.ml b/library/indrec.ml index 655db9af7e..59e11cbff8 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -93,14 +93,14 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs = let st = hnf_prod_appvect env sigma t vargs in let process_pos depK pk = let rec prec i p = - let p',largs = whd_betadeltaiota_stack env sigma p [] in + let p',largs = whd_betadeltaiota_stack env sigma p in match kind_of_term p' with | IsProd (n,t,c) -> assert (largs=[]); make_prod env (n,t,prec (i+1) c) | IsMutInd (_,_) -> let (_,realargs) = list_chop nparams largs in let base = applist (lift i pk,realargs) in if depK then - mkAppList base [appvect (Rel (i+1),rel_vect 0 i)] + mkAppL (base, [|appvect (Rel (i+1),rel_vect 0 i)|]) else base | _ -> assert false @@ -108,7 +108,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs = prec 0 in let rec process_constr i c recargs co = - let c', largs = whd_betadeltaiota_stack env sigma c [] in + let c', largs = whd_betadeltaiota_stack env sigma c in match kind_of_term c' with | IsProd (n,t,c_0) -> assert (largs = []); @@ -124,20 +124,20 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs = (match optionpos with | None -> make_prod env (n,t,process_constr (i+1) c_0 rest - (mkAppList (lift 1 co) [Rel 1])) + (mkAppL (lift 1 co, [|Rel 1|]))) | Some(dep',p) -> let nP = lift (i+1+decP) p in let t_0 = process_pos dep' nP (lift 1 t) in make_prod_dep (dep or dep') env (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest - (mkAppList (lift 2 co) [Rel 2])))) + (mkAppL (lift 2 co, [|Rel 2|]))))) | IsMutInd ((_,tyi),_) -> let nP = match depPvect.(tyi) with | Some(_,p) -> lift (i+decP) p | _ -> assert false in let (_,realargs) = list_chop nparams largs in let base = applist (nP,realargs) in - if dep then mkAppList base [co] else base + if dep then mkAppL (base, [|co|]) else base | _ -> assert false in process_constr 0 st recargs (appvect(co,vargs)) @@ -145,7 +145,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs = let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = let process_pos fk = let rec prec i p = - let p',largs = whd_betadeltaiota_stack env sigma p [] in + let p',largs = whd_betadeltaiota_stack env sigma p in match kind_of_term p' with | IsProd (n,t,c) -> lambda_name env (n,t,prec (i+1) c) | IsMutInd _ -> @@ -170,14 +170,14 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = | None -> lambda_name env (n,incast_type t,process_constr (i+1) - (applist(whd_beta_stack (lift 1 f) [(Rel 1)])) + (whd_beta (applist (lift 1 f, [(Rel 1)]))) (cprest,rest)) | Some(_,f_0) -> let nF = lift (i+1+decF) f_0 in let arg = process_pos nF (lift 1 (body_of_type t)) in lambda_name env (n,incast_type t,process_constr (i+1) - (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) + (whd_beta (applist (lift 1 f, [(Rel 1); arg]))) (cprest,rest))) | (n,Some c,t)::cprest, rest -> failwith "TODO" | [],[] -> f diff --git a/library/redinfo.ml b/library/redinfo.ml index 6bd08a2ff8..ecd977e561 100644 --- a/library/redinfo.ml +++ b/library/redinfo.ml @@ -30,7 +30,7 @@ exception Elimconst let compute_consteval c = let rec srec n labs c = - let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c [] in + let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c in match kind_of_term c' with | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g | IsFix ((nv,i),(tys,_,bds)) -> diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 1a2cc53aef..af2f73b130 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -112,8 +112,8 @@ let ids_of_ctxt ctxt = let maybe_constructor env s = try - match Declare.global_reference CCI (id_of_string s) with - | DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl) + match kind_of_term (Declare.global_reference CCI (id_of_string s)) with + | IsMutConstruct ((spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl) | _ -> warning ("Defined identifier " ^s^" is here considered as a matching variable"); None with Not_found -> @@ -156,13 +156,12 @@ let dbize_global loc = function | _ -> anomaly_loc (loc,"dbize_global", [< 'sTR "Bad ast for this global a reference">]) -let ref_from_constr = function - | DOPN (Const sp,ctxt) -> RConst (sp, dbize_constr_ctxt ctxt) - | DOPN (Evar ev,ctxt) -> REVar (ev, dbize_constr_ctxt ctxt) - | DOPN (MutConstruct (spi,j),ctxt) -> - RConstruct ((spi,j), dbize_constr_ctxt ctxt) - | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), dbize_constr_ctxt ctxt) - | VAR id -> RVar id (* utilisé pour coe_value (tmp) *) +let ref_from_constr c = match kind_of_term c with + | IsConst (sp,ctxt) -> RConst (sp, dbize_constr_ctxt ctxt) + | IsEvar (ev,ctxt) -> REVar (ev, dbize_constr_ctxt ctxt) + | IsMutConstruct (csp,ctxt) -> RConstruct (csp, dbize_constr_ctxt ctxt) + | IsMutInd (isp,ctxt) -> RInd (isp, dbize_constr_ctxt ctxt) + | IsVar id -> RVar id (* utilisé pour coe_value (tmp) *) | _ -> anomaly "Not a reference" (* [vars1] is a set of name to avoid (used for the tactic language); @@ -469,14 +468,14 @@ let ast_adjust_consts sigma = (* locations are kept *) ast else try - match Declare.global_reference CCI id with - | DOPN (Const sp,_) -> + match kind_of_term (Declare.global_reference CCI id) with + | IsConst (sp,_) -> Node(loc,"CONST",[path_section loc sp]) - | DOPN (Evar ev,_) -> + | IsEvar (ev,_) -> Node(loc,"EVAR",[Num(loc,ev)]) - | DOPN (MutConstruct ((sp,i),j),_) -> + | IsMutConstruct (((sp,i),j),_) -> Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j]) - | DOPN (MutInd (sp,i),_) -> + | IsMutInd ((sp,i),_) -> Node (loc,"MUTIND",[path_section loc sp;num i]) | _ -> anomaly "Not a reference" with UserError _ | Not_found -> diff --git a/parsing/pattern.ml b/parsing/pattern.ml index f84a2d929c..47c1d5716d 100644 --- a/parsing/pattern.ml +++ b/parsing/pattern.ml @@ -64,11 +64,11 @@ let rec head_pattern_bound t = | PRel _ | PMeta _ | PSoApp _ | PSort _ -> raise BoundPattern | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type" -let head_of_constr_reference = function - | DOPN (Const sp,_) -> ConstNode sp - | DOPN (MutConstruct sp,_) -> CstrNode sp - | DOPN (MutInd sp,_) -> IndNode sp - | VAR id -> VarNode id +let head_of_constr_reference c = match kind_of_term c with + | IsConst (sp,_) -> ConstNode sp + | IsMutConstruct (sp,_) -> CstrNode sp + | IsMutInd (sp,_) -> IndNode sp + | IsVar id -> VarNode id | _ -> anomaly "Not a rigid reference" @@ -166,8 +166,7 @@ let matches_core convert pat c = | PSort RType, IsSort (Type _) -> sigma | PApp (c1,arg1), IsAppL (c2,arg2) -> - array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) - arg1 (Array.of_list arg2) + array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) -> sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 @@ -221,7 +220,7 @@ let rec try_matches nocc pat = function let rec sub_match nocc pat c = match kind_of_term c with | IsCast (c1,c2) -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1] in (lm,mkCast (List.hd lc, c2)) @@ -229,7 +228,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in (lm,mkCast (List.hd lc, c2))) | IsLambda (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;c2] in (lm,mkLambda (x,List.hd lc,List.nth lc 1)) @@ -237,7 +236,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in (lm,mkLambda (x,List.hd lc,List.nth lc 1))) | IsProd (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;c2] in (lm,mkProd (x,List.hd lc,List.nth lc 1)) @@ -245,7 +244,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in (lm,mkProd (x,List.hd lc,List.nth lc 1))) | IsLetIn (x,c1,t2,c2) -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)) @@ -253,15 +252,15 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))) | IsAppL (c1,lc) -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with | PatternMatchingFailure -> - let (lm,le) = try_sub_match nocc pat (c1::lc) in - (lm,mkAppL (Array.of_list le)) + let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in + (lm,mkAppList le) | NextOccurrence nocc -> - let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in - (lm,mkAppL (Array.of_list le))) + let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in + (lm,mkAppList le)) | IsMutCase (ci,hd,c1,lc) -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with | PatternMatchingFailure -> let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)) @@ -270,7 +269,7 @@ let rec sub_match nocc pat c = (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))) | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _ | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ -> - (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with | PatternMatchingFailure -> raise (NextOccurrence nocc) | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) @@ -311,8 +310,7 @@ let rec pattern_of_constr t = | IsLambda (na,c,b) -> PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b) | IsAppL (f,args) -> - PApp (pattern_of_constr f, - Array.of_list (List.map pattern_of_constr args)) + PApp (pattern_of_constr f, Array.map pattern_of_constr args) | IsConst (cst_sp,ctxt) -> PRef (RConst (cst_sp, ctxt)) | IsMutInd (ind_sp,ctxt) -> diff --git a/parsing/pretty.ml b/parsing/pretty.ml index d9e22af376..a6f4bdb0e6 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -349,8 +349,8 @@ let crible (fn : string -> env -> constr -> unit) name = let mib = Global.lookup_mind sp in let arities = array_map_to_list (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mib.mind_packets in let env_ar = push_rels arities env in - (match const with - | (DOPN(MutInd(sp',tyi),_)) -> + (match kind_of_term const with + | IsMutInd ((sp',tyi),_) -> if sp = objsp_of sp' then print_constructors fn env_ar (mind_nth_type_packet mib tyi) @@ -493,7 +493,7 @@ let unfold_head_fconst = let rec unfrec k = match kind_of_term k with | IsConst _ -> constant_value (Global.env ()) k | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b) - | IsAppL (f,v) -> applist (unfrec f,v) + | IsAppL (f,v) -> appvect (unfrec f,v) | _ -> k in unfrec @@ -502,8 +502,9 @@ let unfold_head_fconst = let print_extracted_name name = let (sigma,(sign,fsign)) = initial_sigma_assumptions() in try - match (Machops.global (gLOB sign) name) with - | DOPN(Const _,_) as x -> + let x = (Machops.global (gLOB sign) name) in + match kind_of_term x with + | IsConst _ -> let cont = snd(infexecute sigma (sign,fsign) x) in (match cont with | Inf {_VAL=trm; _TYPE=typ} -> @@ -519,7 +520,7 @@ let print_extracted_name name = [< >]; 'sTR " : "; fprterm typ; 'fNL >]) | _ -> error "Non informative term") - | VAR id -> + | IsVar id -> (* Pourquoi on n'utilise pas fsign ? *) let a = snd(lookup_sign id sign) in let cont = snd(infexecute sigma (sign,fsign) a.body) in @@ -530,14 +531,14 @@ let print_extracted_name name = fprint_var (string_of_id name) {body=t;typ=s}) | _ -> error "Non informative term") - | DOPN(MutInd (sp,_),_) as x -> + | IsMutInd ((sp,_),_) -> let cont = snd(infexecute sigma (sign,fsign) x) in (match cont with | Inf _ -> (hOV 0 [< 'sTR (string_of_id name); 'sTR " ==>"; 'bRK(1,4); print_extracted_mutual sp >]) | _ -> error "Non informative term") - | DOPN(MutConstruct _ ,_) as x -> + | IsMutConstruct _ -> let cont = snd(infexecute sigma (sign,fsign) x) in (match cont with | Inf d -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1e48d3443c..0745081760 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -74,13 +74,6 @@ let count_rec_arg j = in crec 0 -(* Used in Program only *) -let make_case_ml isrec pred c ci lf = - if isrec then - DOPN(XTRA("REC"),Array.append [|pred;c|] lf) - else - 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 * [a_bar:A'_bar](lift k pred) @@ -160,11 +153,11 @@ let insert_lifted a = (0,a);; (* INVARIANT: - The pattern variables of it are the disjoint union of [user_ids] - and the domain of [subst]. Non global VAR in the codomain of [subst] are - in private_ids. - The non pattern variables of it + the global VAR in the codomain of - [subst] are in others_ids + The pattern variables for [it] are the disjoint union of [user_ids] + and the domain of [subst]. Non global Var in the codomain of [subst] are + in [private_ids]. + The non pattern variables of [it] + the global Var in the codomain of + [subst] are in [other_ids] *) @@ -496,7 +489,14 @@ let push_rels_eqn sign eqn = {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign' eqn.rhs.rhs_env} } - +(* +let push_decls_eqn sign eqn = + let pats = List.rev (fst (list_chop (List.length sign) eqn.patterns)) in + let sign' = recover_pat_names (sign, pats) in + {eqn with + rhs = {eqn.rhs with + rhs_env = push_decls sign' eqn.rhs.rhs_env} } +*) let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } (* @@ -510,19 +510,10 @@ let pop_pattern eqn = { eqn with patterns = List.tl eqn.patterns } exception Occur let noccur_between_without_evar n m term = - let rec occur_rec n = function - | Rel(p) -> if n<=p && p<n+m then raise Occur - | VAR _ -> () - | DOPN(Evar _,cl) -> () - | DOPN(_,cl) -> Array.iter (occur_rec n) cl - | DOP1(_,c) -> occur_rec n c - | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2 - | DLAM(_,c) -> occur_rec (n+1) c - | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v - | CLam (_,t,c) -> occur_rec n (body_of_type t); occur_rec (n+1) c - | CPrd (_,t,c) -> occur_rec n (body_of_type t); occur_rec (n+1) c - | CLet (_,b,t,c) -> occur_rec n b; occur_rec n (body_of_type t); occur_rec (n+1) c - | _ -> () + let rec occur_rec n c = match kind_of_term c with + | IsRel p -> if n<=p && p<n+m then raise Occur + | IsEvar (_,cl) -> () + | _ -> iter_constr_with_binders succ occur_rec n c in try occur_rec n term; true with Occur -> false @@ -1075,15 +1066,20 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)= (* with the type of arguments to match *) let pred = prepare_predicate typing_fun isevars env tomatchs predopt in + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) let initial_pushed = List.map (fun tm -> Pushed (insert_lifted (tm,NotDepInRhs))) tomatchs in + let initial_sign = + List.map (fun (_,t) -> (Anonymous, type_of_tomatch_type t)) tomatchs in + let matx_with_initial_aliases = (*List.map (push_rels_eqn initial_sign) *)matx in let pb = { env = env; isevars = isevars; pred = pred; tomatch = initial_pushed; - mat = matx; + mat = matx_with_initial_aliases; typing_function = typing_fun } in let j = compile pb in diff --git a/pretyping/class.ml b/pretyping/class.ml index 6c0da8c204..ee759ad96d 100644 --- a/pretyping/class.ml +++ b/pretyping/class.ml @@ -127,7 +127,7 @@ let constructor_at_head1 t = | IsVar id -> t',[],[],CL_Var id,0 | IsCast (c,_) -> aux c | IsAppL(f,args) -> - let t',_,l,c,_ = aux f in t',args,l,c,List.length args + let t',_,l,c,_ = aux f in t',Array.to_list args,l,c,Array.length args | IsProd (_,_,_) -> t',[],[],CL_FUN,0 | IsLetIn (_,_,_,c) -> aux c | IsSort _ -> t',[],[],CL_SORT,0 diff --git a/pretyping/classops.ml b/pretyping/classops.ml index f5af725b26..d8475e50e3 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -20,11 +20,11 @@ type cte_typ = | NAM_Inductive of inductive_path | NAM_Constructor of constructor_path -let cte_of_constr = function - | DOPN(Const sp,_) -> NAM_Constant sp - | DOPN(MutInd ind_sp,_) -> NAM_Inductive ind_sp - | DOPN(MutConstruct cstr_cp,_) -> NAM_Constructor cstr_cp - | VAR id -> NAM_Var id +let cte_of_constr c = match kind_of_term c with + | IsConst (sp,_) -> NAM_Constant sp + | IsMutInd (ind_sp,_) -> NAM_Inductive ind_sp + | IsMutConstruct (cstr_cp,_) -> NAM_Constructor cstr_cp + | IsVar id -> NAM_Var id | _ -> raise Not_found type cl_typ = @@ -196,7 +196,7 @@ let constructor_at_head t = | IsLetIn (_,_,_,c) -> aux c | IsSort _ -> CL_SORT,0 | IsCast (c,_) -> aux (collapse_appl c) - | IsAppL (f,args) -> let c,_ = aux f in c, List.length args + | IsAppL (f,args) -> let c,_ = aux f in c, Array.length args | _ -> raise Not_found in aux (collapse_appl t) @@ -217,13 +217,7 @@ let class_of env sigma t = in if n = n1 then t,i else raise Not_found -let rec class_args_of c = - let aux = function - | (DOP2(Cast,c,_)) -> class_args_of c - | (DOPN(AppL,cl)) -> Array.to_list(array_tl cl) - | _ -> [] - in - aux (collapse_appl c) +let class_args_of c = snd (decomp_app c) (* verfications pour l'ajout d'une classe *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7197110bf3..c298852f40 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -80,14 +80,14 @@ let inh_tosort_force env isevars j = let inh_tosort env isevars j = let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in - match typ with - | DOP0(Sort _) -> j (* idem inh_app_fun *) + match kind_of_term typ with + | IsSort _ -> j (* idem inh_app_fun *) | _ -> inh_tosort_force env isevars j let inh_ass_of_j env isevars j = let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in - match typ with - | DOP0(Sort s) -> { utj_val = j.uj_val; utj_type = s } + match kind_of_term typ with + | IsSort s -> { utj_val = j.uj_val; utj_type = s } | _ -> let j1 = inh_tosort_force env isevars j in type_judgment env !isevars j1 @@ -147,7 +147,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = {uj_val = Rel 1; uj_type = typed_app (fun _ -> u1) assu1 } in let h2 = inh_conv_coerce_to_fail env isevars u2 - { uj_val = DOPN(AppL,[|(lift 1 v);h1.uj_val|]); + { uj_val = mkAppL (lift 1 v, [|h1.uj_val|]); uj_type = get_assumption_of env1 !isevars (subst1 h1.uj_val t2) } in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ce72f7e011..0801d8f2c3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -49,33 +49,7 @@ let occur_id env id0 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 (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_names = 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_names t = let rec next id = if List.mem id l or occur_id env_names id t then next (lift_ident id) @@ -314,7 +288,7 @@ let rec detype avoid env t = | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c | IsAppL (f,args) -> - RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args) + RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args) | IsConst (sp,cl) -> RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) | IsEvar (ev,cl) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4f551f31dd..0a400a3a6d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -44,12 +44,15 @@ open Evarutil * ass. *) -let rec evar_apprec env isevars stack c = - let (t,stack) = Reduction.apprec env !isevars c stack in - if ise_defined isevars t then - evar_apprec env isevars stack (existential_value !isevars (destEvar t)) - else - (t,stack) +let evar_apprec env isevars stack c = + let rec aux s = + let (t,stack as s') = Reduction.apprec env !isevars s in + match kind_of_term t with + | IsEvar (n,_ as ev) when Evd.is_defined !isevars n -> + aux (existential_value !isevars ev, stack) + | _ -> (t, list_of_stack stack) + in aux (c, append_stack (Array.of_list stack) empty_stack) + let conversion_problems = ref ([] : (conv_pb * constr * constr) list) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index e94ac55d39..c360df8695 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -153,12 +153,12 @@ let ise_map isevars sp = Evd.map !isevars sp let ise_define isevars sp body = isevars := Evd.define !isevars sp body (* Does k corresponds to an (un)defined existential ? *) -let ise_undefined isevars = function - | DOPN(Evar n,_) -> not (Evd.is_defined !isevars n) +let ise_undefined isevars c = match kind_of_term c with + | IsEvar (n,_) -> not (Evd.is_defined !isevars n) | _ -> false -let ise_defined isevars = function - | DOPN(Evar n,_) -> Evd.is_defined !isevars n +let ise_defined isevars c = match kind_of_term c with + | IsEvar (n,_) -> Evd.is_defined !isevars n | _ -> false let restrict_hyps isevars c = @@ -180,6 +180,22 @@ let has_ise sigma t = * conversion test that lead to the faulty call to [real_clean] should return * false. The problem is that we won't get the right error message. *) + +let real_clean isevars sp args rhs = + let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in + let rec subs k t = + match kind_of_term t with + |IsRel i -> + if i<=k then t + else (try List.assoc (Rel (i-k)) subst with Not_found -> t) + | IsVar _ -> (try List.assoc t subst with Not_found -> t) + | _ -> map_constr_with_binders (fun na k -> k+1) subs k t + in + let body = subs 0 rhs in + (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *) + body + +(* let real_clean isevars sp args rhs = let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in let rec subs k t = @@ -201,6 +217,7 @@ let real_clean isevars sp args rhs = let body = subs 0 rhs in (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *) body +*) let make_instance_with_rel env = let n = rel_context_length (rel_context env) in @@ -233,7 +250,7 @@ let new_isevar isevars env typ k = evar (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated - * evar, i.e. tries to find the body ?sp for lhs=DOPN(Const sp,args) + * evar, i.e. tries to find the body ?sp for lhs=mkConst (sp,args) * ?sp [ sp.hyps \ args ] unifies to rhs * ?sp must be a closed term, not referring to itself. * Not so trivial because some terms of args may be terms that are not @@ -340,29 +357,28 @@ let has_undefined_isevars isevars c = let head_is_exist isevars = let rec hrec k = match kind_of_term k with | IsEvar _ -> ise_undefined isevars k - | IsAppL (f,l) -> hrec f + | IsAppL (f,_) -> hrec f | IsCast (c,_) -> hrec c | _ -> false in hrec -let rec is_eliminator = function - | DOPN (AppL,_) -> true - | DOPN (MutCase _,_) -> true - | DOP2 (Cast,c,_) -> is_eliminator c +let rec is_eliminator c = match kind_of_term c with + | IsAppL _ -> true + | IsMutCase _ -> true + | IsCast (c,_) -> is_eliminator c | _ -> false let head_is_embedded_exist isevars c = (head_is_exist isevars c) & (is_eliminator c) let head_evar = - let rec hrec = function - | DOPN(Evar ev,_) -> ev - | DOPN(MutCase _,_) as mc -> - let (_,_,c,_) = destCase mc in hrec c - | DOPN(AppL,cl) -> hrec (array_hd cl) - | DOP2(Cast,c,_) -> hrec c - | _ -> failwith "headconstant" + let rec hrec c = match kind_of_term c with + | IsEvar (ev,_) -> ev + | IsMutCase (_,_,c,_) -> hrec c + | IsAppL (c,_) -> hrec c + | IsCast (c,_) -> hrec c + | _ -> failwith "headconstant" in hrec diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 41f1878d6b..5743d7d063 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -27,38 +27,6 @@ open Coercion open Inductive open Instantiate -(* -(* Pour le vieux "match" que Program utilise encore, vieille histoire ... *) - -(* Awful special reduction function which skips abstraction on Xtra in - order to be safe for Program ... *) - -let stacklamxtra recfun = - let rec lamrec sigma s t = match s,kind_of_term t with - | (stack, IsLambda (_,DOP1(XTRA "COMMENT",_),_)) -> - recfun stack (substl sigma t) - | ((h::t), IsLambda (_,_,c)) -> lamrec (h::sigma) t c - | (stack, _) -> recfun stack (substl sigma t) - in - lamrec - -let rec whrec x stack = - match kind_of_term x with - | IsLambda (name, DOP1(XTRA "COMMENT",c),t) -> - let t' = applist (whrec t (List.map (lift 1) stack)) in - mkLambda (name,DOP1(XTRA "COMMENT",c),t'),[] - | IsLambda (name,c1,c2) -> - (match stack with - | [] -> mkLambda (name,c1,whd_betaxtra c2),[] - | a1::rest -> stacklamxtra (fun l x -> whrec x l) [a1] rest c2) - | IsAppL (f,args) -> whrec f (args@stack) - | IsCast (c,_) -> whrec c stack - | _ -> x,stack - -and whd_betaxtra x = applist(whrec x []) -*) -let whd_betaxtra = whd_beta - let lift_context n l = let k = List.length l in list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l @@ -85,7 +53,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = let branches = array_map3 (fun f t reca -> - whd_betaxtra + whd_beta (Indrec.make_rec_branch_arg env sigma (nparams,depFvec,nar+1) f t reca)) @@ -109,9 +77,9 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = (List.map (lift nar) params) (rel_list 0 nar))), (if dep then - applist (whd_beta_stack (lift (nar+1) p) (rel_list 0 (nar+1))) + whd_beta (applist (lift (nar+1) p, rel_list 0 (nar+1))) else - applist (whd_beta_stack (lift (nar+1) p) (rel_list 1 nar))))) + whd_beta (applist (lift (nar+1) p, rel_list 1 nar))))) lnames in let fix = mkFix (([|nar|],0), @@ -258,7 +226,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) user_err_loc (loc,"pretype", [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >]) in - { uj_val=DOP0 (Meta n); uj_type = outcast_type metaty }) + { uj_val= mkMeta n; uj_type = outcast_type metaty }) | RHole loc -> if !compter then nbimpl:=!nbimpl+1; @@ -464,12 +432,13 @@ let process_evars fail_evar env sigma = [< 'sTR"There is an unknown subterm I cannot solve" >] else whd_ise1_metas env sigma) - +(* let j_apply f env sigma j = - let under_outer_cast f env sigma = function - | DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t) - | c -> f env sigma c in - { uj_val=strong (under_outer_cast f) env sigma j.uj_val; + { uj_val= local_strong (under_outer_cast (f env sigma)) j.uj_val; + uj_type= typed_app (strong f env sigma) j.uj_type } +*) +let j_apply f env sigma j = + { uj_val= strong f env sigma j.uj_val; uj_type= typed_app (strong f env sigma) j.uj_type } let utj_apply f env sigma j = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index d6d3395e53..0bae65053c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -34,7 +34,7 @@ let sort_of_atomic_type env sigma ft args = match kind_of_term (whd_betadeltaiota env sigma ar) with | IsProd (_, _, b) -> concl_of_arity b | IsSort s -> s - | _ -> outsort env sigma (subst_type env sigma ft args) + | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args)) in concl_of_arity ft let typeur sigma metamap = @@ -71,14 +71,15 @@ let rec type_of env cstr= | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i) | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i) | IsAppL(f,args)-> - strip_outer_cast (subst_type env sigma (type_of env f) args) + strip_outer_cast (subst_type env sigma (type_of env f) + (Array.to_list args)) | IsCast (c,t) -> t | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr) | IsXtra _ -> error "type_of: Unexpected constr" and sort_of env t = match kind_of_term t with - | IsCast (c,DOP0(Sort s)) -> s + | IsCast (c,s) when isSort s -> destSort s | IsSort (Prop c) -> type_0 | IsSort (Type u) -> Type Univ.dummy_univ | IsProd (name,t,c2) -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 99f2f09a8f..b946911e06 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -79,7 +79,7 @@ let rec execute mf env sigma cstr = | IsAppL (f,args) -> let j = execute mf env sigma f in - let jl = execute_list mf env sigma args in + let jl = execute_list mf env sigma (Array.to_list args) in let (j,_) = apply_rel_list env sigma mf.nocheck jl j in j diff --git a/proofs/clenv.ml b/proofs/clenv.ml index efc5190511..5fce6b5956 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -35,7 +35,7 @@ type wc = walking_constraints let new_evar_in_sign env = let ids = ids_of_var_context (Environ.var_context env) in let ev = new_evar () in - mkEvar (ev, Array.of_list (List.map (fun id -> VAR id) ids)) + mkEvar (ev, Array.of_list (List.map mkVar ids)) let rec whd_evar sigma t = match kind_of_term t with | IsEvar (ev,_ as evc) when is_defined sigma ev -> @@ -92,19 +92,19 @@ let unify_0 mc wc m n = unirec_rec (unirec_rec substn t1 t2) c1 c2 | IsAppL (f1,l1), IsAppL (f2,l2) -> - let len1 = List.length l1 - and len2 = List.length l2 in + let len1 = Array.length l1 + and len2 = Array.length l2 in if len1 = len2 then - List.fold_left2 unirec_rec (unirec_rec substn f1 f2) l1 l2 + array_fold_left2 unirec_rec (unirec_rec substn f1 f2) l1 l2 else if len1 < len2 then - let extras,restl2 = list_chop (len2-len1) l2 in - List.fold_left2 unirec_rec - (unirec_rec substn f1 (applist (f2,extras))) + let extras,restl2 = array_chop (len2-len1) l2 in + array_fold_left2 unirec_rec + (unirec_rec substn f1 (appvect (f2,extras))) l1 restl2 else - let extras,restl1 = list_chop (len1-len2) l1 in - List.fold_left2 unirec_rec - (unirec_rec substn (applist (f1,extras)) f2) + let extras,restl1 = array_chop (len1-len2) l1 in + array_fold_left2 unirec_rec + (unirec_rec substn (appvect (f1,extras)) f2) restl1 l2 | IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) -> @@ -155,18 +155,18 @@ let unify_0 mc wc m n = unirec_rec (mc,[]) m n -let whd_castappevar_stack sigma c l = +let whd_castappevar_stack sigma c = let rec whrec (c, l as s) = match kind_of_term c with | IsEvar (ev,args) when is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,args) -> whrec (f, args@l) + | IsAppL (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) | _ -> s in - whrec (c,l) + whrec (c, []) -let whd_castappevar sigma c = applist(whd_castappevar_stack sigma c []) +let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c) let w_whd wc c = whd_castappevar (w_Underlying wc) c @@ -245,7 +245,7 @@ and w_resrec metas evars wc = with ex when catchable_exception ex -> (match krhs with | IsAppL (f,cl) when isConst f -> - let wc' = mimick_evar f (List.length cl) evn wc in + let wc' = mimick_evar f (Array.length cl) evn wc in w_resrec metas evars wc' | _ -> error "w_Unify")) | _ -> anomaly "w_resrec" @@ -445,7 +445,7 @@ let clenv_cast_meta clenv = | Clval(_) -> u with Not_found -> u) - | IsAppL(f,args) -> mkAppList (crec_hd f) (List.map crec args) + | IsAppL(f,args) -> mkAppL (crec_hd f, Array.map crec args) | IsMutCase(ci,p,c,br) -> mkMutCase (ci, crec_hd p, crec_hd c, Array.map crec br) | _ -> u @@ -553,7 +553,8 @@ let clenv_merge with_types = (match krhs with | IsAppL (f,cl) when isConst f or isMutConstruct f -> clenv_resrec metas evars - (clenv_wtactic (mimick_evar f (List.length cl) evn) + (clenv_wtactic + (mimick_evar f (Array.length cl) evn) clenv) | _ -> error "w_Unify")) @@ -681,7 +682,7 @@ let constrain_clenv_to_subterm clause (op,cl) = else error "Bound 1" with ex when catchable_exception ex -> (match kind_of_term (telescope_appl cl) with - | IsAppL (c1,[c2]) -> + | IsAppL (c1,[|c2|]) -> (try matchrec c1 with ex when catchable_exception ex -> diff --git a/proofs/logic.ml b/proofs/logic.ml index e06949be3f..fdece93e21 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -70,7 +70,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | IsAppL (f,l) -> let (acc',hdty) = mk_hdgoals sigma goal goalacc f in - let (acc'',conclty') = mk_arggoals sigma goal acc' hdty l in + let (acc'',conclty') = + mk_arggoals sigma goal acc' hdty (Array.to_list l) in let _ = conv_leq_goal env sigma trm conclty' conclty in (acc'',conclty') @@ -103,7 +104,7 @@ and mk_hdgoals sigma goal goalacc trm = | IsAppL (f,l) -> let (acc',hdty) = mk_hdgoals sigma goal goalacc f in - mk_arggoals sigma goal acc' hdty l + mk_arggoals sigma goal acc' hdty (Array.to_list l) | IsMutCase (_,p,c,lf) -> let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in @@ -155,7 +156,7 @@ let new_meta_variables = let rec newrec x = match kind_of_term x with | IsMeta _ -> mkMeta (new_meta()) | IsCast (c,t) -> mkCast (newrec c, t) - | IsAppL (f,cl) -> applist (newrec f, List.map newrec cl) + | IsAppL (f,cl) -> appvect (newrec f, Array.map newrec cl) | IsMutCase (ci,p,c,lf) -> mkMutCase (ci, newrec p, newrec c, Array.map newrec lf) | _ -> x @@ -298,13 +299,13 @@ let prim_refiner r sigma goal = | IsProd (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); let a = get_assumption_of env sigma c1 - and v = VAR id in + and v = mkVar id in let sg = mk_goal info (push_var_decl (id,a) env) (subst1 v b) in [sg] | IsLetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let a = get_assumption_of env sigma t1 - and v = VAR id in + and v = mkVar id in let sg = mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in [sg] @@ -319,14 +320,14 @@ let prim_refiner r sigma goal = | IsProd (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); let a = get_assumption_of env sigma c1 - and v = VAR id in + and v = mkVar id in let env' = insert_after_hyp env whereid (id,None,a) in let sg = mk_goal info env' (subst1 v b) in [sg] | IsLetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let a = get_assumption_of env sigma t1 - and v = VAR id in + and v = mkVar id in let env' = insert_after_hyp env whereid (id,Some c1,a) in let sg = mk_goal info env' (subst1 v b) in [sg] @@ -339,14 +340,14 @@ let prim_refiner r sigma goal = | IsProd (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); let a = get_assumption_of env sigma c1 - and v = VAR id in + and v = mkVar id in let env' = replace_hyp env id (id,None,a) in let sg = mk_goal info env' (subst1 v b) in [sg] | IsLetIn (_,c1,t1,b) -> if occur_meta c1 then error_use_instantiate(); let a = get_assumption_of env sigma t1 - and v = VAR id in + and v = mkVar id in let env' = replace_hyp env id (id,Some c1,a) in let sg = mk_goal info env' (subst1 v b) in [sg] diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e6130c3f60..ae2ebc9eec 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -61,8 +61,7 @@ val pf_reduce : goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr -val pf_whd_betadeltaiota_stack : - goal sigma -> constr -> constr list -> constr * constr list +val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list val pf_hnf_constr : goal sigma -> constr -> constr val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 09d8885d83..bad9866f63 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -92,13 +92,10 @@ let instantiate_tac = function (fun gl -> instantiate n (pf_interp_constr gl com) gl) | _ -> invalid_arg "Instantiate called with bad arguments" -let whd_evar env sigma = function - | DOPN(Evar n, cl) as k -> - if Evd.in_dom sigma n & Evd.is_defined sigma n then +let whd_evar env sigma c = match kind_of_term c with + | IsEvar (n, cl) when Evd.in_dom sigma n & Evd.is_defined sigma n -> Instantiate.existential_value sigma (n,cl) - else - k - | x -> x + | _ -> c let normEvars gl = let sigma = project gl in diff --git a/tactics/equality.ml b/tactics/equality.ml index bec81d44a8..2b9b230115 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -172,8 +172,9 @@ let v_conditional_rewriteRL = is substitutive *) let find_constructor env sigma c = - match whd_betadeltaiota_stack env sigma c [] with - | DOPN(MutConstruct _,_) as hd,stack -> (hd,stack) + let hd,stack = whd_betadeltaiota_stack env sigma c in + match kind_of_term hd with + | IsMutConstruct _ -> (hd,stack) | _ -> error "find_constructor" type leibniz_eq = { @@ -342,8 +343,8 @@ exception DiscrFound of (sorts oper * int) list * sorts oper * sorts oper let find_positions env sigma t1 t2 = let rec findrec posn t1 t2 = - match (whd_betadeltaiota_stack env sigma t1 [], - whd_betadeltaiota_stack env sigma t2 []) with + match (whd_betadeltaiota_stack env sigma t1, + whd_betadeltaiota_stack env sigma t2) with | ((DOPN(MutConstruct sp1 as oper1,_) as hd1,args1), (DOPN(MutConstruct sp2 as oper2,_) as hd2,args2)) -> @@ -527,8 +528,8 @@ let rec build_discriminator sigma env dirn c sort = function let subval = build_discriminator sigma cnum_env dirn newc sort l in (match necessary_elimination arsort (destSort sort) with | Type_Type -> - kont subval (build_EmptyT (),DOP0(Sort(Type(dummy_univ)))) - | _ -> kont subval (build_False (),DOP0(Sort(Prop Null)))) + kont subval (build_EmptyT (),mkSort (Type(dummy_univ))) + | _ -> kont subval (build_False (),mkSort (Prop Null))) | _ -> assert false let find_eq_data_decompose eqn = @@ -615,7 +616,7 @@ let discr id gls = in tclCOMPLETE((tclTHENS (cut_intro absurd_term) ([onLastHyp (compose gen_absurdity out_some); - refine (mkAppL [| pf; VAR id |])]))) gls + refine (mkAppL (pf, [| VAR id |]))]))) gls | _ -> assert false) let not_found_message id = @@ -774,11 +775,11 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) = in (bindings,dFLT) else - let (a,p) = match whd_beta_stack ty [] with + let (a,p) = match whd_beta_stack ty with | (_,[a;p]) -> (a,p) | _ -> anomaly "sig_clausale_forme: should be a sigma type" in let mv = new_meta() in - let rty = applist(p,[DOP0(Meta mv)]) in + let rty = applist(p,[mkMeta mv]) in let (bindings,tuple_tail) = sigrec_clausale_forme (siglen-1) rty in let w = try List.assoc mv bindings @@ -958,7 +959,7 @@ let decompEqThen ntac id gls = tclCOMPLETE ((tclTHENS (cut_intro absurd_term) ([onLastHyp (compose gen_absurdity out_some); - refine (mkAppL [| pf; VAR id |])]))) gls + refine (mkAppL (pf, [| VAR id |]))]))) gls | Inr posns -> (let e = pf_get_new_id (id_of_string "e") gls in let e_env = @@ -1041,7 +1042,7 @@ let swapEquandsInConcl gls = with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) in let sym_equal = get_squel lbeq.sym in - refine (applist(sym_equal,[t;e2;e1;DOP0(Meta(new_meta()))])) gls + refine (applist(sym_equal,[t;e2;e1;mkMeta (new_meta())])) gls let swapEquandsInHyp id gls = ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls))) @@ -1054,9 +1055,9 @@ let swapEquandsInHyp id gls = otherwise *) let find_elim sort_of_gl lbeq = - match sort_of_gl with - | DOP0(Sort(Prop Null)) (* Prop *) -> (get_squel lbeq.ind, false) - | DOP0(Sort(Prop Pos)) (* Set *) -> + match kind_of_term sort_of_gl with + | IsSort(Prop Null) (* Prop *) -> (get_squel lbeq.ind, false) + | IsSort(Prop Pos) (* Set *) -> (match lbeq.rrec with | Some eq_rec -> (get_squel eq_rec, false) | None -> errorlabstrm "find_elim" @@ -1100,8 +1101,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = else (build_non_dependent_rewrite_predicate (t,e1,e2) body gls) in - refine (applist(eq_elim,[t;e1;p;DOP0(Meta(new_meta())); - e2;DOP0(Meta(new_meta()))])) gls + refine (applist(eq_elim,[t;e1;p;mkMeta(new_meta()); + e2;mkMeta(new_meta())])) gls (* [subst_tuple_term dep_pair B] @@ -1169,6 +1170,27 @@ let decomp_tuple_term env c t = in List.split (decomprec (Rel 1) c t) +(* +let whd_const_state namelist env sigma = + let rec whrec (x, l as s) = + match kind_of_term x with + | IsConst (sp,_) when List.mem sp namelist -> + if evaluable_constant env x then + whrec (constant_value env x, l) + else + error "whd_const_stack" + | IsCast (c,_) -> whrec (c, l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) + | _ -> s + in + whrec +let whd_const_state namelist = whd_state (const namelist) +let whd_const_stack namelist env sigma x = + whd_const_state namelist env sigma (x, empty_stack) +let whd_const namelist env sigma c = + app_stack (whd_const_stack namelist env sigma (c, empty_stack)) +*) + let subst_tuple_term env sigma dep_pair b = let typ = get_type_of env sigma dep_pair in let e_list,proj_list = decomp_tuple_term env dep_pair typ in @@ -1291,7 +1313,7 @@ let rec eq_mod_rel l_meta t0 t1 = let is_hd_const c = match kind_of_term c with | IsAppL (f,args) -> (match kind_of_term f with - | IsConst (c,_) -> Some (c, Array.of_list args) + | IsConst (c,_) -> Some (c, args) |_ -> None) | _ -> None diff --git a/tactics/refine.ml b/tactics/refine.ml index 08105aa9f0..ce60df06a1 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -88,7 +88,7 @@ let replace_by_meta env = function | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp | (TH (c,mm,_)) as th -> let n = new_meta() in - let m = DOP0(Meta n) in + let m = mkMeta n in (* quand on introduit une mv on calcule son type *) let ty = match kind_of_term c with | IsLambda (Name id,c1,c2) when isCast c2 -> @@ -131,7 +131,7 @@ let rec compute_metamap env c = match kind_of_term c with | IsMeta n -> Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n); TH (c,[],[None]) - | IsCast (DOP0(Meta n),ty) -> TH (c,[n,ty],[None]) + | IsCast (m,ty) when isMeta m -> TH (c,[destMeta m,ty],[None]) (* abstraction => il faut décomposer si le terme dessous n'est pas pur * attention : dans ce cas il faut remplacer (Rel 1) par (VAR x) @@ -154,10 +154,10 @@ let rec compute_metamap env c = match kind_of_term c with (* 4. Application *) | IsAppL (f,v) -> - let a = Array.map (compute_metamap env) (Array.of_list (f::v)) in + let a = Array.map (compute_metamap env) (Array.append [|f|] v) in begin try - let v',mm,sgp = replace_in_array env a in TH (mkAppL v',mm,sgp) + let v',mm,sgp = replace_in_array env a in TH (mkAppA v',mm,sgp) with NoMeta -> TH (c,[],[]) end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index d5ee7f9659..feb48e4ef9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -52,7 +52,7 @@ let tclMAP tacfun l = (* apply a tactic to the nth element of the signature *) let tclNTH_HYP m (tac : constr->tactic) gl = - tac (try VAR(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) + tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) with Failure _ -> error "No such assumption") gl (* apply a tactic to the last element of the signature *) @@ -62,8 +62,8 @@ let tclLAST_HYP = tclNTH_HYP 1 let tclTRY_sign (tac : constr->tactic) sign gl = let rec arec = function | [] -> tclFAIL 0 - | [s] -> tac (VAR(s)) (* added in order to get useful error messages *) - | (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl) + | [s] -> tac (mkVar s) (*added in order to get useful error messages *) + | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) in arec (ids_of_var_context sign) gl @@ -281,16 +281,16 @@ let elim_sign ity i = analrec [] recarg.(i-1) let sort_of_goal gl = - match hnf_type_of gl (pf_concl gl) with - | DOP0(Sort s) -> s - | _ -> anomaly "goal should be a type" + match kind_of_term (hnf_type_of gl (pf_concl gl)) with + | IsSort s -> s + | _ -> anomaly "goal should be a type" (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let last_arg c = match kind_of_term c with - | IsAppL (f,cl) -> List.nth cl (List.length cl - 1) + | IsAppL (f,cl) -> array_last cl | _ -> anomaly "last_arg" let general_elim_then_using @@ -312,9 +312,10 @@ let general_elim_then_using | IsMeta mv -> mv | _ -> error "elimination" in - let pmv = - match decomp_app (clenv_template_type elimclause).rebus with - | (DOP0(Meta(p)),oplist) -> p + let pmv = + let p, _ = decomp_app (clenv_template_type elimclause).rebus in + match kind_of_term p with + | IsMeta p -> p | _ -> error ("The elimination combinator " ^ (string_of_id name_elim) ^ " is not known") in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a8693a70be..60ea7e8d07 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -40,17 +40,6 @@ 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 - | DOPN (Evar ev,ctxt) -> c - | DOPN (MutConstruct (spi,j),ctxt) -> c - | DOPN (MutInd (sp,i),ctxt) -> c - | VAR id -> c - | _ -> error "Not an atomic type" -*) - 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) -> @@ -70,7 +59,8 @@ let rec head_constr_bound t l = let t = strip_outer_cast(collapse_appl t) in match kind_of_term t with | IsProd (_,_,c2) -> head_constr_bound c2 l - | IsAppL (f,args) -> head_constr_bound f (args@l) + | IsAppL (f,args) -> + head_constr_bound f (Array.fold_right (fun a l -> a::l) args l) | IsConst _ -> t::l | IsMutInd _ -> t::l | IsMutConstruct _ -> t::l @@ -155,8 +145,8 @@ let reduct_in_concl redfun gl = let reduct_in_hyp redfun id gl = let ty = pf_get_hyp_typ gl id in - let redfun' = under_casts (fun _ _ -> pf_reduce redfun gl) in - convert_hyp id (redfun' (pf_env gl) (project gl) ty) gl + let redfun' = under_casts (pf_reduce redfun gl) in + convert_hyp id (redfun' ty) gl let reduct_option redfun = function | Some id -> reduct_in_hyp redfun id @@ -271,9 +261,9 @@ let id_of_name_with_default s = function let default_id gl = match kind_of_term (strip_outer_cast (pf_concl gl)) with | IsProd (name,c1,c2) -> - (match pf_whd_betadeltaiota gl (pf_type_of gl c1) with - | DOP0(Sort(Prop _)) -> (id_of_name_with_default "H" name) - | DOP0(Sort(Type(_))) -> (id_of_name_with_default "X" name) + (match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl c1)) with + | IsSort (Prop _) -> (id_of_name_with_default "H" name) + | IsSort (Type _) -> (id_of_name_with_default "X" name) | _ -> anomaly "Wrong sort") | _ -> error "Introduction needs a product" @@ -466,10 +456,10 @@ let bring_hyps clsl gl = | None -> error "BringHyps") clsl in let newcl = List.fold_right - (fun id cl' -> mkNamedProd id (pf_type_of gl (VAR id)) cl') + (fun id cl' -> mkNamedProd id (pf_type_of gl (mkVar id)) cl') ids (pf_concl gl) in - apply_type newcl (List.map (fun id -> VAR id) ids) gl + apply_type newcl (List.map mkVar ids) gl (* Resolution with missing arguments *) @@ -535,7 +525,7 @@ let cut_and_apply c gl = | IsProd (_,c1,c2) when not (dependent (mkRel 1) c2) -> tclTHENS (apply_type (mkProd (Anonymous,c2,goal_constr)) - [DOP0(Meta(new_meta()))]) + [mkMeta (new_meta())]) [tclIDTAC;apply_term c [mkMeta (new_meta())]] gl | _ -> error "Imp_elim needs a non-dependent product" @@ -549,8 +539,8 @@ let dyn_cut_and_apply = function (**************************) let cut c gl = - match hnf_type_of gl c with - | (DOP0(Sort _)) -> + match kind_of_term (hnf_type_of gl c) with + | IsSort _ -> apply_type (mkProd (Anonymous, c, pf_concl gl)) [mkMeta (new_meta())] gl | _ -> error "Not a proposition or a type" @@ -582,8 +572,8 @@ let cut_in_parallel l = let generalize_goal gl c cl = let t = pf_type_of gl c in - match c with - | (VAR id) -> mkNamedProd id t cl + match kind_of_term c with + | IsVar id -> mkNamedProd id t cl | _ -> let cl' = subst_term c cl in if noccurn 1 cl' then @@ -608,8 +598,8 @@ let generalize_dep c gl = let qhyps = List.map (fun (id,_,_) -> id) to_quantify in let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in let tothin' = - match c with - | VAR id when mem_var_context id sign & not (List.mem id init_ids) + match kind_of_term c with + | IsVar id when mem_var_context id sign & not (List.mem id init_ids) -> id::tothin | _ -> tothin in @@ -618,7 +608,7 @@ let generalize_dep c gl = (fun c d -> mkNamedProd_or_LetIn d c) (pf_concl gl) to_quantify in let cl'' = generalize_goal gl c cl' in tclTHEN - (apply_type cl'' (c::(List.map (fun id -> VAR id) qhyps))) + (apply_type cl'' (c::(List.map mkVar qhyps))) (thin (List.rev tothin')) gl @@ -670,7 +660,7 @@ let letin_abstract id c occ_ccl occ_hyps gl = let abstract ((depdecls,marks,occl as accu),lhyp) (hyp,bodyopt,typ as d) = try let occ = if allhyp then [] else List.assoc hyp occl in - let newdecl = subst1 (VAR id) (subst_term_occ_decl occ c d) in + let newdecl = subst1 (mkVar id) (subst_term_occ_decl occ c d) in let newoccl = list_except_assoc hyp occl in if d=newdecl then (accu,Some hyp) @@ -689,7 +679,7 @@ let letin_abstract id c occ_ccl occ_hyps gl = end; let ccl = match occ_ccl with | None -> (pf_concl gl) - | Some occ -> subst1 (VAR id) (subst_term_occ occ c (pf_concl gl)) + | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in (depdecls,marks,ccl) @@ -710,10 +700,10 @@ let letin_tac with_eq name c occ_ccl occ_hyps gl = in let heq = next_global_ident_away (id_of_string "Heq") (ids_of_sign hyps) in let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in - let tmpargs = List.map (fun (id,_,_) -> VAR id) depdecls in + let tmpargs = List.map (fun (id,_,_) -> mkVar id) depdecls in let newcl,args = if with_eq then - let eq = applist (eqc,[t;VAR id;c]) in + let eq = applist (eqc,[t;mkVar id;c]) in let refl = applist (reflc,[t;c]) in (mkNamedProd id t (mkNamedProd heq eq tmpcl), c::refl::tmpargs) else @@ -769,7 +759,7 @@ let (assumption : tactic) = fun gl -> let rec arec = function | [] -> error "No such assumption" | (id,c,t)::rest -> - if pf_conv_x_leq gl (body_of_type t) concl then refine (VAR id) gl + if pf_conv_x_leq gl (body_of_type t) concl then refine (mkVar id) gl else arec rest in arec (pf_hyps gl) @@ -939,7 +929,7 @@ let dyn_split = function *) let last_arg c = match kind_of_term c with - | IsAppL (f,cl) -> List.nth cl (List.length cl - 1) + | IsAppL (f,cl) -> array_last cl | _ -> anomaly "last_arg" let elimination_clause_scheme kONT wc elimclause indclause gl = @@ -1098,21 +1088,21 @@ let atomize_param_of_ind hyp0 gl = if i<>nparams then let tmptyp0 = pf_get_hyp_typ gl hyp0 in let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in - match (destAppL (whd_castapp indtyp)).(i) with - | VAR id when not (List.exists (occur_var id) avoid) -> - atomize_one (i-1) ((VAR id)::avoid) gl - | VAR id -> + match kind_of_term (destAppL (whd_castapp indtyp)).(i) with + | IsVar id when not (List.exists (occur_var id) avoid) -> + atomize_one (i-1) ((mkVar id)::avoid) gl + | IsVar id -> let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) (VAR id) (Some []) []) - (atomize_one (i-1) ((VAR x)::avoid)) gl + (letin_tac true (Name x) (mkVar id) (Some []) []) + (atomize_one (i-1) ((mkVar x)::avoid)) gl | c -> let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let x = fresh_id [] id gl in tclTHEN (letin_tac true (Name x) c (Some []) []) - (atomize_one (i-1) ((VAR x)::avoid)) gl + (atomize_one (i-1) ((mkVar x)::avoid)) gl else tclIDTAC gl in @@ -1126,8 +1116,8 @@ let find_atomic_param_of_ind mind indtyp = let params = list_firstn nparams argl in let indvars = ref Idset.empty in for i = nparams to (Array.length argv)-1 do - match argv.(i) with - | VAR id when not (List.exists (occur_var id) params) -> + match kind_of_term argv.(i) with + | IsVar id when not (List.exists (occur_var id) params) -> indvars := Idset.add id !indvars | _ -> () done; @@ -1269,7 +1259,7 @@ let cook_sign hyp0 indvars sign = *) let induction_tac varname typ (elimc,elimt) gl = - let c = VAR varname in + let c = mkVar varname in let (wc,kONT) = startWalk gl in let indclause = make_clenv_binding wc (c,typ) [] in let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in @@ -1305,7 +1295,7 @@ let induction_from_context hyp0 gl = let tmpcl = List.fold_right2 mkNamedProd dephyps deptyps (pf_concl gl) in let lc = get_constructors hyp0 (elimc,elimt) mind mindpath in tclTHENLIST - [ apply_type tmpcl (List.map (fun id -> VAR id) dephyps); + [ apply_type tmpcl (List.map mkVar dephyps); thin dephyps; tclTHENS (tclTHEN @@ -1320,8 +1310,8 @@ let induction_with_atomization_of_ind_arg hyp0 = (induction_from_context hyp0) let new_induct c gl = - match c with - | (VAR id) when not (List.mem id (ids_of_sign (Global.var_context()))) -> + match kind_of_term c with + | IsVar id when not (List.mem id (ids_of_sign (Global.var_context()))) -> tclORELSE (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim)) (induction_with_atomization_of_ind_arg id) gl @@ -1469,7 +1459,7 @@ let dyn_case_type = function let andE id gl = let t = pf_get_hyp_typ gl id in if is_conjunction (pf_hnf_constr gl t) then - (tclTHEN (simplest_elim (VAR id)) (tclDO 2 intro)) gl + (tclTHEN (simplest_elim (mkVar id)) (tclDO 2 intro)) gl else errorlabstrm "andE" [< 'sTR("Tactic andE expects "^(string_of_id id)^" is a conjunction.")>] @@ -1482,7 +1472,7 @@ let dAnd cls gl = let orE id gl = let t = pf_get_hyp_typ gl id in if is_disjunction (pf_hnf_constr gl t) then - (tclTHEN (simplest_elim (VAR id)) intro) gl + (tclTHEN (simplest_elim (mkVar id)) intro) gl else errorlabstrm "orE" [< 'sTR("Tactic orE expects "^(string_of_id id)^" is a disjunction.")>] @@ -1497,7 +1487,7 @@ let impE id gl = if is_imp_term (pf_hnf_constr gl t) then let (dom, _, rng) = destProd (pf_hnf_constr gl t) in (tclTHENS (cut_intro rng) - [tclIDTAC;apply_term (VAR id) [DOP0(Meta(new_meta()))]]) gl + [tclIDTAC;apply_term (mkVar id) [mkMeta (new_meta())]]) gl else errorlabstrm "impE" [< 'sTR("Tactic impE expects "^(string_of_id id)^ @@ -1517,7 +1507,7 @@ let dImp cls gl = let contradiction_on_hyp id gl = let hyp = pf_get_hyp_typ gl id in if is_empty_type hyp then - simplest_elim (VAR id) gl + simplest_elim (mkVar id) gl else error "Not a contradiction" @@ -1532,7 +1522,7 @@ let absurd c gls = ((fun gl -> let ida = pf_nth_hyp_id gl 1 and idna = pf_nth_hyp_id gl 2 in - exact (applist(VAR idna,[VAR ida])) gl))); + exact (applist(mkVar idna,[mkVar ida])) gl))); tclIDTAC])); tclIDTAC])) gls @@ -1580,8 +1570,8 @@ let symmetry gl = (apply (pf_parse_const gl ("sym_"^hdcncls)) gl) with _ -> let symc = match args with - | [typ;c1;c2] -> mkAppL [| hdcncl; typ; c2; c1 |] - | [c1;c2] -> mkAppL [| hdcncl; c2; c1 |] + | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; c2; c1 |]) + | [c1;c2] -> mkAppL (hdcncl, [| c2; c1 |]) | _ -> assert false in (tclTHENS (cut symc) @@ -1619,13 +1609,13 @@ let transitivity t gl = apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl with _ -> let eq1 = match args with - | [typ;c1;c2] -> mkAppL [| hdcncl; typ; c1; t |] - | [c1;c2] -> mkAppL [| hdcncl; c1; t|] + | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; c1; t |]) + | [c1;c2] -> mkAppL (hdcncl, [| c1; t|]) | _ -> assert false in let eq2 = match args with - | [typ;c1;c2] -> mkAppL [| hdcncl; typ; t; c2 |] - | [c1;c2] -> mkAppL [| hdcncl; t; c2 |] + | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; t; c2 |]) + | [c1;c2] -> mkAppL (hdcncl, [| t; c2 |]) | _ -> assert false in (tclTHENS (cut eq2) @@ -1677,7 +1667,7 @@ let abstract_subproof name tac gls = Declare.construct_reference newenv CCI na in exact (applist (lemme, - List.map (fun id -> VAR id) (List.rev (ids_of_var_context sign)))) + List.map mkVar (List.rev (ids_of_var_context sign)))) gls let tclABSTRACT name_op tac gls = diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 7c00a6b1d3..171eea17b6 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -81,7 +81,7 @@ let is_atomic m = (is_matching (get_pat pi_pattern) m) || (is_matching (not_pattern ()) m)) -let hypothesis = function Some id -> exact (VAR id) | None -> assert false +let hypothesis = function Some id -> exact (mkVar id) | None -> assert false (* Steps of the procedure *) @@ -205,12 +205,12 @@ B,Gamma|- G D->B,Gamma |- C->D *) let back_thru_2 id = - applist(VAR id,[DOP0(Meta(new_meta()));DOP0(Meta(new_meta()))]) + applist(mkVar id,[mkMeta (new_meta());mkMeta (new_meta())]) let back_thru_1 id = - applist(VAR id,[DOP0(Meta(new_meta()))]) + applist(mkVar id,[mkMeta(new_meta())]) -let exact_last_hyp = onLastHyp (fun h -> exact (VAR (out_some h))) +let exact_last_hyp = onLastHyp (fun h -> exact (mkVar (out_some h))) let imply_imply_bot_pattern = put_pat mmk "(?1 -> ?2) -> ?3" @@ -260,7 +260,7 @@ let true_imply_step cls gls = let h0 = out_some cls in (tclTHENS (cut_intro b) [(clear_clause cls); - (tclTHEN (apply(VAR h0)) (one_constructor 1 []))]) gls + (tclTHEN (apply(mkVar h0)) (one_constructor 1 []))]) gls | _ -> anomaly "Inconsistent pattern-matching" with PatternMatchingFailure -> error "true_imply_step" @@ -1765,7 +1765,7 @@ let search env id = Rel (fst (lookup_rel_id id (Environ.rel_context env))) with Not_found -> if mem_var_context id (Environ.var_context env) then - VAR id + mkVar id else global_reference CCI id @@ -1837,11 +1837,13 @@ let cut_in_parallelUsing idlist l = in prec (List.rev idlist) (List.rev l) -let exacto tt gls = - match (try cci_of_tauto_term (pf_env gls) tt with - _ -> (DOP0 Prod)) with (* Efectivamente, es cualquier cosa!! *) - | (DOP0 Prod) -> tAUTOFAIL gls (* Esto confirma el comentario anterior *) - | t -> (exact t) gls +let exacto tt gls = + let tac = + try + let t = cci_of_tauto_term (pf_env gls) tt in + exact t + with _ -> tAUTOFAIL (* Efectivamente, es cualquier cosa!! *) + in tac gls (* Esto confirma el comentario anterior *) let subbuts l hyp = cut_in_parallelUsing (lisvar l) diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 920e6ba310..c62746cc71 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -17,7 +17,7 @@ type 'a t = (constr_label,constr_pattern,'a) Dn.t let decomp = let rec decrec acc c = match kind_of_term c with - | IsAppL (f,l) -> decrec (l@acc) f + | IsAppL (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f | IsCast (c1,_) -> decrec acc c1 | _ -> (c,acc) in diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 4f071980e6..de5adc94df 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -132,15 +132,14 @@ and build_term ce p_0 c = match p_0, kind_of_term c with | ((na,Some t), IsMeta mv) -> (* let mv = new_meta() in *) - (DOP0(Meta mv), - clenv_pose (na,mv,t) ce) + (mkMeta mv, clenv_pose (na,mv,t) ce) | ((na,_), IsCast (c,t)) -> build_term ce (na,Some t) c | ((na,Some t), _) -> if (not((occur_meta c))) then (c,ce) else let (hd,args) = - whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in + whd_betadeltaiota_stack env (w_Underlying ce.hook) c in let hdty = w_type_of ce.hook hd in let (args,ce') = build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in @@ -155,7 +154,7 @@ and build_term ce p_0 c = (c,ce) else let (hd,args) = - whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in + whd_betadeltaiota_stack env (w_Underlying ce.hook) c in let hdty = w_type_of ce.hook hd in let (args,ce') = build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 9a55f5adfb..3240e9db51 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -204,7 +204,7 @@ let expmod_constr oldenv modlist c = | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t)) | c -> f c in - let c' = modify_opers expfun (fun a b -> mkAppL [|a; b|]) modlist c in + let c' = modify_opers expfun (fun a b -> mkAppL (a, [|b|])) modlist c in match c' with | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ) | _ -> simpfun c' |