Commit c35b73a0 authored by Andrei Paskevich's avatar Andrei Paskevich

explicit mutual dependence in Why declarations

parent d2a26201
theory Test
type t = u
type u = t
with u = t
end
theory TreeForest
type list 'a = Nil | Cons 'a (list 'a)
type tree 'a = Leaf 'a | Node (forest 'a)
type forest 'a = list (tree 'a)
with forest 'a = list (tree 'a)
end
......@@ -2,9 +2,9 @@ theory Test
type t1 = t2
type t5
with t5
type t2 = t5
with t2 = t5
logic f (x : t1) (y : t2) : t5
......
......@@ -320,81 +320,6 @@ let create_prop_decl k p f =
let news = news_id Sid.empty p.pr_name in
mk_decl (Dprop (k,p,check_fvs f)) syms news
(** Split declarations *)
let build_dls get_id get_dep dl =
let add_id acc d = Sid.add (get_id d) acc in
let s = List.fold_left add_id Sid.empty dl in
let add_dl (next,loan,dls,dl) d =
let dl = d :: dl in
let id = get_id d in
let next = Sid.remove id next in
let loan = Sid.remove id loan in
let loan = get_dep next loan d in
if Sid.is_empty loan
then next, loan, List.rev dl :: dls, []
else next, loan, dls, dl
in
let init = (s, Sid.empty, [], []) in
let next,loan,dls,dl = List.fold_left add_dl init dl in
assert (Sid.is_empty next);
assert (Sid.is_empty loan);
assert (dl = []);
dls
let get_ty_id (ts,_) = ts.ts_name
let get_ty_dep next loan (ts,td) =
let dep acc ts = if Sid.mem ts.ts_name next
then Sid.add ts.ts_name acc else acc in
let loan = match ts.ts_def with
| Some ty -> ty_s_fold dep loan ty
| None -> loan
in
let cns acc ls =
List.fold_left (ty_s_fold dep) acc ls.ls_args in
match td with
| Tabstract -> loan
| Talgebraic fdl -> List.fold_left cns loan fdl
let get_logic_id (ls,_) = ls.ls_name
let get_logic_dep next loan (_,ld) =
let dts acc _ = acc in
let dep acc ls = if Sid.mem ls.ls_name next
then Sid.add ls.ls_name acc else acc in
match ld with
| Some (_,f) -> f_s_fold dts dep loan f
| None -> loan
let get_ind_id (ps,_) = ps.ls_name
let get_ind_dep next loan (_,al) =
let dts acc _ = acc in
let dep acc ls = if Sid.mem ls.ls_name next
then Sid.add ls.ls_name acc else acc in
let prp acc (_,f) = f_s_fold dts dep acc f in
List.fold_left prp loan al
let create_ty_decls tdl =
let build = build_dls get_ty_id get_ty_dep in
match tdl with
| [_] -> [create_ty_decl tdl]
| _ -> List.rev_map create_ty_decl (build tdl)
let create_logic_decls ldl =
let build = build_dls get_logic_id get_logic_dep in
match ldl with
| [_] -> [create_logic_decl ldl]
| _ -> List.rev_map create_logic_decl (build ldl)
let create_ind_decls idl =
let build = build_dls get_ind_id get_ind_dep in
match idl with
| [_] -> [create_ind_decl idl]
| _ -> List.rev_map create_ind_decl (build idl)
(** Utilities *)
let decl_map fnT fnF d = match d.d_node with
......
......@@ -105,12 +105,6 @@ val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
val create_prop_decl : prop_kind -> prsymbol -> fmla -> decl
(* separate independent groups of declarations *)
val create_ty_decls : ty_decl list -> decl list
val create_logic_decls : logic_decl list -> decl list
val create_ind_decls : ind_decl list -> decl list
(* exceptions *)
exception IllegalTypeAlias of tysymbol
......
......@@ -163,10 +163,6 @@ let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)
let add_ty_decls tk dl = List.fold_left add_decl tk (create_ty_decls dl)
let add_logic_decls tk dl = List.fold_left add_decl tk (create_logic_decls dl)
let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)
(* task constructors *)
let rec add_tdecl task td = match td.td_node with
......
......@@ -79,10 +79,6 @@ val add_logic_decl : task -> logic_decl list -> task
val add_ind_decl : task -> ind_decl list -> task
val add_prop_decl : task -> prop_kind -> prsymbol -> fmla -> task
val add_ty_decls : task -> ty_decl list -> task
val add_logic_decls : task -> logic_decl list -> task
val add_ind_decls : task -> ind_decl list -> task
(** {2 utilities} *)
val split_theory : theory -> Spr.t option -> task -> task list
......
......@@ -360,10 +360,6 @@ let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
let add_ind_decl uc dl = add_decl uc (create_ind_decl dl)
let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
let add_ty_decls uc dl = List.fold_left add_decl uc (create_ty_decls dl)
let add_logic_decls uc dl = List.fold_left add_decl uc (create_logic_decls dl)
let add_ind_decls uc dl = List.fold_left add_decl uc (create_ind_decls dl)
(** Use *)
let create_use th = mk_tdecl (Use th)
......
......@@ -127,10 +127,6 @@ val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
val add_ind_decl : theory_uc -> ind_decl list -> theory_uc
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> fmla -> theory_uc
val add_ty_decls : theory_uc -> ty_decl list -> theory_uc
val add_logic_decls : theory_uc -> logic_decl list -> theory_uc
val add_ind_decls : theory_uc -> ind_decl list -> theory_uc
(** Use *)
val create_use : theory -> tdecl
......
......@@ -81,9 +81,6 @@
/* Precedences */
%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE
%nonassoc DOT ELSE IN
%nonassoc prec_named
%nonassoc COLON
......@@ -132,12 +129,12 @@ list0_decl:
;
decl:
| list1_type_decl
{ TypeDecl $1 }
| list1_logic_decl
{ LogicDecl $1 }
| list1_inductive_decl
{ IndDecl $1 }
| TYPE list1_type_decl
{ TypeDecl $2 }
| LOGIC list1_logic_decl
{ LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
{ IndDecl $2 }
| AXIOM uident COLON lexpr
{ PropDecl (loc (), Kaxiom, $2, $4) }
| LEMMA uident COLON lexpr
......@@ -214,13 +211,13 @@ meta_arg:
/* Type declarations */
list1_type_decl:
| type_decl %prec prec_decls { [$1] }
| type_decl list1_type_decl { $1 :: $2 }
| type_decl { [$1] }
| type_decl WITH list1_type_decl { $1 :: $3 }
;
type_decl:
| TYPE lident type_args typedefn
{ { td_loc = loc (); td_ident = $2; td_params = $3; td_def = $4 } }
| lident type_args typedefn
{ { td_loc = loc (); td_ident = $1; td_params = $2; td_def = $3 } }
;
type_args:
......@@ -247,14 +244,14 @@ typecase:
/* Logic declarations */
list1_logic_decl:
| logic_decl %prec prec_decls { [$1] }
| logic_decl list1_logic_decl { $1 :: $2 }
| logic_decl { [$1] }
| logic_decl WITH list1_logic_decl { $1 :: $3 }
;
logic_decl:
| LOGIC lident_rich params logic_type_option logic_def_option
{ { ld_loc = loc (); ld_ident = $2; ld_params = $3;
ld_type = $4; ld_def = $5; } }
| lident_rich params logic_type_option logic_def_option
{ { ld_loc = loc (); ld_ident = $1; ld_params = $2;
ld_type = $3; ld_def = $4; } }
;
logic_type_option:
......@@ -270,13 +267,13 @@ logic_def_option:
/* Inductive declarations */
list1_inductive_decl:
| inductive_decl %prec prec_decls { [$1] }
| inductive_decl list1_inductive_decl { $1 :: $2 }
| inductive_decl { [$1] }
| inductive_decl WITH list1_inductive_decl { $1 :: $3 }
;
inductive_decl:
| INDUCTIVE lident_rich params inddefn
{ { in_loc = loc (); in_ident = $2; in_params = $3; in_def = $4 } }
| lident_rich params inddefn
{ { in_loc = loc (); in_ident = $1; in_params = $2; in_def = $3 } }
;
inddefn:
......
......@@ -202,13 +202,13 @@ let with_tuples ?(reset=false) f uc x =
uc
let add_ty_decl = with_tuples add_ty_decl
let add_ty_decls = with_tuples ~reset:true add_ty_decls
let add_ty_decls = with_tuples ~reset:true add_ty_decl
let add_logic_decl = with_tuples add_logic_decl
let add_logic_decls = with_tuples ~reset:true add_logic_decls
let add_logic_decls = with_tuples ~reset:true add_logic_decl
let add_ind_decl = with_tuples add_ind_decl
let add_ind_decls = with_tuples ~reset:true add_ind_decls
let add_ind_decls = with_tuples ~reset:true add_ind_decl
let add_prop_decl = with_tuples ~reset:true add_prop_decl
......
......@@ -34,10 +34,12 @@ let add_id q (ld,id) = function
let elim q d = match d.d_node with
| Dlogic l ->
create_logic_decls (List.map (add_ld q) l)
[create_logic_decl (List.map (add_ld q) l)]
| Dind l ->
let ld, id = List.fold_left (add_id q) ([],[]) l in
create_logic_decls (List.rev ld) @ create_ind_decls (List.rev id)
let ld = if ld = [] then [] else [create_logic_decl (List.rev ld)] in
let id = if id = [] then [] else [create_ind_decl (List.rev id)] in
ld @ id
| _ -> [d]
let eliminate_builtin = Trans.on_meta Printer.meta_remove_logic (fun tds ->
......
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