diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-25 11:57:31 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-25 11:57:31 +0000 |
commit | 6faaf8f7bb9f14fa0f9f46c3d2e21373c9077190 (patch) | |
tree | 8284f9a09d87bb65ed7277c7e6de538d7ae25043 | |
parent | 0da6cf417bdab6d5768dad8e47e3c1ea18c1e709 (diff) |
Fixing and completing interpretation of let's in notations for iterated binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | interp/constrintern.ml | 27 | ||||
-rw-r--r-- | test-suite/output/Notations2.out | 7 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 8 |
3 files changed, 32 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 9a599c8ab..d23d9b5cf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -491,6 +491,19 @@ let traverse_binder (terms,_,_ as subst) let renaming' = if id=id' then renaming else (id,id')::renaming in (renaming',env), Name id' +let make_letins loc = List.fold_right (fun (na,b,t) c -> GLetIn (loc,na,b,c)) + +let rec subordinate_letins letins = function + (* binders come in reverse order; the non-let are returned in reverse order together *) + (* with the subordinated let-in in writing order *) + | (na,_,Some b,t)::l -> + subordinate_letins ((na,b,t)::letins) l + | (na,bk,None,t)::l -> + let letins',rest = subordinate_letins [] l in + letins',((na,bk,t),letins)::rest + | [] -> + letins,[] + let rec subst_iterator y t = function | GVar (_,id) as x -> if id = y then t else x | x -> map_glob_constr (subst_iterator y t) x @@ -536,19 +549,21 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = List.assoc x binders in let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in + let letins,bl = subordinate_letins [] bl in let termin = aux subst' (renaming,env) terminator in - List.fold_left (fun t binder -> + let res = List.fold_left (fun t binder -> subst_iterator ldots_var t (aux (terms,Some(x,binder)) subinfos iter)) - termin bl + termin bl in + make_letins loc letins res with Not_found -> anomaly "Inconsistent substitution of recursive notation") | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> - let (na,bk,_,t) = snd (Option.get binderopt) in - GProd (loc,na,bk,t,aux subst' infos c') + let (na,bk,t),letins = snd (Option.get binderopt) in + GProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> - let (na,bk,_,t) = snd (Option.get binderopt) in - GLambda (loc,na,bk,t,aux subst' infos c') + let (na,bk,t),letins = snd (Option.get binderopt) in + GLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) | t -> glob_constr_of_aconstr_with_binders loc (traverse_binder subst) (aux subst') subinfos t diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 783b30c0f..2e0e145e1 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -14,6 +14,11 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 : Prop +∃ x y : nat, +let b := 1 in +let c := b in +let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d + : Prop ∀ n p : nat, n + p = 0 : Prop λ n p : nat, n + p = 0 @@ -25,7 +30,7 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 λ A : Type, ∀ n p : A, n = p : Type -> Prop Defining 'let'' as keyword -let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in (f(0)) 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 4f9b9ccc7..e902a3c27 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -31,11 +31,13 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x). (* Test notations with binders *) -Notation "∃ x .. y , P":= - (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity). Check (∃ n p, n+p=0). +Check ∃ (a:=0) (x:nat) y (b:=1) (c:=b) (d:=2) z (e:=3) (f:=4), x+y = z+d. + Notation "∀ x .. y , P":= (forall x, .. (forall y, P) ..) (x binder, at level 200, right associativity). @@ -57,7 +59,7 @@ Notation "'let'' f x .. y := t 'in' u":= (f ident, x closed binder, y closed binder, at level 200, right associativity). -Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2. +Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* In practice, only the printing rule is used here *) (* Note: does not work for pattern *) |