Changeset 2950

Timestamp:

Mar 25, 2013, 10:39:07 PM (5 years ago)

Author:

sacerdot

Message:

linearise repaired (did I do the right thing???)

File:

• src/joint/linearise.ma (modified) (1 diff)

src/joint/linearise.ma

@@ -881 +881 @@
 
 definition linearise : ∀p : uns_params.
-  program (joint_function (mk_graph_params p)) ℕ →
-  program (joint_function (mk_lin_params p)) ℕ
+  joint_program (mk_graph_params p) →
+  joint_program (mk_lin_params p)
+  (*program (joint_function (mk_graph_params p)) ℕ →
+  program (joint_function (mk_lin_params p)) ℕ*)
    ≝
-  λp,pr.transform_program ??? pr
-    mk_joint_program
+  λp,pr.(*transform_program ??? pr*)
+   mk_joint_program ?
+    (transform_program ??? pr
+     (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))))
+    (init_cost_label ? pr).
+    
+(*    mk_joint_program
       (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in)))
       (init_cost_label … pr).
-
+*)
 (*
 definition good_sigma :