From 4da5cd28c6080ceeb66acc2163cf10a43e8bcade Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 3 Sep 2008 00:03:32 +0000 Subject: Correct handling of implicit arguments in [Equations] definitions, support for "where" notation declarations as well. Better checking of recursivity or not, after type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/equations.ml4 | 85 +++++++++++++++++++++++++----------------- parsing/g_vernac.ml4 | 3 +- test-suite/success/Equations.v | 73 +++++++++++++++++++++++++----------- theories/Program/Equality.v | 2 +- 4 files changed, 105 insertions(+), 58 deletions(-) diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 index ab2fa6cfbf..4464d1ca63 100644 --- a/contrib/subtac/equations.ml4 +++ b/contrib/subtac/equations.ml4 @@ -579,7 +579,7 @@ open Topconstr open Constrintern open Decl_kinds -type equation = identifier located * constr_expr list * (constr_expr, identifier located) rhs +type equation = constr_expr * (constr_expr, identifier located) rhs let locate_reference qid = match Nametab.extended_locate qid with @@ -612,9 +612,10 @@ let ids_of_patc c ?(bound=Idset.empty) l = fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c - -let interp_pats isevar env impls pats sign = - let vars = fold_left (fun acc patc -> ids_of_patc patc acc) [] pats in + +let interp_pats i isevar env impls pat sign recu = + let bound = Idset.singleton i in + let vars = ids_of_patc pat ~bound [] in let varsctx, env' = fold_right (fun (loc, id) (ctx, env) -> let decl = @@ -624,19 +625,21 @@ let interp_pats isevar env impls pats sign = decl::ctx, push_rel decl env) vars ([], env) in - let patcs = - fold_left2 (fun subst pat (_, _, ty) -> - let ty = substl subst ty in - interp_casted_constr_evars isevar env' ~impls pat ty :: subst) - [] pats (List.rev sign) + let pats = + let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in + let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in + match kind_of_term patt with + | App (m, args) -> Array.to_list args + | _ -> user_err_loc (constr_loc pat, "interp_pats", + str "Error parsing pattern: unnexpected left-hand side") in isevar := nf_evar_defs !isevar; (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, nf_env_evar (Evd.evars_of !isevar) env', - map (nf_evar (Evd.evars_of !isevar)) patcs) + rev_map (nf_evar (Evd.evars_of !isevar)) pats) -let interp_eqn isevar env impls sign arity (idl, pats, rhs) = - let ctx, env', patcs = interp_pats isevar env impls pats sign in +let interp_eqn i isevar env impls sign arity recu (pats, rhs) = + let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in let rhs' = match rhs with | Program p -> Program (interp_casted_constr_evars isevar env' ~impls p (substl patcs arity)) @@ -645,31 +648,34 @@ let interp_eqn isevar env impls sign arity (idl, pats, rhs) = open Entries -let define_by_eqs i l t eqs = +let define_by_eqs i l t nt eqs = let env = Global.env () in let isevar = ref (create_evar_defs Evd.empty) in let (env', sign), impls = interp_context_evars isevar env l in let arity = interp_type_evars isevar env' t in - let is_recursive, fixenv = - let occur_eqn (_, _, rhs) = - match rhs with - | Program c -> occur_var_constr_expr i c - | _ -> false - in - if exists occur_eqn eqs then - let ty = it_mkProd_or_LetIn arity sign in - let fixenv = push_rel (Name i, None, ty) env in - true, fixenv - else false, env + let ty = it_mkProd_or_LetIn arity sign in + let data = Command.compute_interning_datas env [] [i] [ty] [impls] in + let fixenv = push_rel (Name i, None, ty) env in + let equations = + States.with_heavy_rollback (fun () -> + Option.iter (Command.declare_interning_data data) nt; + map (interp_eqn i isevar fixenv data sign arity None) eqs) () in - let equations = map (interp_eqn isevar fixenv ([],[]) sign arity) eqs in let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in let arity = nf_evar (Evd.evars_of !isevar) arity in let prob = (i, sign, arity) in let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in - let split = make_split fixenv prob equations in + let ce = check_evars fixenv Evd.empty !isevar in + let is_recursive, env' = + let occur_eqn (ctx, _, rhs) = + match rhs with + | Program c -> dependent (mkRel (succ (length ctx))) c + | _ -> false + in if exists occur_eqn equations then true, fixenv else false, env + in + let split = make_split env' prob equations in (* if valid_tree prob split then *) - let t, ty = term_of_tree isevar fixenv prob split in + let t, ty = term_of_tree isevar env' prob split in let t = if is_recursive then let firstsplit = @@ -681,7 +687,7 @@ let define_by_eqs i l t eqs = in let undef = undefined_evars !isevar in let obls, t', ty' = Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 t ty in - ignore(Subtac_obligations.add_definition i t' ty' obls) + ignore(Subtac_obligations.add_definition ~implicits:impls i t' ty' obls) module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ @@ -694,6 +700,9 @@ struct let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations" let binders_let2 : local_binder list Gram.Entry.e = gec "binders_let2" + +(* let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *) + end open Rawterm @@ -702,6 +711,7 @@ open Util open Pcoq open Prim open Constr +open G_vernac GEXTEND Gram GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2; @@ -715,11 +725,7 @@ GEXTEND Gram ; equation: - [ [ c = Constr.lconstr; r=rhs -> - match c with - | CApp (loc, (None, CRef (Ident lid)), l) -> - (lid, List.map fst l, r) - | _ -> error "Error parsing equation" ] ] + [ [ c = Constr.lconstr; r=rhs -> (c, r) ] ] ; rhs: @@ -744,10 +750,19 @@ let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype), (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) = Genarg.create_arg "binders_let2" +type 'a decl_notation_argtype = (Vernacexpr.decl_notation, 'a) Genarg.abstract_argument_type + +let (wit_decl_notation : Genarg.tlevel decl_notation_argtype), + (globwit_decl_notation : Genarg.glevel decl_notation_argtype), + (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) = + Genarg.create_arg "decl_notation" + + VERNAC COMMAND EXTEND Define_equations -| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs) ] -> - [ define_by_eqs i l t eqs ] +| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs) + decl_notation(nt) ] -> + [ define_by_eqs i l t nt eqs ] END open Tacmach diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5f656ed5c2..c9fc4e2ffb 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -46,6 +46,7 @@ let noedit_mode = Gram.Entry.create "vernac:noedit_command" let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" let thm_token = Gram.Entry.create "vernac:thm_token" let def_body = Gram.Entry.create "vernac:def_body" +let decl_notation = Gram.Entry.create "vernac:decl_notation" let typeclass_context = Gram.Entry.create "vernac:typeclass_context" let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion" @@ -119,7 +120,7 @@ let no_coercion loc (c,x) = (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - typeclass_context typeclass_constraint; + typeclass_context typeclass_constraint decl_notation; gallina: (* Definition, Theorem, Variable, Axiom, ... *) diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v index 3ef5919596..ea4d693dda 100644 --- a/test-suite/success/Equations.v +++ b/test-suite/success/Equations.v @@ -21,51 +21,60 @@ Equations tail {A} (l : list A) : (list A) := tail A nil := nil ; tail A (cons a v) := v. -Eval compute in tail. +Eval compute in @tail. -Eval compute in (tail _ (cons 1 nil)). +Eval compute in (tail (cons 1 nil)). + +Reserved Notation " x ++ y " (at level 60, right associativity). + +Equations app (l l' : list nat) : list nat := + [] ++ l := l ; + (a :: v) ++ l := a :: (v ++ l) + +where " x ++ y " := (app x y). Equations app' {A} (l l' : list A) : (list A) := app' A nil l := l ; -app' A (cons a v) l := cons a (app' A v l). +app' A (cons a v) l := cons a (app' v l). -Eval compute in app'. + +Eval compute in @app'. Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) := zip' A f nil nil := nil ; -zip' A f (cons a v) (cons b w) := cons (f a b) (zip' _ f v w) ; +zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ; zip' A f nil (cons b w) := nil ; zip' A f (cons a v) nil := nil. -Eval compute in zip'. +Eval compute in @zip'. -Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] beta iota zeta in zip'. +Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] beta iota zeta in @zip'. Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) := zip'' A f nil nil def := nil ; -zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' _ f v w def) ; +zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ; zip'' A f nil (cons b w) def := def ; zip'' A f (cons a v) nil def := def. -Eval compute in zip''. -Eval cbv delta [ zip'' ] beta iota zeta in zip''. +Eval compute in @zip''. +Eval cbv delta [ zip'' ] beta iota zeta in @zip''. Implicit Arguments Vnil [[A]]. Implicit Arguments Vcons [[A] [n]]. -Equations vhead A n (v : vector A (S n)) : A := +Equations vhead {A n} (v : vector A (S n)) : A := vhead A n (Vcons a v) := a. -Eval compute in (vhead _ _ (Vcons 2 (Vcons 1 Vnil))). -Eval compute in vhead. +Eval compute in (vhead (Vcons 2 (Vcons 1 Vnil))). +Eval compute in @vhead. -Equations vmap {A B} (f : A -> B) n (v : vector A n) : (vector B n) := +Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) := vmap A B f 0 Vnil := Vnil ; -vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap A B f n v). +vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v). -Eval compute in (vmap _ _ id _ (@Vnil nat)). -Eval compute in (vmap _ _ id _ (@Vcons nat 2 _ Vnil)). -Eval compute in vmap. +Eval compute in (vmap id (@Vnil nat)). +Eval compute in (vmap id (@Vcons nat 2 _ Vnil)). +Eval compute in @vmap. Inductive fin : nat -> Set := | fz : Π {n}, fin (S n) @@ -79,12 +88,12 @@ Implicit Arguments finle [[n]]. Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := trans (S n) fz j k leqz q := leqz ; -trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans _ _ _ _ p q). +trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans p q). -Lemma trans_eq1 n (j k : fin (S n)) q : trans (S n) fz j k leqz q = leqz. +Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. Proof. intros. simplify_equations ; reflexivity. Qed. -Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans _ _ _ _ p q). +Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). Proof. intros. simplify_equations ; reflexivity. Qed. Section Image. @@ -100,3 +109,25 @@ Section Image. End Image. +Section Univ. + + Inductive univ : Set := + | ubool | unat | uarrow (from:univ) (to:univ). + + Equations interp (u : univ) : Type := + interp ubool := bool ; interp unat := nat ; + interp (uarrow from to) := interp from -> interp to. + + Equations foo (u : univ) (el : interp u) : interp u := + foo ubool true := false ; + foo ubool false := true ; + foo unat t := t ; + foo (uarrow from to) f := id ∘ f. + + Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo. + +End Univ. + +Eval compute in (foo ubool false). +Eval compute in (foo (uarrow ubool ubool) negb). +Eval compute in (foo (uarrow ubool ubool) id). diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 869df369b8..2bf25c8e70 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -389,7 +389,7 @@ Ltac depelim id := (used internally). *) Ltac destruct_last := - on_last_hyp ltac:(fun id => generalize_eqs id ; destruct id). + on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id). (** The rest is support tactics for the [Equations] command. *) -- cgit v1.2.3