Commit 8833aaad authored by Andrei Paskevich's avatar Andrei Paskevich

eliminate definitions of algebraic types

(unusable so far, must eliminate match statements, too)
parent cdae5e39
......@@ -213,7 +213,7 @@ let create_ty_decl tdl =
let check_constr ty acc fs =
if not fs.ls_constr then raise (ConstructorExpected fs);
let vty = of_option fs.ls_value in
ignore (Ty.matching Mtv.empty vty ty);
ignore (ty_match Mtv.empty vty ty);
let add s ty = match ty.ty_node with
| Tyvar v -> Stv.add v s
| _ -> assert false
......@@ -280,11 +280,11 @@ let create_ind_decl idl =
let cls, f = clause [] (check_fvs f) in
match f.f_node with
| Fapp (s, tl) when s == ps ->
let tymatch sb t ty =
try Ty.matching sb (t.t_ty) ty with TypeMismatch ->
let mtch sb t ty =
try ty_match sb (t.t_ty) ty with TypeMismatch ->
raise (TooSpecificIndDecl (ps, pr, t))
in
ignore (List.fold_left2 tymatch Mtv.empty tl ps.ls_args);
ignore (List.fold_left2 mtch Mtv.empty tl ps.ls_args);
(try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
with Found ls ->
raise (NonPositiveIndDecl (ps, pr, ls)));
......
......@@ -165,10 +165,10 @@ exception PredicateSymbolExpected of lsymbol
let pat_app fs pl ty =
if not fs.ls_constr then raise (ConstructorExpected fs);
let s = match fs.ls_value with
| Some vty -> Ty.matching Mtv.empty vty ty
| Some vty -> ty_match Mtv.empty vty ty
| None -> raise (FunctionSymbolExpected fs)
in
let mtch s ty p = Ty.matching s ty p.pat_ty in
let mtch s ty p = ty_match s ty p.pat_ty in
ignore (try List.fold_left2 mtch s fs.ls_args pl
with Invalid_argument _ -> raise BadArity);
pat_app fs pl ty
......@@ -567,20 +567,32 @@ let f_any_unsafe prT prF lvl f =
let t_app fs tl ty =
let s = match fs.ls_value with
| Some vty -> Ty.matching Mtv.empty vty ty
| Some vty -> ty_match Mtv.empty vty ty
| _ -> raise (FunctionSymbolExpected fs)
in
let mtch s ty t = Ty.matching s ty t.t_ty in
let mtch s ty t = ty_match s ty t.t_ty in
ignore (try List.fold_left2 mtch s fs.ls_args tl
with Invalid_argument _ -> raise BadArity);
t_app fs tl ty
let t_app_infer fs tl =
let mtch s ty t = ty_match s ty t.t_ty in
let s =
try List.fold_left2 mtch Mtv.empty fs.ls_args tl
with Invalid_argument _ -> raise BadArity
in
let ty = match fs.ls_value with
| Some ty -> ty_inst s ty
| _ -> raise (FunctionSymbolExpected fs)
in
t_app_unsafe fs tl ty
let f_app ps tl =
let s = match ps.ls_value with
| None -> Mtv.empty
| _ -> raise (PredicateSymbolExpected ps)
in
let mtch s ty t = Ty.matching s ty t.t_ty in
let mtch s ty t = ty_match s ty t.t_ty in
ignore (try List.fold_left2 mtch s ps.ls_args tl
with Invalid_argument _ -> raise BadArity);
f_app ps tl
......@@ -1163,9 +1175,6 @@ and f_match_quant s qf1 qf2 =
if list_all2 cmp vl1 vl2
then f_match s f1 f2 else raise NoMatch
let t_match t1 t2 s = try Some (t_match s t1 t2) with NoMatch -> None
let f_match f1 f2 s = try Some (f_match s f1 f2) with NoMatch -> None
(* occurrence check *)
let rec t_occurs_term r lvl t = r == t ||
......
......@@ -173,6 +173,8 @@ val t_let : vsymbol -> term -> term -> term
val t_case : term list -> (pattern list * term) list -> ty -> term
val t_eps : vsymbol -> fmla -> term
val t_app_infer : lsymbol -> term list -> term
val t_label : label list -> term -> term
val t_label_add : label -> term -> term
val t_label_copy : term -> term -> term
......@@ -342,6 +344,8 @@ val f_subst_fmla_alpha : fmla -> fmla -> fmla -> fmla
(* term/fmla matching modulo alpha in the pattern *)
val t_match : term -> term -> term Mvs.t -> term Mvs.t option
val f_match : fmla -> fmla -> term Mvs.t -> term Mvs.t option
exception NoMatch
val t_match : term Mvs.t -> term -> term -> term Mvs.t
val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t
......@@ -364,16 +364,16 @@ let cl_init_ts cl ts ts' =
let cl_init_ls cl ls ls' =
let id = ls.ls_name in
if not (Sid.mem id cl.id_local) then raise (NonLocal id);
let tymatch sb ty ty' =
try Ty.matching sb ty' (cl_trans_ty cl ty)
let mtch sb ty ty' =
try ty_match sb ty' (cl_trans_ty cl ty)
with TypeMismatch -> raise (BadInstance (id, ls'.ls_name))
in
let sb = match ls.ls_value,ls'.ls_value with
| Some ty, Some ty' -> tymatch Mtv.empty ty ty'
| Some ty, Some ty' -> mtch Mtv.empty ty ty'
| None, None -> Mtv.empty
| _ -> raise (BadInstance (id, ls'.ls_name))
in
ignore (try List.fold_left2 tymatch sb ls.ls_args ls'.ls_args
ignore (try List.fold_left2 mtch sb ls.ls_args ls'.ls_args
with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name)));
cl_add_ls cl ls ls'
......
......@@ -173,19 +173,20 @@ let ty_s_any pr ty =
exception TypeMismatch
let rec matching s ty1 ty2 =
let rec ty_match s ty1 ty2 =
if ty1 == ty2 then s
else match ty1.ty_node, ty2.ty_node with
| Tyvar n1, _ ->
(try if Mtv.find n1 s == ty2 then s else raise TypeMismatch
with Not_found -> Mtv.add n1 ty2 s)
| Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
List.fold_left2 matching s l1 l2
List.fold_left2 ty_match s l1 l2
| _ ->
raise TypeMismatch
let ty_match ty1 ty2 s =
try Some (matching s ty1 ty2) with TypeMismatch -> None
let rec ty_inst s ty = match ty.ty_node with
| Tyvar n -> (try Mtv.find n s with Not_found -> ty)
| _ -> ty_map (ty_inst s) ty
(* built-in symbols *)
......
......@@ -77,8 +77,8 @@ val ty_s_any : (tysymbol -> bool) -> ty -> bool
exception TypeMismatch
val matching : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ty_match : ty -> ty -> ty Mtv.t -> ty Mtv.t option
val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ty_inst : ty Mtv.t -> ty -> ty
(* built-in symbols *)
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Util
open Ident
open Ty
open Term
open Decl
open Task
type state = {
cs_map : lsymbol Mls.t; (* from constructors to abstract functions *)
mt_map : lsymbol Mts.t; (* from type symbols to selector functions *)
pj_map : lsymbol list Mls.t; (* from constructors to projections *)
}
let empty_state = {
cs_map = Mls.empty;
mt_map = Mts.empty;
pj_map = Mls.empty;
}
let rec rewriteT state t = match t.t_node with
| Tcase (tl,bl) -> assert false
(*
let mk_b (pl,_,t) = (pl,t) in
let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
Pattern.CompileTerm.compile (find_constructors state) tl bl
*)
| _ -> t_map (rewriteT state) (rewriteF state) t
and rewriteF state f = match f.f_node with
| Fcase (tl,bl) -> assert false
(*
let mk_b (pl,_,f) = (pl,f) in
let bl = List.map (fun b -> mk_b (f_open_branch b)) bl in
Pattern.CompileFmla.compile (find_constructors state) tl bl
*)
| _ -> f_map (rewriteT state) (rewriteF state) f
let add_type (state, task) ts csl =
(* declare constructors as abstract functions *)
let cs_add (m,tsk) cs =
let id = id_clone cs.ls_name in
let fs = create_fsymbol id cs.ls_args (of_option cs.ls_value) in
Mls.add cs fs m, add_decl tsk (create_logic_decl [fs, None])
in
let csmap, task = List.fold_left cs_add (state.cs_map, task) csl in
(* declare the selector function *)
let mt_id = id_derive ("match_" ^ ts.ts_name.id_long) ts.ts_name in
let mt_hd = ty_app ts (List.map ty_var ts.ts_args) in
let mt_ty = ty_var (create_tvsymbol (id_fresh "a")) in
let mt_al = mt_hd :: List.rev_map (fun _ -> mt_ty) csl in
let mt_ls = create_fsymbol mt_id mt_al mt_ty in
let mtmap = Mts.add ts mt_ls state.mt_map in
let task = add_decl task (create_logic_decl [mt_ls, None]) in
(* define the selector function *)
let mt_vs _ = create_vsymbol (id_fresh "z") mt_ty in
let mt_vl = List.rev_map mt_vs csl in
let mt_tl = List.rev_map t_var mt_vl in
let mt_add tsk cs t =
let fs = Mls.find cs csmap in
let id = mt_ls.ls_name.id_long ^ "_" ^ cs.ls_name.id_long in
let pr = create_prsymbol (id_derive id cs.ls_name) in
let vl = List.rev_map (create_vsymbol (id_fresh "u")) fs.ls_args in
let hd = t_app fs (List.rev_map t_var vl) (of_option fs.ls_value) in
let hd = t_app mt_ls (hd::mt_tl) mt_ty in
let vl = List.rev_append mt_vl (List.rev vl) in
let ax = f_forall vl [[Term hd]] (f_equ hd t) in
add_decl tsk (create_prop_decl Paxiom pr ax)
in
let task = List.fold_left2 mt_add task csl mt_tl in
(* declare and define the projection functions *)
let pj_add (m,tsk) cs =
let fs = Mls.find cs csmap in
let id = cs.ls_name.id_long ^ "_proj_" in
let vl = List.rev_map (create_vsymbol (id_fresh "u")) fs.ls_args in
let tl = List.rev_map t_var vl in
let hd = t_app fs tl (of_option fs.ls_value) in
let c = ref 0 in
let add (pjl,tsk) t =
let id = id_derive (id ^ (incr c; string_of_int !c)) cs.ls_name in
let ls = create_fsymbol id [of_option fs.ls_value] t.t_ty in
let tsk = add_decl tsk (create_logic_decl [ls, None]) in
let id = id_derive (ls.ls_name.id_long ^ "_def") ls.ls_name in
let pr = create_prsymbol id in
let hh = t_app ls [hd] t.t_ty in
let ax = f_forall (List.rev vl) [[Term hd]] (f_equ hh t) in
ls::pjl, add_decl tsk (create_prop_decl Paxiom pr ax)
in
let pjl,tsk = List.fold_left add ([],tsk) tl in
Mls.add cs pjl m, tsk
in
let pjmap, task = List.fold_left pj_add (state.pj_map, task) csl in
(* add the inversion axiom *)
let ax_id = ts.ts_name.id_long ^ "_inversion" in
let ax_pr = create_prsymbol (id_derive ax_id ts.ts_name) in
let ax_vs = create_vsymbol (id_fresh "u") mt_hd in
let ax_hd = t_var ax_vs in
let mk_cs cs =
let fs = Mls.find cs csmap in
let pjl = Mls.find cs pjmap in
let app pj = t_app_infer pj [ax_hd] in
f_equ ax_hd (t_app fs (List.rev_map app pjl) mt_hd)
in
let ax_f = f_forall [ax_vs] [] (map_join_left mk_cs f_or csl) in
let task = add_decl task (create_prop_decl Paxiom ax_pr ax_f) in
(* return the updated state and task *)
{ cs_map = csmap; mt_map = mtmap; pj_map = pjmap }, task
let comp t (state,task) = match t.task_decl.d_node with
| Dtype dl ->
(* add abstract type declarations *)
let tydl = List.rev_map (fun (ts,_) -> (ts,Tabstract)) dl in
let task = add_decl task (create_ty_decl tydl) in
(* add needed functions and axioms *)
let add acc (ts,df) = match df with
| Tabstract -> acc
| Talgebraic csl -> add_type acc ts csl
in
List.fold_left add (state,task) dl
| d ->
let fnT = rewriteT state in
let fnF = rewriteF state in
state, add_decl task (decl_map fnT fnF t.task_decl)
let comp = Register.store (fun () -> Trans.fold_map comp empty_state None)
let () = Driver.register_transform "eliminate_algebraic" comp
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