Revision c02d255e
Added by PierreLoïc Garoche almost 9 years ago
src/corelang.ml  

75  75 
 Expr_pre of expr 
76  76 
 Expr_when of expr * ident * label 
77  77 
 Expr_merge of ident * (label * expr) list 
78 
 Expr_appl of ident * expr * (ident * label) option


78 
 Expr_appl of call_t


79  79 
 Expr_uclock of expr * int 
80  80 
 Expr_dclock of expr * int 
81  81 
 Expr_phclock of expr * rat 
82  
82 
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) 

83  83  
84  84 
type eq = 
85  85 
{eq_lhs: ident list; 
...  ...  
513  513 
 _ > decl 
514  514 
) prog 
515  515  
516  
517  
518 
(************************************************************************) 

519 
(* Renaming *) 

520  
516  521 
(* applies the renaming function [fvar] to all variables of expression [expr] *) 
517  522 
let rec expr_replace_var fvar expr = 
518  523 
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } 
...  ...  
571  576 
 _ > assert false) 
572  577 
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } 
573  578  
579  
580 
let rec rename_expr f_node f_var f_const expr = 

581 
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } 

582 
and rename_expr_desc f_node f_var f_const expr_desc = 

583 
let re = rename_expr f_node f_var f_const in 

584 
match expr_desc with 

585 
 Expr_const _ > expr_desc 

586 
 Expr_ident i > Expr_ident (f_var i) 

587 
 Expr_array el > Expr_array (List.map re el) 

588 
 Expr_access (e1, d) > Expr_access (re e1, d) 

589 
 Expr_power (e1, d) > Expr_power (re e1, d) 

590 
 Expr_tuple el > Expr_tuple (List.map re el) 

591 
 Expr_ite (c, t, e) > Expr_ite (re c, re t, re e) 

592 
 Expr_arrow (e1, e2)> Expr_arrow (re e1, re e2) 

593 
 Expr_fby (e1, e2) > Expr_fby (re e1, re e2) 

594 
 Expr_pre e' > Expr_pre (re e') 

595 
 Expr_when (e', i, l)> Expr_when (re e', f_var i, l) 

596 
 Expr_merge (i, hl) > 

597 
Expr_merge (f_var i, List.map (fun (t, h) > (t, re h)) hl) 

598 
 Expr_appl (i, e', i') > 

599 
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) > f_var x, l) i') 

600 
 _ > assert false 

601  
602 
let rename_node_annot f_node f_var f_const expr = 

603 
assert false 

604  
605 
let rename_expr_annot f_node f_var f_const annot = 

606 
assert false 

607  
608 
let rename_node f_node f_var f_const nd = 

609 
let rename_var v = { v with var_id = f_var v.var_id } in 

610 
let inputs = List.map rename_var nd.node_inputs in 

611 
let outputs = List.map rename_var nd.node_outputs in 

612 
let locals = List.map rename_var nd.node_locals in 

613 
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in 

614 
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in 

615 
let node_asserts = List.map 

616 
(fun a > 

617 
{ a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 

618 
) nd.node_asserts 

619 
in 

620 
let eqs = List.map 

621 
(fun eq > { eq with 

622 
eq_lhs = List.map f_var eq.eq_lhs; 

623 
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs 

624 
} ) nd.node_eqs 

625 
in 

626 
let spec = 

627 
Utils.option_map 

628 
(fun s > rename_node_annot f_node f_var f_const s) 

629 
nd.node_spec 

630 
in 

631 
let annot = 

632 
Utils.option_map 

633 
(fun s > rename_expr_annot f_node f_var f_const s) 

634 
nd.node_annot 

635 
in 

636 
{ 

637 
node_id = f_node nd.node_id; 

638 
node_type = nd.node_type; 

639 
node_clock = nd.node_clock; 

640 
node_inputs = inputs; 

641 
node_outputs = outputs; 

642 
node_locals = locals; 

643 
node_gencalls = gen_calls; 

644 
node_checks = node_checks; 

645 
node_asserts = node_asserts; 

646 
node_eqs = eqs; 

647 
node_spec = spec; 

648 
node_annot = annot; 

649 
} 

650  
651  
652 
let rename_const f_const c = 

653 
{ c with const_id = f_const c.const_id } 

654 


655 
let rename_prog f_node f_var f_const prog = 

656 
List.rev ( 

657 
List.fold_left (fun accu top > 

658 
(match top.top_decl_desc with 

659 
 Node nd > 

660 
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } 

661 
 Consts c > 

662 
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) } 

663 
 ImportedNode _ 

664 
 ImportedFun _ 

665 
 Open _ > top) 

666 
::accu 

667 
) [] prog 

668 
) 

669  
670 
(**********************************************************************) 

574  671 
(* Pretty printers *) 
575  672  
576  673 
let pp_decl_type fmt tdecl = 
Also available in: Unified diff
Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process