Commit 1b769a78 authored by Andrei Paskevich's avatar Andrei Paskevich

separate abstract types and logic symbols

- put abstract types and aliases in Dtype of tysymbol
- put (recursive) algebraic types in Ddata of (ts,constr list) list
- put abstract function/predicate symbols in Dparam of lsymbol
- put defined logic symbols in Dlogic of (ls,ls_definition) list
parent cd2443ec
......@@ -9,7 +9,7 @@ transformation "eliminate_builtin"
(* PVS does not support mutual recursion *)
transformation "eliminate_mutual_recursion"
transformation "simplify_recursive_definition"
(*transformation "simplify_recursive_definition"*)
(* though we could do better, we only use recursion on one argument *)
transformation "eliminate_non_struct_recursion"
......
......@@ -57,8 +57,8 @@ let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None]
let task2 = Task.add_logic_decl task2 [prop_var_B, None]
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
......
......@@ -110,19 +110,13 @@ and print_fmla info fmt f = match f.t_node with
"tptp : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
let print_logic_decl _ _ (_,ld) = match ld with
| None -> ()
| Some _ -> unsupported "Predicate and function definition aren't supported"
let print_logic_decl info fmt d =
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
| Dtype _ -> false
| Dtype _ | Dparam _ -> false
(* print_list_opt newline (print_type_decl info) fmt dl *)
| Dlogic dl ->
print_list_opt newline (print_logic_decl info) fmt dl
| Ddata _ -> unsupportedDecl d
"Algebraic datatypes are not supported"
| Dlogic _ -> unsupportedDecl d
"Predicate and function definition aren't supported"
| Dind _ -> unsupportedDecl d
"tptp : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
......
......@@ -584,16 +584,16 @@ let flush_impl ~strict env uc impl =
in
let update s e (env,uc) = match e with
| SType ts ->
Mstr.add s e env, add_ty_decl uc [ts,Tabstract]
Mstr.add s e env, add_ty_decl uc ts
| SFunc (_,_,_,ls) | SPred (_,_,_,ls) ->
Mstr.add s e env, add_logic_decl uc [ls,None]
Mstr.add s e env, add_param_decl uc ls
| STVar tv when strict ->
errorm ?loc:tv.tv_name.id_loc "Unbound type variable %s" s
| SVar vs when strict ->
errorm ?loc:vs.vs_name.id_loc "Unbound variable %s" s
| STVar _ | SVar _ -> env,uc
| Sdobj ls ->
let uc = add_logic_decl uc [ls,None] in
let uc = add_param_decl uc ls in
let t = t_app ls [] ls.ls_value in
let add _ s f = match s with
| Sdobj fs -> t_and_simp f (t_neq (t_app fs [] fs.ls_value) t)
......
......@@ -549,7 +549,7 @@ module Select = struct
This is the function directly used to filter axioms. *)
let filter fTbl tTbl symTbl goal_clauses (gc,gp) decl =
match decl.d_node with
| Dtype _ | Dlogic _ | Dind _ -> [decl]
| Dtype _ | Ddata _ | Dparam _ | Dlogic _ | Dind _ -> [decl]
| Dprop (Paxiom,_,fmla) -> (* filter only axioms *)
Format.eprintf "filter : @[%a@]@." Pretty.print_term fmla;
let goal_exprs = goal_clauses in
......
......@@ -419,7 +419,7 @@ and tr_global_ts dep env r =
| None ->
Ty.create_tysymbol id vars None
in
let decl = Decl.create_ty_decl [ts, Decl.Tabstract] in
let decl = Decl.create_ty_decl ts in
add_dep dep decl;
add_table global_ts r (Some ts);
global_decl := Ident.Mid.add ts.ts_name decl !global_decl;
......@@ -466,11 +466,11 @@ and tr_global_ts dep env r =
ls, List.map (fun _ -> None) ls.ls_args
in
let ls = Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc) in
ts, Decl.Talgebraic ls
ts, ls
in
let decl = Array.mapi make_one mib.mind_packets in
let decl = Array.to_list decl in
let decl = Decl.create_ty_decl decl in
let decl = Decl.create_data_decl decl in
(* Format.printf "decl = %a@." Pretty.print_decl decl; *)
add_dep dep decl;
List.iter
......@@ -512,19 +512,18 @@ and tr_global_ls dep env r =
ignore (tr_type dep' tvm env t);
lookup_table global_ls r
| ConstRef c ->
let ld = decompose_definition dep' env c in
let decl = decompose_definition dep' env c in
(* let ld = match defl with *)
(* | [] -> *)
(* [make_def_decl dep env r None] *)
(* | _ -> *)
(* List.map (fun (r, t) -> make_def_decl dep env r (Some t)) defl *)
(* in *)
let decl = Decl.create_logic_decl ld in
add_dep dep decl;
List.iter
(fun (ls, _) ->
global_decl := Ident.Mid.add ls.ls_name decl !global_decl)
ld;
Ident.Sid.iter
(fun id ->
global_decl := Ident.Mid.add id decl !global_decl)
decl.Decl.d_news;
global_dep := Decl.Mdecl.add decl !dep' !global_dep;
lookup_table global_ls r
| VarRef _ | IndRef _ ->
......@@ -586,7 +585,7 @@ and decompose_definition dep env c =
let ls = lookup_table global_ls r in
match b with
| None ->
ls, None
assert false
| Some b ->
let tvs = List.fold_left Ty.ty_freevars Stv.empty
(Ty.oty_cons ls.ls_args ls.ls_value) in
......@@ -609,7 +608,11 @@ and decompose_definition dep env c =
Decl.make_ls_defn ls vsl b
end
in
List.map make_one_decl dl
match dl with
| [r,None] ->
Decl.create_param_decl (lookup_table global_ls r)
| _ ->
Decl.create_logic_decl (List.map make_one_decl dl)
(***
(* is it defined? *)
......
This diff is collapsed.
......@@ -30,17 +30,13 @@ open Term
type constructor = lsymbol * lsymbol option list
(** constructor symbol with the list of projections *)
type ty_defn =
| Tabstract
| Talgebraic of constructor list
type ty_decl = tysymbol * ty_defn
type data_decl = tysymbol * constructor list
(** {2 Logic symbols declaration} *)
type ls_defn
type logic_decl = lsymbol * ls_defn option
type logic_decl = lsymbol * ls_defn
val make_ls_defn : lsymbol -> vsymbol list -> term -> logic_decl
......@@ -102,8 +98,10 @@ type decl = private {
}
and decl_node =
| Dtype of ty_decl list (* recursive types *)
| Dlogic of logic_decl list (* recursive functions/predicates *)
| Dtype of tysymbol (* abstract types and aliases *)
| Ddata of data_decl list (* recursive algebraic types *)
| Dparam of lsymbol (* abstract functions and predicates *)
| Dlogic of logic_decl list (* recursive functions and predicates *)
| Dind of ind_decl list (* inductive predicates *)
| Dprop of prop_decl (* axiom / lemma / goal *)
......@@ -116,7 +114,9 @@ val d_hash : decl -> int
(** {2 Declaration constructors} *)
val create_ty_decl : ty_decl list -> decl
val create_ty_decl : tysymbol -> decl
val create_data_decl : data_decl list -> decl
val create_param_decl : lsymbol -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
val create_prop_decl : prop_kind -> prsymbol -> term -> decl
......@@ -175,7 +175,6 @@ exception RedeclaredIdent of ident
exception NonExhaustiveCase of pattern list * term
exception NonFoundedTypeDecl of tysymbol
val find_type_definition : known_map -> tysymbol -> ty_defn
val find_constructors : known_map -> tysymbol -> constructor list
val find_inductive_cases : known_map -> lsymbol -> (prsymbol * term) list
val find_logic_definition : known_map -> lsymbol -> ls_defn option
......
......@@ -307,28 +307,24 @@ let print_constr fmt (cs,pjl) =
(print_list nothing print_pj)
(List.fold_right2 add_pj pjl cs.ls_args [])
let print_type_decl fst fmt (ts,def) = match def with
| Tabstract -> begin match ts.ts_def with
| None ->
fprintf fmt "@[<hov 2>%s %a%a%a@]"
(if fst then "type" else "with") print_ts ts
print_ident_labels ts.ts_name
(print_list nothing print_tv_arg) ts.ts_args
| Some ty ->
fprintf fmt "@[<hov 2>%s %a%a%a =@ %a@]"
(if fst then "type" else "with") print_ts ts
print_ident_labels ts.ts_name
(print_list nothing print_tv_arg) ts.ts_args print_ty ty
end
| Talgebraic csl ->
fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]"
(if fst then "type" else "with") print_ts ts
print_ident_labels ts.ts_name
(print_list nothing print_tv_arg) ts.ts_args
(print_list newline print_constr) csl
let print_type_decl first fmt d =
print_type_decl first fmt d; forget_tvs ()
let print_ty_decl fmt ts =
let print_def fmt = function
| None -> ()
| Some ty -> fprintf fmt " =@ %a" print_ty ty
in
fprintf fmt "@[<hov 2>type %a%a%a%a@]"
print_ts ts print_ident_labels ts.ts_name
(print_list nothing print_tv_arg) ts.ts_args
print_def ts.ts_def;
forget_tvs ()
let print_data_decl fst fmt (ts,csl) =
fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]"
(if fst then "type" else "with") print_ts ts
print_ident_labels ts.ts_name
(print_list nothing print_tv_arg) ts.ts_args
(print_list newline print_constr) csl;
forget_tvs ()
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
......@@ -336,24 +332,23 @@ let ls_kind ls =
if ls.ls_value = None then "predicate"
else if ls.ls_args = [] then "constant" else "function"
let print_logic_decl fst fmt (ls,ld) = match ld with
| Some ld ->
let vl,e = open_ls_defn ld in
fprintf fmt "@[<hov 2>%s %a%a%a%a =@ %a@]"
(if fst then ls_kind ls else "with") print_ls ls
print_ident_labels ls.ls_name
(print_list nothing print_vs_arg) vl
(print_option print_ls_type) ls.ls_value print_term e;
List.iter forget_var vl
| None ->
fprintf fmt "@[<hov 2>%s %a%a%a%a@]"
(if fst then ls_kind ls else "with") print_ls ls
print_ident_labels ls.ls_name
(print_list nothing print_ty_arg) ls.ls_args
(print_option print_ls_type) ls.ls_value
let print_param_decl fmt ls =
fprintf fmt "@[<hov 2>%s %a%a%a%a@]"
(ls_kind ls) print_ls ls
print_ident_labels ls.ls_name
(print_list nothing print_ty_arg) ls.ls_args
(print_option print_ls_type) ls.ls_value;
forget_tvs ()
let print_logic_decl first fmt d =
print_logic_decl first fmt d; forget_tvs ()
let print_logic_decl fst fmt (ls,ld) =
let vl,e = open_ls_defn ld in
fprintf fmt "@[<hov 2>%s %a%a%a%a =@ %a@]"
(if fst then ls_kind ls else "with") print_ls ls
print_ident_labels ls.ls_name
(print_list nothing print_vs_arg) vl
(print_option print_ls_type) ls.ls_value print_term e;
List.iter forget_var vl;
forget_tvs ()
let print_ind fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
......@@ -364,10 +359,8 @@ let print_ind_decl fst fmt (ps,bl) =
(if fst then "inductive" else "with") print_ls ps
print_ident_labels ps.ls_name
(print_list nothing print_ty_arg) ps.ls_args
(print_list newline print_ind) bl
let print_ind_decl first fmt d =
print_ind_decl first fmt d; forget_tvs ()
(print_list newline print_ind) bl;
forget_tvs ()
let sprint_pkind = function
| Paxiom -> "axiom"
......@@ -389,13 +382,15 @@ let print_list_next sep print fmt = function
print_list sep (print false) fmt r
let print_decl fmt d = match d.d_node with
| Dtype tl -> print_list_next newline print_type_decl fmt tl
| Dtype ts -> print_ty_decl fmt ts
| Ddata tl -> print_list_next newline print_data_decl fmt tl
| Dparam ls -> print_param_decl fmt ls
| Dlogic ll -> print_list_next newline print_logic_decl fmt ll
| Dind il -> print_list_next newline print_ind_decl fmt il
| Dprop p -> print_prop_decl fmt p
let print_next_type_decl = print_type_decl false
let print_type_decl = print_type_decl true
let print_next_data_decl = print_data_decl false
let print_data_decl = print_data_decl true
let print_next_logic_decl = print_logic_decl false
let print_logic_decl = print_logic_decl true
let print_next_ind_decl = print_ind_decl false
......
......@@ -53,10 +53,12 @@ val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg -> unit
val print_meta_arg_type : formatter -> meta_arg_type -> unit
val print_type_decl : formatter -> ty_decl -> unit
val print_ty_decl : formatter -> tysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
val print_param_decl : formatter -> lsymbol -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_decl -> unit
val print_next_type_decl : formatter -> ty_decl -> unit
val print_next_data_decl : formatter -> data_decl -> unit
val print_next_logic_decl : formatter -> logic_decl -> unit
val print_next_ind_decl : formatter -> ind_decl -> unit
val print_prop_decl : formatter -> prop_decl -> unit
......
......@@ -167,7 +167,9 @@ let new_meta task t td =
let add_decl task d = new_decl task d (create_decl d)
let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)
let add_ty_decl tk ts = add_decl tk (create_ty_decl ts)
let add_data_decl tk dl = add_decl tk (create_data_decl dl)
let add_param_decl tk ls = add_decl tk (create_param_decl ls)
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)
......
......@@ -75,7 +75,9 @@ val add_meta : task -> meta -> meta_arg list -> task
(** {2 declaration constructors + add_decl} *)
val add_ty_decl : task -> ty_decl list -> task
val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task
val add_param_decl : task -> lsymbol -> task
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 -> term -> task
......
......@@ -351,7 +351,7 @@ let add_symbol add id v uc =
uc_export = add true id.id_string v e0 :: ste }
| _ -> assert false
let add_type uc (ts,def) =
let add_data uc (ts,csl) =
let add_proj uc = function
| Some pj -> add_symbol add_ls pj.ls_name pj uc
| None -> uc in
......@@ -359,9 +359,7 @@ let add_type uc (ts,def) =
let uc = add_symbol add_ls fs.ls_name fs uc in
List.fold_left add_proj uc pl in
let uc = add_symbol add_ts ts.ts_name ts uc in
match def with
| Tabstract -> uc
| Talgebraic lfs -> List.fold_left add_constr uc lfs
List.fold_left add_constr uc csl
let add_logic uc (ls,_) = add_symbol add_ls ls.ls_name ls uc
......@@ -377,14 +375,18 @@ let create_decl d = mk_tdecl (Decl d)
let add_decl uc d =
let uc = add_tdecl uc (create_decl d) in
match d.d_node with
| Dtype dl -> List.fold_left add_type uc dl
| Dtype ts -> add_symbol add_ts ts.ts_name ts uc
| Ddata dl -> List.fold_left add_data uc dl
| Dparam ls -> add_symbol add_ls ls.ls_name ls uc
| Dlogic dl -> List.fold_left add_logic uc dl
| Dind dl -> List.fold_left add_ind uc dl
| Dprop p -> add_prop uc p
(** Declaration constructors + add_decl *)
let add_ty_decl uc dl = add_decl uc (create_ty_decl dl)
let add_ty_decl uc ts = add_decl uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl uc (create_data_decl dl)
let add_param_decl uc ls = add_decl uc (create_param_decl ls)
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)
......@@ -517,28 +519,29 @@ let cl_init th inst =
(* clone declarations *)
let cl_type cl inst tdl =
let cl_type cl inst ts =
if Mts.mem ts inst.inst_ts then
if ts.ts_def = None then raise EmptyDecl
else raise (CannotInstantiate ts.ts_name);
create_ty_decl (cl_find_ts cl ts)
let cl_data cl inst tdl =
let add_ls ls =
if Mls.mem ls inst.inst_ls
then raise (CannotInstantiate ls.ls_name)
else cl_find_ls cl ls
if Mls.mem ls inst.inst_ls then
raise (CannotInstantiate ls.ls_name);
cl_find_ls cl ls
in
let add_constr (ls,pl) =
add_ls ls, List.map (option_map add_ls) pl
add_ls ls, List.map (option_map add_ls) pl
in
let add_type (ts,td) acc =
let add_type (ts,csl) =
if Mts.mem ts inst.inst_ts then
if ts.ts_def = None && td = Tabstract then acc
else raise (CannotInstantiate ts.ts_name)
else
let ts' = cl_find_ts cl ts in
let td' = match td with
| Tabstract -> Tabstract
| Talgebraic cl -> Talgebraic (List.map add_constr cl)
in
(ts',td') :: acc
raise (CannotInstantiate ts.ts_name);
let ts' = cl_find_ts cl ts in
let td' = List.map add_constr csl in
(ts',td')
in
create_ty_decl (List.fold_right add_type tdl [])
create_data_decl (List.map add_type tdl)
let extract_ls_defn f =
let vl,_,f = match f.t_node with
......@@ -549,19 +552,18 @@ let extract_ls_defn f =
| Tbinop (_, {t_node = Tapp (ls,_)}, f) -> make_ls_defn ls vl f
| _ -> assert false
let cl_param cl inst ls =
if Mls.mem ls inst.inst_ls then raise EmptyDecl;
create_param_decl (cl_find_ls cl ls)
let cl_logic cl inst ldl =
let add_logic (ls,ld) acc = match ld with
| None when Mls.mem ls inst.inst_ls ->
acc
| None ->
(cl_find_ls cl ls, None) :: acc
| Some _ when Mls.mem ls inst.inst_ls ->
raise (CannotInstantiate ls.ls_name)
| Some ld ->
let f = ls_defn_axiom ld in
extract_ls_defn (cl_trans_fmla cl f) :: acc
let add_logic (ls,ld) =
if Mls.mem ls inst.inst_ls then
raise (CannotInstantiate ls.ls_name);
let f = ls_defn_axiom ld in
extract_ls_defn (cl_trans_fmla cl f)
in
create_logic_decl (List.fold_right add_logic ldl [])
create_logic_decl (List.map add_logic ldl)
let cl_ind cl inst idl =
let add_case (pr,f) =
......@@ -589,7 +591,9 @@ let cl_prop cl inst (k,pr,f) =
create_prop_decl k' pr' f'
let cl_decl cl inst d = match d.d_node with
| Dtype tdl -> cl_type cl inst tdl
| Dtype ts -> cl_type cl inst ts
| Ddata tdl -> cl_data cl inst tdl
| Dparam ls -> cl_param cl inst ls
| Dlogic ldl -> cl_logic cl inst ldl
| Dind idl -> cl_ind cl inst idl
| Dprop p -> cl_prop cl inst p
......@@ -747,9 +751,9 @@ let on_meta _meta fn acc theory =
let builtin_theory =
let uc = empty_theory (id_fresh "BuiltIn") [] in
let uc = add_ty_decl uc [ts_int, Tabstract] in
let uc = add_ty_decl uc [ts_real, Tabstract] in
let uc = add_logic_decl uc [ps_equ, None] in
let uc = add_ty_decl uc ts_int in
let uc = add_ty_decl uc ts_real in
let uc = add_param_decl uc ps_equ in
close_theory uc
let create_theory ?(path=[]) n =
......@@ -757,22 +761,22 @@ let create_theory ?(path=[]) n =
let bool_theory =
let uc = empty_theory (id_fresh "Bool") [] in
let uc = add_ty_decl uc [ts_bool, Talgebraic [fs_true,[]; fs_false,[]]] in
let uc = add_data_decl uc [ts_bool, [fs_true,[]; fs_false,[]]] in
close_theory uc
let highord_theory =
let uc = empty_theory (id_fresh "HighOrd") [] in
let uc = add_ty_decl uc [ts_func, Tabstract] in
let uc = add_ty_decl uc [ts_pred, Tabstract] in
let uc = add_logic_decl uc [fs_func_app, None] in
let uc = add_logic_decl uc [ps_pred_app, None] in
let uc = add_ty_decl uc ts_func in
let uc = add_ty_decl uc ts_pred in
let uc = add_param_decl uc fs_func_app in
let uc = add_param_decl uc ps_pred_app in
close_theory uc
let tuple_theory = Util.memo_int 17 (fun n ->
let ts = ts_tuple n and fs = fs_tuple n in
let pl = List.map (fun _ -> None) ts.ts_args in
let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) [] in
let uc = add_ty_decl uc [ts, Talgebraic [fs,pl]] in
let uc = add_data_decl uc [ts, [fs,pl]] in
close_theory uc)
let tuple_theory_name s =
......
......@@ -135,7 +135,9 @@ val create_decl : decl -> tdecl
val add_decl : theory_uc -> decl -> theory_uc
val add_ty_decl : theory_uc -> ty_decl list -> theory_uc
val add_ty_decl : theory_uc -> tysymbol -> theory_uc
val add_data_decl : theory_uc -> data_decl list -> theory_uc
val add_param_decl : theory_uc -> lsymbol -> theory_uc
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 -> term -> theory_uc
......
......@@ -151,7 +151,9 @@ let specialize_tysymbol loc p uc =
(* lazy declaration of tuples *)
let add_ty_decl uc dl = add_decl_with_tuples uc (create_ty_decl dl)
let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl)
let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls)
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
let add_ind_decl uc dl = add_decl_with_tuples uc (create_ind_decl dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
......@@ -832,12 +834,19 @@ let add_types dl th =
Hashtbl.add tysymbols x (Some ts);
ts
in
let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in
let th' = try add_ty_decl th tsl
let th' =
let add_ts (abstr,alias) d =
let ts = visit d.td_ident.id in
if ts.ts_def = None then ts::abstr, alias else abstr, ts::alias in
let abstr,alias = List.fold_left add_ts ([],[]) dl in
try
let th = List.fold_left add_ty_decl th abstr in
let th = List.fold_left add_ty_decl th alias in
th
with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (ClashSymbol s)
in
let csymbols = Hashtbl.create 17 in
let decl d =
let decl d (abstr,algeb,alias) =
let ts, denv' = match Hashtbl.find tysymbols d.td_ident.id with
| None ->
assert false
......@@ -851,9 +860,9 @@ let add_types dl th =
ts.ts_args;
ts, denv'
in
let d = match d.td_def with
| TDabstract | TDalias _ ->
Tabstract
match d.td_def with
| TDabstract -> ts::abstr, algeb, alias
| TDalias _ -> abstr, algeb, ts::alias
| TDalgebraic cl ->
let ht = Hashtbl.create 17 in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
......@@ -879,13 +888,16 @@ let add_types dl th =
Hashtbl.replace csymbols id.id loc;
create_fsymbol (create_user_id id) tyl ty, pjl
in
Talgebraic (List.map constructor cl)
abstr, (ts, List.map constructor cl) :: algeb, alias
| TDrecord _ ->
assert false
in
ts, d
in
try add_ty_decl th (List.map decl dl)
let abstr,algeb,alias = List.fold_right decl dl ([],[],[]) in
try
let th = List.fold_left add_ty_decl th abstr in
let th = if algeb = [] then th else add_data_decl th algeb in
let th = List.fold_left add_ty_decl th alias in
th
with
| ClashSymbol s ->
error ~loc:(Hashtbl.find csymbols s) (ClashSymbol s)
......@@ -935,18 +947,18 @@ let add_logics dl th =
| None -> (* predicate *)
let ps = create_psymbol v pl in
Hashtbl.add psymbols id ps;
add_logic_decl th [ps, None]
add_param_decl th ps
| Some t -> (* function *)
let t = type_ty (None, t) in
let fs = create_fsymbol v pl t in
Hashtbl.add fsymbols id fs;
add_logic_decl th [fs, None]
add_param_decl th fs
in
Loc.try1 d.ld_loc add d
in
let th' = List.fold_left create_symbol th dl in
(* 2. then type-check all definitions *)
let type_decl d =
let type_decl d (abst,defn) =
let id = d.ld_ident.id in
check_quant_linearity d.ld_params;
let dadd_var denv (x, ty) = match x with
......@@ -969,7 +981,7 @@ let add_logics dl th =
| None -> (* predicate *)
let ps = Hashtbl.find psymbols id in
begin match d.ld_def with
| None -> ps,None
| None -> ps :: abst, defn
| Some f ->
let f = dfmla th' denv f in
let vl = match ps.ls_value with
......@@ -977,12 +989,12 @@ let add_logics dl th =
| _ -> assert false
in
let env = env_of_vsymbol_list vl in
make_ls_defn ps vl (fmla env f)
abst, make_ls_defn ps vl (fmla env f) :: defn
end
| Some ty -> (* function *)
let fs = Hashtbl.find fsymbols id in
begin match d.ld_def with
| None -> fs,None
| None -> fs :: abst, defn
| Some t ->
let loc = t.pp_loc in
let ty = dty th' denv ty in
......@@ -993,10 +1005,13 @@ let add_logics dl th =
| _ -> assert false
in
let env = env_of_vsymbol_list vl in
make_ls_defn fs vl (term env t)
abst, make_ls_defn fs vl (term env t) :: defn
end
in
add_logic_decl th (List.map type_decl dl)
let abst,defn = List.fold_right type_decl dl ([],[]) in
let th = List.fold_left add_param_decl th abst in
let th = if defn = [] then th else add_logic_decl th defn in
th
let type_term uc denv env t =
let t = dterm uc denv t in
......@@ -1024,7 +1039,7 @@ let add_inductives dl th =
let pl = List.map type_ty d.in_params in
let ps = create_psymbol v pl in
Hashtbl.add psymbols id ps;
Loc.try2 d.in_loc add_logic_decl th [ps, None]
Loc.try2 d.in_loc add_param_decl th ps
in
let th' = List.fold_left create_symbol th dl in
(* 2. then type-check all definitions *)
......
......@@ -193,14 +193,15 @@ let print_enum_decl fmt ts csl =
fprintf fmt "type %a =@ %a@\n@\n" print_ident ts.ts_name
(print_list alt print_cs) csl
let print_type_decl info fmt = function
| ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> ()
| ts, Tabstract ->
fprintf fmt "%a@\n@\n" print_type_decl ts; forget_tvs ()
| ts, Talgebraic csl (* monomorphic enumeration *)
let print_ty_decl info fmt ts =
if Mid.mem ts.ts_name info.info_syn then () else
(fprintf fmt