Commit 5d817e7e authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: fixed bug in typing (patterns)

parent 30b2bf6b
...@@ -159,11 +159,11 @@ programs bench/programs/good ...@@ -159,11 +159,11 @@ programs bench/programs/good
programs examples/programs programs examples/programs
echo "" echo ""
# echo "=== VC generation on good programs ===" *) echo "=== VC generation on good programs ==="
# pgml_options= *) pgml_options=
# programs bench/programs/good *) programs bench/programs/good
# programs examples/programs *) # programs examples/programs
# echo "" *) echo ""
# echo "=== Checking valid goals ===" *) # echo "=== Checking valid goals ===" *)
# valid_goals bench/valid *) # valid_goals bench/valid *)
......
...@@ -180,7 +180,6 @@ let harness () = ...@@ -180,7 +180,6 @@ let harness () =
let get_b_0 = get b 0 in assert { get_b_0 = default }; let get_b_0 = get b 0 in assert { get_b_0 = default };
() ()
end end
(* (*
......
...@@ -1075,10 +1075,11 @@ and add_binder env (i, v) = ...@@ -1075,10 +1075,11 @@ and add_binder env (i, v) =
env, vs env, vs
let rec pattern env p = let rec pattern env p =
let env, n = pattern_node env p.ipat_node in let ty = purify p.ipat_pat.pat_ty in
env, { ppat_pat = p.ipat_pat; ppat_node = n } let env, (lp, n) = pattern_node env ty p.ipat_node in
env, { ppat_pat = lp; ppat_node = n }
and pattern_node env p = and pattern_node env ty p =
let add1 env i = let add1 env i =
let v = let v =
create_pvsymbol (id_clone i.i_pgm.vs_name) ~vs:i.i_logic create_pvsymbol (id_clone i.i_pgm.vs_name) ~vs:i.i_logic
...@@ -1088,21 +1089,22 @@ and pattern_node env p = ...@@ -1088,21 +1089,22 @@ and pattern_node env p =
in in
match p with match p with
| IPwild -> | IPwild ->
env, Pwild env, (pat_wild ty, Pwild)
| IPapp (ls, pl) -> | IPapp (ls, pl) ->
let env, pl = map_fold_left pattern env pl in let env, pl = map_fold_left pattern env pl in
env, Papp (ls, pl) let lpl = List.map (fun p -> p.ppat_pat) pl in
env, (pat_app ls lpl ty, Papp (ls, pl))
| IPor (p1, p2) -> | IPor (p1, p2) ->
let env, p1 = pattern env p1 in let env, p1 = pattern env p1 in
let _ , p2 = pattern env p2 in let _ , p2 = pattern env p2 in
env, Por (p1, p2) env, (pat_or p1.ppat_pat p2.ppat_pat, Por (p1, p2))
| IPvar vs -> | IPvar vs ->
let env, v = add1 env vs in let env, v = add1 env vs in
env, Pvar v env, (pat_var v.pv_vs, Pvar v)
| IPas (p, vs) -> | IPas (p, vs) ->
let env, v = add1 env vs in let env, v = add1 env vs in
let env, p = pattern env p in let env, p = pattern env p in
env, Pas (p, v) env, (pat_as p.ppat_pat v.pv_vs, Pas (p, v))
let make_apply loc e1 ty c = let make_apply loc e1 ty c =
let x = create_pvsymbol (id_fresh "f") (tpure e1.expr_type) in let x = create_pvsymbol (id_fresh "f") (tpure e1.expr_type) in
......
...@@ -4,17 +4,6 @@ module P ...@@ -4,17 +4,6 @@ module P
use import int.Int use import int.Int
use import module stdlib.Ref use import module stdlib.Ref
use import list.List
use import list.Length
let rec length_ (l : list 'a) variant { length l } =
{}
match l with
| Nil -> 0
| Cons _ r -> 1 + length_ r
end
{ result = length l }
(* parameter b : ref int *) (* parameter b : ref int *)
(* let f () = *) (* let f () = *)
......
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