clone (en cours)

parent b97bb9c0
theory A
type t
end
theory B
clone import A
type t
end
...@@ -498,14 +498,56 @@ type th_inst = { ...@@ -498,14 +498,56 @@ type th_inst = {
inst_ps : psymbol Mps.t; inst_ps : psymbol Mps.t;
} }
let clone_export th t i = let clone_export uc th i =
let check_sym id = let check_sym id =
if not (Sid.mem id t.th_param) then raise (CannotInstantiate id) if not (Sid.mem id th.th_param) then raise (CannotInstantiate id)
in in
let check_ts s _ = check_sym s.ts_name in Mts.iter check_ts i.inst_ts; let check_ts s _ = check_sym s.ts_name in Mts.iter check_ts i.inst_ts;
let check_fs s _ = check_sym s.fs_name in Mfs.iter check_fs i.inst_fs; let check_fs s _ = check_sym s.fs_name in Mfs.iter check_fs i.inst_fs;
let check_ps s _ = check_sym s.ps_name in Mps.iter check_ps i.inst_ps; let check_ps s _ = check_sym s.ps_name in Mps.iter check_ps i.inst_ps;
assert false (* TODO *) (* memo tables *)
let ts_table = Hashtbl.create 17 in
let known = ref th.th_known in
let rec memo_ts ts =
try
Hashtbl.find ts_table ts.ts_name
with Not_found ->
let nm = id_clone ts.ts_name in
let def = match ts.ts_def with
| None -> None
| Some ty -> Some (ty_s_map memo_ts ty)
in
let ts' = create_tysymbol nm ts.ts_args def in
Hashtbl.add ts_table ts.ts_name ts';
known := Mid.add ts'.ts_name uc.uc_name (Mid.remove ts.ts_name !known);
ts'
in
let find_ts ts =
let tid = Mid.find ts.ts_name th.th_known in
if tid == th.th_name then memo_ts ts else ts
in
(* 1. merge in the new namespace *)
let rec merge_namespace acc ns =
let acc =
Mnm.fold (fun n ts acc -> add_ts n (find_ts ts) acc) ns.ns_ts acc
in
(* ... *)
(* let acc = Mnm.fold (fun n ns acc -> ) ns.ns_ns acc in *)
acc
in
let ns = merge_namespace empty_ns th.th_export in
let uc = match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste ->
{ uc with
uc_import = merge_ns ns i0 :: sti;
uc_export = merge_ns ns e0 :: ste;
uc_known = merge_known uc.uc_known !known }
| _ ->
assert false
in
(* 2. merge in the new declarations *)
(* ... *)
uc
(** Debugging *) (** Debugging *)
......
...@@ -281,8 +281,10 @@ decl: ...@@ -281,8 +281,10 @@ decl:
{ Prop (loc (), Klemma, $2, $4) } { Prop (loc (), Klemma, $2, $4) }
| INDUCTIVE lident primitive_types inddefn | INDUCTIVE lident primitive_types inddefn
{ Inductive_def (loc (), $2, $3, $4) } { Inductive_def (loc (), $2, $3, $4) }
| CLONE use clone_subst
{ UseClone (loc (), $2, Some $3) }
| USE use | USE use
{ Use (loc (), $2) } { UseClone (loc (), $2, None) }
| NAMESPACE uident list0_decl END | NAMESPACE uident list0_decl END
{ Namespace (loc (), $2, $3) } { Namespace (loc (), $2, $3) }
; ;
...@@ -502,6 +504,27 @@ imp_exp: ...@@ -502,6 +504,27 @@ imp_exp:
| /* epsilon */ { Nothing } | /* epsilon */ { Nothing }
; ;
clone_subst:
| /* epsilon */
{ { ts_subst = []; fs_subst = []; ps_subst = [] } }
| WITH list1_comma_subst
{ let t, f, p = $2 in
{ ts_subst = t; fs_subst = f; ps_subst = p } }
;
list1_comma_subst:
| subst
{ $1 }
| subst COMMA list1_comma_subst
{ let t,f,p = $1 in let tl,fl,pl = $3 in t@tl, f@fl, p@pl }
;
subst:
| TYPE qualid EQUAL qualid { [$2, $4], [], [] }
| FUNCTION qualid EQUAL qualid { [], [$2, $4], [] }
| PREDICATE qualid EQUAL qualid { [], [], [$2, $4] }
;
/******* programs ************************************************** /******* programs **************************************************
list0_ident_sep_comma: list0_ident_sep_comma:
......
...@@ -75,6 +75,12 @@ type use = { ...@@ -75,6 +75,12 @@ type use = {
use_imp_exp : imp_exp; use_imp_exp : imp_exp;
} }
type clone_subst = {
ts_subst : (qualid * qualid) list;
fs_subst : (qualid * qualid) list;
ps_subst : (qualid * qualid) list;
}
type param = ident option * pty type param = ident option * pty
type type_def = type type_def =
...@@ -105,7 +111,7 @@ type decl = ...@@ -105,7 +111,7 @@ type decl =
| Logic of loc * logic_decl list | Logic of loc * logic_decl list
| Inductive_def of loc * ident * pty list * (loc * ident * lexpr) list | Inductive_def of loc * ident * pty list * (loc * ident * lexpr) list
| Prop of loc * prop_kind * ident * lexpr | Prop of loc * prop_kind * ident * lexpr
| Use of loc * use | UseClone of loc * use * clone_subst option
| Namespace of loc * ident * decl list | Namespace of loc * ident * decl list
type theory = { type theory = {
......
...@@ -273,12 +273,15 @@ let rec find f q ns = match q with ...@@ -273,12 +273,15 @@ let rec find f q ns = match q with
(** specific find functions using a path *) (** specific find functions using a path *)
let find_tysymbol {id=x; id_loc=loc} ns = let find_local_tysymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_ts try Mnm.find x ns.ns_ts
with Not_found -> error ~loc (UnboundType x) with Not_found -> error ~loc (UnboundType x)
let find_tysymbol_ns p ns =
find find_local_tysymbol p ns
let find_tysymbol p th = let find_tysymbol p th =
find find_tysymbol p (get_namespace th) find_tysymbol_ns p (get_namespace th)
let specialize_tysymbol ~loc x env = let specialize_tysymbol ~loc x env =
let s = find_tysymbol x env.th in let s = find_tysymbol x env.th in
...@@ -289,8 +292,11 @@ let find_fsymbol {id=x; id_loc=loc} ns = ...@@ -289,8 +292,11 @@ let find_fsymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_fs try Mnm.find x ns.ns_fs
with Not_found -> error ~loc (UnboundSymbol x) with Not_found -> error ~loc (UnboundSymbol x)
let find_fsymbol_ns p ns =
find find_fsymbol p ns
let find_fsymbol p th = let find_fsymbol p th =
find find_fsymbol p (get_namespace th) find_fsymbol_ns p (get_namespace th)
let specialize_fsymbol ~loc s = let specialize_fsymbol ~loc s =
let tl, t = s.fs_scheme in let tl, t = s.fs_scheme in
...@@ -301,8 +307,11 @@ let find_psymbol {id=x; id_loc=loc} ns = ...@@ -301,8 +307,11 @@ let find_psymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_ps try Mnm.find x ns.ns_ps
with Not_found -> error ~loc (UnboundSymbol x) with Not_found -> error ~loc (UnboundSymbol x)
let find_psymbol_ns p ns =
find find_psymbol p ns
let find_psymbol p th = let find_psymbol p th =
find find_psymbol p (get_namespace th) find_psymbol_ns p (get_namespace th)
let specialize_psymbol ~loc s = let specialize_psymbol ~loc s =
let env = Htv.create 17 in let env = Htv.create 17 in
...@@ -790,8 +799,28 @@ and add_decl env th = function ...@@ -790,8 +799,28 @@ and add_decl env th = function
add_logics loc dl th add_logics loc dl th
| Prop (loc, k, s, f) -> | Prop (loc, k, s, f) ->
add_prop (prop_kind k) loc s f th add_prop (prop_kind k) loc s f th
| Use (loc, use) -> | UseClone (loc, use, subst) ->
let t = find_theory env use.use_theory in let t = find_theory env use.use_theory in
let use_or_clone th = match subst with
| None ->
use_export th t
| Some s ->
let add_ts m (p, q) =
Mts.add (find_tysymbol_ns p t.th_export) (find_tysymbol q th) m
in
let add_fs m (p, q) =
Mfs.add (find_fsymbol_ns p t.th_export) (find_fsymbol q th) m
in
let add_ps m (p, q) =
Mps.add (find_psymbol_ns p t.th_export) (find_psymbol q th) m
in
let s =
{ inst_ts = List.fold_left add_ts Mts.empty s.ts_subst;
inst_fs = List.fold_left add_fs Mfs.empty s.fs_subst;
inst_ps = List.fold_left add_ps Mps.empty s.ps_subst; }
in
clone_export th t s
in
let n = match use.use_as with let n = match use.use_as with
| None -> t.th_name.id_short | None -> t.th_name.id_short
| Some x -> x.id | Some x -> x.id
...@@ -800,15 +829,15 @@ and add_decl env th = function ...@@ -800,15 +829,15 @@ and add_decl env th = function
| Nothing -> | Nothing ->
(* use T = namespace T use_export T end *) (* use T = namespace T use_export T end *)
let th = open_namespace th in let th = open_namespace th in
let th = use_export th t in let th = use_or_clone th in
close_namespace th n ~import:false close_namespace th n ~import:false
| Import -> | Import ->
(* use import T = namespace T use_export T end import T *) (* use import T = namespace T use_export T end import T *)
let th = open_namespace th in let th = open_namespace th in
let th = use_export th t in let th = use_or_clone th in
close_namespace th n ~import:true close_namespace th n ~import:true
| Export -> | Export ->
use_export th t use_or_clone th
with Theory.ClashSymbol s -> with Theory.ClashSymbol s ->
error ~loc (Clash s) error ~loc (Clash s)
end end
......
(* test file *) (* test file *)
theory Test theory A
type t
logic c : t
end
theory B
use A as C
clone import A
logic f(C.t) : t
axiom Ax : forall x:t. x = C.c
end
theory TreeForest
type 'a list = Nil | Cons('a, 'a list) type 'a list = Nil | Cons('a, 'a list)
type 'a tree = Leaf('a) | Node('a forest) type 'a tree = Leaf('a) | Node('a forest)
type 'a forest = 'a tree list type 'a forest = 'a tree list
axiom Ax : Cons(Nil,Nil)=Nil
end end
theory TestPrelude theory TestPrelude
...@@ -14,24 +24,6 @@ theory TestPrelude ...@@ -14,24 +24,6 @@ theory TestPrelude
use prelude.List use prelude.List
end end
theory A
use import prelude.Int
logic c : int
type 'a t
logic mem('a, 'a t)
logic p(s : 'a t) = forall x:'a. mem(x, s)
end
theory B
use import prelude.List
type t
axiom Ax : forall x : t list. true
lemma L : forall x : t list. true
goal G : forall x : t list. true
end
(* (*
Local Variables: Local Variables:
......
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