Commit 9cf86e9f authored by Pascal Raymond's avatar Pascal Raymond
Browse files

LutExp compiles (but does not run)

parent 56ef7cac
......@@ -119,6 +119,8 @@ SOURCES=\
$(OBJDIR)/utils.mli \
$(LURETTE_SOURCES_C) \
$(LURETTE_SOURCES) \
$(OBJDIR)/expEval.mli \
$(OBJDIR)/expEval.ml \
$(OBJDIR)/verbose.ml \
$(OBJDIR)/verbose.mli \
$(OBJDIR)/errors.ml \
......@@ -136,16 +138,20 @@ SOURCES=\
$(OBJDIR)/checkEnv.mli \
$(OBJDIR)/predef.ml \
$(OBJDIR)/checkType.ml \
$(OBJDIR)/coIdent.ml \
$(OBJDIR)/coIdent.mli \
$(OBJDIR)/coAlgExp.ml \
$(OBJDIR)/coIdent.ml \
$(OBJDIR)/coAlgExp.mli \
$(OBJDIR)/coTraceExp.ml \
$(OBJDIR)/coAlgExp.ml \
$(OBJDIR)/coTraceExp.mli \
$(OBJDIR)/coTraceExp.ml \
$(OBJDIR)/glue.mli \
$(OBJDIR)/glue.ml \
$(OBJDIR)/guard.ml \
$(OBJDIR)/guard.mli \
$(OBJDIR)/expand.ml \
$(OBJDIR)/expand.mli \
$(OBJDIR)/lutExe.mli \
$(OBJDIR)/lutExe.ml \
$(OBJDIR)/autoExplore.ml \
$(OBJDIR)/autoExplore.mli \
$(OBJDIR)/autoGen.ml \
......@@ -166,6 +172,7 @@ SOURCES=\
RESULT=lutin
ln: $(OBJDIR) $(SOURCES)
......
......@@ -137,7 +137,7 @@ let init_control (it:t) = it.init_control
let transitions (it:t) = it.transitions
(* ADD/REPLACE pre values in data strore *)
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.escope) = (
match pctx with
| [] -> data
| _ -> (
......@@ -145,13 +145,17 @@ let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.
| Some d -> d
| None -> Guard.empty_store
in
let addp accin (id, e) = (
let v = try (
Guard.value_of_algexp unalias ctx e
) with Guard.Not_constant e -> raise (Internal_error ("AutoExplore.add_pres",
("initial value of \""^id^"\" must be a constant expression")))
in
Value.OfIdent.add accin (id, v)
let addp accin (id, eo) = (
match eo with
| None -> accin
| Some e -> (
let v = try (
Guard.value_of_algexp unalias ctx e
) with Guard.Not_constant e -> raise (Internal_error ("AutoExplore.add_pres",
("initial value of \""^id^"\" must be a constant expression")))
in
Value.OfIdent.add accin (id, v)
)
) in
let new_pres = List.fold_left addp ctx.Guard.pres pctx in
Some {Guard.curs=ctx.Guard.curs; Guard.pres=new_pres}
......@@ -529,11 +533,11 @@ let gentrans
cont None
)
)
(** init_pre
(** exist: matters is some vars are re-initialised
recursive call with a new store
*)
| TE_init_pre (pctx, te) -> (
let new_data = add_pres unalias data pctx in
| TE_exist (ectx, te) -> (
let new_data = add_pres unalias data ectx in
rec_gentrans new_data te acc cont
)
(** RAISE
......
......@@ -160,7 +160,7 @@ let init_control (it:t) = it.init_control
let transitions (it:t) = it.transitions
(* ADD/REPLACE pre values in data strore *)
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.pre_ctx) = (
let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.escope) = (
match pctx with
| [] -> data
| _ -> (
......@@ -168,13 +168,17 @@ let add_pres (unalias:Guard.unalias) (data:Guard.store option) (pctx:CoTraceExp.
| Some d -> d
| None -> Guard.empty_store
in
let addp accin (id, e) = (
let v = try (
Guard.value_of_algexp unalias ctx e
) with Guard.Not_constant e -> raise (Internal_error ("AutoExplore.add_pres",
("initial value of \""^id^"\" must be a constant expression")))
in
Value.OfIdent.add accin (id, v)
let addp accin (id, eo) = (
match eo with
| None -> accin
| Some e -> (
let v = try (
Guard.value_of_algexp unalias ctx e
) with Guard.Not_constant e -> raise (Internal_error ("AutoExplore.add_pres",
("initial value of \""^id^"\" must be a constant expression")))
in
Value.OfIdent.add accin (id, v)
)
) in
let new_pres = List.fold_left addp ctx.Guard.pres pctx in
Some {Guard.curs=ctx.Guard.curs; Guard.pres=new_pres}
......@@ -553,8 +557,8 @@ let gentrans
(** init_pre
recursive call with a new store
*)
| TE_init_pre (pctx, te) -> (
let new_data = add_pres unalias data pctx in
| TE_exist (ectx, te) -> (
let new_data = add_pres unalias data ectx in
rec_gentrans new_data te acc cont
)
(** RAISE
......
......@@ -36,18 +36,11 @@ let nb_loops () = !loop_cpt_number
(* type loop_weighter = int -> (int, int) *)
(* pre context for local variable scope :
list of (id * CoAlgExp.t)
WARNING : maybe use a table/set later ???
*)
type pre_ctx = (CoIdent.t * CoAlgExp.t) list
let add_pre_ctx pctx (i,v) = (i,v)::pctx
let new_pre_ctx () = []
let get_pre_ctx pctx id = (
try Some (List.assoc id pctx)
with Not_found -> None
)
(* exist-scope = list of ident + init_value option *)
type escope = (CoIdent.t * CoAlgExp.t option) list
let add_escope ctx (i,v) = (i,v)::ctx
let new_escope () = []
type t =
| TE_eps
......@@ -67,7 +60,7 @@ type t =
| TE_assert of CoAlgExp.t * t
(* Takes a list (id,val) *)
| TE_init_pre of pre_ctx * t
| TE_exist of escope * t
| TE_raise of string
| TE_try of t * t option
| TE_catch of string * t * t option
......@@ -91,7 +84,7 @@ let of_loopg getweights cpt e = (TE_loopg (getweights, cpt, e))
let of_assert c e = (TE_assert (c,e))
let of_init_pre pctx e = (TE_init_pre (pctx,e))
let of_exist ctx e = (TE_exist (ctx,e))
let of_raise s = (TE_raise s)
......@@ -179,16 +172,20 @@ let rec _dump (pr: string -> unit) te = (
pr " in ";
_dump pr e ;
)
| TE_init_pre (pctx,e) -> (
pr "init ";
let pp (i,v) = (
pr "pre ";
| TE_exist (ctx,e) -> (
pr "exist ";
let pp (i,vo) = (
pr (CoIdent.to_string i);
pr " = ";
pr (CoAlgExp.lus_dumps v) ;
let _ = match vo with
| Some v -> (
pr " init ";
pr (CoAlgExp.lus_dumps v) ;
)
| None -> ()
in
pr ";"
) in
List.iter pp pctx;
List.iter pp ctx;
pr " in ";
_dump pr e ;
)
......
......@@ -17,11 +17,10 @@ N.B. les exceptions sont enti
(** On exporte la structure du type *)
type pre_ctx = (CoIdent.t * CoAlgExp.t) list
type escope = (CoIdent.t * CoAlgExp.t option) list
val new_pre_ctx : unit -> pre_ctx
val add_pre_ctx : pre_ctx -> (CoIdent.t * CoAlgExp.t) -> pre_ctx
val get_pre_ctx : pre_ctx -> CoIdent.t -> CoAlgExp.t option
val new_escope : unit -> escope
val add_escope : escope -> (CoIdent.t * CoAlgExp.t option) -> escope
type t =
| TE_eps
......@@ -38,7 +37,7 @@ type t =
(* internal loop with inline weigth computer + compteur *)
| TE_loopg of (int -> int * int) * int * t
| TE_assert of CoAlgExp.t * t
| TE_init_pre of pre_ctx * t
| TE_exist of escope * t
| TE_raise of string
| TE_try of t * t option
| TE_catch of string * t * t option
......@@ -79,7 +78,7 @@ val of_choice : (t * CoAlgExp.t option ) list -> t
val of_assert : CoAlgExp.t -> t -> t
val of_init_pre : pre_ctx -> t -> t
val of_exist : escope -> t -> t
val of_raise : string -> t
......
......@@ -78,16 +78,17 @@ type support_nature =
| Output
| Local
and support_info = {
si_nature : support_nature ;
si_type : CkTypeEff.t ;
si_ref_exp : CoAlgExp.t ;
si_src : CoIdent.src_stack;
(* on ne la crée qu'à la demande *)
mutable si_pre_ref_exp : CoAlgExp.t option ;
si_default : CoAlgExp.t option ;
si_scope : support_scope option ;
si_init : CoAlgExp.t option ;
si_range : (CoAlgExp.t * CoAlgExp.t) option;
si_ident : CoIdent.t ;
si_nature : support_nature ;
si_type : CkTypeEff.t ;
si_ref_exp : CoAlgExp.t ;
si_src : CoIdent.src_stack;
(* on ne la crée qu'à la demande *)
mutable si_pre_ref_exp : CoAlgExp.t option ;
si_default : CoAlgExp.t option ;
si_scope : support_scope option ;
si_init : CoAlgExp.t option ;
si_range : (CoAlgExp.t * CoAlgExp.t) option;
}
(**************************************************************
......@@ -98,27 +99,18 @@ A scope contains a pre (re)init context
and support_scope = {
sco_src : CoIdent.src_stack;
mutable sco_init : CoTraceExp.pre_ctx option;
mutable sco_escope : CoTraceExp.escope;
}
let new_support_scope (src : CoIdent.src_stack) = (
let res = {
sco_src = src;
(* made on demand *)
sco_init = None ;
sco_escope = CoTraceExp.new_escope () ;
} in
res
)
let add_support_scope_constraint scope id va = (
let oldp = match scope.sco_init with
| None -> CoTraceExp.new_pre_ctx ()
| Some p -> p
in
scope.sco_init <- Some (CoTraceExp.add_pre_ctx oldp (id, va))
)
(**
Alias : L'info contient le type, l'expression à utiliser pour faire
référence à l'alias, et celle qui correspond à sa définition
......@@ -342,22 +334,22 @@ let new_support_input
let te = CkTypeEff.of_texp t in
let src = CoIdent.get_src_stack i.src sstack in
Hashtbl.add _support_tab tgtid {
si_nature = Input ;
si_type = CkTypeEff.of_texp t ;
si_ref_exp = CoAlgExp.of_support tgtid te false;
(* a priori pas utilisé *)
(* si_pre_ref_exp = CoAlgExp.of_pre tgtid te ; *)
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = None;
si_init = None;
si_ident = tgtid ;
si_nature = Input ;
si_type = CkTypeEff.of_texp t ;
si_ref_exp = CoAlgExp.of_support tgtid te false;
(* a priori pas utilisé *)
(* si_pre_ref_exp = CoAlgExp.of_pre tgtid te ; *)
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = None;
si_init = None;
si_range = None;
};
(* on garde la liste pour les sortir dans l'ordre *)
_input_list := (tgtid) :: !_input_list ;
};
(* on garde la liste pour les sortir dans l'ordre *)
_input_list := (tgtid) :: !_input_list ;
add_support_target_id i tgtid
)
......@@ -375,23 +367,24 @@ let new_support_output
let te = CkTypeEff.of_texp t in
let src = get_src_stack i.src sstack in
Hashtbl.add _support_tab tgtid {
si_nature = Output ;
si_type = CkTypeEff.of_texp t ;
si_ref_exp = CoAlgExp.of_support tgtid te true;
(* a priori pas utilisé *)
(* si_pre_ref_exp = CoAlgExp.of_pre tgtid te ; *)
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = None;
si_init = init;
si_range = range_opt;
};
(* on garde la liste pour les sortir dans l'ordre *)
_output_list := (tgtid) :: !_output_list ;
add_support_target_id i tgtid
si_ident = tgtid ;
si_nature = Output ;
si_type = CkTypeEff.of_texp t ;
si_ref_exp = CoAlgExp.of_support tgtid te true;
(* a priori pas utilisé *)
(* si_pre_ref_exp = CoAlgExp.of_pre tgtid te ; *)
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = None;
si_init = init;
si_range = range_opt;
};
(* on garde la liste pour les sortir dans l'ordre *)
_output_list := (tgtid) :: !_output_list ;
add_support_target_id i tgtid
)
(** Déclaration d'une locale *)
......@@ -409,23 +402,29 @@ let new_support_local
let tgtid = CoIdent.get_fresh i.it in
let te = CkTypeEff.of_texp t in
let src = get_src_stack i.src sstack in
Hashtbl.add _support_tab tgtid {
si_nature = Local;
si_type = CkTypeEff.of_texp t ;
si_ref_exp = CoAlgExp.of_support tgtid te true;
(* a priori pas utilisé *)
(* si_pre_ref_exp = CoAlgExp.of_pre tgtid te ; *)
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = scope;
si_init = init;
si_range = range_opt;
};
(* on garde la liste pour les sortir dans l'ordre *)
_local_list := (tgtid) :: !_local_list ;
Hashtbl.add _support_tab tgtid {
si_ident = tgtid;
si_nature = Local;
si_type = CkTypeEff.of_texp t ;
si_ref_exp = CoAlgExp.of_support tgtid te true;
(* a priori pas utilisé *)
(* si_pre_ref_exp = CoAlgExp.of_pre tgtid te ; *)
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = scope;
si_init = init;
si_range = range_opt;
};
(* on garde la liste pour les sortir dans l'ordre *)
_local_list := (tgtid) :: !_local_list ;
(* adds the def to the exist-scope if any *)
let _ = match scope with
| None -> ()
| Some ctx -> ctx.sco_escope <- CoTraceExp.add_escope ctx.sco_escope (tgtid, init)
in
add_support_target_id i tgtid
)
......@@ -507,62 +506,7 @@ let new_pre_handler
= (
let te = id_info.si_type in
let pre_X = CoAlgExp.of_pre id te in
(* Reinitializable LOCAL var ? *)
let _ = match (id_info.si_scope, id_info.si_init) with
| (Some scope, Some init) -> (
add_support_scope_constraint scope id init
)
| (_,_) -> (
(* NO: nothing to do ... *)
) in
pre_X
(*
(* var preX inherit type and has no source *)
let preid = CoIdent.get ("pre"^(CoIdent.to_string id)) in
let te = id_info.si_type in
let src = CoIdent.base_stack () in
(* "pre X" *)
let pre_X = CoAlgExp.of_pre id te in
(* Reinitializable LOCAL var ? *)
let ze_right_ref = match (id_info.si_scope, id_info.si_init) with
| (Some scope, Some init) -> (
(* YES: NEW SUPPORT VAR, NEW scope CONSTRAINTS *)
(* let eref = CoAlgExp.of_support preid te true in *)
let eref = CoAlgExp.of_support preid te false in
Hashtbl.add _support_tab preid {
si_nature = Local;
si_type = te;
si_ref_exp = eref ;
si_pre_ref_exp = None ;
si_src = src;
si_default = None;
si_scope = Some scope;
si_init = Some init;
(* HERE: is it right ? *)
si_range = None ;
};
_local_list := preid::!_local_list ;
let initc = CoAlgExp.of_eq eref init in
let otherc = CoAlgExp.of_eq eref pre_X in
add_support_scope_constraint scope initc otherc;
eref
)
| (_,_) -> (
(* NO: simple alias: preX = pre X *)
let eref = CoAlgExp.of_alias preid te false in
let edef = pre_X in
Hashtbl.add _alias_tab preid {
ai_type = te ;
ai_def_exp = edef ;
ai_ref_exp = eref ;
ai_src = src ;
};
_alias_list := preid::!_alias_list;
eref
) in
ze_right_ref
*)
)
let alg_exp_of_support_pre_ref tgtid = (
......@@ -584,6 +528,8 @@ Table des traces
let _trace_tab : (CoIdent.t, trace_info) Hashtbl.t = Hashtbl.create 50
(* Unicité des idents target de traces *)
let fresh_trace_id s = ( CoIdent.get_fresh s )
let fixed_trace_id s = ( CoIdent.get s )
......@@ -1254,19 +1200,16 @@ and
let newidlist = List.map (eval_init_in_var_decl env sstack) idlst in
let src_scope = CoIdent.get_src_stack e.src sstack in
(* The scope contraints are created EMPTY ... *)
(* The exist-scope is created EMPTY ... *)
let zescope = new_support_scope src_scope in
(* ... then filled by added var one by one *)
(* ... then filled by added var one by one *)
let f = function (i, t, ivopt, range_opt) -> (
new_support_local ~scope:(Some zescope) ~init:ivopt range_opt i t sstack
new_support_local ~scope:(Some zescope) ~init:ivopt range_opt i t sstack
) in
List.iter f newidlist;
(* on continu dans ce nouvel env ... *)
let res = treat_trace env sstack ee in
(* un reinit a-il été associé au scope lors du traitement des id ? *)
match zescope.sco_init with
| None -> res
| Some p -> CoTraceExp.of_init_pre p res
CoTraceExp.of_exist zescope.sco_escope res
)
(* traces *)
| FBY_n (e1,e2) -> (
......@@ -1468,6 +1411,10 @@ let trace_tab (x:t) = x.ttab
let extern_tab (x:t) = x.etab
let main_trace (x:t) = x.mtrace
let get_trace_info it id = (
Hashtbl.find it.ttab id
)
let make (env : CheckEnv.t) (p : Syntaxe.package) (n : string) = (
(* On (re)met les variables globales à 0, au cas où ... *)
CoIdent.reset ();
......
......@@ -53,6 +53,7 @@ type support_nature =
| Output
| Local
and support_info = {
si_ident : CoIdent.t ;
si_nature : support_nature ;
si_type : CkTypeEff.t ;
si_ref_exp : CoAlgExp.t ;
......@@ -99,6 +100,8 @@ type trace_info = {
val trace_tab : t -> (CoIdent.t, trace_info) Hashtbl.t
val get_trace_info : t -> CoIdent.t -> trace_info
(** Info et table des externes utilisées
on garde le CkIdentInfo.t tel quel pour
usage ultérieur (génération de code)
......
......@@ -17,6 +17,7 @@ let dbg = Verbose.get_flag "Guard"
(* a guard is splitted into:
- a Value.OfIdent.t corresponding to the set of "var = val" constraints
- a list of remaining constaints
*)
type t = {
idies : Value.OfIdent.t ;
......@@ -29,6 +30,8 @@ type store = { curs : Value.OfIdent.t; pres: Value.OfIdent.t }
let empty_store = { curs=Value.OfIdent.empty; pres=Value.OfIdent.empty }
let get_store c p = { curs=c; pres=p}
type unalias = CoIdent.t -> CoAlgExp.t
let no_unalias = fun _ -> ( assert false )
......@@ -57,9 +60,13 @@ let to_exp_list g = (
(List.map idy2exp (Value.OfIdent.content g.idies))@(g.others)
)
let to_string g = (
let cl = List.map CoAlgExp.lus_dumps (to_exp_list g) in
String.concat " and " cl
)
let dumpf os g = (
let x = to_exp_list g in
Utils.iter_sep (CoAlgExp.dumpf os) (function _ -> Printf.fprintf os " & ") x
Printf.fprintf os "%s" (to_string g)
)
......@@ -324,6 +331,9 @@ let add_idy g (v,x) = (
Value.OfIdent.add g (v,x)
)
)
let merge_idies (g1:Value.OfIdent.t) (g2:Value.OfIdent.t) = (
Value.OfIdent.fold (fun v x g -> add_idy g (v, x)) g1 g2
)
let add_atom accin e = (
try (
(* search for identities *)
......@@ -389,7 +399,12 @@ match context with
Verbose.put ~flag:dbg " and pres =\n%s\n" (Value.OfIdent.to_string "" d.pres)
);
);
let c' = simplify_exp unalias ctx c in
(* take both context and current idies in g to simplify c *)
let ctx' = { curs = merge_idies g.idies ctx.curs; pres = ctx.pres } in
let c' = simplify_exp unalias ctx' c in
(* c' does not contain any var from ctx' *)
Verbose.put ~flag:dbg " partial eval gives %s\n" (CoAlgExp.lus_dumps c');
let cl = split_conj c' in
let res = List.fold_left add_atom g cl in
......@@ -423,5 +438,3 @@ let merge ?(unalias=no_unalias) ?(context=None) g1 g2 = (
(* HERE: really necessary ??? *)
(* let simplify ctx x = x *)
(* List.map (simplify_exp ctx) x *)
......@@ -22,6 +22,10 @@ type unalias = CoIdent.t -> CoAlgExp.t
val empty_store : store
val get_store : Value.OfIdent.t -> Value.OfIdent.t -> store
val to_string : t -> string
exception Unsat
val of_exp : ?unalias:unalias -> ?context:store option -> CoAlgExp.t -> t
......