From 4fa8ff4c0463a85382351910522daf75bcdd6795 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 2 Dec 2002 19:02:41 +0000 Subject: Remplacement de Syntactic Definition par Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/ring/Setoid_ring_theory.v | 185 +++++++++++++++++--------------------- parsing/egrammar.ml | 122 ++++++++++++++++++++----- test-suite/success/CasesDep.v | 4 +- 3 files changed, 182 insertions(+), 129 deletions(-) diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index 15f79158f3..ffb44d0d3d 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -13,41 +13,13 @@ Require Export Setoid. Set Implicit Arguments. -Grammar ring formula : constr := - formula_expr [ expr($p) ] -> [$p] -| formula_eq [ expr($p) "==" expr($c) ] -> [ (Aequiv $p $c) ] - -with expr : constr := - RIGHTA - expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ] - | expr_expr1 [ expr1($p) ] -> [$p] - -with expr1 : constr := - RIGHTA - expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ] - | expr1_final [ final($p) ] -> [$p] - -with final : constr := - final_var [ prim:var($id) ] -> [ $id ] -| final_constr [ "[" constr:constr($c) "]" ] -> [ $c ] -| final_app [ "(" application($r) ")" ] -> [ $r ] -| final_0 [ "0" ] -> [ Azero ] -| final_1 [ "1" ] -> [ Aone ] -| final_uminus [ "-" expr($c) ] -> [ (Aopp $c) ] - -with application : constr := - LEFTA - app_cons [ application($p) application($c1) ] -> [ ($p $c1) ] - | app_tail [ expr($c1) ] -> [ $c1 ]. - -Grammar constr constr0 := - formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ]. - Section Setoid_rings. Variable A : Type. Variable Aequiv : A -> A -> Prop. +Infix "==" Aequiv (at level 5). + Variable S : (Setoid_Theory A Aequiv). Add Setoid A Aequiv S. @@ -59,12 +31,15 @@ Variable Azero : A. Variable Aopp : A -> A. Variable Aeq : A -> A -> bool. -Variable plus_morph : (a,a0,a1,a2:A) - (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Aplus a a1) (Aplus a0 a2)). -Variable mult_morph : (a,a0,a1,a2:A) - (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Amult a a1) (Amult a0 a2)). -Variable opp_morph : (a,a0:A) - (Aequiv a a0)->(Aequiv (Aopp a) (Aopp a0)). +Infix "+" Aplus (at level 4). +Infix "*" Amult (at level 3). +Notation "0" := Azero. +Notation "1" := Aone. +Notation "- x" := (Aopp x) (at level 3). + +Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2. +Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2. +Variable opp_morph : (a,a0:A) a == a0 -> -a == -a1. Add Morphism Aplus : Aplus_ext. Exact plus_morph. @@ -81,16 +56,16 @@ Save. Section Theory_of_semi_setoid_rings. Record Semi_Setoid_Ring_Theory : Prop := -{ SSR_plus_sym : (n,m:A) [| n + m == m + n |]; - SSR_plus_assoc : (n,m,p:A) [| n + (m + p) == (n + m) + p |]; - SSR_mult_sym : (n,m:A) [| n*m == m*n |]; - SSR_mult_assoc : (n,m,p:A) [| n*(m*p) == (n*m)*p |]; - SSR_plus_zero_left :(n:A) [| 0 + n == n|]; - SSR_mult_one_left : (n:A) [| 1*n == n |]; - SSR_mult_zero_left : (n:A) [| 0*n == 0 |]; - SSR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |]; - SSR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> (Aequiv m p); - SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv x y) +{ SSR_plus_sym : (n,m:A) n + m == m + n; + SSR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; + SSR_mult_sym : (n,m:A) n*m == m*n; + SSR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; + SSR_plus_zero_left :(n:A) 0 + n == n; + SSR_mult_one_left : (n:A) 1*n == n; + SSR_mult_zero_left : (n:A) 0*n == 0; + SSR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; + SSR_plus_reg_left : (n,m,p:A)n + m == n + p -> m == p; + SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y }. Variable T : Semi_Setoid_Ring_Theory. @@ -115,25 +90,25 @@ Hints Immediate equiv_sym. (* Lemmas whose form is x=y are also provided in form y=x because Auto does not symmetry *) -Lemma SSR_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |]. +Lemma SSR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). Auto. Save. -Lemma SSR_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |]. +Lemma SSR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). Auto. Save. -Lemma SSR_plus_zero_left2 : (n:A)[| n == 0 + n |]. +Lemma SSR_plus_zero_left2 : (n:A) n == 0 + n. Auto. Save. -Lemma SSR_mult_one_left2 : (n:A)[| n == 1*n |]. +Lemma SSR_mult_one_left2 : (n:A) n == 1*n. Auto. Save. -Lemma SSR_mult_zero_left2 : (n:A)[| 0 == 0*n |]. +Lemma SSR_mult_zero_left2 : (n:A) 0 == 0*n. Auto. Save. -Lemma SSR_distr_left2 : (n,m,p:A)[| n*p + m*p == (n + m)*p |]. +Lemma SSR_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. Auto. Save. -Lemma SSR_plus_permute : (n,m,p:A)[| n+(m+p) == m+(n+p) |]. +Lemma SSR_plus_permute : (n,m,p:A) n+(m+p) == m+(n+p). Intros. Rewrite (plus_assoc n m p). Rewrite (plus_sym n m). @@ -141,7 +116,7 @@ Rewrite <- (plus_assoc m n p). Trivial. Save. -Lemma SSR_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |]. +Lemma SSR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). Intros. Rewrite (mult_assoc n m p). Rewrite (mult_sym n m). @@ -151,7 +126,7 @@ Save. Hints Resolve SSR_plus_permute SSR_mult_permute. -Lemma SSR_distr_right : (n,m,p:A) [| n*(m+p) == (n*m) + (n*p) |]. +Lemma SSR_distr_right : (n,m,p:A) n*(m+p) == (n*m) + (n*p). Intros. Rewrite (mult_sym n (Aplus m p)). Rewrite (mult_sym n m). @@ -159,37 +134,37 @@ Rewrite (mult_sym n p). Auto. Save. -Lemma SSR_distr_right2 : (n,m,p:A) [| (n*m) + (n*p) == n*(m + p) |]. +Lemma SSR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). Intros. Apply equiv_sym. Apply SSR_distr_right. Save. -Lemma SSR_mult_zero_right : (n:A)[| n*0 == 0|]. +Lemma SSR_mult_zero_right : (n:A) n*0 == 0. Intro; Rewrite (mult_sym n Azero); Auto. Save. -Lemma SSR_mult_zero_right2 : (n:A)[| 0 == n*0 |]. +Lemma SSR_mult_zero_right2 : (n:A) 0 == n*0. Intro; Rewrite (mult_sym n Azero); Auto. Save. -Lemma SSR_plus_zero_right :(n:A)[| n + 0 == n |]. +Lemma SSR_plus_zero_right :(n:A) n + 0 == n. Intro; Rewrite (plus_sym n Azero); Auto. Save. -Lemma SSR_plus_zero_right2 :(n:A)[| n == n + 0 |]. +Lemma SSR_plus_zero_right2 :(n:A) n == n + 0. Intro; Rewrite (plus_sym n Azero); Auto. Save. -Lemma SSR_mult_one_right : (n:A)[| n*1 == n |]. +Lemma SSR_mult_one_right : (n:A) n*1 == n. Intro; Rewrite (mult_sym n Aone); Auto. Save. -Lemma SSR_mult_one_right2 : (n:A)[| n == n*1 |]. +Lemma SSR_mult_one_right2 : (n:A) n == n*1. Intro; Rewrite (mult_sym n Aone); Auto. Save. -Lemma SSR_plus_reg_right : (n,m,p:A) [| m+n == p+n |] -> [| m==p |]. +Lemma SSR_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p. Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n). Intro; Apply plus_reg_left with n; Trivial. Save. @@ -199,15 +174,15 @@ End Theory_of_semi_setoid_rings. Section Theory_of_setoid_rings. Record Setoid_Ring_Theory : Prop := -{ STh_plus_sym : (n,m:A)[| n + m == m + n |]; - STh_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |]; - STh_mult_sym : (n,m:A)[| n*m == m*n |]; - STh_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |]; - STh_plus_zero_left :(n:A)[| 0 + n == n|]; - STh_mult_one_left : (n:A)[| 1*n == n |]; - STh_opp_def : (n:A) [| n + (-n) == 0 |]; - STh_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |]; - STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv x y) +{ STh_plus_sym : (n,m:A) n + m == m + n; + STh_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; + STh_mult_sym : (n,m:A) n*m == m*n; + STh_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; + STh_plus_zero_left :(n:A) 0 + n == n; + STh_mult_one_left : (n:A) 1*n == n; + STh_opp_def : (n:A) n + (-n) == 0; + STh_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; + STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y }. Variable T : Setoid_Ring_Theory. @@ -231,25 +206,25 @@ Hints Resolve plus_sym plus_assoc mult_sym mult_assoc (* Lemmas whose form is x=y are also provided in form y=x because Auto does not symmetry *) -Lemma STh_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |]. +Lemma STh_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). Auto. Save. -Lemma STh_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |]. +Lemma STh_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). Auto. Save. -Lemma STh_plus_zero_left2 : (n:A)[| n == 0 + n |]. +Lemma STh_plus_zero_left2 : (n:A) n == 0 + n. Auto. Save. -Lemma STh_mult_one_left2 : (n:A)[| n == 1*n |]. +Lemma STh_mult_one_left2 : (n:A) n == 1*n. Auto. Save. -Lemma STh_distr_left2 : (n,m,p:A) [| n*p + m*p == (n + m)*p |]. +Lemma STh_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. Auto. Save. -Lemma STh_opp_def2 : (n:A) [| 0 == n + (-n) |]. +Lemma STh_opp_def2 : (n:A) 0 == n + (-n). Auto. Save. -Lemma STh_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |]. +Lemma STh_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). Intros. Rewrite (plus_assoc n m p). Rewrite (plus_sym n m). @@ -257,7 +232,7 @@ Rewrite <- (plus_assoc m n p). Trivial. Save. -Lemma STh_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |]. +Lemma STh_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). Intros. Rewrite (mult_assoc n m p). Rewrite (mult_sym n m). @@ -267,7 +242,7 @@ Save. Hints Resolve STh_plus_permute STh_mult_permute. -Lemma Saux1 : (a:A) [| a + a == a |] -> [| a == 0 |]. +Lemma Saux1 : (a:A) a + a == a -> a == 0. Intros. Rewrite <- (plus_zero_left a). Rewrite (plus_sym Azero a). @@ -277,7 +252,7 @@ Rewrite H. Apply opp_def. Save. -Lemma STh_mult_zero_left :(n:A)[| 0*n == 0 |]. +Lemma STh_mult_zero_left :(n:A) 0*n == 0. Intros. Apply Saux1. Rewrite <- (distr_left Azero Azero n). @@ -286,11 +261,11 @@ Trivial. Save. Hints Resolve STh_mult_zero_left. -Lemma STh_mult_zero_left2 : (n:A)[| 0 == 0*n |]. +Lemma STh_mult_zero_left2 : (n:A) 0 == 0*n. Auto. Save. -Lemma Saux2 : (x,y,z:A) [|x+y==0|] -> [|x+z==0|] -> (Aequiv y z). +Lemma Saux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y == z. Intros. Rewrite <- (plus_zero_left y). Rewrite <- H0. @@ -301,7 +276,7 @@ Rewrite H. Auto. Save. -Lemma STh_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |]. +Lemma STh_opp_mult_left : (x,y:A) -(x*y) == (-x)*y. Intros. Apply Saux2 with (Amult x y); Auto. Rewrite <- (distr_left x (Aopp x) y). @@ -310,49 +285,49 @@ Auto. Save. Hints Resolve STh_opp_mult_left. -Lemma STh_opp_mult_left2 : (x,y:A)[| (-x)*y == -(x*y) |]. +Lemma STh_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y) . Auto. Save. -Lemma STh_mult_zero_right : (n:A)[| n*0 == 0|]. +Lemma STh_mult_zero_right : (n:A) n*0 == 0. Intro; Rewrite (mult_sym n Azero); Auto. Save. -Lemma STh_mult_zero_right2 : (n:A)[| 0 == n*0 |]. +Lemma STh_mult_zero_right2 : (n:A) 0 == n*0. Intro; Rewrite (mult_sym n Azero); Auto. Save. -Lemma STh_plus_zero_right :(n:A)[| n + 0 == n |]. +Lemma STh_plus_zero_right :(n:A) n + 0 == n. Intro; Rewrite (plus_sym n Azero); Auto. Save. -Lemma STh_plus_zero_right2 :(n:A)[| n == n + 0 |]. +Lemma STh_plus_zero_right2 :(n:A) n == n + 0. Intro; Rewrite (plus_sym n Azero); Auto. Save. -Lemma STh_mult_one_right : (n:A)[| n*1 == n |]. +Lemma STh_mult_one_right : (n:A) n*1 == n. Intro; Rewrite (mult_sym n Aone); Auto. Save. -Lemma STh_mult_one_right2 : (n:A)[| n == n*1 |]. +Lemma STh_mult_one_right2 : (n:A) n == n*1. Intro; Rewrite (mult_sym n Aone); Auto. Save. -Lemma STh_opp_mult_right : (x,y:A)[| -(x*y) == x*(-y) |]. +Lemma STh_opp_mult_right : (x,y:A) -(x*y) == x*(-y). Intros. Rewrite (mult_sym x y). Rewrite (mult_sym x (Aopp y)). Auto. Save. -Lemma STh_opp_mult_right2 : (x,y:A)[| x*(-y) == -(x*y) |]. +Lemma STh_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y). Intros. Rewrite (mult_sym x y). Rewrite (mult_sym x (Aopp y)). Auto. Save. -Lemma STh_plus_opp_opp : (x,y:A)[| (-x) + (-y) == -(x+y) |]. +Lemma STh_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y). Intros. Apply Saux2 with (Aplus x y); Auto. Rewrite (STh_plus_permute (Aplus x y) (Aopp x) (Aopp y)). @@ -361,40 +336,40 @@ Rewrite (opp_def y); Rewrite (STh_plus_zero_right x). Rewrite (STh_opp_def2 x); Trivial. Save. -Lemma STh_plus_permute_opp: (n,m,p:A)[| (-m)+(n+p) == n+((-m)+p) |]. +Lemma STh_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p). Auto. Save. -Lemma STh_opp_opp : (n:A)[| -(-n) == n |]. +Lemma STh_opp_opp : (n:A) -(-n) == n. Intro. Apply Saux2 with (Aopp n); Auto. Rewrite (plus_sym (Aopp n) n); Auto. Save. Hints Resolve STh_opp_opp. -Lemma STh_opp_opp2 : (n:A)[| n == -(-n) |]. +Lemma STh_opp_opp2 : (n:A) n == -(-n). Auto. Save. -Lemma STh_mult_opp_opp : (x,y:A)[| (-x)*(-y) == x*y |]. +Lemma STh_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y. Intros. Rewrite (STh_opp_mult_left2 x (Aopp y)). Rewrite (STh_opp_mult_right2 x y). Trivial. Save. -Lemma STh_mult_opp_opp2 : (x,y:A)[| x*y == (-x)*(-y) |]. +Lemma STh_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y). Intros. Apply equiv_sym. Apply STh_mult_opp_opp. Save. -Lemma STh_opp_zero :[| -0 == 0 |]. +Lemma STh_opp_zero : -0 == 0. Rewrite <- (plus_zero_left (Aopp Azero)). Trivial. Save. -Lemma STh_plus_reg_left : (n,m,p:A)[| n+m == n+p |] -> [|m==p|]. +Lemma STh_plus_reg_left : (n,m,p:A) n+m == n+p -> m==p. Intros. Rewrite <- (plus_zero_left m). Rewrite <- (plus_zero_left p). @@ -405,14 +380,14 @@ Rewrite <- (plus_assoc (Aopp n) n p). Auto. Save. -Lemma STh_plus_reg_right : (n,m,p:A)[| m+n == p+n |] -> [|m==p|]. +Lemma STh_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p. Intros. Apply STh_plus_reg_left with n. Rewrite (plus_sym n m); Rewrite (plus_sym n p); Assumption. Save. -Lemma STh_distr_right : (n,m,p:A)[|n*(m+p) == (n*m)+(n*p)|]. +Lemma STh_distr_right : (n,m,p:A) n*(m+p) == (n*m)+(n*p). Intros. Rewrite (mult_sym n (Aplus m p)). Rewrite (mult_sym n m). @@ -420,7 +395,7 @@ Rewrite (mult_sym n p). Trivial. Save. -Lemma STh_distr_right2 : (n,m,p:A)(Aequiv (Aplus (Amult n m) (Amult n p)) (Amult n (Aplus m p))). +Lemma STh_distr_right2 : (n,m,p:A) (n*m)+(n*p) == n*(m+p). Intros. Apply equiv_sym. Apply STh_distr_right. diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 126baea710..c125c4479d 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -56,10 +56,14 @@ exception Found of Gramext.g_assoc open Ppextend let admissible_assoc = function - | Gramext.LeftA, (Gramext.RightA | Gramext.NonA) -> false - | Gramext.RightA, Gramext.LeftA -> false + | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false + | Gramext.RightA, Some Gramext.LeftA -> false | _ -> true +let create_assoc = function + | None -> Gramext.RightA + | Some a -> a + let find_position other assoc lev = let current = List.hd !level_stack in match lev with @@ -67,8 +71,7 @@ let find_position other assoc lev = level_stack := current :: !level_stack; None, (if other then assoc else None), None | Some n -> - let assoc = out_some assoc in - if n = 8 & assoc = Gramext.LeftA then + if n = 8 & assoc = Some Gramext.LeftA then error "Left associativity not allowed at level 8"; let after = ref (8,Gramext.RightA) in let rec add_level q = function @@ -79,17 +82,18 @@ let find_position other assoc lev = if a = Gramext.LeftA then match l with | (p,a)::_ as l' when p = n -> raise (Found a) - | _ -> after := pa; (n,assoc)::l' + | _ -> after := pa; (n,create_assoc assoc)::l' else (* This was not (p,LeftA) hence assoc is LeftA *) - (after := q; (n,assoc)::l') + (after := q; (n,create_assoc assoc)::l') | l -> - after := q; (n,assoc)::l + after := q; (n,create_assoc assoc)::l in try (* Create the entry *) let current = List.hd !level_stack in level_stack := add_level (8,Gramext.RightA) current :: !level_stack; + let assoc = create_assoc assoc in Some (Gramext.After (constr_level !after)), Some assoc, Some (constr_level (n,assoc)) with @@ -138,8 +142,10 @@ let specify_name name e = open Names -let make_act f pil = - let rec make env = function +type 'a action_env = (identifier * 'a) list + +let make_act (f : loc -> constr_expr action_env -> constr_expr) pil = + let rec make (env : constr_expr action_env) = function | [] -> Gramext.action (fun loc -> f loc env) | None :: tl -> (* parse a non-binding item *) @@ -158,8 +164,9 @@ let make_act f pil = failwith "Unexpected entry of type cases pattern" in make [] (List.rev pil) -let make_cases_pattern_act f pil = - let rec make env = function +let make_cases_pattern_act + (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil = + let rec make (env : cases_pattern_expr action_env) = function | [] -> Gramext.action (fun loc -> f loc env) | None :: tl -> (* parse a non-binding item *) @@ -194,24 +201,95 @@ let symbol_of_prod_item univ assoc = function let eobj = build_prod_item univ assoc nt in (eobj, ovar) +let coerce_to_id = function + | CRef (Ident (_,id)) -> id + | c -> + user_err_loc (constr_loc c, "subst_rawconstr", + str"This expression should be a simple identifier") + +let coerce_to_ref = function + | CRef r -> r + | c -> + user_err_loc (constr_loc c, "subst_rawconstr", + str"This expression should be a simple reference") + +let subst_ref loc subst id = + try coerce_to_ref (List.assoc id subst) with Not_found -> Ident (loc,id) + +let subst_pat_id loc subst id = + try List.assoc id subst + with Not_found -> CPatAtom (loc,Some (Ident (loc,id))) + +let subst_id subst id = + try coerce_to_id (List.assoc id subst) with Not_found -> id + +let name_app f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + +let subst_cases_pattern_expr a loc subs = + let rec subst = function + | CPatAlias (_,p,x) -> CPatAlias (loc,subst p,x) + (* No subst in compound pattern ? *) + | CPatCstr (_,ref,pl) -> CPatCstr (loc,ref,List.map subst pl) + | CPatAtom (_,Some (Ident (_,id))) -> subst_pat_id loc subs id + | CPatAtom (_,x) -> CPatAtom (loc,x) + | CPatNumeral (_,n) -> CPatNumeral (loc,n) + | CPatDelimiters (_,key,p) -> CPatDelimiters (loc,key,subst p) + in subst a + +let subst_constr_expr a loc subs = + let rec subst = function + | CRef (Ident (_,id)) -> + (try List.assoc id subs with Not_found -> CRef (Ident (loc,id))) + (* Temporary: no robust treatment of substituted binders *) + | CLambdaN (_,[],c) -> subst c + | CLambdaN (_,([],t)::bl,c) -> subst (CLambdaN (loc,bl,c)) + | CLambdaN (_,((_,na)::bl,t)::bll,c) -> + let na = name_app (subst_id subs) na in + CLambdaN (loc,[[loc,na],subst t], subst (CLambdaN (loc,(bl,t)::bll,c))) + | CProdN (_,[],c) -> subst c + | CProdN (_,([],t)::bl,c) -> subst (CProdN (loc,bl,c)) + | CProdN (_,((_,na)::bl,t)::bll,c) -> + let na = name_app (subst_id subs) na in + CProdN (loc,[[loc,na],subst t], subst (CProdN (loc,(bl,t)::bll,c))) + | CLetIn (_,(_,na),b,c) -> + let na = name_app (subst_id subs) na in + CLetIn (loc,(loc,na),subst b,subst c) + | CArrow (_,a,b) -> CArrow (loc,subst a,subst b) + | CAppExpl (_,Ident (_,id),l) -> + CAppExpl (loc,subst_ref loc subs id,List.map subst l) + | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) + | CApp (_,a,l) -> CApp (loc,subst a,List.map (fun (a,i) -> (subst a,i)) l) + | CCast (_,a,b) -> CCast (loc,subst a,subst b) + | CNotation (_,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,subst t)) l) + | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) + | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x + | CCases (_,po,a,bl) -> + (* TODO: apply g on the binding variables in pat... *) + let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in + CCases (loc,option_app subst po,List.map subst a,bl) + | COrderedCase (_,s,po,a,bl) -> + COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl) + | CFix (_,id,dl) -> + CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl) + | CCoFix (_,id,dl) -> + CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl) + in subst a + let make_rule univ assoc etyp rule = let pil = List.map (symbol_of_prod_item univ assoc) rule.gr_production in let (symbs,ntl) = List.split pil in - let f loc env = match rule.gr_action, env with - | AVar p, [p',a] when p=p' -> a - | AApp (AVar f,[AVar a]), [f',v;a',w] when f=f' & a=a' -> - CApp (loc,v,[w,None]) - | AApp (AVar f,[AVar a]), [a',w;f',v] when f=f' & a=a' -> - CApp (loc,v,[w,None]) - | pat,_ -> CGrammar (loc, pat, env) in let act = match etyp with - | ETPattern -> + | ETPattern -> (* Ugly *) let f loc env = match rule.gr_action, env with - | AVar p, [p',a] when p=p' -> a + | CRef (Ident(_,p)), [p',a] when p=p' -> a | _ -> error "Unable to handle this grammar extension of pattern" in - make_cases_pattern_act f ntl - | _ -> make_act f ntl in + make_cases_pattern_act f ntl + | ETIdent | ETBigint | ETReference -> error "Cannot extend" + | ETConstr _ | ETOther _ -> + make_act (subst_constr_expr rule.gr_action) ntl in (symbs, act) (* Rules of a level are entered in reverse order, so that the first rules diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 8d0dc0f5ca..3313827f1c 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -76,7 +76,7 @@ Grammar constr constr1 := Definition equal := [A:Setoid] <[s:Setoid](Relation |s|)>let (S,R,e)=A in R. -Grammar constr constr1 := +Grammar constr constr1 := NONA equal [ constr0($c) "=" "%" "S" constr0($c2) ] -> [ (equal ? $c $c2) ]. @@ -111,7 +111,7 @@ End Maps. Notation ap := (explicit_ap ? ?). -Grammar constr constr8 := +Grammar constr constr8 := RIGHTA map_setoid [ constr7($c1) "=>" constr8($c2) ] -> [ (Map_setoid $c1 $c2) ]. -- cgit v1.2.3