diff options
| -rw-r--r-- | coqpp/coqpp_ast.mli | 2 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll | 15 | ||||
| -rw-r--r-- | coqpp/coqpp_main.ml | 16 | ||||
| -rw-r--r-- | theories/Lists/List.v | 91 |
4 files changed, 113 insertions, 11 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 181c43615b..956a916792 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -11,7 +11,7 @@ type loc = { loc_end : Lexing.position; } -type code = { code : string } +type code = { code : string; loc : loc; } type user_symbol = | Ulist1 of user_symbol diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index bfa4e2b57b..81a53e887b 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -29,6 +29,7 @@ let newline lexbuf = let num_comments = ref 0 let num_braces = ref 0 +let ocaml_start_pos = ref Lexing.dummy_pos let mode () = if !num_braces = 0 then Extend else OCaml @@ -57,10 +58,10 @@ let end_comment lexbuf = else None -let start_ocaml _ = +let start_ocaml lexbuf = let () = match mode () with | OCaml -> Buffer.add_string ocaml_buf "{" - | Extend -> () + | Extend -> ocaml_start_pos := lexeme_start_p lexbuf in incr num_braces @@ -70,7 +71,11 @@ let end_ocaml lexbuf = else if !num_braces = 0 then let s = Buffer.contents ocaml_buf in let () = Buffer.reset ocaml_buf in - Some (CODE { Coqpp_ast.code = s }) + let loc = { + Coqpp_ast.loc_start = !ocaml_start_pos; + Coqpp_ast.loc_end = lexeme_end_p lexbuf + } in + Some (CODE { Coqpp_ast.code = s; loc }) else let () = Buffer.add_string ocaml_buf "}" in None @@ -87,7 +92,7 @@ let number = [ '0'-'9' ] rule extend = parse | "(*" { start_comment (); comment lexbuf } -| "{" { start_ocaml (); ocaml lexbuf } +| "{" { start_ocaml lexbuf; ocaml lexbuf } | "GRAMMAR" { GRAMMAR } | "VERNAC" { VERNAC } | "TACTIC" { TACTIC } @@ -127,7 +132,7 @@ rule extend = parse | eof { EOF } and ocaml = parse -| "{" { start_ocaml (); ocaml lexbuf } +| "{" { start_ocaml lexbuf; ocaml lexbuf } | "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf } | '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf } | '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index a8ed95f5ba..d9fff46d88 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -21,6 +21,13 @@ let pr_loc loc = let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos +let print_code fmt c = + let loc = c.loc.loc_start in + (** Print the line location as a source annotation *) + let padding = String.make (loc.pos_cnum - loc.pos_bol + 1) ' ' in + let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in + fprintf fmt "@[@<0>%s@]@\n" code_insert + let parse_file f = let chan = open_in f in let lexbuf = Lexing.from_channel chan in @@ -181,8 +188,7 @@ let print_fun fmt (vars, body) = in let () = fprintf fmt "fun@ " in let () = List.iter iter vars in - (* FIXME: use Coq locations in the macros *) - let () = fprintf fmt "loc ->@ @[%s@]" body.code in + let () = fprintf fmt "loc ->@ @[%a@]" print_code body in () (** Meta-program instead of calling Tok.of_pattern here because otherwise @@ -304,8 +310,8 @@ let rec print_binders fmt = function fprintf fmt "%s@ %a" id print_binders rem let print_rule fmt r = - fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]" - print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code + fprintf fmt "@[TyML (%a, @[fun %a -> %a@])@]" + print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body let rec print_rules fmt = function | [] -> () @@ -338,7 +344,7 @@ let declare_plugin fmt name = fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name let pr_ast fmt = function -| Code s -> fprintf fmt "%s@\n" s.code +| Code s -> fprintf fmt "%a@\n" print_code s | Comment s -> fprintf fmt "%s@\n" s | DeclarePlugin name -> declare_plugin fmt name | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ca5f154e95..4614d215eb 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1023,6 +1023,18 @@ Proof. intros; rewrite H by intuition; rewrite IHl; auto. Qed. +Lemma ext_in_map : + forall (A B : Type)(f g:A->B) l, map f l = map g l -> forall a, In a l -> f a = g a. +Proof. induction l; intros [=] ? []; subst; auto. Qed. + +Arguments ext_in_map [A B f g l]. + +Lemma map_ext_in_iff : + forall (A B : Type)(f g:A->B) l, map f l = map g l <-> forall a, In a l -> f a = g a. +Proof. split; [apply ext_in_map | apply map_ext_in]. Qed. + +Arguments map_ext_in_iff [A B f g l]. + Lemma map_ext : forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l. Proof. @@ -1717,6 +1729,32 @@ Section Cutting. end end. + Lemma firstn_skipn_comm : forall m n l, + firstn m (skipn n l) = skipn n (firstn (n + m) l). + Proof. now intros m; induction n; intros []; simpl; destruct m. Qed. + + Lemma skipn_firstn_comm : forall m n l, + skipn m (firstn n l) = firstn (n - m) (skipn m l). + Proof. now induction m; intros [] []; simpl; rewrite ?firstn_nil. Qed. + + Lemma skipn_O : forall l, skipn 0 l = l. + Proof. reflexivity. Qed. + + Lemma skipn_nil : forall n, skipn n ([] : list A) = []. + Proof. now intros []. Qed. + + Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l. + Proof. reflexivity. Qed. + + Lemma skipn_none : forall l, skipn (length l) l = []. + Proof. now induction l. Qed. + + Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = []. + Proof. + intros l L%Nat.sub_0_le; rewrite <-(firstn_all l) at 1. + now rewrite skipn_firstn_comm, L. + Qed. + Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l. Proof. induction n. @@ -1730,6 +1768,51 @@ Section Cutting. induction n; destruct l; simpl; auto. Qed. + Lemma skipn_length n : + forall l, length (skipn n l) = length l - n. + Proof. + induction n. + - intros l; simpl; rewrite Nat.sub_0_r; reflexivity. + - destruct l; simpl; auto. + Qed. + + Lemma skipn_all l: skipn (length l) l = nil. + Proof. now induction l. Qed. + + Lemma skipn_app n : forall l1 l2, + skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2). + Proof. induction n; auto; intros [|]; simpl; auto. Qed. + + Lemma firstn_skipn_rev: forall x l, + firstn x l = rev (skipn (length l - x) (rev l)). + Proof. + intros x l; rewrite <-(firstn_skipn x l) at 3. + rewrite rev_app_distr, skipn_app, rev_app_distr, rev_length, + skipn_length, Nat.sub_diag; simpl; rewrite rev_involutive. + rewrite <-app_nil_r at 1; f_equal; symmetry; apply length_zero_iff_nil. + repeat rewrite rev_length, skipn_length; apply Nat.sub_diag. + Qed. + + Lemma firstn_rev: forall x l, + firstn x (rev l) = rev (skipn (length l - x) l). + Proof. + now intros x l; rewrite firstn_skipn_rev, rev_involutive, rev_length. + Qed. + + Lemma skipn_rev: forall x l, + skipn x (rev l) = rev (firstn (length l - x) l). + Proof. + intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. + destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. + - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. + now rewrite L, Nat.sub_0_r, skipn_none. + - replace (length (rev l) - (length (rev l) - x)) + with (length (rev l) + x - length (rev l)). + rewrite minus_plus. reflexivity. + rewrite <- (Nat.sub_add _ _ L) at 2. + now rewrite <-!(Nat.add_comm x), <-minus_plus_simpl_l_reverse. + Qed. + Lemma removelast_firstn : forall n l, n < length l -> removelast (firstn (S n) l) = firstn n l. Proof. @@ -2073,6 +2156,14 @@ Section NatSeq. rewrite in_seq. intros (H,_). apply (Lt.lt_irrefl _ H). Qed. + Lemma seq_app : forall len1 len2 start, + seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2. + Proof. + induction len1 as [|len1' IHlen]; intros; simpl in *. + - now rewrite Nat.add_0_r. + - now rewrite Nat.add_succ_r, IHlen. + Qed. + End NatSeq. Section Exists_Forall. |