Commit 602cd848 authored by Andrei Paskevich's avatar Andrei Paskevich

disjunctive patterns

parent ab753d4f
theory A
type list 'a = Nil | Cons 'a (list 'a)
axiom A : forall l:int list. match l with Cons x x -> true | Nil -> false end
axiom A : forall l: list int. match l with Cons x x -> true | Nil -> false end
end
theory A
type list 'a = Nil | Cons 'a (list 'a)
axiom A : forall l:int list. (match l with Cons x x -> 0 | Nil -> 1 end) = 2
axiom A : forall l:list int. (match l with Cons x x -> 0 | Nil -> 1 end) = 2
end
......@@ -2,14 +2,13 @@ theory Induction2
use import list.List
use import list.Length
logic p ('a list, 'b list)
logic p (list 'a) (list 'b)
axiom Induction :
p(Nil : 'a list, Nil : 'b list) ->
(forall x1:'a, x2:'b, l1:'a list, l2:'b list.
p(l1, l2) -> p(Cons(x1,l1), Cons(x2,l2))) ->
forall l1:'a list, l2:'b list. length(l1)=length(l2) -> p(l1, l2)
p (Nil : list 'a) (Nil : list 'b) ->
(forall x1:'a, x2:'b, l1:list 'a, l2:list 'b.
p l1 l2 -> p (Cons x1 l1) (Cons x2 l2)) ->
forall l1:list 'a, l2:list 'b. length l1 = length l2 -> p l1 l2
end
theory Test1
......@@ -17,31 +16,31 @@ theory Test1
use export list.List
use export list.Length
goal G1 : length(Cons(1, Nil)) = 1
goal G2 : length(Cons(1, Cons (2, Nil))) = 1 + 1
goal G1 : length (Cons 1 Nil) = 1
goal G2 : length (Cons 1 (Cons 2 Nil)) = 1 + 1
logic zip(l1 : 'a list, l2 : 'b list) : ('a * 'b) list =
logic zip (l1 : list 'a) (l2 : list 'b) : list ('a,'b) =
match l1, l2 with
| Cons (x1, r1), Cons (x2, r2) -> Cons ((x1, x2), zip (r1, r2))
| _, _ -> Nil (* to make it total *)
| Cons x1 r1, Cons x2 r2 -> Cons (x1,x2) (zip r1 r2)
| (Cons _ _|Nil), _ -> Nil (* to make it total *)
end
logic foo(l1 : 'a list, l2 : 'b list) =
length(zip(l1, l2)) = length(l1)
logic foo (l1 : list 'a) (l2 : list 'b) =
length (zip l1 l2) = length l1
clone Induction2 with logic p = foo
lemma G3 : forall l1: 'a list, l2 : 'b list.
length(l1) = length(l2) ->
length(zip(l1, l2)) = length(l1)
lemma G3 : forall l1: list 'a, l2 : list 'b.
length l1 = length l2 ->
length (zip l1 l2) = length l1
goal G4 : zip(Cons(1, Cons(2, Nil)),
Cons(1., Cons(2., Nil))) =
Cons ((1, 1.), Cons((2, 2.), Nil))
goal G4 : zip (Cons 1 (Cons 2 Nil))
(Cons 1. (Cons 2. Nil)) =
Cons (1, 1.) (Cons (2, 2.) Nil)
goal G5 : forall l1: 'a list, l2 : 'b list, l3: 'c list, l4: 'd list.
length(l1) = length(l2) and length(l2) = length(l3) and
length(l3) = length(l4) ->
length(zip(zip(l1,l2), zip(l3, l4))) = length(l3)
goal G5 : forall l1: list 'a, l2 : list 'b, l3: list 'c, l4: list 'd.
length l1 = length l2 and length l2 = length l3 and
length l3 = length l4 ->
length (zip (zip l1 l2) (zip l3 l4)) = length l3
end
......@@ -498,17 +498,17 @@ let find_prop_decl kn pr =
exception NonExhaustiveExpr of (pattern list * expr)
let rec check_matchT kn () t = match t.t_node with
| Tcase (tl,bl) ->
let bl = List.map t_open_branch bl in
ignore (try Pattern.CompileTerm.compile (find_constructors kn) tl bl
| Tcase (t1,bl) ->
let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Term t)));
t_fold (check_matchT kn) (check_matchF kn) () t
| _ -> t_fold (check_matchT kn) (check_matchF kn) () t
and check_matchF kn () f = match f.f_node with
| Fcase (tl,bl) ->
let bl = List.map f_open_branch bl in
ignore (try Pattern.CompileFmla.compile (find_constructors kn) tl bl
| Fcase (t1,bl) ->
let bl = List.map (fun b -> let p,f = f_open_branch b in [p],f) bl in
ignore (try Pattern.CompileFmla.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));
f_fold (check_matchT kn) (check_matchF kn) () f
| _ -> f_fold (check_matchT kn) (check_matchF kn) () f
......
......@@ -53,6 +53,7 @@ module Compile (X : Action) = struct
let rec populate types p = match p.pat_node with
| Pwild | Pvar _ -> types
| Pas (p,_) -> populate types p
| Por (p,q) -> populate (populate types p) q
| Papp (fs,pl) ->
if Sls.mem fs css then Mls.add fs pl types
else raise (ConstructorExpected fs)
......@@ -73,6 +74,8 @@ module Compile (X : Action) = struct
match p.pat_node with
| Papp (fs,pl') ->
add_case fs (List.rev_append pl' pl) a cases, wilds
| Por (p,q) ->
dispatch (p::pl, a) (dispatch (q::pl, a) (cases,wilds))
| Pas (p,x) ->
dispatch (p::pl, mk_let x t a) (cases,wilds)
| Pvar x ->
......@@ -121,15 +124,12 @@ end
module CompileTerm = Compile (struct
type action = term
let mk_let v s t = t_let v s t
let mk_case t bl =
let ty = (snd (List.hd bl)).t_ty in
t_case [t] (List.map (fun (p,a) -> [p],a) bl) ty
let mk_case t bl = t_case t bl (snd (List.hd bl)).t_ty
end)
module CompileFmla = Compile (struct
type action = fmla
let mk_let v t f = f_let v t f
let mk_case t bl =
f_case [t] (List.map (fun (p,a) -> [p],a) bl)
let mk_case t bl = f_case t bl
end)
......@@ -40,7 +40,7 @@ let iprinter,tprinter,lprinter,pprinter =
let usanitize = sanitizer char_to_ualpha char_to_alnumus in
create_ident_printer bl ~sanitizer:isanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:isanitize,
create_ident_printer bl ~sanitizer:usanitize
let forget_all () =
......@@ -92,6 +92,8 @@ let protect_on x s = if x then "(" ^^ s ^^ ")" else s
let rec print_ty_node inn fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
(print_list comma (print_ty_node false)) tl
| Tyapp (ts, []) -> print_ts fmt ts
| Tyapp (ts, tl) -> fprintf fmt (protect_on inn "%a@ %a")
print_ts ts (print_list space (print_ty_node true)) tl
......@@ -119,16 +121,27 @@ let unambig_fs fs =
(** Patterns, terms, and formulas *)
let rec print_pat_node inn fmt p = match p.pat_node with
| Pwild -> fprintf fmt "_"
| Pvar v -> print_vs fmt v
| Pas (p,v) -> fprintf fmt (protect_on inn "%a as %a")
(print_pat_node false) p print_vs v
| Papp (cs,[]) -> print_cs fmt cs
| Papp (cs,pl) -> fprintf fmt (protect_on inn "%a@ %a")
print_cs cs (print_list space (print_pat_node true)) pl
let print_pat = print_pat_node false
let rec print_pat_node pri fmt p = match p.pat_node with
| Pwild ->
fprintf fmt "_"
| Pvar v ->
print_vs fmt v
| Pas (p, v) ->
fprintf fmt (protect_on (pri > 1) "%a as %a")
(print_pat_node 1) p print_vs v
| Por (p, q) ->
fprintf fmt (protect_on (pri > 0) "%a | %a")
(print_pat_node 0) p (print_pat_node 0) q
| Papp (cs, pl) when is_fs_tuple cs ->
fprintf fmt (protect_on (pri > 0) "%a")
(print_list comma (print_pat_node 1)) pl
| Papp (cs, []) ->
print_cs fmt cs
| Papp (cs, pl) ->
fprintf fmt (protect_on (pri > 1) "%a@ %a")
print_cs cs (print_list space (print_pat_node 2)) pl
let print_pat = print_pat_node 0
let print_vsty fmt v =
fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
......@@ -171,6 +184,8 @@ and print_tnode pri fmt t = match t.t_node with
print_vs fmt v
| Tconst c ->
print_const fmt c
| Tapp (fs, tl) when is_fs_tuple fs ->
fprintf fmt "(%a)" (print_list comma print_term) tl
| Tapp (fs, []) when unambig_fs fs ->
print_ls fmt fs
| Tapp (fs, []) ->
......@@ -191,10 +206,9 @@ and print_tnode pri fmt t = match t.t_node with
fprintf fmt (protect_on (pri > 0) "let %a =@ %a in@ %a")
print_vs v (print_lterm 4) t1 print_term t2;
forget_var v
| Tcase (tl,bl) ->
| Tcase (t1,bl) ->
fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
(print_list comma print_term) tl
(print_list newline print_tbranch) bl
print_term t1 (print_list newline print_tbranch) bl
| Teps fb ->
let v,f = f_open_bound fb in
fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
......@@ -233,22 +247,19 @@ and print_fnode pri fmt f = match f.f_node with
fprintf fmt (protect_on (pri > 0) "let %a =@ %a in@ %a")
print_vs v (print_lterm 4) t print_fmla f;
forget_var v
| Fcase (tl,bl) ->
| Fcase (t,bl) ->
fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
(print_list comma print_term) tl
(print_list newline print_fbranch) bl
print_term t (print_list newline print_fbranch) bl
and print_tbranch fmt br =
let pl,t = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]"
(print_list comma print_pat) pl print_term t;
Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
let p,t = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
Svs.iter forget_var p.pat_vars
and print_fbranch fmt br =
let pl,f = f_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]"
(print_list comma print_pat) pl print_fmla f;
Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
let p,f = f_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
Svs.iter forget_var p.pat_vars
and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
......@@ -426,6 +437,8 @@ let () = Exn_printer.register
print_ls ls ls_arg app_arg
| Term.DuplicateVar vs ->
fprintf fmt "Variable %a is used twice" print_vsty vs
| Term.UncoveredVar vs ->
fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
| Term.FunctionSymbolExpected ls ->
fprintf fmt "Not a function symbol: %a" print_ls ls
| Term.PredicateSymbolExpected ls ->
......
This diff is collapsed.
......@@ -58,6 +58,7 @@ val create_psymbol : preid -> ty list -> lsymbol
(** {2 Exceptions} *)
exception DuplicateVar of vsymbol
exception UncoveredVar of vsymbol
exception BadArity of lsymbol * int * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
......@@ -66,6 +67,7 @@ exception PredicateSymbolExpected of lsymbol
type pattern = private {
pat_node : pattern_node;
pat_vars : Svs.t;
pat_ty : ty;
pat_tag : int;
}
......@@ -74,6 +76,7 @@ and pattern_node = private
| Pwild
| Pvar of vsymbol
| Papp of lsymbol * pattern list
| Por of pattern * pattern
| Pas of pattern * vsymbol
val pat_equal : pattern -> pattern -> bool
......@@ -83,6 +86,7 @@ val pat_equal : pattern -> pattern -> bool
val pat_wild : ty -> pattern
val pat_var : vsymbol -> pattern
val pat_app : lsymbol -> pattern list -> ty -> pattern
val pat_or : pattern -> pattern -> pattern
val pat_as : pattern -> vsymbol -> pattern
(** generic traversal functions *)
......@@ -92,8 +96,6 @@ val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
val pat_freevars : Svs.t -> pattern -> Svs.t
(** {2 Terms and formulas} *)
type label = string
......@@ -136,7 +138,7 @@ and term_node = private
| Tapp of lsymbol * term list
| Tif of fmla * term * term
| Tlet of term * term_bound
| Tcase of term list * term_branch list
| Tcase of term * term_branch list
| Teps of fmla_bound
and fmla_node = private
......@@ -148,7 +150,7 @@ and fmla_node = private
| Ffalse
| Fif of fmla * fmla * fmla
| Flet of term * fmla_bound
| Fcase of term list * fmla_branch list
| Fcase of term * fmla_branch list
and term_bound
......@@ -187,7 +189,7 @@ val t_real_const : real_constant -> term
val t_app : lsymbol -> term list -> ty -> term
val t_if : fmla -> term -> term -> term
val t_let : vsymbol -> term -> term -> term
val t_case : term list -> (pattern list * term) list -> ty -> term
val t_case : term -> (pattern * term) list -> ty -> term
val t_eps : vsymbol -> fmla -> term
val t_app_infer : lsymbol -> term list -> term
......@@ -213,7 +215,7 @@ val f_true : fmla
val f_false : fmla
val f_if : fmla -> fmla -> fmla -> fmla
val f_let : vsymbol -> term -> fmla -> fmla
val f_case : term list -> (pattern list * fmla) list -> fmla
val f_case : term -> (pattern * fmla) list -> fmla
val f_app_inst : lsymbol -> term list -> ty Mtv.t
......@@ -243,8 +245,8 @@ val f_let_simp : vsymbol -> term -> fmla -> fmla
val t_open_bound : term_bound -> vsymbol * term
val f_open_bound : fmla_bound -> vsymbol * fmla
val t_open_branch : term_branch -> pattern list * term
val f_open_branch : fmla_branch -> pattern list * fmla
val t_open_branch : term_branch -> pattern * term
val f_open_branch : fmla_branch -> pattern * fmla
val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
......
......@@ -116,29 +116,42 @@ let rec ty_of_dty = function
| Tyapp (s, tl) ->
ty_app s (List.map ty_of_dty tl)
type ident = Ptree.ident
type dpattern = { dp_node : dpattern_node; dp_ty : dty }
and dpattern_node =
| Pwild
| Pvar of string
| Pvar of ident
| Papp of lsymbol * dpattern list
| Pas of dpattern * string
let rec pattern env p =
let ty = ty_of_dty p.dp_ty in
match p.dp_node with
| Pwild ->
env, pat_wild ty
| Pvar x ->
let v = create_vsymbol (id_fresh x) ty in
Mstr.add x v env, pat_var v
| Por of dpattern * dpattern
| Pas of dpattern * ident
let rec pattern_env env p = match p.dp_node with
| Pwild -> env
| Papp (_, pl) -> List.fold_left pattern_env env pl
| Por (p, _) -> pattern_env env p
| Pvar { id = x ; id_loc = loc } ->
let ty = ty_of_dty p.dp_ty in
let vs = create_vsymbol (id_user x loc) ty in
Mstr.add x vs env
| Pas (p, { id = x ; id_loc = loc }) ->
let ty = ty_of_dty p.dp_ty in
let vs = create_vsymbol (id_user x loc) ty in
pattern_env (Mstr.add x vs env) p
let get_pat_var env p x = try Mstr.find x env with Not_found ->
raise (Term.UncoveredVar (create_vsymbol (id_fresh x) (ty_of_dty p.dp_ty)))
let rec pattern_pat env p = match p.dp_node with
| Pwild -> pat_wild (ty_of_dty p.dp_ty)
| Pvar x -> pat_var (get_pat_var env p x.id)
| Pas (p, x) -> pat_as (pattern_pat env p) (get_pat_var env p x.id)
| Por (p, q) -> pat_or (pattern_pat env p) (pattern_pat env q)
| Papp (s, pl) ->
let env, pl = map_fold_left pattern env pl in
env, pat_app s pl ty
| Pas (p, x) ->
let v = create_vsymbol (id_fresh x) ty in
let env, p = pattern (Mstr.add x v env) p in
env, pat_as p v
pat_app s (List.map (pattern_pat env) pl) (ty_of_dty p.dp_ty)
let pattern env p = let env = pattern_env env p in env, pattern_pat env p
type dterm = { dt_node : dterm_node; dt_ty : dty }
......@@ -147,21 +160,21 @@ and dterm_node =
| Tconst of constant
| Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm
| Tlet of dterm * string * dterm
| Tmatch of dterm list * (dpattern list * dterm) list
| Tlet of dterm * ident * dterm
| Tmatch of dterm * (dpattern * dterm) list
| Tnamed of string * dterm
| Teps of string * dty * dfmla
| Teps of ident * dty * dfmla
and dfmla =
| Fapp of lsymbol * dterm list
| Fquant of quant * (string * dty) list * dtrigger list list * dfmla
| Fquant of quant * (ident * dty) list * dtrigger list list * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
| Ftrue
| Ffalse
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * string * dfmla
| Fmatch of dterm list * (dpattern list * dfmla) list
| Flet of dterm * ident * dfmla
| Fmatch of dterm * (dpattern * dfmla) list
| Fnamed of string * dfmla
| Fvar of fmla
......@@ -179,27 +192,26 @@ let rec term env t = match t.dt_node with
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| Tif (f, t1, t2) ->
t_if (fmla env f) (term env t1) (term env t2)
| Tlet (e1, x, e2) ->
| Tlet (e1, { id = x ; id_loc = loc }, e2) ->
let ty = ty_of_dty e1.dt_ty in
let e1 = term env e1 in
let v = create_vsymbol (id_fresh x) ty in
let v = create_vsymbol (id_user x loc) ty in
let env = Mstr.add x v env in
let e2 = term env e2 in
t_let v e1 e2
| Tmatch (tl, bl) ->
let branch (pl,e) =
let env, pl = map_fold_left pattern env pl in
(pl, term env e)
| Tmatch (t1, bl) ->
let branch (p,e) =
let env, p = pattern env p in (p, term env e)
in
let bl = List.map branch bl in
let ty = (snd (List.hd bl)).t_ty in
t_case (List.map (term env) tl) bl ty
t_case (term env t1) bl ty
| Tnamed (x, e1) ->
let e1 = term env e1 in
t_label_add x e1
| Teps (x, ty, e1) ->
| Teps ({ id = x ; id_loc = loc }, ty, e1) ->
let ty = ty_of_dty ty in
let v = create_vsymbol (id_fresh x) ty in
let v = create_vsymbol (id_user x loc) ty in
let env = Mstr.add x v env in
let e1 = fmla env e1 in
t_eps v e1
......@@ -216,10 +228,9 @@ and fmla env = function
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, uqu, trl, f1) ->
(* TODO: shouldn't we localize this ident? *)
let uquant env (x,ty) =
let uquant env ({ id = x ; id_loc = loc },ty) =
let ty = ty_of_dty ty in
let v = create_vsymbol (id_fresh x) ty in
let v = create_vsymbol (id_user x loc) ty in
Mstr.add x v env, v
in
let env, vl = map_fold_left uquant env uqu in
......@@ -231,19 +242,18 @@ and fmla env = function
f_quant q vl trl (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, x, f2) ->
| Flet (e1, { id = x ; id_loc = loc }, f2) ->
let ty = ty_of_dty e1.dt_ty in
let e1 = term env e1 in
let v = create_vsymbol (id_fresh x) ty in
let v = create_vsymbol (id_user x loc) ty in
let env = Mstr.add x v env in
let f2 = fmla env f2 in
f_let v e1 f2
| Fmatch (tl, bl) ->
let branch (pl,e) =
let env, pl = map_fold_left pattern env pl in
(pl, fmla env e)
| Fmatch (t, bl) ->
let branch (p,e) =
let env, p = pattern env p in (p, fmla env e)
in
f_case (List.map (term env) tl) (List.map branch bl)
f_case (term env t) (List.map branch bl)
| Fnamed (x, f1) ->
let f1 = fmla env f1 in
f_label_add x f1
......@@ -272,24 +282,33 @@ let specialize_lsymbol ~loc s =
let env = Htv.create 17 in
List.map (specialize_ty ~loc env) tl, option_map (specialize_ty ~loc env) t
let ident_of_vs ~loc vs =
{ id = vs.vs_name.id_string;
id_loc = match vs.vs_name.id_origin with
| User loc -> loc
| _ -> loc }
let rec specialize_pattern ~loc htv p =
{ dp_node = specialize_pattern_node ~loc htv p.pat_node;
dp_ty = specialize_ty ~loc htv p.pat_ty; }
dp_ty = specialize_ty ~loc htv p.pat_ty; }
and specialize_pattern_node ~loc htv = function
| Term.Pwild ->
Pwild
| Term.Pvar v ->
Pvar v.vs_name.id_string
Pvar (ident_of_vs ~loc v)
| Term.Papp (s, pl) ->
Papp (s, List.map (specialize_pattern ~loc htv) pl)
| Term.Pas (p, v) ->
Pas (specialize_pattern ~loc htv p, v.vs_name.id_string)
Pas (specialize_pattern ~loc htv p, ident_of_vs ~loc v)
| Term.Por (p, q) ->
Por (specialize_pattern ~loc htv p, specialize_pattern ~loc htv q)
let rec specialize_term ~loc htv t =
{ dt_node = specialize_term_node ~loc htv t.t_node;
dt_ty = specialize_ty ~loc htv t.t_ty; }
dt_ty = specialize_ty ~loc htv t.t_ty; }
(* TODO: labels are lost *)
and specialize_term_node ~loc htv = function
| Term.Tbvar _ ->
assert false
......@@ -305,16 +324,15 @@ and specialize_term_node ~loc htv = function
| Term.Tlet (t1, t2) ->
let v, t2 = t_open_bound t2 in
Tlet (specialize_term ~loc htv t1,
v.vs_name.id_string, specialize_term ~loc htv t2)
| Term.Tcase (tl, bl) ->
let branch b =
let pl, t = t_open_branch b in
List.map (specialize_pattern ~loc htv) pl, specialize_term ~loc htv t
ident_of_vs ~loc v, specialize_term ~loc htv t2)
| Term.Tcase (t1, bl) ->
let branch b = let p, t = t_open_branch b in
specialize_pattern ~loc htv p, specialize_term ~loc htv t
in
Tmatch (List.map (specialize_term ~loc htv) tl, List.map branch bl)
Tmatch (specialize_term ~loc htv t1, List.map branch bl)
| Term.Teps fb ->
let v, f = f_open_bound fb in
Teps (v.vs_name.id_string, specialize_ty ~loc htv v.vs_ty,
Teps (ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty,
specialize_fmla ~loc htv f)
(* TODO: labels are lost *)
......@@ -323,7 +341,7 @@ and specialize_fmla ~loc htv f = match f.f_node with
Fapp (ls, List.map (specialize_term ~loc htv) tl)
| Term.Fquant (q, fq) ->
let vl, tl, f = f_open_quant fq in
let uquant v = v.vs_name.id_string, specialize_ty ~loc htv v.vs_ty in
let uquant v = ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty in
let tl = List.map (List.map (specialize_trigger ~loc htv)) tl in
Fquant (q, List.map uquant vl, tl, specialize_fmla ~loc htv f)
| Term.Fbinop (b, f1, f2) ->
......@@ -340,13 +358,12 @@ and specialize_fmla ~loc htv f = match f.f_node with
| Term.Flet (t1, f2b) ->
let v, f2 = f_open_bound f2b in
Flet (specialize_term ~loc htv t1,
v.vs_name.id_string, specialize_fmla ~loc htv f2)
| Term.Fcase (tl, fbl) ->
let branch b =
let pl, f = f_open_branch b in
List.map (specialize_pattern ~loc htv) pl, specialize_fmla ~loc htv f
in
Fmatch (List.map (specialize_term ~loc htv) tl, List.map branch fbl)
ident_of_vs ~loc v, specialize_fmla ~loc htv f2)
| Term.Fcase (t, fbl) ->
let branch b = let p, f = f_open_branch b in
specialize_pattern ~loc htv p, specialize_fmla ~loc htv f
in
Fmatch (specialize_term ~loc htv t, List.map branch fbl)
and specialize_trigger ~loc htv = function
| Term.Term t -> TRterm (specialize_term ~loc htv t)
......
......@@ -38,13 +38,16 @@ val print_dty : Format.formatter -> dty -> unit
val ty_of_dty : dty -> ty
type ident = Ptree.ident
type dpattern = { dp_node : dpattern_node; dp_ty : dty }
and dpattern_node =
| Pwild
| Pvar of string
| Pvar of ident
| Papp of lsymbol * dpattern list
| Pas of dpattern * string
| Por of dpattern * dpattern
| Pas of dpattern * ident
val pattern : vsymbol Mstr.t -> dpattern -> vsymbol Mstr.t * pattern
......@@ -55,21 +58,21 @@ and dterm_node =
| Tconst of constant
| Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm
| Tlet of dterm * string * dterm
| Tmatch of dterm list * (dpattern list * dterm) list
| Tlet of dterm * ident * dterm
| Tmatch of dterm * (dpattern * dterm) list
| Tnamed of string * dterm
| Teps of string * dty * dfmla