# HG changeset patch
# User nipkow
# Date 1141399530 -3600
# Node ID 9b295c37854fd2cb3610e5732748ccf1cc2cc557
# Parent  68c6824d8bb6d84c94a9ba2d6fe494aaad4a4ba7
ignore repeated vars on lhs, cleanup

diff -r 68c6824d8bb6 -r 9b295c37854f src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Fri Mar 03 08:52:39 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML	Fri Mar 03 16:25:30 2006 +0100
@@ -98,11 +98,9 @@
     else S.app Eval_Constr (S.tup [S.quote s,S.list args ])
   | IVar s => S.nbe_apps (MLvname s) args
   | e1 `$ e2 => mk (args @ [mk [] e2]) e1
-  | (nm, _) `|-> e =>
-      S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args
+  | (nm, _) `|-> e => S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args
   | IAbs (_, e) => mk args e
   | ICase (_, e) => mk args e
-  | _ => sys_error "NBE mkexpr"
   in mk [] end;
 
 val mk_lexpr =
@@ -117,8 +115,15 @@
   | _ => sys_error "NBE mk_lexpr illegal pattern"
   in mk [] end;
 
+fun vars (IVar s) = [s]
+  | vars (e1 `$ e2) = (vars e1) @ (vars e2)
+  | vars (IAbs(_,e)) = vars e
+  | vars (ICase(_,e)) = vars e
+  | vars _ = [] (* note that a lambda won't occur here anyway *)
+
 fun mk_eqn defined nm ar (lhs,e) =
-  ([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e);
+  if has_duplicates (op =) (Library.flat (map vars lhs)) then [] else
+  [([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e)];
 
 fun consts_of (IConst ((s, _), _)) = insert (op =) s
   | consts_of (e1 `$ e2) =
@@ -138,7 +143,8 @@
         val globals = map lookup (filter defined funs);
         val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
         val code = S.eqns (MLname nm)
-                          (map (mk_eqn defined nm ar) eqns @ [default_eqn])
+                          (Library.flat(map (mk_eqn defined nm ar) eqns) 
+                           @ [default_eqn])
         val register = tab_update
             (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
       in
@@ -168,211 +174,3 @@
   in to_term [] t end;
 
 end;
-
-(*
-
-val use_show = fn s => (writeln ("\n---generated code:\n"^ s);
-     use_text(writeln o enclose "\n---compiler echo:\n" "\n---\n",
-              writeln o enclose "\n--- compiler echo (with error!):\n" 
-                                "\n---\n")
-      true s);
-
-val dummyIT = CodegenThingol.IType("DUMMY",[]);
-
-use_show(NBE_Codegen.generate (the_context()) ("append",CodegenThingol.Fun(
-  [([CodegenThingol.IConst(("Nil",dummyIT),[]),
-     CodegenThingol.IVarE("ys",dummyIT)],
-    CodegenThingol.IVarE("ys",dummyIT)),
-   ([CodegenThingol.IApp(
-       CodegenThingol.IApp(
-         CodegenThingol.IConst(("Cons",dummyIT),[]),
-         CodegenThingol.IVarE("x",dummyIT)),
-       CodegenThingol.IVarE("xs",dummyIT)),
-     CodegenThingol.IVarE("ys",dummyIT)],
-    CodegenThingol.IApp(
-       CodegenThingol.IApp(
-         CodegenThingol.IConst(("Cons",dummyIT),[]),
-         CodegenThingol.IVarE("x",dummyIT)),
-       CodegenThingol.IApp(
-         CodegenThingol.IApp(
-           CodegenThingol.IConst(("append",dummyIT),[]),
-           CodegenThingol.IVarE("xs",dummyIT)),
-         CodegenThingol.IVarE("ys",dummyIT))))]
-  ,([],dummyIT))));
-
-
-let
-fun test a b = if a=b then () else error "oops!";
-
-val CNil = Const("Nil",dummyT);
-val CCons = Const("Cons",dummyT);
-val Cappend = Const("append",dummyT);
-val Fx = Free("x",dummyT);
-val Fy = Free("y",dummyT);
-val Fxs = Free("xs",dummyT);
-val Fys = Free("ys",dummyT);
-open NBE_Eval
-in
-test (nbe(CNil)) (C "Nil");
-test (nbe(CCons)) (C "Cons");
-test (nbe(Cappend)) (C "append");
-test (nbe(Cappend $ CNil $ CNil)) (C "Nil");
-test (nbe(Cappend $ Fxs)) (A (C "append", V "xs"));
-test (nbe(Cappend $ Fxs $ Fys)) (A (A (C "append", V "xs"), V "ys"));
-test (nbe(Cappend $ CNil $ Fxs)) (V "xs");
-test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ Fys))
-     (A (A (C "Cons", V "x"), A (A (C "append", V "xs"), V "ys")));
-test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ (CCons $ Fy $ Fys)))
-     (A (A (C "Cons", V "x"), A (A (C "append", V "xs"), A (A (C "Cons", V "y"), V "ys"))));
-test (nbe(Cappend $ (CCons $ Fx $ (CCons $ Fy $ Fxs)) $ (CCons$Fy$Fys)))
- (A
-      (A (C "Cons", V "x"),
-         A
-            (A (C "Cons", V "y"),
-               A (A (C "append", V "xs"), A (A (C "Cons", V "y"), V "ys")))))
-
-end;
-
-
-use_show(NBE_Codegen.generate (the_context()) ("app",CodegenThingol.Fun(
-  [
-  ([CodegenThingol.IConst(("Nil",dummyIT),[])],
-    CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
-                        CodegenThingol.IVarE("ys",dummyIT))),
-
-   ([CodegenThingol.IApp(
-       CodegenThingol.IApp(
-         CodegenThingol.IConst(("Cons",dummyIT),[]),
-         CodegenThingol.IVarE("x",dummyIT)),
-       CodegenThingol.IVarE("xs",dummyIT))],
-    CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
-    CodegenThingol.IApp(
-       CodegenThingol.IApp(
-         CodegenThingol.IConst(("Cons",dummyIT),[]),
-         CodegenThingol.IVarE("x",dummyIT)),
-       CodegenThingol.IApp(
-         CodegenThingol.IApp(
-           CodegenThingol.IConst(("app",dummyIT),[]),
-           CodegenThingol.IVarE("xs",dummyIT)),
-         CodegenThingol.IVarE("ys",dummyIT)))))]
-  ,([],dummyIT))));
-
-
-let
-fun test a b = if a=b then () else error "oops!";
-
-val CNil = Const("Nil",dummyT);
-val CCons = Const("Cons",dummyT);
-val Cappend = Const("app",dummyT);
-val Fx = Free("x",dummyT);
-val Fy = Free("y",dummyT);
-val Fxs = Free("xs",dummyT);
-val Fys = Free("ys",dummyT);
-open NBE_Eval
-in
-test (nbe(CNil)) (C "Nil");
-test (nbe(CCons)) (C "Cons");
-test (nbe(Cappend)) (C "app");
-test (nbe(Cappend $ CNil)) (AbsN (1, B 1));
-test (nbe(Cappend $ CNil $ CNil)) (C "Nil");
-test (nbe(Cappend $ Fxs)) (A (C "app", V "xs"));
-test (nbe(Cappend $ Fxs $ Fys)) (A (A (C "app", V "xs"), V "ys"));
-test (nbe(Cappend $ CNil $ Fxs)) (V "xs");
-test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ Fys))
-     (A (A (C "Cons", V "x"), A (A (C "app", V "xs"), V "ys")));
-test (nbe(Cappend $ (CCons $ Fx $ Fxs))) 
-   (AbsN (1, A (A (C "Cons", V "x"), A (A (C "app", V "xs"), B 1))));
-test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ (CCons $ Fy $ Fys)))
-     (A (A (C "Cons", V "x"), A (A (C "app", V "xs"), A (A (C "Cons", V "y"), V "ys"))));
-test (nbe(Cappend $ (CCons $ Fx $ (CCons $ Fy $ Fxs)) $ (CCons$Fy$Fys)))
- (A
-      (A (C "Cons", V "x"),
-         A
-            (A (C "Cons", V "y"),
-               A (A (C "app", V "xs"), A (A (C "Cons", V "y"), V "ys")))));
-()
-end;
-
-
-use_show(NBE_Codegen.generate (the_context()) ("add",CodegenThingol.Fun(
-  [
-  ([CodegenThingol.IConst(("0",dummyIT),[])],
-    CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
-                        CodegenThingol.IVarE("n",dummyIT))),
-   ([CodegenThingol.IApp(
-       CodegenThingol.IConst(("S",dummyIT),[]),
-       CodegenThingol.IVarE("n",dummyIT))],
-    CodegenThingol.IAbs(CodegenThingol.IVarE("m",dummyIT),
-      CodegenThingol.IApp(
-         CodegenThingol.IConst(("S",dummyIT),[]),
-           CodegenThingol.IApp(
-             CodegenThingol.IApp(
-               CodegenThingol.IConst(("add",dummyIT),[]),
-               CodegenThingol.IVarE("n",dummyIT)),
-             CodegenThingol.IVarE("m",dummyIT)))))]
-  ,([],dummyIT))));
-
-
-let
-fun test a b = if a=b then () else error "oops!";
-
-val C0 = Const("0",dummyT);
-val CS = Const("S",dummyT);
-val Cadd = Const("add",dummyT);
-val Fx = Free("x",dummyT);
-val Fy = Free("y",dummyT);
-open NBE_Eval
-in
-test (nbe(Cadd $ C0)) (AbsN (1, B 1));
-test (nbe(Cadd $ C0 $ C0)) (C "0");
-test (nbe(Cadd $ (CS $ (CS $ (CS $ Fx))) $ (CS $ (CS $ (CS $ Fy)))))
-(A (C "S", A (C "S", A (C "S", A (A (C "add", V "x"), A (C "S", A (C "S", A (C "S", V "y")))))))
-)
-end;
-
-
-
-use_show(NBE_Codegen.generate (the_context()) ("mul",CodegenThingol.Fun(
-  [
-  ([CodegenThingol.IConst(("0",dummyIT),[])],
-    CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
-                        CodegenThingol.IConst(("0",dummyIT),[]))),
-   ([CodegenThingol.IApp(
-       CodegenThingol.IConst(("S",dummyIT),[]),
-       CodegenThingol.IVarE("n",dummyIT))],
-    CodegenThingol.IAbs(CodegenThingol.IVarE("m",dummyIT),
-      CodegenThingol.IApp(
-       CodegenThingol.IApp(
-         CodegenThingol.IConst(("add",dummyIT),[]),
-        CodegenThingol.IVarE("m",dummyIT)),
-           CodegenThingol.IApp(
-             CodegenThingol.IApp(
-               CodegenThingol.IConst(("mul",dummyIT),[]),
-               CodegenThingol.IVarE("n",dummyIT)),
-             CodegenThingol.IVarE("m",dummyIT)))))]
-  ,([],dummyIT))));
-
-
-let
-fun test a b = if a=b then () else error "oops!";
-
-val C0 = Const("0",dummyT);
-val CS = Const("S",dummyT);
-val Cmul = Const("mul",dummyT);
-val Fx = Free("x",dummyT);
-val Fy = Free("y",dummyT);
-open NBE_Eval
-in
-test (nbe(Cmul $ C0)) (AbsN (1, C "0"));
-test (nbe(Cmul $ C0 $ Fx)) (C "0");
-test (nbe(Cmul $ (CS $ (CS $ (CS $ C0)))))
-(AbsN (1, A (A (C "add", B 1), A (A (C "add", B 1), A (A (C "add", B 1), C "0")))));
-test (nbe(Cmul $ (CS $ (CS $ (CS $ Fx)))))
- (AbsN (1, A (A (C "add", B 1), A (A (C "add", B 1),
-                     A (A (C "add", B 1), A (A (C "mul", V "x"), B 1))))));
-test (nbe(Cmul $ (CS $ (CS $ Fx)) $ (CS $ (CS $ (CS $ Fy)))))
-(A (C "S", A(C "S",A(C "S",A(A (C "add", V "y"),A(C "S",A(C "S",A(C "S",A
- (A (C "add", V "y"),A(A (C "mul", V "x"),A(C "S",A(C "S",A(C "S", V"y")))))))))))));
-()
-end;
-*)