diff options
| -rw-r--r-- | interp/constrextern.ml | 44 | ||||
| -rw-r--r-- | test-suite/output/Implicit.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Implicit.v | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations5.out | 26 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 26 |
5 files changed, 72 insertions, 38 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3667757a2f..43fef8685d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -636,10 +636,10 @@ exception Expl (* If the removal of implicit arguments is not possible, raise [Expl] *) (* [inctx] tells if the term is in a context which will enforce the external type *) (* [n] is the total number of arguments block to which the [args] belong *) -let adjust_implicit_arguments inctx n q args impl = - let rec exprec q = function +let adjust_implicit_arguments inctx n args impl = + let rec exprec = function | a::args, imp::impl when is_status_implicit imp -> - let tail = exprec (q+1) (args,impl) in + let tail = exprec (args,impl) in let visible = !Flags.raw_print || (!print_implicits && !print_implicits_explicit_args) || @@ -652,13 +652,13 @@ let adjust_implicit_arguments inctx n q args impl = (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail else tail - | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl) + | a::args, _::impl -> (Lazy.force a,None) :: exprec (args,impl) | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*) | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp -> (* The non-explicit application cannot be parsed back with the same type *) raise Expl | [], _ -> [] - in exprec q (args,impl) + in exprec (args,impl) let extern_projection (cf,f) args impl = let ip = is_projection (List.length args) cf in @@ -750,14 +750,14 @@ let extern_applied_ref inctx impl (cf,f) us args = match extern_projection (cf,f) args impl with (* Try a [t.(f args1) args2] projection-style notation *) | Some (i,(args1,impl1),(args2,impl2)) -> - let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in - let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in + let args1 = adjust_implicit_arguments inctx n args1 impl1 in + let args2 = adjust_implicit_arguments inctx n args2 impl2 in let ip = Some (List.length args1) in CApp ((ip,f),args1@args2) (* A normal application node with each individual implicit arguments either dropped or made explicit *) | None -> - let args = adjust_implicit_arguments inctx n 1 args impl in + let args = adjust_implicit_arguments inctx n args impl in if args = [] then ref else CApp ((None, f), args) with Expl -> (* A [@f args] node *) @@ -765,10 +765,10 @@ let extern_applied_ref inctx impl (cf,f) us args = let isproj = if !print_projections then isproj else None in CAppExpl ((isproj,f,us), args) -let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs = +let extern_applied_syntactic_definition inctx n extraimpl (cf,f) syndefargs extraargs = try let syndefargs = List.map (fun a -> (a,None)) syndefargs in - let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in + let extraargs = adjust_implicit_arguments inctx n extraargs extraimpl in let args = syndefargs @ extraargs in if args = [] then cf else CApp ((None, CAst.make cf), args) with Expl -> @@ -784,12 +784,12 @@ let mkFlattenedCApp (head,args) = | _ -> CApp ((None, head), args) -let extern_applied_notation n impl f args = +let extern_applied_notation inctx n impl f args = if List.is_empty args then f.CAst.v else try - let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in + let args = adjust_implicit_arguments inctx n args impl in mkFlattenedCApp (f,args) with Expl -> raise No_match @@ -940,11 +940,11 @@ let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> - (try extern_notations scopes vars (Some nargs) r + (try extern_notations inctx scopes vars (Some nargs) r with No_match -> extern inctx scopes vars r') | None -> - try extern_notations scopes vars None r + try extern_notations inctx scopes vars None r with No_match -> let loc = r.CAst.loc in @@ -1000,7 +1000,7 @@ let rec extern inctx ?impargs scopes vars r = mkFlattenedCApp (head,args)) | GLetIn (na,b,t,c) -> - CLetIn (make ?loc na,sub_extern false scopes vars b, + CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b, Option.map (extern_typ scopes vars) t, extern inctx ?impargs scopes (add_vname vars na) c) @@ -1197,7 +1197,7 @@ and extern_local_binder scopes vars = function extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, CLocalDef(CAst.make na, extern false scopes vars bd, - Option.map (extern false scopes vars) ty) :: l) + Option.map (extern_typ scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> let implicit_type = is_reserved_type na ty in @@ -1225,14 +1225,14 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notations scopes vars nargs t = +and extern_notations inctx scopes vars nargs t = if !Flags.raw_print || !print_no_symbol then raise No_match; try extern_possible_prim_token scopes t with No_match -> let t = flatten_application t in - extern_notation scopes vars t (filter_enough_applied nargs (uninterp_notations t)) + extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t)) -and extern_notation (custom,scopes as allscopes) vars t rules = +and extern_notation inctx (custom,scopes as allscopes) vars t rules = match rules with | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> @@ -1313,7 +1313,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in - CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args) + CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -1323,13 +1323,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let a = CRef (cf,None) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in - let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in + let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in if isCRef_no_univ c.CAst.v && entry_has_global custom then c else match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> insert_entry_coercion coercion c with - No_match -> extern_notation allscopes vars t rules + No_match -> extern_notation inctx allscopes vars t rules let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 2265028d3e..d8b88b8c1c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -17,3 +17,7 @@ fix f (x : nat) : option nat := match x with | S _ => x end : nat -> option nat +fun x : False => let y := False_rect (A:=bool) x in y + : False -> bool +fun x : False => let y : True := False_rect x in y + : False -> True diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index a7c4399e38..86420bd8c8 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -61,3 +61,13 @@ Coercion some_nat := @Some nat. Check fix f x := match x with 0 => None | n => some_nat n end. End MatchBranchesInContext. + +Module LetInContext. + +Set Implicit Arguments. +Set Contextual Implicit. +Axiom False_rect : forall A:Type, False -> A. +Check fun x:False => let y:= False_rect (A:=bool) x in y. (* will not be in context: explicitation *) +Check fun x:False => let y:= False_rect (A:=True) x in y. (* will be in context: no explicitation *) + +End LetInContext. diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index f59306c454..a6c2553a89 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -146,8 +146,10 @@ v : forall (B : Type) (b : B), 0 = 0 /\ b = b @v 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b -v 0 (B:=bool) +v 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=v 0 (B:=bool)} + : nat v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b v 0 @@ -166,8 +168,10 @@ v : forall (B : Type) (b : B), 0 = 0 /\ b = b @v 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b -v 0 (B:=bool) +v 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=v 0 (B:=bool)} + : nat ## : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where @@ -192,10 +196,12 @@ where : 0 = 0 /\ true = true ## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=## 0 0 (B:=bool)} + : nat ## ?A : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where @@ -230,10 +236,12 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=## 0 0 (B:=bool)} + : nat ## 0 0 true : 0 = 0 /\ true = true ## 0 0 true @@ -246,10 +254,12 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=## 0 0 (B:=bool)} + : nat ## 0 0 true : 0 = 0 /\ true = true ## 0 0 true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index 09d5e31c48..010b0da4a9 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -189,7 +189,9 @@ Module AppliedTermsPrinting. Check @v 0. (* @v 0 *) Check @p nat 0 0 bool. - (* v 0 (B:=bool) *) + (* v 0 *) + Eval simpl in (fun x => _:nat) (@p nat 0 0 bool). + (* ?n@{x:=v 0 (B:=bool)} *) End AtAbbreviationForPartialApplication. @@ -217,7 +219,9 @@ Module AppliedTermsPrinting. Check @v 0. (* @v 0 *) Check @p nat 0 0 bool. - (* v 0 (B:=bool) *) + (* v 0 *) + Eval simpl in (fun x => _:nat) (@p nat 0 0 bool). + (* ?n@{x:=v 0 (B:=bool)} *) End AbbreviationForPartialApplication. @@ -247,9 +251,11 @@ Module AppliedTermsPrinting. Check ## 0 0 true. (* ## 0 0 true *) Check p 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) Check ## 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) + Eval simpl in (fun x => _:nat) (@p nat 0 0 bool). + (* ?n@{x:=## 0 0 (B:=bool)} *) End NotationForHeadApplication. @@ -301,9 +307,11 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) Check ## 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) + Eval simpl in (fun x => _:nat) (## 0 0 (B:=bool)). + (* ?n@{## 0 0 (B:=bool)} *) Check p 0 0 true. (* ## 0 0 true *) Check ## 0 0 true. @@ -327,9 +335,11 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) Check ## 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) + Eval simpl in (fun x => _:nat) (## 0 0 (B:=bool)). + (* ?n@{## 0 0 (B:=bool)} *) Check p 0 0 true. (* ## 0 0 true *) Check ## 0 0 true. |