Commit 5a6d04b9 authored by Mário Pereira's avatar Mário Pereira

Code extraction (printer);

Fold_left for lists and sequences (wip)
parent 67f0aa20
......@@ -259,7 +259,7 @@ module Print = struct
| _ -> assert false in
syntax_arguments s print_constant fmt pvl
| _, Some s, _ ->
syntax_arguments s (print_expr ~paren:true info) fmt pvl
syntax_arguments s (print_expr ~paren:true info) fmt pvl;
| _, _, tl when is_rs_tuple rs ->
fprintf fmt "@[(%a)@]"
(print_list comma (print_expr info)) tl
......@@ -330,7 +330,7 @@ module Print = struct
fprintf fmt "false"
| Eapp (rs, [e1; e2]) when rs_equal rs rs_func_app ->
fprintf fmt (protect_on paren "@[<hov 1>%a %a@]")
(print_expr info) e1 (print_expr info) e2
(print_expr info) e1 (print_expr ~paren:true info) e2
| Eapp (rs, []) ->
(* avoids parenthesis around values *)
fprintf fmt "%a" (print_apply info (Hrs.find_def ht_rs rs rs)) []
......@@ -344,8 +344,8 @@ module Print = struct
| _ -> assert false end in
syntax_arguments s print_constant fmt pvl
| _ ->
fprintf fmt (protect_on paren "%a")
(print_apply info (Hrs.find_def ht_rs rs rs)) pvl end
fprintf fmt (protect_on paren "%a")
(print_apply info (Hrs.find_def ht_rs rs rs)) pvl end
| Ematch (e, pl) ->
fprintf fmt (protect_on paren "begin match @[%a@] with@\n@[%a@] end")
(print_expr info) e (print_list newline (print_branch info)) pl
......@@ -381,7 +381,7 @@ module Print = struct
fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]"
(print_list semi (print_expr info)) el
| Efun (varl, e) ->
fprintf fmt (protect_on paren "@[<hov 2>(fun %a ->@ %a)@]")
fprintf fmt (protect_on paren "@[<hov 2>fun %a ->@ %a@]")
(print_list space (print_vs_arg info)) varl (print_expr info) e
| Ewhile (e1, e2) ->
fprintf fmt "@[<hov 2>while %a do@\n%a@ done@]"
......
......@@ -545,25 +545,25 @@ theory Sum
end
(* TODO: redesign these modules using higher-order instead
(*
(** {2 Induction on lists} *)
theory Induction
use import List
type elt
(* type elt *)
predicate p (list elt)
(* predicate p (list elt) *)
axiom Induction:
p (Nil: list elt) ->
(forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
forall l:list elt. p l
forall p: list 'a -> bool.
p (Nil: list 'a) ->
(forall x:'a. forall l:list 'a. p l -> p (Cons x l)) ->
forall l:list 'a. p l
end
*)
(** {2 Maps as lists of pairs} *)
......@@ -571,14 +571,10 @@ theory Map
use import List
type a
type b
function f a : b
function map (l: list a) : list b =
function map (f: 'a -> 'b) (l: list 'a) : list 'b =
match l with
| Nil -> Nil
| Cons x r -> Cons (f x) (map r)
| Cons x r -> Cons (f x) (map f r)
end
end
......@@ -588,26 +584,35 @@ theory FoldLeft
use import List
function fold_left (f: 'b -> 'a -> b') (acc: 'b) (l: list 'a) : 'b =
function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (l: list 'a) : 'b =
match l with
| Nil -> acc
| Cons x r -> fold_left (f acc x) r
| Cons x r -> fold_left f (f acc x) r
end
use import Append
lemma fold_left_append:
forall l1"induction" l2: list 'a, f: 'b -> 'a -> 'b, acc : 'b.
fold_left f acc (l1++l2) = fold_left f (fold_left f acc l1) l2
(* lemma fold_left_step: *)
(* forall l: list 'a, f: 'b -> 'a -> 'b, acc : 'b, x: 'a. *)
(* f (fold_left f acc l) x = fold_left f acc (Cons x l) *)
end
theory FoldRight
use import List
function fold_right (f: 'a -> 'b -> b') (l: list 'a) (acc: 'b) : 'b =
function fold_right (f: 'a -> 'b -> 'b) (l: list 'a) (acc: 'b) : 'b =
match l with
| Nil -> acc
| Cons x r -> f x (fold_right r acc)
| Cons x r -> f x (fold_right f r acc)
end
end
*)
(** {2 Importation of all list theories in one} *)
......
......@@ -179,11 +179,10 @@ theory OfList
use import list.Nth
use import list.Append
function of_list (l: list 'a) : seq 'a
= match l with
| Nil -> empty
| Cons x r -> cons x (of_list r)
end
function of_list (l: list 'a) : seq 'a = match l with
| Nil -> empty
| Cons x r -> cons x (of_list r)
end
meta coercion function of_list
lemma length_of_list:
......@@ -441,6 +440,30 @@ theory Permut
end
theory FoldLeft
use import Seq
use import int.Int
function fold ('b -> 'a -> 'b) 'b (seq 'a) int : 'b
axiom fold_stop: forall f: 'b -> 'a -> 'b, acc: 'b, s: seq 'a, i: int.
i >= length s -> fold f acc s i = acc
axiom fold_loop: forall f: 'b -> 'a -> 'b, acc: 'b, s: seq 'a, i: int.
i < length s -> fold f acc s i = fold f (f acc s[i]) s (i+1)
function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (s: seq 'a) : 'b =
fold f acc s 0
use import list.List
use import OfList
use list.FoldLeft as List
lemma fold_left_equiv: forall l: list 'a, f: 'b -> 'a -> 'b, acc : 'b.
List.fold_left f acc l = fold_left f acc (of_list l)
end
(* TODO / TO DISCUSS
- what about s[i..j] when i..j is not a valid range?
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment